awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 * b 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

Tactic:
(mul_left_inj' <| ne_zero_of_mem_finMulAntidiag hb 2).mp hfab2

Premises used: Iff.mp, mul_left_inj', OfNat.ofNat, Nat.ne_zero_of_mem_finMulAntidiag
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 * b 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

Tactic:
exact (mul_left_inj' <| ne_zero_of_mem_finMulAntidiag hb 2).mp hfab2

Premises used: Iff.mp, mul_left_inj', OfNat.ofNat, Nat.ne_zero_of_mem_finMulAntidiag
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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

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;
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
⊢ b 0 * a 1 = b 0 * b 1

Tactic:
rw [hab0] at hfab1
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
hfab1₁ : b 0 * a 1 = b 0 * b 1
⊢ a 0 * a 2 = b 0 * b 2

Tactic:
rw [hab0] at hfab1
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
hfab1₁ : b 0 * a 1 = b 0 * b 1
hfab2₁ : a 0 * a 2 = b 0 * b 2
⊢ a 0 * a 1 * a 2 = a 0 * a 1 * b 2

Tactic:
rw [hab0] at hfab1
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
hfab1₁ : b 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
⊢ a 2 = b 2

Tactic:
rw [hab0] at hfab1
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
hfab1₁ : b 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

Tactic:
rw [hab0] at hfab1
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 : b 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

Tactic:
(mul_right_inj' <| ne_zero_of_mem_finMulAntidiag hb 0).mp hfab1

Premises used: Iff.mp, mul_right_inj', OfNat.ofNat, Nat.ne_zero_of_mem_finMulAntidiag
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 : b 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

Tactic:
exact (mul_right_inj' <| ne_zero_of_mem_finMulAntidiag hb 0).mp hfab1

Premises used: Iff.mp, mul_right_inj', OfNat.ofNat, Nat.ne_zero_of_mem_finMulAntidiag
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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

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;
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
h : ∀ (i : Fin 3), a i = b i
⊢ a = b

Tactic:
funext i
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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, ⋯⟩)
h₂ : a ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) = b ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)
⊢ a i = b i

Tactic:
fin_cases i
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) = b ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)

Tactic:
assumption
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) = b ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)

Tactic:
assumption
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) = b ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)

Tactic:
assumption
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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]
rw : ∏ i : Fin 3, a i = n ∧ n ≠ 0
⊢ Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a

Tactic:
rw [mem_finMulAntidiag]

Premises used: Nat.mem_finMulAntidiag
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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]
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
⊢ ∏ i : Fin 3, a i = n ∧ n ≠ 0

Tactic:
rw [mem_filter, Finset.mem_product] at hb

Premises used: Finset.mem_filter, Finset.mem_product
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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

Tactic:
⟨?_, hn⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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]
refine : ∏ i : Fin 3, a i = n
⊢ ∏ i : Fin 3, a i = n ∧ n ≠ 0

Tactic:
refine ⟨?_, hn⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 : a 0 * a 1 * a 2 = n
⊢ ∏ i : Fin 3, a i = n

Tactic:
rw [Fin.prod_univ_three a]

Premises used: Fin.prod_univ_three
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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]
dsimp : g * (b.1 / g) * (b.2 / g) = n
⊢ a 0 * a 1 * a 2 = n

Tactic:
dsimp only [a, Matrix.cons_val]

Premises used: Matrix.cons_val
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
rw₃ rw₄ : b.1 * (b.2 / g) = b.1 * (b.2 / b.1.gcd b.2)
⊢ g * (b.1 / g) * (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)]

Premises used: Nat.lcm, Nat.gcd_dvd_left, Nat.mul_div_cancel_left', Prod.fst, And.right, Nat.gcd_dvd_right, Prod.snd, Nat.mul_div_assoc
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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

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)]
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 : ∃ (ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a), f a ha = b
⊢ ∃ (a : Fin 3 → ℕ) (ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a), f a ha = b

