awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (hypothesis)
Goal:
n : ℕ
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
b : Fin 3 → ℕ
hb : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) b
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
⊢ a 0 = b 0
have hfab2₁ : a 0 * b 2 = b 0 * b 2
Tactic: rw [hab2] at hfab2
Cleared hypotheses: hfab2, hprods, hab2
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (hypothesis)
Goal:
n : ℕ
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
b : Fin 3 → ℕ
hb : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) b
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
⊢ a = b
have hab0 : a 0 = b 0
Tactic: have hab0 : a 0 = b 0 := by
    rw [hab2] at hfab2
    exact (mul_left_inj' <| ne_zero_of_mem_finMulAntidiag hb 2).mp hfab2;
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (hypothesis)
Goal:
n : ℕ
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
b : Fin 3 → ℕ
hb : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) b
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
⊢ a 1 = b 1
have hfab1₁ : b 0 * a 1 = b 0 * b 1
Tactic: rw [hab0] at hfab1
Cleared hypotheses: hfab1, hfab2, hprods, hab2, hab0
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (hypothesis)
Goal:
n : ℕ
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
b : Fin 3 → ℕ
hb : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) b
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
⊢ a = b
have hab1 : a 1 = b 1
Tactic: have hab1 : a 1 = b 1 := by
    rw [hab0] at hfab1
    exact (mul_right_inj' <| ne_zero_of_mem_finMulAntidiag hb 0).mp hfab1;
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
b : Fin 3 → ℕ
hb : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) b
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
⊢ a = b
have h : ∀ (i : Fin 3), a i = b i
Tactic: funext i
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
b : Fin 3 → ℕ
hb : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) b
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
i : Fin 3
⊢ a i = b i
have h : a ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)) = b ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
b : Fin 3 → ℕ
hb : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) b
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
i : Fin 3
h : a ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) = b ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
⊢ a i = b i
have h₁ : a ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3)) = b ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
b : Fin 3 → ℕ
hb : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) b
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
hab1 : a 1 = b 1
i : Fin 3
h : a ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) = b ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
h₁ : a ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) = b ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)
⊢ a i = b i
have h₂ : a ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3)) = b ((fun (i : Fin 3) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
have rw : ∏ i : Fin 3, a i = n ∧ n ≠ 0
Tactic: rw [mem_finMulAntidiag]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∏ i : Fin 3, a i = n ∧ n ≠ 0
have rw : ∀ (hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n),
  let g := b.1.gcd b.2;
  let a := ![g, b.1 / g, b.2 / g];
  ∏ i : Fin 3, a i = n ∧ n ≠ 0
Tactic: rw [mem_filter, Finset.mem_product] at hb
Cleared hypotheses: hb, g, a
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∏ i : Fin 3, a i = n ∧ n ≠ 0
have refine : ∏ i : Fin 3, a i = n
Tactic: refine ⟨?_, hn⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∏ i : Fin 3, a i = n
have rw : a 0 * a 1 * a 2 = n
Tactic: rw [Fin.prod_univ_three a]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ a 0 * a 1 * a 2 = n
have dsimp : g * (b.1 / g) * (b.2 / g) = n
Tactic: dsimp only [a, Matrix.cons_val]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ g * (b.1 / g) * (b.2 / g) = n
have rw : b.1 * (b.2 / g) = n
Tactic: rw [Nat.mul_div_cancel_left' (Nat.gcd_dvd_left _ _), ← hb.2, lcm,
        Nat.mul_div_assoc b.fst (Nat.gcd_dvd_right b.fst b.snd)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
rw : b.1 * (b.2 / g) = n
⊢ g * (b.1 / g) * (b.2 / g) = n
have rw₁ : b.1 * (b.2 / g) = b.1.lcm b.2
Tactic: rw [Nat.mul_div_cancel_left' (Nat.gcd_dvd_left _ _), ← hb.2, lcm,
        Nat.mul_div_assoc b.fst (Nat.gcd_dvd_right b.fst b.snd)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
rw : b.1 * (b.2 / g) = n
rw₁ : b.1 * (b.2 / g) = b.1.lcm b.2
⊢ g * (b.1 / g) * (b.2 / g) = n
have rw₂ : b.1 * (b.2 / g) = b.1 * b.2 / b.1.gcd b.2
Tactic: rw [Nat.mul_div_cancel_left' (Nat.gcd_dvd_left _ _), ← hb.2, lcm,
        Nat.mul_div_assoc b.fst (Nat.gcd_dvd_right b.fst b.snd)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
rw : b.1 * (b.2 / g) = n
rw₁ : b.1 * (b.2 / g) = b.1.lcm b.2
rw₂ : b.1 * (b.2 / g) = b.1 * b.2 / b.1.gcd b.2
⊢ g * (b.1 / g) * (b.2 / g) = n
have rw₃ : b.1 * (b.2 / g) = b.1 * (b.2 / b.1.gcd b.2)
Tactic: rw [Nat.mul_div_cancel_left' (Nat.gcd_dvd_left _ _), ← hb.2, lcm,
        Nat.mul_div_assoc b.fst (Nat.gcd_dvd_right b.fst b.snd)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∃ (a : Fin 3 → ℕ) (ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a), f a ha = b
have ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
Tactic: have ha : a ∈ finMulAntidiag 3 n := by
    rw [mem_finMulAntidiag]
    rw [mem_filter, Finset.mem_product] at hb
    refine ⟨?_, hn⟩
    · rw [Fin.prod_univ_three a]
      dsimp only [a, Matrix.cons_val]
      rw [Nat.mul_div_cancel_left' (Nat.gcd_dvd_left _ _), ← hb.2, lcm,
        Nat.mul_div_assoc b.fst (Nat.gcd_dvd_right b.fst b.snd)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ ∃ (a : Fin 3 → ℕ) (ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a), f a ha = b
have h : ∃ (ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a), f a ha = b
Tactic: use a
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ ∃ (ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a), f a ha = b
have h : f a ha = b
Tactic: use ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ f a ha = b
have h : (f a ha).1 = b.1
Tactic: apply Prod.ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
h : (f a ha).1 = b.1
⊢ f a ha = b
have h₁ : (f a ha).2 = b.2
Tactic: apply Prod.ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ (f a ha).1 = b.1
have h : g * (b.1 / g) = b.1
Tactic: dsimp only [a, Matrix.cons_val]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ (f a ha).2 = b.2
have h : g * (b.2 / g) = b.2
Tactic: dsimp only [a, Matrix.cons_val]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ g * (b.1 / g) = b.1
have h : g ∣ b.1
Tactic: apply Nat.mul_div_cancel'
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ g * (b.2 / g) = b.2
have h : g ∣ b.2
Tactic: apply Nat.mul_div_cancel'
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : Squarefree n
⊢ #({p ∈ n.divisors ×ˢ n.divisors | p.1.lcm p.2 = n}) = HPow.hPow (α := ℕ) (β := ℕ) 3 ((ω : (a : ℕ) → ℕ) n : ℕ)
have rw : card (α := Fin 3 → ℕ) (finMulAntidiag 3 n) = #({p ∈ n.divisors ×ˢ n.divisors | p.1.lcm p.2 = n})
Tactic: rw [← card_finMulAntidiag_of_squarefree hn, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (hypothesis)
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d_1 : ℕ
n : μ
d : ℕ
i : μ × μ
_hi : i ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
j : μ × μ
_hj : j ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
hij : i ≠ j
t : Fin (d + 1) → μ
hti :
  Membership.mem (γ := Finset (Fin (d + 1) → μ))
    ((fun (ab : μ × μ) ↦
        (map
            { toFun := Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) ab.1, inj' := ⋯ : ((i : Fin d) → μ) ↪ Fin (d + 1) → μ }
            (↑(aux d ab.2) : Finset (Fin d → μ)) :
          Finset (Fin (d + 1) → μ)))
      i)
    t
htj :
  Membership.mem (γ := Finset (Fin (d + 1) → μ))
    ((fun (ab : μ × μ) ↦
        (map
            { toFun := Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) ab.1, inj' := ⋯ : ((i : Fin d) → μ) ↪ Fin (d + 1) → μ }
            (↑(aux d ab.2) : Finset (Fin d → μ)) :
          Finset (Fin (d + 1) → μ)))
      j)
    t
⊢ i = j
have hti₁ : ∃ (a : (i : Fin d) → μ),
  Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d i.2) : Finset (Fin d → μ)) a ∧
    Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) i.1 a = t
Tactic: simp_rw [Finset.mem_map, Embedding.coeFn_mk] at hti htj
Cleared hypotheses: hti, htj
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (hypothesis)
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d_1 : ℕ
n : μ
d : ℕ
i : μ × μ
_hi : i ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
j : μ × μ
_hj : j ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
hij : i ≠ j
t : Fin (d + 1) → μ
hti :
  Membership.mem (γ := Finset (Fin (d + 1) → μ))
    ((fun (ab : μ × μ) ↦
        (map
            { toFun := Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) ab.1, inj' := ⋯ : ((i : Fin d) → μ) ↪ Fin (d + 1) → μ }
            (↑(aux d ab.2) : Finset (Fin d → μ)) :
          Finset (Fin (d + 1) → μ)))
      i)
    t
htj :
  Membership.mem (γ := Finset (Fin (d + 1) → μ))
    ((fun (ab : μ × μ) ↦
        (map
            { toFun := Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) ab.1, inj' := ⋯ : ((i : Fin d) → μ) ↪ Fin (d + 1) → μ }
            (↑(aux d ab.2) : Finset (Fin d → μ)) :
          Finset (Fin (d + 1) → μ)))
      j)
    t
hti₁ :
  ∃ (a : (i : Fin d) → μ),
    Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d i.2) : Finset (Fin d → μ)) a ∧
      Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) i.1 a = t
⊢ i = j
have htj₁ : ∃ (a : (i : Fin d) → μ),
  Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d j.2) : Finset (Fin d → μ)) a ∧
    Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) j.1 a = t
