awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : f ∉ Ideal.span {X}
hfI : f ∈ I
⊢ ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)

Tactic:
rw [Ideal.mem_span_singleton, X_dvd_iff] at hfX

Premises used: Ideal.mem_span_singleton, PowerSeries.X_dvd_iff
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : f ∉ Ideal.span {X}
hfI : f ∈ I
hfX₁ : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
⊢ f ∈ I

Tactic:
rw [Ideal.mem_span_singleton, X_dvd_iff] at hfX

Premises used: Ideal.mem_span_singleton, PowerSeries.X_dvd_iff
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
hfI : f ∈ I
rw rw₁ : Eq (α := k⟦X⟧) ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧) ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)
⊢ (C : (a : k) → k⟦X⟧) (f 0) = f - HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)

Tactic:
rw [sub_sub_cancel]

Premises used: sub_sub_cancel
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
hfI : f ∈ I
⊢ (C : (a : k) → k⟦X⟧) (f 0) = f - HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)

Tactic:
have : C (f 0) = f - (f - C (f 0)) := by rw [sub_sub_cancel]
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
hfI : f ∈ I
this : (C : (a : k) → k⟦X⟧) (f 0) = f - HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)
rw : f - HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧) ∈ I
⊢ Membership.mem (α := k⟦X⟧) I ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
hfI : f ∈ I
this : (C : (a : k) → k⟦X⟧) (f 0) = f - HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)
apply : HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧) ∈ I
⊢ f - HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧) ∈ I

Tactic:
apply Ideal.sub_mem I hfI

Premises used: Ideal.sub_mem
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
hfI : f ∈ I
this : (C : (a : k) → k⟦X⟧) (f 0) = f - HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)
a :
  Membership.mem (γ := Submodule k⟦X⟧ k⟦X⟧) (Ideal.span {X})
    (HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧))
⊢ HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧) ∈ I

Tactic:
apply hI
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
hfI : f ∈ I
this : (C : (a : k) → k⟦X⟧) (f 0) = f - HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)
a : (constantCoeff : (a : k⟦X⟧) → k) f = f 0
⊢ Membership.mem (γ := Submodule k⟦X⟧ k⟦X⟧) (Ideal.span {X})
    (HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧))

Tactic:
rw [Ideal.mem_span_singleton, X_dvd_iff, map_sub, constantCoeff_C, ←
          coeff_zero_eq_constantCoeff_apply, sub_eq_zero, coeff_zero_eq_constantCoeff]

Premises used: map_sub, sub_eq_zero, PowerSeries.constantCoeff_C, PowerSeries.coeff_zero_eq_constantCoeff_apply, PowerSeries.coeff_zero_eq_constantCoeff, Ideal.mem_span_singleton, PowerSeries.X_dvd_iff
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
hfI : f ∈ I
this : (C : (a : k) → k⟦X⟧) (f 0) = f - HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)
⊢ (constantCoeff : (a : k⟦X⟧) → k) f = f 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
hfI : f ∈ I
⊢ Membership.mem (α := k⟦X⟧) I ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)

Tactic:
have hfI0 : C (f 0) ∈ I := by
        have : C (f 0) = f - (f - C (f 0)) := by rw [sub_sub_cancel]
        rw [this]
        apply Ideal.sub_mem I hfI
        apply hI
        rw [Ideal.mem_span_singleton, X_dvd_iff, map_sub, constantCoeff_C, ←
          coeff_zero_eq_constantCoeff_apply, sub_eq_zero, coeff_zero_eq_constantCoeff]
        rfl
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
hfI : f ∈ I
hfI0 : Membership.mem (α := k⟦X⟧) I ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)
right : I = ⊤
⊢ 1 ∈ I

Tactic:
rw [← Ideal.eq_top_iff_one]

Premises used: Ideal.eq_top_iff_one
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
hfI : f ∈ I
hfI0 : Membership.mem (α := k⟦X⟧) I ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)
⊢ I = ⊤

Tactic:
apply Ideal.eq_top_of_isUnit_mem I hfI0 (IsUnit.map C (Ne.isUnit hfX))

Premises used: Ne.isUnit, Ideal.eq_top_of_isUnit_mem, PowerSeries.C, IsUnit.map
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
⊢ Ideal.IsMaximal (α := k⟦X⟧) (Ideal.span {X})

