awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
⊢ x + y = single a n ↔ ∃ (a_1 : ℕ) (b : ℕ), a_1 + b = n ∧ single a a_1 = x ∧ single a b = y
have h : x + y = single a n → ∃ (a_2 : ℕ) (b : ℕ), a_2 + b = n ∧ single a a_2 = x ∧ single a b = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x + y = single a n → ∃ (a_2 : ℕ) (b : ℕ), a_2 + b = n ∧ single a a_2 = x ∧ single a b = y
⊢ x + y = single a n ↔ ∃ (a_1 : ℕ) (b : ℕ), a_1 + b = n ∧ single a a_1 = x ∧ single a b = y
have h₁ : (∃ (a_1 : ℕ) (b : ℕ), a_1 + b = n ∧ single a a_1 = x ∧ single a b = y) → x + y = single a n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x + y = single a n
⊢ ∃ (a_1 : ℕ) (b : ℕ), a_1 + b = n ∧ single a a_1 = x ∧ single a b = y
have h₁ : single a ((x : (a : α) → ℕ) a) = x ∧ single a ((y : (a : α) → ℕ) a) = y
Tactic: refine ⟨x a, y a, DFunLike.congr_fun h a |>.trans single_eq_same, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x + y = single a n
⊢ single a ((x : (a : α) → ℕ) a) = x ∧ single a ((y : (a : α) → ℕ) a) = y
have h₁ : ∀ (x_1 : α),
  Eq (α := ℕ) (((single a ((x : (a : α) → ℕ) a) : α →₀ ℕ) : (a : α) → ℕ) x_1 : ℕ) ((x : (a : α) → ℕ) x_1 : ℕ) ∧
    Eq (α := ℕ) (((single a ((y : (a : α) → ℕ) a) : α →₀ ℕ) : (a : α) → ℕ) x_1 : ℕ) ((y : (a : α) → ℕ) x_1 : ℕ)
Tactic: simp_rw [DFunLike.ext_iff, ← forall_and]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x + y = single a n
i : α
⊢ Eq (α := ℕ) (((single a ((x : (a : α) → ℕ) a) : α →₀ ℕ) : (a : α) → ℕ) i : ℕ) ((x : (a : α) → ℕ) i : ℕ) ∧
    Eq (α := ℕ) (((single a ((y : (a : α) → ℕ) a) : α →₀ ℕ) : (a : α) → ℕ) i : ℕ) ((y : (a : α) → ℕ) i : ℕ)
have h₁ : Eq (α := ℕ) ((x + y : (a : α) → ℕ) i : ℕ) ((single a n : (a : α) → ℕ) i : ℕ)
Tactic: replace h := DFunLike.congr_fun h i
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : Eq (α := ℕ) ((x + y : (a : α) → ℕ) i : ℕ) ((single a n : (a : α) → ℕ) i : ℕ)
⊢ Eq (α := ℕ) (((single a ((x : (a : α) → ℕ) a) : α →₀ ℕ) : (a : α) → ℕ) i : ℕ) ((x : (a : α) → ℕ) i : ℕ) ∧
    Eq (α := ℕ) (((single a ((y : (a : α) → ℕ) a) : α →₀ ℕ) : (a : α) → ℕ) i : ℕ) ((y : (a : α) → ℕ) i : ℕ)
have h₁ : ∀ (h : HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : α) → ℕ) i : ℕ) ((y : (a : α) → ℕ) i : ℕ) = if a = i then n else 0),
  Eq (α := ℕ) (if a = i then (x : (a : α) → ℕ) a else 0 : ℕ) ((x : (a : α) → ℕ) i : ℕ) ∧
    Eq (α := ℕ) (if a = i then (y : (a : α) → ℕ) a else 0 : ℕ) ((y : (a : α) → ℕ) i : ℕ)
Tactic: simp_rw [single_apply, Finsupp.add_apply] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : α) → ℕ) i : ℕ) ((y : (a : α) → ℕ) i : ℕ) = if a = i then n else 0
⊢ Eq (α := ℕ) (if a = i then (x : (a : α) → ℕ) a else 0 : ℕ) ((x : (a : α) → ℕ) i : ℕ) ∧
    Eq (α := ℕ) (if a = i then (y : (a : α) → ℕ) a else 0 : ℕ) ((y : (a : α) → ℕ) i : ℕ)
