awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (a • g) :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : (a • g).IsWeierstrassFactorization ((a • g).weierstrassDistinguished hg) ((a • g).weierstrassUnit hg)
⊢ (a • g).weierstrassUnit hg = a • g.weierstrassUnit ⋯
have ha : Ne (α := IsLocalRing.ResidueField A)
  ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) a : IsLocalRing.ResidueField A)
  (0 : IsLocalRing.ResidueField A)
Tactic: have ha : IsLocalRing.residue A a ≠ 0 := fun h ↦ hg (by simp [Algebra.smul_def, h])
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
R : Type u_1
inst : Ring R
u : Rˣ
⊢ (constantCoeff : (a : R⟦X⟧) → R) (invUnitsSub u) = 1 /ₚ u
have rw : (coeff 0 : (a : R⟦X⟧) → R) (invUnitsSub u) = 1 /ₚ u
Tactic: rw [← coeff_zero_eq_constantCoeff_apply, coeff_invUnitsSub, zero_add, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
R : Type u_1
inst : Ring R
u : Rˣ
rw : (coeff 0 : (a : R⟦X⟧) → R) (invUnitsSub u) = 1 /ₚ u
⊢ (constantCoeff : (a : R⟦X⟧) → R) (invUnitsSub u) = 1 /ₚ u
have rw₁ : 1 /ₚ u ^ HAdd.hAdd (α := ℕ) 0 1 = 1 /ₚ u
Tactic: rw [← coeff_zero_eq_constantCoeff_apply, coeff_invUnitsSub, zero_add, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
R : Type u_1
inst : Ring R
u : Rˣ
rw : (coeff 0 : (a : R⟦X⟧) → R) (invUnitsSub u) = 1 /ₚ u
rw₁ : 1 /ₚ u ^ HAdd.hAdd (α := ℕ) 0 1 = 1 /ₚ u
rw₂ : 1 /ₚ HPow.hPow (β := ℕ) u 1 = 1 /ₚ u
⊢ (constantCoeff : (a : R⟦X⟧) → R) (invUnitsSub u) = 1 /ₚ u
have rw₃ : 1 /ₚ u = 1 /ₚ u
Tactic: rw [← coeff_zero_eq_constantCoeff_apply, coeff_invUnitsSub, zero_add, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
R : Type u_1
inst : Ring R
u : Rˣ
⊢ invUnitsSub u * X = HMul.hMul (β := R⟦X⟧) (invUnitsSub u) ((C : (a : R) → R⟦X⟧) (↑u : R) : R⟦X⟧) - 1
have h : Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) (invUnitsSub u * X) : R)
  ((coeff 0 : (a : R⟦X⟧) → R) (HMul.hMul (β := R⟦X⟧) (invUnitsSub u) ((C : (a : R) → R⟦X⟧) (↑u : R) : R⟦X⟧) - 1) : R)
Tactic: ext (_ | n)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
R : Type u_1
inst : Ring R
u : Rˣ
h :
  Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) (invUnitsSub u * X) : R)
    ((coeff 0 : (a : R⟦X⟧) → R) (HMul.hMul (β := R⟦X⟧) (invUnitsSub u) ((C : (a : R) → R⟦X⟧) (↑u : R) : R⟦X⟧) - 1) : R)
⊢ invUnitsSub u * X = HMul.hMul (β := R⟦X⟧) (invUnitsSub u) ((C : (a : R) → R⟦X⟧) (↑u : R) : R⟦X⟧) - 1
have h₁ : ∀ (n : ℕ),
  Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (invUnitsSub u * X) : R)
    ((coeff (n + 1) : (a : R⟦X⟧) → R)
        (HMul.hMul (β := R⟦X⟧) (invUnitsSub u) ((C : (a : R) → R⟦X⟧) (↑u : R) : R⟦X⟧) - 1) :
      R)
Tactic: ext (_ | n)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
u : Rˣ
⊢ Eq.{u_2 + 1} (α := S⟦X⟧) ((map f : (a : R⟦X⟧) → S⟦X⟧) (invUnitsSub u) : S⟦X⟧)
    (invUnitsSub (((Units.map (↑f : R →* S) : MonoidHom.{u_1, u_2} Rˣ Sˣ) : (a : Rˣ) → Sˣ) u) : S⟦X⟧)
