awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
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 : Eq (α := Submodule R M) (torsion R M) ⊥
⊢ Flat R M
have rw : ∀ ⦃I : Ideal R⦄,
  I.FG → Function.Injective (α := ↥I ⊗[R] M) (β := M) (⇑(lift (lsmul R M ∘ₗ Submodule.subtype I)) : (a : ↥I ⊗[R] M) → M)
Tactic: rw [iff_lift_lsmul_comp_subtype_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
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 : Eq (α := Submodule R M) (torsion R M) ⊥
I : Ideal R
hFG : I.FG
⊢ Function.Injective (α := ↥I ⊗[R] M) (β := M) (⇑(lift (lsmul R M ∘ₗ Submodule.subtype I)) : (a : ↥I ⊗[R] M) → M)
have inl : ∀ (hFG : Ideal.FG.{u_1} (R := R) ⊥),
  Function.Injective (α := ↥⊥ ⊗[R] M) (β := M) (⇑(lift (lsmul R M ∘ₗ Submodule.subtype ⊥)) : (a : ↥⊥ ⊗[R] M) → M)
Tactic: obtain (rfl | h) := eq_or_ne I ⊥
Cleared hypotheses: I, hFG
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
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 : Eq (α := Submodule R M) (torsion R M) ⊥
I : Ideal R
hFG : I.FG
inl :
  ∀ (hFG : Ideal.FG.{u_1} (R := R) ⊥),
    Function.Injective (α := ↥⊥ ⊗[R] M) (β := M) (⇑(lift (lsmul R M ∘ₗ Submodule.subtype ⊥)) : (a : ↥⊥ ⊗[R] M) → M)
⊢ Function.Injective (α := ↥I ⊗[R] M) (β := M) (⇑(lift (lsmul R M ∘ₗ Submodule.subtype I)) : (a : ↥I ⊗[R] M) → M)
have inr : ∀ (h : I ≠ ⊥),
  Function.Injective (α := ↥I ⊗[R] M) (β := M) (⇑(lift (lsmul R M ∘ₗ Submodule.subtype I)) : (a : ↥I ⊗[R] M) → M)
Tactic: obtain (rfl | h) := eq_or_ne I ⊥
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (hypothesis)
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 : Eq (α := Submodule R M) (torsion R M) ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
⊢ Function.Injective (α := ↥I ⊗[R] M) (β := M) (⇑(lift (lsmul R M ∘ₗ Submodule.subtype I)) : (a : ↥I ⊗[R] M) → M)
have hprinc : Submodule.IsPrincipal I
Tactic: have hprinc : I.IsPrincipal := IsBezout.isPrincipal_of_FG I hFG
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
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 : Eq (α := Submodule R M) (torsion R M) ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
⊢ IsPrincipal.generator I ≠ 0
have rwa : ¬IsPrincipal.generator I = 0
Tactic: rwa [ne_eq, ← IsPrincipal.eq_bot_iff_generator_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
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 : Eq (α := Submodule R M) (torsion R M) ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
rwa : ¬IsPrincipal.generator I = 0
⊢ IsPrincipal.generator I ≠ 0
have rwa₁ : ¬I = ⊥
Tactic: rwa [ne_eq, ← IsPrincipal.eq_bot_iff_generator_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (hypothesis)
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 : Eq (α := Submodule R M) (torsion R M) ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
⊢ Function.Injective (α := ↥I ⊗[R] M) (β := M) (⇑(lift (lsmul R M ∘ₗ Submodule.subtype I)) : (a : ↥I ⊗[R] M) → M)
have this : IsPrincipal.generator I ≠ 0
Tactic: have : IsPrincipal.generator I ≠ 0 := by
      rwa [ne_eq, ← IsPrincipal.eq_bot_iff_generator_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
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 : Eq (α := Submodule R M) (torsion R M) ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
⊢ Function.Injective (α := ↥I ⊗[R] M) (β := M) (⇑(lift (lsmul R M ∘ₗ Submodule.subtype I)) : (a : ↥I ⊗[R] M) → M)
have apply : Function.Injective (α := R ⊗[R] M) (β := M)
  (Function.comp (β := ↥I ⊗[R] M) (⇑(lift (lsmul R M ∘ₗ Submodule.subtype I)) : (a : ↥I ⊗[R] M) → M)
    (⇑(LinearEquiv.rTensor M (Ideal.isoBaseOfIsPrincipal h)) : (a : R ⊗[R] M) → ↥I ⊗[R] M))
Tactic: apply Function.Injective.of_comp_right _
      (LinearEquiv.rTensor M (Ideal.isoBaseOfIsPrincipal h)).surjective
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
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 : Eq (α := Submodule R M) (torsion R M) ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
⊢ Function.Injective (α := R ⊗[R] M) (β := M)
    (Function.comp (β := ↥I ⊗[R] M) (⇑(lift (lsmul R M ∘ₗ Submodule.subtype I)) : (a : ↥I ⊗[R] M) → M)
      (⇑(LinearEquiv.rTensor M (Ideal.isoBaseOfIsPrincipal h)) : (a : R ⊗[R] M) → ↥I ⊗[R] M))
have rw : Function.Injective (α := R ⊗[R] M) (β := M)
  (Function.comp (β := M) (⇑((lsmul R M : (a : R) → M →ₗ[R] M) (IsPrincipal.generator I) : M →ₗ[R] M) : (a : M) → M)
    (⇑(lift (lsmul R M)) : (a : R ⊗[R] M) → M))
Tactic: rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.coe_comp, LinearEquiv.coe_rTensor, rTensor,
      lift_comp_map, LinearMap.compl₂_id, LinearMap.comp_assoc,
      Ideal.subtype_isoBaseOfIsPrincipal_eq_mul, LinearMap.lift_lsmul_mul_eq_lsmul_lift_lsmul,
      LinearMap.coe_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
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 : Eq (α := Submodule R M) (torsion R M) ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
⊢ Function.Injective (α := R ⊗[R] M) (β := M)
    (Function.comp (β := M) (⇑((lsmul R M : (a : R) → M →ₗ[R] M) (IsPrincipal.generator I) : M →ₗ[R] M) : (a : M) → M)
      (⇑(lift (lsmul R M)) : (a : R ⊗[R] M) → M))
have rw : ∀ (htors : IsTorsionFree R M) ⦃I : Ideal R⦄ (hFG : I.FG) (h : I ≠ ⊥) (hprinc : Submodule.IsPrincipal I)
  (this : IsPrincipal.generator I ≠ 0),
  Function.Injective (α := R ⊗[R] M) (β := M)
    (Function.comp (β := M) (⇑((lsmul R M : (a : R) → M →ₗ[R] M) (IsPrincipal.generator I) : M →ₗ[R] M) : (a : M) → M)
      (⇑(lift (lsmul R M)) : (a : R ⊗[R] M) → M))
Tactic: rw [← Submodule.isTorsionFree_iff_torsion_eq_bot] at htors
Cleared hypotheses: htors, I, hFG, h, hprinc, this
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
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
⊢ Function.Injective (α := R ⊗[R] M) (β := M)
    (Function.comp (β := M) (⇑((lsmul R M : (a : R) → M →ₗ[R] M) (IsPrincipal.generator I) : M →ₗ[R] M) : (a : M) → M)
      (⇑(lift (lsmul R M)) : (a : R ⊗[R] M) → M))
have refine : Function.Injective (α := R ⊗[R] M) (β := M) (⇑(lift (lsmul R M)) : (a : R ⊗[R] M) → M)
Tactic: refine Function.Injective.comp (LinearMap.lsmul_injective this) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
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
⊢ Function.Injective (α := R ⊗[R] M) (β := M) (⇑(lift (lsmul R M)) : (a : R ⊗[R] M) → M)
have rw : 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: rw [← Equiv.injective_comp (TensorProduct.lid R M).symm.toEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
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
⊢ 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))
have 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
Tactic: convert! Function.injective_id
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
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
⊢ 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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
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) ⊥
have refine : ∀ (h : Eq (α := Submodule R M) (torsion R M) ⊥), Flat R M
Tactic: refine ⟨fun _ ↦ Flat.torsion_eq_bot, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
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) ⊥
⊢ Flat R M
have h₁ : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], Flat R (LocalizedModule P.primeCompl M)
Tactic: apply flat_of_localized_maximal
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
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
⊢ Flat R (LocalizedModule P.primeCompl M)
have h₁ : ∀ (h : IsTorsionFree R M) (P : Ideal R) [hP : P.IsMaximal], Flat R (LocalizedModule P.primeCompl M)
Tactic: rw [← Submodule.isTorsionFree_iff_torsion_eq_bot] at h
Cleared hypotheses: h, P, hP
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
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
⊢ Flat R (LocalizedModule P.primeCompl M)
have h₁ : IsTorsionFree (Localization (M := R) P.primeCompl) (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]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
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
⊢ Flat R M ↔ Eq (α := Submodule R M) (torsion R M) ⊥
have h : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], ValuationRing.{u_1} (Localization (M := R) P.primeCompl)
Tactic: apply flat_iff_torsion_eq_bot_of_valuationRing_localization_isMaximal
-- Lean 4 proof step from Mathlib.RingTheory.FormalGroup.Basic (hypothesis)
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 (α := 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₁))
have aux₁ : 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)
-- Lean 4 proof step from Mathlib.RingTheory.FormalGroup.Basic (hypothesis)
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 (α := 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₁))
have aux₂ : 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)
-- Lean 4 proof step from Mathlib.RingTheory.FormalGroup.Basic (goal)
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₁)]
⊢ 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₁))
have 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)
Tactic: simp_rw [subst_add aux₁, subst_X aux₁, subst_add aux₂, subst_X aux₂]
-- Lean 4 proof step from Mathlib.RingTheory.FormalGroup.Basic (hypothesis)
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 (α := 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₁))
have 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₂]
Tactic: obtain aux₁ := HasSubst.cons_subst_zero_left (f := X₀ + X₁ + X₀ * X₁) (0 : Fin 3) 1 2 (by simp)
-- Lean 4 proof step from Mathlib.RingTheory.FormalGroup.Basic (hypothesis)
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 (α := 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₁))
have 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₁)]
Tactic: obtain aux₂ := HasSubst.cons_subst_zero_right (f := X₀ + X₁ + X₀ * X₁) (0 : Fin 3) 1 2 (by simp)
-- Lean 4 proof step from Mathlib.RingTheory.FormalGroup.Basic (goal)
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₁)]
⊢ 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₁))
have 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)
Tactic: simp_rw [subst_add aux₁, subst_mul aux₁, subst_X aux₁, subst_add aux₂, subst_mul aux₂,
      subst_X aux₂]
-- Lean 4 proof step from Mathlib.RingTheory.FormalGroup.Basic (goal)
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)
        (![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)
have 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₂)
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]