awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : Semiring A
k : ℕ
ih : ∀ {m : ℕ} (hn_fac : IsUnit.{u_1} (M := A) (↑(m + k)! : A)), IsUnit.{u_1} (M := A) (↑m ! : A)
m : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(m + 1 + k)! : A)
this : IsUnit.{u_1} (M := A) (↑(m + 1)! : A)
⊢ IsUnit.{u_1} (M := A) (↑(m + 1) : A) ∧ IsUnit.{u_1} (M := A) (↑m ! : A)

Tactic:
rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_commute _ _ |>.isUnit_mul_iff] at this

Premises used: Nat.factorial_succ, Nat.cast_mul, Commute.isUnit_mul_iff
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : Semiring A
k : ℕ
ih : ∀ {m : ℕ} (hn_fac : IsUnit.{u_1} (M := A) (↑(m + k)! : A)), IsUnit.{u_1} (M := A) (↑m ! : A)
m : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(m + 1 + k)! : A)
this : IsUnit.{u_1} (M := A) (↑(m + 1) : A) ∧ IsUnit.{u_1} (M := A) (↑m ! : A)
⊢ IsUnit.{u_1} (M := A) (↑m ! : A)

Tactic:
this.2

Premises used: And.right
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : Semiring A
k : ℕ
ih : ∀ {m : ℕ} (hn_fac : IsUnit.{u_1} (M := A) (↑(m + k)! : A)), IsUnit.{u_1} (M := A) (↑m ! : A)
m : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(m + 1 + k)! : A)
this : IsUnit.{u_1} (M := A) (↑(m + 1) : A) ∧ IsUnit.{u_1} (M := A) (↑m ! : A)
⊢ IsUnit.{u_1} (M := A) (↑m ! : A)

Tactic:
exact this.2

Premises used: And.right
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : Semiring A
m k : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(m + k)! : A)
zero : ∀ {m : ℕ} (hn_fac : IsUnit.{u_1} (M := A) (↑(m + 0)! : A)), IsUnit.{u_1} (M := A) (↑m ! : A)
succ :
  ∀ (k : ℕ) (ih : ∀ {m : ℕ} (hn_fac : IsUnit.{u_1} (M := A) (↑(m + k)! : A)), IsUnit.{u_1} (M := A) (↑m ! : A)) {m : ℕ}
    (hn_fac : IsUnit.{u_1} (M := A) (↑(m + (k + 1))! : A)), IsUnit.{u_1} (M := A) (↑m ! : A)
⊢ IsUnit.{u_1} (M := A) (↑m ! : A)

Tactic:
induction k generalizing m with
  | zero => simpa using hn_fac
  | succ k ih =>
    rw [← add_assoc, add_right_comm] at hn_fac
    have := ih hn_fac
    rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_commute _ _ |>.isUnit_mul_iff] at this
    exact this.2

Premises used: Nat.factorial_succ, add_assoc, add_right_comm, Nat.cast_mul, Commute.isUnit_mul_iff, Nat.zero, Nat.succ
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : Semiring A
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
m : ℕ
hmn : m < n
⊢ IsUnit.{u_1} (M := A) (↑m ! : A)

Tactic:
hn_fac.natCast_factorial_of_le <| le_sub_one_of_lt hmn

Premises used: IsUnit.natCast_factorial_of_le, Nat.le_sub_one_of_lt
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : Semiring A
K : Type u_2
inst_1 : Semifield K
inst_2 : CharZero K
inst_3 : Algebra K A
n : ℕ
this : IsUnit.{u_2} (M := K) (↑n ! : K)
⊢ IsUnit.{u_1} (M := A) (↑n ! : A)

Tactic:
simpa using this.map (algebraMap K A)

Premises used: Algebra.algebraMap, IsUnit.map
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : Semiring A
K : Type u_2
inst_1 : Semifield K
inst_2 : CharZero K
inst_3 : Algebra K A
n : ℕ
suffices : IsUnit.{u_2} (M := K) (↑n ! : K)
⊢ IsUnit.{u_1} (M := A) (↑n ! : A)

