awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
⊢ Function.Exact (M := Ideal.Cotangent (RingHom.ker (F := A →+* B) (algebraMap A B))) (N := B ⊗[A] Ω[A⁄R]) (P := Ω[B⁄R])
    (⇑(kerCotangentToTensor R A B) : (a : (RingHom.ker (algebraMap A B)).Cotangent) → B ⊗[A] Ω[A⁄R])
    (⇑(mapBaseChange R A B) : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R])

Tactic:
SetLike.ext_iff.mp (range_kerCotangentToTensor R A B h).symm

Premises used: Function.Exact, Set.Mem, setOf, SetLike.ext_iff, Set.preimage, Set.singleton, Iff.mp, Set.range, KaehlerDifferential.range_kerCotangentToTensor, Eq.symm
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
⊢ Subsingleton.{u_3 + 1} Ω[B⁄A]

Tactic:
have := subsingleton_of_surjective A B h
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
this : Subsingleton.{u_3 + 1} Ω[B⁄A]
rw : LE.le (α := Submodule B Ω[B⁄R]) ⊤ (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))
⊢ Function.Surjective (α := B ⊗[A] Ω[A⁄R]) (β := Ω[B⁄R]) (⇑(mapBaseChange R A B) : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄R])

Tactic:
rw [← LinearMap.range_eq_top, range_mapBaseChange, ← top_le_iff]

Premises used: KaehlerDifferential.range_mapBaseChange, LinearMap.range_eq_top, top_le_iff
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
this : Subsingleton.{u_3 + 1} Ω[B⁄A]
⊢ LE.le (α := Submodule B Ω[B⁄R]) ⊤ (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))

Tactic:
fun x _ ↦ Subsingleton.elim _ _

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, Subsingleton.elim, OfNat.ofNat, DFunLike.coe, KaehlerDifferential.map
-- Module: Mathlib.RingTheory.Kaehler.Basic
Goal:
R : Type u
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
this : Subsingleton.{u_3 + 1} Ω[B⁄A]
⊢ LE.le (α := Submodule B Ω[B⁄R]) ⊤ (LinearMap.ker (M₂ := Ω[B⁄A]) (map R A B B))

Tactic:
exact fun x _ ↦ Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : Q.toExtension.Cotangent
obtain :
  ∀ (x : Q.toExtension.Ring) (hx : x ∈ Q.toExtension.ker),
    ∃ (a : Extension.Cotangent (toExtension (Q.comp P))),
      Eq (α := Q.toExtension.Cotangent)
        ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
              (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
            a :
          Q.toExtension.Cotangent)
        ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
            (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker) x hx) :
          Q.toExtension.Cotangent)
⊢ ∃ (a : Extension.Cotangent (toExtension (Q.comp P))),
    (Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
        a =
      x

Tactic:
obtain ⟨⟨x, hx⟩, rfl⟩ := Extension.Cotangent.mk_surjective x

Premises used: Algebra.Extension.Cotangent.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : Q.toExtension.Ring
hx : x ∈ Q.toExtension.ker
⊢ x ∈ Q.ker

Tactic:
have : x ∈ Q.ker := hx
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : Q.toExtension.Ring
hx : x ∈ Q.toExtension.ker
this : x ∈ Q.ker
⊢ ∃ (x_1 : Generators.Ring (Q.comp P)),
    Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x_1 ∧
      (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x_1 = x

Tactic:
rw [← map_ofComp_ker Q P, Ideal.mem_map_iff_of_surjective
    _ (toAlgHom_ofComp_surjective Q P)] at this

Premises used: Algebra.Generators.map_ofComp_ker, Algebra.Generators.toAlgHom_ofComp_surjective, Ideal.mem_map_iff_of_surjective
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : Q.toExtension.Ring
hx : x ∈ Q.toExtension.ker
this :
  ∃ (x_1 : Generators.Ring (Q.comp P)),
    Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x_1 ∧
      (Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x_1 = x
obtain :
  ∀ (x : Generators.Ring (Q.comp P)) (hx' : Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x)
    (hx :
      Membership.mem (α := Q.toExtension.Ring) Q.toExtension.ker
        ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring)),
    ∃ (a : Extension.Cotangent (toExtension (Q.comp P))),
      Eq (α := Q.toExtension.Cotangent)
        ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
              (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
            a :
          Q.toExtension.Cotangent)
        ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
            (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker)
              ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x) hx) :
          Q.toExtension.Cotangent)