Tactic:
have hX : (Ideal.span {(X : k⟦X⟧)}).IsMaximal := by
    rw [Ideal.isMaximal_iff]
    constructor
    · rw [Ideal.mem_span_singleton]
      exact Prime.not_dvd_one X_prime
    · intro I f hI hfX hfI
      rw [Ideal.mem_span_singleton, X_dvd_iff] at hfX
      have hfI0 : C (f 0) ∈ I := by
        have : C (f 0) = f - (f - C (f 0)) := by rw [sub_sub_cancel]
        rw [this]
        apply Ideal.sub_mem I hfI
        apply hI
        rw [Ideal.mem_span_singleton, X_dvd_iff, map_sub, constantCoeff_C, ←
          coeff_zero_eq_constantCoeff_apply, sub_eq_zero, coeff_zero_eq_constantCoeff]
        rfl
      rw [← Ideal.eq_top_iff_one]
      apply Ideal.eq_top_of_isUnit_mem I hfI0 (IsUnit.map C (Ne.isUnit hfX))
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
hX : Ideal.IsMaximal (α := k⟦X⟧) (Ideal.span {X})
rw rw₁ : Eq.{u_2 + 1} (α := Ideal k⟦X⟧) (IsLocalRing.maximalIdeal k⟦X⟧) (IsLocalRing.maximalIdeal k⟦X⟧)
⊢ Eq (α := Ideal k⟦X⟧) (IsLocalRing.maximalIdeal k⟦X⟧) (Ideal.span {X})

Tactic:
rw [IsLocalRing.eq_maximalIdeal hX]

Premises used: IsLocalRing.eq_maximalIdeal
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
k : Type u_2
inst : Field k
⊢ Eq.{u_2 + 1} (α := k⟦X⟧ˣ) (Unit_of_divided_by_X_pow_order 0)⁻¹ 1

Tactic:
simp only [Unit_of_divided_by_X_pow_order_zero, inv_one]

Premises used: PowerSeries.Unit_of_divided_by_X_pow_order_zero, inv_one
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
k : Type u_2
inst : Field k
a b : k⟦X⟧
hf : a ≠ 0
hg : b ≠ 0
simp :
  (a * b).Unit_of_divided_by_X_pow_order =
    HMul.hMul (α := k⟦X⟧ˣ) a.Unit_of_divided_by_X_pow_order b.Unit_of_divided_by_X_pow_order
⊢ (a * b).Unit_of_divided_by_X_pow_order⁻¹ =
    HMul.hMul (α := k⟦X⟧ˣ) a.Unit_of_divided_by_X_pow_order⁻¹ b.Unit_of_divided_by_X_pow_order⁻¹

Tactic:
simp only [← mul_inv, inv_inj]

Premises used: mul_inv, inv_inj
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
k : Type u_2
inst : Field k
a b : k⟦X⟧
hf : a ≠ 0
hg : b ≠ 0
⊢ (a * b).Unit_of_divided_by_X_pow_order =
    HMul.hMul (α := k⟦X⟧ˣ) a.Unit_of_divided_by_X_pow_order b.Unit_of_divided_by_X_pow_order

Tactic:
simp only [Unit_of_divided_by_X_pow_order_nonzero (mul_ne_zero hf hg),
      Unit_of_divided_by_X_pow_order_nonzero hf, Unit_of_divided_by_X_pow_order_nonzero hg,
      Units.ext_iff, Units.val_mul, ← divXPowOrder_mul]

Premises used: Units.ext_iff, PowerSeries.divXPowOrder_mul, PowerSeries.Unit_of_divided_by_X_pow_order_nonzero, mul_ne_zero, Units.val_mul
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
k : Type u_2
inst : Field k
u : k⟦X⟧ˣ
set :
  let u₀ := (↑u : k⟦X⟧);
  ∀ (hu : u₀ = (↑u : k⟦X⟧)), u₀.Unit_of_divided_by_X_pow_order⁻¹ = u⁻¹
⊢ (↑u : k⟦X⟧).Unit_of_divided_by_X_pow_order⁻¹ = u⁻¹

Tactic:
set u₀ := u.1 with hu

