awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap (F := A →+* B) (algebraMap A B) I = RingHom.ker (F := A →+* B) (algebraMap A B) ⊔ J
eqmap : I = map (F := A →+* B) (algebraMap A B) J
x : J.Cotangent
hx : x ∈ (J.mapCotangent I (Algebra.ofId A B) ⋯).ker
x' : ↥J
hx' : (J.toCotangent : (a : ↥J) → J.Cotangent) x' = x
⊢ x ∈
    Submodule.map J.toCotangent
      (Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J))
have this : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(Algebra.ofId A B) : (a : A) → B)
Tactic: have : Function.Surjective (Algebra.ofId A B) := surj
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap (F := A →+* B) (algebraMap A B) I = RingHom.ker (F := A →+* B) (algebraMap A B) ⊔ J
eqmap : I = map (F := A →+* B) (algebraMap A B) J
x : J.Cotangent
hx : x ∈ (J.mapCotangent I (Algebra.ofId A B) ⋯).ker
x' : ↥J
hx' : (J.toCotangent : (a : ↥J) → J.Cotangent) x' = x
this : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(Algebra.ofId A B) : (a : A) → B)
⊢ x ∈
    Submodule.map J.toCotangent
      (Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J))
have hx₁ : Membership.mem (α := B) (HPow.hPow (α := Ideal B) (β := ℕ) (map (F := A →+* B) (algebraMap A B) J) 2)
  ((algebraMap A B : (a : A) → B) (↑x' : A) : B)
Tactic: simp only [← hx', LinearMap.mem_ker, Ideal.mapCotangent_toCotangent,
      Ideal.toCotangent_eq_zero, eqmap, Algebra.ofId_apply] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap (F := A →+* B) (algebraMap A B) I = RingHom.ker (F := A →+* B) (algebraMap A B) ⊔ J
eqmap : I = map (F := A →+* B) (algebraMap A B) J
x : J.Cotangent
x' : ↥J
hx' : (J.toCotangent : (a : ↥J) → J.Cotangent) x' = x
this : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(Algebra.ofId A B) : (a : A) → B)
hx :
  Membership.mem (α := B) (HPow.hPow (α := Ideal B) (β := ℕ) (map (F := A →+* B) (algebraMap A B) J) 2)
    ((algebraMap A B : (a : A) → B) (↑x' : A) : B)
⊢ x ∈
    Submodule.map J.toCotangent
      (Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J))
have hx₁ : (↑x' : A) ∈ HPow.hPow (β := ℕ) J 2 ⊔ RingHom.ker (F := A →+* B) (algebraMap A B)
Tactic: rw [← Ideal.map_pow, ← Ideal.mem_comap, Ideal.comap_map_of_surjective' _ surj] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap (F := A →+* B) (algebraMap A B) I = RingHom.ker (F := A →+* B) (algebraMap A B) ⊔ J
eqmap : I = map (F := A →+* B) (algebraMap A B) J
x : J.Cotangent
x' : ↥J
hx' : (J.toCotangent : (a : ↥J) → J.Cotangent) x' = x
this : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(Algebra.ofId A B) : (a : A) → B)
hx : (↑x' : A) ∈ HPow.hPow (β := ℕ) J 2 ⊔ RingHom.ker (F := A →+* B) (algebraMap A B)
⊢ x ∈
    Submodule.map J.toCotangent
      (Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J))
have refine_1 : ∀ (y : A) (hy : y ∈ HPow.hPow (β := ℕ) J 2) (z : A)
  (hz : Membership.mem (γ := Submodule A A) (RingHom.ker (F := A →+* B) (algebraMap A B)) z) (hyz : y + z = (↑x' : A)),
  x ∈
    Submodule.map J.toCotangent
      (Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J))
Tactic: rcases Submodule.mem_sup.mp hx with ⟨y, hy, z, hz, hyz⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap (F := A →+* B) (algebraMap A B) I = RingHom.ker (F := A →+* B) (algebraMap A B) ⊔ J
eqmap : I = map (F := A →+* B) (algebraMap A B) J
x : J.Cotangent
x' : ↥J
hx' : (J.toCotangent : (a : ↥J) → J.Cotangent) x' = x
this : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(Algebra.ofId A B) : (a : A) → B)
hx : (↑x' : A) ∈ HPow.hPow (β := ℕ) J 2 ⊔ RingHom.ker (F := A →+* B) (algebraMap A B)
y : A
hy : y ∈ HPow.hPow (β := ℕ) J 2
z : A
hz : Membership.mem (γ := Submodule A A) (RingHom.ker (F := A →+* B) (algebraMap A B)) z
hyz : y + z = (↑x' : A)
⊢ x ∈
    Submodule.map J.toCotangent
      (Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J))
have this₁ : y + z ∈ J
Tactic: have : y + z ∈ J := by simp [hyz]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap (F := A →+* B) (algebraMap A B) I = RingHom.ker (F := A →+* B) (algebraMap A B) ⊔ J
eqmap : I = map (F := A →+* B) (algebraMap A B) J
x : J.Cotangent
x' : ↥J
hx' : (J.toCotangent : (a : ↥J) → J.Cotangent) x' = x
this_1 : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(Algebra.ofId A B) : (a : A) → B)
hx : (↑x' : A) ∈ HPow.hPow (β := ℕ) J 2 ⊔ RingHom.ker (F := A →+* B) (algebraMap A B)
y : A
hy : y ∈ HPow.hPow (β := ℕ) J 2
z : A
hz : Membership.mem (γ := Submodule A A) (RingHom.ker (F := A →+* B) (algebraMap A B)) z
hyz : y + z = (↑x' : A)
this : y + z ∈ J
zmemJ : z ∈ J
⊢ x ∈
    Submodule.map J.toCotangent
      (Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J))
have xeq : x = (J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : A) ↦ x ∈ J) z zmemJ)
Tactic: have xeq : x = J.toCotangent ⟨z, zmemJ⟩ := by simpa [← hx', J.toCotangent_eq, ← hyz] using hy
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap (F := A →+* B) (algebraMap A B) I = RingHom.ker (F := A →+* B) (algebraMap A B) ⊔ J
eqmap : I = map (F := A →+* B) (algebraMap A B) J
x : J.Cotangent
x' : ↥J
hx' : (J.toCotangent : (a : ↥J) → J.Cotangent) x' = x
this_1 : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(Algebra.ofId A B) : (a : A) → B)
hx : (↑x' : A) ∈ HPow.hPow (β := ℕ) J 2 ⊔ RingHom.ker (F := A →+* B) (algebraMap A B)
y : A
hy : y ∈ HPow.hPow (β := ℕ) J 2
z : A
hz : Membership.mem (γ := Submodule A A) (RingHom.ker (F := A →+* B) (algebraMap A B)) z
hyz : y + z = (↑x' : A)
this : y + z ∈ J
zmemJ : z ∈ J
xeq : x = (J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : A) ↦ x ∈ J) z zmemJ)
⊢ x ∈
    Submodule.map J.toCotangent
      (Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J))
have refine_1 : Membership.mem (α := J.Cotangent)
  (Submodule.map J.toCotangent
    (Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J)))
  ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : A) ↦ x ∈ J) z zmemJ) : J.Cotangent)
