awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCancelCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
h :
  (f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s) →
    ∃ (a : μ) (b : μ),
      a + b = n ∧
        ∃ (a_1 : (t : ι) → μ),
          (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧
            (addRightEmbedding fun (t : ι) ↦ if t = i then a else 0 : (a : (t : ι) → μ) → ι → μ) a_1 = f
⊢ (f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s) ↔
    ∃ (a : μ) (b : μ),
      a + b = n ∧
        ∃ (a_1 : (t : ι) → μ),
          (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧
            (addRightEmbedding fun (t : ι) ↦ if t = i then a else 0 : (a : (t : ι) → μ) → ι → μ) a_1 = f
have h₁ : (∃ (a : μ) (b : μ),
    a + b = n ∧
      ∃ (a_1 : (t : ι) → μ),
        (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧
          (addRightEmbedding fun (t : ι) ↦ if t = i then a else 0 : (a : (t : ι) → μ) → ι → μ) a_1 = f) →
  f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCancelCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
hn : f i + ∑ x ∈ s, f x = n
hf : ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s
⊢ ∃ (a : μ) (b : μ),
    a + b = n ∧
      ∃ (a_1 : (t : ι) → μ),
        (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧
          (addRightEmbedding fun (t : ι) ↦ if t = i then a else 0 : (a : (t : ι) → μ) → ι → μ) a_1 = f
have h : ∀ (j : ι), ¬update (β := fun (t : ι) ↦ μ) f i 0 j = 0 → j ∈ s
Tactic: refine ⟨_, _, hn, update f i 0, ⟨sum_update_of_notMem hi _ _, fun j ↦ ?_⟩, by aesop⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (hypothesis)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCancelCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
hn : f i + ∑ x ∈ s, f x = n
hf : ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s
j : ι
⊢ ¬update (β := fun (t : ι) ↦ μ) f i 0 j = 0 → j ∈ s
have this : ∀ (h₁ : ¬f j = 0) (h₂ : ¬j = i), j ∈ s
Tactic: have := fun h₁ h₂ ↦ (hf j h₁).resolve_left h₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (hypothesis)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCancelCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a : μ
g : (t : ι) → μ
hg : ∀ (i : ι), ¬g i = 0 → i ∈ s
hn : a + s.sum g = n
⊢ HAdd.hAdd (α := μ) (β := μ)
        ((addRightEmbedding fun (t : ι) ↦ if t = i then a else 0 : (a : (t : ι) → μ) → ι → μ) g i : μ)
        (∑ x ∈ s, (addRightEmbedding fun (t : ι) ↦ if t = i then a else 0 : (a : (t : ι) → μ) → ι → μ) g x : μ) =
      n ∧
    ∀ (i_1 : ι),
      ¬Eq.{u_2 + 1} (α := μ)
            ((addRightEmbedding fun (t : ι) ↦ if t = i then a else 0 : (a : (t : ι) → μ) → ι → μ) g i_1 : μ) (0 : μ) →
        i_1 = i ∨ i_1 ∈ s
have this : ¬g i = 0 → i ∈ s
Tactic: have := hg i
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : PartialOrder μ
inst_3 : CanonicallyOrderedAdd μ
inst_4 : HasAntidiagonal μ
inst_5 : DecidableEq μ
s : Finset ι
⊢ Eq (α := Finset (ι → μ)) (s.piAntidiag 0) {0}
have h : ∀ (a : ι → μ), Membership.mem (γ := Finset (ι → μ)) (s.piAntidiag 0) a ↔ Membership.mem (γ := Finset (ι → μ)) {0} a
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
n k : ℕ
⊢ piAntidiag univ n = Nat.antidiagonalTuple k n
have h : ∀ (a : Fin k → ℕ), Membership.mem (γ := Finset (Fin k → ℕ)) (piAntidiag univ n) a ↔ a ∈ Nat.antidiagonalTuple k n
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
⊢ SMul.smul n (s.piAntidiag m) = {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}
have h : ∀ (f : ι → ℕ), f ∈ SMul.smul n (s.piAntidiag m) ↔ f ∈ {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}
Tactic: ext f
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
⊢ f ∈ SMul.smul n (s.piAntidiag m) ↔ f ∈ {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}
have h : (∃ y ∈ s.piAntidiag m, n • y = f) ↔ f ∈ {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}
Tactic: refine mem_smul_finset.trans ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
⊢ (∃ y ∈ s.piAntidiag m, n • y = f) ↔ f ∈ {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}
have h : (∃ (y : ι → ℕ), s.sum y = m ∧ (∀ (i : ι), y i ≠ 0 → i ∈ s) ∧ n • y = f) ↔
  s.sum f = n * m ∧ (∀ (i : ι), f i ≠ 0 → i ∈ s) ∧ ∀ i ∈ s, n ∣ f i
Tactic: simp only [mem_filter, mem_piAntidiag, and_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
⊢ (∃ (y : ι → ℕ), s.sum y = m ∧ (∀ (i : ι), y i ≠ 0 → i ∈ s) ∧ n • y = f) ↔
    s.sum f = n * m ∧ (∀ (i : ι), f i ≠ 0 → i ∈ s) ∧ ∀ i ∈ s, n ∣ f i
have h : (∃ (y : ι → ℕ), s.sum y = m ∧ (∀ (i : ι), y i ≠ 0 → i ∈ s) ∧ n • y = f) →
  s.sum f = n * m ∧ (∀ (i : ι), f i ≠ 0 → i ∈ s) ∧ ∀ i ∈ s, n ∣ f i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
h :
  (∃ (y : ι → ℕ), s.sum y = m ∧ (∀ (i : ι), y i ≠ 0 → i ∈ s) ∧ n • y = f) →
    s.sum f = n * m ∧ (∀ (i : ι), f i ≠ 0 → i ∈ s) ∧ ∀ i ∈ s, n ∣ f i
⊢ (∃ (y : ι → ℕ), s.sum y = m ∧ (∀ (i : ι), y i ≠ 0 → i ∈ s) ∧ n • y = f) ↔
    s.sum f = n * m ∧ (∀ (i : ι), f i ≠ 0 → i ∈ s) ∧ ∀ i ∈ s, n ∣ f i
have h₁ : (s.sum f = n * m ∧ (∀ (i : ι), f i ≠ 0 → i ∈ s) ∧ ∀ i ∈ s, n ∣ f i) →
  ∃ (y : ι → ℕ), s.sum y = m ∧ (∀ (i : ι), y i ≠ 0 → i ∈ s) ∧ n • y = f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
i : ι
⊢ n ∣ f i
have pos : ∀ (hi : i ∈ s), n ∣ f i
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
i : ι
pos : ∀ (hi : i ∈ s), n ∣ f i
⊢ n ∣ f i
have neg : ∀ (hi : i ∉ s), n ∣ f i
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
i : ι
hi : i ∉ s
⊢ n ∣ f i
have neg : n ∣ 0
Tactic: rw [not_imp_comm.1 (hfsup _) hi]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (hypothesis)
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
⊢ ∃ (y : ι → ℕ), s.sum y = m ∧ (∀ (i : ι), y i ≠ 0 → i ∈ s) ∧ n • y = f
have this : ∀ (i : ι), n ∣ f i
Tactic: have (i : _) : n ∣ f i := by
    by_cases hi : i ∈ s
    · exact hfdvd _ hi
    · rw [not_imp_comm.1 (hfsup _) hi]
      exact dvd_zero _
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
this : ∀ (i : ι), n ∣ f i
⊢ ∃ (y : ι → ℕ), s.sum y = m ∧ (∀ (i : ι), y i ≠ 0 → i ∈ s) ∧ n • y = f
have h : ∑ i ∈ s, f i / n = m ∧
  (∀ (i : ι), Ne (α := ℕ) ((fun (i : ι) ↦ f i / n) i) 0 → i ∈ s) ∧
    (HSMul.hSMul (β := ι → ℕ) n fun (i : ι) ↦ f i / n) = f
Tactic: refine ⟨fun i ↦ f i / n, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
this : ∀ (i : ι), n ∣ f i
⊢ ∑ i ∈ s, f i / n = m ∧
    (∀ (i : ι), Ne (α := ℕ) ((fun (i : ι) ↦ f i / n) i) 0 → i ∈ s) ∧
      (HSMul.hSMul (β := ι → ℕ) n fun (i : ι) ↦ f i / n) = f
have h : ∀ (i : ι), n ≤ f i → i ∈ s
Tactic: simp [funext_iff, Nat.mul_div_cancel', ← Nat.sum_div, *]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
m n : ℕ
hn : n ≠ 0
⊢ map { toFun := fun (x : (x : ι) → ℕ) ↦ n • x, inj' := ⋯ } (s.piAntidiag m) =
    {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}
have rw : image (⇑{ toFun := fun (x : (x : ι) → ℕ) ↦ n • x, inj' := sorry } : (a : (x : ι) → ℕ) → (x : ι) → ℕ) (s.piAntidiag m) =
  {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}
Tactic: rw [map_eq_image]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
m n : ℕ
hn : n ≠ 0
⊢ map { toFun := fun (x : (x : ι) → ℕ) ↦ n • x, inj' := ⋯ } (s.piAntidiag m) =
    {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}
have classical : image (⇑{ toFun := fun (x : (x : ι) → ℕ) ↦ n • x, inj' := sorry } : (a : (x : ι) → ℕ) → (x : ι) → ℕ) (s.piAntidiag m) =
  {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}
Tactic: classical rw [map_eq_image]; exact nsmul_piAntidiag _ _ hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
n : ℕ
⊢ map { toFun := fun (m : Sym ι n) (a : ι) ↦ Multiset.count a (↑m : Multiset ι), inj' := ⋯ : Sym ι n ↪ (a : ι) → ℕ }
      (s.sym n) =
    s.piAntidiag n
have h : ∀ (f : (a : ι) → ℕ),
  f ∈
      map { toFun := fun (m : Sym ι n) (a : ι) ↦ Multiset.count a (↑m : Multiset ι), inj' := sorry : Sym ι n ↪ (a : ι) → ℕ }
        (s.sym n) ↔
    f ∈ s.piAntidiag n
Tactic: ext f
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
n : ℕ
f : (a : ι) → ℕ
⊢ f ∈
      map { toFun := fun (m : Sym ι n) (a : ι) ↦ Multiset.count a (↑m : Multiset ι), inj' := ⋯ : Sym ι n ↪ (a : ι) → ℕ }
        (s.sym n) ↔
    f ∈ s.piAntidiag n
have h : (∃ (s_1 : Multiset ι), (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x) ↔
  s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s
Tactic: simp only [Sym.val_eq_coe, mem_map, mem_sym_iff, Embedding.coeFn_mk, funext_iff, Sym.exists,
    Sym.mem_mk, Sym.coe_mk, exists_and_left, exists_prop, mem_piAntidiag, ne_eq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
n : ℕ
f : (a : ι) → ℕ
⊢ (∃ (s_1 : Multiset ι), (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x) ↔
    s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s
have h : (∃ (s_1 : Multiset ι), (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x) →
  s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
n : ℕ
f : (a : ι) → ℕ
h :
  (∃ (s_1 : Multiset ι), (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x) →
    s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s
⊢ (∃ (s_1 : Multiset ι), (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x) ↔
    s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s
have h₁ : (s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s) →
  ∃ (s_1 : Multiset ι), (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
f : (a : ι) → ℕ
hf : ∀ (i : ι), ¬f i = 0 → i ∈ s
⊢ ∃ (s_1 : Multiset ι), (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = s.sum f ∧ ∀ (x : ι), Multiset.count x s_1 = f x
have h : ∀ (a : ι), Membership.mem (γ := Multiset ι) (∑ a ∈ s, HSMul.hSMul (β := Multiset ι) (f a) {a}) a → a ∈ s
Tactic: refine ⟨∑ a ∈ s, f a • {a}, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
f : (a : ι) → ℕ
hf : ∀ (i : ι), ¬f i = 0 → i ∈ s
h : ∀ (a : ι), Membership.mem (γ := Multiset ι) (∑ a ∈ s, HSMul.hSMul (β := Multiset ι) (f a) {a}) a → a ∈ s
⊢ ∃ (s_1 : Multiset ι), (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = s.sum f ∧ ∀ (x : ι), Multiset.count x s_1 = f x
have h₁ : Multiset.card (α := ι) (∑ a ∈ s, HSMul.hSMul (β := Multiset ι) (f a) {a}) = s.sum f ∧
  ∀ (x : ι), Multiset.count x (∑ a ∈ s, HSMul.hSMul (β := Multiset ι) (f a) {a}) = f x
Tactic: refine ⟨∑ a ∈ s, f a • {a}, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddMonoid A
a : A → Finset (A × A)
ha : ∀ {n : A} {a_1 : A × A}, a_1 ∈ a n ↔ a_1.1 + a_1.2 = n
b : A → Finset (A × A)
hb : ∀ {n : A} {a : A × A}, a ∈ b n ↔ a.1 + a.2 = n
⊢ { antidiagonal := a, mem_antidiagonal := @ha : HasAntidiagonal A } = { antidiagonal := b, mem_antidiagonal := @hb }
have e_antidiagonal : ∀ (n : A) (xy : A × A), xy ∈ a n ↔ xy ∈ b n
Tactic: congr with n xy
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddMonoid A
a : A → Finset (A × A)
ha : ∀ {n : A} {a_1 : A × A}, a_1 ∈ a n ↔ a_1.1 + a_1.2 = n
b : A → Finset (A × A)
hb : ∀ {n : A} {a : A × A}, a ∈ b n ↔ a.1 + a.2 = n
n : A
xy : A × A
⊢ xy ∈ a n ↔ xy ∈ b n
have e_antidiagonal : xy.1 + xy.2 = n ↔ xy ∈ b n
Tactic: rw [ha, hb]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddMonoid A
a : A → Finset (A × A)
ha : ∀ {n : A} {a_1 : A × A}, a_1 ∈ a n ↔ a_1.1 + a_1.2 = n
b : A → Finset (A × A)
hb : ∀ {n : A} {a : A × A}, a ∈ b n ↔ a.1 + a.2 = n
n : A
xy : A × A
e_antidiagonal : xy.1 + xy.2 = n ↔ xy ∈ b n
⊢ xy ∈ a n ↔ xy ∈ b n
have e_antidiagonal₁ : xy.1 + xy.2 = n ↔ xy.1 + xy.2 = n
Tactic: rw [ha, hb]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_2
inst : AddMonoid A
H1 H2 : HasAntidiagonal A
⊢ Eq.{u_2 + 1} (α := A → Finset (A × A)) (@antidiagonal _ inst _) (@antidiagonal _ inst _)
have h : H1 = H2
Tactic: congr!
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCancelMonoid A
inst_1 : HasAntidiagonal A
p q : A × A
n : A
hp : p ∈ @antidiagonal _ AddRightCancelMonoid.toAddMonoid _ n
hq : q ∈ @antidiagonal _ AddRightCancelMonoid.toAddMonoid _ n
⊢ p = q ↔ p.1 = q.1
have refine : ∀ (h : p.1 = q.1), q.1 + p.2 = q.1 + q.2
Tactic: refine ⟨congr_arg Prod.fst, fun h ↦ Prod.ext h ((add_right_inj q.fst).mp ?_)⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (hypothesis)
Goal:
A : Type u_1
inst : AddCancelMonoid A
inst_1 : HasAntidiagonal A
p q : A × A
n : A
hp : p ∈ @antidiagonal _ AddRightCancelMonoid.toAddMonoid _ n
hq : q ∈ @antidiagonal _ AddRightCancelMonoid.toAddMonoid _ n
h : p.1 = q.1
⊢ q.1 + p.2 = q.1 + q.2
have hp₁ : p.1 + p.2 = n
Tactic: rw [mem_antidiagonal] at hp hq
Cleared hypotheses: hp, hq, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (hypothesis)
Goal:
A : Type u_1
inst : AddCancelMonoid A
inst_1 : HasAntidiagonal A
p q : A × A
n : A
hp : p ∈ @antidiagonal _ AddRightCancelMonoid.toAddMonoid _ n
hq : q ∈ @antidiagonal _ AddRightCancelMonoid.toAddMonoid _ n
h : p.1 = q.1
hp₁ : p.1 + p.2 = n
⊢ q.1 + p.2 = q.1 + q.2
have hq₁ : q.1 + q.2 = n
Tactic: rw [mem_antidiagonal] at hp hq
Cleared hypotheses: hp, hq, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCancelMonoid A
inst_1 : HasAntidiagonal A
p q : A × A
n : A
hp : p.1 + p.2 = n
hq : q.1 + q.2 = n
h : p.1 = q.1
⊢ q.1 + p.2 = q.1 + q.2
have rw : q.1 + p.2 = n
Tactic: rw [hq, ← h, hp]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCancelMonoid A
inst_1 : HasAntidiagonal A
p q : A × A
n : A
hp : p.1 + p.2 = n
hq : q.1 + q.2 = n
h : p.1 = q.1
rw : q.1 + p.2 = n
rw₁ : p.1 + p.2 = n
⊢ q.1 + p.2 = q.1 + q.2
have rw₂ : n = n
Tactic: rw [hq, ← h, hp]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCancelCommMonoid A
inst_1 : HasAntidiagonal A
p q : A × A
n : A
hp : p ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
hq : q ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
⊢ p = q ↔ p.2 = q.2
have rw : p.swap = q.swap ↔ p.2 = q.2
Tactic: rw [← Prod.swap_inj]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : HasAntidiagonal A
⊢ Eq (α := Finset (A × A)) (@antidiagonal _ AddCommMonoid.toAddMonoid _ 0) {(0, 0)}
have h : ∀ (x y : A),
  Membership.mem (γ := Finset (A × A)) (@antidiagonal _ AddCommMonoid.toAddMonoid _ 0) (x, y) ↔
    Membership.mem (γ := Finset (A × A)) {(0, 0)} (x, y)
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
⊢ kl.1 ≤ n
have rw : ∃ (c : A), n = kl.1 + c
Tactic: rw [le_iff_exists_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
⊢ ∃ (c : A), n = kl.1 + c
have h : n = kl.1 + kl.2
Tactic: use kl.2
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
⊢ n = kl.1 + kl.2
have h : ∀ (hlk : kl.1 + kl.2 = n), n = kl.1 + kl.2
Tactic: rwa [mem_antidiagonal, eq_comm] at hlk
Cleared hypotheses: hlk
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
h : ∀ (hlk : kl.1 + kl.2 = n), n = kl.1 + kl.2
⊢ n = kl.1 + kl.2
have h₁ : ∀ (hlk : n = kl.1 + kl.2), n = kl.1 + kl.2
Tactic: rwa [mem_antidiagonal, eq_comm] at hlk
Cleared hypotheses: hlk
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
⊢ kl.2 ≤ n
have rw : ∃ (c : A), n = kl.2 + c
Tactic: rw [le_iff_exists_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
⊢ ∃ (c : A), n = kl.2 + c
have h : n = kl.2 + kl.1
Tactic: use kl.1
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
⊢ n = kl.2 + kl.1
have h : ∀ (hlk : kl.1 + kl.2 = n), n = kl.2 + kl.1
Tactic: rwa [mem_antidiagonal, eq_comm, add_comm] at hlk
Cleared hypotheses: hlk
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
h : ∀ (hlk : kl.1 + kl.2 = n), n = kl.2 + kl.1
⊢ n = kl.2 + kl.1
have h₁ : ∀ (hlk : n = kl.1 + kl.2), n = kl.2 + kl.1
Tactic: rwa [mem_antidiagonal, eq_comm, add_comm] at hlk
Cleared hypotheses: hlk
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n
h : ∀ (hlk : kl.1 + kl.2 = n), n = kl.2 + kl.1
h₁ : ∀ (hlk : n = kl.1 + kl.2), n = kl.2 + kl.1
⊢ n = kl.2 + kl.1
have h₂ : ∀ (hlk : n = kl.2 + kl.1), n = kl.2 + kl.1
Tactic: rwa [mem_antidiagonal, eq_comm, add_comm] at hlk
Cleared hypotheses: hlk
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : Sub A
inst_4 : OrderedSub A
inst_5 : AddLeftReflectLE A
inst_6 : HasAntidiagonal A
n m : A
inst_7 : DecidablePred fun (x : A) ↦ x = m
inst_8 : Decidable (m ≤ n)
⊢ {x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n | x.1 = m} = if m ≤ n then {(m, n - m)} else ∅
have h : ∀ (a b : A),
  (a, b) ∈ {x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n | x.1 = m} ↔
    Membership.mem (γ := Finset (A × A)) (if m ≤ n then {(m, n - m)} else ∅) (a, b)
Tactic: ext ⟨a, b⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : Sub A
inst_4 : OrderedSub A
inst_5 : AddLeftReflectLE A
inst_6 : HasAntidiagonal A
n m : A
inst_7 : DecidablePred fun (x : A) ↦ x = m
inst_8 : Decidable (m ≤ n)
a b : A
this : a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)
⊢ (a, b) ∈ {x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n | x.1 = m} ↔
    Membership.mem (γ := Finset (A × A)) (if m ≤ n then {(m, n - m)} else ∅) (a, b)
have rw : (a, b).1 + (a, b).2 = n ∧ (a, b).1 = m ↔
  m ≤ n ∧ a = m ∧ b = n - m ∨ ¬m ≤ n ∧ Membership.mem (γ := Finset (A × A)) ∅ (a, b)
Tactic: rw [mem_filter, mem_antidiagonal, apply_ite (fun n ↦ (a, b) ∈ n), mem_singleton,
      Prod.mk_inj, ite_prop_iff_or]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : Sub A
inst_4 : OrderedSub A
inst_5 : AddLeftReflectLE A
inst_6 : HasAntidiagonal A
n m : A
inst_7 : DecidablePred fun (x : A) ↦ x = m
inst_8 : Decidable (m ≤ n)
a b : A
⊢ (a, b) ∈ {x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n | x.1 = m} ↔
    Membership.mem (γ := Finset (A × A)) (if m ≤ n then {(m, n - m)} else ∅) (a, b)
have h : a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)
Tactic: suffices a = m → (a + b = n ↔ m ≤ n ∧ b = n - m) by
    rw [mem_filter, mem_antidiagonal, apply_ite (fun n ↦ (a, b) ∈ n), mem_singleton,
      Prod.mk_inj, ite_prop_iff_or]
    simpa [← and_assoc, @and_right_comm _ (a = _), and_congr_left_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : Sub A
inst_4 : OrderedSub A
inst_5 : AddLeftReflectLE A
inst_6 : HasAntidiagonal A
n a b : A
inst_7 : DecidablePred fun (x : A) ↦ x = a
inst_8 : Decidable (a ≤ n)
⊢ a + b = n ↔ a ≤ n ∧ b = n - a
have h : a + b = n → a ≤ n ∧ b = n - a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Prod (goal)
Goal:
A : Type u_1
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : Sub A
inst_4 : OrderedSub A
inst_5 : AddLeftReflectLE A
inst_6 : HasAntidiagonal A
n a b : A
inst_7 : DecidablePred fun (x : A) ↦ x = a
inst_8 : Decidable (a ≤ n)
h : a + b = n → a ≤ n ∧ b = n - a
⊢ a + b = n ↔ a ≤ n ∧ b = n - a
have h₁ : a ≤ n ∧ b = n - a → a + b = n
Tactic: constructor