have h : ∀ (n : ℕ),
  Eq.{u_2 + 1} (α := S) ((coeff n : (a : S⟦X⟧) → S) ((map f : (a : R⟦X⟧) → S⟦X⟧) (invUnitsSub u) : S⟦X⟧) : S)
    ((coeff n : (a : S⟦X⟧) → S)
        (invUnitsSub (((Units.map (↑f : R →* S) : MonoidHom.{u_1, u_2} Rˣ Sˣ) : (a : Rˣ) → Sˣ) u)) :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
u : Rˣ
n : ℕ
⊢ Eq.{u_2 + 1} (α := S) ((coeff n : (a : S⟦X⟧) → S) ((map f : (a : R⟦X⟧) → S⟦X⟧) (invUnitsSub u) : S⟦X⟧) : S)
    ((coeff n : (a : S⟦X⟧) → S)
        (invUnitsSub (((Units.map (↑f : R →* S) : MonoidHom.{u_1, u_2} Rˣ Sˣ) : (a : Rˣ) → Sˣ) u)) :
      S)
have h : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (↑(u ^ (n + 1))⁻¹ : R) : S)
  ((↑(((Units.map (↑f : R →* S) : MonoidHom.{u_1, u_2} Rˣ Sˣ) : (a : Rˣ) → Sˣ) (u ^ (n + 1)))⁻¹ : S) : S)
Tactic: simp only [← map_pow, coeff_map, coeff_invUnitsSub, one_divp]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
⊢ mk 1 * HSub.hSub (α := S⟦X⟧) 1 X = 1
have rw : ∀ (n : ℕ),
  Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) (HSub.hSub (α := S⟦X⟧) 1 X * mk 1) : S) ((coeff n : (a : S⟦X⟧) → S) 1 : S)
Tactic: rw [mul_comm, PowerSeries.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
n : ℕ
⊢ Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) (HSub.hSub (α := S⟦X⟧) 1 X * mk 1) : S) ((coeff n : (a : S⟦X⟧) → S) 1 : S)
have zero : Eq (α := S) ((coeff 0 : (a : S⟦X⟧) → S) (HSub.hSub (α := S⟦X⟧) 1 X * mk 1) : S) ((coeff 0 : (a : S⟦X⟧) → S) 1 : S)
Tactic: cases n with
  | zero => simp
  | succ n => simp [sub_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
n : ℕ
zero :
  Eq (α := S) ((coeff 0 : (a : S⟦X⟧) → S) (HSub.hSub (α := S⟦X⟧) 1 X * mk 1) : S) ((coeff 0 : (a : S⟦X⟧) → S) 1 : S)
⊢ Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) (HSub.hSub (α := S⟦X⟧) 1 X * mk 1) : S) ((coeff n : (a : S⟦X⟧) → S) 1 : S)
have succ : ∀ (n : ℕ),
  Eq (α := S) ((coeff (n + 1) : (a : S⟦X⟧) → S) (HSub.hSub (α := S⟦X⟧) 1 X * mk 1) : S)
    ((coeff (n + 1) : (a : S⟦X⟧) → S) 1 : S)
Tactic: cases n with
  | zero => simp
  | succ n => simp [sub_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
⊢ HPow.hPow (α := S⟦X⟧) (mk 1) (HAdd.hAdd (α := ℕ) 0 1) = mk fun (n : ℕ) ↦ (↑((0 + n).choose 0) : S)
have zero : ∀ (n : ℕ),
  Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) (HPow.hPow (α := S⟦X⟧) (mk 1) (HAdd.hAdd (α := ℕ) 0 1)) : S)
    ((coeff n : (a : S⟦X⟧) → S) (mk fun (n : ℕ) ↦ (↑((0 + n).choose 0) : S)) : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
hd : HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)
⊢ HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1 + 1) = mk fun (n : ℕ) ↦ (↑((d + 1 + n).choose (d + 1)) : S)
have succ : ∀ (n : ℕ),
  Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) (HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1 + 1)) : S)
    ((coeff n : (a : S⟦X⟧) → S) (mk fun (n : ℕ) ↦ (↑((d + 1 + n).choose (d + 1)) : S)) : S)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
