awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
x : R
⊢ Eq (α := Ring (R := T) (S := T ⊗[R] S) P.baseChange)
    ((algebraMap R (Ring (R := T) (S := T ⊗[R] S) P.baseChange) : (a : R) → P.baseChange.Ring) x :
      Ring (R := T) (S := T ⊗[R] S) P.baseChange)
    ((algebraMap P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) : (a : P.Ring) → P.baseChange.Ring)
        ((algebraMap R P.Ring : (a : R) → P.Ring) x) :
      Ring (R := T) (S := T ⊗[R] S) P.baseChange)
have simp : Eq (α := TensorProduct.{u, u_1, w} R T P.Ring)
  ((algebraMap R (TensorProduct.{u, u_1, w} R T P.Ring) : (a : R) → T ⊗[R] P.Ring) x :
    TensorProduct.{u, u_1, w} R T P.Ring)
  ((algebraMap R T : (a : R) → T) x ⊗ₜ[R] 1 : TensorProduct.{u, u_1, w} R T P.Ring)
Tactic: simp [baseChange, RingHom.algebraMap_toAlgebra]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
⊢ (Hom.id P).toAlgHom = AlgHom.id R P.Ring
have H : ∀ (x : P.Ring),
  Eq (α := P.Ring) (((Hom.id P).toAlgHom : (a : P.Ring) → P.Ring) x : P.Ring)
    ((AlgHom.id R P.Ring : (a : P.Ring) → P.Ring) x : P.Ring)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u_1
S' : Type u_2
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{u_3, u_1, u_2} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
f : P.Hom P'
⊢ f.comp (Hom.id P) = f
have toRingHom : ∀ (x : P.Ring),
  Eq.{u_3 + 1} (α := P'.Ring) ((toRingHom (f.comp (Hom.id P)) : (a : P.Ring) → P'.Ring) x : P'.Ring)
    ((f.toRingHom : (a : P.Ring) → P'.Ring) x : P'.Ring)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u_1
S' : Type u_2
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{u_3, u_1, u_2} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
f : P.Hom P'
⊢ (Hom.id P').comp f = f
have toRingHom : ∀ (x : P.Ring),
  Eq.{u_3 + 1} (α := P'.Ring) ((toRingHom ((Hom.id P').comp f) : (a : P.Ring) → P'.Ring) x : P'.Ring)
    ((f.toRingHom : (a : P.Ring) → P'.Ring) x : P'.Ring)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
R' : Type ?u.217031
S' : Type ?u.217034
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.217158
S'' : Type ?u.217161
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
P : Extension.{u_1, u, v} R S
x : S
⊢ (algebraMap (P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2) S : (a : P.Ring ⧸ P.ker ^ 2) → S)
      (((⇑(Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2)) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) ∘ P.σ) x) =
    x
