internlm/Lean-Github huggingface dataset:
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝¹ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ (ν d1 * w d1 * ν d2 * w d2 * if l ∣ d1.gcd d2 then 1 / g l else 0) =
    if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
rw [mul_ite_zero]
Proof state after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝¹ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ (if l ∣ d1.gcd d2 then ν d1 * w d1 * ν d2 * w d2 * (1 / g l) else 0) =
    if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝¹ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ (if l ∣ d1.gcd d2 then ν d1 * w d1 * ν d2 * w d2 * (1 / g l) else 0) =
    if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
apply if_congr Iff.rfl _ rfl
Proof state after:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝¹ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ ν d1 * w d1 * ν d2 * w d2 * (1 / g l) = 1 / g l * (ν d1 * w d1) * (ν d2 * w d2)
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
a✝¹ : d2 ∈ P.divisors
hgcd_dvd : d1.gcd d2 ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ ν d1 * w d1 * ν d2 * w d2 * (1 / g l) = 1 / g l * (ν d1 * w d1) * (ν d2 * w d2)
Tactic:
ring
Proof state after:
no goals
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
s : Sieve
w : ℕ → ℝ
⊢ (∑ d1 ∈ P.divisors,
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ l ∈ P.divisors,
      ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
apply symm
Proof state after:
case a
s : Sieve
w : ℕ → ℝ
⊢ (∑ l ∈ P.divisors,
      ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ d1 ∈ P.divisors,
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
case a
s : Sieve
w : ℕ → ℝ
⊢ (∑ l ∈ P.divisors,
      ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ d1 ∈ P.divisors,
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
rw [sum_comm, sum_congr rfl]
Proof state after:
case a
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    (∑ x_1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if x_1 ∣ x.gcd d2 then 1 / g x_1 * (ν x * w x) * (ν d2 * w d2) else 0) =
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ x.gcd d2 then 1 / g l * (ν x * w x) * (ν d2 * w d2) else 0
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
case a
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    (∑ x_1 ∈ P.divisors, ∑ d2 ∈ P.divisors, if x_1 ∣ x.gcd d2 then 1 / g x_1 * (ν x * w x) * (ν d2 * w d2) else 0) =
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ x.gcd d2 then 1 / g l * (ν x * w x) * (ν d2 * w d2) else 0
Tactic:
intro d1 _
Proof state after:
case a
s : Sieve
w : ℕ → ℝ
d1 : ℕ
a✝ : d1 ∈ P.divisors
⊢ (∑ x ∈ P.divisors, ∑ d2 ∈ P.divisors, if x ∣ d1.gcd d2 then 1 / g x * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Theorem: Sieve.lambdaSquared_mainSum_eq_diag_quad_form
Proof state before:
case a
s : Sieve
w : ℕ → ℝ
d1 : ℕ
a✝ : d1 ∈ P.divisors
⊢ (∑ x ∈ P.divisors, ∑ d2 ∈ P.divisors, if x ∣ d1.gcd d2 then 1 / g x * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
Tactic:
rw[sum_comm]
Proof state after:
no goals
Theorem: Nat.finMulAntidiagonal_zero
Proof state before:
d : ℕ
⊢ d.finMulAntidiagonal 0 = ∅
Tactic:
ext
Proof state after:
case a
d : ℕ
a✝ : Fin d → ℕ
⊢ a✝ ∈ d.finMulAntidiagonal 0 ↔ a✝ ∈ ∅
Theorem: Nat.finMulAntidiagonal_zero
Proof state before:
case a
d : ℕ
a✝ : Fin d → ℕ
⊢ a✝ ∈ d.finMulAntidiagonal 0 ↔ a✝ ∈ ∅
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.finMulAntidiagonal_one
Proof state before:
d : ℕ
⊢ d.finMulAntidiagonal 1 = {fun x => 1}
Tactic:
ext f
Proof state after:
case a
d : ℕ
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal 1 ↔ f ∈ {fun x => 1}
Theorem: Nat.finMulAntidiagonal_one
Proof state before:
case a
d : ℕ
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal 1 ↔ f ∈ {fun x => 1}
Tactic:
simp only [mem_finMulAntidiagonal, and_true, mem_singleton]
Proof state after:
case a
d : ℕ
f : Fin d → ℕ
⊢ ∏ i : Fin d, f i = 1 ∧ 1 ≠ 0 ↔ f = fun x => 1
Theorem: Nat.finMulAntidiagonal_one
Proof state before:
case a
d : ℕ
f : Fin d → ℕ
⊢ ∏ i : Fin d, f i = 1 ∧ 1 ≠ 0 ↔ f = fun x => 1
Tactic:
constructor
Proof state after:
case a.mp
d : ℕ
f : Fin d → ℕ
⊢ ∏ i : Fin d, f i = 1 ∧ 1 ≠ 0 → f = fun x => 1

case a.mpr
d : ℕ
f : Fin d → ℕ
⊢ (f = fun x => 1) → ∏ i : Fin d, f i = 1 ∧ 1 ≠ 0
Theorem: Nat.finMulAntidiagonal_one
Proof state before:
case a.mp
d : ℕ
f : Fin d → ℕ
⊢ ∏ i : Fin d, f i = 1 ∧ 1 ≠ 0 → f = fun x => 1
Tactic:
intro ⟨hf, _⟩
Proof state after:
case a.mp
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
⊢ f = fun x => 1
Theorem: Nat.finMulAntidiagonal_one
Proof state before:
case a.mp
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
⊢ f = fun x => 1
Tactic:
ext i
Proof state after:
case a.mp.h
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
i : Fin d
⊢ f i = 1
Theorem: Nat.finMulAntidiagonal_one
Proof state before:
case a.mp.h
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
i : Fin d
⊢ f i = 1
Tactic:
rw [←Nat.dvd_one, ←hf]
Proof state after:
case a.mp.h
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
i : Fin d
⊢ f i ∣ ∏ i : Fin d, f i
Theorem: Nat.finMulAntidiagonal_one
Proof state before:
case a.mp.h
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
i : Fin d
⊢ f i ∣ ∏ i : Fin d, f i
Tactic:
exact dvd_prod_of_mem f (mem_univ _)
Proof state after:
no goals
Theorem: Nat.finMulAntidiagonal_one
Proof state before:
case a.mpr
d : ℕ
f : Fin d → ℕ
⊢ (f = fun x => 1) → ∏ i : Fin d, f i = 1 ∧ 1 ≠ 0
Tactic:
rintro rfl
Proof state after:
case a.mpr
d : ℕ
⊢ ∏ i : Fin d, (fun x => 1) i = 1 ∧ 1 ≠ 0
Theorem: Nat.finMulAntidiagonal_one
Proof state before:
case a.mpr
d : ℕ
⊢ ∏ i : Fin d, (fun x => 1) i = 1 ∧ 1 ≠ 0
Tactic:
simp only [prod_const_one, implies_true, ne_eq, one_ne_zero, not_false_eq_true,
and_self]
Proof state after:
no goals
Theorem: Nat.finMulAntidiagonal_empty_of_ne_one
Proof state before:
n : ℕ
hn : n ≠ 1
⊢ finMulAntidiagonal 0 n = ∅
Tactic:
ext
Proof state after:
case a
n : ℕ
hn : n ≠ 1
a✝ : Fin 0 → ℕ
⊢ a✝ ∈ finMulAntidiagonal 0 n ↔ a✝ ∈ ∅
Theorem: Nat.finMulAntidiagonal_empty_of_ne_one
Proof state before:
case a
n : ℕ
hn : n ≠ 1
a✝ : Fin 0 → ℕ
⊢ a✝ ∈ finMulAntidiagonal 0 n ↔ a✝ ∈ ∅
Tactic:
simp [hn.symm]
Proof state after:
no goals
Theorem: Nat.dvd_of_mem_finMulAntidiagonal
Proof state before:
n d : ℕ
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiagonal n
i : Fin d
⊢ f i ∣ n
Tactic:
rw [mem_finMulAntidiagonal] at hf
Proof state after:
n d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
⊢ f i ∣ n
Theorem: Nat.dvd_of_mem_finMulAntidiagonal
Proof state before:
n d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
⊢ f i ∣ n
Tactic:
rw [←hf.1]
Proof state after:
n d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
⊢ f i ∣ ∏ i : Fin d, f i
Theorem: Nat.dvd_of_mem_finMulAntidiagonal
Proof state before:
n d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
⊢ f i ∣ ∏ i : Fin d, f i
Tactic:
exact dvd_prod_of_mem f (mem_univ i)
Proof state after:
no goals
Theorem: Nat.finMulAntidiagonal_univ_eq
Proof state before:
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ d.finMulAntidiagonal m = filter (fun f => ∏ i : Fin d, f i = m) (Fintype.piFinset fun x => n.divisors)
Tactic:
ext f
Proof state after:
case a
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal m ↔ f ∈ filter (fun f => ∏ i : Fin d, f i = m) (Fintype.piFinset fun x => n.divisors)
Theorem: Nat.finMulAntidiagonal_univ_eq
Proof state before:
case a
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal m ↔ f ∈ filter (fun f => ∏ i : Fin d, f i = m) (Fintype.piFinset fun x => n.divisors)
Tactic:
simp only [mem_univ, not_true, IsEmpty.forall_iff, implies_true, ne_eq, true_and,
  Fintype.mem_piFinset, mem_divisors, Nat.isUnit_iff, mem_filter]
Proof state after:
case a
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal m ↔ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m
Theorem: Nat.finMulAntidiagonal_univ_eq
Proof state before:
case a
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal m ↔ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m
Tactic:
constructor
Proof state after:
case a.mp
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal m → (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m

case a.mpr
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m → f ∈ d.finMulAntidiagonal m
Theorem: Nat.finMulAntidiagonal_univ_eq
Proof state before:
case a.mp
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal m → (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m
Tactic:
intro hf
Proof state after:
case a.mp
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiagonal m
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m
Theorem: Nat.finMulAntidiagonal_univ_eq
Proof state before:
case a.mp
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiagonal m
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m
Tactic:
refine ⟨?_, prod_eq_of_mem_finMulAntidiagonal hf⟩
Proof state after:
case a.mp
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiagonal m
⊢ ∀ (a : Fin d), f a ∣ n ∧ ¬n = 0
Theorem: Nat.finMulAntidiagonal_univ_eq
Proof state before:
case a.mp
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiagonal m
⊢ ∀ (a : Fin d), f a ∣ n ∧ ¬n = 0
Tactic:
exact fun i => ⟨(dvd_of_mem_finMulAntidiagonal hf i).trans hmn, hn⟩
Proof state after:
no goals
Theorem: Nat.finMulAntidiagonal_univ_eq
Proof state before:
case a.mpr
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m → f ∈ d.finMulAntidiagonal m
Tactic:
rw [mem_finMulAntidiagonal]
Proof state after:
case a.mpr
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m → ∏ i : Fin d, f i = m ∧ m ≠ 0
Theorem: Nat.finMulAntidiagonal_univ_eq
Proof state before:
case a.mpr
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m → ∏ i : Fin d, f i = m ∧ m ≠ 0
Tactic:
exact fun ⟨_, hprod⟩ => ⟨hprod, ne_zero_of_dvd_ne_zero hn hmn⟩
Proof state after:
no goals
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
d n : ℕ
i : Fin d
hd : d ≠ 1
⊢ image (fun f => f i) (d.finMulAntidiagonal n) = n.divisors
Tactic:
ext k
Proof state after:
case a
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∈ image (fun f => f i) (d.finMulAntidiagonal n) ↔ k ∈ n.divisors
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
case a
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∈ image (fun f => f i) (d.finMulAntidiagonal n) ↔ k ∈ n.divisors
Tactic:
simp only [mem_image, ne_eq, mem_divisors, Nat.isUnit_iff]
Proof state after:
case a
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ (∃ a ∈ d.finMulAntidiagonal n, a i = k) ↔ k ∣ n ∧ ¬n = 0
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
case a
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ (∃ a ∈ d.finMulAntidiagonal n, a i = k) ↔ k ∣ n ∧ ¬n = 0
Tactic:
constructor
Proof state after:
case a.mp
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ (∃ a ∈ d.finMulAntidiagonal n, a i = k) → k ∣ n ∧ ¬n = 0

case a.mpr
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∣ n ∧ ¬n = 0 → ∃ a ∈ d.finMulAntidiagonal n, a i = k
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
case a.mp
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ (∃ a ∈ d.finMulAntidiagonal n, a i = k) → k ∣ n ∧ ¬n = 0
Tactic:
rintro ⟨f, hf, rfl⟩
Proof state after:
case a.mp.intro.intro
d n : ℕ
i : Fin d
hd : d ≠ 1
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiagonal n
⊢ f i ∣ n ∧ ¬n = 0
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
case a.mp.intro.intro
d n : ℕ
i : Fin d
hd : d ≠ 1
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiagonal n
⊢ f i ∣ n ∧ ¬n = 0
Tactic:
refine ⟨dvd_of_mem_finMulAntidiagonal hf _, (mem_finMulAntidiagonal.mp hf).2⟩
Proof state after:
no goals
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
case a.mpr
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∣ n ∧ ¬n = 0 → ∃ a ∈ d.finMulAntidiagonal n, a i = k
Tactic:
simp_rw [mem_finMulAntidiagonal]
Proof state after:
case a.mpr
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∣ n ∧ ¬n = 0 → ∃ a, (∏ i : Fin d, a i = n ∧ n ≠ 0) ∧ a i = k
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
case a.mpr
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∣ n ∧ ¬n = 0 → ∃ a, (∏ i : Fin d, a i = n ∧ n ≠ 0) ∧ a i = k
Tactic:
rintro ⟨⟨r, rfl⟩, hn⟩
Proof state after:
case a.mpr.intro.intro
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
⊢ ∃ a, (∏ i : Fin d, a i = k * r ∧ k * r ≠ 0) ∧ a i = k
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
case a.mpr.intro.intro
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
⊢ ∃ a, (∏ i : Fin d, a i = k * r ∧ k * r ≠ 0) ∧ a i = k
Tactic:
obtain ⟨i', hi_ne⟩ := exists_ne i
Proof state after:
case a.mpr.intro.intro.intro
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ ∃ a, (∏ i : Fin d, a i = k * r ∧ k * r ≠ 0) ∧ a i = k
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
case a.mpr.intro.intro.intro
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ ∃ a, (∏ i : Fin d, a i = k * r ∧ k * r ≠ 0) ∧ a i = k
Tactic:
use fun j => if j = i then k else if j = i' then r else 1
Proof state after:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ ((∏ i_1 : Fin d, if i_1 = i then k else if i_1 = i' then r else 1) = k * r ∧ k * r ≠ 0) ∧
    (if i = i then k else if i = i' then r else 1) = k
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ ((∏ i_1 : Fin d, if i_1 = i then k else if i_1 = i' then r else 1) = k * r ∧ k * r ≠ 0) ∧
    (if i = i then k else if i = i' then r else 1) = k
Tactic:
simp only [ite_true, and_true, hn]
Proof state after:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ (∏ i_1 : Fin d, if i_1 = i then k else if i_1 = i' then r else 1) = k * r ∧ k * r ≠ 0
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ (∏ i_1 : Fin d, if i_1 = i then k else if i_1 = i' then r else 1) = k * r ∧ k * r ≠ 0
Tactic:
rw [←Finset.mul_prod_erase (a:=i) (h:=mem_univ _),
  ←Finset.mul_prod_erase (a:= i')]
Proof state after:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ (if i = i then k else if i = i' then r else 1) *
        ((if i' = i then k else if i' = i' then r else 1) *
          ∏ x ∈ (univ.erase i).erase i', if x = i then k else if x = i' then r else 1) =
      k * r ∧
    k * r ≠ 0

case h.h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ i' ∈ univ.erase i
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
case h.h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ i' ∈ univ.erase i
Tactic:
exact mem_erase.mpr ⟨hi_ne, mem_univ _⟩
Proof state after:
no goals
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
⊢ Nontrivial (Fin d)
Tactic:
rw[Fin.nontrivial_iff_two_le]
Proof state after:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
⊢ 2 ≤ d
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
⊢ 2 ≤ d
Tactic:
by_cases hd' : d = 0
Proof state after:
case pos
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hd' : d = 0
⊢ 2 ≤ d

case neg
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hd' : ¬d = 0
⊢ 2 ≤ d
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
case neg
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hd' : ¬d = 0
⊢ 2 ≤ d
Tactic:
omega
Proof state after:
no goals
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
case pos
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hd' : d = 0
⊢ 2 ≤ d
Tactic:
subst hd'
Proof state after:
case pos
k r : ℕ
hn : ¬k * r = 0
i : Fin 0
hd : 0 ≠ 1
⊢ 2 ≤ 0
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
case pos
k r : ℕ
hn : ¬k * r = 0
i : Fin 0
hd : 0 ≠ 1
⊢ 2 ≤ 0
Tactic:
apply Fin.isEmpty.elim' i
Proof state after:
no goals
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ (if i = i then k else if i = i' then r else 1) *
        ((if i' = i then k else if i' = i' then r else 1) *
          ∏ x ∈ (univ.erase i).erase i', if x = i then k else if x = i' then r else 1) =
      k * r ∧
    k * r ≠ 0
Tactic:
rw [if_neg hi_ne, if_pos rfl, if_pos rfl, prod_eq_one]
Proof state after:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ k * (r * 1) = k * r ∧ k * r ≠ 0

case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ ∀ x ∈ (univ.erase i).erase i', (if x = i then k else if x = i' then r else 1) = 1
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ ∀ x ∈ (univ.erase i).erase i', (if x = i then k else if x = i' then r else 1) = 1
Tactic:
intro j hj
Proof state after:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
j : Fin d
hj : j ∈ (univ.erase i).erase i'
⊢ (if j = i then k else if j = i' then r else 1) = 1
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
j : Fin d
hj : j ∈ (univ.erase i).erase i'
⊢ (if j = i then k else if j = i' then r else 1) = 1
Tactic:
simp only [mem_erase, ne_eq, mem_univ, and_true] at hj
Proof state after:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
j : Fin d
hj : ¬j = i' ∧ ¬j = i
⊢ (if j = i then k else if j = i' then r else 1) = 1
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
j : Fin d
hj : ¬j = i' ∧ ¬j = i
⊢ (if j = i then k else if j = i' then r else 1) = 1
Tactic:
rw [if_neg hj.1, if_neg hj.2]
Proof state after:
no goals
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ k * (r * 1) = k * r ∧ k * r ≠ 0
Tactic:
refine ⟨by ring, hn⟩
Proof state after:
no goals
Theorem: Nat.image_apply_finMulAntidiagonal
Proof state before:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ k * (r * 1) = k * r
Tactic:
ring
Proof state after:
no goals
Theorem: Nat.image_piFinTwoEquiv
Proof state before:
n : ℕ
⊢ image (⇑(piFinTwoEquiv fun x => ℕ)) (finMulAntidiagonal 2 n) = n.divisorsAntidiagonal
Tactic:
ext x
Proof state after:
case a
n : ℕ
x : ℕ × ℕ
⊢ x ∈ image (⇑(piFinTwoEquiv fun x => ℕ)) (finMulAntidiagonal 2 n) ↔ x ∈ n.divisorsAntidiagonal
Theorem: Nat.image_piFinTwoEquiv
Proof state before:
case a
n : ℕ
x : ℕ × ℕ
⊢ x ∈ image (⇑(piFinTwoEquiv fun x => ℕ)) (finMulAntidiagonal 2 n) ↔ x ∈ n.divisorsAntidiagonal
Tactic:
simp only [piFinTwoEquiv_apply, mem_image, mem_finMulAntidiagonal, Fin.prod_univ_two, ne_eq,
  mem_divisorsAntidiagonal]
Proof state after:
case a
n : ℕ
x : ℕ × ℕ
⊢ (∃ a, (a 0 * a 1 = n ∧ ¬n = 0) ∧ (a 0, a 1) = x) ↔ x.1 * x.2 = n ∧ ¬n = 0
Theorem: Nat.image_piFinTwoEquiv
Proof state before:
case a
n : ℕ
x : ℕ × ℕ
⊢ (∃ a, (a 0 * a 1 = n ∧ ¬n = 0) ∧ (a 0, a 1) = x) ↔ x.1 * x.2 = n ∧ ¬n = 0
Tactic:
constructor
Proof state after:
case a.mp
n : ℕ
x : ℕ × ℕ
⊢ (∃ a, (a 0 * a 1 = n ∧ ¬n = 0) ∧ (a 0, a 1) = x) → x.1 * x.2 = n ∧ ¬n = 0

case a.mpr
n : ℕ
x : ℕ × ℕ
⊢ x.1 * x.2 = n ∧ ¬n = 0 → ∃ a, (a 0 * a 1 = n ∧ ¬n = 0) ∧ (a 0, a 1) = x
Theorem: Nat.image_piFinTwoEquiv
Proof state before:
case a.mp
n : ℕ
x : ℕ × ℕ
⊢ (∃ a, (a 0 * a 1 = n ∧ ¬n = 0) ∧ (a 0, a 1) = x) → x.1 * x.2 = n ∧ ¬n = 0
Tactic:
rintro ⟨y, ⟨h1, h2⟩, rfl⟩
Proof state after:
case a.mp.intro.intro.intro
n : ℕ
y : Fin 2 → ℕ
h1 : y 0 * y 1 = n
h2 : ¬n = 0
⊢ (y 0, y 1).1 * (y 0, y 1).2 = n ∧ ¬n = 0
Theorem: Nat.image_piFinTwoEquiv
Proof state before:
case a.mp.intro.intro.intro
n : ℕ
y : Fin 2 → ℕ
h1 : y 0 * y 1 = n
h2 : ¬n = 0
⊢ (y 0, y 1).1 * (y 0, y 1).2 = n ∧ ¬n = 0
Tactic:
exact ⟨h1, h2⟩
Proof state after:
no goals
Theorem: Nat.image_piFinTwoEquiv
Proof state before:
case a.mpr
n : ℕ
x : ℕ × ℕ
⊢ x.1 * x.2 = n ∧ ¬n = 0 → ∃ a, (a 0 * a 1 = n ∧ ¬n = 0) ∧ (a 0, a 1) = x
Tactic:
rintro ⟨h, hn⟩
Proof state after:
case a.mpr.intro
n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n
hn : ¬n = 0
⊢ ∃ a, (a 0 * a 1 = n ∧ ¬n = 0) ∧ (a 0, a 1) = x
Theorem: Nat.image_piFinTwoEquiv
Proof state before:
case a.mpr.intro
n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n
hn : ¬n = 0
⊢ ∃ a, (a 0 * a 1 = n ∧ ¬n = 0) ∧ (a 0, a 1) = x
Tactic:
use fun i => if i = 0 then x.fst else x.snd
Proof state after:
case h
n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n
hn : ¬n = 0
⊢ (((if 0 = 0 then x.1 else x.2) * if 1 = 0 then x.1 else x.2) = n ∧ ¬n = 0) ∧
    (if 0 = 0 then x.1 else x.2, if 1 = 0 then x.1 else x.2) = x
Theorem: Nat.image_piFinTwoEquiv
Proof state before:
case h
n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n
hn : ¬n = 0
⊢ (((if 0 = 0 then x.1 else x.2) * if 1 = 0 then x.1 else x.2) = n ∧ ¬n = 0) ∧
    (if 0 = 0 then x.1 else x.2, if 1 = 0 then x.1 else x.2) = x
Tactic:
simp (config:={decide:=true}) only [ite_true, ite_false, h, mem_univ, not_true, IsEmpty.forall_iff, forall_const, not_false_eq_true,
  and_self, Prod.mk.eta, hn]
Proof state after:
no goals
Theorem: Nat.filter_primeFactors
Proof state before:
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ filter (fun p => p ∣ m) n.primeFactors = m.primeFactors
Tactic:
ext p
Proof state after:
case a
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
p : ℕ
⊢ p ∈ filter (fun p => p ∣ m) n.primeFactors ↔ p ∈ m.primeFactors
Theorem: Nat.filter_primeFactors
Proof state before:
case a
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
p : ℕ
⊢ p ∈ filter (fun p => p ∣ m) n.primeFactors ↔ p ∈ m.primeFactors
Tactic:
simp only [mem_filter, mem_primeFactors, ne_eq, hn, not_false_eq_true, and_true,
  ne_zero_of_dvd_ne_zero hn hmn, and_congr_left_iff, and_iff_left_iff_imp]
Proof state after:
case a
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
p : ℕ
⊢ p ∣ m → p.Prime → p ∣ n
Theorem: Nat.filter_primeFactors
Proof state before:
case a
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
p : ℕ
⊢ p ∣ m → p.Prime → p ∣ n
Tactic:
exact fun h _ ↦ h.trans hmn
Proof state after:
no goals
Theorem: Nat.finMulAntidiagonal_exists_unique_prime_dvd
Proof state before:
d n p : ℕ
hn : Squarefree n
hp : p ∈ n.factors
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiagonal n
⊢ ∃! i, p ∣ f i
Tactic:
rw [mem_finMulAntidiagonal] at hf
Proof state after:
d n p : ℕ
hn : Squarefree n
hp : p ∈ n.factors
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
⊢ ∃! i, p ∣ f i