have h₁ : ∀ (h : HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : α) → ℕ) a : ℕ) ((y : (a : α) → ℕ) a : ℕ) = if a = a then n else 0),
  Eq (α := ℕ) (if a = a then (x : (a : α) → ℕ) a else 0 : ℕ) ((x : (a : α) → ℕ) a : ℕ) ∧
    Eq (α := ℕ) (if a = a then (y : (a : α) → ℕ) a else 0 : ℕ) ((y : (a : α) → ℕ) a : ℕ)
Tactic: obtain rfl | hai := Decidable.eq_or_ne a i
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : α) → ℕ) i : ℕ) ((y : (a : α) → ℕ) i : ℕ) = if a = i then n else 0
h₁ :
  ∀ (h : HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : α) → ℕ) a : ℕ) ((y : (a : α) → ℕ) a : ℕ) = if a = a then n else 0),
    Eq (α := ℕ) (if a = a then (x : (a : α) → ℕ) a else 0 : ℕ) ((x : (a : α) → ℕ) a : ℕ) ∧
      Eq (α := ℕ) (if a = a then (y : (a : α) → ℕ) a else 0 : ℕ) ((y : (a : α) → ℕ) a : ℕ)
⊢ Eq (α := ℕ) (if a = i then (x : (a : α) → ℕ) a else 0 : ℕ) ((x : (a : α) → ℕ) i : ℕ) ∧
    Eq (α := ℕ) (if a = i then (y : (a : α) → ℕ) a else 0 : ℕ) ((y : (a : α) → ℕ) i : ℕ)
have h₂ : ∀ (hai : a ≠ i),
  Eq (α := ℕ) (if a = i then (x : (a : α) → ℕ) a else 0 : ℕ) ((x : (a : α) → ℕ) i : ℕ) ∧
    Eq (α := ℕ) (if a = i then (y : (a : α) → ℕ) a else 0 : ℕ) ((y : (a : α) → ℕ) i : ℕ)
Tactic: obtain rfl | hai := Decidable.eq_or_ne a i
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : α) → ℕ) i : ℕ) ((y : (a : α) → ℕ) i : ℕ) = if a = i then n else 0
hai : a ≠ i
⊢ Eq (α := ℕ) (if a = i then (x : (a : α) → ℕ) a else 0 : ℕ) ((x : (a : α) → ℕ) i : ℕ) ∧
    Eq (α := ℕ) (if a = i then (y : (a : α) → ℕ) a else 0 : ℕ) ((y : (a : α) → ℕ) i : ℕ)
have h₁ : ∀ (h : Eq (α := ℕ) ((x : (a : α) → ℕ) i : ℕ) (0 : ℕ) ∧ Eq (α := ℕ) ((y : (a : α) → ℕ) i : ℕ) (0 : ℕ)),
  Eq (α := ℕ) (0 : ℕ) ((x : (a : α) → ℕ) i : ℕ) ∧ Eq (α := ℕ) (0 : ℕ) ((y : (a : α) → ℕ) i : ℕ)
Tactic: simp_rw [if_neg hai, add_eq_zero] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
⊢ image (Prod.map (embDomain f) (embDomain f)) (@antidiagonal _ instAddMonoid _ y) =
    @antidiagonal _ instAddMonoid _ (embDomain f y)
have h : ∀ (u v : β →₀ ℕ),
  (u, v) ∈ image (Prod.map (embDomain f) (embDomain f)) (@antidiagonal _ instAddMonoid _ y) ↔
    (u, v) ∈ @antidiagonal _ instAddMonoid _ (embDomain f y)
Tactic: ext ⟨u, v⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
⊢ (u, v) ∈ image (Prod.map (embDomain f) (embDomain f)) (@antidiagonal _ instAddMonoid _ y) ↔
    (u, v) ∈ @antidiagonal _ instAddMonoid _ (embDomain f y)
