awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommRing A
n p : ℕ
h_1 : p.Coprime n
m : ℕ
hm : HPow.hPow (α := A) (↑p : A) m = 0
a b : A
h : HPow.hPow (α := A) (↑p : A) m * a + (↑n : A) * b = 1
⊢ IsUnit.{u_1} (M := A) (↑n : A)
have refine : (↑n : A) * b = 1
Tactic: refine .of_mul_eq_one b ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : HPow.hPow (α := A) (↑p : A) m = 0
⊢ IsUnit.{u_1} (M := A) (↑n : A)
have suffices : ∃ (a : A) (b : A), HPow.hPow (α := A) (↑p : A) m * a + (↑n : A) * b = 1
Tactic: suffices ∃ a b : A, p ^ m * a + n * b = 1 by
    obtain ⟨a, b, h⟩ := this
    refine .of_mul_eq_one b ?_
    simpa [hm] using h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : HPow.hPow (α := A) (↑p : A) m = 0
⊢ ∃ (a : A) (b : A), HPow.hPow (α := A) (↑p : A) m * a + (↑n : A) * b = 1
have refine : HPow.hPow (α := A) (↑p : A) m * (↑((p ^ m).gcdA n) : A) + HMul.hMul (α := A) (↑n : A) (↑((p ^ m).gcdB n) : A) = 1
Tactic: refine ⟨(p ^ m).gcdA n, (p ^ m).gcdB n, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : HPow.hPow (α := A) (↑p : A) m = 0
⊢ HPow.hPow (α := A) (↑p : A) m * (↑((p ^ m).gcdA n) : A) + HMul.hMul (α := A) (↑n : A) (↑((p ^ m).gcdB n) : A) = 1
have norm_cast : Eq.{u_1 + 1} (α := A) (↑((↑(p ^ m) : ℤ) * (p ^ m).gcdA n + (↑n : ℤ) * (p ^ m).gcdB n) : A) 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : HPow.hPow (α := A) (↑p : A) m = 0
⊢ Eq.{u_1 + 1} (α := A) (↑((↑(p ^ m) : ℤ) * (p ^ m).gcdA n + (↑n : ℤ) * (p ^ m).gcdB n) : A) 1
have rw : Eq.{u_1 + 1} (α := A) (↑((↑(p ^ m) : ℤ) * (p ^ m).gcdA n + (↑n : ℤ) * (p ^ m).gcdB n) : A) (↑1 : A)
Tactic: rw [← Nat.cast_one, ← Int.cast_natCast 1, ← (h.pow_left m).gcd_eq_one, Nat.gcd_eq_gcd_ab]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : HPow.hPow (α := A) (↑p : A) m = 0
rw : Eq.{u_1 + 1} (α := A) (↑((↑(p ^ m) : ℤ) * (p ^ m).gcdA n + (↑n : ℤ) * (p ^ m).gcdB n) : A) (↑1 : A)
⊢ Eq.{u_1 + 1} (α := A) (↑((↑(p ^ m) : ℤ) * (p ^ m).gcdA n + (↑n : ℤ) * (p ^ m).gcdB n) : A) 1
have rw₁ : Eq.{u_1 + 1} (α := A) (↑((↑(p ^ m) : ℤ) * (p ^ m).gcdA n + (↑n : ℤ) * (p ^ m).gcdB n) : A) (↑(↑1 : ℤ) : A)
Tactic: rw [← Nat.cast_one, ← Int.cast_natCast 1, ← (h.pow_left m).gcd_eq_one, Nat.gcd_eq_gcd_ab]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : HPow.hPow (α := A) (↑p : A) m = 0
rw : Eq.{u_1 + 1} (α := A) (↑((↑(p ^ m) : ℤ) * (p ^ m).gcdA n + (↑n : ℤ) * (p ^ m).gcdB n) : A) (↑1 : A)
rw₁ : Eq.{u_1 + 1} (α := A) (↑((↑(p ^ m) : ℤ) * (p ^ m).gcdA n + (↑n : ℤ) * (p ^ m).gcdB n) : A) (↑(↑1 : ℤ) : A)
⊢ Eq.{u_1 + 1} (α := A) (↑((↑(p ^ m) : ℤ) * (p ^ m).gcdA n + (↑n : ℤ) * (p ^ m).gcdB n) : A) 1
have rw₂ : Eq.{u_1 + 1} (α := A) (↑((↑(p ^ m) : ℤ) * (p ^ m).gcdA n + (↑n : ℤ) * (p ^ m).gcdB n) : A) (↑(↑((p ^ m).gcd n) : ℤ) : A)
Tactic: rw [← Nat.cast_one, ← Int.cast_natCast 1, ← (h.pow_left m).gcd_eq_one, Nat.gcd_eq_gcd_ab]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : HPow.hPow (α := A) (↑p : A) m = 0
rw : Eq.{u_1 + 1} (α := A) (↑((↑(p ^ m) : ℤ) * (p ^ m).gcdA n + (↑n : ℤ) * (p ^ m).gcdB n) : A) (↑1 : A)
rw₁ : Eq.{u_1 + 1} (α := A) (↑((↑(p ^ m) : ℤ) * (p ^ m).gcdA n + (↑n : ℤ) * (p ^ m).gcdB n) : A) (↑(↑1 : ℤ) : A)
rw₂ :
  Eq.{u_1 + 1} (α := A) (↑((↑(p ^ m) : ℤ) * (p ^ m).gcdA n + (↑n : ℤ) * (p ^ m).gcdB n) : A)
    (↑(↑((p ^ m).gcd n) : ℤ) : A)
