internlm/Lean-Github huggingface dataset:
Theorem: Nat.primeFactorsPiBij_surj
Proof state before:
case refine_2
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
⊢ Nat.primeFactorsPiBij d n f ⋯ = t
Tactic:
funext i
Proof state after:
case refine_2.h
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
⊢ Nat.primeFactorsPiBij d n f ⋯ i = t i
Theorem: Nat.primeFactorsPiBij_surj
Proof state before:
case refine_2.h
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
⊢ Nat.primeFactorsPiBij d n f ⋯ i = t i
Tactic:
have : t i ∣ n := dvd_of_mem_finMulAntidiagonal ht _
Proof state after:
case refine_2.h
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ Nat.primeFactorsPiBij d n f ⋯ i = t i
Theorem: Nat.primeFactorsPiBij_surj
Proof state before:
case refine_2.h
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ Nat.primeFactorsPiBij d n f ⋯ i = t i
Tactic:
trans (∏ p in n.primeFactors.attach, if p.1 ∣ t i then p else 1)
Proof state after:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ Nat.primeFactorsPiBij d n f ⋯ i = ∏ p ∈ n.primeFactors.attach, if ↑p ∣ t i then ↑p else 1

d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ (∏ p ∈ n.primeFactors.attach, if ↑p ∣ t i then ↑p else 1) = t i
Theorem: Nat.primeFactorsPiBij_surj
Proof state before:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ (∏ p ∈ n.primeFactors.attach, if ↑p ∣ t i then ↑p else 1) = t i
Tactic:
rw [prod_attach (f:=fun p => if p ∣ t i then p else 1), ←Finset.prod_filter]
Proof state after:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ ∏ a ∈ filter (fun x => x ∣ t i) n.primeFactors, a = t i
Theorem: Nat.primeFactorsPiBij_surj
Proof state before:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ ∏ a ∈ filter (fun x => x ∣ t i) n.primeFactors, a = t i
Tactic:
rw [filter_primeFactors this hn.ne_zero]
Proof state after:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ ∏ a ∈ (t i).primeFactors, a = t i
Theorem: Nat.primeFactorsPiBij_surj
Proof state before:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ ∏ a ∈ (t i).primeFactors, a = t i
Tactic:
apply prod_primeFactors_of_squarefree $ hn.squarefree_of_dvd this
Proof state after:
no goals
Theorem: Nat.primeFactorsPiBij_surj
Proof state before:
case refine_1
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
⊢ f ∈ n.primeFactors.pi fun x => univ
Tactic:
simp only [mem_pi]
Proof state after:
case refine_1
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
⊢ ∀ (a : ℕ) (h : a ∈ n.primeFactors), f a h ∈ univ
Theorem: Nat.primeFactorsPiBij_surj
Proof state before:
case refine_1
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
⊢ ∀ (a : ℕ) (h : a ∈ n.primeFactors), f a h ∈ univ
Tactic:
exact fun a h => mem_univ (f a h)
Proof state after:
no goals
Theorem: Nat.primeFactorsPiBij_surj
Proof state before:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ Nat.primeFactorsPiBij d n f ⋯ i = ∏ p ∈ n.primeFactors.attach, if ↑p ∣ t i then ↑p else 1
Tactic:
rw [Nat.primeFactorsPiBij, ←prod_filter]
Proof state after:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ ∏ p ∈ filter (fun p => f ↑p ⋯ = i) n.primeFactors.attach, ↑p =
    ∏ a ∈ filter (fun p => ↑p ∣ t i) n.primeFactors.attach, ↑a
Theorem: Nat.primeFactorsPiBij_surj
Proof state before:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ ∏ p ∈ filter (fun p => f ↑p ⋯ = i) n.primeFactors.attach, ↑p =
    ∏ a ∈ filter (fun p => ↑p ∣ t i) n.primeFactors.attach, ↑a