Tactic: simp_rw [Finset.mem_map, Embedding.coeFn_mk] at hti htj
Cleared hypotheses: hti, htj
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d_1 : ℕ
n : μ
d : ℕ
i : μ × μ
_hi : i ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
j : μ × μ
_hj : j ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
hij : i ≠ j
t : Fin (d + 1) → μ
hti :
  ∃ (a : (i : Fin d) → μ),
    Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d i.2) : Finset (Fin d → μ)) a ∧
      Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) i.1 a = t
htj :
  ∃ (a : (i : Fin d) → μ),
    Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d j.2) : Finset (Fin d → μ)) a ∧
      Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) j.1 a = t
⊢ i = j
have obtain : ∀ (ai : (i : Fin d) → μ) (hai : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d i.2) : Finset (Fin d → μ)) ai)
  (hij' : Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) i.1 ai = t), i = j
Tactic: obtain ⟨ai, hai, hij'⟩ := hti
Cleared hypotheses: hti
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d_1 : ℕ
n : μ
d : ℕ
i : μ × μ
_hi : i ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
j : μ × μ
_hj : j ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
hij : i ≠ j
t : Fin (d + 1) → μ
htj :
  ∃ (a : (i : Fin d) → μ),
    Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d j.2) : Finset (Fin d → μ)) a ∧
      Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) j.1 a = t