hd : HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)
n : ℕ
⊢ Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) (HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1 + 1)) : S)
    ((coeff n : (a : S⟦X⟧) → S) (mk fun (n : ℕ) ↦ (↑((d + 1 + n).choose (d + 1)) : S)) : S)
have succ : Eq.{u_1 + 1} (α := S)
  (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := S) (β := S) ((coeff p.1 : (a : S⟦X⟧) → S) (mk 1) : S)
        ((coeff p.2 : (a : S⟦X⟧) → S) (mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)) : S) :
    S)
  ((coeff n : (a : S⟦X⟧) → S) (mk fun (n : ℕ) ↦ (↑((d + 1 + n).choose (d + 1)) : S)) : S)
Tactic: rw [pow_add, hd, pow_one, mul_comm, coeff_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
hd : HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)
n : ℕ
⊢ Eq.{u_1 + 1} (α := S)
    (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HMul.hMul (α := S) (β := S) ((coeff p.1 : (a : S⟦X⟧) → S) (mk 1) : S)
          ((coeff p.2 : (a : S⟦X⟧) → S) (mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)) : S) :
      S)
    ((coeff n : (a : S⟦X⟧) → S) (mk fun (n : ℕ) ↦ (↑((d + 1 + n).choose (d + 1)) : S)) : S)
have succ : Eq.{u_1 + 1} (α := S) (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, (↑((d + x.2).choose d) : S))
  (↑((d + 1 + n).choose (d + 1)) : S)
Tactic: simp_rw [coeff_mk, Pi.one_apply, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
hd : HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)
n : ℕ
⊢ Eq.{u_1 + 1} (α := S) (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, (↑((d + x.2).choose d) : S))
    (↑((d + 1 + n).choose (d + 1)) : S)
have succ : Eq.{u_1 + 1} (α := S) (↑(∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, (d + x.2).choose d) : S)
  (↑((d + 1 + n).choose (d + 1)) : S)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
hd : HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)
n : ℕ
⊢ Eq.{u_1 + 1} (α := S) (↑(∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, (d + x.2).choose d) : S)
    (↑((d + 1 + n).choose (d + 1)) : S)
have succ : Eq.{u_1 + 1} (α := S) (↑((d + n + 1).choose (d + 1)) : S) (↑((d + 1 + n).choose (d + 1)) : S)
Tactic: rw [Finset.sum_antidiagonal_choose_add, add_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
hd : HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)
n : ℕ
succ : Eq.{u_1 + 1} (α := S) (↑((d + n + 1).choose (d + 1)) : S) (↑((d + 1 + n).choose (d + 1)) : S)
⊢ Eq.{u_1 + 1} (α := S) (↑(∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, (d + x.2).choose d) : S)
    (↑((d + 1 + n).choose (d + 1)) : S)
have succ₁ : Eq.{u_1 + 1} (α := S) (↑((d + 1 + n).choose (d + 1)) : S) (↑((d + 1 + n).choose (d + 1)) : S)
Tactic: rw [Finset.sum_antidiagonal_choose_add, add_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
⊢ HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)
have zero : HPow.hPow (α := S⟦X⟧) (mk 1) (HAdd.hAdd (α := ℕ) 0 1) = mk fun (n : ℕ) ↦ (↑((0 + n).choose 0) : S)
Tactic: induction d with
  | zero => ext; simp
  | succ d hd =>
      ext n
      rw [pow_add, hd, pow_one, mul_comm, coeff_mul]
      simp_rw [coeff_mk, Pi.one_apply, one_mul]
      norm_cast
      rw [Finset.sum_antidiagonal_choose_add, add_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
zero : HPow.hPow (α := S⟦X⟧) (mk 1) (HAdd.hAdd (α := ℕ) 0 1) = mk fun (n : ℕ) ↦ (↑((0 + n).choose 0) : S)
⊢ HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)
have succ : ∀ (d : ℕ) (hd : HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)),
  HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1 + 1) = mk fun (n : ℕ) ↦ (↑((d + 1 + n).choose (d + 1)) : S)