Premises used: Units.val
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
k : Type u_2
inst : Field k
u : k⟦X⟧ˣ
u₀ : k⟦X⟧ := (↑u : k⟦X⟧)
hu : u₀ = (↑u : k⟦X⟧)
⊢ IsUnit u₀

Tactic:
have h₀ : IsUnit u₀ := ⟨u, hu.symm⟩
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
k : Type u_2
inst : Field k
u : k⟦X⟧ˣ
u₀ : k⟦X⟧ := (↑u : k⟦X⟧)
hu : u₀ = (↑u : k⟦X⟧)
h₀ : IsUnit u₀
rw : u₀.divXPowOrder = u₀
⊢ u₀.Unit_of_divided_by_X_pow_order⁻¹ = u⁻¹

Tactic:
rw [inv_inj, Units.ext_iff, ← hu, Unit_of_divided_by_X_pow_order_nonzero h₀.ne_zero]

Premises used: Units.ext_iff, inv_inj, PowerSeries.Unit_of_divided_by_X_pow_order_nonzero, IsUnit.ne_zero
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
k : Type u_2
inst : Field k
u : k⟦X⟧ˣ
u₀ : k⟦X⟧ := (↑u : k⟦X⟧)
hu : u₀ = (↑u : k⟦X⟧)
h₀ : IsUnit u₀
⊢ u₀.divXPowOrder = u₀

Tactic:
((eq_divided_by_X_pow_order_Iff_Unit h₀.ne_zero).mpr h₀).symm

Premises used: Iff.mpr, PowerSeries.eq_divided_by_X_pow_order_Iff_Unit, IsUnit.ne_zero, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
k : Type u_2
inst : Field k
u : k⟦X⟧ˣ
u₀ : k⟦X⟧ := (↑u : k⟦X⟧)
hu : u₀ = (↑u : k⟦X⟧)
h₀ : IsUnit u₀
⊢ u₀.divXPowOrder = u₀

Tactic:
exact ((eq_divided_by_X_pow_order_Iff_Unit h₀.ne_zero).mpr h₀).symm

Premises used: Iff.mpr, PowerSeries.eq_divided_by_X_pow_order_Iff_Unit, IsUnit.ne_zero, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
⊢ Eq.{u_2 + 1} (α := k⟦X⟧ˣ) (normUnit X) 1

Tactic:
simp [normUnit, ← Units.val_eq_one, Unit_of_divided_by_X_pow_order_nonzero]

Premises used: PowerSeries.Unit_of_divided_by_X_pow_order_nonzero, Units.val_eq_one, NormalizationMonoid.normUnit
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
⊢ Eq.{u_2 + 1} (α := k⟦X⟧) X ((normalize : (a : k⟦X⟧) → k⟦X⟧) X)

Tactic:
simp only [normalize_apply, normUnit_X, Units.val_one, mul_one]

Premises used: PowerSeries.normUnit_X, normalize_apply, Units.val_one, mul_one
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
P : k[X]
hP : P ≠ 0
H :
  ∀ (c : ℕ),
    c ≤ Multiset.count X (normalizedFactors (↑P : k⟦X⟧)) ↔ c ≤ Multiset.count Polynomial.X (normalizedFactors P)
⊢ Multiset.count X (normalizedFactors (↑P : k⟦X⟧)) = Multiset.count Polynomial.X (normalizedFactors P)

Tactic:
apply eq_of_forall_le_iff

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
P : k[X]
hP : P ≠ 0
H :
  ∀ (c : ℕ),
    LE.le (α := ℕ∞) (↑c : ℕ∞) (↑(Multiset.count X (normalizedFactors (↑P : k⟦X⟧))) : ℕ∞) ↔
      LE.le (α := ℕ∞) (↑c : ℕ∞) (↑(Multiset.count Polynomial.X (normalizedFactors P)) : ℕ∞)
⊢ ∀ (c : ℕ),
    c ≤ Multiset.count X (normalizedFactors (↑P : k⟦X⟧)) ↔ c ≤ Multiset.count Polynomial.X (normalizedFactors P)

Tactic:
simp only [← Nat.cast_le (α := ℕ∞)]