Tactic:
suffices IsUnit (n ! : K) by
    simpa using this.map (algebraMap K A)
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : Semiring A
K : Type u_2
inst_1 : Semifield K
inst_2 : CharZero K
inst_3 : Algebra K A
n : ℕ
⊢ IsUnit.{u_2} (M := K) (↑n ! : K)

Tactic:
simp [isUnit_iff_ne_zero, n.factorial_ne_zero]

Premises used: isUnit_iff_ne_zero, Nat.factorial_ne_zero
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : Ring A
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP A p
n : ℕ
⊢ Nat.Prime p

Tactic:
have hp : p.Prime := Fact.out
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : Ring A
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP A p
hp : Nat.Prime p
⊢ IsUnit.{u_1} (M := A) (↑0! : A) ↔ 0 < p

Tactic:
simp [hp.pos]

Premises used: Nat.Prime.pos
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : Ring A
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP A p
hp : Nat.Prime p
n : ℕ
ih : IsUnit.{u_1} (M := A) (↑n ! : A) ↔ n < p
succ : ¬p ∣ n + 1 ∧ n + 1 ≤ p ↔ n + 1 < p
⊢ IsUnit.{u_1} (M := A) (↑(n + 1)! : A) ↔ n + 1 < p

Tactic:
rw [factorial_succ, cast_mul, Nat.cast_commute _ _ |>.isUnit_mul_iff, ih.symm.symm,
      ← Nat.add_one_le_iff, CharP.isUnit_natCast_iff hp]

Premises used: Nat.factorial_succ, Nat.cast_mul, Nat.add_one_le_iff, Commute.isUnit_mul_iff, CharP.isUnit_natCast_iff, Iff.symm
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : Ring A
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP A p
hp : Nat.Prime p
n : ℕ
ih : IsUnit.{u_1} (M := A) (↑n ! : A) ↔ n < p
⊢ ¬p ∣ n + 1 ∧ n + 1 ≤ p ↔ n + 1 < p

Tactic:
⟨fun ⟨h1, h2⟩ ↦ lt_of_le_of_ne h2 (mt (· ▸ dvd_rfl) h1),
      fun h ↦ ⟨not_dvd_of_pos_of_lt (Nat.succ_pos _) h, h.le⟩⟩

Premises used: _private.0.IsUnit.natCast_factorial_iff_of_charP.match_1, mt, LT.lt.le, Nat.not_dvd_of_pos_of_lt, HAdd.hAdd, Nat.succ_pos, And.intro, LT.lt, Iff.intro, OfNat.ofNat, lt_of_le_of_ne
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : Ring A
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP A p
hp : Nat.Prime p
n : ℕ
ih : IsUnit.{u_1} (M := A) (↑n ! : A) ↔ n < p
⊢ ¬p ∣ n + 1 ∧ n + 1 ≤ p ↔ n + 1 < p

Tactic:
exact ⟨fun ⟨h1, h2⟩ ↦ lt_of_le_of_ne h2 (mt (· ▸ dvd_rfl) h1),
      fun h ↦ ⟨not_dvd_of_pos_of_lt (Nat.succ_pos _) h, h.le⟩⟩
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : Ring A
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP A p
n : ℕ
hp : Nat.Prime p
zero : IsUnit.{u_1} (M := A) (↑0! : A) ↔ 0 < p
succ : ∀ (n : ℕ) (ih : IsUnit.{u_1} (M := A) (↑n ! : A) ↔ n < p), IsUnit.{u_1} (M := A) (↑(n + 1)! : A) ↔ n + 1 < p
⊢ IsUnit.{u_1} (M := A) (↑n ! : A) ↔ n < p

Tactic:
induction n with
  | zero => simp [hp.pos]
  | succ n ih =>
    -- TODO: why is `.symm.symm` needed here!?
    rw [factorial_succ, cast_mul, Nat.cast_commute _ _ |>.isUnit_mul_iff, ih.symm.symm,
      ← Nat.add_one_le_iff, CharP.isUnit_natCast_iff hp]
    exact ⟨fun ⟨h1, h2⟩ ↦ lt_of_le_of_ne h2 (mt (· ▸ dvd_rfl) h1),
      fun h ↦ ⟨not_dvd_of_pos_of_lt (Nat.succ_pos _) h, h.le⟩⟩