⊢ ∃ (a : Extension.Cotangent (toExtension (Q.comp P))),
    Eq (α := Q.toExtension.Cotangent)
      ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
            (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
          a :
        Q.toExtension.Cotangent)
      ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker) x hx) :
        Q.toExtension.Cotangent)

Tactic:
obtain ⟨x, hx', rfl⟩ := this

Premises used: rfl
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : Generators.Ring (Q.comp P)
hx' : Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x
hx :
  Membership.mem (α := Q.toExtension.Ring) Q.toExtension.ker
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring)
⊢ ∃ (a : Extension.Cotangent (toExtension (Q.comp P))),
    Eq (α := Q.toExtension.Cotangent)
      ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
            (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
          a :
        Q.toExtension.Cotangent)
      ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker)
            ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x) hx) :
        Q.toExtension.Cotangent)

Tactic:
⟨.mk ⟨x, hx'⟩, Extension.Cotangent.map_mk _ _⟩

Premises used: Subtype.mk, Exists.intro, Algebra.Extension.Cotangent.mk, DFunLike.coe, Algebra.Extension.Cotangent.map_mk
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : Generators.Ring (Q.comp P)
hx' : Membership.mem (γ := Ideal (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x
hx :
  Membership.mem (α := Q.toExtension.Ring) Q.toExtension.ker
    ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring)
⊢ ∃ (a : Extension.Cotangent (toExtension (Q.comp P))),
    Eq (α := Q.toExtension.Cotangent)
      ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
            (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
          a :
        Q.toExtension.Cotangent)
      ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker)
            ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x) hx) :
        Q.toExtension.Cotangent)

Tactic:
exact ⟨.mk ⟨x, hx'⟩, Extension.Cotangent.map_mk _ _⟩
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
h1 :
  Eq (α := T ⊗[S] P.toExtension.Cotangent →ₗ[T] Q.toExtension.Cotangent)
    (Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) ∘ₗ
      LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P))))
    0
h2 :
  ∀ (x : Extension.Cotangent (toExtension (Q.comp P))),
    Eq (α := Q.toExtension.Cotangent)
        ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
              (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
            x :
          Q.toExtension.Cotangent)
        (0 : Q.toExtension.Cotangent) →
      Membership.mem (γ := Submodule T (Extension.Cotangent (toExtension (Q.comp P))))
        (LinearMap.range (M := T ⊗[S] P.toExtension.Cotangent)
          (LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P)))))
        x
⊢ Function.Exact (M := T ⊗[S] P.toExtension.Cotangent) (N := Extension.Cotangent (toExtension (Q.comp P))) (P :=
    Q.toExtension.Cotangent)
    (⇑(LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P)))) :
      (a : T ⊗[S] P.toExtension.Cotangent) → (Q.comp P).toExtension.Cotangent)
    (⇑(Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P))) :
      (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)

Tactic:
apply LinearMap.exact_of_comp_of_mem_range

Premises used: LinearMap.exact_of_comp_of_mem_range
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
h1 :
  Eq (α := P.toExtension.Cotangent →ₗ[S] Q.toExtension.Cotangent)
    (Extension.Cotangent.map
      (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
        (Hom.toExtensionHom (Q.toComp P))))
    0
⊢ Eq (α := T ⊗[S] P.toExtension.Cotangent →ₗ[T] Q.toExtension.Cotangent)
    (Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) ∘ₗ
      LinearMap.liftBaseChange T (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P))))
    0

Tactic:
rw [LinearMap.liftBaseChange_comp, ← Extension.Cotangent.map_comp,
      EmbeddingLike.map_eq_zero_iff]