Tactic: rw [xeq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap (F := A →+* B) (algebraMap A B) I = RingHom.ker (F := A →+* B) (algebraMap A B) ⊔ J
eqmap : I = map (F := A →+* B) (algebraMap A B) J
⊢ Submodule.map J.toCotangent
      (Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J)) ≤
    (J.mapCotangent I (Algebra.ofId A B) ⋯).ker
have refine_2 : Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J) ≤
  (J.mapCotangent I (Algebra.ofId A B) sorry ∘ₗ J.toCotangent).ker
Tactic: rw [Submodule.map_le_iff_le_comap, ← LinearMap.ker_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap (F := A →+* B) (algebraMap A B) I = RingHom.ker (F := A →+* B) (algebraMap A B) ⊔ J
eqmap : I = map (F := A →+* B) (algebraMap A B) J
x : ↥J
hx : x ∈ Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J)
⊢ x ∈ (J.mapCotangent I (Algebra.ofId A B) ⋯ ∘ₗ J.toCotangent).ker
have refine_2 : Eq (α := I.Cotangent)
  ((I.toCotangent : (a : ↥I) → I.Cotangent)
      (Subtype.mk (p := fun (x : B) ↦ x ∈ I) ((Algebra.ofId A B : (a : A) → B) (↑x : A)) sorry) :
    I.Cotangent)
  (0 : I.Cotangent)
Tactic: simp only [LinearMap.mem_ker, LinearMap.comp_apply, Ideal.mapCotangent_toCotangent]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap (F := A →+* B) (algebraMap A B) I = RingHom.ker (F := A →+* B) (algebraMap A B) ⊔ J
eqmap : I = map (F := A →+* B) (algebraMap A B) J
x : ↥J
hx : x ∈ Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J)
⊢ Eq (α := I.Cotangent)
    ((I.toCotangent : (a : ↥I) → I.Cotangent)
        (Subtype.mk (p := fun (x : B) ↦ x ∈ I) ((Algebra.ofId A B : (a : A) → B) (↑x : A)) ⋯) :
      I.Cotangent)
    (0 : I.Cotangent)