have h : (∃ (a : α →₀ ℕ) (b : α →₀ ℕ), a + b = y ∧ embDomain f a = u ∧ embDomain f b = v) ↔ u + v = embDomain f y
Tactic: simp only [mem_image, mem_antidiagonal, Prod.exists, Prod.map_apply,
    Prod.mk.injEq]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
⊢ (∃ (a : α →₀ ℕ) (b : α →₀ ℕ), a + b = y ∧ embDomain f a = u ∧ embDomain f b = v) ↔ u + v = embDomain f y
have h : (∃ (a : α →₀ ℕ) (b : α →₀ ℕ), a + b = y ∧ embDomain f a = u ∧ embDomain f b = v) →
  ∀ (w z : α →₀ ℕ) (h : w + z = y) (hw : embDomain f w = u) (hz : embDomain f z = v), u + v = embDomain f y
Tactic: refine ⟨fun ⟨w, z, h, hw, hz⟩ ↦ ?_, fun h ↦ ⟨u.comapDomain f f.injective.injOn,
    ⟨v.comapDomain f f.injective.injOn, ?_, ?_, ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h :
  (∃ (a : α →₀ ℕ) (b : α →₀ ℕ), a + b = y ∧ embDomain f a = u ∧ embDomain f b = v) →
    ∀ (w z : α →₀ ℕ) (h : w + z = y) (hw : embDomain f w = u) (hz : embDomain f z = v), u + v = embDomain f y
⊢ (∃ (a : α →₀ ℕ) (b : α →₀ ℕ), a + b = y ∧ embDomain f a = u ∧ embDomain f b = v) ↔ u + v = embDomain f y
have h₁ : ∀ (h : u + v = embDomain f y), comapDomain (⇑f : (a : α) → β) u sorry + comapDomain (⇑f : (a : α) → β) v sorry = y
Tactic: refine ⟨fun ⟨w, z, h, hw, hz⟩ ↦ ?_, fun h ↦ ⟨u.comapDomain f f.injective.injOn,
    ⟨v.comapDomain f f.injective.injOn, ?_, ?_, ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h :
  (∃ (a : α →₀ ℕ) (b : α →₀ ℕ), a + b = y ∧ embDomain f a = u ∧ embDomain f b = v) →
    ∀ (w z : α →₀ ℕ) (h : w + z = y) (hw : embDomain f w = u) (hz : embDomain f z = v), u + v = embDomain f y
h₁ : ∀ (h : u + v = embDomain f y), comapDomain (⇑f : (a : α) → β) u ⋯ + comapDomain (⇑f : (a : α) → β) v ⋯ = y
⊢ (∃ (a : α →₀ ℕ) (b : α →₀ ℕ), a + b = y ∧ embDomain f a = u ∧ embDomain f b = v) ↔ u + v = embDomain f y
have h₂ : ∀ (h : u + v = embDomain f y), embDomain f (comapDomain (⇑f : (a : α) → β) u sorry) = u
Tactic: refine ⟨fun ⟨w, z, h, hw, hz⟩ ↦ ?_, fun h ↦ ⟨u.comapDomain f f.injective.injOn,
    ⟨v.comapDomain f f.injective.injOn, ?_, ?_, ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h :
  (∃ (a : α →₀ ℕ) (b : α →₀ ℕ), a + b = y ∧ embDomain f a = u ∧ embDomain f b = v) →
    ∀ (w z : α →₀ ℕ) (h : w + z = y) (hw : embDomain f w = u) (hz : embDomain f z = v), u + v = embDomain f y
h₁ : ∀ (h : u + v = embDomain f y), comapDomain (⇑f : (a : α) → β) u ⋯ + comapDomain (⇑f : (a : α) → β) v ⋯ = y
h₂ : ∀ (h : u + v = embDomain f y), embDomain f (comapDomain (⇑f : (a : α) → β) u ⋯) = u
⊢ (∃ (a : α →₀ ℕ) (b : α →₀ ℕ), a + b = y ∧ embDomain f a = u ∧ embDomain f b = v) ↔ u + v = embDomain f y
have h₃ : ∀ (h : u + v = embDomain f y), embDomain f (comapDomain (⇑f : (a : α) → β) v sorry) = v
Tactic: refine ⟨fun ⟨w, z, h, hw, hz⟩ ↦ ?_, fun h ↦ ⟨u.comapDomain f f.injective.injOn,
    ⟨v.comapDomain f f.injective.injOn, ?_, ?_, ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h_1 : ∃ (a : α →₀ ℕ) (b : α →₀ ℕ), a + b = y ∧ embDomain f a = u ∧ embDomain f b = v