Premises used: Nat.factorial_succ, Nat.Prime.pos, Nat.cast_mul, Nat.add_one_le_iff, Commute.isUnit_mul_iff, Nat.zero, CharP.isUnit_natCast_iff, Nat.succ
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : CommRing A
n p : ℕ
hp : IsNilpotent.{u_1} (R := A) (↑p : A)
h : p.Coprime n
obtain : ∀ (m : ℕ) (hm : HPow.hPow (α := A) (↑p : A) m = 0), IsUnit.{u_1} (M := A) (↑n : A)
⊢ IsUnit.{u_1} (M := A) (↑n : A)

Tactic:
obtain ⟨m, hm⟩ := hp
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : HPow.hPow (α := A) (↑p : A) m = 0
this : ∃ (a : A) (b : A), HPow.hPow (α := A) (↑p : A) m * a + (↑n : A) * b = 1
obtain : ∀ (a b : A) (h : HPow.hPow (α := A) (↑p : A) m * a + (↑n : A) * b = 1), IsUnit.{u_1} (M := A) (↑n : A)
⊢ IsUnit.{u_1} (M := A) (↑n : A)

Tactic:
obtain ⟨a, b, h⟩ := this
-- Module: Mathlib.Data.Nat.Factorial.NatCast
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)

Tactic:
.of_mul_eq_one b ?_

Premises used: IsUnit.of_mul_eq_one
-- Module: Mathlib.Data.Nat.Factorial.NatCast
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
refine : (↑n : A) * b = 1
⊢ IsUnit.{u_1} (M := A) (↑n : A)

Tactic:
refine .of_mul_eq_one b ?_
-- Module: Mathlib.Data.Nat.Factorial.NatCast
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
⊢ (↑n : A) * b = 1

Tactic:
simpa [hm] using h
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : HPow.hPow (α := A) (↑p : A) m = 0
suffices : ∃ (a : A) (b : A), HPow.hPow (α := A) (↑p : A) m * a + (↑n : A) * b = 1
⊢ IsUnit.{u_1} (M := A) (↑n : A)

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
-- Module: Mathlib.Data.Nat.Factorial.NatCast
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

Tactic:
⟨(p ^ m).gcdA n, (p ^ m).gcdB n, ?_⟩

Premises used: Int.cast, Nat.gcdB, HPow.hPow, Exists.intro, Nat.gcdA
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : HPow.hPow (α := A) (↑p : A) m = 0
refine :
  HPow.hPow (α := A) (↑p : A) m * (↑((p ^ m).gcdA n) : A) + HMul.hMul (α := A) (↑n : A) (↑((p ^ m).gcdB n) : A) = 1
⊢ ∃ (a : A) (b : A), HPow.hPow (α := A) (↑p : A) m * a + (↑n : A) * b = 1

Tactic:
refine ⟨(p ^ m).gcdA n, (p ^ m).gcdB n, ?_⟩
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : HPow.hPow (α := A) (↑p : A) m = 0
norm_cast : Eq.{u_1 + 1} (α := A) (↑((↑(p ^ m) : ℤ) * (p ^ m).gcdA n + (↑n : ℤ) * (p ^ m).gcdB n) : A) 1
⊢ HPow.hPow (α := A) (↑p : A) m * (↑((p ^ m).gcdA n) : A) + HMul.hMul (α := A) (↑n : A) (↑((p ^ m).gcdB n) : A) = 1

Tactic:
norm_cast
-- Module: Mathlib.Data.Nat.Factorial.NatCast
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)
rw₃ 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)
⊢ Eq.{u_1 + 1} (α := A) (↑((↑(p ^ m) : ℤ) * (p ^ m).gcdA n + (↑n : ℤ) * (p ^ m).gcdB n) : A) 1

Tactic:
rw [← Nat.cast_one, ← Int.cast_natCast 1, ← (h.pow_left m).gcd_eq_one, Nat.gcd_eq_gcd_ab]