have h : Eq.{u_2 + 1} (α := B) ((Algebra.ofId A B : (a : A) → B) (↑x : A) : B) ((↑0 : B) : B)
Tactic: convert! map_zero I.toCotangent
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.CotangentBaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
I : Ideal S
x y : ↥I
⊢ Eq (α :=
    Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))
    ((sorry ∘ₗ
            (↑R :
                {S M : Type u_2} →
                  {M₂ : Type (max u_2 u_3)} →
                    [inst : Semiring R] →
                      [inst_5 : Semiring S] →
                        [inst_6 : AddCommMonoid M] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R M] →
                              [inst_9 : Module R M₂] →
                                [inst_10 : Module S M] →
                                  [inst_11 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (Algebra.idealMap (T ⊗[R] S) I) :
          (a : ↥I) → (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent)
        (x * y) :
      Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))
    (0 : Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))
have simp : Eq (α := Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (↑Algebra.TensorProduct.includeRight : S →+* T ⊗[R] S) I))
  ((sorry :
        (a : ↥(map (algebraMap S (T ⊗[R] S)) I)) →
          (map (↑Algebra.TensorProduct.includeRight : S →+* T ⊗[R] S) I).Cotangent)
      (HMul.hMul (α := ↥(map (F := S →+* T ⊗[R] S) (algebraMap S (T ⊗[R] S)) I)) (β :=
        ↥(map (F := S →+* T ⊗[R] S) (algebraMap S (T ⊗[R] S)) I))
        ((Algebra.idealMap (T ⊗[R] S) I : (a : ↥I) → ↥(map (algebraMap S (T ⊗[R] S)) I)) x :
          ↥(map (F := S →+* T ⊗[R] S) (algebraMap S (T ⊗[R] S)) I))
        ((Algebra.idealMap (T ⊗[R] S) I : (a : ↥I) → ↥(map (algebraMap S (T ⊗[R] S)) I)) y :
          ↥(map (F := S →+* T ⊗[R] S) (algebraMap S (T ⊗[R] S)) I))) :
    Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (↑Algebra.TensorProduct.includeRight : S →+* T ⊗[R] S) I))
  (0 : Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))
Tactic: simp only [AlgHom.toRingHom_eq_coe, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
      Function.comp_apply, Algebra.idealMap_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.CotangentBaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
I : Ideal S
a : S →+* T ⊗[R] S := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x : Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I)
⊢ ∃ (a : TensorProduct.{u_1, u_3, u_2} R T I.Cotangent),
    (tensorCotangentHom R T I :
          (a : T ⊗[R] I.Cotangent) → (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent)
        a =
      x
have obtain : ∀ (x : T ⊗[R] S)
  (hx :
    Membership.mem (γ := Ideal (T ⊗[R] S))
      (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) x),
  ∃ (a : TensorProduct.{u_1, u_3, u_2} R T I.Cotangent),
    Eq (α :=
      Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))
      ((tensorCotangentHom R T I :
            (a : T ⊗[R] I.Cotangent) → (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent)
          a :
        Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))
      ((toCotangent (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) :
            (a : ↥(map Algebra.TensorProduct.includeRight.toRingHom I)) →
              (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent)
          (Subtype.mk (p := fun (x : T ⊗[R] S) ↦
            Membership.mem (γ := Ideal (T ⊗[R] S))
              (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) x)
            x hx) :
        Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))
Tactic: obtain ⟨⟨x, hx⟩, rfl⟩ := Ideal.toCotangent_surjective _ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.CotangentBaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
I : Ideal S
a : S →+* T ⊗[R] S := AlgHom.toRingHom Algebra.TensorProduct.includeRight
t : T
x : ↥(Submodule.restrictScalars R I)
⊢ ∃ (a : TensorProduct.{u_1, u_3, u_2} R T I.Cotangent),
    Eq (α :=
      Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))
      ((tensorCotangentHom R T I :
            (a : T ⊗[R] I.Cotangent) → (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent)
          a :
        Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))
      ((toCotangent (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) :
            (a : ↥(map Algebra.TensorProduct.includeRight.toRingHom I)) →
              (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent)
          (Subtype.mk (p := fun (x : T ⊗[R] S) ↦
            Membership.mem (γ := Ideal (T ⊗[R] S))
              (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) x)
            ((LinearMap.lTensor T (Submodule.subtype (Submodule.restrictScalars R I)) :
                (a : T ⊗[R] ↥(Submodule.restrictScalars R I)) → T ⊗[R] S)
              (t ⊗ₜ[R] x))
            ⋯) :
        Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))