have dsimp : (algebraMap (P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2) S : (a : P.Ring ⧸ P.ker ^ 2) → S)
    ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ x) :
      P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2) =
  x
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type ?u.238586
S' : Type ?u.238589
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.238713
S'' : Type ?u.238716
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
r s : S
x : P.Cotangent
⊢ (r * s) • x = r • s • x
have this : (P.σ (r * s) - P.σ r * P.σ s) • x = 0
Tactic: have := smul_eq_zero_of_mem (P.σ (r * s) - (P.σ r * P.σ s) : P.Ring) (by simp) x
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type ?u.238586
S' : Type ?u.238589
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.238713
S'' : Type ?u.238716
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
x : P.Cotangent
⊢ HSMul.hSMul.{v, w, w} (α := S) 1 x = x
have this : (P.σ 1 - 1) • x = 0
Tactic: have := smul_eq_zero_of_mem (P.σ 1 - 1 : P.Ring) (by simp) x
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type ?u.238586
S' : Type ?u.238589
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.238713
S'' : Type ?u.238716
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
r s : S
x : P.Cotangent
⊢ (r + s) • x = r • x + s • x
have this : (P.σ (r + s) - (P.σ r + P.σ s)) • x = 0
Tactic: have := smul_eq_zero_of_mem (P.σ (r + s) - (P.σ r + P.σ s) : P.Ring) (by simp) x
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type ?u.279762
S' : Type ?u.279765
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.279889
S'' : Type ?u.279892
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
R₁ : Type u_1
R₂ : Type u_2
inst_9 : CommRing R₁
inst_10 : CommRing R₂
inst_11 : Algebra R₁ S
inst_12 : Algebra R₂ S
inst_13 : Algebra R₁ R₂
inst_14 : IsScalarTower R₁ R₂ S
⊢ IsScalarTower.{u_1, u_2, w} R₁ R₂ P.Cotangent
have smul_assoc : ∀ (x : R₁) (y : R₂) (z : P.Cotangent), (x • y) • z = x • y • z
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type ?u.279762
S' : Type ?u.279765
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.279889
S'' : Type ?u.279892
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
R₁ : Type u_1
R₂ : Type u_2
inst_9 : CommRing R₁
inst_10 : CommRing R₂
inst_11 : Algebra R₁ S
inst_12 : Algebra R₂ S
inst_13 : Algebra R₁ R₂
inst_14 : IsScalarTower R₁ R₂ S
r : R₁
s : R₂
m : P.Cotangent
⊢ (r • s) • m = r • s • m
have smul_assoc : HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) (r • s) : S) m =
  HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
    (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
Tactic: change algebraMap R₂ S (r • s) • m = (algebraMap _ S r) • (algebraMap _ S s) • m
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type ?u.279762
S' : Type ?u.279765
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.279889
S'' : Type ?u.279892
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
R₁ : Type u_1
R₂ : Type u_2
inst_9 : CommRing R₁
inst_10 : CommRing R₂
inst_11 : Algebra R₁ S
inst_12 : Algebra R₂ S
inst_13 : Algebra R₁ R₂
inst_14 : IsScalarTower R₁ R₂ S
r : R₁
s : R₂
m : P.Cotangent
⊢ HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) (r • s) : S) m =
    HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
      (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
have smul_assoc : HSMul.hSMul.{v, w, w} (α := S)
    ((algebraMap R₂ S : (a : R₂) → S) (HMul.hMul (α := R₂) ((algebraMap R₁ R₂ : (a : R₁) → R₂) r : R₂) s) : S) m =
  HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
    (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
Tactic: rw [Algebra.smul_def, map_mul, mul_smul, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type ?u.279762
S' : Type ?u.279765
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.279889
S'' : Type ?u.279892
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
R₁ : Type u_1
R₂ : Type u_2
inst_9 : CommRing R₁
inst_10 : CommRing R₂
inst_11 : Algebra R₁ S
inst_12 : Algebra R₂ S
inst_13 : Algebra R₁ R₂
inst_14 : IsScalarTower R₁ R₂ S
r : R₁
s : R₂
m : P.Cotangent
smul_assoc :
  HSMul.hSMul.{v, w, w} (α := S)
      ((algebraMap R₂ S : (a : R₂) → S) (HMul.hMul (α := R₂) ((algebraMap R₁ R₂ : (a : R₁) → R₂) r : R₂) s) : S) m =
    HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
      (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
⊢ HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) (r • s) : S) m =
    HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
      (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
have smul_assoc₁ : HMul.hMul (α := S) (β := S) ((algebraMap R₂ S : (a : R₂) → S) ((algebraMap R₁ R₂ : (a : R₁) → R₂) r : R₂) : S)
      ((algebraMap R₂ S : (a : R₂) → S) s : S) •
    m =
  HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
    (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
Tactic: rw [Algebra.smul_def, map_mul, mul_smul, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type ?u.279762
S' : Type ?u.279765
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.279889
S'' : Type ?u.279892
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
R₁ : Type u_1
R₂ : Type u_2
inst_9 : CommRing R₁
inst_10 : CommRing R₂
inst_11 : Algebra R₁ S
inst_12 : Algebra R₂ S
inst_13 : Algebra R₁ R₂
inst_14 : IsScalarTower R₁ R₂ S
r : R₁
s : R₂
m : P.Cotangent
smul_assoc :
  HSMul.hSMul.{v, w, w} (α := S)
      ((algebraMap R₂ S : (a : R₂) → S) (HMul.hMul (α := R₂) ((algebraMap R₁ R₂ : (a : R₁) → R₂) r : R₂) s) : S) m =
    HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
      (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
smul_assoc₁ :
  HMul.hMul (α := S) (β := S) ((algebraMap R₂ S : (a : R₂) → S) ((algebraMap R₁ R₂ : (a : R₁) → R₂) r : R₂) : S)
        ((algebraMap R₂ S : (a : R₂) → S) s : S) •
      m =
    HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
      (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
⊢ HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) (r • s) : S) m =
    HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
      (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
have smul_assoc₂ : HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) ((algebraMap R₁ R₂ : (a : R₁) → R₂) r : R₂) : S)
    (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m) =
  HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
    (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
Tactic: rw [Algebra.smul_def, map_mul, mul_smul, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type ?u.279762
S' : Type ?u.279765
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.279889
S'' : Type ?u.279892
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
R₁ : Type u_1
R₂ : Type u_2
inst_9 : CommRing R₁
inst_10 : CommRing R₂
inst_11 : Algebra R₁ S
inst_12 : Algebra R₂ S
inst_13 : Algebra R₁ R₂
inst_14 : IsScalarTower R₁ R₂ S
r : R₁
s : R₂
m : P.Cotangent
smul_assoc :
  HSMul.hSMul.{v, w, w} (α := S)
      ((algebraMap R₂ S : (a : R₂) → S) (HMul.hMul (α := R₂) ((algebraMap R₁ R₂ : (a : R₁) → R₂) r : R₂) s) : S) m =
    HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
      (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
smul_assoc₁ :
  HMul.hMul (α := S) (β := S) ((algebraMap R₂ S : (a : R₂) → S) ((algebraMap R₁ R₂ : (a : R₁) → R₂) r : R₂) : S)
        ((algebraMap R₂ S : (a : R₂) → S) s : S) •
      m =
    HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
      (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
smul_assoc₂ :
  HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) ((algebraMap R₁ R₂ : (a : R₁) → R₂) r : R₂) : S)
      (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m) =
    HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
      (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
⊢ HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) (r • s) : S) m =
    HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
      (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
have smul_assoc₃ : HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
    (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m) =
  HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
    (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
Tactic: rw [Algebra.smul_def, map_mul, mul_smul, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
r : P.Ring
x : P.Cotangent
⊢ (r • x).val = r • x.val
have rw : (P.σ ((algebraMap P.Ring S : (a : P.Ring) → S) r) - r) • x.val = 0
Tactic: rw [val_smul''', ← sub_eq_zero, ← sub_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
r : R
x : P.Cotangent
⊢ (r • x).val = r • x.val
have rw : (HSMul.hSMul (α := P.Ring) ((algebraMap R P.Ring : (a : R) → P.Ring) r : P.Ring) x).val = r • x.val
Tactic: rw [← algebraMap_smul P.Ring, val_smul', algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
r : R
x : P.Cotangent
rw : (HSMul.hSMul (α := P.Ring) ((algebraMap R P.Ring : (a : R) → P.Ring) r : P.Ring) x).val = r • x.val
⊢ (r • x).val = r • x.val
have rw₁ : HSMul.hSMul (α := P.Ring) ((algebraMap R P.Ring : (a : R) → P.Ring) r : P.Ring) x.val = r • x.val
Tactic: rw [← algebraMap_smul P.Ring, val_smul', algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
r : R
x : P.Cotangent
rw : (HSMul.hSMul (α := P.Ring) ((algebraMap R P.Ring : (a : R) → P.Ring) r : P.Ring) x).val = r • x.val
rw₁ : HSMul.hSMul (α := P.Ring) ((algebraMap R P.Ring : (a : R) → P.Ring) r : P.Ring) x.val = r • x.val
⊢ (r • x).val = r • x.val
have rw₂ : r • x.val = r • x.val
Tactic: rw [← algebraMap_smul P.Ring, val_smul', algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
⊢ LinearMap.ker mk = HSMul.hSMul (β := Submodule P.Ring ↥P.ker) P.ker ⊤
have h : ∀ (x : P.Ring) (hx : x ∈ P.ker),
  Membership.mem (γ := Submodule P.Ring ↥P.ker) (LinearMap.ker mk)
      (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) x hx) ↔
    Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) x hx ∈ HSMul.hSMul (β := Submodule P.Ring ↥P.ker) P.ker ⊤
Tactic: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
ι : Type u_1
s : ι → P.Ring
hs : Ideal.span (Set.range s) = P.ker
⊢ Eq.{w + 1} (α := Submodule S P.Cotangent)
    (Submodule.span S
      (Set.range fun (i : ι) ↦
        (mk : (a : ↥P.ker) → P.Cotangent) (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)))
    ⊤
have rw : ∀ (hs_1 : Submodule.span P.Ring (Set.range s) = P.ker)
  (hs_2 :
    Eq.{w + 1} (α := Submodule P.Ring ↥P.ker)
      (Submodule.span P.Ring (Set.range fun (i : ι) ↦ Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) sorry)) ⊤),
  Eq.{w + 1} (α := Submodule S P.Cotangent)
    (Submodule.span S
      (Set.range fun (i : ι) ↦
        (mk : (a : ↥P.ker) → P.Cotangent) (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) sorry)))
    ⊤
Tactic: rw [Ideal.span, ← Submodule.span_range_subtype_eq_top_iff] at hs
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
ι : Type u_1
s : ι → P.Ring
hs : Ideal.span (Set.range s) = P.ker
rw :
  ∀ (hs_1 : Submodule.span P.Ring (Set.range s) = P.ker)
    (hs_2 :
      Eq.{w + 1} (α := Submodule P.Ring ↥P.ker)
        (Submodule.span P.Ring (Set.range fun (i : ι) ↦ Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)) ⊤),
    Eq.{w + 1} (α := Submodule S P.Cotangent)
      (Submodule.span S
        (Set.range fun (i : ι) ↦
          (mk : (a : ↥P.ker) → P.Cotangent) (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)))
      ⊤
⊢ Eq.{w + 1} (α := Submodule S P.Cotangent)
    (Submodule.span S
      (Set.range fun (i : ι) ↦
        (mk : (a : ↥P.ker) → P.Cotangent) (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)))
    ⊤
have hs₁ : ∀ (hs : Submodule.span P.Ring (Set.range s) = P.ker) (i : ι), s i ∈ P.ker
Tactic: rw [Ideal.span, ← Submodule.span_range_subtype_eq_top_iff] at hs
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
ι : Type u_1
s : ι → P.Ring
hs_1 : Ideal.span (Set.range s) = P.ker
hs_2 : Submodule.span P.Ring (Set.range s) = P.ker
hs :
  Eq.{w + 1} (α := Submodule P.Ring ↥P.ker)
    (Submodule.span P.Ring (Set.range fun (i : ι) ↦ Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)) ⊤
⊢ Eq.{w + 1} (α := Submodule S P.Cotangent)
    (Submodule.span S
      (Set.range fun (i : ι) ↦
        (mk : (a : ↥P.ker) → P.Cotangent) (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)))
    ⊤
have hs₁ : Eq.{w + 1} (α := Submodule P.Ring P.Cotangent)
  (Submodule.span P.Ring
    (Set.range fun (i : ι) ↦
      (mk : (a : ↥P.ker) → P.Cotangent) (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) sorry)))
  ⊤
Tactic: apply Submodule.span_eq_top_of_span_eq_top (R := P.Ring)
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
ι : Type u_1
s : ι → P.Ring
hs_1 : Ideal.span (Set.range s) = P.ker
hs_2 : Submodule.span P.Ring (Set.range s) = P.ker
hs :
  Eq.{w + 1} (α := Submodule P.Ring ↥P.ker)
    (Submodule.span P.Ring (Set.range fun (i : ι) ↦ Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)) ⊤
⊢ Eq.{w + 1} (α := Submodule P.Ring P.Cotangent)
    (Submodule.span P.Ring
      (Set.range fun (i : ι) ↦
        (mk : (a : ↥P.ker) → P.Cotangent) (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)))
    ⊤
have hs₁ : Eq.{w + 1} (α := Submodule P.Ring P.Cotangent)
  (Submodule.span P.Ring
    (Set.range.{w, u_1 + 1} (ι := ι)
      (Function.comp (β := ↥P.ker) (⇑mk : (a : ↥P.ker) → P.Cotangent) fun (i : ι) ↦
        Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) sorry)))
  ⊤
Tactic: rw [← Function.comp_def, Set.range_comp, ← Submodule.map_span, hs, Submodule.map_top,
      LinearMap.range_eq_top_of_surjective _ mk_surjective]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
ι : Type u_1
s : ι → P.Ring
hs_1 : Ideal.span (Set.range s) = P.ker
hs_2 : Submodule.span P.Ring (Set.range s) = P.ker
hs :
  Eq.{w + 1} (α := Submodule P.Ring ↥P.ker)
    (Submodule.span P.Ring (Set.range fun (i : ι) ↦ Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)) ⊤
hs₁ :
  Eq.{w + 1} (α := Submodule P.Ring P.Cotangent)
    (Submodule.span P.Ring
      (Set.range.{w, u_1 + 1} (ι := ι)
        (Function.comp (β := ↥P.ker) (⇑mk : (a : ↥P.ker) → P.Cotangent) fun (i : ι) ↦
          Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)))
    ⊤
⊢ Eq.{w + 1} (α := Submodule P.Ring P.Cotangent)
    (Submodule.span P.Ring
      (Set.range fun (i : ι) ↦
        (mk : (a : ↥P.ker) → P.Cotangent) (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)))
    ⊤
have hs₂ : Eq.{w + 1} (α := Submodule P.Ring P.Cotangent)
  (Submodule.span P.Ring
    (Set.image (α := ↥P.ker) (⇑mk : (a : ↥P.ker) → P.Cotangent)
      (Set.range fun (i : ι) ↦ Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) sorry)))
  ⊤
Tactic: rw [← Function.comp_def, Set.range_comp, ← Submodule.map_span, hs, Submodule.map_top,
      LinearMap.range_eq_top_of_surjective _ mk_surjective]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
ι : Type u_1
s : ι → P.Ring
hs_1 : Ideal.span (Set.range s) = P.ker
hs_2 : Submodule.span P.Ring (Set.range s) = P.ker
hs :
  Eq.{w + 1} (α := Submodule P.Ring ↥P.ker)
    (Submodule.span P.Ring (Set.range fun (i : ι) ↦ Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)) ⊤
hs₁ :
  Eq.{w + 1} (α := Submodule P.Ring P.Cotangent)
    (Submodule.span P.Ring
      (Set.range.{w, u_1 + 1} (ι := ι)
        (Function.comp (β := ↥P.ker) (⇑mk : (a : ↥P.ker) → P.Cotangent) fun (i : ι) ↦
          Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)))
    ⊤
hs₂ :
  Eq.{w + 1} (α := Submodule P.Ring P.Cotangent)
    (Submodule.span P.Ring
      (Set.image (α := ↥P.ker) (⇑mk : (a : ↥P.ker) → P.Cotangent)
        (Set.range fun (i : ι) ↦ Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)))
    ⊤
⊢ Eq.{w + 1} (α := Submodule P.Ring P.Cotangent)
    (Submodule.span P.Ring
      (Set.range fun (i : ι) ↦
        (mk : (a : ↥P.ker) → P.Cotangent) (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)))
    ⊤
have hs₃ : Eq.{w + 1} (α := Submodule P.Ring P.Cotangent)
  (Submodule.map mk
    (Submodule.span P.Ring (Set.range fun (i : ι) ↦ Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) sorry)))
  ⊤
Tactic: rw [← Function.comp_def, Set.range_comp, ← Submodule.map_span, hs, Submodule.map_top,
      LinearMap.range_eq_top_of_surjective _ mk_surjective]