awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
this : (h :
    LE.le (α := Submodule R P)
      (Submodule.restrictScalars R (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
      (LinearMap.ker (M₂ := S ⊗[P] Ω[P⁄R])
        ((↑R :
              {S M : Type u_2} →
                {M₂ : Type (max u_3 u_2)} →
                  [inst : Semiring R] →
                    [inst_7 : Semiring S] →
                      [inst_8 : AddCommMonoid M] →
                        [inst_9 : AddCommMonoid M₂] →
                          [inst_10 : Module R M] →
                            [inst_11 : Module R M₂] →
                              [inst_12 : Module S M] →
                                [inst_13 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := P) ((mk P S Ω[P⁄R] : (a : S) → Ω[P⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) 1) ∘ₗ
          (↑(D R P) : P →ₗ[R] Ω[P⁄R])))) →
  HasQuotient.Quotient P (B := Submodule R P)
      (Submodule.restrictScalars R
        (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)) →ₗ[R]
    S ⊗[P] Ω[P⁄R] :=
  Submodule.liftQ (R := R) (M := P)
    (Submodule.restrictScalars R (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
    (R₂ := R) (M₂ := S ⊗[P] Ω[P⁄R]) (τ₁₂ := RingHom.id R)
    ((↑R :
          {S M : Type u_2} →
            {M₂ : Type (max u_3 u_2)} →
              [inst : Semiring R] →
                [inst_7 : Semiring S] →
                  [inst_8 : AddCommMonoid M] →
                    [inst_9 : AddCommMonoid M₂] →
                      [inst_10 : Module R M] →
                        [inst_11 : Module R M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (S := P) ((mk P S Ω[P⁄R] : (a : S) → Ω[P⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) 1) ∘ₗ
      (↑(D R P) : P →ₗ[R] Ω[P⁄R]))
x : P
hx :
  x ∈
    HMul.hMul (α := Ideal P) (RingHom.ker (F := P →+* S) (algebraMap P S)) (RingHom.ker (F := P →+* S) (algebraMap P S))
⊢ Eq (α := S ⊗[P] Ω[P⁄R]) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) x : S ⊗[P] Ω[P⁄R]) (0 : S ⊗[P] Ω[P⁄R])
have refine_1 : ∀ (r : P),
  Membership.mem (γ := Submodule P P) (RingHom.ker (F := P →+* S) (algebraMap P S)) r →
    ∀ (n : P),
      Membership.mem (γ := Submodule P P) (RingHom.ker (F := P →+* S) (algebraMap P S)) n →
        Eq (α := S ⊗[P] Ω[P⁄R]) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) (r • n) : S ⊗[P] Ω[P⁄R]) (0 : S ⊗[P] Ω[P⁄R])
Tactic: refine Submodule.smul_induction_on hx ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
this : (h :
    LE.le (α := Submodule R P)
      (Submodule.restrictScalars R (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
      (LinearMap.ker (M₂ := S ⊗[P] Ω[P⁄R])
        ((↑R :
              {S M : Type u_2} →
                {M₂ : Type (max u_3 u_2)} →
                  [inst : Semiring R] →
                    [inst_7 : Semiring S] →
                      [inst_8 : AddCommMonoid M] →
                        [inst_9 : AddCommMonoid M₂] →
                          [inst_10 : Module R M] →
                            [inst_11 : Module R M₂] →
                              [inst_12 : Module S M] →
                                [inst_13 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := P) ((mk P S Ω[P⁄R] : (a : S) → Ω[P⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) 1) ∘ₗ
          (↑(D R P) : P →ₗ[R] Ω[P⁄R])))) →
  HasQuotient.Quotient P (B := Submodule R P)
      (Submodule.restrictScalars R
        (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)) →ₗ[R]
    S ⊗[P] Ω[P⁄R] :=
  Submodule.liftQ (R := R) (M := P)
    (Submodule.restrictScalars R (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
    (R₂ := R) (M₂ := S ⊗[P] Ω[P⁄R]) (τ₁₂ := RingHom.id R)
    ((↑R :
          {S M : Type u_2} →
            {M₂ : Type (max u_3 u_2)} →
              [inst : Semiring R] →
                [inst_7 : Semiring S] →
                  [inst_8 : AddCommMonoid M] →
                    [inst_9 : AddCommMonoid M₂] →
                      [inst_10 : Module R M] →
                        [inst_11 : Module R M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (S := P) ((mk P S Ω[P⁄R] : (a : S) → Ω[P⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) 1) ∘ₗ
      (↑(D R P) : P →ₗ[R] Ω[P⁄R]))
⊢ Eq (α := S ⊗[P] Ω[P⁄R]) ((this ⋯ : (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → S ⊗[P] Ω[P⁄R]) 1) 0
have refine_2 : Eq (α := S ⊗[P] Ω[P⁄R]) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) 1) 0
Tactic: change (1 : S) ⊗ₜ[P] KaehlerDifferential.D R P 1 = 0
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
s : S
t : P
⊢ Eq (α := S ⊗[P] Ω[P⁄R])
    ((tensorKaehlerQuotKerSqEquiv R P S :
          (a : S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) → S ⊗[P] Ω[P⁄R])
        (s ⊗ₜ[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2]
          (D R (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
              (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
            ((Ideal.Quotient.mk (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
                (a : P) → P ⧸ RingHom.ker (algebraMap P S) ^ 2)
              t)) :
      S ⊗[P] Ω[P⁄R])
    (s ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) t : S ⊗[P] Ω[P⁄R])
have change : HSMul.hSMul (β := S ⊗[P] Ω[P⁄R]) s
    (((Derivation.liftKaehlerDifferential (R := R) (S :=
              P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) (M :=
              S ⊗[P] Ω[P⁄R]) (derivationQuotKerSq R P S) :
            LinearMap (R := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)
              (RingHom.id (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
              Ω[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2⁄R]
              (S ⊗[P] Ω[P⁄R])) :
          (a : Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) → S ⊗[P] Ω[P⁄R])
        ((D R (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
            (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
          ((Ideal.Quotient.mk (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
              (a : P) → P ⧸ RingHom.ker (algebraMap P S) ^ 2)
            t)) :
      S ⊗[P] Ω[P⁄R]) =
  s ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) t
Tactic: change s • (derivationQuotKerSq R P S).liftKaehlerDifferential
    (.D _ _ (Ideal.Quotient.mk _ t)) = _
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
s : S
t : P
⊢ Eq (α :=
    TensorProduct.{u_2, u_3, u_2}
      (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) S
      Ω[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2⁄R])
    ((LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P S) :
          (a : S ⊗[P] Ω[P⁄R]) → S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
        (s ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) t) :
      TensorProduct.{u_2, u_3, u_2}
        (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) S
        Ω[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2⁄R])
    (s ⊗ₜ[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2]
        (D R (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
            (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
          ((Ideal.Quotient.mk (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
              (a : P) → P ⧸ RingHom.ker (algebraMap P S) ^ 2)
            t) :
      TensorProduct.{u_2, u_3, u_2}
        (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) S
        Ω[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2⁄R])
have a : Eq (α := S ⊗[P] Ω[P⁄R])
  ((tensorKaehlerQuotKerSqEquiv R P S :
        (a : S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) → S ⊗[P] Ω[P⁄R])
      ((LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P S) :
          (a : S ⊗[P] Ω[P⁄R]) → S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
        (s ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) t)) :
    S ⊗[P] Ω[P⁄R])
  ((tensorKaehlerQuotKerSqEquiv R P S :
        (a : S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) → S ⊗[P] Ω[P⁄R])
      (s ⊗ₜ[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2]
        (D R (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
            (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
          ((Ideal.Quotient.mk (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
              (a : P) → P ⧸ RingHom.ker (algebraMap P S) ^ 2)
            t)) :
    S ⊗[P] Ω[P⁄R])
Tactic: apply (tensorKaehlerQuotKerSqEquiv R P S).injective
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (hypothesis)
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
P' : Type u_2 := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2
⊢ { l : S ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) //
      l ∘ₗ kerCotangentToTensor R P S = LinearMap.id } ≃
    { g :
      AlgHom.{u_1, u_3, u_2} R S
        (P ⧸
          HPow.hPow (α := Ideal P) (β := ℕ)
            (RingHom.ker (F := P →+* S) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P S))) 2) //
      AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P S)) g = AlgHom.id R S }
have h₁ : Surjective.{u_2 + 1, u_3 + 1} (α := P') (β := S) (⇑(algebraMap P' S) : (a : P') → S)
Tactic: have h₁ : Surjective (algebraMap P' S) := Function.Surjective.of_comp (g := algebraMap P P') hf
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (hypothesis)
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
P' : Type u_2 := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2
h₁ : Surjective.{u_2 + 1, u_3 + 1} (α := P') (β := S) (⇑(algebraMap P' S) : (a : P') → S)
⊢ { l : S ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) //
      l ∘ₗ kerCotangentToTensor R P S = LinearMap.id } ≃
    { g :
      AlgHom.{u_1, u_3, u_2} R S
        (P ⧸
          HPow.hPow (α := Ideal P) (β := ℕ)
            (RingHom.ker (F := P →+* S) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P S))) 2) //
      AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P S)) g = AlgHom.id R S }
have h₂ : HPow.hPow (α := Ideal P') (β := ℕ) (RingHom.ker (F := P' →+* S) (algebraMap P' S)) 2 = ⊥
Tactic: have h₂ : RingHom.ker (algebraMap P' S) ^ 2 = ⊥ := by
    rw [RingHom.algebraMap_toAlgebra, AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (hypothesis)
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
P' : Type u_2 := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2
h₁ : Surjective.{u_2 + 1, u_3 + 1} (α := P') (β := S) (⇑(algebraMap P' S) : (a : P') → S)
h₂ : HPow.hPow (α := Ideal P') (β := ℕ) (RingHom.ker (F := P' →+* S) (algebraMap P' S)) 2 = ⊥
e₁ : Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) ≃ₗ[P]
  ↥(RingHom.ker (F := P' →+* S) (algebraMap P' S)) :=
  Ideal.cotangentEquivIdeal (RingHom.ker (F := P →+* S) (algebraMap P S)) ≪≫ₗ
    LinearEquiv.restrictScalars P
      (LinearEquiv.ofEq
        (Ideal.cotangentIdeal (RingHom.ker (F := P →+* S) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P S))))
        (RingHom.ker (F :=
          RingHom.{u_2, u_3}
            (P ⧸
              HPow.hPow (α := Ideal P) (β := ℕ)
                (RingHom.ker (F := P →+* S) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P S))) 2)
            S)
          (AlgHom.toRingHom (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P S))))
        ⋯)
e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)
⊢ { l : S ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) //
      l ∘ₗ kerCotangentToTensor R P S = LinearMap.id } ≃
    { g :
      AlgHom.{u_1, u_3, u_2} R S
        (P ⧸
          HPow.hPow (α := Ideal P) (β := ℕ)
            (RingHom.ker (F := P →+* S) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P S))) 2) //
      AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P S)) g = AlgHom.id R S }
have H : kerCotangentToTensor R P S =
  (↑e₂ : S ⊗[P'] Ω[P'⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) ∘ₗ
    (↑P :
          {S M : Type u_2} →
            {M₂ : Type (max u_2 u_3)} →
              [inst : Semiring P] →
                [inst_7 : Semiring S] →
                  [inst_8 : AddCommMonoid M] →
                    [inst_9 : AddCommMonoid M₂] →
                      [inst_10 : Module P M] →
                        [inst_11 : Module P M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
        (kerToTensor R P' S) ∘ₗ
      (↑e₁ : (RingHom.ker (algebraMap P S)).Cotangent →ₗ[P] ↥(RingHom.ker (algebraMap P' S)))
Tactic: have H : kerCotangentToTensor R P S =
      e₂.toLinearMap ∘ₗ (kerToTensor R P' S).restrictScalars P ∘ₗ e₁.toLinearMap := by
    ext x
    obtain ⟨x, rfl⟩ := Ideal.toCotangent_surjective _ x
    exact (tensorKaehlerQuotKerSqEquiv_tmul_D 1 x.1).symm
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
P' : Type u_2 := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2
h₁ : Surjective.{u_2 + 1, u_3 + 1} (α := P') (β := S) (⇑(algebraMap P' S) : (a : P') → S)
h₂ : HPow.hPow (α := Ideal P') (β := ℕ) (RingHom.ker (F := P' →+* S) (algebraMap P' S)) 2 = ⊥
e₁ : Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) ≃ₗ[P]
  ↥(RingHom.ker (F := P' →+* S) (algebraMap P' S)) :=
  Ideal.cotangentEquivIdeal (RingHom.ker (F := P →+* S) (algebraMap P S)) ≪≫ₗ
    LinearEquiv.restrictScalars P
      (LinearEquiv.ofEq
        (Ideal.cotangentIdeal (RingHom.ker (F := P →+* S) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P S))))
        (RingHom.ker (F :=
          RingHom.{u_2, u_3}
            (P ⧸
              HPow.hPow (α := Ideal P) (β := ℕ)
                (RingHom.ker (F := P →+* S) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P S))) 2)
            S)
          (AlgHom.toRingHom (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P S))))
        ⋯)
e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)
H :
  kerCotangentToTensor R P S =
    (↑e₂ : S ⊗[P'] Ω[P'⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) ∘ₗ
      (↑P :
            {S M : Type u_2} →
              {M₂ : Type (max u_2 u_3)} →
                [inst : Semiring P] →
                  [inst_7 : Semiring S] →
                    [inst_8 : AddCommMonoid M] →
                      [inst_9 : AddCommMonoid M₂] →
                        [inst_10 : Module P M] →
                          [inst_11 : Module P M₂] →
                            [inst_12 : Module S M] →
                              [inst_13 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
          (kerToTensor R P' S) ∘ₗ
        (↑e₁ : (RingHom.ker (algebraMap P S)).Cotangent →ₗ[P] ↥(RingHom.ker (algebraMap P' S)))
⊢ { l : S ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) //
      l ∘ₗ kerCotangentToTensor R P S = LinearMap.id } ≃
    { g :
      AlgHom.{u_1, u_3, u_2} R S
        (P ⧸
          HPow.hPow (α := Ideal P) (β := ℕ)
            (RingHom.ker (F := P →+* S) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P S))) 2) //
      AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P S)) g = AlgHom.id R S }
have refine : { l : S ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) //
    l ∘ₗ kerCotangentToTensor R P S = LinearMap.id } ≃
  { l : S ⊗[P'] Ω[P'⁄R] →ₗ[P'] ↥(RingHom.ker (F := P' →+* S) (algebraMap P' S)) //
    l ∘ₗ kerToTensor R P' S = LinearMap.id }
Tactic: refine Equiv.trans ?_ (retractionKerToTensorEquivSection (R := R) h₂ h₁)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
this :
  CotangentSpace.map P.toInfinitesimal =
    (↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
      S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
        S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R])
⊢ Function.Bijective (α := P.CotangentSpace) (β := P.infinitesimal.CotangentSpace)
    (⇑(CotangentSpace.map P.toInfinitesimal) : (a : P.CotangentSpace) → P.infinitesimal.CotangentSpace)
have rw : Function.Bijective (α := P.CotangentSpace) (β := P.infinitesimal.CotangentSpace)
  (⇑(↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
        S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
          S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R]) :
    (a : P.CotangentSpace) → P.infinitesimal.CotangentSpace)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
⊢ Function.Bijective (α := P.CotangentSpace) (β := P.infinitesimal.CotangentSpace)
    (⇑(CotangentSpace.map P.toInfinitesimal) : (a : P.CotangentSpace) → P.infinitesimal.CotangentSpace)
have suffices : CotangentSpace.map P.toInfinitesimal =
  (↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
    S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
      S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R])
Tactic: suffices CotangentSpace.map P.toInfinitesimal =
      (tensorKaehlerQuotKerSqEquiv _ _ _).symm.toLinearMap by
    rw [this]; exact (tensorKaehlerQuotKerSqEquiv _ _ _).symm.bijective
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (hypothesis)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
this : Algebra P.Ring P.infinitesimal.Ring :=
  { smul := map_toInfinitesimal_bijective._aux_1 P, algebraMap := map_toInfinitesimal_bijective._aux_2 P,
    commutes' := ⋯, smul_def' := ⋯ }
⊢ CotangentSpace.map P.toInfinitesimal =
    (↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
      S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
        S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R])
have this₁ : IsScalarTower.{u, u, u_3} P.Ring P.infinitesimal.Ring S
Tactic: have : IsScalarTower P.Ring P.infinitesimal.Ring S := .of_algebraMap_eq' rfl