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
ι : 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) ⋯)))
    ⊤
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) ⋯)))
    ⊤
⊢ 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 ⊤) ⊤
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) ⋯)))
    ⊤
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) ⋯)))
    ⊤
hs₄ : Eq.{w + 1} (α := Submodule P.Ring P.Cotangent) (Submodule.map mk ⊤) ⊤
⊢ 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) (LinearMap.range mk) ⊤
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) ⋯)))
    ⊤
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) ⋯)))
    ⊤
hs₄ : Eq.{w + 1} (α := Submodule P.Ring P.Cotangent) (Submodule.map mk ⊤) ⊤
hs₅ : Eq.{w + 1} (α := Submodule P.Ring P.Cotangent) (LinearMap.range mk) ⊤
⊢ 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) ⊤ ⊤
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
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'
R'' : Type ?u.337215
S'' : Type ?u.337218
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : Algebra R S'
inst_16 : IsScalarTower R R' S'
f : P.Hom P'
r : S
x : P.Cotangent
⊢ val
      (of
        (((P.ker.mapCotangent P'.ker f.toAlgHom ⋯ :
              LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
            (a : P.ker.Cotangent) → P'.ker.Cotangent)
          (r • x).val)) =
    (HSMul.hSMul (α := S) (β := P'.Cotangent) ((RingHom.id S : (a : S) → S) r : S)
        (of
          (((P.ker.mapCotangent P'.ker f.toAlgHom ⋯ :
                LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
              (a : P.ker.Cotangent) → P'.ker.Cotangent)
            x.val))).val
have e : ∀ (x : ↥P.ker),
  val
      (of
        (((P.ker.mapCotangent P'.ker f.toAlgHom sorry :
              LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
            (a : P.ker.Cotangent) → P'.ker.Cotangent)
          (HSMul.hSMul (β := P.Cotangent) r ((mk : (a : ↥P.ker) → P.Cotangent) x : P.Cotangent)).val)) =
    (HSMul.hSMul (α := S) (β := P'.Cotangent) ((RingHom.id S : (a : S) → S) r : S)
        (of
          (((P.ker.mapCotangent P'.ker f.toAlgHom sorry :
                LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
              (a : P.ker.Cotangent) → P'.ker.Cotangent)
            (val ((mk : (a : ↥P.ker) → P.Cotangent) x))))).val
Tactic: obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
Cleared hypotheses: 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_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'
R'' : Type ?u.337215
S'' : Type ?u.337218
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : Algebra R S'
inst_16 : IsScalarTower R R' S'
f : P.Hom P'
r : S
x : ↥P.ker
⊢ val
      (of
        (((P.ker.mapCotangent P'.ker f.toAlgHom ⋯ :
              LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
            (a : P.ker.Cotangent) → P'.ker.Cotangent)
          (HSMul.hSMul (β := P.Cotangent) r ((mk : (a : ↥P.ker) → P.Cotangent) x : P.Cotangent)).val)) =
    (HSMul.hSMul (α := S) (β := P'.Cotangent) ((RingHom.id S : (a : S) → S) r : S)
        (of
          (((P.ker.mapCotangent P'.ker f.toAlgHom ⋯ :
                LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
              (a : P.ker.Cotangent) → P'.ker.Cotangent)
            (val ((mk : (a : ↥P.ker) → P.Cotangent) x))))).val
have e : ∀ (r : P.Ring),
  val
      (of
        (((P.ker.mapCotangent P'.ker f.toAlgHom sorry :
              LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
            (a : P.ker.Cotangent) → P'.ker.Cotangent)
          (HSMul.hSMul.{v, w, w} (α := S) (β := P.Cotangent) ((algebraMap P.Ring S : (a : P.Ring) → S) r : S)
              ((mk : (a : ↥P.ker) → P.Cotangent) x : P.Cotangent)).val)) =
    (HSMul.hSMul (α := S) (β := P'.Cotangent)
        ((RingHom.id S : (a : S) → S) ((algebraMap P.Ring S : (a : P.Ring) → S) r : S) : S)
        (of
          (((P.ker.mapCotangent P'.ker f.toAlgHom sorry :
                LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
              (a : P.ker.Cotangent) → P'.ker.Cotangent)
            (val ((mk : (a : ↥P.ker) → P.Cotangent) x))))).val
Tactic: obtain ⟨r, rfl⟩ := P.algebraMap_surjective r
Cleared hypotheses: r
-- 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'
R'' : Type ?u.337215
S'' : Type ?u.337218
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : Algebra R S'
inst_16 : IsScalarTower R R' S'
f : P.Hom P'
x : ↥P.ker
r : P.Ring
⊢ val
      (of
        (((P.ker.mapCotangent P'.ker f.toAlgHom ⋯ :
              LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
            (a : P.ker.Cotangent) → P'.ker.Cotangent)
          (HSMul.hSMul.{v, w, w} (α := S) (β := P.Cotangent) ((algebraMap P.Ring S : (a : P.Ring) → S) r : S)
              ((mk : (a : ↥P.ker) → P.Cotangent) x : P.Cotangent)).val)) =
    (HSMul.hSMul (α := S) (β := P'.Cotangent)
        ((RingHom.id S : (a : S) → S) ((algebraMap P.Ring S : (a : P.Ring) → S) r : S) : S)
        (of
          (((P.ker.mapCotangent P'.ker f.toAlgHom ⋯ :
                LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
              (a : P.ker.Cotangent) → P'.ker.Cotangent)
            (val ((mk : (a : ↥P.ker) → P.Cotangent) x))))).val
have e : (P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
    (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
      (((f.toAlgHom : AlgHom.{u, w, u_3} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑(r • x) : P.Ring)) sorry) =
  (HSMul.hSMul.{v, u_3, u_3} (α := S) (β := P'.Cotangent) ((algebraMap P.Ring S : (a : P.Ring) → S) r : S)
      (of
        ((P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
          (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
            (((f.toAlgHom : AlgHom.{u, w, u_3} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) sorry)))).val
Tactic: simp only [algebraMap_smul, val_smul', val_mk, val_of, Ideal.mapCotangent_toCotangent,
      RingHomCompTriple.comp_apply, ← (Ideal.toCotangent _).map_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' : 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'
R'' : Type ?u.337215
S'' : Type ?u.337218
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : Algebra R S'
inst_16 : IsScalarTower R R' S'
f : P.Hom P'
x : ↥P.ker
r : P.Ring
| (HSMul.hSMul.{v, u_3, u_3} (α := S) (β := P'.Cotangent) ((algebraMap P.Ring S : (a : P.Ring) → S) r : S)
      (of
        ((P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
          (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
            (((f.toAlgHom : AlgHom.{u, w, u_3} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯)))).val
have rw : ((P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
    (HSMul.hSMul (α := P'.Ring) (β := ↥P'.ker) ((f.toRingHom : (a : P.Ring) → P'.Ring) r : P'.Ring)
      (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
          (((f.toAlgHom : AlgHom.{u, w, u_3} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) sorry :
        ↥P'.ker)) :
  P'.ker.Cotangent)
Tactic: rw [← algebraMap_smul S', ← f.algebraMap_toRingHom, algebraMap_smul, val_smul',
      val_of, ← (Ideal.toCotangent _).map_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' : 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'
R'' : Type ?u.337215
S'' : Type ?u.337218
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : Algebra R S'
inst_16 : IsScalarTower R R' S'
f : P.Hom P'
x : ↥P.ker
r : P.Ring
⊢ (P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
      (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
        (((f.toAlgHom : AlgHom.{u, w, u_3} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑(r • x) : P.Ring)) ⋯) =
    (HSMul.hSMul.{v, u_3, u_3} (α := S) (β := P'.Cotangent) ((algebraMap P.Ring S : (a : P.Ring) → S) r : S)
        (of
          ((P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
            (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
              (((f.toAlgHom : AlgHom.{u, w, u_3} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯)))).val
have e : Eq (α := P'.ker.Cotangent)
  ((P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
      (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
        (((f.toAlgHom : AlgHom.{u, w, u_3} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑(r • x) : P.Ring)) sorry) :
    P'.ker.Cotangent)
  ((P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
      (HSMul.hSMul (α := P'.Ring) (β := ↥P'.ker) ((f.toRingHom : (a : P.Ring) → P'.Ring) r : P'.Ring)
        (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
            (((f.toAlgHom : AlgHom.{u, w, u_3} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) sorry :
          ↥P'.ker)) :
    P'.ker.Cotangent)
Tactic: conv_rhs => rw [← algebraMap_smul S', ← f.algebraMap_toRingHom, algebraMap_smul, val_smul',
      val_of, ← (Ideal.toCotangent _).map_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' : 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'
R'' : Type ?u.337215
S'' : Type ?u.337218
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : Algebra R S'
inst_16 : IsScalarTower R R' S'
f : P.Hom P'
x : ↥P.ker
r : P.Ring
⊢ Eq (α := P'.ker.Cotangent)
    ((P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
        (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
          (((f.toAlgHom : AlgHom.{u, w, u_3} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑(r • x) : P.Ring)) ⋯) :
      P'.ker.Cotangent)
    ((P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
        (HSMul.hSMul (α := P'.Ring) (β := ↥P'.ker) ((f.toRingHom : (a : P.Ring) → P'.Ring) r : P'.Ring)
          (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
              (((f.toAlgHom : AlgHom.{u, w, u_3} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯ :
            ↥P'.ker)) :
      P'.ker.Cotangent)
have e : Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
    (((f.toAlgHom : AlgHom.{u, w, u_3} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑(r • x) : P.Ring)) sorry =
  HSMul.hSMul (α := P'.Ring) (β := ↥P'.ker) ((f.toRingHom : (a : P.Ring) → P'.Ring) r : P'.Ring)
    (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
        (((f.toAlgHom : AlgHom.{u, w, u_3} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) sorry :
      ↥P'.ker)
Tactic: congr 1
-- 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'
R'' : Type ?u.337215
S'' : Type ?u.337218
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : Algebra R S'
inst_16 : IsScalarTower R R' S'
f : P.Hom P'
x : ↥P.ker
r : P.Ring
⊢ Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
      (((f.toAlgHom : AlgHom.{u, w, u_3} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑(r • x) : P.Ring)) ⋯ =
    HSMul.hSMul (α := P'.Ring) (β := ↥P'.ker) ((f.toRingHom : (a : P.Ring) → P'.Ring) r : P'.Ring)
      (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
          (((f.toAlgHom : AlgHom.{u, w, u_3} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯ :
        ↥P'.ker)
have e : (↑(Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
        (((f.toAlgHom : AlgHom.{u, w, u_3} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑(r • x) : P.Ring)) sorry) :
    P'.Ring) =
  (↑(HSMul.hSMul (α := P'.Ring) (β := ↥P'.ker) ((f.toRingHom : (a : P.Ring) → P'.Ring) r : P'.Ring)
        (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
            (((f.toAlgHom : AlgHom.{u, w, u_3} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) sorry :
          ↥P'.ker)) :
    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
⊢ map (Hom.id P) = LinearMap.id
have h : ∀ (x : P.Cotangent),
  Eq.{w + 1} (α := P.ker.Cotangent) (val ((map (Hom.id P) : (a : P.Cotangent) → P.Cotangent) x))
    (val ((LinearMap.id : (a : P.Cotangent) → P.Cotangent) x))
Tactic: ext 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
x : P.Cotangent
⊢ Eq.{w + 1} (α := P.ker.Cotangent) (val ((map (Hom.id P) : (a : P.Cotangent) → P.Cotangent) x))
    (val ((LinearMap.id : (a : P.Cotangent) → P.Cotangent) x))
have h : ∀ (x : ↥P.ker),
  Eq.{w + 1} (α := P.ker.Cotangent)
    (val ((map (Hom.id P) : (a : P.Cotangent) → P.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x)))
    (val ((LinearMap.id : (a : P.Cotangent) → P.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x)))
Tactic: obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
Cleared hypotheses: 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_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'
R'' : Type u_4
S'' : Type u_5
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension.{u_6, u_4, u_5} R'' S''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : Algebra R S'
inst_16 : IsScalarTower R R' S'
inst_17 : Algebra R R''
inst_18 : IsScalarTower R R' R''
inst_19 : IsScalarTower R' R'' S''
inst_20 : Algebra R S''
inst_21 : IsScalarTower R R'' S''
inst_22 : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
⊢ Eq (α := LinearMap.{v, v, w, u_6} (RingHom.id S) P.Cotangent P''.Cotangent) (map (g.comp f))
    ((↑S :
          {S_1 : Type u_2} →
            {M : Type u_3} →
              {M₂ : Type u_6} →
                [inst : Semiring S] →
                  [inst_23 : Semiring S_1] →
                    [inst_24 : AddCommMonoid M] →
                      [inst_25 : AddCommMonoid M₂] →
                        [inst_26 : Module S M] →
                          [inst_27 : Module S M₂] →
                            [inst_28 : Module S_1 M] →
                              [inst_29 : Module S_1 M₂] →
                                [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
        (map g) ∘ₗ
      map f)
have h : ∀ (x : P.Cotangent),
  Eq.{u_6 + 1} (α := P''.ker.Cotangent)
    (val
      (((map (g.comp f) : LinearMap.{v, v, w, u_6} (RingHom.id S) P.Cotangent P''.Cotangent) :
          (a : P.Cotangent) → P''.Cotangent)
        x))
    (val
      ((((↑S :
                  {S_1 : Type u_2} →
                    {M : Type u_3} →
                      {M₂ : Type u_6} →
                        [inst : Semiring S] →
                          [inst_23 : Semiring S_1] →
                            [inst_24 : AddCommMonoid M] →
                              [inst_25 : AddCommMonoid M₂] →
                                [inst_26 : Module S M] →
                                  [inst_27 : Module S M₂] →
                                    [inst_28 : Module S_1 M] →
                                      [inst_29 : Module S_1 M₂] →
                                        [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                (map g) ∘ₗ
              map f :
            LinearMap.{v, v, w, u_6} (RingHom.id S) P.Cotangent P''.Cotangent) :
          (a : P.Cotangent) → P''.Cotangent)
        x))
Tactic: ext 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
hP : P.ker.FG
⊢ Module.Finite.{v, w} S P.Cotangent
have refine : Submodule.FG.{w, w} (R := P.Ring) (M := P.Cotangent) (Submodule.restrictScalars.{w, v, w} P.Ring (R := S) ⊤)
Tactic: refine ⟨.of_restrictScalars (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
hP : P.ker.FG
⊢ Submodule.FG.{w, w} (R := P.Ring) (M := P.Cotangent) (Submodule.restrictScalars.{w, v, w} P.Ring (R := S) ⊤)
have rw : Submodule.FG.{w, w} (R := P.Ring) (Submodule.map mk ⊤)
Tactic: rw [Submodule.restrictScalars_top, ← LinearMap.range_eq_top.mpr Extension.Cotangent.mk_surjective,
    ← Submodule.map_top]