Premises used: Int.cast_natCast, Nat.Coprime.pow_left, Nat.Coprime.gcd_eq_one, OfNat.ofNat, Nat.gcd_eq_gcd_ab, Nat.cast_one
-- Module: Mathlib.Data.Nat.Factorial.NatCast
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 : 0 < p
⊢ IsUnit.{u_1} (M := A) (↑0! : A)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorial.NatCast
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
succ : IsUnit.{u_1} (M := A) (↑(n + 1) : A) ∧ IsUnit.{u_1} (M := A) (↑n ! : A)
⊢ IsUnit.{u_1} (M := A) (↑(n + 1)! : A)

Tactic:
simp only [factorial_succ, cast_mul, IsUnit.mul_iff]

Premises used: IsUnit.mul_iff, Nat.factorial_succ, Nat.cast_mul
-- Module: Mathlib.Data.Nat.Factorial.NatCast
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
⊢ n < p

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorial.NatCast
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
succ : p.Coprime (n + 1)
⊢ IsUnit.{u_1} (M := A) (↑(n + 1) : A) ∧ IsUnit.{u_1} (M := A) (↑n ! : A)

Tactic:
refine ⟨.natCast_of_isNilpotent_of_coprime hp ?_, ih (by lia)⟩
-- Module: Mathlib.Data.Nat.Factorial.NatCast
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
succ : ¬p ∣ n + 1
⊢ p.Coprime (n + 1)

Tactic:
rw [Nat.Prime.coprime_iff_not_dvd Fact.out]

Premises used: Nat.Prime.coprime_iff_not_dvd, Fact.out
-- Module: Mathlib.Data.Nat.Factorial.NatCast
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
⊢ 0 < n + 1

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorial.NatCast
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 ∣ n + 1

Tactic:
exact Nat.not_dvd_of_pos_of_lt (by lia) h

Premises used: Nat.not_dvd_of_pos_of_lt
-- Module: Mathlib.Data.Nat.Factorial.NatCast
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)
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)
⊢ IsUnit.{u_1} (M := A) (↑n ! : 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

Premises used: IsUnit.mul_iff, Nat.factorial_succ, Nat.cast_mul, Nat.not_dvd_of_pos_of_lt, Nat.zero, Nat.Prime.coprime_iff_not_dvd, Nat.succ, Fact.out
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : CommSemiring A
m : ℕ
k : ℕ × ℕ
hm : IsUnit.{u_1} (M := A) (↑m ! : A)
hk : k ∈ @Finset.antidiagonal _ instAddMonoid _ m
⊢ k.1 + k.2 = m

Tactic:
rw [Finset.mem_antidiagonal] at hk

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : CommSemiring A
m : ℕ
k : ℕ × ℕ
hm : IsUnit.{u_1} (M := A) (↑m ! : A)
hk : k.1 + k.2 = m
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)⁻¹ʳ
⊢ (↑(m.choose k.1) : A) = HMul.hMul (α := A) (↑m ! : A) (↑k.1! : A)⁻¹ʳ * (↑k.2! : A)⁻¹ʳ

Tactic:
subst hk
-- Module: Mathlib.Data.Nat.Factorial.NatCast
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)
h₁ : IsUnit.{u_1} (M := A) (↑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:
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]

Premises used: add_comm, Nat.cast_mul, Nat.add_choose_mul_factorial_mul_factorial, Ring.eq_mul_inverse_iff_mul_eq
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : CommSemiring A
k : ℕ × ℕ
hm : IsUnit.{u_1} (M := A) (↑(k.1 + k.2)! : A)
h : k.1 ≤ k.1 + k.2
⊢ IsUnit.{u_1} (M := A) (↑k.1! : A)

Tactic:
apply hm.natCast_factorial_of_le

Premises used: IsUnit.natCast_factorial_of_le
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : CommSemiring A
k : ℕ × ℕ
hm : IsUnit.{u_1} (M := A) (↑(k.1 + k.2)! : A)
h : k.2 ≤ k.1 + k.2
⊢ IsUnit.{u_1} (M := A) (↑k.2! : A)

Tactic:
apply hm.natCast_factorial_of_le

Premises used: IsUnit.natCast_factorial_of_le
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : CommSemiring A
k : ℕ × ℕ
hm : IsUnit.{u_1} (M := A) (↑(k.1 + k.2)! : A)
⊢ k.1 ≤ k.1 + k.2