have h : Eq (α := Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))
  ((tensorCotangentHom R T I :
        (a : T ⊗[R] I.Cotangent) → (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent)
      (t ⊗ₜ[R] (I.toCotangent : (a : ↥I) → I.Cotangent) x) :
    Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))
  ((toCotangent (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) :
        (a : ↥(map Algebra.TensorProduct.includeRight.toRingHom I)) →
          (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent)
      (Subtype.mk (p := fun (x : T ⊗[R] S) ↦
        Membership.mem (γ := Ideal (T ⊗[R] S))
          (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) x)
        ((LinearMap.lTensor T (Submodule.subtype (Submodule.restrictScalars R I)) :
            (a : T ⊗[R] ↥(Submodule.restrictScalars R I)) → T ⊗[R] S)
          (t ⊗ₜ[R] x))
        sorry) :
    Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))
Tactic: use t ⊗ₜ I.toCotangent x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.CotangentBaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
I : Ideal S
inst_5 : Module.Flat R T
a : S →+* T ⊗[R] S := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : Cotangent (R := T ⊗[R] S) (map a I) →ₗ[T] T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2 := sorry
⊢ Function.Injective (α := TensorProduct.{u_1, u_3, u_2} R T I.Cotangent) (β :=
    Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))
    (⇑(tensorCotangentHom R T I) :
      (a : T ⊗[R] I.Cotangent) → (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent)
have suffices : Function.Injective (α := TensorProduct.{u_1, u_3, u_2} R T I.Cotangent) (β :=
  T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
  (⇑(f ∘ₗ tensorCotangentHom R T I) : (a_1 : T ⊗[R] I.Cotangent) → T ⊗[R] S ⧸ map a I ^ 2)
Tactic: suffices h : Function.Injective (f ∘ₗ tensorCotangentHom R T I) from .of_comp h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.CotangentBaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
I : Ideal S
inst_5 : Module.Flat R T
a : S →+* T ⊗[R] S := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : Cotangent (R := T ⊗[R] S) (map a I) →ₗ[T] T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2 := sorry
g : TensorProduct.{u_1, u_3, u_2} R T I.Cotangent →ₗ[T]
  TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2) :=
  ((AlgebraTensorModule.lTensor T T :
        (I.Cotangent →ₗ[R] S ⧸ HPow.hPow (β := ℕ) I 2) →ₗ[R]
          TensorProduct.{u_1, u_3, u_2} R T I.Cotangent →ₗ[T]
            TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2)) :
      (a : I.Cotangent →ₗ[R] S ⧸ I ^ 2) → T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2))
    ((↑R :
        {S M M₂ : Type u_2} →
          [inst : Semiring R] →
            [inst_6 : Semiring S] →
              [inst_7 : AddCommMonoid M] →
                [inst_8 : AddCommMonoid M₂] →
                  [inst_9 : Module R M] →
                    [inst_10 : Module R M₂] →
                      [inst_11 : Module S M] →
                        [inst_12 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      I.cotangentToQuotientSquare)
hₐ : TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2) ≃ₐ[T]
  T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2 :=
  AlgEquiv.trans
    (Algebra.TensorProduct.tensorQuotientEquiv T S T (HPow.hPow (β := ℕ) I 2) :
      TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2) ≃ₐ[T]
        HasQuotient.Quotient (T ⊗[R] S) (B := Ideal (T ⊗[R] S))
          (map (F := S →ₐ[R] T ⊗[R] S) Algebra.TensorProduct.includeRight (HPow.hPow (β := ℕ) I 2)))
    (quotientEquivAlgOfEq T ⋯ :
      HasQuotient.Quotient (T ⊗[R] S) (B := Ideal (T ⊗[R] S))
          (map (F := S →ₐ[R] T ⊗[R] S) Algebra.TensorProduct.includeRight (HPow.hPow (β := ℕ) I 2)) ≃ₐ[T]
        T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
⊢ f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g
have a₁ : ∀ (x : I.Cotangent),
  Eq (α := T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
    ((((AlgebraTensorModule.curry (f ∘ₗ tensorCotangentHom R T I) :
                T →ₗ[T] I.Cotangent →ₗ[R] T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2) :
              (a_1 : T) → I.Cotangent →ₗ[R] T ⊗[R] S ⧸ map a I ^ 2)
            1 :
          (a_1 : I.Cotangent) → T ⊗[R] S ⧸ map a I ^ 2)
        x :
      T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
    ((((AlgebraTensorModule.curry (hₐ.toLinearMap ∘ₗ g) :
                T →ₗ[T] I.Cotangent →ₗ[R] T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2) :
              (a_1 : T) → I.Cotangent →ₗ[R] T ⊗[R] S ⧸ map a I ^ 2)
            1 :
          (a_1 : I.Cotangent) → T ⊗[R] S ⧸ map a I ^ 2)
        x :
      T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
Tactic: ext x