awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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)
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))
⊢ 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⟩

Premises used: Iff.mp, Submodule.mem_sup
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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)
⊢ y + z ∈ J

Tactic:
simp [hyz]
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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)
⊢ y + z ∈ J

Tactic:
have : y + z ∈ J := by simp [hyz]
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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
⊢ Ne (α := ℕ) 2 0

Tactic:
omega
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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 = (J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : A) ↦ x ∈ J) z zmemJ)

Tactic:
simpa [← hx', J.toCotangent_eq, ← hyz] using hy

Premises used: Ideal.toCotangent_eq
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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 = (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
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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)
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)
⊢ x ∈
    Submodule.map J.toCotangent
      (Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J))

Tactic:
rw [xeq]
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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)
⊢ 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:
Submodule.mem_map_of_mem (Submodule.mem_comap.mpr (Ideal.mem_inf.mpr ⟨hz, zmemJ⟩))

Premises used: Iff.mpr, Submodule.mem_comap, Ideal.mem_inf, And.intro, Submodule.mem_map_of_mem
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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)
⊢ 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:
exact Submodule.mem_map_of_mem (Submodule.mem_comap.mpr (Ideal.mem_inf.mpr ⟨hz, zmemJ⟩))

Premises used: Iff.mpr, Submodule.mem_comap, Ideal.mem_inf, And.intro, Submodule.mem_map_of_mem
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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
refine_2 :
  Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J) ≤
    (J.mapCotangent I (Algebra.ofId A B) ⋯ ∘ₗ J.toCotangent).ker
⊢ 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

Tactic:
rw [Submodule.map_le_iff_le_comap, ← LinearMap.ker_comp]

Premises used: LinearMap.ker_comp, Submodule.map_le_iff_le_comap
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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)
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)) ⋯) :
      I.Cotangent)
    (0 : I.Cotangent)
⊢ x ∈ (J.mapCotangent I (Algebra.ofId A B) ⋯ ∘ₗ J.toCotangent).ker

Tactic:
simp only [LinearMap.mem_ker, LinearMap.comp_apply, Ideal.mapCotangent_toCotangent]

Premises used: LinearMap.comp_apply, Ideal.mapCotangent_toCotangent, LinearMap.mem_ker
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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) 0) 0

Tactic:
map_zero I.toCotangent

Premises used: map_zero, Ideal.toCotangent
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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)
h : Eq.{u_2 + 1} (α := B) ((Algebra.ofId A B : (a : A) → B) (↑x : A) : B) ((↑0 : B) : B)
⊢ 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)

Tactic:
convert! map_zero I.toCotangent

Premises used: map_zero, Ideal.toCotangent
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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.{u_2 + 1} (α := B) ((Algebra.ofId A B : (a : A) → B) (↑x : A) : B) ((↑0 : B) : B)

Tactic:
(Ideal.mem_inf.mp hx).1

Premises used: Set.Mem, setOf, Set.preimage, And.left, Ideal.mem_inf, Set.singleton, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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.{u_2 + 1} (α := B) ((Algebra.ofId A B : (a : A) → B) (↑x : A) : B) ((↑0 : B) : B)

Tactic:
exact (Ideal.mem_inf.mp hx).1

Premises used: And.left, Ideal.mem_inf, Iff.mp
-- 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
x y : ↥I
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))
⊢ 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))

Tactic:
simp only [AlgHom.toRingHom_eq_coe, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
      Function.comp_apply, Algebra.idealMap_mul]

Premises used: LinearMap.coe_restrictScalars, LinearMap.coe_comp, AlgHom.toRingHom_eq_coe, Function.comp_apply, Algebra.idealMap_mul
-- 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
x y : ↥I
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
mul_mem_mul ((Algebra.idealMap (T ⊗[R] S) I) x).property
      ((Algebra.idealMap (T ⊗[R] S) I) y).property

Premises used: Algebra.idealMap, Ideal.mul_mem_mul, TensorProduct, DFunLike.coe, Subtype.property
-- 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
x : Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I)
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))
⊢ ∃ (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

Tactic:
obtain ⟨⟨x, hx⟩, rfl⟩ := Ideal.toCotangent_surjective _ x

Premises used: Ideal.toCotangent_surjective, rfl
-- 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
y : TensorProduct.{u_1, u_3, u_2} R T ↥(Submodule.restrictScalars R I)
hx :
  Membership.mem (α := T ⊗[R] S) (γ := Ideal (T ⊗[R] S))
    (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I)
    ((LinearMap.lTensor T (Submodule.subtype (Submodule.restrictScalars R I)) :
          (a : T ⊗[R] ↥(Submodule.restrictScalars R I)) → T ⊗[R] S)
        y :
      T ⊗[R] S)
⊢ hx = ⋯

Tactic:
rfl

Premises used: rfl
-- 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
⊢ Eq (α :=
    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))
    ((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)
          0 ⋯) :
      Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))

Tactic:
(map_zero _).symm

Premises used: Set.Mem, map_zero, Eq.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
⊢ Eq (α :=
    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))
    ((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)
          0 ⋯) :
      Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))

Tactic:
exact (map_zero _).symm

Premises used: map_zero, Eq.symm