Tactic:
Nat.le_add_right k.1 k.2

Premises used: Nat.le_add_right, Prod.fst, Prod.snd
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : CommSemiring A
k : ℕ × ℕ
hm : IsUnit.{u_1} (M := A) (↑(k.1 + k.2)! : A)
⊢ k.2 ≤ k.1 + k.2

Tactic:
Nat.le_add_left k.2 k.1

Premises used: Nat.le_add_left, Prod.fst, Prod.snd
-- Module: Mathlib.Data.Nat.Factorial.NatCast
Goal:
A : Type u_1
inst : CommSemiring A
k : ℕ × ℕ
hm : IsUnit.{u_1} (M := A) (↑(k.1 + k.2)! : A)
⊢ k.1 ≤ k.1 + k.2

Tactic:
exacts [Nat.le_add_right k.1 k.2, Nat.le_add_left k.2 k.1]

Premises used: Nat.le_add_right, Nat.le_add_left, Prod.fst, Prod.snd
-- Module: Mathlib.Data.Nat.Factorial.SuperFactorial
Goal:
⊢ sf 0 = 1

Tactic:
rfl

Premises used: Nat.superFactorial, rfl
-- Module: Mathlib.Data.Nat.Factorial.SuperFactorial
Goal:
n : ℕ
⊢ sf n.succ = (n + 1)! * sf n

Tactic:
rfl

Premises used: Nat.superFactorial, rfl
-- Module: Mathlib.Data.Nat.Factorial.SuperFactorial
Goal:
⊢ sf 1 = 1

Tactic:
rfl

Premises used: Nat.superFactorial, rfl
-- Module: Mathlib.Data.Nat.Factorial.SuperFactorial
Goal:
⊢ sf 2 = 2

Tactic:
rfl

Premises used: Nat.superFactorial, rfl
-- Module: Mathlib.Data.Nat.Factorial.SuperFactorial
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
rw₇ rw₈ : (n + 1) * n ! * sf n = n.succ * n ! * sf n
⊢ ∏ x ∈ Icc 1 (n + 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]

Premises used: Nat.superFactorial, Nat.factorial_succ, Finset.Ico_add_one_right_eq_Icc, Nat.factorial, Finset.prod_Ico_succ_top, mul_comm, OfNat.ofNat, le_add_self
-- Module: Mathlib.Data.Nat.Factorial.SuperFactorial
Goal:
n : ℕ
⊢ ∏ x ∈ range n, (x + 1)! = sf n

Tactic:
prod_Icc_factorial n ▸ range_eq_Ico n ▸ Finset.prod_Ico_add' _ _ _ _

Premises used: Eq.rec, Finset.prod_Ico_add', Nat.prod_Icc_factorial, Finset.range_eq_Ico, Eq.symm
-- Module: Mathlib.Data.Nat.Factorial.SuperFactorial
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
rw₃ rw₄ : (n + 1)! * sf n = n.succ ! * sf n
⊢ ∏ x ∈ range (n + 1 + 1), x ! = sf n + 1

Tactic:
rw [prod_range_succ, prod_range_succ_factorial n, mul_comm, superFactorial]

Premises used: Nat.superFactorial, mul_comm, Finset.prod_range_succ
-- Module: Mathlib.Data.Nat.Factorial.SuperFactorial
Goal:
n : ℕ
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 !)
⊢ sf 2 * (n + 1) =
    HPow.hPow (α := ℕ) (β := ℕ) (∏ i ∈ range (n + 1), (2 * i + 1)!) 2 * HPow.hPow (α := ℕ) 2 (n + 1) * (n + 1)!

Tactic:
simp only [prod_range_succ, mul_pow, mul_add, mul_one, superFactorial_succ,
      superFactorial_two_mul n, factorial_succ]