Tactic: induction d with
  | zero => ext; simp
  | succ d hd =>
      ext n
      rw [pow_add, hd, pow_one, mul_comm, coeff_mul]
      simp_rw [coeff_mk, Pi.one_apply, one_mul]
      norm_cast
      rw [Finset.sum_antidiagonal_choose_add, add_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
⊢ (mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)) * HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) = 1
have rw : HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) * HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) = 1
Tactic: rw [← mk_one_pow_eq_mk_choose_add, ← mul_pow, mk_one_mul_one_sub_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
rw : HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) * HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) = 1
⊢ (mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)) * HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) = 1
have rw₁ : (mk 1 * HSub.hSub (α := S⟦X⟧) 1 X) ^ (d + 1) = 1
Tactic: rw [← mk_one_pow_eq_mk_choose_add, ← mul_pow, mk_one_mul_one_sub_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
rw : HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) * HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) = 1
rw₁ : (mk 1 * HSub.hSub (α := S⟦X⟧) 1 X) ^ (d + 1) = 1
⊢ (mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)) * HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) = 1
have rw₂ : HPow.hPow (α := S⟦X⟧) 1 (d + 1) = 1
Tactic: rw [← mk_one_pow_eq_mk_choose_add, ← mul_pow, mk_one_mul_one_sub_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
rw : HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) * HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) = 1
rw₁ : (mk 1 * HSub.hSub (α := S⟦X⟧) 1 X) ^ (d + 1) = 1
rw₂ : HPow.hPow (α := S⟦X⟧) 1 (d + 1) = 1
⊢ (mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)) * HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) = 1
have rw₃ : Eq.{u_1 + 1} (α := S⟦X⟧) 1 1
Tactic: rw [← mk_one_pow_eq_mk_choose_add, ← mul_pow, mk_one_mul_one_sub_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
⊢ (HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) * mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)) = 1
have rw : HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) * HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = 1
Tactic: rw [← mk_one_pow_eq_mk_choose_add, ← mul_pow, mul_comm, mk_one_mul_one_sub_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
rw : HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) * HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = 1
⊢ (HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) * mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)) = 1
have rw₁ : (HSub.hSub (α := S⟦X⟧) 1 X * mk 1) ^ (d + 1) = 1
Tactic: rw [← mk_one_pow_eq_mk_choose_add, ← mul_pow, mul_comm, mk_one_mul_one_sub_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
rw : HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) * HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = 1
rw₁ : (HSub.hSub (α := S⟦X⟧) 1 X * mk 1) ^ (d + 1) = 1
⊢ (HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) * mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)) = 1
have rw₂ : (mk 1 * HSub.hSub (α := S⟦X⟧) 1 X) ^ (d + 1) = 1
Tactic: rw [← mk_one_pow_eq_mk_choose_add, ← mul_pow, mul_comm, mk_one_mul_one_sub_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
rw : HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) * HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = 1
rw₁ : (HSub.hSub (α := S⟦X⟧) 1 X * mk 1) ^ (d + 1) = 1
rw₂ : (mk 1 * HSub.hSub (α := S⟦X⟧) 1 X) ^ (d + 1) = 1
⊢ (HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) * mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)) = 1
have rw₃ : HPow.hPow (α := S⟦X⟧) 1 (d + 1) = 1
Tactic: rw [← mk_one_pow_eq_mk_choose_add, ← mul_pow, mul_comm, mk_one_mul_one_sub_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
rw : HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) * HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = 1
rw₁ : (HSub.hSub (α := S⟦X⟧) 1 X * mk 1) ^ (d + 1) = 1
rw₂ : (mk 1 * HSub.hSub (α := S⟦X⟧) 1 X) ^ (d + 1) = 1
rw₃ : HPow.hPow (α := S⟦X⟧) 1 (d + 1) = 1
⊢ (HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) * mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)) = 1
have rw₄ : Eq.{u_1 + 1} (α := S⟦X⟧) 1 1
Tactic: rw [← mk_one_pow_eq_mk_choose_add, ← mul_pow, mul_comm, mk_one_mul_one_sub_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
h : 0 < d
⊢ (↑(invOneSubPow S d) : S⟦X⟧) = mk fun (n : ℕ) ↦ (↑((d - 1 + n).choose (d - 1)) : S)
have rw : (↑(invOneSubPow S (d - 1 + 1)) : S⟦X⟧) = mk fun (n : ℕ) ↦ (↑((d - 1 + 1 - 1 + n).choose (d - 1 + 1 - 1)) : S)
Tactic: rw [← Nat.sub_one_add_one_eq_of_pos h, invOneSubPow, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
h : 0 < d
rw : (↑(invOneSubPow S (d - 1 + 1)) : S⟦X⟧) = mk fun (n : ℕ) ↦ (↑((d - 1 + 1 - 1 + n).choose (d - 1 + 1 - 1)) : S)
⊢ (↑(invOneSubPow S d) : S⟦X⟧) = mk fun (n : ℕ) ↦ (↑((d - 1 + n).choose (d - 1)) : S)
have rw₁ : (↑{ val := mk fun (n : ℕ) ↦ (↑((d - 1 + n).choose (d - 1)) : S), inv := HSub.hSub (α := S⟦X⟧) 1 X ^ (d - 1 + 1),
        val_inv := sorry, inv_val := sorry : S⟦X⟧ˣ } :
    S⟦X⟧) =
  mk fun (n : ℕ) ↦ (↑((d - 1 + 1 - 1 + n).choose (d - 1 + 1 - 1)) : S)
Tactic: rw [← Nat.sub_one_add_one_eq_of_pos h, invOneSubPow, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
h : 0 < d
rw : (↑(invOneSubPow S (d - 1 + 1)) : S⟦X⟧) = mk fun (n : ℕ) ↦ (↑((d - 1 + 1 - 1 + n).choose (d - 1 + 1 - 1)) : S)
rw₁ :
  (↑{ val := mk fun (n : ℕ) ↦ (↑((d - 1 + n).choose (d - 1)) : S), inv := HSub.hSub (α := S⟦X⟧) 1 X ^ (d - 1 + 1),
          val_inv := ⋯, inv_val := ⋯ : S⟦X⟧ˣ } :
      S⟦X⟧) =
    mk fun (n : ℕ) ↦ (↑((d - 1 + 1 - 1 + n).choose (d - 1 + 1 - 1)) : S)
⊢ (↑(invOneSubPow S d) : S⟦X⟧) = mk fun (n : ℕ) ↦ (↑((d - 1 + n).choose (d - 1)) : S)
have rw₂ : (↑{ val := mk fun (n : ℕ) ↦ (↑((d - 1 + n).choose (d - 1)) : S), inv := HSub.hSub (α := S⟦X⟧) 1 X ^ (d - 1 + 1),
        val_inv := sorry, inv_val := sorry : S⟦X⟧ˣ } :
    S⟦X⟧) =
  mk fun (n : ℕ) ↦ (↑((d - 1 + n).choose (d - 1)) : S)
Tactic: rw [← Nat.sub_one_add_one_eq_of_pos h, invOneSubPow, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
h : invOneSubPow S d = HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ d
⊢ invOneSubPow S (d + 1) = HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ (d + 1)
have succ : invOneSubPow S (d + 1) = (HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) sorry) (d + 1))⁻¹
Tactic: rw [inv_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
h : invOneSubPow S d = HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ d
⊢ HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯) (d + 1) * invOneSubPow S (d + 1) = 1
have rw : (↑(Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) sorry) : S⟦X⟧) ^ (d + 1) * (↑(invOneSubPow S (d + 1)) : S⟦X⟧) = 1
Tactic: rw [← Units.val_eq_one, Units.val_mul, Units.val_pow_eq_pow_val]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
⊢ invOneSubPow S d = HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ d
have zero : invOneSubPow S 0 = HPow.hPow (α := S⟦X⟧ˣ) (β := ℕ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) sorry)⁻¹ 0
Tactic: induction d with
  | zero => exact Eq.symm <| pow_zero _
  | succ d _ =>
      rw [inv_pow]
      exact (DivisionMonoid.inv_eq_of_mul _ (invOneSubPow S (d + 1)) <| by
        rw [← Units.val_eq_one, Units.val_mul, Units.val_pow_eq_pow_val]
        exact (invOneSubPow S (d + 1)).inv_val).symm
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
zero : invOneSubPow S 0 = HPow.hPow (α := S⟦X⟧ˣ) (β := ℕ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ 0
⊢ invOneSubPow S d = HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ d
have succ : ∀ (d : ℕ),
  invOneSubPow S d = HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) sorry)⁻¹ d →
    invOneSubPow S (d + 1) = HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) sorry)⁻¹ (d + 1)
