[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
b : β
⊢ (∃ a, a ∈ s.val ∧ ↑f a = b) ↔ ∃ a, a ∈ s ∧ ↑f a = b
[PROOFSTEP]
simp only [exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
b : β
⊢ (∃ a, a ∈ s.val ∧ ↑f a = b) ↔ ∃ a, a ∈ s ∧ ↑f a = b
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s : Finset α
f : α ≃ β
b : β
⊢ b ∈ map (Equiv.toEmbedding f) s ↔ ↑f.symm b ∈ s
[PROOFSTEP]
rw [mem_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s : Finset α
f : α ≃ β
b : β
⊢ (∃ a, a ∈ s ∧ ↑(Equiv.toEmbedding f) a = b) ↔ ↑f.symm b ∈ s
[PROOFSTEP]
exact
  ⟨by
    rintro ⟨a, H, rfl⟩
    simpa, fun h => ⟨_, h, by simp⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s : Finset α
f : α ≃ β
b : β
⊢ (∃ a, a ∈ s ∧ ↑(Equiv.toEmbedding f) a = b) → ↑f.symm b ∈ s
[PROOFSTEP]
rintro ⟨a, H, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s : Finset α
f : α ≃ β
a : α
H : a ∈ s
⊢ ↑f.symm (↑(Equiv.toEmbedding f) a) ∈ s
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s : Finset α
f : α ≃ β
b : β
h : ↑f.symm b ∈ s
⊢ ↑(Equiv.toEmbedding f) (↑f.symm b) = b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s✝ : Finset α
f : α ↪ β
s : Finset α
p : (a : β) → a ∈ map f s → Prop
h : ∀ (x : α) (H : x ∈ s), p (↑f x) (_ : ↑f x ∈ map f s)
x : β
hx : x ∈ map f s
⊢ p x hx
[PROOFSTEP]
obtain ⟨y, hy, rfl⟩ := mem_map.1 hx
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s✝ : Finset α
f : α ↪ β
s : Finset α
p : (a : β) → a ∈ map f s → Prop
h : ∀ (x : α) (H : x ∈ s), p (↑f x) (_ : ↑f x ∈ map f s)
y : α
hy : y ∈ s
hx : ↑f y ∈ map f s
⊢ p (↑f y) hx
[PROOFSTEP]
exact h _ hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s✝ : Finset α
f : α ↪ β
s : Finset α
⊢ ∀ (x : β), x ∈ ↑(map f s) ↔ x ∈ ↑f '' ↑s
[PROOFSTEP]
simp only [mem_coe, mem_map, Set.mem_image, implies_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s✝ : Finset α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
x✝ : β
⊢ x✝ ∈ map f (toFinset s) ↔ x✝ ∈ toFinset (Multiset.map (↑f) s)
[PROOFSTEP]
simp only [mem_map, Multiset.mem_map, exists_prop, Multiset.mem_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
x✝ : α
⊢ x✝ ∈ map (Embedding.refl α) s ↔ x✝ ∈ s
[PROOFSTEP]
simpa only [mem_map, exists_prop] using exists_eq_right
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
f : α✝ ↪ β✝
s✝ : Finset α✝
α β : Type u_4
h : α = β
s : Finset α
⊢ HEq (map (Equiv.toEmbedding (Equiv.cast h)) s) s
[PROOFSTEP]
subst h
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
f : α✝ ↪ β
s✝ : Finset α✝
α : Type u_4
s : Finset α
⊢ HEq (map (Equiv.toEmbedding (Equiv.cast (_ : α = α))) s) s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s✝ : Finset α
f : α ↪ β
g : β ↪ γ
s : Finset α
⊢ (map g (map f s)).val = (map (Embedding.trans f g) s).val
[PROOFSTEP]
simp only [map_val, Multiset.map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s✝ : Finset α
f : α ↪ β
g : β ↪ γ
s : Finset α
⊢ Multiset.map ((fun x => ↑g x) ∘ fun x => ↑f x) s.val = Multiset.map (fun x => ↑(Embedding.trans f g) x) s.val
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s : Finset α
β' : Type u_4
f : β ↪ γ
g : α ↪ β
f' : α ↪ β'
g' : β' ↪ γ
h_comm : ∀ (a : α), ↑f (↑g a) = ↑g' (↑f' a)
⊢ map f (map g s) = map g' (map f' s)
[PROOFSTEP]
simp_rw [map_map, Embedding.trans, Function.comp, h_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s s₁ s₂ : Finset α
h : s₁ ⊆ s₂
⊢ map f s₁ ⊆ map f s₂
[PROOFSTEP]
simp [subset_def, Multiset.map_subset_map h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s : Finset α
f : α ≃ β
p : α → Prop
inst✝ : DecidablePred p
⊢ map (Equiv.toEmbedding f) (filter p s) = filter (p ∘ ↑f.symm) (map (Equiv.toEmbedding f) s)
[PROOFSTEP]
simp only [filter_map, Function.comp, Equiv.toEmbedding_apply, Equiv.symm_apply_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s✝ s t : Finset α
f : α ↪ β
⊢ _root_.Disjoint (map f s) (map f t) ↔ _root_.Disjoint s t
[PROOFSTEP]
simp only [disjoint_iff_ne, mem_map, exists_prop, exists_imp, and_imp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s✝ s t : Finset α
f : α ↪ β
⊢ (∀ (a : β) (x : α), x ∈ s → ↑f x = a → ∀ (b : β) (x : α), x ∈ t → ↑f x = b → a ≠ b) ↔
    ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b
[PROOFSTEP]
refine' ⟨fun h a ha b hb hab => h _ _ ha rfl _ _ hb rfl <| congr_arg _ hab, _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s✝ s t : Finset α
f : α ↪ β
⊢ (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b) →
    ∀ (a : β) (x : α), x ∈ s → ↑f x = a → ∀ (b : β) (x : α), x ∈ t → ↑f x = b → a ≠ b
[PROOFSTEP]
rintro h _ a ha rfl _ b hb rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s✝ s t : Finset α
f : α ↪ β
h : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ ↑f a ≠ ↑f b
[PROOFSTEP]
exact f.injective.ne (h _ ha _ hb)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s : Finset α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α ↪ β
s₁ s₂ : Finset α
⊢ ↑(map f (s₁ ∪ s₂)) = ↑(map f s₁ ∪ map f s₂)
[PROOFSTEP]
simp only [coe_map, coe_union, Set.image_union]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s : Finset α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α ↪ β
s₁ s₂ : Finset α
⊢ ↑(map f (s₁ ∩ s₂)) = ↑(map f s₁ ∩ map f s₂)
[PROOFSTEP]
simp only [coe_map, coe_inter, Set.image_inter f.injective]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s : Finset α
f : α ↪ β
a : α
⊢ ↑(map f {a}) = ↑{↑f a}
[PROOFSTEP]
simp only [coe_map, coe_singleton, Set.image_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s✝ : Finset α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α ↪ β
a : α
s : Finset α
⊢ map f (insert a s) = insert (↑f a) (map f s)
[PROOFSTEP]
simp only [insert_eq, map_union, map_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s✝ : Finset α
f : α ↪ β
a : α
s : Finset α
ha : ¬a ∈ s
⊢ ¬↑f a ∈ map f s
[PROOFSTEP]
simpa using ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
⊢ Finset.Nonempty (map f s) ↔ Finset.Nonempty s
[PROOFSTEP]
rw [nonempty_iff_ne_empty, nonempty_iff_ne_empty, Ne.def, map_eq_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s✝ s : Finset α
⊢ (map (Embedding.subtype fun x => x ∈ s) (attach s)).val = s.val
[PROOFSTEP]
rw [map_val, attach_val]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s✝ s : Finset α
⊢ Multiset.map (↑(Embedding.subtype fun x => x ∈ s)) (Multiset.attach s.val) = s.val
[PROOFSTEP]
exact Multiset.attach_map_val _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
a b : ℕ
⊢ _root_.Disjoint (range a) (map (addLeftEmbedding a) (range b))
[PROOFSTEP]
refine' disjoint_iff_inf_le.mpr _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
a b : ℕ
⊢ range a ⊓ map (addLeftEmbedding a) (range b) ≤ ⊥
[PROOFSTEP]
intro k hk
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
a b k : ℕ
hk : k ∈ range a ⊓ map (addLeftEmbedding a) (range b)
⊢ k ∈ ⊥
[PROOFSTEP]
simp only [exists_prop, mem_range, inf_eq_inter, mem_map, addLeftEmbedding, mem_inter] at hk
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
a b k : ℕ
hk : k < a ∧ ∃ a_1, a_1 < b ∧ ↑{ toFun := fun h => a + h, inj' := (_ : Injective ((fun x x_1 => x + x_1) a)) } a_1 = k
⊢ k ∈ ⊥
[PROOFSTEP]
obtain ⟨a, _, ha⟩ := hk.2
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
a✝ b k : ℕ
hk : k < a✝ ∧ ∃ a, a < b ∧ ↑{ toFun := fun h => a✝ + h, inj' := (_ : Injective ((fun x x_1 => x + x_1) a✝)) } a = k
a : ℕ
left✝ : a < b
ha : ↑{ toFun := fun h => a✝ + h, inj' := (_ : Injective ((fun x x_1 => x + x_1) a✝)) } a = k
⊢ k ∈ ⊥
[PROOFSTEP]
simpa [← ha] using hk.1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
a b : ℕ
⊢ _root_.Disjoint (range a) (map (addRightEmbedding a) (range b))
[PROOFSTEP]
refine' disjoint_iff_inf_le.mpr _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
a b : ℕ
⊢ range a ⊓ map (addRightEmbedding a) (range b) ≤ ⊥
[PROOFSTEP]
intro k hk
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
a b k : ℕ
hk : k ∈ range a ⊓ map (addRightEmbedding a) (range b)
⊢ k ∈ ⊥
[PROOFSTEP]
simp only [exists_prop, mem_range, inf_eq_inter, mem_map, addRightEmbedding, mem_inter] at hk
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
a b k : ℕ
hk : k < a ∧ ∃ a_1, a_1 < b ∧ ↑{ toFun := fun h => h + a, inj' := (_ : Injective fun x => x + a) } a_1 = k
⊢ k ∈ ⊥
[PROOFSTEP]
obtain ⟨a, _, ha⟩ := hk.2
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
a✝ b k : ℕ
hk : k < a✝ ∧ ∃ a, a < b ∧ ↑{ toFun := fun h => h + a✝, inj' := (_ : Injective fun x => x + a✝) } a = k
a : ℕ
left✝ : a < b
ha : ↑{ toFun := fun h => h + a✝, inj' := (_ : Injective fun x => x + a✝) } a = k
⊢ k ∈ ⊥
[PROOFSTEP]
simpa [← ha] using hk.1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s✝ s : Finset α
t : α → Finset β
f : β ↪ γ
h : Set.PairwiseDisjoint (↑s) t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
x : γ
hxa : x ∈ (fun a => map f (t a)) a
hxb : x ∈ (fun a => map f (t a)) b
⊢ False
[PROOFSTEP]
obtain ⟨xa, hfa, rfl⟩ := mem_map.mp hxa
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s✝ s : Finset α
t : α → Finset β
f : β ↪ γ
h : Set.PairwiseDisjoint (↑s) t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
xa : β
hfa : xa ∈ t a
hxa : ↑f xa ∈ (fun a => map f (t a)) a
hxb : ↑f xa ∈ (fun a => map f (t a)) b
⊢ False
[PROOFSTEP]
obtain ⟨xb, hfb, hfab⟩ := mem_map.mp hxb
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s✝ s : Finset α
t : α → Finset β
f : β ↪ γ
h : Set.PairwiseDisjoint (↑s) t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
xa : β
hfa : xa ∈ t a
hxa : ↑f xa ∈ (fun a => map f (t a)) a
hxb : ↑f xa ∈ (fun a => map f (t a)) b
xb : β
hfb : xb ∈ t b
hfab : ↑f xb = ↑f xa
⊢ False
[PROOFSTEP]
obtain rfl := f.injective hfab
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α ↪ β
s✝ s : Finset α
t : α → Finset β
f : β ↪ γ
h : Set.PairwiseDisjoint (↑s) t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
xb : β
hfb : xb ∈ t b
hfa : xb ∈ t a
hxa : ↑f xb ∈ (fun a => map f (t a)) a
hxb : ↑f xb ∈ (fun a => map f (t a)) b
hfab : ↑f xb = ↑f xb
⊢ False
[PROOFSTEP]
exact disjoint_left.mp (h ha hb hab) hfa hfb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n i j : ℕ
⊢ (fun i => i + 1) i = (fun i => i + 1) j → i = j
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ range (n + 1) = insert 0 (map { toFun := fun i => i + 1, inj' := (_ : ∀ (i j : ℕ), i + 1 = j + 1 → i = j) } (range n))
[PROOFSTEP]
ext (⟨⟩ | ⟨n⟩)
[GOAL]
case a.zero
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ Nat.zero ∈ range (n + 1) ↔
    Nat.zero ∈ insert 0 (map { toFun := fun i => i + 1, inj' := (_ : ∀ (i j : ℕ), i + 1 = j + 1 → i = j) } (range n))
[PROOFSTEP]
simp [Nat.succ_eq_add_one, Nat.zero_lt_succ n]
[GOAL]
case a.succ
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ n : ℕ
⊢ Nat.succ n ∈ range (n✝ + 1) ↔
    Nat.succ n ∈ insert 0 (map { toFun := fun i => i + 1, inj' := (_ : ∀ (i j : ℕ), i + 1 = j + 1 → i = j) } (range n✝))
[PROOFSTEP]
simp [Nat.succ_eq_add_one, Nat.zero_lt_succ n]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
⊢ b ∈ image f s ↔ ∃ a, a ∈ s ∧ f a = b
[PROOFSTEP]
simp only [mem_def, image_val, mem_dedup, Multiset.mem_map, exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
p : β → Prop
⊢ (∀ (b : β), b ∈ image f s → p b) ↔ ∀ (a : α), a ∈ s → p (f a)
[PROOFSTEP]
simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
⊢ c ∈ image (const α b) s ↔ Finset.Nonempty s ∧ b = c
[PROOFSTEP]
rw [mem_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
⊢ (∃ a, a ∈ s ∧ const α b a = c) ↔ Finset.Nonempty s ∧ b = c
[PROOFSTEP]
simp only [exists_prop, const_apply, exists_and_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
⊢ (∃ x, x ∈ s) ∧ b = c ↔ Finset.Nonempty s ∧ b = c
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c✝ : β
c : α → β
p : β → Prop
inst✝ : CanLift β α c p
⊢ ∀ (x : Finset β), (∀ (x_1 : β), x_1 ∈ x → p x_1) → ∃ y, image c y = x
[PROOFSTEP]
rintro ⟨⟨l⟩, hd : l.Nodup⟩ hl
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c✝ : β
c : α → β
p : β → Prop
inst✝ : CanLift β α c p
val✝ : Multiset β
l : List β
hd : List.Nodup l
hl : ∀ (x : β), x ∈ { val := Quot.mk Setoid.r l, nodup := hd } → p x
⊢ ∃ y, image c y = { val := Quot.mk Setoid.r l, nodup := hd }
[PROOFSTEP]
lift l to List α using hl
[GOAL]
case mk.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c✝ : β
c : α → β
p : β → Prop
inst✝ : CanLift β α c p
val✝ : Multiset β
l : List α
hd : List.Nodup (List.map c l)
⊢ ∃ y, image c y = { val := Quot.mk Setoid.r (List.map c l), nodup := hd }
[PROOFSTEP]
exact ⟨⟨l, hd.of_map _⟩, ext fun a => by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a✝ : α
b c✝ : β
c : α → β
p : β → Prop
inst✝ : CanLift β α c p
val✝ : Multiset β
l : List α
hd : List.Nodup (List.map c l)
a : β
⊢ a ∈ image c { val := ↑l, nodup := (_ : List.Nodup l) } ↔ a ∈ { val := Quot.mk Setoid.r (List.map c l), nodup := hd }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
h : Set.EqOn f g ↑s
⊢ image f s = image g s
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
h : Set.EqOn f g ↑s
a✝ : β
⊢ a✝ ∈ image f s ↔ a✝ ∈ image g s
[PROOFSTEP]
simp_rw [mem_image, ← bex_def]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
h : Set.EqOn f g ↑s
a✝ : β
⊢ (∃ x x_1, f x = a✝) ↔ ∃ x x_1, g x = a✝
[PROOFSTEP]
exact bex_congr fun x hx => by rw [h hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
h : Set.EqOn f g ↑s
a✝ : β
x : α
hx : x ∈ s
⊢ f x = a✝ ↔ g x = a✝
[PROOFSTEP]
rw [h hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
hf : Injective f
⊢ f a ∈ image f s ↔ a ∈ s
[PROOFSTEP]
refine' ⟨fun h => _, Finset.mem_image_of_mem f⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
hf : Injective f
h : f a ∈ image f s
⊢ a ∈ s
[PROOFSTEP]
obtain ⟨y, hy, heq⟩ := mem_image.1 h
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
hf : Injective f
h : f a ∈ image f s
y : α
hy : y ∈ s
heq : f y = f a
⊢ a ∈ s
[PROOFSTEP]
exact hf heq ▸ hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
f : α → β
s : Finset α
t : Finset β
h : ∀ (x : α), x ∈ s → f x ∈ t
⊢ filter (fun y => y ∈ image f s) t = image f s
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
f : α → β
s : Finset α
t : Finset β
h : ∀ (x : α), x ∈ s → f x ∈ t
a✝ : β
⊢ a✝ ∈ filter (fun y => y ∈ image f s) t ↔ a✝ ∈ image f s
[PROOFSTEP]
simp only [mem_filter, mem_image, decide_eq_true_eq, and_iff_right_iff_imp, forall_exists_index, and_imp]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
f : α → β
s : Finset α
t : Finset β
h : ∀ (x : α), x ∈ s → f x ∈ t
a✝ : β
⊢ ∀ (x : α), x ∈ s → f x = a✝ → a✝ ∈ t
[PROOFSTEP]
rintro x xel rfl
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
f : α → β
s : Finset α
t : Finset β
h : ∀ (x : α), x ∈ s → f x ∈ t
x : α
xel : x ∈ s
⊢ f x ∈ t
[PROOFSTEP]
exact h _ xel
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a : α
b c : β
f : α → β
s : Finset α
y : β
⊢ Finset.Nonempty (filter (fun x => f x = y) s) ↔ y ∈ image f s
[PROOFSTEP]
simp [Finset.Nonempty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a : α
b c : β
f : α → β
⊢ ∀ (x : β), x ∈ ↑(image f s) ↔ x ∈ f '' ↑s
[PROOFSTEP]
simp only [mem_coe, mem_image, Set.mem_image, implies_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f g : α → β
s✝ : Finset α
t : Finset β
a : α
b c : β
inst✝ : DecidableEq α
s : Multiset α
x✝ : β
⊢ x✝ ∈ image f (toFinset s) ↔ x✝ ∈ toFinset (Multiset.map f s)
[PROOFSTEP]
simp only [mem_image, Multiset.mem_toFinset, exists_prop, Multiset.mem_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
inst✝ : DecidableEq α
x✝ : α
⊢ x✝ ∈ image id s ↔ x✝ ∈ s
[PROOFSTEP]
simp only [mem_image, exists_prop, id, exists_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f g✝ : α → β
s : Finset α
t : Finset β
a : α
b c : β
inst✝ : DecidableEq γ
g : β → γ
⊢ (image g (image f s)).val = (image (g ∘ f) s).val
[PROOFSTEP]
simp only [image_val, dedup_map_dedup_eq, Multiset.map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq β
f✝ g✝ : α → β
s : Finset α
t : Finset β
a : α
b c : β
β' : Type u_4
inst✝¹ : DecidableEq β'
inst✝ : DecidableEq γ
f : β → γ
g : α → β
f' : α → β'
g' : β' → γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ image f (image g s) = image g' (image f' s)
[PROOFSTEP]
simp_rw [image_image, comp, h_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
s₁ s₂ : Finset α
h : s₁ ⊆ s₂
⊢ image f s₁ ⊆ image f s₂
[PROOFSTEP]
simp only [subset_def, image_val, subset_dedup', dedup_subset', Multiset.map_subset_map h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
⊢ image f s ⊆ t ↔ f '' ↑s ⊆ ↑t
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t✝ : Finset β
a : α
b c : β
t : Finset α
hf : Injective f
⊢ image f s ⊆ image f t ↔ s ⊆ t
[PROOFSTEP]
simp_rw [← coe_subset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t✝ : Finset β
a : α
b c : β
t : Finset α
hf : Injective f
⊢ ↑(image f s) ⊆ ↑(image f t) ↔ ↑s ⊆ ↑t
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t✝ : Finset β
a : α
b c : β
t : Finset α
hf : Injective f
⊢ f '' ↑s ⊆ f '' ↑t ↔ ↑s ⊆ ↑t
[PROOFSTEP]
exact Set.image_subset_image_iff hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b✝ c : β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ b ∈ filter p (image f s) ↔ b ∈ image f (filter (p ∘ f) s)
[PROOFSTEP]
simp only [mem_filter, mem_image, exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b✝ c : β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a, a ∈ s ∧ f a = b) ∧ p b ↔ ∃ a, (a ∈ s ∧ (p ∘ f) a) ∧ f a = b
[PROOFSTEP]
exact ⟨by rintro ⟨⟨x, h1, rfl⟩, h2⟩; exact ⟨x, ⟨h1, h2⟩, rfl⟩, by rintro ⟨x, ⟨h1, h2⟩, rfl⟩; exact ⟨⟨x, h1, rfl⟩, h2⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b✝ c : β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a, a ∈ s ∧ f a = b) ∧ p b → ∃ a, (a ∈ s ∧ (p ∘ f) a) ∧ f a = b
[PROOFSTEP]
rintro ⟨⟨x, h1, rfl⟩, h2⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
p : β → Prop
inst✝ : DecidablePred p
x : α
h1 : x ∈ s
h2 : p (f x)
⊢ ∃ a, (a ∈ s ∧ (p ∘ f) a) ∧ f a = f x
[PROOFSTEP]
exact ⟨x, ⟨h1, h2⟩, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b✝ c : β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a, (a ∈ s ∧ (p ∘ f) a) ∧ f a = b) → (∃ a, a ∈ s ∧ f a = b) ∧ p b
[PROOFSTEP]
rintro ⟨x, ⟨h1, h2⟩, rfl⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
p : β → Prop
inst✝ : DecidablePred p
x : α
h1 : x ∈ s
h2 : (p ∘ f) x
⊢ (∃ a, a ∈ s ∧ f a = f x) ∧ p (f x)
[PROOFSTEP]
exact ⟨⟨x, h1, rfl⟩, h2⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a : α
b c : β
inst✝ : DecidableEq α
f : α → β
s₁ s₂ : Finset α
x✝ : β
⊢ x✝ ∈ image f (s₁ ∪ s₂) ↔ x✝ ∈ image f s₁ ∪ image f s₂
[PROOFSTEP]
simp only [mem_image, mem_union, exists_prop, or_and_right, exists_or]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
hf : Set.InjOn f (↑s ∪ ↑t)
⊢ ↑(image f (s ∩ t)) = ↑(image f s ∩ image f t)
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
hf : Set.InjOn f (↑s ∪ ↑t)
⊢ f '' (↑s ∩ ↑t) = f '' ↑s ∩ f '' ↑t
[PROOFSTEP]
exact Set.image_inter_on fun a ha b hb => hf (Or.inr ha) <| Or.inl hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a✝ : α
b c : β
f : α → β
a : α
x : β
⊢ x ∈ image f {a} ↔ x ∈ {f a}
[PROOFSTEP]
simpa only [mem_image, exists_prop, mem_singleton, exists_eq_left] using eq_comm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : α → β
a : α
s : Finset α
⊢ image f (insert a s) = insert (f a) (image f s)
[PROOFSTEP]
simp only [insert_eq, image_singleton, image_union]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : α → β
s : Finset α
a : α
⊢ erase (image f s) (f a) ⊆ image f (erase s a)
[PROOFSTEP]
simp only [subset_iff, and_imp, exists_prop, mem_image, exists_imp, mem_erase]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : α → β
s : Finset α
a : α
⊢ ∀ ⦃x : β⦄, x ≠ f a → ∀ (x_1 : α), x_1 ∈ s → f x_1 = x → ∃ a_4, (a_4 ≠ a ∧ a_4 ∈ s) ∧ f a_4 = x
[PROOFSTEP]
rintro b hb x hx rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : α → β
s : Finset α
a x : α
hx : x ∈ s
hb : f x ≠ f a
⊢ ∃ a_1, (a_1 ≠ a ∧ a_1 ∈ s) ∧ f a_1 = f x
[PROOFSTEP]
exact ⟨_, ⟨ne_of_apply_ne f hb, hx⟩, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : α → β
hf : Injective f
s : Finset α
a : α
⊢ image f (erase s a) = erase (image f s) (f a)
[PROOFSTEP]
refine' (erase_image_subset_image_erase _ _ _).antisymm' fun b => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b✝ c : β
inst✝ : DecidableEq α
f : α → β
hf : Injective f
s : Finset α
a : α
b : β
⊢ b ∈ image f (erase s a) → b ∈ erase (image f s) (f a)
[PROOFSTEP]
simp only [mem_image, exists_prop, mem_erase]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b✝ c : β
inst✝ : DecidableEq α
f : α → β
hf : Injective f
s : Finset α
a : α
b : β
⊢ (∃ a_1, (a_1 ≠ a ∧ a_1 ∈ s) ∧ f a_1 = b) → b ≠ f a ∧ ∃ a, a ∈ s ∧ f a = b
[PROOFSTEP]
rintro ⟨a', ⟨haa', ha'⟩, rfl⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : α → β
hf : Injective f
s : Finset α
a a' : α
haa' : a' ≠ a
ha' : a' ∈ s
⊢ f a' ≠ f a ∧ ∃ a, a ∈ s ∧ f a = f a'
[PROOFSTEP]
exact ⟨hf.ne haa', a', ha', rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
hf : Injective f
⊢ ↑(image f (s \ t)) = ↑(image f s \ image f t)
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
hf : Injective f
⊢ f '' (↑s \ ↑t) = f '' ↑s \ f '' ↑t
[PROOFSTEP]
exact Set.image_diff hf _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
hf : Injective f
⊢ ↑(image f (s ∆ t)) = ↑(image f s ∆ image f t)
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
hf : Injective f
⊢ f '' ↑s ∆ ↑t = (f '' ↑s) ∆ (f '' ↑t)
[PROOFSTEP]
exact Set.image_symmDiff hf _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ Set.range f ↔ a ∈ image (fun i => f i) (range n)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ Set.range f → a ∈ image (fun i => f i) (range n)
[PROOFSTEP]
rintro ⟨i, hi⟩
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
i : ℕ
hi : f i = a
⊢ a ∈ image (fun i => f i) (range n)
[PROOFSTEP]
simp only [mem_image, exists_prop, mem_range]
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
i : ℕ
hi : f i = a
⊢ ∃ a_1, a_1 < n ∧ f a_1 = a
[PROOFSTEP]
exact ⟨i % n, Nat.mod_lt i hn, (rfl.congr hi).mp (h i)⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ image (fun i => f i) (range n) → a ∈ Set.range f
[PROOFSTEP]
rintro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h✝ : ∀ (i : ℕ), f (i % n) = f i
h : a ∈ image (fun i => f i) (range n)
⊢ a ∈ Set.range f
[PROOFSTEP]
simp only [mem_image, exists_prop, Set.mem_range, mem_range] at *
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h✝ : ∀ (i : ℕ), f (i % n) = f i
h : ∃ a_1, a_1 < n ∧ f a_1 = a
⊢ ∃ y, f y = a
[PROOFSTEP]
rcases h with ⟨i, _, ha⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
i : ℕ
left✝ : i < n
ha : f i = a
⊢ ∃ y, f y = a
[PROOFSTEP]
exact ⟨i, ha⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % ↑n) = f i
hn' : 0 < ↑n
x✝ : ∃ i, f (i % ↑n) = a
i : ℤ
hi : f (i % ↑n) = a
this : 0 ≤ i % ↑n
⊢ Int.toNat (i % ↑n) < n ∧ f ↑(Int.toNat (i % ↑n)) = a
[PROOFSTEP]
rw [← Int.ofNat_lt, Int.toNat_of_nonneg this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % ↑n) = f i
hn' : 0 < ↑n
x✝ : ∃ i, f (i % ↑n) = a
i : ℤ
hi : f (i % ↑n) = a
this : 0 ≤ i % ↑n
⊢ i % ↑n < ↑n ∧ f (i % ↑n) = a
[PROOFSTEP]
exact ⟨Int.emod_lt_of_pos i hn', hi⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % ↑n) = f i
hn' : 0 < ↑n
x✝ : ∃ i, i < n ∧ f ↑i = a
i : ℕ
hi : i < n
ha : f ↑i = a
⊢ f (↑i % ↑n) = a
[PROOFSTEP]
rw [Int.emod_eq_of_lt (Int.ofNat_zero_le _) (Int.ofNat_lt_ofNat_of_lt hi), ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % ↑n) = f i
this : (∃ i, f (i % ↑n) = a) ↔ ∃ i, i < n ∧ f ↑i = a
⊢ a ∈ Set.range f ↔ a ∈ image (fun i => f ↑i) (range n)
[PROOFSTEP]
simpa [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a✝ : α
b✝ c : β
a b : ℕ
⊢ range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)
[PROOFSTEP]
rw [← val_inj, union_val]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a✝ : α
b✝ c : β
a b : ℕ
⊢ (range (a + b)).val = (range a).val ∪ (map (addLeftEmbedding a) (range b)).val
[PROOFSTEP]
exact Multiset.range_add_eq_union a b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f g : α → β
s✝ : Finset α
t : Finset β
a : α
b c : β
inst✝ : DecidableEq α
s : Finset α
⊢ (image Subtype.val (attach s)).val = s.val
[PROOFSTEP]
rw [image_val, attach_val, Multiset.attach_map_val, dedup_eq_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
s t : Finset α
f : α → β
hf : Injective f
⊢ _root_.Disjoint (image f s) (image f t) ↔ _root_.Disjoint s t
[PROOFSTEP]
convert disjoint_map ⟨_, hf⟩ using 1
[GOAL]
case h.e'_1.a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
s t : Finset α
f : α → β
hf : Injective f
⊢ _root_.Disjoint (image f s) (image f t) ↔
    _root_.Disjoint (map { toFun := f, inj' := hf } s) (map { toFun := f, inj' := hf } t)
[PROOFSTEP]
simp [map_eq_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s✝ : Finset α
t : Finset β
a : α
b✝ c : β
s : Finset α
h : Finset.Nonempty s
b b' : β
⊢ b' ∈ image (fun x => b) s ↔ b' ∈ {b}
[PROOFSTEP]
simp only [mem_image, exists_prop, exists_and_right, h.bex, true_and_iff, mem_singleton, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : α ↪ β
s : Finset α
a : α
⊢ map f (erase s a) = erase (map f s) (↑f a)
[PROOFSTEP]
simp_rw [map_eq_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq α
f : α ↪ β
s : Finset α
a : α
⊢ image (↑f) (erase s a) = erase (image (↑f) s) (↑f a)
[PROOFSTEP]
exact s.image_erase f.2 a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝¹ : Finset α
t✝ : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq γ
f : α → β
s✝ : Finset α
t : β → Finset γ
this : DecidableEq α
a : α
s : Finset α
x✝ : ¬a ∈ s
ih : Finset.biUnion (image f s) t = Finset.biUnion s fun a => t (f a)
⊢ Finset.biUnion (image f (insert a s)) t = Finset.biUnion (insert a s) fun a => t (f a)
[PROOFSTEP]
simp only [image_insert, biUnion_insert, ih]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝¹ : Finset α
t✝ : Finset β
a✝ : α
b c : β
inst✝ : DecidableEq γ
s✝ : Finset α
t : α → Finset β
f : β → γ
this : DecidableEq α
a : α
s : Finset α
x✝ : ¬a ∈ s
ih : image f (Finset.biUnion s t) = Finset.biUnion s fun a => image f (t a)
⊢ image f (Finset.biUnion (insert a s) t) = Finset.biUnion (insert a s) fun a => image f (t a)
[PROOFSTEP]
simp only [biUnion_insert, image_union, ih]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a : α
b c : β
f : α → β
x : β
⊢ (x ∈ Finset.biUnion s fun a => {f a}) ↔ x ∈ image f s
[PROOFSTEP]
simp only [mem_biUnion, mem_image, mem_singleton, eq_comm]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.123056
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
x : { x // x ∈ filter p s }
⊢ p ↑x
[PROOFSTEP]
simpa using (Finset.mem_filter.1 x.2).2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
a : α
ha : p a
⊢ { val := a, property := ha } ∈ Finset.subtype p s ↔ ↑{ val := a, property := ha } ∈ s
[PROOFSTEP]
simp [Finset.subtype, ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ Finset.subtype p s = ∅ ↔ ∀ (x : α), p x → ¬x ∈ s
[PROOFSTEP]
simp [ext_iff, Subtype.forall, Subtype.coe_mk]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ map (Embedding.subtype p) (Finset.subtype p s) = filter p s
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
x : α
⊢ x ∈ map (Embedding.subtype p) (Finset.subtype p s) ↔ x ∈ filter p s
[PROOFSTEP]
simp [@and_comm _ (_ = _), @and_left_comm _ (_ = _), @and_comm (p x) (x ∈ s)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
h : ∀ (x : α), x ∈ s → p x
⊢ ∀ (a : α), a ∈ map (Embedding.subtype p) (Finset.subtype p s) ↔ a ∈ s
[PROOFSTEP]
simpa [subtype_map] using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { x // p x }
a : α
h : a ∈ map (Embedding.subtype fun x => p x) s
⊢ p a
[PROOFSTEP]
rcases mem_map.1 h with ⟨x, _, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { x // p x }
x : { x // p x }
left✝ : x ∈ s
h : ↑(Embedding.subtype fun x => p x) x ∈ map (Embedding.subtype fun x => p x) s
⊢ p (↑(Embedding.subtype fun x => p x) x)
[PROOFSTEP]
exact x.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
t : Set α
s : Finset ↑t
⊢ ↑(map (Embedding.subtype fun x => x ∈ t) s) ⊆ t
[PROOFSTEP]
intro a ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
t : Set α
s : Finset ↑t
a : α
ha : a ∈ ↑(map (Embedding.subtype fun x => x ∈ t) s)
⊢ a ∈ t
[PROOFSTEP]
rw [mem_coe] at ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
t : Set α
s : Finset ↑t
a : α
ha : a ∈ map (Embedding.subtype fun x => x ∈ t) s
⊢ a ∈ t
[PROOFSTEP]
convert property_of_mem_map_subtype s ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
s : Finset ℕ
a : ℕ
ha : a < n
⊢ { val := a, isLt := ha } ∈ Finset.fin n s ↔ ↑{ val := a, isLt := ha } ∈ s
[PROOFSTEP]
simp [Finset.fin, ha, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
s t : Finset ℕ
h : s ≤ t
x : Fin n
⊢ x ∈ Finset.fin n s → x ∈ Finset.fin n t
[PROOFSTEP]
simpa using @h x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
s : Finset ℕ
⊢ map Fin.valEmbedding (Finset.fin n s) = filter (fun x => x < n) s
[PROOFSTEP]
simp [Finset.fin, Finset.map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ ↑t ⊆ f '' s ↔ ∃ s', ↑s' ⊆ s ∧ image f s' = t
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ ↑t ⊆ f '' s → ∃ s', ↑s' ⊆ s ∧ image f s' = t
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ (∃ s', ↑s' ⊆ s ∧ image f s' = t) → ↑t ⊆ f '' s
[PROOFSTEP]
swap
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ (∃ s', ↑s' ⊆ s ∧ image f s' = t) → ↑t ⊆ f '' s
[PROOFSTEP]
rintro ⟨t, ht, rfl⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s : Set α
f : α → β
t : Finset α
ht : ↑t ⊆ s
⊢ ↑(image f t) ⊆ f '' s
[PROOFSTEP]
rw [coe_image]
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s : Set α
f : α → β
t : Finset α
ht : ↑t ⊆ s
⊢ f '' ↑t ⊆ f '' s
[PROOFSTEP]
exact Set.image_subset f ht
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ ↑t ⊆ f '' s → ∃ s', ↑s' ⊆ s ∧ image f s' = t
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
h : ↑t ⊆ f '' s
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = t
[PROOFSTEP]
letI : CanLift β s (f ∘ (↑)) fun y => y ∈ f '' s := ⟨fun y ⟨x, hxt, hy⟩ => ⟨⟨x, hxt⟩, hy⟩⟩
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
h : ↑t ⊆ f '' s
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  {
    prf := fun y x =>
      match x with
      | Exists.intro x { left := hxt, right := hy } => Exists.intro { val := x, property := hxt } hy }
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = t
[PROOFSTEP]
lift t to Finset s using h
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  {
    prf := fun y x =>
      match x with
      | Exists.intro x { left := hxt, right := hy } => Exists.intro { val := x, property := hxt } hy }
t : Finset ↑s
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = image (f ∘ Subtype.val) t
[PROOFSTEP]
refine' ⟨t.map (Embedding.subtype _), map_subtype_subset _, _⟩
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  {
    prf := fun y x =>
      match x with
      | Exists.intro x { left := hxt, right := hy } => Exists.intro { val := x, property := hxt } hy }
t : Finset ↑s
⊢ image f (map (Embedding.subtype fun x => x ∈ s) t) = image (f ∘ Subtype.val) t
[PROOFSTEP]
ext y
[GOAL]
case mp.intro.a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s :=
  {
    prf := fun y x =>
      match x with
      | Exists.intro x { left := hxt, right := hy } => Exists.intro { val := x, property := hxt } hy }
t : Finset ↑s
y : β
⊢ y ∈ image f (map (Embedding.subtype fun x => x ∈ s) t) ↔ y ∈ image (f ∘ Subtype.val) t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ range (n + 1) \ {0} = image Nat.succ (range n)
[PROOFSTEP]
induction' n with k hk
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ range (Nat.zero + 1) \ {0} = image Nat.succ (range Nat.zero)
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ range (Nat.succ k + 1) \ {0} = image Nat.succ (range (Nat.succ k))
[PROOFSTEP]
conv_rhs => rw [range_succ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
| image Nat.succ (range (Nat.succ k))
[PROOFSTEP]
rw [range_succ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
| image Nat.succ (range (Nat.succ k))
[PROOFSTEP]
rw [range_succ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
| image Nat.succ (range (Nat.succ k))
[PROOFSTEP]
rw [range_succ]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ range (Nat.succ k + 1) \ {0} = image Nat.succ (insert k (range k))
[PROOFSTEP]
rw [range_succ, image_insert, ← hk, insert_sdiff_of_not_mem]
[GOAL]
case succ.h
α : Type u_1
β : Type u_2
γ : Type u_3
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ ¬k + 1 ∈ {0}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
s : Finset α
⊢ (fun s => Finset.map (Equiv.toEmbedding e.symm) s) ((fun s => Finset.map (Equiv.toEmbedding e) s) s) = s
[PROOFSTEP]
simp [Finset.map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
s : Finset β
⊢ (fun s => Finset.map (Equiv.toEmbedding e) s) ((fun s => Finset.map (Equiv.toEmbedding e.symm) s) s) = s
[PROOFSTEP]
simp [Finset.map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ Equiv.finsetCongr (Equiv.refl α) = Equiv.refl (Finset α)
[PROOFSTEP]
ext
[GOAL]
case H.a
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : Finset α
a✝ : α
⊢ a✝ ∈ ↑(Equiv.finsetCongr (Equiv.refl α)) x✝ ↔ a✝ ∈ ↑(Equiv.refl (Finset α)) x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
e' : β ≃ γ
⊢ (Equiv.finsetCongr e).trans (Equiv.finsetCongr e') = Equiv.finsetCongr (e.trans e')
[PROOFSTEP]
ext
[GOAL]
case H.a
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
e' : β ≃ γ
x✝ : Finset α
a✝ : γ
⊢ a✝ ∈ ↑((Equiv.finsetCongr e).trans (Equiv.finsetCongr e')) x✝ ↔ a✝ ∈ ↑(Equiv.finsetCongr (e.trans e')) x✝
[PROOFSTEP]
simp [-Finset.mem_map, -Equiv.trans_toEmbedding]


[GOAL]
n : ℕ
x : ℕ × ℕ
⊢ x ∈ antidiagonal n ↔ x.fst + x.snd = n
[PROOFSTEP]
rw [antidiagonal, mem_def, Multiset.Nat.mem_antidiagonal]
[GOAL]
n : ℕ
⊢ card (antidiagonal n) = n + 1
[PROOFSTEP]
simp [antidiagonal]
[GOAL]
n : ℕ
⊢ ¬(0, n + 1) ∈
      map (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)) (antidiagonal n)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ antidiagonal (n + 1) =
    cons (0, n + 1)
      (map (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)) (antidiagonal n))
      (_ :
        ¬(0, n + 1) ∈
            map (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ))
              (antidiagonal n))
[PROOFSTEP]
apply eq_of_veq
[GOAL]
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (cons (0, n + 1)
        (map (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)) (antidiagonal n))
        (_ :
          ¬(0, n + 1) ∈
              map (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ))
                (antidiagonal n))).val
[PROOFSTEP]
rw [cons_val, map_val]
[GOAL]
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (0, n + 1) ::ₘ
      Multiset.map (↑(Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)))
        (antidiagonal n).val
[PROOFSTEP]
apply Multiset.Nat.antidiagonal_succ
[GOAL]
n : ℕ
⊢ ¬(n + 1, 0) ∈
      map (Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ antidiagonal (n + 1) =
    cons (n + 1, 0)
      (map (Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n))
      (_ :
        ¬(n + 1, 0) ∈
            map (Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective })
              (antidiagonal n))
[PROOFSTEP]
apply eq_of_veq
[GOAL]
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (cons (n + 1, 0)
        (map (Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n))
        (_ :
          ¬(n + 1, 0) ∈
              map (Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective })
                (antidiagonal n))).val
[PROOFSTEP]
rw [cons_val, map_val]
[GOAL]
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (n + 1, 0) ::ₘ
      Multiset.map (↑(Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective }))
        (antidiagonal n).val
[PROOFSTEP]
exact Multiset.Nat.antidiagonal_succ'
[GOAL]
n : ℕ
⊢ ¬(n + 2, 0) ∈
      map
        (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
          { toFun := Nat.succ, inj' := Nat.succ_injective })
        (antidiagonal n)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ ¬(0, n + 2) ∈
      cons (n + 2, 0)
        (map
          (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
            { toFun := Nat.succ, inj' := Nat.succ_injective })
          (antidiagonal n))
        (_ :
          ¬(n + 2, 0) ∈
              map
                (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
                  { toFun := Nat.succ, inj' := Nat.succ_injective })
                (antidiagonal n))
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ antidiagonal (n + 2) =
    cons (0, n + 2)
      (cons (n + 2, 0)
        (map
          (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
            { toFun := Nat.succ, inj' := Nat.succ_injective })
          (antidiagonal n))
        (_ :
          ¬(n + 2, 0) ∈
              map
                (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
                  { toFun := Nat.succ, inj' := Nat.succ_injective })
                (antidiagonal n)))
      (_ :
        ¬(0, n + 2) ∈
            cons (n + 2, 0)
              (map
                (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
                  { toFun := Nat.succ, inj' := Nat.succ_injective })
                (antidiagonal n))
              (_ :
                ¬(n + 2, 0) ∈
                    map
                      (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
                        { toFun := Nat.succ, inj' := Nat.succ_injective })
                      (antidiagonal n)))
[PROOFSTEP]
simp_rw [antidiagonal_succ (n + 1), antidiagonal_succ', Finset.map_cons, map_map]
[GOAL]
n : ℕ
⊢ cons (0, n + 1 + 1)
      (cons (↑(Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)) (n + 1, 0))
        (map
          (Embedding.trans (Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective })
            (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)))
          (antidiagonal n))
        (_ :
          ¬↑(Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)) (n + 1, 0) ∈
              map
                (Embedding.trans
                  (Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective })
                  (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)))
                (antidiagonal n)))
      (_ :
        ¬(0, n + 1 + 1) ∈
            cons (↑(Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)) (n + 1, 0))
              (map
                (Embedding.trans
                  (Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective })
                  (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)))
                (antidiagonal n))
              (_ :
                ¬↑(Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)) (n + 1, 0) ∈
                    map
                      (Embedding.trans
                        (Embedding.prodMap (Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective })
                        (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ)))
                      (antidiagonal n))) =
    cons (0, n + 2)
      (cons (n + 2, 0)
        (map
          (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
            { toFun := Nat.succ, inj' := Nat.succ_injective })
          (antidiagonal n))
        (_ :
          ¬(n + 2, 0) ∈
              map
                (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
                  { toFun := Nat.succ, inj' := Nat.succ_injective })
                (antidiagonal n)))
      (_ :
        ¬(0, n + 2) ∈
            cons (n + 2, 0)
              (map
                (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
                  { toFun := Nat.succ, inj' := Nat.succ_injective })
                (antidiagonal n))
              (_ :
                ¬(n + 2, 0) ∈
                    map
                      (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }
                        { toFun := Nat.succ, inj' := Nat.succ_injective })
                      (antidiagonal n)))
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ (map { toFun := Prod.swap, inj' := (_ : Injective Prod.swap) } (antidiagonal n)).val = (antidiagonal n).val
[PROOFSTEP]
simp [antidiagonal, Multiset.Nat.map_swap_antidiagonal]
[GOAL]
n : ℕ
p q : ℕ × ℕ
hp : p ∈ antidiagonal n
hq : q ∈ antidiagonal n
⊢ p = q ↔ p.fst = q.fst
[PROOFSTEP]
refine' ⟨congr_arg Prod.fst, fun h ↦ Prod.ext h ((add_right_inj q.fst).mp _)⟩
[GOAL]
n : ℕ
p q : ℕ × ℕ
hp : p ∈ antidiagonal n
hq : q ∈ antidiagonal n
h : p.fst = q.fst
⊢ q.fst + p.snd = q.fst + q.snd
[PROOFSTEP]
rw [mem_antidiagonal] at hp hq
[GOAL]
n : ℕ
p q : ℕ × ℕ
hp : p.fst + p.snd = n
hq : q.fst + q.snd = n
h : p.fst = q.fst
⊢ q.fst + p.snd = q.fst + q.snd
[PROOFSTEP]
rw [hq, ← h, hp]
[GOAL]
n : ℕ
kl : ℕ × ℕ
hlk : kl ∈ antidiagonal n
⊢ kl.fst ≤ n
[PROOFSTEP]
rw [le_iff_exists_add]
[GOAL]
n : ℕ
kl : ℕ × ℕ
hlk : kl ∈ antidiagonal n
⊢ ∃ c, n = kl.fst + c
[PROOFSTEP]
use kl.2
[GOAL]
case h
n : ℕ
kl : ℕ × ℕ
hlk : kl ∈ antidiagonal n
⊢ n = kl.fst + kl.snd
[PROOFSTEP]
rwa [mem_antidiagonal, eq_comm] at hlk
[GOAL]
n : ℕ
kl : ℕ × ℕ
hlk : kl ∈ antidiagonal n
⊢ kl.snd ≤ n
[PROOFSTEP]
rw [le_iff_exists_add]
[GOAL]
n : ℕ
kl : ℕ × ℕ
hlk : kl ∈ antidiagonal n
⊢ ∃ c, n = kl.snd + c
[PROOFSTEP]
use kl.1
[GOAL]
case h
n : ℕ
kl : ℕ × ℕ
hlk : kl ∈ antidiagonal n
⊢ n = kl.snd + kl.fst
[PROOFSTEP]
rwa [mem_antidiagonal, eq_comm, add_comm] at hlk
[GOAL]
n m : ℕ
⊢ filter (fun x => x.fst = m) (antidiagonal n) = if m ≤ n then {(m, n - m)} else ∅
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
n m x y : ℕ
⊢ (x, y) ∈ filter (fun x => x.fst = m) (antidiagonal n) ↔ (x, y) ∈ if m ≤ n then {(m, n - m)} else ∅
[PROOFSTEP]
simp only [mem_filter, Nat.mem_antidiagonal]
[GOAL]
case a.mk
n m x y : ℕ
⊢ x + y = n ∧ x = m ↔ (x, y) ∈ if m ≤ n then {(m, n - m)} else ∅
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n m x y : ℕ
h : m ≤ n
⊢ x + y = n ∧ x = m ↔ (x, y) ∈ {(m, n - m)}
[PROOFSTEP]
simp (config := { contextual := true }) [and_comm, eq_tsub_iff_add_eq_of_le h, add_comm]
[GOAL]
case neg
n m x y : ℕ
h : ¬m ≤ n
⊢ x + y = n ∧ x = m ↔ (x, y) ∈ ∅
[PROOFSTEP]
rw [not_le] at h
[GOAL]
case neg
n m x y : ℕ
h : n < m
⊢ x + y = n ∧ x = m ↔ (x, y) ∈ ∅
[PROOFSTEP]
simp only [not_mem_empty, iff_false_iff, not_and, decide_eq_true_eq]
[GOAL]
case neg
n m x y : ℕ
h : n < m
⊢ x + y = n → ¬x = m
[PROOFSTEP]
exact fun hn => ne_of_lt (lt_of_le_of_lt (le_self_add.trans hn.le) h)
[GOAL]
n m : ℕ
⊢ filter (fun x => x.snd = m) (antidiagonal n) = if m ≤ n then {(n - m, m)} else ∅
[PROOFSTEP]
have : (fun x : ℕ × ℕ ↦ (x.snd = m)) ∘ Prod.swap = fun x : ℕ × ℕ ↦ x.fst = m := by ext; simp
[GOAL]
n m : ℕ
⊢ (fun x => x.snd = m) ∘ Prod.swap = fun x => x.fst = m
[PROOFSTEP]
ext
[GOAL]
case h.a
n m : ℕ
x✝ : ℕ × ℕ
⊢ ((fun x => x.snd = m) ∘ Prod.swap) x✝ ↔ x✝.fst = m
[PROOFSTEP]
simp
[GOAL]
n m : ℕ
this : (fun x => x.snd = m) ∘ Prod.swap = fun x => x.fst = m
⊢ filter (fun x => x.snd = m) (antidiagonal n) = if m ≤ n then {(n - m, m)} else ∅
[PROOFSTEP]
rw [← map_swap_antidiagonal, filter_map]
[GOAL]
n m : ℕ
this : (fun x => x.snd = m) ∘ Prod.swap = fun x => x.fst = m
⊢ map { toFun := Prod.swap, inj' := (_ : Injective Prod.swap) }
      (filter ((fun x => x.snd = m) ∘ ↑{ toFun := Prod.swap, inj' := (_ : Injective Prod.swap) }) (antidiagonal n)) =
    if m ≤ n then {(n - m, m)} else ∅
[PROOFSTEP]
simp [this, filter_fst_eq_antidiagonal, apply_ite (Finset.map _)]
[GOAL]
n k : ℕ
h : k ≤ n
⊢ filter (fun a => a.snd ≤ k) (antidiagonal n) =
    map
      (Embedding.prodMap { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) }
        (Embedding.refl ℕ))
      (antidiagonal k)
[PROOFSTEP]
ext ⟨i, j⟩
[GOAL]
case a.mk
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (i, j) ∈ filter (fun a => a.snd ≤ k) (antidiagonal n) ↔
    (i, j) ∈
      map
        (Embedding.prodMap { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) }
          (Embedding.refl ℕ))
        (antidiagonal k)
[PROOFSTEP]
suffices : i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i
[GOAL]
case a.mk
n k : ℕ
h : k ≤ n
i j : ℕ
this : i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i
⊢ (i, j) ∈ filter (fun a => a.snd ≤ k) (antidiagonal n) ↔
    (i, j) ∈
      map
        (Embedding.prodMap { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) }
          (Embedding.refl ℕ))
        (antidiagonal k)
[PROOFSTEP]
simpa
[GOAL]
case this
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i
[PROOFSTEP]
refine' ⟨fun hi ↦ ⟨k - j, tsub_add_cancel_of_le hi.2, _⟩, _⟩
[GOAL]
case this.refine'_1
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ j ≤ k
⊢ k - j + (n - k) = i
[PROOFSTEP]
rw [add_comm, tsub_add_eq_add_tsub h, ← hi.1, add_assoc, Nat.add_sub_of_le hi.2, add_tsub_cancel_right]
[GOAL]
case this.refine'_2
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (∃ a, a + j = k ∧ a + (n - k) = i) → i + j = n ∧ j ≤ k
[PROOFSTEP]
rintro ⟨l, hl, rfl⟩
[GOAL]
case this.refine'_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ l + (n - k) + j = n ∧ j ≤ k
[PROOFSTEP]
refine' ⟨_, hl ▸ Nat.le_add_left j l⟩
[GOAL]
case this.refine'_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ l + (n - k) + j = n
[PROOFSTEP]
rw [add_assoc, add_comm, add_assoc, add_comm j l, hl]
[GOAL]
case this.refine'_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ n - k + k = n
[PROOFSTEP]
exact Nat.sub_add_cancel h
[GOAL]
n k : ℕ
h : k ≤ n
⊢ filter (fun a => a.fst ≤ k) (antidiagonal n) =
    map
      (Embedding.prodMap (Embedding.refl ℕ)
        { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) })
      (antidiagonal k)
[PROOFSTEP]
have aux₁ : (fun a ↦ a.fst ≤ k) = (fun a ↦ a.snd ≤ k) ∘ (Equiv.prodComm ℕ ℕ).symm := rfl
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => a.fst ≤ k) = (fun a => a.snd ≤ k) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
⊢ filter (fun a => a.fst ≤ k) (antidiagonal n) =
    map
      (Embedding.prodMap (Embedding.refl ℕ)
        { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) })
      (antidiagonal k)
[PROOFSTEP]
have aux₂ : ∀ i j, (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j :=
  fun i j ↦ by rw [exists_comm]; exact exists₂_congr (fun a b ↦ by rw [add_comm])
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => a.fst ≤ k) = (fun a => a.snd ≤ k) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
i j : ℕ
⊢ (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
[PROOFSTEP]
rw [exists_comm]
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => a.fst ≤ k) = (fun a => a.snd ≤ k) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
i j : ℕ
⊢ (∃ b a, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
[PROOFSTEP]
exact exists₂_congr (fun a b ↦ by rw [add_comm])
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => a.fst ≤ k) = (fun a => a.snd ≤ k) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
i j a b : ℕ
⊢ b + a = k ∧ a = i ∧ b + (n - k) = j ↔ a + b = k ∧ a = i ∧ b + (n - k) = j
[PROOFSTEP]
rw [add_comm]
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => a.fst ≤ k) = (fun a => a.snd ≤ k) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
⊢ filter (fun a => a.fst ≤ k) (antidiagonal n) =
    map
      (Embedding.prodMap (Embedding.refl ℕ)
        { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) })
      (antidiagonal k)
[PROOFSTEP]
rw [← map_prodComm_antidiagonal]
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => a.fst ≤ k) = (fun a => a.snd ≤ k) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
⊢ filter (fun a => a.fst ≤ k) (map (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) (antidiagonal n)) =
    map
      (Embedding.prodMap (Embedding.refl ℕ)
        { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) })
      (antidiagonal k)
[PROOFSTEP]
simp_rw [aux₁, ← map_filter, antidiagonal_filter_snd_le_of_le h, map_map]
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => a.fst ≤ k) = (fun a => a.snd ≤ k) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
⊢ map
      (Embedding.trans
        (Embedding.prodMap { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) }
          (Embedding.refl ℕ))
        (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)))
      (antidiagonal k) =
    map
      (Embedding.prodMap (Embedding.refl ℕ)
        { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) })
      (antidiagonal k)
[PROOFSTEP]
ext ⟨i, j⟩
[GOAL]
case a.mk
n k : ℕ
h : k ≤ n
aux₁ : (fun a => a.fst ≤ k) = (fun a => a.snd ≤ k) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
i j : ℕ
⊢ (i, j) ∈
      map
        (Embedding.trans
          (Embedding.prodMap { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) }
            (Embedding.refl ℕ))
          (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)))
        (antidiagonal k) ↔
    (i, j) ∈
      map
        (Embedding.prodMap (Embedding.refl ℕ)
          { toFun := fun x => x + (n - k), inj' := (_ : Injective fun x => x + (n - k)) })
        (antidiagonal k)
[PROOFSTEP]
simpa using aux₂ i j
[GOAL]
n k : ℕ
h : k ≤ n
⊢ filter (fun a => k ≤ a.fst) (antidiagonal n) =
    map (Embedding.prodMap { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) } (Embedding.refl ℕ))
      (antidiagonal (n - k))
[PROOFSTEP]
ext ⟨i, j⟩
[GOAL]
case a.mk
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (i, j) ∈ filter (fun a => k ≤ a.fst) (antidiagonal n) ↔
    (i, j) ∈
      map (Embedding.prodMap { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) } (Embedding.refl ℕ))
        (antidiagonal (n - k))
[PROOFSTEP]
suffices : i + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i
[GOAL]
case a.mk
n k : ℕ
h : k ≤ n
i j : ℕ
this : i + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i
⊢ (i, j) ∈ filter (fun a => k ≤ a.fst) (antidiagonal n) ↔
    (i, j) ∈
      map (Embedding.prodMap { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) } (Embedding.refl ℕ))
        (antidiagonal (n - k))
[PROOFSTEP]
simpa
[GOAL]
case this
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ i + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i
[PROOFSTEP]
refine' ⟨fun hi ↦ ⟨i - k, _, tsub_add_cancel_of_le hi.2⟩, _⟩
[GOAL]
case this.refine'_1
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ k ≤ i
⊢ i - k + j = n - k
[PROOFSTEP]
rw [← Nat.sub_add_comm hi.2, hi.1]
[GOAL]
case this.refine'_2
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (∃ a, a + j = n - k ∧ a + k = i) → i + j = n ∧ k ≤ i
[PROOFSTEP]
rintro ⟨l, hl, rfl⟩
[GOAL]
case this.refine'_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ l + k + j = n ∧ k ≤ l + k
[PROOFSTEP]
refine' ⟨_, Nat.le_add_left k l⟩
[GOAL]
case this.refine'_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ l + k + j = n
[PROOFSTEP]
rw [add_right_comm, hl]
[GOAL]
case this.refine'_2.intro.intro
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ n - k + k = n
[PROOFSTEP]
exact tsub_add_cancel_of_le h
[GOAL]
n k : ℕ
h : k ≤ n
⊢ filter (fun a => k ≤ a.snd) (antidiagonal n) =
    map (Embedding.prodMap (Embedding.refl ℕ) { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) })
      (antidiagonal (n - k))
[PROOFSTEP]
have aux₁ : (fun a ↦ k ≤ a.snd) = (fun a ↦ k ≤ a.fst) ∘ (Equiv.prodComm ℕ ℕ).symm := rfl
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.snd) = (fun a => k ≤ a.fst) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
⊢ filter (fun a => k ≤ a.snd) (antidiagonal n) =
    map (Embedding.prodMap (Embedding.refl ℕ) { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) })
      (antidiagonal (n - k))
[PROOFSTEP]
have aux₂ : ∀ i j, (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j := fun i j ↦ by
  rw [exists_comm]; exact exists₂_congr (fun a b ↦ by rw [add_comm])
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.snd) = (fun a => k ≤ a.fst) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
i j : ℕ
⊢ (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
[PROOFSTEP]
rw [exists_comm]
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.snd) = (fun a => k ≤ a.fst) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
i j : ℕ
⊢ (∃ b a, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
[PROOFSTEP]
exact exists₂_congr (fun a b ↦ by rw [add_comm])
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.snd) = (fun a => k ≤ a.fst) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
i j a b : ℕ
⊢ b + a = n - k ∧ a = i ∧ b + k = j ↔ a + b = n - k ∧ a = i ∧ b + k = j
[PROOFSTEP]
rw [add_comm]
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.snd) = (fun a => k ≤ a.fst) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
⊢ filter (fun a => k ≤ a.snd) (antidiagonal n) =
    map (Embedding.prodMap (Embedding.refl ℕ) { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) })
      (antidiagonal (n - k))
[PROOFSTEP]
rw [← map_prodComm_antidiagonal]
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.snd) = (fun a => k ≤ a.fst) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
⊢ filter (fun a => k ≤ a.snd) (map (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) (antidiagonal n)) =
    map (Embedding.prodMap (Embedding.refl ℕ) { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) })
      (antidiagonal (n - k))
[PROOFSTEP]
simp_rw [aux₁, ← map_filter, antidiagonal_filter_le_fst_of_le h, map_map]
[GOAL]
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.snd) = (fun a => k ≤ a.fst) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
⊢ map
      (Embedding.trans
        (Embedding.prodMap { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) } (Embedding.refl ℕ))
        (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)))
      (antidiagonal (n - k)) =
    map (Embedding.prodMap (Embedding.refl ℕ) { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) })
      (antidiagonal (n - k))
[PROOFSTEP]
ext ⟨i, j⟩
[GOAL]
case a.mk
n k : ℕ
h : k ≤ n
aux₁ : (fun a => k ≤ a.snd) = (fun a => k ≤ a.fst) ∘ ↑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
i j : ℕ
⊢ (i, j) ∈
      map
        (Embedding.trans
          (Embedding.prodMap { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) } (Embedding.refl ℕ))
          (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)))
        (antidiagonal (n - k)) ↔
    (i, j) ∈
      map (Embedding.prodMap (Embedding.refl ℕ) { toFun := fun x => x + k, inj' := (_ : Injective fun x => x + k) })
        (antidiagonal (n - k))
[PROOFSTEP]
simpa using aux₂ i j
[GOAL]
⊢ LeftInverse
    (fun x => { fst := x.fst + x.snd, snd := { val := x, property := (_ : x ∈ antidiagonal (x.fst + x.snd)) } })
    fun x => ↑x.snd
[PROOFSTEP]
rintro ⟨n, ⟨k, l⟩, h⟩
[GOAL]
case mk.mk.mk
n k l : ℕ
h : (k, l) ∈ antidiagonal n
⊢ (fun x => { fst := x.fst + x.snd, snd := { val := x, property := (_ : x ∈ antidiagonal (x.fst + x.snd)) } })
      ((fun x => ↑x.snd) { fst := n, snd := { val := (k, l), property := h } }) =
    { fst := n, snd := { val := (k, l), property := h } }
[PROOFSTEP]
rw [mem_antidiagonal] at h
[GOAL]
case mk.mk.mk
n k l : ℕ
h✝ : (k, l) ∈ antidiagonal n
h : (k, l).fst + (k, l).snd = n
⊢ (fun x => { fst := x.fst + x.snd, snd := { val := x, property := (_ : x ∈ antidiagonal (x.fst + x.snd)) } })
      ((fun x => ↑x.snd) { fst := n, snd := { val := (k, l), property := h✝ } }) =
    { fst := n, snd := { val := (k, l), property := h✝ } }
[PROOFSTEP]
exact Sigma.subtype_ext h rfl