Premises used: Nat.cast_le
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
P : k[X]
hP : P ≠ 0
H : ∀ (c : ℕ), (↑c : ℕ∞) ≤ emultiplicity X (↑P : k⟦X⟧) ↔ (↑c : ℕ∞) ≤ emultiplicity Polynomial.X P
H₁ : (↑P : k⟦X⟧) ≠ 0
⊢ ∀ (c : ℕ),
    LE.le (α := ℕ∞) (↑c : ℕ∞) (↑(Multiset.count X (normalizedFactors (↑P : k⟦X⟧))) : ℕ∞) ↔
      LE.le (α := ℕ∞) (↑c : ℕ∞) (↑(Multiset.count Polynomial.X (normalizedFactors P)) : ℕ∞)

Tactic:
rw [X_eq_normalize, PowerSeries.X_eq_normalizeX, ← emultiplicity_eq_count_normalizedFactors
    irreducible_X hP, ← emultiplicity_eq_count_normalizedFactors X_irreducible]

Premises used: UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors, Polynomial.irreducible_X, PowerSeries.X_eq_normalizeX, Polynomial.X_eq_normalize
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
P : k[X]
hP : P ≠ 0
⊢ ∀ (c : ℕ), (↑c : ℕ∞) ≤ emultiplicity X (↑P : k⟦X⟧) ↔ (↑c : ℕ∞) ≤ emultiplicity Polynomial.X P

Tactic:
simp only [← pow_dvd_iff_le_emultiplicity, Polynomial.X_pow_dvd_iff,
    PowerSeries.X_pow_dvd_iff, Polynomial.coeff_coe P, implies_true, ne_eq, coe_eq_zero_iff, hP,
    not_false_eq_true]

Premises used: Polynomial.coe_eq_zero_iff, ne_eq, Polynomial.X_pow_dvd_iff, pow_dvd_iff_le_emultiplicity, implies_true, PowerSeries.X_pow_dvd_iff, not_false_eq_true, Polynomial.coeff_coe
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
P : k[X]
hP : P ≠ 0
⊢ (↑P : k⟦X⟧) ≠ 0

Tactic:
simp only [← pow_dvd_iff_le_emultiplicity, Polynomial.X_pow_dvd_iff,
    PowerSeries.X_pow_dvd_iff, Polynomial.coeff_coe P, implies_true, ne_eq, coe_eq_zero_iff, hP,
    not_false_eq_true]

Premises used: Polynomial.coe_eq_zero_iff, ne_eq, Polynomial.X_pow_dvd_iff, pow_dvd_iff_le_emultiplicity, implies_true, PowerSeries.X_pow_dvd_iff, not_false_eq_true, Polynomial.coeff_coe
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
x : k⟦X⟧
rw :
  Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) x : k) (0 : k) ↔
    Membership.mem (γ := Ideal k⟦X⟧) (maximalIdeal k⟦X⟧ : Ideal k⟦X⟧) x
rw₁ : Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) x : k) (0 : k) ↔ Membership.mem (γ := Ideal k⟦X⟧) (Ideal.span {X}) x
rw₂ : Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) x : k) (0 : k) ↔ X ∣ x
rw₃ rw₄ :
  Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) x : k) (0 : k) ↔
    Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) x : k) (0 : k)
⊢ Membership.mem (γ := Ideal k⟦X⟧) (RingHom.ker (F := k⟦X⟧ →+* k) constantCoeff) x ↔
    Membership.mem (γ := Ideal k⟦X⟧) (maximalIdeal k⟦X⟧ : Ideal k⟦X⟧) x

Tactic:
rw [RingHom.mem_ker, maximalIdeal_eq_span_X, Ideal.mem_span_singleton, X_dvd_iff]

Premises used: PowerSeries.maximalIdeal_eq_span_X, RingHom.mem_ker, Ideal.mem_span_singleton, PowerSeries.X_dvd_iff
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) (log A) : A)
    (if n = 0 then 0 else (algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) (n + 1) / (↑n : ℚ)) : A)

Tactic:
coeff_mk _ _

Premises used: PowerSeries.log, PowerSeries.coeff_mk
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
⊢ Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) (log A) : A) (0 : A)

Tactic:
simp [← coeff_zero_eq_constantCoeff_apply]