Premises used: Nat.factorial_succ, Finset.prod_range_succ, Nat.superFactorial_succ, mul_add, mul_one, mul_pow
-- Module: Mathlib.Data.Nat.Factorial.SuperFactorial
Goal:
n : ℕ
⊢ (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:
ring
-- Module: Mathlib.Data.Nat.Factorial.SuperFactorial
Goal:
n : ℕ
rw : sf 4 * n = sf 2 * (2 * n)
rw₁ : sf 4 * n = sf HMul.hMul (α := ℕ) 2 2 * n
rw₂ rw₃ : sf 4 * n = sf HAdd.hAdd (α := ℕ) 2 2 * n
⊢ sf 4 * n = HPow.hPow (α := ℕ) (β := ℕ) (∏ i ∈ range (2 * n), (2 * i + 1)!) 2 * HPow.hPow (α := ℕ) 2 (2 * n) * (2 * n)!

Tactic:
rw [← superFactorial_two_mul, ← mul_assoc, Nat.mul_two]

Premises used: mul_assoc, Nat.superFactorial_two_mul, Nat.mul_two
-- Module: Mathlib.Data.Nat.Factorial.SuperFactorial
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)!
rw₁ 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)!
⊢ 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)!

Tactic:
rw [pow_mul', mul_pow]

Premises used: mul_pow, pow_mul'
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
h : n < p
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
Finsupp.notMem_support_iff.mp (mt le_of_mem_primeFactors (not_le_of_gt h))

Premises used: Finsupp.notMem_support_iff, mt, Iff.mp, not_le_of_gt, Nat.le_of_mem_primeFactors
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
hn : Ne (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ p ∣ n

Tactic:
dvd_of_mem_primeFactorsList <| mem_primeFactors_iff_mem_primeFactorsList.1 <| mem_support_iff.2 hn

Premises used: Iff.mpr, Finsupp.mem_support_iff, Nat.mem_primeFactors_iff_mem_primeFactorsList, Iff.mp, Nat.dvd_of_mem_primeFactorsList
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
⊢ ¬p ∣ r ↔ Eq (α := ℕ) (((p * i + r).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
⟨factorization_eq_zero_of_remainder i, fun h => ?_⟩

Premises used: Iff.intro, Nat.factorization_eq_zero_of_remainder
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
refine : ∀ (h : Eq (α := ℕ) (((p * i + r).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)), ¬p ∣ r
⊢ ¬p ∣ r ↔ Eq (α := ℕ) (((p * i + r).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
refine ⟨factorization_eq_zero_of_remainder i, fun h => ?_⟩
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : Eq (α := ℕ) (((p * i + r).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ ¬Prime p ∨ ¬p ∣ p * i + r ∨ p * i + r = 0

Tactic:
rw [factorization_eq_zero_iff] at h

Premises used: Nat.factorization_eq_zero_iff
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : ¬Prime p ∨ ¬p ∣ p * i + r ∨ p * i + r = 0
contrapose! : ∀ (h : p ∣ r), Prime p ∧ p ∣ p * i + r ∧ p * i + r ≠ 0
⊢ ¬p ∣ r

Tactic:
contrapose! h
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ Prime p ∧ p ∣ p * i + r ∧ p * i + r ≠ 0

Tactic:
⟨pp, ?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
refine_1 : p ∣ p * i + r
refine_2 : p * i + r ≠ 0
⊢ Prime p ∧ p ∣ p * i + r ∧ p * i + r ≠ 0

Tactic:
refine ⟨pp, ?_, ?_⟩
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h refine_1 refine_1₁ refine_1₂ refine_1₃ : p ∣ r
⊢ p ∣ p * i + r

Tactic:
rwa [← Nat.dvd_add_iff_right (dvd_mul_right p i)]

Premises used: dvd_mul_right, Nat.dvd_add_iff_right
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
refine_2 : ∀ (hr0 : p * i + r = 0), r = 0
⊢ p * i + r ≠ 0

Tactic:
contrapose hr0
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p r i : ℕ
pp : Prime p
h : p ∣ r
hr0 : p * i + r = 0
⊢ r = 0

Tactic:
(add_eq_zero.1 hr0).2

Premises used: And.right, Iff.mp, add_eq_zero
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p r i : ℕ
pp : Prime p
h : p ∣ r
hr0 : p * i + r = 0
⊢ r = 0

Tactic:
exact (add_eq_zero.1 hr0).2

Premises used: And.right, Iff.mp, add_eq_zero