w z : α →₀ ℕ
h : w + z = y
hw : embDomain f w = u
hz : embDomain f z = v
⊢ u + v = embDomain f y
have h₁ : embDomain f w + v = embDomain f y
Tactic: rw [← hw, ← hz, ← embDomain_add, h]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h_1 : ∃ (a : α →₀ ℕ) (b : α →₀ ℕ), a + b = y ∧ embDomain f a = u ∧ embDomain f b = v
w z : α →₀ ℕ
h : w + z = y
hw : embDomain f w = u
hz : embDomain f z = v
h₁ : embDomain f w + v = embDomain f y
⊢ u + v = embDomain f y
have h₂ : embDomain f w + embDomain f z = embDomain f y
Tactic: rw [← hw, ← hz, ← embDomain_add, h]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h_1 : ∃ (a : α →₀ ℕ) (b : α →₀ ℕ), a + b = y ∧ embDomain f a = u ∧ embDomain f b = v
w z : α →₀ ℕ
h : w + z = y
hw : embDomain f w = u
hz : embDomain f z = v
h₁ : embDomain f w + v = embDomain f y
h₂ : embDomain f w + embDomain f z = embDomain f y
⊢ u + v = embDomain f y
have h₃ : embDomain f (w + z) = embDomain f y
Tactic: rw [← hw, ← hz, ← embDomain_add, h]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h_1 : ∃ (a : α →₀ ℕ) (b : α →₀ ℕ), a + b = y ∧ embDomain f a = u ∧ embDomain f b = v
w z : α →₀ ℕ
h : w + z = y
hw : embDomain f w = u
hz : embDomain f z = v
h₁ : embDomain f w + v = embDomain f y
h₂ : embDomain f w + embDomain f z = embDomain f y
h₃ : embDomain f (w + z) = embDomain f y
⊢ u + v = embDomain f y
have h₄ : embDomain f y = embDomain f y
Tactic: rw [← hw, ← hz, ← embDomain_add, h]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h : u + v = embDomain f y
⊢ comapDomain (⇑f : (a : α) → β) u ⋯ + comapDomain (⇑f : (a : α) → β) v ⋯ = y
have h₁ : comapDomain (⇑f : (a : α) → β) (u + v) sorry = y
Tactic: rw [← comapDomain_add_of_injective f.injective, h, comapDomain_embDomain]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h : u + v = embDomain f y
h₁ : comapDomain (⇑f : (a : α) → β) (u + v) ⋯ = y
⊢ comapDomain (⇑f : (a : α) → β) u ⋯ + comapDomain (⇑f : (a : α) → β) v ⋯ = y
have h₂ : comapDomain (⇑f : (a : α) → β) (embDomain f y) sorry = y
Tactic: rw [← comapDomain_add_of_injective f.injective, h, comapDomain_embDomain]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h : u + v = embDomain f y
h₁ : comapDomain (⇑f : (a : α) → β) (u + v) ⋯ = y
h₂ : comapDomain (⇑f : (a : α) → β) (embDomain f y) ⋯ = y
⊢ comapDomain (⇑f : (a : α) → β) u ⋯ + comapDomain (⇑f : (a : α) → β) v ⋯ = y
have h₃ : y = y
Tactic: rw [← comapDomain_add_of_injective f.injective, h, comapDomain_embDomain]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h : u + v = embDomain f y
⊢ embDomain f (comapDomain (⇑f : (a : α) → β) u ⋯) = u
have h₁ : u = u
Tactic: rw [embDomain_comapDomain ((mem_range_embDomain_iff ..).mp
      (isLowerSet_range_embDomain f (le_iff_exists_add.mpr ⟨v, h.symm⟩) (by simp)))]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h : u + v = embDomain f y
