awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Flat.TorsionFree
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsBezout R
inst_4 : IsDomain R
htors : IsTorsionFree R M
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
h₁ :
  Eq.{u_2 + 1} (α := M → M)
    (Function.comp (β := R ⊗[R] M) (⇑(lift (lsmul R M)) : (a : R ⊗[R] M) → M)
      (⇑(LinearEquiv.toEquiv (LinearEquiv.symm (TensorProduct.lid R M))) : (a : M) → R ⊗[R] M))
    id
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := M) (β := M)
    (Function.comp (β := R ⊗[R] M) (⇑(lift (lsmul R M)) : (a : R ⊗[R] M) → M)
      (⇑(LinearEquiv.toEquiv (LinearEquiv.symm (TensorProduct.lid R M))) : (a : M) → R ⊗[R] M))

Tactic:
convert! Function.injective_id

Premises used: Function.injective_id
-- Module: Mathlib.RingTheory.Flat.TorsionFree
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsBezout R
inst_4 : IsDomain R
htors : IsTorsionFree R M
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
h₁ :
  ∀ (x : M),
    Function.comp (β := R ⊗[R] M) (⇑(lift (lsmul R M)) : (a : R ⊗[R] M) → M)
        (⇑(LinearEquiv.toEquiv (LinearEquiv.symm (TensorProduct.lid R M))) : (a : M) → R ⊗[R] M) x =
      id x
⊢ Eq.{u_2 + 1} (α := M → M)
    (Function.comp (β := R ⊗[R] M) (⇑(lift (lsmul R M)) : (a : R ⊗[R] M) → M)
      (⇑(LinearEquiv.toEquiv (LinearEquiv.symm (TensorProduct.lid R M))) : (a : M) → R ⊗[R] M))
    id

Tactic:
ext
-- Module: Mathlib.RingTheory.Flat.TorsionFree
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsBezout R
inst_4 : IsDomain R
htors : IsTorsionFree R M
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
x : M
⊢ Function.comp (β := R ⊗[R] M) (⇑(lift (lsmul R M)) : (a : R ⊗[R] M) → M)
      (⇑(LinearEquiv.toEquiv (LinearEquiv.symm (TensorProduct.lid R M))) : (a : M) → R ⊗[R] M) x =
    id x

Tactic:
simp
-- Module: Mathlib.RingTheory.Flat.TorsionFree
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
h : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], ValuationRing.{u_1} (Localization (M := R) P.primeCompl)
⊢ Flat R M ↔ Eq (α := Submodule R M) (torsion R M) ⊥

Tactic:
⟨fun _ ↦ Flat.torsion_eq_bot, fun h ↦ ?_⟩

Premises used: Module.Flat.torsion_eq_bot, Iff.intro
-- Module: Mathlib.RingTheory.Flat.TorsionFree
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
h : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], ValuationRing.{u_1} (Localization (M := R) P.primeCompl)
refine : ∀ (h : Eq (α := Submodule R M) (torsion R M) ⊥), Flat R M
⊢ Flat R M ↔ Eq (α := Submodule R M) (torsion R M) ⊥

Tactic:
refine ⟨fun _ ↦ Flat.torsion_eq_bot, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Flat.TorsionFree
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
h_1 : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], ValuationRing.{u_1} (Localization (M := R) P.primeCompl)
h : Eq (α := Submodule R M) (torsion R M) ⊥
h₁ : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], Flat R (LocalizedModule P.primeCompl M)
⊢ Flat R M

Tactic:
apply flat_of_localized_maximal

Premises used: Module.flat_of_localized_maximal
-- Module: Mathlib.RingTheory.Flat.TorsionFree
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
h_1 : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], ValuationRing.{u_1} (Localization (M := R) P.primeCompl)
h : Eq (α := Submodule R M) (torsion R M) ⊥
P : Ideal R
hP : P.IsMaximal
h₁ : ∀ (h : IsTorsionFree R M) (P : Ideal R) [hP : P.IsMaximal], Flat R (LocalizedModule P.primeCompl M)
⊢ Flat R (LocalizedModule P.primeCompl M)

Tactic:
rw [← Submodule.isTorsionFree_iff_torsion_eq_bot] at h