ai : (i : Fin d) → μ
hai : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d i.2) : Finset (Fin d → μ)) ai
hij' : Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) i.1 ai = t
⊢ i = j
have obtain : ∀ (aj : (i : Fin d) → μ) (haj : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d j.2) : Finset (Fin d → μ)) aj)
  (hij' :
    Eq.{u_2 + 1} (α := Fin (d + 1) → μ) (Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) i.1 ai)
      (Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) j.1 aj)),
  i = j
Tactic: obtain ⟨aj, haj, rfl⟩ := htj
Cleared hypotheses: t, htj, hij'
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (hypothesis)
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d_1 : ℕ
n : μ
d : ℕ
i : μ × μ
_hi : i ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
j : μ × μ
_hj : j ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
hij : i ≠ j
ai : (i : Fin d) → μ
hai : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d i.2) : Finset (Fin d → μ)) ai
aj : (i : Fin d) → μ
haj : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d j.2) : Finset (Fin d → μ)) aj
hij' :
  Eq.{u_2 + 1} (α := Fin (d + 1) → μ) (Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) i.1 ai)
    (Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) j.1 aj)
⊢ i = j
have hij'₁ : i.1 = j.1 ∧ ai = aj
Tactic: rw [Fin.cons_inj] at hij'
Cleared hypotheses: hij'
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d_1 : ℕ
n : μ
d : ℕ
i : μ × μ
_hi : i ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
j : μ × μ
_hj : j ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
hij : i ≠ j
ai : (i : Fin d) → μ
hai : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d i.2) : Finset (Fin d → μ)) ai
aj : (i : Fin d) → μ
haj : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d j.2) : Finset (Fin d → μ)) aj
hij' : i.1 = j.1 ∧ ai = aj
⊢ i = j
have fst : i.1 = j.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d_1 : ℕ
n : μ
d : ℕ
i : μ × μ
_hi : i ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
j : μ × μ
_hj : j ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
hij : i ≠ j
ai : (i : Fin d) → μ
hai : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d i.2) : Finset (Fin d → μ)) ai
aj : (i : Fin d) → μ
haj : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d j.2) : Finset (Fin d → μ)) aj
hij' : i.1 = j.1 ∧ ai = aj
fst : i.1 = j.1
⊢ i = j
have snd : i.2 = j.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (hypothesis)
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d_1 : ℕ
n : μ
d : ℕ
i : μ × μ
_hi : i ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
j : μ × μ
_hj : j ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
hij : i ≠ j
ai : (i : Fin d) → μ
hai : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d i.2) : Finset (Fin d → μ)) ai
aj : (i : Fin d) → μ
haj : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d j.2) : Finset (Fin d → μ)) aj
hij' : i.1 = j.1 ∧ ai = aj
⊢ i.2 = j.2
have haj₁ : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d j.2) : Finset (Fin d → μ)) ai
Tactic: obtain ⟨-, rfl⟩ := hij'
Cleared hypotheses: aj, haj, hij'
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d_1 : ℕ
n : μ
d : ℕ
i : μ × μ
_hi : i ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
j : μ × μ
_hj : j ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
hij : i ≠ j
ai : (i : Fin d) → μ
hai : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d i.2) : Finset (Fin d → μ)) ai
haj : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d j.2) : Finset (Fin d → μ)) ai
⊢ i.2 = j.2
have snd : ∑ i : Fin d, ai i = j.2
Tactic: rw [← (aux d i.2).prop ai |>.mp hai, ← (aux d j.2).prop ai |>.mp haj]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d_1 : ℕ
n : μ
d : ℕ
i : μ × μ
_hi : i ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
j : μ × μ
_hj : j ∈ (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ n) : Set (μ × μ))
hij : i ≠ j
ai : (i : Fin d) → μ
hai : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d i.2) : Finset (Fin d → μ)) ai
haj : Membership.mem (γ := Finset ((i : Fin d) → μ)) (↑(aux d j.2) : Finset (Fin d → μ)) ai
snd : ∑ i : Fin d, ai i = j.2
⊢ i.2 = j.2
have snd₁ : Eq.{u_2 + 1} (α := μ) (∑ i : Fin d, ai i) (∑ i : Fin d, ai i)
Tactic: rw [← (aux d i.2).prop ai |>.mp hai, ← (aux d j.2).prop ai |>.mp haj]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Pi (goal)
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d_1 : ℕ
n : μ
d : ℕ
f : Fin (d + 1) → μ
⊢ Membership.mem (γ := Finset (Fin (d + 1) → μ))
      ((@antidiagonal _ AddCommMonoid.toAddMonoid _ n).disjiUnion
        (fun (ab : μ × μ) ↦
          map
            { toFun := Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) ab.1, inj' := ⋯ : ((i : Fin d) → μ) ↪ Fin (d + 1) → μ }
            (↑(aux d ab.2) : Finset (Fin d → μ)))
        ⋯)
      f ↔
    ∑ i : Fin (d + 1), f i = n
have simp_rw : (∃ (a : μ) (b : μ),
    a + b = n ∧
      ∃ (a_1 : (i : Fin d) → μ), ∑ i : Fin d, a_1 i = b ∧ Fin.cons (α := fun (a : Fin (d + 1)) ↦ μ) a a_1 = f) ↔
  f 0 + ∑ i : Fin d, f i.succ = n
Tactic: simp_rw [mem_disjiUnion, mem_antidiagonal, mem_map, Embedding.coeFn_mk, Prod.exists,
          (aux d _).prop, Fin.sum_univ_succ]