Tactic: induction d with
  | zero => exact Eq.symm <| pow_zero _
  | succ d _ =>
      rw [inv_pow]
      exact (DivisionMonoid.inv_eq_of_mul _ (invOneSubPow S (d + 1)) <| by
        rw [← Units.val_eq_one, Units.val_mul, Units.val_pow_eq_pow_val]
        exact (invOneSubPow S (d + 1)).inv_val).symm
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
⊢ Units.inv (invOneSubPow S d) = HSub.hSub (α := S⟦X⟧) 1 X ^ d
have zero : Units.inv (invOneSubPow S 0) = HPow.hPow (β := ℕ) (HSub.hSub (α := S⟦X⟧) 1 X) 0
Tactic: induction d with
  | zero => exact Eq.symm <| pow_zero _
  | succ d => rfl
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
zero : Units.inv (invOneSubPow S 0) = HPow.hPow (β := ℕ) (HSub.hSub (α := S⟦X⟧) 1 X) 0
⊢ Units.inv (invOneSubPow S d) = HSub.hSub (α := S⟦X⟧) 1 X ^ d
have succ : ∀ (d : ℕ),
  Units.inv (invOneSubPow S d) = HSub.hSub (α := S⟦X⟧) 1 X ^ d →
    Units.inv (invOneSubPow S (d + 1)) = HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1)