Premises used: Submodule.isTorsionFree_iff_torsion_eq_bot
-- Module: Mathlib.RingTheory.Flat.TorsionFree
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
h_1 : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], ValuationRing.{u_1} (Localization (M := R) P.primeCompl)
h : IsTorsionFree R M
P : Ideal R
hP : P.IsMaximal
h₁ : IsTorsionFree (Localization (M := R) P.primeCompl) (LocalizedModule P.primeCompl M)
⊢ Flat R (LocalizedModule P.primeCompl M)

Tactic:
rw [← flat_iff_of_isLocalization (Localization P.primeCompl) P.primeCompl,
    Flat.flat_iff_torsion_eq_bot_of_isBezout, ← Submodule.isTorsionFree_iff_torsion_eq_bot]

Premises used: Localization, Module.Flat.flat_iff_torsion_eq_bot_of_isBezout, Submodule.isTorsionFree_iff_torsion_eq_bot, Ideal.primeCompl, Module.flat_iff_of_isLocalization
-- Module: Mathlib.RingTheory.Flat.TorsionFree
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
h_1 : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], ValuationRing.{u_1} (Localization (M := R) P.primeCompl)
h : IsTorsionFree R M
P : Ideal R
hP : P.IsMaximal
⊢ IsTorsionFree (Localization (M := R) P.primeCompl) (LocalizedModule P.primeCompl M)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Flat.TorsionFree
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDedekindDomain R
h : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], ValuationRing.{u_1} (Localization (M := R) P.primeCompl)
⊢ Flat R M ↔ Eq (α := Submodule R M) (torsion R M) ⊥

Tactic:
apply flat_iff_torsion_eq_bot_of_valuationRing_localization_isMaximal

Premises used: Module.Flat.flat_iff_torsion_eq_bot_of_valuationRing_localization_isMaximal
-- Module: Mathlib.RingTheory.Flat.TorsionFree
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDedekindDomain R
⊢ ∀ (P : Ideal R) [inst_4 : P.IsMaximal], ValuationRing.{u_1} (Localization (M := R) P.primeCompl)

Tactic:
fun P ↦ inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Flat.TorsionFree
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDedekindDomain R
⊢ ∀ (P : Ideal R) [inst_4 : P.IsMaximal], ValuationRing.{u_1} (Localization (M := R) P.primeCompl)

Tactic:
exact fun P ↦ inferInstance
-- Module: Mathlib.RingTheory.Flat.TorsionFree
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDedekindDomain R
inst_4 rw : IsTorsionFree R M
⊢ Flat R M

Tactic:
rw [IsDedekindDomain.flat_iff_torsion_eq_bot, ← Submodule.isTorsionFree_iff_torsion_eq_bot]

Premises used: Submodule.isTorsionFree_iff_torsion_eq_bot, IsDedekindDomain.flat_iff_torsion_eq_bot
-- Module: Mathlib.RingTheory.Flat.TorsionFree
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDedekindDomain R
inst_4 : IsTorsionFree R M
⊢ IsTorsionFree R M

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
⊢ Eq (α := R) ((constantCoeff : (a : MvPowerSeries (Fin 2) R) → R) (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁) : R)
    (0 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
⊢ Eq (α := R)
    ((coeff (single 0 1) : (a : MvPowerSeries (Fin 2) R) → R) (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁) : R)
    (1 : R)

Tactic:
simp [coeff_index_single_X]

Premises used: MvPowerSeries.coeff_index_single_X
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
⊢ Eq (α := R)
    ((coeff (single 1 1) : (a : MvPowerSeries (Fin 2) R) → R) (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁) : R)
    (1 : R)

Tactic:
simp [coeff_index_single_X]

Premises used: MvPowerSeries.coeff_index_single_X
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
⊢ HasSubst (τ := Fin 3) (S := R) ![subst ![Y₀, Y₁] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁), Y₂]

Tactic:
obtain aux₁ := HasSubst.cons_subst_zero_left (f := X₀ + X₁) (0 : Fin 3) 1 2 (by simp)
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
aux₁ : HasSubst (τ := Fin 3) (S := R) ![subst ![Y₀, Y₁] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁), Y₂]
⊢ Eq (α := R) ((constantCoeff : (a : MvPowerSeries (Fin 2) R) → R) (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁) : R)
    (0 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
aux₁ : HasSubst (τ := Fin 3) (S := R) ![subst ![Y₀, Y₁] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁), Y₂]
⊢ HasSubst (τ := Fin 3) (S := R) ![Y₀, subst ![Y₁, Y₂] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁)]

