awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.CotangentBaseChange
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
⊢ ∃ (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)
              0)
            ⋯) :
        Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))

Tactic:
exact ⟨0, by simp only [map_zero]; exact (map_zero _).symm⟩
-- Module: Mathlib.RingTheory.Ideal.CotangentBaseChange
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)
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))
          ⋯) :
      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),
    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))

Tactic:
use t ⊗ₜ I.toCotangent x

Premises used: Ideal.toCotangent, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.CotangentBaseChange
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)
⊢ Eq (α :=
    T ⊗[R] S ⧸
      HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ)
        (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) 2)
    ((cotangentToQuotientSquare (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) :
          (a : (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent) →
            T ⊗[R] S ⧸ map Algebra.TensorProduct.includeRight.toRingHom I ^ 2)
        ((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)) :
      T ⊗[R] S ⧸
        HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ)
          (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) 2)
    ((cotangentToQuotientSquare (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) :
          (a : (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent) →
            T ⊗[R] S ⧸ map Algebra.TensorProduct.includeRight.toRingHom I ^ 2)
        ((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))
            ⋯)) :
      T ⊗[R] S ⧸
        HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ)
          (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) 2)

Tactic:
simp [-AlgHom.toRingHom_eq_coe, tensorCotangentHom_tmul, Algebra.smul_def,
      ← Ideal.Quotient.mk_algebraMap, ← map_mul]

Premises used: Ideal.tensorCotangentHom_tmul, map_mul, AlgHom.toRingHom_eq_coe, Algebra.smul_def, Ideal.Quotient.mk_algebraMap
-- Module: Mathlib.RingTheory.Ideal.CotangentBaseChange
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
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)
⊢ 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)

Tactic:
suffices h : Function.Injective (f ∘ₗ tensorCotangentHom R T I) from .of_comp h
-- Module: Mathlib.RingTheory.Ideal.CotangentBaseChange
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)
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)
⊢ f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g

Tactic:
ext x
-- Module: Mathlib.RingTheory.Ideal.CotangentBaseChange
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

Tactic:
have : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g := by
    ext x
    obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
    dsimp [f, g, hₐ]
    rw [tensorCotangentHom_tmul, one_smul, Ideal.toCotangent_to_quotient_square]
    simp
-- Module: Mathlib.RingTheory.Ideal.CotangentBaseChange
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)
this : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g
rw :
  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)
    (Function.comp (β := TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2))
      (⇑hₐ.toLinearMap : (a_1 : T ⊗[R] (S ⧸ I ^ 2)) → T ⊗[R] S ⧸ map a I ^ 2)
      (⇑g : (a : T ⊗[R] I.Cotangent) → T ⊗[R] (S ⧸ I ^ 2)))
⊢ 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:
rw [this, LinearMap.coe_comp]

Premises used: LinearMap.coe_comp
-- Module: Mathlib.RingTheory.Ideal.CotangentBaseChange
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)
this : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g
apply :
  Function.Injective (α := TensorProduct.{u_1, u_3, u_2} R T I.Cotangent) (β :=
    TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2)) (⇑g : (a : T ⊗[R] I.Cotangent) → T ⊗[R] (S ⧸ I ^ 2))
⊢ 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)
    (Function.comp (β := TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2))
      (⇑hₐ.toLinearMap : (a_1 : T ⊗[R] (S ⧸ I ^ 2)) → T ⊗[R] S ⧸ map a I ^ 2)
      (⇑g : (a : T ⊗[R] I.Cotangent) → T ⊗[R] (S ⧸ I ^ 2)))

Tactic:
apply hₐ.injective.comp

Premises used: Function.Injective.comp, AlgEquiv.injective
-- Module: Mathlib.RingTheory.Ideal.CotangentBaseChange
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)
this : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g
⊢ Function.Injective (α := I.Cotangent) (β := S ⧸ HPow.hPow (β := ℕ) 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) :
      (a : I.Cotangent) → S ⧸ I ^ 2)

Tactic:
apply cotangentToQuotientSquare_injective

Premises used: Ideal.cotangentToQuotientSquare_injective
-- Module: Mathlib.RingTheory.Ideal.CotangentBaseChange
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
t : T
x : ↥I
⊢ (tensorCotangentEquiv R T I :
        (a : T ⊗[R] I.Cotangent) → (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent)
      (t ⊗ₜ[R] (I.toCotangent : (a : ↥I) → I.Cotangent) x) =
    HSMul.hSMul (β :=
      Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I)) t
      ((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)
            (1 ⊗ₜ[R] (↑x : S)) ⋯) :
        Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Semiring α
I : Ideal α
⊢ 0 ∈ I

Tactic:
Submodule.zero_mem I

Premises used: Set.Mem, Submodule.zero_mem
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Semiring α
I : Ideal α
a b : α
⊢ a ∈ I → b ∈ I → a + b ∈ I

Tactic:
Submodule.add_mem I

Premises used: Set.Mem, Submodule.add_mem
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u
inst : Semiring α
I : Ideal α
a b : α
⊢ b ∈ I → a * b ∈ I

Tactic:
Submodule.smul_mem I a

Premises used: Set.Mem, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Ideal.Defs
Goal:
α : Type u_1
a b : α
inst : Semiring α
I : Ideal α
inst_1 : I.IsTwoSided
h : a ∈ I
⊢ a * b ∈ I

Tactic:
IsTwoSided.mul_mem_of_left b h

Premises used: Ideal.IsTwoSided.mul_mem_of_left