Premises used: Algebra.Extension.Cotangent.map_comp, LinearMap.liftBaseChange_comp, EmbeddingLike.map_eq_zero_iff
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
h1 :
  ∀ (x : P.toExtension.Cotangent),
    Eq (α := Q.toExtension.ker.Cotangent)
      (Extension.Cotangent.val
        ((Extension.Cotangent.map
              (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
                (Hom.toExtensionHom (Q.toComp P))) :
            (a : P.toExtension.Cotangent) → Q.toExtension.Cotangent)
          x))
      (Extension.Cotangent.val ((0 : (a : P.toExtension.Cotangent) → Q.toExtension.Cotangent) x))
⊢ Eq (α := P.toExtension.Cotangent →ₗ[S] Q.toExtension.Cotangent)
    (Extension.Cotangent.map
      (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
        (Hom.toExtensionHom (Q.toComp P))))
    0

Tactic:
ext x
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Cotangent
h1 :
  ∀ (x : P.toExtension.Ring) (hx : x ∈ P.toExtension.ker),
    Eq (α := Q.toExtension.ker.Cotangent)
      (Extension.Cotangent.val
        ((Extension.Cotangent.map
              (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
                (Hom.toExtensionHom (Q.toComp P))) :
            (a : P.toExtension.Cotangent) → Q.toExtension.Cotangent)
          ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
            (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) x hx))))
      (Extension.Cotangent.val
        ((0 : (a : P.toExtension.Cotangent) → Q.toExtension.Cotangent)
          ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
            (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) x hx))))
⊢ Eq (α := Q.toExtension.ker.Cotangent)
    (Extension.Cotangent.val
      ((Extension.Cotangent.map
            (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
              (Hom.toExtensionHom (Q.toComp P))) :
          (a : P.toExtension.Cotangent) → Q.toExtension.Cotangent)
        x))
    (Extension.Cotangent.val ((0 : (a : P.toExtension.Cotangent) → Q.toExtension.Cotangent) x))

Tactic:
obtain ⟨⟨x, hx⟩, rfl⟩ := Extension.Cotangent.mk_surjective x

Premises used: Algebra.Extension.Cotangent.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
h1 :
  Eq (α := Q.toExtension.ker.Cotangent)
    ((Q.toExtension.ker.toCotangent : (a : ↥Q.toExtension.ker) → Q.toExtension.ker.Cotangent)
        (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker)
          ((Extension.Hom.toAlgHom
                (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
                  (Hom.toExtensionHom (Q.toComp P))) :
              (a : P.toExtension.Ring) → Q.toExtension.Ring)
            x)
          ⋯) :
      Q.toExtension.ker.Cotangent)
    (0 : Q.toExtension.ker.Cotangent)
⊢ Eq (α := Q.toExtension.ker.Cotangent)
    (Extension.Cotangent.val
      ((Extension.Cotangent.map
            (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
              (Hom.toExtensionHom (Q.toComp P))) :
          (a : P.toExtension.Cotangent) → Q.toExtension.Cotangent)
        ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) x hx))))
    (Extension.Cotangent.val
      ((0 : (a : P.toExtension.Cotangent) → Q.toExtension.Cotangent)
        ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) x hx))))

Tactic:
simp only [map_mk, val_mk, LinearMap.zero_apply, val_zero]

Premises used: LinearMap.zero_apply, Algebra.Extension.Cotangent.val_mk, Algebra.Extension.Cotangent.val_zero, Algebra.Extension.Cotangent.map_mk
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
⊢ Eq (α := Q.ker.Cotangent) ((Q.ker.toCotangent : (a : ↥Q.ker) → Q.ker.Cotangent) 0) 0

Tactic:
Q.ker.toCotangent.map_zero

Premises used: Algebra.Generators.ker, LinearMap.map_zero, Ideal.toCotangent
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
h :
  ↥Q.toExtension.ker = ↥Q.ker →
    Eq (α := Q.toExtension.Ring)
      ((Extension.Hom.toAlgHom
              (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
                (Hom.toExtensionHom (Q.toComp P))) :
            (a : P.toExtension.Ring) → Q.toExtension.Ring)
          x :
        Q.toExtension.Ring)
      ((↑0 : Q.toExtension.Ring) : Q.toExtension.Ring)