⊢ embDomain f (comapDomain (⇑f : (a : α) → β) v ⋯) = v
have h₁ : v = v
Tactic: rw [embDomain_comapDomain ((mem_range_embDomain_iff ..).mp
      (isLowerSet_range_embDomain f (le_iff_exists_add'.mpr ⟨u, h.symm⟩) (by simp)))]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
⊢ image
      (fun (x : Prod.{u, u_1} ((α →₀ ℕ) × (α →₀ ℕ)) ((β →₀ ℕ) × (β →₀ ℕ))) ↦
        match (motive := Prod.{u, u_1} ((α →₀ ℕ) × (α →₀ ℕ)) ((β →₀ ℕ) × (β →₀ ℕ)) → (α ⊕ β →₀ ℕ) × (α ⊕ β →₀ ℕ)) x with
        | ((x, y), z, w) => (x.sumElim z, y.sumElim w))
      (@antidiagonal _ instAddMonoid _ x ×ˢ @antidiagonal _ instAddMonoid _ y) =
    @antidiagonal _ instAddMonoid _ (x.sumElim y)
have h : ∀ (u v : α ⊕ β →₀ ℕ),
  Membership.mem (γ := Finset ((α ⊕ β →₀ ℕ) × (α ⊕ β →₀ ℕ)))
      (image
        (fun (x : Prod.{u, u_1} ((α →₀ ℕ) × (α →₀ ℕ)) ((β →₀ ℕ) × (β →₀ ℕ))) ↦
          match (motive := Prod.{u, u_1} ((α →₀ ℕ) × (α →₀ ℕ)) ((β →₀ ℕ) × (β →₀ ℕ)) → (α ⊕ β →₀ ℕ) × (α ⊕ β →₀ ℕ))
            x with
          | ((x, y), z, w) => (x.sumElim z, y.sumElim w))
        (@antidiagonal _ instAddMonoid _ x ×ˢ @antidiagonal _ instAddMonoid _ y))
      (u, v) ↔
    (u, v) ∈ @antidiagonal _ instAddMonoid _ (x.sumElim y)
Tactic: ext ⟨u, v⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
⊢ Membership.mem (γ := Finset ((α ⊕ β →₀ ℕ) × (α ⊕ β →₀ ℕ)))
      (image
        (fun (x : Prod.{u, u_1} ((α →₀ ℕ) × (α →₀ ℕ)) ((β →₀ ℕ) × (β →₀ ℕ))) ↦
          match (motive := Prod.{u, u_1} ((α →₀ ℕ) × (α →₀ ℕ)) ((β →₀ ℕ) × (β →₀ ℕ)) → (α ⊕ β →₀ ℕ) × (α ⊕ β →₀ ℕ))
            x with
          | ((x, y), z, w) => (x.sumElim z, y.sumElim w))
        (@antidiagonal _ instAddMonoid _ x ×ˢ @antidiagonal _ instAddMonoid _ y))
      (u, v) ↔
    (u, v) ∈ @antidiagonal _ instAddMonoid _ (x.sumElim y)
have h : (∃ (a : α →₀ ℕ) (b : α →₀ ℕ) (a_1 : β →₀ ℕ) (b_1 : β →₀ ℕ),
    (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v) ↔
  u + v = x.sumElim y
Tactic: simp only [mem_antidiagonal, mem_image, mem_product, Prod.mk.injEq, Prod.exists]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
⊢ (∃ (a : α →₀ ℕ) (b : α →₀ ℕ) (a_1 : β →₀ ℕ) (b_1 : β →₀ ℕ),
      (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v) ↔
    u + v = x.sumElim y
have h : (∃ (a : α →₀ ℕ) (b : α →₀ ℕ) (a_1 : β →₀ ℕ) (b_1 : β →₀ ℕ),
    (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v) →
  ∀ (a b : α →₀ ℕ) (a' b' : β →₀ ℕ) (h1 : a + b = x ∧ a' + b' = y) (h2 : a.sumElim a' = u) (h3 : b.sumElim b' = v),
    u + v = x.sumElim y
Tactic: refine ⟨fun ⟨a, b, a', b', h1, h2, h3⟩ ↦ ?_, fun h ↦
    ⟨u.comapDomain Sum.inl Sum.inl_injective.injOn, v.comapDomain Sum.inl Sum.inl_injective.injOn,
    u.comapDomain Sum.inr Sum.inr_injective.injOn, v.comapDomain Sum.inr Sum.inr_injective.injOn,
    ⟨?_, ?_⟩, comapDomain_sumElim_comapDomain .., comapDomain_sumElim_comapDomain ..⟩⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h :
  (∃ (a : α →₀ ℕ) (b : α →₀ ℕ) (a_1 : β →₀ ℕ) (b_1 : β →₀ ℕ),
      (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v) →
    ∀ (a b : α →₀ ℕ) (a' b' : β →₀ ℕ) (h1 : a + b = x ∧ a' + b' = y) (h2 : a.sumElim a' = u) (h3 : b.sumElim b' = v),
      u + v = x.sumElim y
⊢ (∃ (a : α →₀ ℕ) (b : α →₀ ℕ) (a_1 : β →₀ ℕ) (b_1 : β →₀ ℕ),
      (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v) ↔
    u + v = x.sumElim y
have h₁ : ∀ (h : u + v = x.sumElim y), comapDomain Sum.inl u sorry + comapDomain Sum.inl v sorry = x
Tactic: refine ⟨fun ⟨a, b, a', b', h1, h2, h3⟩ ↦ ?_, fun h ↦
    ⟨u.comapDomain Sum.inl Sum.inl_injective.injOn, v.comapDomain Sum.inl Sum.inl_injective.injOn,
    u.comapDomain Sum.inr Sum.inr_injective.injOn, v.comapDomain Sum.inr Sum.inr_injective.injOn,
    ⟨?_, ?_⟩, comapDomain_sumElim_comapDomain .., comapDomain_sumElim_comapDomain ..⟩⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h :
  (∃ (a : α →₀ ℕ) (b : α →₀ ℕ) (a_1 : β →₀ ℕ) (b_1 : β →₀ ℕ),
      (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v) →
    ∀ (a b : α →₀ ℕ) (a' b' : β →₀ ℕ) (h1 : a + b = x ∧ a' + b' = y) (h2 : a.sumElim a' = u) (h3 : b.sumElim b' = v),
      u + v = x.sumElim y
h₁ : ∀ (h : u + v = x.sumElim y), comapDomain Sum.inl u ⋯ + comapDomain Sum.inl v ⋯ = x
⊢ (∃ (a : α →₀ ℕ) (b : α →₀ ℕ) (a_1 : β →₀ ℕ) (b_1 : β →₀ ℕ),
      (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v) ↔
    u + v = x.sumElim y
have h₂ : ∀ (h : u + v = x.sumElim y), comapDomain Sum.inr u sorry + comapDomain Sum.inr v sorry = y
Tactic: refine ⟨fun ⟨a, b, a', b', h1, h2, h3⟩ ↦ ?_, fun h ↦
    ⟨u.comapDomain Sum.inl Sum.inl_injective.injOn, v.comapDomain Sum.inl Sum.inl_injective.injOn,
    u.comapDomain Sum.inr Sum.inr_injective.injOn, v.comapDomain Sum.inr Sum.inr_injective.injOn,
    ⟨?_, ?_⟩, comapDomain_sumElim_comapDomain .., comapDomain_sumElim_comapDomain ..⟩⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h :
  ∃ (a : α →₀ ℕ) (b : α →₀ ℕ) (a_1 : β →₀ ℕ) (b_1 : β →₀ ℕ),
    (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v
a b : α →₀ ℕ
a' b' : β →₀ ℕ
h1 : a + b = x ∧ a' + b' = y
h2 : a.sumElim a' = u
h3 : b.sumElim b' = v
⊢ u + v = x.sumElim y
have h : a.sumElim a' + v = x.sumElim y
Tactic: rw [← h2, ← h3, ← sumElim_add, h1.left, h1.right]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h_1 :
  ∃ (a : α →₀ ℕ) (b : α →₀ ℕ) (a_1 : β →₀ ℕ) (b_1 : β →₀ ℕ),
    (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v
a b : α →₀ ℕ
a' b' : β →₀ ℕ
h1 : a + b = x ∧ a' + b' = y
h2 : a.sumElim a' = u
h3 : b.sumElim b' = v
h : a.sumElim a' + v = x.sumElim y
⊢ u + v = x.sumElim y
have h₁ : a.sumElim a' + b.sumElim b' = x.sumElim y
Tactic: rw [← h2, ← h3, ← sumElim_add, h1.left, h1.right]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h_1 :
  ∃ (a : α →₀ ℕ) (b : α →₀ ℕ) (a_1 : β →₀ ℕ) (b_1 : β →₀ ℕ),
    (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v
a b : α →₀ ℕ
a' b' : β →₀ ℕ
h1 : a + b = x ∧ a' + b' = y
h2 : a.sumElim a' = u
h3 : b.sumElim b' = v
h : a.sumElim a' + v = x.sumElim y
h₁ : a.sumElim a' + b.sumElim b' = x.sumElim y
⊢ u + v = x.sumElim y
have h₂ : (a + b).sumElim (a' + b') = x.sumElim y
Tactic: rw [← h2, ← h3, ← sumElim_add, h1.left, h1.right]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h_1 :
  ∃ (a : α →₀ ℕ) (b : α →₀ ℕ) (a_1 : β →₀ ℕ) (b_1 : β →₀ ℕ),
    (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v
a b : α →₀ ℕ
a' b' : β →₀ ℕ
h1 : a + b = x ∧ a' + b' = y
h2 : a.sumElim a' = u
h3 : b.sumElim b' = v
h : a.sumElim a' + v = x.sumElim y
h₁ : a.sumElim a' + b.sumElim b' = x.sumElim y
h₂ : (a + b).sumElim (a' + b') = x.sumElim y
⊢ u + v = x.sumElim y
have h₃ : x.sumElim (a' + b') = x.sumElim y
Tactic: rw [← h2, ← h3, ← sumElim_add, h1.left, h1.right]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h_1 :
  ∃ (a : α →₀ ℕ) (b : α →₀ ℕ) (a_1 : β →₀ ℕ) (b_1 : β →₀ ℕ),
    (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v
a b : α →₀ ℕ
a' b' : β →₀ ℕ
h1 : a + b = x ∧ a' + b' = y
h2 : a.sumElim a' = u
h3 : b.sumElim b' = v
h : a.sumElim a' + v = x.sumElim y
h₁ : a.sumElim a' + b.sumElim b' = x.sumElim y
h₂ : (a + b).sumElim (a' + b') = x.sumElim y
h₃ : x.sumElim (a' + b') = x.sumElim y
⊢ u + v = x.sumElim y
have h₄ : x.sumElim y = x.sumElim y
Tactic: rw [← h2, ← h3, ← sumElim_add, h1.left, h1.right]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h : u + v = x.sumElim y
⊢ comapDomain Sum.inl u ⋯ + comapDomain Sum.inl v ⋯ = x
have h₁ : comapDomain Sum.inl (u + v) sorry = x
Tactic: rw [← comapDomain_add_of_injective Sum.inl_injective, h, comapDomain_inl_sumElim]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h : u + v = x.sumElim y
h₁ : comapDomain Sum.inl (u + v) ⋯ = x
⊢ comapDomain Sum.inl u ⋯ + comapDomain Sum.inl v ⋯ = x
have h₂ : comapDomain Sum.inl (x.sumElim y) sorry = x
Tactic: rw [← comapDomain_add_of_injective Sum.inl_injective, h, comapDomain_inl_sumElim]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h : u + v = x.sumElim y
h₁ : comapDomain Sum.inl (u + v) ⋯ = x
h₂ : comapDomain Sum.inl (x.sumElim y) ⋯ = x
⊢ comapDomain Sum.inl u ⋯ + comapDomain Sum.inl v ⋯ = x
have h₃ : x = x
Tactic: rw [← comapDomain_add_of_injective Sum.inl_injective, h, comapDomain_inl_sumElim]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h : u + v = x.sumElim y
⊢ comapDomain Sum.inr u ⋯ + comapDomain Sum.inr v ⋯ = y
have h₁ : comapDomain Sum.inr (u + v) sorry = y
Tactic: rw [← comapDomain_add_of_injective Sum.inr_injective, h, comapDomain_inr_sumElim]