Premises used: PowerSeries.coeff_zero_eq_constantCoeff_apply
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
A' : Type u_2
inst_2 : CommRing A'
inst_3 : Algebra ℚ A'
f : A →+* A'
h :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := A') ((coeff n : (a : A'⟦X⟧) → A') ((map f : (a : A⟦X⟧) → A'⟦X⟧) (log A) : A'⟦X⟧) : A')
      ((coeff n : (a : A'⟦X⟧) → A') (log A') : A')
⊢ (map f : (a : A⟦X⟧) → A'⟦X⟧) (log A) = log A'

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
A' : Type u_2
inst_2 : CommRing A'
inst_3 : Algebra ℚ A'
f : A →+* A'
n : ℕ
h :
  Eq.{u_2 + 1} (α := A')
    ((f : (a : A) → A')
        (if n = 0 then 0 else (algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) (n + 1) / (↑n : ℚ)) : A) :
      A')
    (if n = 0 then 0 else (algebraMap ℚ A' : (a : ℚ) → A') (HPow.hPow (α := ℚ) (-1) (n + 1) / (↑n : ℚ)) : A')
⊢ Eq.{u_2 + 1} (α := A') ((coeff n : (a : A'⟦X⟧) → A') ((map f : (a : A⟦X⟧) → A'⟦X⟧) (log A) : A'⟦X⟧) : A')
    ((coeff n : (a : A'⟦X⟧) → A') (log A') : A')

Tactic:
simp only [coeff_map, coeff_log]

Premises used: PowerSeries.coeff_log, PowerSeries.coeff_map
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
A' : Type u_2
inst_2 : CommRing A'
inst_3 : Algebra ℚ A'
f : A →+* A'
n : ℕ
pos : n = 0 → Eq.{u_2 + 1} (α := A') ((f : (a : A) → A') 0 : A') (0 : A')
neg :
  ¬n = 0 →
    Eq.{u_2 + 1} (α := A')
      ((f : (a : A) → A') ((algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) (n + 1) / (↑n : ℚ)) : A) : A')
      ((algebraMap ℚ A' : (a : ℚ) → A') (HPow.hPow (α := ℚ) (-1) (n + 1) / (↑n : ℚ)) : A')
⊢ Eq.{u_2 + 1} (α := A')
    ((f : (a : A) → A')
        (if n = 0 then 0 else (algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) (n + 1) / (↑n : ℚ)) : A) :
      A')
    (if n = 0 then 0 else (algebraMap ℚ A' : (a : ℚ) → A') (HPow.hPow (α := ℚ) (-1) (n + 1) / (↑n : ℚ)) : A')

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
A' : Type u_2
inst_2 : CommRing A'
inst_3 : Algebra ℚ A'
f : A →+* A'
n : ℕ
h : n = 0
⊢ Eq.{u_2 + 1} (α := A') ((f : (a : A) → A') 0 : A') (0 : A')

Tactic:
simp [RingHom.map_rat_algebraMap]

Premises used: RingHom.map_rat_algebraMap
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
A' : Type u_2
inst_2 : CommRing A'
inst_3 : Algebra ℚ A'
f : A →+* A'
n : ℕ
h : ¬n = 0
⊢ Eq.{u_2 + 1} (α := A')
    ((f : (a : A) → A') ((algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) (n + 1) / (↑n : ℚ)) : A) : A')
    ((algebraMap ℚ A' : (a : ℚ) → A') (HPow.hPow (α := ℚ) (-1) (n + 1) / (↑n : ℚ)) : A')

Tactic:
simp [RingHom.map_rat_algebraMap]

Premises used: RingHom.map_rat_algebraMap
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
⊢ Eq (α := A) ((coeff 1 : (a : A⟦X⟧) → A) (log A) : A) (1 : A)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
inst_2 : Nontrivial A
⊢ Ne (α := A) ((coeff 1 : (a : A⟦X⟧) → A) (log A) : A) (0 : A)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
inst_2 : Nontrivial A
i : ℕ
hi : i < 1
⊢ Eq (α := A) ((coeff i : (a : A⟦X⟧) → A) (log A) : A) (0 : A)

Tactic:
simp [Nat.lt_one_iff.mp hi]

Premises used: Nat.lt_one_iff, Iff.mp
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
h :
  ∀ (n : ℕ),
    Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (log A) : A⟦X⟧) : A)
      ((coeff n : (a : A⟦X⟧) → A) (mk fun (n : ℕ) ↦ (algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) n)) : A)
⊢ Eq (α := A⟦X⟧) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (log A) : A⟦X⟧)
    (mk fun (n : ℕ) ↦ (algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) n) : A⟦X⟧)

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
⊢ HAdd.hAdd (α := A) (↑n : A) 1 = (algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
⊢ HAdd.hAdd (α := A) (↑n : A) 1 = (algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1)

Tactic:
have : (n + 1) = algebraMap ℚ A (n + 1) := by simp
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
this : HAdd.hAdd (α := A) (↑n : A) 1 = (algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1)
h :
  HMul.hMul (α := A)
      (if n + 1 = 0 then 0 else (algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) (n + 1 + 1) / (↑(n + 1) : ℚ)) :
        A)
      (HAdd.hAdd (α := A) (↑n : A) 1) =
    (algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) n)
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (log A) : A⟦X⟧) : A)
    ((coeff n : (a : A⟦X⟧) → A) (mk fun (n : ℕ) ↦ (algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) n)) : A)

Tactic:
rw [coeff_derivative, coeff_log, coeff_mk]

Premises used: PowerSeries.coeff_mk, PowerSeries.coeff_log, PowerSeries.coeff_derivative
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
this : HAdd.hAdd (α := A) (↑n : A) 1 = (algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1)
⊢ HMul.hMul (α := A)
      (if n + 1 = 0 then 0 else (algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) (n + 1 + 1) / (↑(n + 1) : ℚ)) :
        A)
      (HAdd.hAdd (α := A) (↑n : A) 1) =
    (algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) n)

Tactic:
grind
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
⊢ HasSubst (PowerSeries.log A)

Tactic:
HasSubst.of_constantCoeff_zero' constantCoeff_log

Premises used: PowerSeries.HasSubst.of_constantCoeff_zero', PowerSeries.constantCoeff_log
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
⊢ Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) (exp A - 1) : A) (0 : A)