Tactic:
obtain aux₂ := HasSubst.cons_subst_zero_right (f := X₀ + X₁) (0 : Fin 3) 1 2 (by simp)
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
aux₁ : HasSubst (τ := Fin 3) (S := R) ![subst ![Y₀, Y₁] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁), Y₂]
aux₂ : HasSubst (τ := Fin 3) (S := R) ![Y₀, subst ![Y₁, Y₂] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁)]
simp_rw :
  HAdd.hAdd (α := MvPowerSeries (Fin 3) R) (![subst ![Y₀, Y₁] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁), Y₂] 0)
      (![subst ![Y₀, Y₁] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁), Y₂] 1) =
    HAdd.hAdd (α := MvPowerSeries (Fin 3) R) (![Y₀, subst ![Y₁, Y₂] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁)] 0)
      (![Y₀, subst ![Y₁, Y₂] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁)] 1)
⊢ Eq (α := MvPowerSeries (Fin 3) R)
    (subst ![subst ![Y₀, Y₁] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁), Y₂]
      (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁))
    (subst ![Y₀, subst ![Y₁, Y₂] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁)]
      (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁))

Tactic:
simp_rw [subst_add aux₁, subst_X aux₁, subst_add aux₂, subst_X aux₂]

Premises used: MvPowerSeries.subst_add, MvPowerSeries.subst_X
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
aux₁ : HasSubst (τ := Fin 3) (S := R) ![subst ![Y₀, Y₁] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁), Y₂]
aux₂ : HasSubst (τ := Fin 3) (S := R) ![Y₀, subst ![Y₁, Y₂] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁)]
⊢ HAdd.hAdd (α := MvPowerSeries (Fin 3) R) (![subst ![Y₀, Y₁] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁), Y₂] 0)
      (![subst ![Y₀, Y₁] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁), Y₂] 1) =
    HAdd.hAdd (α := MvPowerSeries (Fin 3) R) (![Y₀, subst ![Y₁, Y₂] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁)] 0)
      (![Y₀, subst ![Y₁, Y₂] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁)] 1)

Tactic:
simp [subst_add .X_X, subst_X .X_X, add_assoc]

Premises used: MvPowerSeries.subst_add, add_assoc, MvPowerSeries.HasSubst.X_X, MvPowerSeries.subst_X
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
⊢ Eq.{u_1 + 1} (α := MvPowerSeries (Fin 2) R) (toPowerSeries 𝔾ₐ) (subst (R := R) ![X₁, X₀] (toPowerSeries 𝔾ₐ))

Tactic:
simp [subst_add .X_X, subst_X .X_X, add_comm]

Premises used: MvPowerSeries.subst_add, MvPowerSeries.HasSubst.X_X, add_comm, MvPowerSeries.subst_X
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
⊢ Eq (α := R)
    ((constantCoeff : (a : MvPowerSeries (Fin 2) R) → R)
        (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁) :
      R)
    (0 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
⊢ Eq (α := R)
    ((coeff (single 0 1) : (a : MvPowerSeries (Fin 2) R) → R)
        (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁) :
      R)
    (1 : R)

Tactic:
simp [X, monomial_mul_monomial, coeff_monomial, single_left_inj (one_ne_zero : (1 : ℕ) ≠ 0)]

Premises used: MvPowerSeries.X, MvPowerSeries.coeff_monomial, Finsupp.single_left_inj, MvPowerSeries.monomial_mul_monomial, one_ne_zero
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
⊢ Eq (α := R)
    ((coeff (single 1 1) : (a : MvPowerSeries (Fin 2) R) → R)
        (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁) :
      R)
    (1 : R)

Tactic:
simp [X, monomial_mul_monomial, coeff_monomial, single_left_inj (one_ne_zero : (1 : ℕ) ≠ 0)]

Premises used: MvPowerSeries.X, MvPowerSeries.coeff_monomial, Finsupp.single_left_inj, MvPowerSeries.monomial_mul_monomial, one_ne_zero
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
⊢ HasSubst (τ := Fin 3) (S := R)
    ![subst ![Y₀, Y₁] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁),
      Y₂]