Tactic:
congr
Proof state after:
case e_s.e_p
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ (fun p => f ↑p ⋯ = i) = fun p => ↑p ∣ t i
Theorem: Nat.primeFactorsPiBij_surj
Proof state before:
case e_s.e_p
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ (fun p => f ↑p ⋯ = i) = fun p => ↑p ∣ t i
Tactic:
ext ⟨p, hp⟩
Proof state after:
case e_s.e_p.h.mk.a
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
p : ℕ
hp : p ∈ n.primeFactors
⊢ f ↑⟨p, hp⟩ ⋯ = i ↔ ↑⟨p, hp⟩ ∣ t i
Theorem: Nat.primeFactorsPiBij_surj
Proof state before:
case e_s.e_p.h.mk.a
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
p : ℕ
hp : p ∈ n.primeFactors
⊢ f ↑⟨p, hp⟩ ⋯ = i ↔ ↑⟨p, hp⟩ ∣ t i
Tactic:
refine ⟨by rintro rfl; apply hf, fun h => (hf_unique p hp i h).symm⟩
Proof state after:
no goals
Theorem: Nat.primeFactorsPiBij_surj
Proof state before:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
p : ℕ
hp : p ∈ n.primeFactors
⊢ f ↑⟨p, hp⟩ ⋯ = i → ↑⟨p, hp⟩ ∣ t i
Tactic:
rintro rfl
Proof state after:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
p : ℕ
hp : p ∈ n.primeFactors
this : t (f ↑⟨p, hp⟩ ⋯) ∣ n
⊢ ↑⟨p, hp⟩ ∣ t (f ↑⟨p, hp⟩ ⋯)
Theorem: Nat.primeFactorsPiBij_surj
Proof state before:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
p : ℕ
hp : p ∈ n.primeFactors
this : t (f ↑⟨p, hp⟩ ⋯) ∣ n
⊢ ↑⟨p, hp⟩ ∣ t (f ↑⟨p, hp⟩ ⋯)
Tactic:
apply hf
Proof state after:
no goals
Theorem: Nat.card_finMulAntidiagonal_pi
Proof state before:
d n : ℕ
hn : Squarefree n
⊢ (n.factors.toFinset.pi fun x => univ).card = (d.finMulAntidiagonal n).card
Tactic:
apply Finset.card_bij (Nat.primeFactorsPiBij d n) (primeFactorsPiBij_img d n hn)
  (primeFactorsPiBij_inj d n) (primeFactorsPiBij_surj d n hn)
Proof state after:
no goals
Theorem: Nat.card_finMulAntidiagonal
Proof state before:
d n : ℕ
hn : Squarefree n
⊢ (d.finMulAntidiagonal n).card = d ^ ω n
Tactic:
rw [←card_finMulAntidiagonal_pi d n hn, Finset.card_pi, Finset.prod_const,
  ArithmeticFunction.cardDistinctFactors_apply, List.card_toFinset, Finset.card_fin]
Proof state after:
no goals
Theorem: Nat.finMulAntidiagonal_three
Proof state before:
n : ℕ
⊢ ∀ a ∈ finMulAntidiagonal 3 n, a 0 * a 1 * a 2 = n
Tactic:
intro a ha
Proof state after:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 * a 1 * a 2 = n
Theorem: Nat.finMulAntidiagonal_three
Proof state before:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 * a 1 * a 2 = n
Tactic:
rw [← (mem_finMulAntidiagonal.mp ha).1, Fin.prod_univ_three a]
Proof state after:
no goals
Theorem: Nat.f_img
Proof state before:
n : ℕ
hn : Squarefree n
⊢ ∀ (a : Fin 3 → ℕ) (ha : a ∈ finMulAntidiagonal 3 n),
    Nat.f a ha ∈
      filter
        (fun x =>
          match x with
          | (x, y) => x.lcm y = n)
        (n.divisors ×ˢ n.divisors)
Tactic:
intro a ha
Proof state after:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ Nat.f a ha ∈
    filter
      (fun x =>
        match x with
        | (x, y) => x.lcm y = n)
      (n.divisors ×ˢ n.divisors)
Theorem: Nat.f_img
Proof state before:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ Nat.f a ha ∈
    filter
      (fun x =>
        match x with
        | (x, y) => x.lcm y = n)
      (n.divisors ×ˢ n.divisors)
Tactic:
rw [mem_filter, Finset.mem_product, mem_divisors, mem_divisors, Nat.f]
Proof state after:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (((a 0 * a 1, a 0 * a 2).1 ∣ n ∧ n ≠ 0) ∧ (a 0 * a 1, a 0 * a 2).2 ∣ n ∧ n ≠ 0) ∧
    match (a 0 * a 1, a 0 * a 2) with
    | (x, y) => x.lcm y = n
Theorem: Nat.f_img
Proof state before:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (((a 0 * a 1, a 0 * a 2).1 ∣ n ∧ n ≠ 0) ∧ (a 0 * a 1, a 0 * a 2).2 ∣ n ∧ n ≠ 0) ∧
    match (a 0 * a 1, a 0 * a 2) with
    | (x, y) => x.lcm y = n
Tactic:
refine ⟨⟨⟨?_, hn.ne_zero⟩, ⟨?_, hn.ne_zero⟩⟩, ?_⟩ <;> rw [←finMulAntidiagonal_three a ha]
Proof state after:
case refine_1
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (a 0 * a 1, a 0 * a 2).1 ∣ a 0 * a 1 * a 2

case refine_2
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (a 0 * a 1, a 0 * a 2).2 ∣ a 0 * a 1 * a 2

case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ match (a 0 * a 1, a 0 * a 2) with
  | (x, y) => x.lcm y = a 0 * a 1 * a 2
Theorem: Nat.f_img
Proof state before:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ match (a 0 * a 1, a 0 * a 2) with
  | (x, y) => x.lcm y = a 0 * a 1 * a 2
Tactic:
dsimp only
Proof state after:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (a 0 * a 1).lcm (a 0 * a 2) = a 0 * a 1 * a 2
Theorem: Nat.f_img
Proof state before:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (a 0 * a 1).lcm (a 0 * a 2) = a 0 * a 1 * a 2
Tactic:
rw [lcm_mul_left, Nat.Coprime.lcm_eq_mul]
Proof state after:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 * (a 1 * a 2) = a 0 * a 1 * a 2

