awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
P : Extension.{u, u_1, u_2} R S
Q : Extension.{u, u_1, u_3} R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H :
  Function.Bijective (α := Q.Ring ⊗[P.Ring] ↥P.ker) (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker)
this_1 : Algebra.{u, u_3} P.Ring T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap P.Ring S))
this_2 : IsScalarTower.{u, u_2, u_3} P.Ring S T
this : IsScalarTower.{u, u, u_3} P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : LinearMap (R := Q.Ring) (RingHom.id Q.Ring) (↥Q.ker) (TensorProduct.{u_2, u_3, u} S T P.Cotangent) :=
  LinearMap.liftBaseChange Q.Ring
      ((↑P.Ring :
            {S_1 : Type u_2} →
              {M : Type u} →
                {M₂ : Type (max u_3 u)} →
                  [inst_7 : Semiring P.Ring] →
                    [inst_8 : Semiring S_1] →
                      [inst_9 : AddCommMonoid M] →
                        [inst_10 : AddCommMonoid M₂] →
                          [inst_11 : Module P.Ring M] →
                            [inst_12 : Module P.Ring M₂] →
                              [inst_13 : Module S_1 M] →
                                [inst_14 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ P.Ring S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
          (S := S) ((TensorProduct.mk S T P.Cotangent : (a : T) → P.Cotangent →ₗ[S] T ⊗[S] P.Cotangent) 1) ∘ₗ
        Cotangent.mk) ∘ₗ
    (↑e.symm : ↥Q.ker →ₗ[Q.Ring] Q.Ring ⊗[P.Ring] ↥P.ker)
x : ↥Q.ker
hx : x ∈ (HSMul.hSMul (β := Submodule Q.Ring ↥Q.ker) Q.ker ⊤).toAddSubgroup
⊢ Membership.mem (γ := AddSubgroup ↥Q.ker) (AddMonoidHom.ker (↑f' : ↥Q.ker →+ T ⊗[S] P.Cotangent)) x
have refine : ∀ r ∈ Q.ker,
  ∀ (n : ↥Q.ker),
    Membership.mem (γ := Submodule Q.Ring ↥Q.ker) ⊤ n →
      Membership.mem (γ := AddSubgroup ↥Q.ker) (AddMonoidHom.ker (↑f' : ↥Q.ker →+ T ⊗[S] P.Cotangent)) (r • n)
Tactic: refine Submodule.smul_induction_on hx ?_ fun _ _ ↦ add_mem
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
P : Extension.{u, u_1, u_2} R S
Q : Extension.{u, u_1, u_3} R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H :
  Function.Bijective (α := Q.Ring ⊗[P.Ring] ↥P.ker) (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker)
this_1 : Algebra.{u, u_3} P.Ring T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap P.Ring S))
this_2 : IsScalarTower.{u, u_2, u_3} P.Ring S T
this : IsScalarTower.{u, u, u_3} P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : LinearMap (R := Q.Ring) (RingHom.id Q.Ring) (↥Q.ker) (TensorProduct.{u_2, u_3, u} S T P.Cotangent) :=
  LinearMap.liftBaseChange Q.Ring
      ((↑P.Ring :
            {S_1 : Type u_2} →
              {M : Type u} →
                {M₂ : Type (max u_3 u)} →
                  [inst_7 : Semiring P.Ring] →
                    [inst_8 : Semiring S_1] →
                      [inst_9 : AddCommMonoid M] →
                        [inst_10 : AddCommMonoid M₂] →
                          [inst_11 : Module P.Ring M] →
                            [inst_12 : Module P.Ring M₂] →
                              [inst_13 : Module S_1 M] →
                                [inst_14 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ P.Ring S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
          (S := S) ((TensorProduct.mk S T P.Cotangent : (a : T) → P.Cotangent →ₗ[S] T ⊗[S] P.Cotangent) 1) ∘ₗ
        Cotangent.mk) ∘ₗ
    (↑e.symm : ↥Q.ker →ₗ[Q.Ring] Q.Ring ⊗[P.Ring] ↥P.ker)
a : Q.Ring
ha : a ∈ Q.ker
b : ↥Q.ker
⊢ Membership.mem (γ := AddSubgroup ↥Q.ker) (AddMonoidHom.ker (↑f' : ↥Q.ker →+ T ⊗[S] P.Cotangent)) (a • b)
have obtain : ∀ (x : Q.Ring ⊗[P.Ring] ↥P.ker)
  (hx : (e : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) x = Subtype.mk (p := fun (x : Q.Ring) ↦ x ∈ Q.ker) a ha),
  Membership.mem (γ := AddSubgroup ↥Q.ker) (AddMonoidHom.ker (↑f' : ↥Q.ker →+ T ⊗[S] P.Cotangent)) (a • b)
Tactic: obtain ⟨x, hx⟩ := e.surjective ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
P : Extension.{u, u_1, u_2} R S
Q : Extension.{u, u_1, u_3} R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H :
  Function.Bijective (α := Q.Ring ⊗[P.Ring] ↥P.ker) (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker)
this_1 : Algebra.{u, u_3} P.Ring T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap P.Ring S))
this_2 : IsScalarTower.{u, u_2, u_3} P.Ring S T
this : IsScalarTower.{u, u, u_3} P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : LinearMap (R := Q.Ring) (RingHom.id Q.Ring) (↥Q.ker) (TensorProduct.{u_2, u_3, u} S T P.Cotangent) :=
  LinearMap.liftBaseChange Q.Ring
      ((↑P.Ring :
            {S_1 : Type u_2} →
              {M : Type u} →
                {M₂ : Type (max u_3 u)} →
                  [inst_7 : Semiring P.Ring] →
                    [inst_8 : Semiring S_1] →
                      [inst_9 : AddCommMonoid M] →
                        [inst_10 : AddCommMonoid M₂] →
                          [inst_11 : Module P.Ring M] →
                            [inst_12 : Module P.Ring M₂] →
                              [inst_13 : Module S_1 M] →
                                [inst_14 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ P.Ring S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
          (S := S) ((TensorProduct.mk S T P.Cotangent : (a : T) → P.Cotangent →ₗ[S] T ⊗[S] P.Cotangent) 1) ∘ₗ
        Cotangent.mk) ∘ₗ
    (↑e.symm : ↥Q.ker →ₗ[Q.Ring] Q.Ring ⊗[P.Ring] ↥P.ker)
a : Q.Ring
ha : a ∈ Q.ker
b : ↥Q.ker
x : Q.Ring ⊗[P.Ring] ↥P.ker
hx : (e : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) x = Subtype.mk (p := fun (x : Q.Ring) ↦ x ∈ Q.ker) a ha
⊢ Membership.mem (γ := AddSubgroup ↥Q.ker) (AddMonoidHom.ker (↑f' : ↥Q.ker →+ T ⊗[S] P.Cotangent)) (a • b)
have obtain : ∀ (ha : (↑((e : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) x) : Q.Ring) ∈ Q.ker)
  (hx :
    (e : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) x =
      Subtype.mk (p := fun (x : Q.Ring) ↦ x ∈ Q.ker) (↑((e : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) x) : Q.Ring) ha),
  Membership.mem (γ := AddSubgroup ↥Q.ker) (AddMonoidHom.ker (↑f' : ↥Q.ker →+ T ⊗[S] P.Cotangent))
    (HSMul.hSMul (α := Q.Ring) (↑((e : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) x) : Q.Ring) b)
Tactic: obtain rfl : (e x).1 = a := congr_arg Subtype.val hx
Cleared hypotheses: a, ha, hx
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
P : Extension.{u, u_1, u_2} R S
Q : Extension.{u, u_1, u_3} R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H :
  Function.Bijective (α := Q.Ring ⊗[P.Ring] ↥P.ker) (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker)
this_1 : Algebra.{u, u_3} P.Ring T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap P.Ring S))
this_2 : IsScalarTower.{u, u_2, u_3} P.Ring S T
this : IsScalarTower.{u, u, u_3} P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : LinearMap (R := Q.Ring) (RingHom.id Q.Ring) (↥Q.ker) (TensorProduct.{u_2, u_3, u} S T P.Cotangent) :=
  LinearMap.liftBaseChange Q.Ring
      ((↑P.Ring :
            {S_1 : Type u_2} →
              {M : Type u} →
                {M₂ : Type (max u_3 u)} →
                  [inst_7 : Semiring P.Ring] →
                    [inst_8 : Semiring S_1] →
                      [inst_9 : AddCommMonoid M] →
                        [inst_10 : AddCommMonoid M₂] →
                          [inst_11 : Module P.Ring M] →
                            [inst_12 : Module P.Ring M₂] →
                              [inst_13 : Module S_1 M] →
                                [inst_14 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ P.Ring S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
          (S := S) ((TensorProduct.mk S T P.Cotangent : (a : T) → P.Cotangent →ₗ[S] T ⊗[S] P.Cotangent) 1) ∘ₗ
        Cotangent.mk) ∘ₗ
    (↑e.symm : ↥Q.ker →ₗ[Q.Ring] Q.Ring ⊗[P.Ring] ↥P.ker)
b : ↥Q.ker
x : Q.Ring ⊗[P.Ring] ↥P.ker
ha : (↑((e : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) x) : Q.Ring) ∈ Q.ker
hx :
  (e : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) x =
    Subtype.mk (p := fun (x : Q.Ring) ↦ x ∈ Q.ker) (↑((e : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) x) : Q.Ring) ha
⊢ Membership.mem (γ := AddSubgroup ↥Q.ker) (AddMonoidHom.ker (↑f' : ↥Q.ker →+ T ⊗[S] P.Cotangent))
    (HSMul.hSMul (α := Q.Ring) (↑((e : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) x) : Q.Ring) b)
have obtain : ∀ (y : Q.Ring ⊗[P.Ring] ↥P.ker),
  Membership.mem (γ := AddSubgroup ↥Q.ker) (AddMonoidHom.ker (↑f' : ↥Q.ker →+ T ⊗[S] P.Cotangent))
    (HSMul.hSMul (α := Q.Ring) (β := ↥Q.ker) (↑((e : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) x) : Q.Ring)
      ((e : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) y : ↥Q.ker))
Tactic: obtain ⟨y, rfl⟩ := e.surjective b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
P : Extension.{u, u_1, u_2} R S
Q : Extension.{u, u_1, u_3} R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H :
  Function.Bijective (α := Q.Ring ⊗[P.Ring] ↥P.ker) (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker)
this_1 : Algebra.{u, u_3} P.Ring T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap P.Ring S))
this_2 : IsScalarTower.{u, u_2, u_3} P.Ring S T
this : IsScalarTower.{u, u, u_3} P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : LinearMap (R := Q.Ring) (RingHom.id Q.Ring) (↥Q.ker) (TensorProduct.{u_2, u_3, u} S T P.Cotangent) :=
  LinearMap.liftBaseChange Q.Ring
      ((↑P.Ring :
            {S_1 : Type u_2} →
              {M : Type u} →
                {M₂ : Type (max u_3 u)} →
                  [inst_7 : Semiring P.Ring] →
                    [inst_8 : Semiring S_1] →
                      [inst_9 : AddCommMonoid M] →
                        [inst_10 : AddCommMonoid M₂] →
                          [inst_11 : Module P.Ring M] →
                            [inst_12 : Module P.Ring M₂] →
                              [inst_13 : Module S_1 M] →
                                [inst_14 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ P.Ring S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
          (S := S) ((TensorProduct.mk S T P.Cotangent : (a : T) → P.Cotangent →ₗ[S] T ⊗[S] P.Cotangent) 1) ∘ₗ
        Cotangent.mk) ∘ₗ
    (↑e.symm : ↥Q.ker →ₗ[Q.Ring] Q.Ring ⊗[P.Ring] ↥P.ker)
a : Q.Ring
b : ↥P.ker
c : Q.Ring
d : ↥P.ker
⊢ (a * (↑((f.mapKer halg : (a : ↥P.ker) → ↥Q.ker) b) : Q.Ring)) •
      HSMul.hSMul (β := TensorProduct.{u_2, u_3, u} S T P.Cotangent) c
        (1 ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) d : TensorProduct.{u_2, u_3, u} S T P.Cotangent) =
    0
have h₂ : HSMul.hSMul (β := P.Cotangent) (↑b : P.Ring) ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) d : P.Cotangent) = 0
Tactic: have h₂ : b.1 • Cotangent.mk d = 0 := by ext; simp [Cotangent.smul_eq_zero_of_mem _ b.2]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
P : Extension.{u, u_1, u_2} R S
Q : Extension.{u, u_1, u_3} R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H :
  Function.Bijective (α := Q.Ring ⊗[P.Ring] ↥P.ker) (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker)
this_1 : Algebra.{u, u_3} P.Ring T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap P.Ring S))
this_2 : IsScalarTower.{u, u_2, u_3} P.Ring S T
this : IsScalarTower.{u, u, u_3} P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : LinearMap (R := Q.Ring) (RingHom.id Q.Ring) (↥Q.ker) (TensorProduct.{u_2, u_3, u} S T P.Cotangent) :=
  LinearMap.liftBaseChange Q.Ring
      ((↑P.Ring :
            {S_1 : Type u_2} →
              {M : Type u} →
                {M₂ : Type (max u_3 u)} →
                  [inst_7 : Semiring P.Ring] →
                    [inst_8 : Semiring S_1] →
                      [inst_9 : AddCommMonoid M] →
                        [inst_10 : AddCommMonoid M₂] →
                          [inst_11 : Module P.Ring M] →
                            [inst_12 : Module P.Ring M₂] →
                              [inst_13 : Module S_1 M] →
                                [inst_14 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ P.Ring S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
          (S := S) ((TensorProduct.mk S T P.Cotangent : (a : T) → P.Cotangent →ₗ[S] T ⊗[S] P.Cotangent) 1) ∘ₗ
        Cotangent.mk) ∘ₗ
    (↑e.symm : ↥Q.ker →ₗ[Q.Ring] Q.Ring ⊗[P.Ring] ↥P.ker)
a : Q.Ring
b : ↥P.ker
c : Q.Ring
d : ↥P.ker
h₂ : HSMul.hSMul (β := P.Cotangent) (↑b : P.Ring) ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) d : P.Cotangent) = 0
⊢ (a * (↑((f.mapKer halg : (a : ↥P.ker) → ↥Q.ker) b) : Q.Ring)) •
      HSMul.hSMul (β := TensorProduct.{u_2, u_3, u} S T P.Cotangent) c
        (1 ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) d : TensorProduct.{u_2, u_3, u} S T P.Cotangent) =
    0
have tmul : HSMul.hSMul (β := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (a * (↑((f.mapKer halg : (a : ↥P.ker) → ↥Q.ker) b) : Q.Ring))
    (HSMul.hSMul (β := T) c 1 ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) d :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent) =
  0
Tactic: rw [TensorProduct.smul_tmul', mul_smul, f.mapKer_apply_coe, ← halg,
          algebraMap_smul, ← TensorProduct.tmul_smul, h₂, tmul_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
P : Extension.{u, u_1, u_2} R S
Q : Extension.{u, u_1, u_3} R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H :
  Function.Bijective (α := Q.Ring ⊗[P.Ring] ↥P.ker) (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker)
this_1 : Algebra.{u, u_3} P.Ring T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap P.Ring S))
this_2 : IsScalarTower.{u, u_2, u_3} P.Ring S T
this : IsScalarTower.{u, u, u_3} P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : LinearMap (R := Q.Ring) (RingHom.id Q.Ring) (↥Q.ker) (TensorProduct.{u_2, u_3, u} S T P.Cotangent) :=
  LinearMap.liftBaseChange Q.Ring
      ((↑P.Ring :
            {S_1 : Type u_2} →
              {M : Type u} →
                {M₂ : Type (max u_3 u)} →
                  [inst_7 : Semiring P.Ring] →
                    [inst_8 : Semiring S_1] →
                      [inst_9 : AddCommMonoid M] →
                        [inst_10 : AddCommMonoid M₂] →
                          [inst_11 : Module P.Ring M] →
                            [inst_12 : Module P.Ring M₂] →
                              [inst_13 : Module S_1 M] →
                                [inst_14 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ P.Ring S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
          (S := S) ((TensorProduct.mk S T P.Cotangent : (a : T) → P.Cotangent →ₗ[S] T ⊗[S] P.Cotangent) 1) ∘ₗ
        Cotangent.mk) ∘ₗ
    (↑e.symm : ↥Q.ker →ₗ[Q.Ring] Q.Ring ⊗[P.Ring] ↥P.ker)
a : Q.Ring
b : ↥P.ker
c : Q.Ring
d : ↥P.ker
h₂ : HSMul.hSMul (β := P.Cotangent) (↑b : P.Ring) ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) d : P.Cotangent) = 0
tmul :
  HSMul.hSMul (β := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
      (a * (↑((f.mapKer halg : (a : ↥P.ker) → ↥Q.ker) b) : Q.Ring))
      (HSMul.hSMul (β := T) c 1 ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) d :
        TensorProduct.{u_2, u_3, u} S T P.Cotangent) =
    0
⊢ (a * (↑((f.mapKer halg : (a : ↥P.ker) → ↥Q.ker) b) : Q.Ring)) •
      HSMul.hSMul (β := TensorProduct.{u_2, u_3, u} S T P.Cotangent) c
        (1 ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) d : TensorProduct.{u_2, u_3, u} S T P.Cotangent) =
    0
have tmul₁ : a •
    HSMul.hSMul (α := Q.Ring) (β := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
      (↑((f.mapKer halg : (a : ↥P.ker) → ↥Q.ker) b) : Q.Ring)
      (HSMul.hSMul (β := T) c 1 ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) d :
        TensorProduct.{u_2, u_3, u} S T P.Cotangent) =
  0
Tactic: rw [TensorProduct.smul_tmul', mul_smul, f.mapKer_apply_coe, ← halg,
          algebraMap_smul, ← TensorProduct.tmul_smul, h₂, tmul_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
P : Extension.{u, u_1, u_2} R S
Q : Extension.{u, u_1, u_3} R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H :
  Function.Bijective (α := Q.Ring ⊗[P.Ring] ↥P.ker) (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker)
x : Q.Ring
y : ↥P.ker
this : Algebra.{u, u_3} P.Ring T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap P.Ring S))
⊢ (tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
      (HSMul.hSMul (β := Q.Cotangent) x
        ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
            (Subtype.mk (p := fun (x : Q.Ring) ↦ x ∈ Q.ker) ((f.toRingHom : (a : P.Ring) → Q.Ring) (↑y : P.Ring)) ⋯) :
          Q.Cotangent)) =
    HSMul.hSMul (β := TensorProduct.{u_2, u_3, u} S T P.Cotangent) x
      (1 ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) y : TensorProduct.{u_2, u_3, u} S T P.Cotangent)
have this₁ : IsScalarTower.{u, u_2, u_3} P.Ring S T
Tactic: haveI : IsScalarTower P.Ring S T := .of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
P : Extension.{u, u_1, u_2} R S
Q : Extension.{u, u_1, u_3} R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H :
  Function.Bijective (α := Q.Ring ⊗[P.Ring] ↥P.ker) (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker)
x : Q.Ring
y : ↥P.ker
this_1 : Algebra.{u, u_3} P.Ring T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap P.Ring S))
this : IsScalarTower.{u, u_2, u_3} P.Ring S T
⊢ (tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
      (HSMul.hSMul (β := Q.Cotangent) x
        ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
            (Subtype.mk (p := fun (x : Q.Ring) ↦ x ∈ Q.ker) ((f.toRingHom : (a : P.Ring) → Q.Ring) (↑y : P.Ring)) ⋯) :
          Q.Cotangent)) =
    HSMul.hSMul (β := TensorProduct.{u_2, u_3, u} S T P.Cotangent) x
      (1 ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) y : TensorProduct.{u_2, u_3, u} S T P.Cotangent)
have this₁ : IsScalarTower.{u, u, u_3} P.Ring Q.Ring T
Tactic: haveI : IsScalarTower P.Ring Q.Ring T :=
    .of_algebraMap_eq fun r ↦ halg ▸ (f.algebraMap_toRingHom r).symm
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
P : Extension.{u, u_1, u_2} R S
Q : Extension.{u, u_1, u_3} R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H :
  Function.Bijective (α := Q.Ring ⊗[P.Ring] ↥P.ker) (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker)
x : Q.Ring
y : ↥P.ker
this_1 : Algebra.{u, u_3} P.Ring T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap P.Ring S))
this_2 : IsScalarTower.{u, u_2, u_3} P.Ring S T
this : IsScalarTower.{u, u, u_3} P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
⊢ (tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
      (HSMul.hSMul (β := Q.Cotangent) x
        ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
            (Subtype.mk (p := fun (x : Q.Ring) ↦ x ∈ Q.ker) ((f.toRingHom : (a : P.Ring) → Q.Ring) (↑y : P.Ring)) ⋯) :
          Q.Cotangent)) =
    HSMul.hSMul (β := TensorProduct.{u_2, u_3, u} S T P.Cotangent) x
      (1 ⊗ₜ[S] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) y : TensorProduct.{u_2, u_3, u} S T P.Cotangent)
have trans : Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
  ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
      (HSMul.hSMul (β := Q.Cotangent) x
        ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
            (Subtype.mk (p := fun (x : Q.Ring) ↦ x ∈ Q.ker) ((f.toRingHom : (a : P.Ring) → Q.Ring) (↑y : P.Ring)) sorry) :
          Q.Cotangent)) :
    TensorProduct.{u_2, u_3, u} S T P.Cotangent)
  ((tensorCotangentInvFun f halg H : (a : Q.Cotangent) → T ⊗[S] P.Cotangent)
      ((Cotangent.mk : (a : ↥Q.ker) → Q.Cotangent)
        ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker) (x ⊗ₜ[P.Ring] y))) :
    TensorProduct.{u_2, u_3, u} S T P.Cotangent)
Tactic: trans tensorCotangentInvFun f halg H (.mk ((f.mapKer halg).liftBaseChange Q.Ring (x ⊗ₜ y)))