Tactic:
obtain aux₁ := HasSubst.cons_subst_zero_left (f := X₀ + X₁ + X₀ * X₁) (0 : Fin 3) 1 2 (by simp)
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
aux₁ :
  HasSubst (τ := Fin 3) (S := R)
    ![subst ![Y₀, Y₁] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁),
      Y₂]
⊢ Eq (α := R)
    ((constantCoeff : (a : MvPowerSeries (Fin 2) R) → R)
        (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁) :
      R)
    (0 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
aux₁ :
  HasSubst (τ := Fin 3) (S := R)
    ![subst ![Y₀, Y₁] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁),
      Y₂]
⊢ HasSubst (τ := Fin 3) (S := R)
    ![Y₀,
      subst ![Y₁, Y₂] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁)]

Tactic:
obtain aux₂ := HasSubst.cons_subst_zero_right (f := X₀ + X₁ + X₀ * X₁) (0 : Fin 3) 1 2 (by simp)
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
aux₁ :
  HasSubst (τ := Fin 3) (S := R)
    ![subst ![Y₀, Y₁] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁),
      Y₂]
aux₂ :
  HasSubst (τ := Fin 3) (S := R)
    ![Y₀,
      subst ![Y₁, Y₂] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁)]
simp_rw :
  HAdd.hAdd (α := MvPowerSeries (Fin 3) R)
        (![subst ![Y₀, Y₁]
              (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁),
            Y₂]
          0)
        (![subst ![Y₀, Y₁]
              (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁),
            Y₂]
          1) +
      HMul.hMul (α := MvPowerSeries (Fin 3) R)
        (![subst ![Y₀, Y₁]
              (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁),
            Y₂]
          0)
        (![subst ![Y₀, Y₁]
              (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁),
            Y₂]
          1) =
    HAdd.hAdd (α := MvPowerSeries (Fin 3) R)
        (![Y₀,
            subst ![Y₁, Y₂]
              (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁)]
          0)
        (![Y₀,
            subst ![Y₁, Y₂]
              (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁)]
          1) +
      HMul.hMul (α := MvPowerSeries (Fin 3) R)
        (![Y₀,
            subst ![Y₁, Y₂]
              (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁)]
          0)
        (![Y₀,
            subst ![Y₁, Y₂]
              (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁)]
          1)
⊢ Eq (α := MvPowerSeries (Fin 3) R)
    (subst
      ![subst ![Y₀, Y₁]
          (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁),
        Y₂]
      (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁))
    (subst
      ![Y₀,
        subst ![Y₁, Y₂]
          (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁)]
      (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁))

Tactic:
simp_rw [subst_add aux₁, subst_mul aux₁, subst_X aux₁, subst_add aux₂, subst_mul aux₂,
      subst_X aux₂]

Premises used: MvPowerSeries.subst_add, MvPowerSeries.subst_mul, MvPowerSeries.subst_X
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
aux₁ :
  HasSubst (τ := Fin 3) (S := R)
    ![subst ![Y₀, Y₁] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁),
      Y₂]
aux₂ :
  HasSubst (τ := Fin 3) (S := R)
    ![Y₀,
      subst ![Y₁, Y₂] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁)]
simp :
  HAdd.hAdd (α := MvPowerSeries (Fin 3) R) Y₀ Y₁ + HMul.hMul (α := MvPowerSeries (Fin 3) R) Y₀ Y₁ + Y₂ +
      (HAdd.hAdd (α := MvPowerSeries (Fin 3) R) Y₀ Y₁ + HMul.hMul (α := MvPowerSeries (Fin 3) R) Y₀ Y₁) * Y₂ =
    Y₀ + (HAdd.hAdd (α := MvPowerSeries (Fin 3) R) Y₁ Y₂ + HMul.hMul (α := MvPowerSeries (Fin 3) R) Y₁ Y₂) +
      Y₀ * (HAdd.hAdd (α := MvPowerSeries (Fin 3) R) Y₁ Y₂ + HMul.hMul (α := MvPowerSeries (Fin 3) R) Y₁ Y₂)