case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (a 1).Coprime (a 2)
Theorem: Nat.f_img
Proof state before:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (a 1).Coprime (a 2)
Tactic:
refine coprime_of_squarefree_mul (hn.squarefree_of_dvd ?_)
Proof state after:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 1 * a 2 ∣ n
Theorem: Nat.f_img
Proof state before:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 1 * a 2 ∣ n
Tactic:
use a 0
Proof state after:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ n = a 1 * a 2 * a 0
Theorem: Nat.f_img
Proof state before:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ n = a 1 * a 2 * a 0
Tactic:
rw [←finMulAntidiagonal_three a ha]
Proof state after:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 * a 1 * a 2 = a 1 * a 2 * a 0
Theorem: Nat.f_img
Proof state before:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 * a 1 * a 2 = a 1 * a 2 * a 0
Tactic:
ring
Proof state after:
no goals
Theorem: Nat.f_img
Proof state before:
case refine_1
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (a 0 * a 1, a 0 * a 2).1 ∣ a 0 * a 1 * a 2
Tactic:
apply dvd_mul_right _ (a 2)
Proof state after:
no goals
Theorem: Nat.f_img
Proof state before:
case refine_2
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (a 0 * a 1, a 0 * a 2).2 ∣ a 0 * a 1 * a 2
Tactic:
use a 1
Proof state after:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 * a 1 * a 2 = (a 0 * a 1, a 0 * a 2).2 * a 1
Theorem: Nat.f_img
Proof state before:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 * a 1 * a 2 = (a 0 * a 1, a 0 * a 2).2 * a 1
Tactic:
ring
Proof state after:
no goals
Theorem: Nat.f_img
Proof state before:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 * (a 1 * a 2) = a 0 * a 1 * a 2
Tactic:
ring
Proof state after:
no goals
Theorem: Nat.f_inj
Proof state before:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
⊢ a = b
Tactic:
obtain ⟨hfab1, hfab2⟩ := Prod.mk.inj hfab
Proof state after:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
⊢ a = b
Theorem: Nat.f_inj
Proof state before:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
⊢ a = b
Tactic:
have hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2 := by
  rw [finMulAntidiagonal_three a ha, hfab1, finMulAntidiagonal_three b hb]
Proof state after:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.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
⊢ a = b
Theorem: Nat.f_inj
Proof state before:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.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
⊢ a = b
Tactic:
have hab2 : a 2 = b 2 := by
  rw [← mul_right_inj' $ mul_ne_zero (ne_zero_of_mem_finMulAntidiagonal ha 0)
    (ne_zero_of_mem_finMulAntidiagonal ha 1)]
  exact hprods
Proof state after:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.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
Theorem: Nat.f_inj
Proof state before:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.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
Tactic:
have hab0 : a 0 = b 0 := by
  rw [hab2] at hfab2
  exact (mul_left_inj' $ ne_zero_of_mem_finMulAntidiagonal hb 2).mp hfab2;
Proof state after:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.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
Theorem: Nat.f_inj
Proof state before:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.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
Tactic:
have hab1 : a 1 = b 1 := by
  rw [hab0] at hfab1
  exact (mul_right_inj' $ ne_zero_of_mem_finMulAntidiagonal hb 0).mp hfab1;
Proof state after:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.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
Theorem: Nat.f_inj
Proof state before:
case intro
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.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
Tactic:
funext i
Proof state after:
case intro.h
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.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
Theorem: Nat.f_inj
Proof state before:
case intro.h
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.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
Tactic:
fin_cases i <;> assumption
Proof state after:
no goals
Theorem: Nat.f_inj
Proof state before:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.f b hb
hfab1 : a 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 [finMulAntidiagonal_three a ha, hfab1, finMulAntidiagonal_three b hb]
Proof state after:
no goals
Theorem: Nat.f_inj
Proof state before:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.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
⊢ a 2 = b 2
Tactic:
rw [← mul_right_inj' $ mul_ne_zero (ne_zero_of_mem_finMulAntidiagonal ha 0)
  (ne_zero_of_mem_finMulAntidiagonal ha 1)]
Proof state after:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.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
⊢ a 0 * a 1 * a 2 = a 0 * a 1 * b 2
Theorem: Nat.f_inj
Proof state before:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.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
⊢ a 0 * a 1 * a 2 = a 0 * a 1 * b 2
Tactic:
exact hprods
Proof state after:
no goals
Theorem: Nat.f_inj
Proof state before:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.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:
rw [hab2] at hfab2
Proof state after:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.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
Theorem: Nat.f_inj
Proof state before:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.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_finMulAntidiagonal hb 2).mp hfab2
Proof state after:
no goals
Theorem: Nat.f_inj
Proof state before:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.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:
rw [hab0] at hfab1
Proof state after:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiagonal 3 n
hfab : Nat.f a ha = Nat.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