⊢ Eq.{u_1 + 1} (α := A) (↑((↑(p ^ m) : ℤ) * (p ^ m).gcdA n + (↑n : ℤ) * (p ^ m).gcdB n) : A) 1
have rw₃ : Eq.{u_1 + 1} (α := A) (↑((↑(p ^ m) : ℤ) * (p ^ m).gcdA n + (↑n : ℤ) * (p ^ m).gcdB n) : A)
  (↑((↑(p ^ m) : ℤ) * (p ^ m).gcdA n + (↑n : ℤ) * (p ^ m).gcdB n) : A)
Tactic: rw [← Nat.cast_one, ← Int.cast_natCast 1, ← (h.pow_left m).gcd_eq_one, Nat.gcd_eq_gcd_ab]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommRing A
n_1 p : ℕ
hp : IsNilpotent.{u_1} (R := A) (↑p : A)
inst_1 : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (h : n < p), IsUnit.{u_1} (M := A) (↑n ! : A)
h : n + 1 < p
⊢ IsUnit.{u_1} (M := A) (↑(n + 1)! : A)
have succ : IsUnit.{u_1} (M := A) (↑(n + 1) : A) ∧ IsUnit.{u_1} (M := A) (↑n ! : A)
Tactic: simp only [factorial_succ, cast_mul, IsUnit.mul_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommRing A
n_1 p : ℕ
hp : IsNilpotent.{u_1} (R := A) (↑p : A)
inst_1 : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (h : n < p), IsUnit.{u_1} (M := A) (↑n ! : A)
h : n + 1 < p
⊢ IsUnit.{u_1} (M := A) (↑(n + 1) : A) ∧ IsUnit.{u_1} (M := A) (↑n ! : A)
have succ : p.Coprime (n + 1)
Tactic: refine ⟨.natCast_of_isNilpotent_of_coprime hp ?_, ih (by lia)⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommRing A
n_1 p : ℕ
hp : IsNilpotent.{u_1} (R := A) (↑p : A)
inst_1 : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (h : n < p), IsUnit.{u_1} (M := A) (↑n ! : A)
h : n + 1 < p
⊢ p.Coprime (n + 1)
have succ : ¬p ∣ n + 1
Tactic: rw [Nat.Prime.coprime_iff_not_dvd Fact.out]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommRing A
n p : ℕ
hp : IsNilpotent.{u_1} (R := A) (↑p : A)
inst_1 : Fact (Nat.Prime p)
h : n < p
⊢ IsUnit.{u_1} (M := A) (↑n ! : A)
have zero : ∀ (h : 0 < p), IsUnit.{u_1} (M := A) (↑0! : A)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    simp only [factorial_succ, cast_mul, IsUnit.mul_iff]
    refine ⟨.natCast_of_isNilpotent_of_coprime hp ?_, ih (by lia)⟩
    rw [Nat.Prime.coprime_iff_not_dvd Fact.out]
    exact Nat.not_dvd_of_pos_of_lt (by lia) h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommRing A
n p : ℕ
hp : IsNilpotent.{u_1} (R := A) (↑p : A)
inst_1 : Fact (Nat.Prime p)
h : n < p
zero : ∀ (h : 0 < p), IsUnit.{u_1} (M := A) (↑0! : A)
⊢ IsUnit.{u_1} (M := A) (↑n ! : A)
have succ : ∀ (n : ℕ) (ih : ∀ (h : n < p), IsUnit.{u_1} (M := A) (↑n ! : A)) (h : n + 1 < p), IsUnit.{u_1} (M := A) (↑(n + 1)! : A)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    simp only [factorial_succ, cast_mul, IsUnit.mul_iff]
    refine ⟨.natCast_of_isNilpotent_of_coprime hp ?_, ih (by lia)⟩
    rw [Nat.Prime.coprime_iff_not_dvd Fact.out]
    exact Nat.not_dvd_of_pos_of_lt (by lia) h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (hypothesis)
Goal:
A : Type u_1
inst : CommSemiring A
m : ℕ
k : ℕ × ℕ
hm : IsUnit.{u_1} (M := A) (↑m ! : A)
hk : k ∈ @Finset.antidiagonal _ instAddMonoid _ m
⊢ (↑(m.choose k.1) : A) = HMul.hMul (α := A) (↑m ! : A) (↑k.1! : A)⁻¹ʳ * (↑k.2! : A)⁻¹ʳ
have hk₁ : k.1 + k.2 = m
Tactic: rw [Finset.mem_antidiagonal] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommSemiring A
m : ℕ
k : ℕ × ℕ
hm : IsUnit.{u_1} (M := A) (↑m ! : A)
hk : k.1 + k.2 = m
⊢ (↑(m.choose k.1) : A) = HMul.hMul (α := A) (↑m ! : A) (↑k.1! : A)⁻¹ʳ * (↑k.2! : A)⁻¹ʳ
have subst : ∀ (hm : IsUnit.{u_1} (M := A) (↑(k.1 + k.2)! : A)),
  (↑((k.1 + k.2).choose k.1) : A) = HMul.hMul (α := A) (↑(k.1 + k.2)! : A) (↑k.1! : A)⁻¹ʳ * (↑k.2! : A)⁻¹ʳ
Tactic: subst hk
Cleared hypotheses: m, hm, hk
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommSemiring A
k : ℕ × ℕ
hm : IsUnit.{u_1} (M := A) (↑(k.1 + k.2)! : A)
⊢ (↑((k.1 + k.2).choose k.1) : A) = HMul.hMul (α := A) (↑(k.1 + k.2)! : A) (↑k.1! : A)⁻¹ʳ * (↑k.2! : A)⁻¹ʳ
have h : IsUnit.{u_1} (M := A) (↑k.1! : A)
Tactic: rw [eq_mul_inverse_iff_mul_eq, eq_mul_inverse_iff_mul_eq, ← Nat.cast_mul, ← Nat.cast_mul,
    add_comm, Nat.add_choose_mul_factorial_mul_factorial]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommSemiring A
k : ℕ × ℕ
hm : IsUnit.{u_1} (M := A) (↑(k.1 + k.2)! : A)
h : IsUnit.{u_1} (M := A) (↑k.1! : A)
⊢ (↑((k.1 + k.2).choose k.1) : A) = HMul.hMul (α := A) (↑(k.1 + k.2)! : A) (↑k.1! : A)⁻¹ʳ * (↑k.2! : A)⁻¹ʳ
have h₁ : IsUnit.{u_1} (M := A) (↑k.2! : A)
Tactic: rw [eq_mul_inverse_iff_mul_eq, eq_mul_inverse_iff_mul_eq, ← Nat.cast_mul, ← Nat.cast_mul,
    add_comm, Nat.add_choose_mul_factorial_mul_factorial]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommSemiring A
k : ℕ × ℕ
hm : IsUnit.{u_1} (M := A) (↑(k.1 + k.2)! : A)
⊢ IsUnit.{u_1} (M := A) (↑k.1! : A)
have h : k.1 ≤ k.1 + k.2
Tactic: apply hm.natCast_factorial_of_le
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.NatCast (goal)
Goal:
A : Type u_1
inst : CommSemiring A
k : ℕ × ℕ
hm : IsUnit.{u_1} (M := A) (↑(k.1 + k.2)! : A)
⊢ IsUnit.{u_1} (M := A) (↑k.2! : A)
have h : k.2 ≤ k.1 + k.2
Tactic: apply hm.natCast_factorial_of_le
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.SuperFactorial (goal)
Goal:
n : ℕ
⊢ ∏ x ∈ Icc 1 (n + 1), x ! = sf n + 1
have rw : ∏ x ∈ Ico 1 (n + 1 + 1), x ! = sf n + 1
Tactic: rw [← Ico_add_one_right_eq_Icc 1, prod_Ico_succ_top le_add_self, Nat.factorial_succ,
      Ico_add_one_right_eq_Icc 1 n, prod_Icc_factorial n, superFactorial, factorial, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.SuperFactorial (goal)
Goal:
n : ℕ
rw : ∏ x ∈ Ico 1 (n + 1 + 1), x ! = sf n + 1
⊢ ∏ x ∈ Icc 1 (n + 1), x ! = sf n + 1
have rw₁ : (∏ k ∈ Ico 1 (n + 1), k !) * (n + 1)! = sf n + 1
Tactic: rw [← Ico_add_one_right_eq_Icc 1, prod_Ico_succ_top le_add_self, Nat.factorial_succ,
      Ico_add_one_right_eq_Icc 1 n, prod_Icc_factorial n, superFactorial, factorial, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.SuperFactorial (goal)
Goal:
n : ℕ
rw : ∏ x ∈ Ico 1 (n + 1 + 1), x ! = sf n + 1
rw₁ : (∏ k ∈ Ico 1 (n + 1), k !) * (n + 1)! = sf n + 1
⊢ ∏ x ∈ Icc 1 (n + 1), x ! = sf n + 1
have rw₂ : (∏ k ∈ Ico 1 (n + 1), k !) * ((n + 1) * n !) = sf n + 1
Tactic: rw [← Ico_add_one_right_eq_Icc 1, prod_Ico_succ_top le_add_self, Nat.factorial_succ,
      Ico_add_one_right_eq_Icc 1 n, prod_Icc_factorial n, superFactorial, factorial, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.SuperFactorial (goal)
Goal:
n : ℕ
rw : ∏ x ∈ Ico 1 (n + 1 + 1), x ! = sf n + 1
rw₁ : (∏ k ∈ Ico 1 (n + 1), k !) * (n + 1)! = sf n + 1
rw₂ : (∏ k ∈ Ico 1 (n + 1), k !) * ((n + 1) * n !) = sf n + 1
⊢ ∏ x ∈ Icc 1 (n + 1), x ! = sf n + 1
have rw₃ : (∏ k ∈ Icc 1 n, k !) * ((n + 1) * n !) = sf n + 1
Tactic: rw [← Ico_add_one_right_eq_Icc 1, prod_Ico_succ_top le_add_self, Nat.factorial_succ,
      Ico_add_one_right_eq_Icc 1 n, prod_Icc_factorial n, superFactorial, factorial, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.SuperFactorial (goal)
Goal:
n : ℕ
rw : ∏ x ∈ Ico 1 (n + 1 + 1), x ! = sf n + 1
rw₁ : (∏ k ∈ Ico 1 (n + 1), k !) * (n + 1)! = sf n + 1
rw₂ : (∏ k ∈ Ico 1 (n + 1), k !) * ((n + 1) * n !) = sf n + 1
rw₃ : (∏ k ∈ Icc 1 n, k !) * ((n + 1) * n !) = sf n + 1
⊢ ∏ x ∈ Icc 1 (n + 1), x ! = sf n + 1
have rw₄ : (sf n) * ((n + 1) * n !) = sf n + 1
Tactic: rw [← Ico_add_one_right_eq_Icc 1, prod_Ico_succ_top le_add_self, Nat.factorial_succ,
      Ico_add_one_right_eq_Icc 1 n, prod_Icc_factorial n, superFactorial, factorial, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.SuperFactorial (goal)
Goal:
n : ℕ
rw : ∏ x ∈ Ico 1 (n + 1 + 1), x ! = sf n + 1
rw₁ : (∏ k ∈ Ico 1 (n + 1), k !) * (n + 1)! = sf n + 1
rw₂ : (∏ k ∈ Ico 1 (n + 1), k !) * ((n + 1) * n !) = sf n + 1
rw₃ : (∏ k ∈ Icc 1 n, k !) * ((n + 1) * n !) = sf n + 1
rw₄ : (sf n) * ((n + 1) * n !) = sf n + 1
⊢ ∏ x ∈ Icc 1 (n + 1), x ! = sf n + 1
have rw₅ : (sf n) * ((n + 1) * n !) = n.succ ! * sf n
Tactic: rw [← Ico_add_one_right_eq_Icc 1, prod_Ico_succ_top le_add_self, Nat.factorial_succ,
      Ico_add_one_right_eq_Icc 1 n, prod_Icc_factorial n, superFactorial, factorial, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.SuperFactorial (goal)
Goal:
n : ℕ
rw : ∏ x ∈ Ico 1 (n + 1 + 1), x ! = sf n + 1
rw₁ : (∏ k ∈ Ico 1 (n + 1), k !) * (n + 1)! = sf n + 1
rw₂ : (∏ k ∈ Ico 1 (n + 1), k !) * ((n + 1) * n !) = sf n + 1
rw₃ : (∏ k ∈ Icc 1 n, k !) * ((n + 1) * n !) = sf n + 1
rw₄ : (sf n) * ((n + 1) * n !) = sf n + 1
rw₅ : (sf n) * ((n + 1) * n !) = n.succ ! * sf n
⊢ ∏ x ∈ Icc 1 (n + 1), x ! = sf n + 1
have rw₆ : (sf n) * ((n + 1) * n !) = n.succ * n ! * sf n
Tactic: rw [← Ico_add_one_right_eq_Icc 1, prod_Ico_succ_top le_add_self, Nat.factorial_succ,
      Ico_add_one_right_eq_Icc 1 n, prod_Icc_factorial n, superFactorial, factorial, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.SuperFactorial (goal)
Goal:
n : ℕ
rw : ∏ x ∈ Ico 1 (n + 1 + 1), x ! = sf n + 1
rw₁ : (∏ k ∈ Ico 1 (n + 1), k !) * (n + 1)! = sf n + 1
rw₂ : (∏ k ∈ Ico 1 (n + 1), k !) * ((n + 1) * n !) = sf n + 1
rw₃ : (∏ k ∈ Icc 1 n, k !) * ((n + 1) * n !) = sf n + 1
rw₄ : (sf n) * ((n + 1) * n !) = sf n + 1
rw₅ : (sf n) * ((n + 1) * n !) = n.succ ! * sf n
rw₆ : (sf n) * ((n + 1) * n !) = n.succ * n ! * sf n
⊢ ∏ x ∈ Icc 1 (n + 1), x ! = sf n + 1
have rw₇ : (n + 1) * n ! * sf n = n.succ * n ! * sf n
Tactic: rw [← Ico_add_one_right_eq_Icc 1, prod_Ico_succ_top le_add_self, Nat.factorial_succ,
      Ico_add_one_right_eq_Icc 1 n, prod_Icc_factorial n, superFactorial, factorial, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.SuperFactorial (goal)
Goal:
n : ℕ
⊢ ∏ x ∈ range (n + 1 + 1), x ! = sf n + 1
have rw : (∏ x ∈ range (n + 1), x !) * (n + 1)! = sf n + 1
Tactic: rw [prod_range_succ, prod_range_succ_factorial n, mul_comm, superFactorial]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.SuperFactorial (goal)
Goal:
n : ℕ
rw : (∏ x ∈ range (n + 1), x !) * (n + 1)! = sf n + 1
⊢ ∏ x ∈ range (n + 1 + 1), x ! = sf n + 1
have rw₁ : (sf n) * (n + 1)! = sf n + 1
Tactic: rw [prod_range_succ, prod_range_succ_factorial n, mul_comm, superFactorial]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.SuperFactorial (goal)
Goal:
n : ℕ
rw : (∏ x ∈ range (n + 1), x !) * (n + 1)! = sf n + 1
rw₁ : (sf n) * (n + 1)! = sf n + 1
⊢ ∏ x ∈ range (n + 1 + 1), x ! = sf n + 1
have rw₂ : (n + 1)! * sf n = sf n + 1
Tactic: rw [prod_range_succ, prod_range_succ_factorial n, mul_comm, superFactorial]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.SuperFactorial (goal)
Goal:
n : ℕ
rw : (∏ x ∈ range (n + 1), x !) * (n + 1)! = sf n + 1
rw₁ : (sf n) * (n + 1)! = sf n + 1
rw₂ : (n + 1)! * sf n = sf n + 1
⊢ ∏ x ∈ range (n + 1 + 1), x ! = sf n + 1
have rw₃ : (n + 1)! * sf n = n.succ ! * sf n
Tactic: rw [prod_range_succ, prod_range_succ_factorial n, mul_comm, superFactorial]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.SuperFactorial (goal)
Goal:
n : ℕ
⊢ sf 2 * (n + 1) =
    HPow.hPow (α := ℕ) (β := ℕ) (∏ i ∈ range (n + 1), (2 * i + 1)!) 2 * HPow.hPow (α := ℕ) 2 (n + 1) * (n + 1)!
have simp : (2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!) *
    ((2 * n + 1) * (2 * n)! *
      (HPow.hPow (α := ℕ) (β := ℕ) (∏ x ∈ range n, (2 * x + 1) * (2 * x)!) 2 * HPow.hPow (α := ℕ) 2 n * n !)) =
  HPow.hPow (α := ℕ) (β := ℕ) (∏ x ∈ range n, (2 * x + 1) * (2 * x)!) 2 *
        (HPow.hPow (β := ℕ) (2 * n + 1) 2 * HPow.hPow (β := ℕ) (2 * n)! 2) *
      HPow.hPow (α := ℕ) 2 (n + 1) *
    ((n + 1) * n !)
Tactic: simp only [prod_range_succ, mul_pow, mul_add, mul_one, superFactorial_succ,
      superFactorial_two_mul n, factorial_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.SuperFactorial (goal)
Goal:
n : ℕ
⊢ sf 4 * n = HPow.hPow (α := ℕ) (β := ℕ) (∏ i ∈ range (2 * n), (2 * i + 1)!) 2 * HPow.hPow (α := ℕ) 2 (2 * n) * (2 * n)!
have rw : sf 4 * n = sf 2 * (2 * n)
Tactic: rw [← superFactorial_two_mul, ← mul_assoc, Nat.mul_two]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.SuperFactorial (goal)
Goal:
n : ℕ
rw : sf 4 * n = sf 2 * (2 * n)
⊢ sf 4 * n = HPow.hPow (α := ℕ) (β := ℕ) (∏ i ∈ range (2 * n), (2 * i + 1)!) 2 * HPow.hPow (α := ℕ) 2 (2 * n) * (2 * n)!
have rw₁ : sf 4 * n = sf HMul.hMul (α := ℕ) 2 2 * n
Tactic: rw [← superFactorial_two_mul, ← mul_assoc, Nat.mul_two]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.SuperFactorial (goal)
Goal:
n : ℕ
rw : sf 4 * n = sf 2 * (2 * n)
rw₁ : sf 4 * n = sf HMul.hMul (α := ℕ) 2 2 * n
⊢ sf 4 * n = HPow.hPow (α := ℕ) (β := ℕ) (∏ i ∈ range (2 * n), (2 * i + 1)!) 2 * HPow.hPow (α := ℕ) 2 (2 * n) * (2 * n)!
have rw₂ : sf 4 * n = sf HAdd.hAdd (α := ℕ) 2 2 * n
Tactic: rw [← superFactorial_two_mul, ← mul_assoc, Nat.mul_two]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.SuperFactorial (goal)
Goal:
n : ℕ
⊢ HPow.hPow (α := ℕ) (β := ℕ) (∏ i ∈ range (2 * n), (2 * i + 1)!) 2 * HPow.hPow (α := ℕ) 2 (2 * n) * (2 * n)! =
    HPow.hPow (β := ℕ) ((∏ i ∈ range (2 * n), (2 * i + 1)!) * HPow.hPow (α := ℕ) 2 n) 2 * (2 * n)!
have rw : HPow.hPow (α := ℕ) (β := ℕ) (∏ i ∈ range (2 * n), (2 * i + 1)!) 2 * HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 n) 2 *
    (2 * n)! =
  HPow.hPow (β := ℕ) ((∏ i ∈ range (2 * n), (2 * i + 1)!) * HPow.hPow (α := ℕ) 2 n) 2 * (2 * n)!
Tactic: rw [pow_mul', mul_pow]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorial.SuperFactorial (goal)
Goal:
n : ℕ
rw :
  HPow.hPow (α := ℕ) (β := ℕ) (∏ i ∈ range (2 * n), (2 * i + 1)!) 2 * HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 n) 2 *
      (2 * n)! =
    HPow.hPow (β := ℕ) ((∏ i ∈ range (2 * n), (2 * i + 1)!) * HPow.hPow (α := ℕ) 2 n) 2 * (2 * n)!
⊢ HPow.hPow (α := ℕ) (β := ℕ) (∏ i ∈ range (2 * n), (2 * i + 1)!) 2 * HPow.hPow (α := ℕ) 2 (2 * n) * (2 * n)! =
    HPow.hPow (β := ℕ) ((∏ i ∈ range (2 * n), (2 * i + 1)!) * HPow.hPow (α := ℕ) 2 n) 2 * (2 * n)!
have rw₁ : HPow.hPow (α := ℕ) (β := ℕ) (∏ i ∈ range (2 * n), (2 * i + 1)!) 2 * HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 n) 2 *
    (2 * n)! =
  HPow.hPow (α := ℕ) (β := ℕ) (∏ i ∈ range (2 * n), (2 * i + 1)!) 2 * HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 n) 2 *
    (2 * n)!
Tactic: rw [pow_mul', mul_pow]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
⊢ ¬p ∣ r ↔ Eq (α := ℕ) (((p * i + r).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have refine : ∀ (h : Eq (α := ℕ) (((p * i + r).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)), ¬p ∣ r
Tactic: refine ⟨factorization_eq_zero_of_remainder i, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (hypothesis)
Goal:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : Eq (α := ℕ) (((p * i + r).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ ¬p ∣ r
have h₁ : ¬Prime p ∨ ¬p ∣ p * i + r ∨ p * i + r = 0
Tactic: rw [factorization_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : ¬Prime p ∨ ¬p ∣ p * i + r ∨ p * i + r = 0
⊢ ¬p ∣ r
have contrapose! : ∀ (h : p ∣ r), Prime p ∧ p ∣ p * i + r ∧ p * i + r ≠ 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ Prime p ∧ p ∣ p * i + r ∧ p * i + r ≠ 0
have refine_1 : p ∣ p * i + r
Tactic: refine ⟨pp, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
refine_1 : p ∣ p * i + r
⊢ Prime p ∧ p ∣ p * i + r ∧ p * i + r ≠ 0
have refine_2 : p * i + r ≠ 0
Tactic: refine ⟨pp, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p * i + r ≠ 0
have refine_2 : ∀ (hr0 : p * i + r = 0), r = 0
Tactic: contrapose hr0
Cleared hypotheses: hr0
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n : ℕ
⊢ n.factorization = 0 ↔ n = 0 ∨ n = 1
have rw : Eq (α := ℕ →₀ ℕ) ((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) (↑n.primeFactorsList : Multiset ℕ) : ℕ →₀ ℕ)
    (0 : ℕ →₀ ℕ) ↔
  n = 0 ∨ n = 1
Tactic: rw [factorization_eq_primeFactorsList_multiset n]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
α : Type u_1
p : ℕ
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ Eq (α := ℕ) (((S.prod g).factorization : (a : ℕ) → ℕ) p : ℕ) (∑ x ∈ S, ((g x).factorization : (a : ℕ) → ℕ) p : ℕ)
have rw : Eq (α := ℕ) ((∑ x ∈ S, (g x).factorization : (a : ℕ) → ℕ) p : ℕ) (∑ x ∈ S, ((g x).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [factorization_prod hS, finsetSum_apply]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
α : Type u_1
p : ℕ
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
rw :
  Eq (α := ℕ) ((∑ x ∈ S, (g x).factorization : (a : ℕ) → ℕ) p : ℕ) (∑ x ∈ S, ((g x).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ Eq (α := ℕ) (((S.prod g).factorization : (a : ℕ) → ℕ) p : ℕ) (∑ x ∈ S, ((g x).factorization : (a : ℕ) → ℕ) p : ℕ)
have rw₁ : Eq (α := ℕ) (∑ i ∈ S, ((g i).factorization : (a : ℕ) → ℕ) p) (∑ x ∈ S, ((g x).factorization : (a : ℕ) → ℕ) p)
Tactic: rw [factorization_prod hS, finsetSum_apply]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p k : ℕ
hn : n ≠ 0
h : n.factorization = single p k
⊢ n = p ^ k
have rw : (Finsupp.prod (single p k) fun (x1 x2 : ℕ) ↦ x1 ^ x2) = p ^ k
Tactic: rw [← Nat.prod_factorization_pow_eq_self hn, h]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
⊢ 0 < HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have if : ∀ (pp : Prime p), 0 < HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: if pp : p.Prime then simp [Nat.pow_pos pp.pos] else simp [pp]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
if : ∀ (pp : Prime p), 0 < HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ 0 < HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have if₁ : ∀ (pp : ¬Prime p), 0 < HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: if pp : p.Prime then simp [Nat.pow_pos pp.pos] else simp [pp]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
hn : n ≠ 0
⊢ 0 < n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have if : ∀ (pp : Prime p), 0 < n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: if pp : p.Prime then
    exact Nat.div_pos (ordProj_le p hn) (ordProj_pos n p)
  else
    simpa [Nat.factorization_eq_zero_of_not_prime n pp] using hn.bot_lt
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
n p : ℕ
hn : n ≠ 0
if : ∀ (pp : Prime p), 0 < n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ 0 < n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have if₁ : ∀ (pp : ¬Prime p), 0 < n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: if pp : p.Prime then
    exact Nat.div_pos (ordProj_le p hn) (ordProj_pos n p)
  else
    simpa [Nat.factorization_eq_zero_of_not_prime n pp] using hn.bot_lt
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Basic (goal)
Goal:
a b p : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ a * b / HPow.hPow (β := ℕ) p (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) =
    a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
have simp : a * b /
    (HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
      HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)) =
  a / HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ) *
    (b / HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ))
Tactic: simp only [ordProj_mul p ha hb]