Tactic: induction d with
  | zero => exact Eq.symm <| pow_zero _
  | succ d => rfl
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
S : Type u_1
inst : CommRing S
d e : ℕ
⊢ invOneSubPow S (d + e) = HMul.hMul (α := S⟦X⟧ˣ) (invOneSubPow S d) (invOneSubPow S e)
have simp_rw : HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) sorry)⁻¹ (d + e) =
  HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) sorry)⁻¹ d *
    HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) sorry)⁻¹ e
Tactic: simp_rw [invOneSubPow_eq_inv_one_sub_pow, pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
A : Type u_1
A' : Type u_2
inst : Ring A
inst_1 : Ring A'
inst_2 : Algebra ℚ A
inst_3 : Algebra ℚ A'
f : A →+* A'
⊢ (map f : (a : A⟦X⟧) → A'⟦X⟧) (sin A) = sin A'
have h : ∀ (n : ℕ),
  Eq.{u_2 + 1} (α := A') ((coeff n : (a : A'⟦X⟧) → A') ((map f : (a : A⟦X⟧) → A'⟦X⟧) (sin A) : A'⟦X⟧) : A')
    ((coeff n : (a : A'⟦X⟧) → A') (sin A') : A')
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WellKnown (goal)
Goal:
A : Type u_1
A' : Type u_2
inst : Ring A
inst_1 : Ring A'
inst_2 : Algebra ℚ A
inst_3 : Algebra ℚ A'
f : A →+* A'
⊢ (map f : (a : A⟦X⟧) → A'⟦X⟧) (cos A) = cos A'
have h : ∀ (n : ℕ),
  Eq.{u_2 + 1} (α := A') ((coeff n : (a : A'⟦X⟧) → A') ((map f : (a : A⟦X⟧) → A'⟦X⟧) (cos A) : A'⟦X⟧) : A')
    ((coeff n : (a : A'⟦X⟧) → A') (cos A') : A')
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Prime (hypothesis)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
x y a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hx : x * y = a * ∏ i ∈ insert i s, p i
⊢ ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
    t ∪ u = insert i s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
have hx₁ : x * y = a * p i * ∏ x ∈ s, p x
Tactic: rw [prod_insert his, ← mul_assoc] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Prime (hypothesis)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
x y a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hx : x * y = a * p i * ∏ x ∈ s, p x
⊢ ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
    t ∪ u = insert i s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
have hpi : Prime (p i)
Tactic: have hpi : Prime (p i) := hp i (mem_insert_self _ _)