Tactic:
simp [constantCoeff_exp]

Premises used: PowerSeries.constantCoeff_exp
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
f : A⟦X⟧
⊢ f.logOf = subst (f - 1) (log A)

Tactic:
rfl

Premises used: PowerSeries.logOf, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
f : A⟦X⟧
hf : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A)
rw : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) (subst (f - 1) (log A)) : A) (0 : A)
⊢ Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f.logOf : A) (0 : A)

Tactic:
rw [logOf_eq]

Premises used: PowerSeries.logOf_eq
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
f : A⟦X⟧
hf : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A)
rw :
  HSub.hSub (α := A) (β := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) f : A)
      ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) 1 : A) =
    0
rw₁ : HSub.hSub (α := A) (β := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) f : A) (1 : A) = 0
rw₂ : HSub.hSub (α := A) (β := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A) = 0
rw₃ : HSub.hSub (α := A) 1 1 = 0
rw₄ rw₅ : Eq.{u_1 + 1} (α := A) 0 0
⊢ Eq (α := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) (f - 1) : A) (0 : A)

Tactic:
rw [map_sub, map_one, ← constantCoeff_eq, hf, sub_self]

Premises used: map_sub, sub_self, PowerSeries.constantCoeff_eq, map_one
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
f : A⟦X⟧
hf : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A)
⊢ Eq (α := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) (f - 1) : A) (0 : A)

Tactic:
have h : MvPowerSeries.constantCoeff (f - 1 : A⟦X⟧) = 0 := by
    rw [map_sub, map_one, ← constantCoeff_eq, hf, sub_self]
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
f : A⟦X⟧
hf : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A)
h : Eq (α := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) (f - 1) : A) (0 : A)
⊢ Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) (subst (f - 1) (log A)) : A) (0 : A)

Tactic:
constantCoeff_subst_eq_zero h _ constantCoeff_log

Premises used: PowerSeries.constantCoeff_log, PowerSeries.constantCoeff_subst_eq_zero
-- Module: Mathlib.RingTheory.PowerSeries.Log
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
f : A⟦X⟧
hf : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A)
h : Eq (α := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) (f - 1) : A) (0 : A)
⊢ Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) (subst (f - 1) (log A)) : A) (0 : A)

Tactic:
exact constantCoeff_subst_eq_zero h _ constantCoeff_log

Premises used: PowerSeries.constantCoeff_log, PowerSeries.constantCoeff_subst_eq_zero