Tactic:
use a
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 = b
⊢ ∃ (ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a), f a ha = b

Tactic:
use ha
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
h₁ : (f a ha).2 = b.2
⊢ f a ha = b

Tactic:
apply Prod.ext

Premises used: Prod.ext
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 : g * (b.1 / g) = b.1
⊢ (f a ha).1 = b.1

Tactic:
dsimp only [a, Matrix.cons_val]

Premises used: Matrix.cons_val
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 : g * (b.2 / g) = b.2
⊢ (f a ha).2 = b.2

Tactic:
dsimp only [a, Matrix.cons_val]

Premises used: Matrix.cons_val
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 : g ∣ b.1
⊢ g * (b.1 / g) = b.1

Tactic:
apply Nat.mul_div_cancel'

Premises used: Nat.mul_div_cancel'
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 : g ∣ b.2
⊢ g * (b.2 / g) = b.2

Tactic:
apply Nat.mul_div_cancel'

Premises used: Nat.mul_div_cancel'
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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

Tactic:
apply Nat.gcd_dvd_left

Premises used: Nat.gcd_dvd_left
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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

Tactic:
apply Nat.gcd_dvd_right

Premises used: Nat.gcd_dvd_right
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n : ℕ
hn : Squarefree n
rw : card (α := Fin 3 → ℕ) (finMulAntidiag 3 n) = #({p ∈ n.divisors ×ˢ n.divisors | p.1.lcm p.2 = n})
⊢ #({p ∈ n.divisors ×ˢ n.divisors | p.1.lcm p.2 = n}) = HPow.hPow (α := ℕ) (β := ℕ) 3 ((ω : (a : ℕ) → ℕ) n : ℕ)

Tactic:
rw [← card_finMulAntidiag_of_squarefree hn, eq_comm]

Premises used: eq_comm, Nat.card_finMulAntidiag_of_squarefree
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n : ℕ
hn : Squarefree n
⊢ card (α := Fin 3 → ℕ) (finMulAntidiag 3 n) = #({p ∈ n.divisors ×ˢ n.divisors | p.1.lcm p.2 = n})

Tactic:
apply Finset.card_bij f (f_img hn) f_inj (f_surj hn.ne_zero)

Premises used: _private.0.Nat.card_pair_lcm_eq.f, _private.0.Nat.card_pair_lcm_eq.f_inj, Finset.card_bij, _private.0.Nat.card_pair_lcm_eq.f_surj, _private.0.Nat.card_pair_lcm_eq.f_img, Squarefree.ne_zero
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d : ℕ
n : μ
h : n = 0
⊢ ∀ (f : Fin 0 → μ), Membership.mem (γ := Finset (Fin 0 → μ)) {0} f ↔ ∑ i : Fin 0, f i = n

Tactic:
simp [h, Subsingleton.elim _ ![]]

Premises used: Matrix.vecEmpty, Subsingleton.elim
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
n_1 : μ
d : ℕ
n : μ
h : ¬n = 0
⊢ ∀ (f : Fin 0 → μ), Membership.mem (γ := Finset (Fin 0 → μ)) ∅ f ↔ ∑ i : Fin 0, f i = n

Tactic:
simp [Ne.symm h]

Premises used: Ne.symm
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
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
⊢ ∃ (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

Premises used: Function.Embedding.coeFn_mk, Finset.mem_map
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
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
⊢ ∃ (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

Premises used: Function.Embedding.coeFn_mk, Finset.mem_map
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
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
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
⊢ i = j

Tactic:
obtain ⟨ai, hai, hij'⟩ := hti
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
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
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
⊢ i = j

Tactic:
obtain ⟨aj, haj, rfl⟩ := htj

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
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.1 = j.1 ∧ ai = aj

Tactic:
rw [Fin.cons_inj] at hij'

Premises used: Fin.cons_inj
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
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
snd : i.2 = j.2
⊢ i = j

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Antidiag.Pi
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.1 = j.1

Tactic:
hij'.1

Premises used: And.left