awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
s : Finset β
f : β → α
h : s.Nonempty
y : α
hy : (image f s).max = (↑y : WithBot α)
⊢ ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x
have rcases : ∀ (x : β) (hx : x ∈ s) (hy : (image f s).max = (↑(f x) : WithBot α)), ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x
Tactic: rcases mem_image.mp (mem_of_max hy) with ⟨x, hx, rfl⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
⊢ IsGLB (↑s : Set α) i ↔ IsLeast (↑s : Set α) i
have refine : ∀ (his : IsGLB (↑s : Set α) i), IsLeast (↑s : Set α) i
Tactic: refine ⟨fun his => ?_, IsLeast.isGLB⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s : Set α) i
this : i = s.min' hs
⊢ IsLeast (↑s : Set α) i
have rw : IsLeast (↑s : Set α) (s.min' hs)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s : Set α) i
⊢ IsLeast (↑s : Set α) i
have suffices : i = s.min' hs
Tactic: suffices i = min' s hs by
    rw [this]
    exact isLeast_min' s hs
-- Lean 4 proof step from Mathlib.Data.Finset.Max (hypothesis)
Goal:
α : Type u_2
inst : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s : Set α) i
⊢ i = s.min' hs
have his₁ : (∀ x ∈ (↑s : Set α), i ≤ x) ∧ ∀ x ∈ lowerBounds (↑s : Set α), x ≤ i
Tactic: rw [IsGLB, IsGreatest, mem_lowerBounds, mem_upperBounds] at his
Cleared hypotheses: his
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_7
R : Type u_8
inst : LinearOrder R
f : α → R
s : Multiset α
hs : s ≠ 0
⊢ ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y
have obtain : ∀ (y : α) (hys : y ∈ s.toFinset) (hy : ∀ x' ∈ s.toFinset, f x' ≤ f y), ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y
Tactic: obtain ⟨y, hys, hy⟩ := Finset.exists_max_image s.toFinset f (toFinset_nonempty.mpr hs)
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_7
R : Type u_8
inst : LinearOrder R
f : α → R
s : Multiset α
hs : s ≠ 0
⊢ ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y
have obtain : ∀ (y : α) (hys : y ∈ s.toFinset) (hy : ∀ x' ∈ s.toFinset, f x' ≤ f y), ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y
Tactic: classical
  obtain ⟨y, hys, hy⟩ := Finset.exists_max_image s.toFinset f (toFinset_nonempty.mpr hs)
  exact ⟨y, mem_toFinset.mp hys, fun _ hz ↦ hy _ (mem_toFinset.mpr hz)⟩