⊢ HAdd.hAdd (α := MvPowerSeries (Fin 3) R)
        (![subst ![Y₀, Y₁]
              (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁),
            Y₂]
          0)
        (![subst ![Y₀, Y₁]
              (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁),
            Y₂]
          1) +
      HMul.hMul (α := MvPowerSeries (Fin 3) R)
        (![subst ![Y₀, Y₁]
              (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁),
            Y₂]
          0)
        (![subst ![Y₀, Y₁]
              (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁),
            Y₂]
          1) =
    HAdd.hAdd (α := MvPowerSeries (Fin 3) R)
        (![Y₀,
            subst ![Y₁, Y₂]
              (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁)]
          0)
        (![Y₀,
            subst ![Y₁, Y₂]
              (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁)]
          1) +
      HMul.hMul (α := MvPowerSeries (Fin 3) R)
        (![Y₀,
            subst ![Y₁, Y₂]
              (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁)]
          0)
        (![Y₀,
            subst ![Y₁, Y₂]
              (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁)]
          1)

Tactic:
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, subst_add .X_X, Fin.isValue, subst_X .X_X,
      Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one, subst_mul .X_X]

Premises used: MvPowerSeries.subst_add, Nat.succ_eq_add_one, Matrix.cons_val_one, Matrix.cons_val_zero, MvPowerSeries.HasSubst.X_X, MvPowerSeries.subst_mul, Nat.reduceAdd, Matrix.cons_val_fin_one, Fin.isValue, MvPowerSeries.subst_X
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
aux₁ :
  HasSubst (τ := Fin 3) (S := R)
    ![subst ![Y₀, Y₁] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁),
      Y₂]
aux₂ :
  HasSubst (τ := Fin 3) (S := R)
    ![Y₀,
      subst ![Y₁, Y₂] (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ + HMul.hMul (α := MvPowerSeries (Fin 2) R) X₀ X₁)]
⊢ HAdd.hAdd (α := MvPowerSeries (Fin 3) R) Y₀ Y₁ + HMul.hMul (α := MvPowerSeries (Fin 3) R) Y₀ Y₁ + Y₂ +
      (HAdd.hAdd (α := MvPowerSeries (Fin 3) R) Y₀ Y₁ + HMul.hMul (α := MvPowerSeries (Fin 3) R) Y₀ Y₁) * Y₂ =
    Y₀ + (HAdd.hAdd (α := MvPowerSeries (Fin 3) R) Y₁ Y₂ + HMul.hMul (α := MvPowerSeries (Fin 3) R) Y₁ Y₂) +
      Y₀ * (HAdd.hAdd (α := MvPowerSeries (Fin 3) R) Y₁ Y₂ + HMul.hMul (α := MvPowerSeries (Fin 3) R) Y₁ Y₂)

Tactic:
ring
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
⊢ Eq.{u_1 + 1} (α := MvPowerSeries (Fin 2) R) (toPowerSeries 𝔾ₘ) (subst (R := R) ![X₁, X₀] (toPowerSeries 𝔾ₘ))

Tactic:
simp [subst_add .X_X, subst_mul .X_X, subst_X .X_X, add_comm, mul_comm]

Premises used: MvPowerSeries.subst_add, MvPowerSeries.HasSubst.X_X, MvPowerSeries.subst_mul, add_comm, MvPowerSeries.subst_X, mul_comm
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
f : R →+* S
⊢ Eq.{u_2 + 1} (α := S)
    ((constantCoeff : (a : MvPowerSeries (Fin 2) S) → S)
        (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 2) R) (MvPowerSeries (Fin 2) S)) :
              (a : MvPowerSeries (Fin 2) R) → MvPowerSeries (Fin 2) S)
            F.toPowerSeries :
          MvPowerSeries (Fin 2) S) :
      S)
    (0 : S)

Tactic:
simp [constantCoeff_map, F.zero_constantCoeff, map_zero]

Premises used: FormalGroup.zero_constantCoeff, map_zero, MvPowerSeries.constantCoeff_map
-- Module: Mathlib.RingTheory.FormalGroup.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
τ : Type u_4
σ : Type
F : FormalGroup R
f : R →+* S
⊢ Eq.{u_2 + 1} (α := S)
    ((coeff (single 0 1) : (a : MvPowerSeries (Fin 2) S) → S)
        (((MvPowerSeries.map f : RingHom.{u_1, u_2} (MvPowerSeries (Fin 2) R) (MvPowerSeries (Fin 2) S)) :
              (a : MvPowerSeries (Fin 2) R) → MvPowerSeries (Fin 2) S)
            F.toPowerSeries :
          MvPowerSeries (Fin 2) S) :
      S)
    (1 : S)

Tactic:
simp [F.lin_coeff_X]

Premises used: FormalGroup.lin_coeff_X