⊢ Eq (α := Q.toExtension.ker.Cotangent)
    ((Q.toExtension.ker.toCotangent : (a : ↥Q.toExtension.ker) → Q.toExtension.ker.Cotangent)
        (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker)
          ((Extension.Hom.toAlgHom
                (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
                  (Hom.toExtensionHom (Q.toComp P))) :
              (a : P.toExtension.Ring) → Q.toExtension.Ring)
            x)
          ⋯) :
      Q.toExtension.ker.Cotangent)
    (0 : Q.toExtension.ker.Cotangent)

Tactic:
convert! Q.ker.toCotangent.map_zero

Premises used: Algebra.Generators.ker, LinearMap.map_zero, Ideal.toCotangent
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
e_2 : ↥Q.toExtension.ker = ↥Q.ker
trans :
  Eq (α := Q.toExtension.Ring)
    ((Extension.Hom.toAlgHom
            (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
              (Hom.toExtensionHom (Q.toComp P))) :
          (a : P.toExtension.Ring) → Q.toExtension.Ring)
        x :
      Q.toExtension.Ring)
    ((AlgHom.comp (IsScalarTower.toAlgHom R S Q.toExtension.Ring) (IsScalarTower.toAlgHom R P.Ring S) :
          (a : P.Ring) → Q.toExtension.Ring)
        x :
      Q.toExtension.Ring)
trans₁ :
  Eq (α := Q.toExtension.Ring)
    ((AlgHom.comp (IsScalarTower.toAlgHom R S Q.toExtension.Ring) (IsScalarTower.toAlgHom R P.Ring S) :
          (a : P.Ring) → Q.toExtension.Ring)
        x :
      Q.toExtension.Ring)
    ((↑0 : Q.toExtension.Ring) : Q.toExtension.Ring)
⊢ Eq (α := Q.toExtension.Ring)
    ((Extension.Hom.toAlgHom
            (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
              (Hom.toExtensionHom (Q.toComp P))) :
          (a : P.toExtension.Ring) → Q.toExtension.Ring)
        x :
      Q.toExtension.Ring)
    ((↑0 : Q.toExtension.Ring) : Q.toExtension.Ring)

Tactic:
trans ((IsScalarTower.toAlgHom R _ _).comp (IsScalarTower.toAlgHom R P.Ring S)) x

Premises used: Algebra.Generators.Ring, IsScalarTower.toAlgHom, AlgHom.comp, DFunLike.coe
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
e_2 : ↥Q.toExtension.ker = ↥Q.ker
e_a :
  Eq (α := P.toExtension.Ring →ₐ[R] Q.toExtension.Ring)
    (Extension.Hom.toAlgHom
      (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
        (Hom.toExtensionHom (Q.toComp P))))
    (AlgHom.comp (IsScalarTower.toAlgHom R S Q.toExtension.Ring) (IsScalarTower.toAlgHom R P.Ring S))
⊢ Eq (α := Q.toExtension.Ring)
    ((Extension.Hom.toAlgHom
            (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
              (Hom.toExtensionHom (Q.toComp P))) :
          (a : P.toExtension.Ring) → Q.toExtension.Ring)
        x :
      Q.toExtension.Ring)
    ((AlgHom.comp (IsScalarTower.toAlgHom R S Q.toExtension.Ring) (IsScalarTower.toAlgHom R P.Ring S) :
          (a : P.Ring) → Q.toExtension.Ring)
        x :
      Q.toExtension.Ring)

Tactic:
congr
-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
e_2 : ↥Q.toExtension.ker = ↥Q.ker
⊢ Eq (α := P.toExtension.Ring →ₐ[R] Q.toExtension.Ring)
    (Extension.Hom.toAlgHom
      (Extension.Hom.comp (P' := toExtension (Q.comp P)) (Hom.toExtensionHom (Q.ofComp P))
        (Hom.toExtensionHom (Q.toComp P))))
    (AlgHom.comp (IsScalarTower.toAlgHom R S Q.toExtension.Ring) (IsScalarTower.toAlgHom R P.Ring S))

Tactic:
MvPolynomial.algHom_ext fun i ↦ ?_

Premises used: AddMonoidAlgebra.singleZeroRingHom, MvPolynomial.algHom_ext, AddMonoidAlgebra, Finsupp.single