-- Lean 4 proof step from Mathlib.Data.Finset.MulAntidiagonal (goal)
Goal:
α : Type u_1
s t : Set α
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
hs : s.IsPWO
ht : t.IsPWO
⊢ (s * t).IsPWO
have rw : IsPWO (α := α) ((fun (x : α × α) ↦ x.1 * x.2) '' s ×ˢ t)
Tactic: rw [← image_mul_prod]
-- Lean 4 proof step from Mathlib.Data.Finset.MulAntidiagonal (goal)
Goal:
α : Type u_1
s t : Set α
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ min (s := s * t) ⋯ ⋯ = hs.min (s := s) hsn * ht.min (s := t) htn
have refine : hs.min (s := s) hsn * ht.min (s := t) htn ≤ min (s := s * t) sorry sorry
Tactic: refine le_antisymm (IsWF.min_le _ _ (mem_mul.2 ⟨_, hs.min_mem _, _, ht.min_mem _, rfl⟩)) ?_
-- Lean 4 proof step from Mathlib.Data.Finset.MulAntidiagonal (goal)
Goal:
α : Type u_1
s t : Set α
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ hs.min (s := s) hsn * ht.min (s := t) htn ≤ min (s := s * t) ⋯ ⋯
have rw : ∀ b ∈ s * t, hs.min (s := s) hsn * ht.min (s := t) htn ≤ b
Tactic: rw [IsWF.le_min_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.MulAntidiagonal (hypothesis)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : Membership.mem (γ := Set α) {a : α | (mulAntidiagonal (s := s) (t := t) hs ht a).Nonempty} a
b : α × α
hb : b ∈ mulAntidiagonal (s := s) (t := t) hs ht a
⊢ a ∈ s * t
have hb₁ : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 * b.2 = a
Tactic: rw [mem_mulAntidiagonal] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.Finset.MulAntidiagonal (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
⊢ mulAntidiagonal (s := s) (t := t) ⋯ ⋯ (hs.min (s := s) hns * ht.min (s := t) hnt) =
    {(hs.min (s := s) hns, ht.min (s := t) hnt)}
have h : ∀ (a b : α),
  (a, b) ∈ mulAntidiagonal (s := s) (t := t) sorry sorry (hs.min (s := s) hns * ht.min (s := t) hnt) ↔
    Membership.mem (γ := Finset (α × α)) {(hs.min (s := s) hns, ht.min (s := t) hnt)} (a, b)
Tactic: ext ⟨a, b⟩
-- Lean 4 proof step from Mathlib.Data.Finset.MulAntidiagonal (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
⊢ (a, b) ∈ mulAntidiagonal (s := s) (t := t) ⋯ ⋯ (hs.min (s := s) hns * ht.min (s := t) hnt) ↔
    Membership.mem (γ := Finset (α × α)) {(hs.min (s := s) hns, ht.min (s := t) hnt)} (a, b)
have h : a ∈ s ∧ b ∈ t ∧ a * b = hs.min (s := s) hns * ht.min (s := t) hnt ↔ a = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt
Tactic: simp only [mem_mulAntidiagonal, mem_singleton, Prod.ext_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.MulAntidiagonal (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
⊢ a ∈ s ∧ b ∈ t ∧ a * b = hs.min (s := s) hns * ht.min (s := t) hnt ↔ a = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt
have h : a ∈ s ∧ b ∈ t ∧ a * b = hs.min (s := s) hns * ht.min (s := t) hnt → a = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.MulAntidiagonal (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
h :
  a ∈ s ∧ b ∈ t ∧ a * b = hs.min (s := s) hns * ht.min (s := t) hnt → a = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt
⊢ a ∈ s ∧ b ∈ t ∧ a * b = hs.min (s := s) hns * ht.min (s := t) hnt ↔ a = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt
have h₁ : a = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt → a ∈ s ∧ b ∈ t ∧ a * b = hs.min (s := s) hns * ht.min (s := t) hnt
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.MulAntidiagonal (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
has : a ∈ s
hat : b ∈ t
hst : a * b = hs.min (s := s) hns * ht.min (s := t) hnt
⊢ a = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt
have h : ∀ (has : hs.min (s := s) hns ∈ s) (hst : hs.min (s := s) hns * b = hs.min (s := s) hns * ht.min (s := t) hnt),
  hs.min (s := s) hns = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt
Tactic: obtain rfl :=
      (hs.min_le hns has).eq_of_not_lt fun hlt =>
        (mul_lt_mul_of_lt_of_le hlt <| ht.min_le hnt hat).ne' hst
Cleared hypotheses: a, has, hst
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ #(image₂ f s t) = #s * #t ↔ InjOn (β := γ) (fun (x : α × β) ↦ f x.1 x.2) ((↑s : Set α) ×ˢ (↑t : Set β))
have rw : #(image₂ f s t) = #(s ×ˢ t) ↔ InjOn (β := γ) (fun (x : α × β) ↦ f x.1 x.2) (↑(s ×ˢ t) : Set (α × β))
Tactic: rw [← card_product, ← coe_product]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
b : β
hf : Injective2 f
⊢ f a b ∈ image₂ f s t ↔ a ∈ s ∧ b ∈ t
have rw : f a b ∈ (↑(image₂ f s t) : Set γ) ↔ a ∈ s ∧ b ∈ t
Tactic: rw [← mem_coe, coe_image₂, mem_image2_iff hf, mem_coe, mem_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
b : β
hf : Injective2 f
rw : f a b ∈ (↑(image₂ f s t) : Set γ) ↔ a ∈ s ∧ b ∈ t
⊢ f a b ∈ image₂ f s t ↔ a ∈ s ∧ b ∈ t
have rw₁ : f a b ∈ image2 f (↑s : Set α) (↑t : Set β) ↔ a ∈ s ∧ b ∈ t
Tactic: rw [← mem_coe, coe_image₂, mem_image2_iff hf, mem_coe, mem_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
b : β
hf : Injective2 f
rw : f a b ∈ (↑(image₂ f s t) : Set γ) ↔ a ∈ s ∧ b ∈ t
rw₁ : f a b ∈ image2 f (↑s : Set α) (↑t : Set β) ↔ a ∈ s ∧ b ∈ t
⊢ f a b ∈ image₂ f s t ↔ a ∈ s ∧ b ∈ t
have rw₂ : a ∈ (↑s : Set α) ∧ b ∈ (↑t : Set β) ↔ a ∈ s ∧ b ∈ t
Tactic: rw [← mem_coe, coe_image₂, mem_image2_iff hf, mem_coe, mem_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
b : β
hf : Injective2 f
rw : f a b ∈ (↑(image₂ f s t) : Set γ) ↔ a ∈ s ∧ b ∈ t
rw₁ : f a b ∈ image2 f (↑s : Set α) (↑t : Set β) ↔ a ∈ s ∧ b ∈ t
rw₂ : a ∈ (↑s : Set α) ∧ b ∈ (↑t : Set β) ↔ a ∈ s ∧ b ∈ t
⊢ f a b ∈ image₂ f s t ↔ a ∈ s ∧ b ∈ t
have rw₃ : a ∈ s ∧ b ∈ (↑t : Set β) ↔ a ∈ s ∧ b ∈ t
Tactic: rw [← mem_coe, coe_image₂, mem_image2_iff hf, mem_coe, mem_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
b : β
hf : Injective2 f
rw : f a b ∈ (↑(image₂ f s t) : Set γ) ↔ a ∈ s ∧ b ∈ t
rw₁ : f a b ∈ image2 f (↑s : Set α) (↑t : Set β) ↔ a ∈ s ∧ b ∈ t
rw₂ : a ∈ (↑s : Set α) ∧ b ∈ (↑t : Set β) ↔ a ∈ s ∧ b ∈ t
rw₃ : a ∈ s ∧ b ∈ (↑t : Set β) ↔ a ∈ s ∧ b ∈ t
⊢ f a b ∈ image₂ f s t ↔ a ∈ s ∧ b ∈ t
have rw₄ : a ∈ s ∧ b ∈ t ↔ a ∈ s ∧ b ∈ t
Tactic: rw [← mem_coe, coe_image₂, mem_image2_iff hf, mem_coe, mem_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
hs : s ⊆ s'
ht : t ⊆ t'
⊢ image₂ f s t ⊆ image₂ f s' t'
have rw : image2 f (↑s : Set α) (↑t : Set β) ⊆ image2 f (↑s' : Set α) (↑t' : Set β)
Tactic: rw [← coe_subset, coe_image₂, coe_image₂]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
p : γ → Prop
⊢ (∀ z ∈ image₂ f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)
have simp_rw : (∀ z ∈ (↑(image₂ f s t) : Set γ), p z) ↔ ∀ x ∈ (↑s : Set α), ∀ y ∈ (↑t : Set β), p (f x y)
Tactic: simp_rw [← mem_coe, coe_image₂, forall_mem_image2]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
p : γ → Prop
simp_rw : (∀ z ∈ (↑(image₂ f s t) : Set γ), p z) ↔ ∀ x ∈ (↑s : Set α), ∀ y ∈ (↑t : Set β), p (f x y)
⊢ (∀ z ∈ image₂ f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)
have simp_rw₁ : (∀ z ∈ image2 f (↑s : Set α) (↑t : Set β), p z) ↔ ∀ x ∈ (↑s : Set α), ∀ y ∈ (↑t : Set β), p (f x y)
Tactic: simp_rw [← mem_coe, coe_image₂, forall_mem_image2]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
p : γ → Prop
⊢ (∃ z ∈ image₂ f s t, p z) ↔ ∃ x ∈ s, ∃ y ∈ t, p (f x y)
have simp_rw : (∃ z ∈ (↑(image₂ f s t) : Set γ), p z) ↔ ∃ x ∈ (↑s : Set α), ∃ y ∈ (↑t : Set β), p (f x y)
Tactic: simp_rw [← mem_coe, coe_image₂, exists_mem_image2]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
p : γ → Prop
simp_rw : (∃ z ∈ (↑(image₂ f s t) : Set γ), p z) ↔ ∃ x ∈ (↑s : Set α), ∃ y ∈ (↑t : Set β), p (f x y)
⊢ (∃ z ∈ image₂ f s t, p z) ↔ ∃ x ∈ s, ∃ y ∈ t, p (f x y)
have simp_rw₁ : (∃ z ∈ image2 f (↑s : Set α) (↑t : Set β), p z) ↔ ∃ x ∈ (↑s : Set α), ∃ y ∈ (↑t : Set β), p (f x y)
Tactic: simp_rw [← mem_coe, coe_image₂, exists_mem_image2]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
u : Finset γ
⊢ image₂ f s t ⊆ u ↔ ∀ a ∈ s, image (fun (b : β) ↦ f a b) t ⊆ u
have simp_rw : (∀ x ∈ s, ∀ y ∈ t, f x y ∈ u) ↔ ∀ a ∈ s, image (fun (b : β) ↦ f a b) t ⊆ u
Tactic: simp_rw [image₂_subset_iff, image_subset_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
u : Finset γ
⊢ image₂ f s t ⊆ u ↔ ∀ b ∈ t, image (fun (a : α) ↦ f a b) s ⊆ u
have simp_rw : (∀ x ∈ s, ∀ y ∈ t, f x y ∈ u) ↔ ∀ b ∈ t, image (fun (a : α) ↦ f a b) s ⊆ u
Tactic: simp_rw [image₂_subset_iff, image_subset_iff, @forall₂_comm α]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
u : Finset γ
simp_rw : (∀ x ∈ s, ∀ y ∈ t, f x y ∈ u) ↔ ∀ b ∈ t, image (fun (a : α) ↦ f a b) s ⊆ u
⊢ image₂ f s t ⊆ u ↔ ∀ b ∈ t, image (fun (a : α) ↦ f a b) s ⊆ u
have simp_rw₁ : (∀ x ∈ s, ∀ y ∈ t, f x y ∈ u) ↔ ∀ b ∈ t, ∀ x ∈ s, f x b ∈ u
Tactic: simp_rw [image₂_subset_iff, image_subset_iff, @forall₂_comm α]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ (image₂ f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
have rw : (image2 f (↑s : Set α) (↑t : Set β)).Nonempty ↔ s.Nonempty ∧ t.Nonempty
Tactic: rw [← coe_nonempty, coe_image₂]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ image₂ f s t = ∅ ↔ s = ∅ ∨ t = ∅
have contrapose! : (image₂ f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst_1 : DecidableEq α
⊢ (↑(image₂ f (s ∪ s') t) : Set γ) = (↑(image₂ f s t ∪ image₂ f s' t) : Set γ)
have push_cast : image2 f ((↑s : Set α) ∪ (↑s' : Set α)) (↑t : Set β) =
  image2 f (↑s : Set α) (↑t : Set β) ∪ image2 f (↑s' : Set α) (↑t : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst_1 : DecidableEq β
⊢ (↑(image₂ f s (t ∪ t')) : Set γ) = (↑(image₂ f s t ∪ image₂ f s t') : Set γ)
have push_cast : image2 f (↑s : Set α) ((↑t : Set β) ∪ (↑t' : Set β)) =
  image2 f (↑s : Set α) (↑t : Set β) ∪ image2 f (↑s : Set α) (↑t' : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
inst_1 : DecidableEq α
⊢ (↑(image₂ f (insert a s) t) : Set γ) = (↑(image (fun (b : β) ↦ f a b) t ∪ image₂ f s t) : Set γ)
have push_cast : image2 f (insert a (↑s : Set α)) (↑t : Set β) =
  (fun (b : β) ↦ f a b) '' (↑t : Set β) ∪ image2 f (↑s : Set α) (↑t : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
b : β
inst_1 : DecidableEq β
⊢ (↑(image₂ f s (insert b t)) : Set γ) = (↑(image (fun (a : α) ↦ f a b) s ∪ image₂ f s t) : Set γ)
have push_cast : image2 f (↑s : Set α) (insert b (↑t : Set β)) =
  (fun (a : α) ↦ f a b) '' (↑s : Set α) ∪ image2 f (↑s : Set α) (↑t : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst_1 : DecidableEq α
hf : Injective2 f
⊢ (↑(image₂ f (s ∩ s') t) : Set γ) = (↑(image₂ f s t ∩ image₂ f s' t) : Set γ)
have push_cast : image2 f ((↑s : Set α) ∩ (↑s' : Set α)) (↑t : Set β) =
  image2 f (↑s : Set α) (↑t : Set β) ∩ image2 f (↑s' : Set α) (↑t : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst_1 : DecidableEq β
hf : Injective2 f
⊢ (↑(image₂ f s (t ∩ t')) : Set γ) = (↑(image₂ f s t ∩ image₂ f s t') : Set γ)
have push_cast : image2 f (↑s : Set α) ((↑t : Set β) ∩ (↑t' : Set β)) =
  image2 f (↑s : Set α) (↑t : Set β) ∩ image2 f (↑s : Set α) (↑t' : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst_1 : DecidableEq α
⊢ (↑(image₂ f (s ∩ s') t) : Set γ) ⊆ (↑(image₂ f s t ∩ image₂ f s' t) : Set γ)
have push_cast : image2 f ((↑s : Set α) ∩ (↑s' : Set α)) (↑t : Set β) ⊆
  image2 f (↑s : Set α) (↑t : Set β) ∩ image2 f (↑s' : Set α) (↑t : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst_1 : DecidableEq β
⊢ (↑(image₂ f s (t ∩ t')) : Set γ) ⊆ (↑(image₂ f s t ∩ image₂ f s t') : Set γ)
have push_cast : image2 f (↑s : Set α) ((↑t : Set β) ∩ (↑t' : Set β)) ⊆
  image2 f (↑s : Set α) (↑t : Set β) ∩ image2 f (↑s : Set α) (↑t' : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f f' : α → β → γ
s : Finset α
t : Finset β
h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b
⊢ (↑(image₂ f s t) : Set γ) = (↑(image₂ f' s t) : Set γ)
have push_cast : image2 f (↑s : Set α) (↑t : Set β) = image2 f' (↑s : Set α) (↑t : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
t : Finset β
a : α
hf : Injective (f a)
⊢ #(image₂ f {a} t) = #t
have rw : card.{u_5} (α := γ) (image (fun (b : β) ↦ f a b) t) = #t
Tactic: rw [image₂_singleton_left, card_image_of_injective _ hf]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
t : Finset β
a : α
hf : Injective (f a)
rw : card.{u_5} (α := γ) (image (fun (b : β) ↦ f a b) t) = #t
⊢ #(image₂ f {a} t) = #t
have rw₁ : #t = #t
Tactic: rw [image₂_singleton_left, card_image_of_injective _ hf]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
b : β
hf : Injective.{u_1 + 1, u_5 + 1} (β := γ) fun (a : α) ↦ f a b
⊢ #(image₂ f s {b}) = #s
have rw : card.{u_5} (α := γ) (image (fun (a : α) ↦ f a b) s) = #s
Tactic: rw [image₂_singleton_right, card_image_of_injective _ hf]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
b : β
hf : Injective.{u_1 + 1, u_5 + 1} (β := γ) fun (a : α) ↦ f a b
rw : card.{u_5} (α := γ) (image (fun (a : α) ↦ f a b) s) = #s
⊢ #(image₂ f s {b}) = #s
have rw₁ : #s = #s
Tactic: rw [image₂_singleton_right, card_image_of_injective _ hf]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
a : α
inst_1 : DecidableEq β
t₁ t₂ : Finset β
hf : Injective (f a)
⊢ image₂ f {a} (t₁ ∩ t₂) = image₂ f {a} t₁ ∩ image₂ f {a} t₂
have simp_rw : Eq.{u_5 + 1} (α := Finset γ) (image (fun (b : β) ↦ f a b) (t₁ ∩ t₂))
  (image (fun (b : β) ↦ f a b) t₁ ∩ image (fun (b : β) ↦ f a b) t₂)
Tactic: simp_rw [image₂_singleton_left, image_inter _ _ hf]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
b : β
inst_1 : DecidableEq α
s₁ s₂ : Finset α
hf : Injective.{u_1 + 1, u_5 + 1} (β := γ) fun (a : α) ↦ f a b
⊢ image₂ f (s₁ ∩ s₂) {b} = image₂ f s₁ {b} ∩ image₂ f s₂ {b}
have simp_rw : Eq.{u_5 + 1} (α := Finset γ) (image (fun (a : α) ↦ f a b) (s₁ ∩ s₂))
  (image (fun (a : α) ↦ f a b) s₁ ∩ image (fun (a : α) ↦ f a b) s₂)
Tactic: simp_rw [image₂_singleton_right, image_inter _ _ hf]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ (↑(s.biUnion fun (a : α) ↦ image (f a) t) : Set γ) = (↑(image₂ f s t) : Set γ)
have push_cast : ⋃ x ∈ (↑s : Set α), f x '' (↑t : Set β) = image2 f (↑s : Set α) (↑t : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ (↑(t.biUnion fun (b : β) ↦ image (fun (a : α) ↦ f a b) s) : Set γ) = (↑(image₂ f s t) : Set γ)
have push_cast : ⋃ x ∈ (↑t : Set β), (fun (a : α) ↦ f a x) '' (↑s : Set α) = image2 f (↑s : Set α) (↑t : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
s : Finset α
t : Finset β
inst_1 : DecidableEq δ
f : α → β → γ
g : γ → δ
⊢ (↑(image g (image₂ f s t)) : Set δ) = (↑(image₂ (fun (a : α) (b : β) ↦ g (f a b)) s t) : Set δ)
have push_cast : g '' image2 f (↑s : Set α) (↑t : Set β) = image2 (fun (a : α) (b : β) ↦ g (f a b)) (↑s : Set α) (↑t : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
s : Finset α
t : Finset β
inst_1 : DecidableEq δ
f : γ → β → δ
g : α → γ
⊢ (↑(image₂ f (image g s) t) : Set δ) = (↑(image₂ (fun (a : α) (b : β) ↦ f (g a) b) s t) : Set δ)
have push_cast : image2 f (g '' (↑s : Set α)) (↑t : Set β) = image2 (fun (a : α) (b : β) ↦ f (g a) b) (↑s : Set α) (↑t : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
s : Finset α
t : Finset β
inst_1 : DecidableEq δ
f : α → γ → δ
g : β → γ
⊢ (↑(image₂ f s (image g t)) : Set δ) = (↑(image₂ (fun (a : α) (b : β) ↦ f a (g b)) s t) : Set δ)
have push_cast : image2 f (↑s : Set α) (g '' (↑t : Set β)) = image2 (fun (a : α) (b : β) ↦ f a (g b)) (↑s : Set α) (↑t : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
s : Finset α
t : Finset β
⊢ image₂ Prod.mk s t = s ×ˢ t
have h : ∀ (a : α × β), a ∈ image₂ Prod.mk s t ↔ a ∈ s ×ˢ t
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ (↑(image₂ f s t) : Set γ) = (↑(image₂ (fun (a : β) (b : α) ↦ f b a) t s) : Set γ)
have push_cast : image2 f (↑s : Set α) (↑t : Set β) = image2 (fun (a : β) (b : α) ↦ f b a) (↑t : Set β) (↑s : Set α)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
s : Finset α
t : Finset β
inst : DecidableEq α
h : t.Nonempty
⊢ (↑(image₂ (fun (x : α) (x_1 : β) ↦ x) s t) : Set α) = (↑s : Set α)
have push_cast : image2 (fun (x : α) (x_1 : β) ↦ x) (↑s : Set α) (↑t : Set β) = (↑s : Set α)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
s : Finset α
t : Finset β
inst : DecidableEq β
h : s.Nonempty
⊢ (↑(image₂ (fun (x : α) (y : β) ↦ y) s t) : Set β) = (↑t : Set β)
have push_cast : image2 (fun (x : α) (y : β) ↦ y) (↑s : Set α) (↑t : Set β) = (↑t : Set β)
Tactic: push_cast