awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₃
σ : Type w₂
σ' : Type w₄
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
W : Generators R T τ
x : Extension.Cotangent (toExtension (Q.comp P))
⊢ Eq (α := Q.toExtension.CotangentSpace)
    ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P)) ∘ₗ
            Extension.cotangentComplex (toExtension (Q.comp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.CotangentSpace)
        x :
      Q.toExtension.CotangentSpace)
    ((Q.toExtension.cotangentComplex ∘ₗ Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.CotangentSpace)
        x :
      Q.toExtension.CotangentSpace)

Tactic:
Extension.CotangentSpace.map_cotangentComplex (ofComp Q P).toExtensionHom _

Premises used: Quotient.liftOn', AddCon.liftOn, Algebra.Generators.Hom.toExtensionHom, Algebra.Extension.CotangentSpace.map_cotangentComplex, Algebra.Generators.ofComp
-- 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₃
σ : Type w₂
σ' : Type w₄
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
W : Generators R T τ
x : Extension.Cotangent (toExtension (Q.comp P))
⊢ Eq (α := Q.toExtension.CotangentSpace)
    ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P)) ∘ₗ
            Extension.cotangentComplex (toExtension (Q.comp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.CotangentSpace)
        x :
      Q.toExtension.CotangentSpace)
    ((Q.toExtension.cotangentComplex ∘ₗ Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.CotangentSpace)
        x :
      Q.toExtension.CotangentSpace)

Tactic:
exact Extension.CotangentSpace.map_cotangentComplex (ofComp Q P).toExtensionHom _

Premises used: Algebra.Generators.Hom.toExtensionHom, Algebra.Extension.CotangentSpace.map_cotangentComplex, Algebra.Generators.ofComp
-- 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 σ
hF :
  ∀ (i : σ),
    Eq.{u₃ + 1} (α := Ω[T⁄R])
      ((mapBaseChange R S T ∘ₗ LinearMap.baseChange T P.toExtension.toKaehler :
            (a : T ⊗[S] P.toExtension.CotangentSpace) → Ω[T⁄R])
          ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i) :
        Ω[T⁄R])
      ((Extension.toKaehler (toExtension (Q.comp P)) ∘ₗ
              LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) :
            (a : T ⊗[S] P.toExtension.CotangentSpace) → Ω[T⁄R])
          ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i) :
        Ω[T⁄R])
⊢ Eq (α := T ⊗[S] P.toExtension.CotangentSpace →ₗ[T] Ω[T⁄R])
    (mapBaseChange R S T ∘ₗ LinearMap.baseChange T P.toExtension.toKaehler)
    (Extension.toKaehler (toExtension (Q.comp P)) ∘ₗ
      LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))))

Tactic:
apply (P.cotangentSpaceBasis.baseChange T).ext

Premises used: Algebra.Generators.cotangentSpaceBasis, Module.Basis.baseChange, Module.Basis.ext
-- 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 σ
i : σ
hF :
  Eq (α := Ω[T⁄R]) ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) (P.val i)) : Ω[T⁄R])
    ((Extension.toKaehler (toExtension (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → Ω[T⁄R])
        ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P)) :
            (a : P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
          ((P.cotangentSpaceBasis : (a : σ) → P.toExtension.CotangentSpace) i)) :
      Ω[T⁄R])
⊢ Eq.{u₃ + 1} (α := Ω[T⁄R])
    ((mapBaseChange R S T ∘ₗ LinearMap.baseChange T P.toExtension.toKaehler :
          (a : T ⊗[S] P.toExtension.CotangentSpace) → Ω[T⁄R])
        ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i) :
      Ω[T⁄R])
    ((Extension.toKaehler (toExtension (Q.comp P)) ∘ₗ
            LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) :
          (a : T ⊗[S] P.toExtension.CotangentSpace) → Ω[T⁄R])
        ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i) :
      Ω[T⁄R])

Tactic:
simp only [Basis.baseChange_apply, LinearMap.coe_comp, Function.comp_apply,
      LinearMap.baseChange_tmul, toKaehler_cotangentSpaceBasis, mapBaseChange_tmul, map_D,
      one_smul, LinearMap.liftBaseChange_tmul]

Premises used: KaehlerDifferential.mapBaseChange_tmul, Module.Basis.baseChange_apply, one_smul, LinearMap.liftBaseChange_tmul, LinearMap.coe_comp, Algebra.Generators.toKaehler_cotangentSpaceBasis, Function.comp_apply, KaehlerDifferential.map_D, LinearMap.baseChange_tmul
-- 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 σ
i : σ
hF :
  Eq (α := Ω[T⁄R]) ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) (P.val i)) : Ω[T⁄R])
    ((Extension.toKaehler (toExtension (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → Ω[T⁄R])
        ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P)) :
            (a : P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
          (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i))) :
      Ω[T⁄R])
⊢ Eq (α := Ω[T⁄R]) ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) (P.val i)) : Ω[T⁄R])
    ((Extension.toKaehler (toExtension (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → Ω[T⁄R])
        ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P)) :
            (a : P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
          ((P.cotangentSpaceBasis : (a : σ) → P.toExtension.CotangentSpace) i)) :
      Ω[T⁄R])

Tactic:
rw [cotangentSpaceBasis_apply]

Premises used: Algebra.Generators.cotangentSpaceBasis_apply
-- 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 σ
i : σ
enter :
  ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P)) :
        (a : P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
      (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i)) :
    Extension.CotangentSpace (toExtension (Q.comp P)))
| ((Extension.toKaehler (toExtension (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → Ω[T⁄R])
      ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P)) :
          (a : P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
        (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i))) :
    Ω[T⁄R])

Tactic:
enter [2]
-- 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 σ
i : σ
⊢ Eq (α := Extension.CotangentSpace (toExtension (Q.comp P)))
    ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P)) :
          (a : P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
        (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i)) :
      Extension.CotangentSpace (toExtension (Q.comp P)))
    ((algebraMap S T : (a : S) → T) 1 ⊗ₜ[Extension.Ring (toExtension (Q.comp P))]
        (D R (Extension.Ring (toExtension (Q.comp P))) :
            (a : (Q.comp P).toExtension.Ring) → Ω[(Q.comp P).toExtension.Ring⁄R])
          ((Extension.Hom.toAlgHom (Hom.toExtensionHom (Q.toComp P)) :
              (a : P.toExtension.Ring) → (Q.comp P).toExtension.Ring)
            (X i)) :
      T ⊗[Extension.Ring (toExtension (Q.comp P))] Ω[Extension.Ring (toExtension (Q.comp P))⁄R])

Tactic:
Extension.CotangentSpace.map_tmul ..

Premises used: Set.Mem, Algebra.Extension.CotangentSpace.map_tmul, AddMonoidAlgebra.singleZeroRingHom, AddMonoidAlgebra, Finsupp.single
-- 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 σ
i : σ
⊢ Eq (α := Extension.CotangentSpace (toExtension (Q.comp P)))
    ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P)) :
          (a : P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
        (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i)) :
      Extension.CotangentSpace (toExtension (Q.comp P)))
    ((algebraMap S T : (a : S) → T) 1 ⊗ₜ[Extension.Ring (toExtension (Q.comp P))]
        (D R (Extension.Ring (toExtension (Q.comp P))) :
            (a : (Q.comp P).toExtension.Ring) → Ω[(Q.comp P).toExtension.Ring⁄R])
          ((Extension.Hom.toAlgHom (Hom.toExtensionHom (Q.toComp P)) :
              (a : P.toExtension.Ring) → (Q.comp P).toExtension.Ring)
            (X i)) :
      T ⊗[Extension.Ring (toExtension (Q.comp P))] Ω[Extension.Ring (toExtension (Q.comp P))⁄R])

Tactic:
exact Extension.CotangentSpace.map_tmul ..

Premises used: Algebra.Extension.CotangentSpace.map_tmul
-- 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 σ
i : σ
enter enter₁ :
  ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P)) :
        (a : P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
      (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i)) :
    Extension.CotangentSpace (toExtension (Q.comp P)))
| ((Extension.toKaehler (toExtension (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → Ω[T⁄R])
      ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P)) :
          (a : P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
        (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i))) :
    Ω[T⁄R])

Tactic:
enter [2]; tactic => exact Extension.CotangentSpace.map_tmul ..

Premises used: Algebra.Extension.CotangentSpace.map_tmul
-- 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 σ
i : σ
hF :
  Eq (α := Ω[T⁄R]) ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) (P.val i)) : Ω[T⁄R])
    ((Extension.toKaehler (toExtension (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → Ω[T⁄R])
        ((algebraMap S T : (a : S) → T) 1 ⊗ₜ[Extension.Ring (toExtension (Q.comp P))]
          (D R (Extension.Ring (toExtension (Q.comp P))) :
              (a : (Q.comp P).toExtension.Ring) → Ω[(Q.comp P).toExtension.Ring⁄R])
            ((Extension.Hom.toAlgHom (Hom.toExtensionHom (Q.toComp P)) :
                (a : P.toExtension.Ring) → (Q.comp P).toExtension.Ring)
              (X i))) :
      Ω[T⁄R])
⊢ Eq (α := Ω[T⁄R]) ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) (P.val i)) : Ω[T⁄R])
    ((Extension.toKaehler (toExtension (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → Ω[T⁄R])
        ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P)) :
            (a : P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
          (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i))) :
      Ω[T⁄R])

Tactic:
conv_rhs => enter [2]; tactic => exact Extension.CotangentSpace.map_tmul ..

Premises used: Algebra.Extension.CotangentSpace.map_tmul
-- 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 σ
i : σ
hF :
  Eq (α := Ω[T⁄R]) ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) (P.val i)) : Ω[T⁄R])
    ((D R T : (a : T) → Ω[T⁄R])
        ((algebraMap (Extension.Ring (toExtension (Q.comp P))) T : (a : (Q.comp P).toExtension.Ring) → T)
          ((Extension.Hom.toAlgHom (Hom.toExtensionHom (Q.toComp P)) :
                (a : P.toExtension.Ring) → (Q.comp P).toExtension.Ring)
              (X i) :
            Extension.Ring (toExtension (Q.comp P)))) :
      Ω[T⁄R])
⊢ Eq (α := Ω[T⁄R]) ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) (P.val i)) : Ω[T⁄R])
    ((Extension.toKaehler (toExtension (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → Ω[T⁄R])
        ((algebraMap S T : (a : S) → T) 1 ⊗ₜ[Extension.Ring (toExtension (Q.comp P))]
          (D R (Extension.Ring (toExtension (Q.comp P))) :
              (a : (Q.comp P).toExtension.Ring) → Ω[(Q.comp P).toExtension.Ring⁄R])
            ((Extension.Hom.toAlgHom (Hom.toExtensionHom (Q.toComp P)) :
                (a : P.toExtension.Ring) → (Q.comp P).toExtension.Ring)
              (X i))) :
      Ω[T⁄R])

Tactic:
simp only [map_one, mapBaseChange_tmul, map_D, one_smul]

Premises used: KaehlerDifferential.mapBaseChange_tmul, one_smul, map_one, KaehlerDifferential.map_D
-- 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 σ
i : σ
⊢ Eq (α := Ω[T⁄R]) ((D R T : (a : T) → Ω[T⁄R]) ((algebraMap S T : (a : S) → T) (P.val i)) : Ω[T⁄R])
    ((D R T : (a : T) → Ω[T⁄R])
        ((algebraMap (Extension.Ring (toExtension (Q.comp P))) T : (a : (Q.comp P).toExtension.Ring) → T)
          ((Extension.Hom.toAlgHom (Hom.toExtensionHom (Q.toComp P)) :
                (a : P.toExtension.Ring) → (Q.comp P).toExtension.Ring)
              (X i) :
            Extension.Ring (toExtension (Q.comp P)))) :
      Ω[T⁄R])

Tactic:
simp [Extension.Hom.toAlgHom]

Premises used: Algebra.Extension.Hom.toAlgHom
-- 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 σ
⊢ Function.Surjective (α := T ⊗[S] P.toExtension.CotangentSpace) (β := T ⊗[S] Ω[S⁄R])
    (⇑(LinearMap.baseChange T P.toExtension.toKaehler) : (a : T ⊗[S] P.toExtension.CotangentSpace) → T ⊗[S] Ω[S⁄R])

Tactic:
LinearMap.lTensor_surjective T P.toExtension.toKaehler_surjective

Premises used: LinearMap.lTensor_surjective, Algebra.Extension.toKaehler_surjective, TensorProduct.tmul, AddCon.toQuotient
-- 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 σ
⊢ Function.Surjective (α := T ⊗[S] P.toExtension.CotangentSpace) (β := T ⊗[S] Ω[S⁄R])
    (⇑(LinearMap.baseChange T P.toExtension.toKaehler) : (a : T ⊗[S] P.toExtension.CotangentSpace) → T ⊗[S] Ω[S⁄R])

Tactic:
exact LinearMap.lTensor_surjective T P.toExtension.toKaehler_surjective

Premises used: LinearMap.lTensor_surjective, Algebra.Extension.toKaehler_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.H1Cotangent
y : Extension.Cotangent (toExtension (Q.comp P))
hy :
  (Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
        (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
      y =
    (↑x : Q.toExtension.Cotangent)
z : T ⊗[S] P.toExtension.CotangentSpace
hz :
  Eq (α := Extension.CotangentSpace (toExtension (Q.comp P)))
    ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) :
          (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
        z :
      Extension.CotangentSpace (toExtension (Q.comp P)))
    ((Extension.cotangentComplex (toExtension (Q.comp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
        y :
      Extension.CotangentSpace (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)
        y :
      Q.toExtension.Cotangent)
    ((Extension.h1Cotangentι : (a : Q.toExtension.H1Cotangent) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)

Tactic:
hy
-- 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.H1Cotangent
y : Extension.Cotangent (toExtension (Q.comp P))
hy :
  (Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
        (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
      y =
    (↑x : Q.toExtension.Cotangent)
z : T ⊗[S] P.toExtension.CotangentSpace
hz :
  Eq (α := Extension.CotangentSpace (toExtension (Q.comp P)))
    ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) :
          (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
        z :
      Extension.CotangentSpace (toExtension (Q.comp P)))
    ((Extension.cotangentComplex (toExtension (Q.comp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
        y :
      Extension.CotangentSpace (toExtension (Q.comp P)))
⊢ Eq (α := Extension.CotangentSpace (toExtension (Q.comp P)))
    ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) :
          (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
        z :
      Extension.CotangentSpace (toExtension (Q.comp P)))
    ((Extension.cotangentComplex (toExtension (Q.comp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → (Q.comp P).toExtension.CotangentSpace)
        y :
      Extension.CotangentSpace (toExtension (Q.comp P)))

Tactic:
hz
-- 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.ker
hx :
  Membership.mem (α := Q.toExtension.Cotangent) Q.toExtension.cotangentComplex.ker
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
y : Extension.Cotangent (toExtension (Q.comp P)) :=
  (Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
    (Q.kerCompPreimage P x)
simp :
  Eq (α := 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)
          ((Extension.Hom.toAlgHom (Hom.toExtensionHom (Q.ofComp P)) :
              (a : (Q.comp P).toExtension.Ring) → Q.toExtension.Ring)
            (↑(Q.kerCompPreimage P x) : (Q.comp P).toExtension.Ring))
          ⋯) :
      Q.toExtension.Cotangent)
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
⊢ Eq (α := Q.toExtension.Cotangent)
    ((Extension.Cotangent.map (Hom.toExtensionHom (Q.ofComp P)) :
          (a : (Q.comp P).toExtension.Cotangent) → Q.toExtension.Cotangent)
        y :
      Q.toExtension.Cotangent)
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)

Tactic:
simp only [y, Extension.Cotangent.map_mk]

Premises used: 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 : ↥Q.ker
hx :
  Membership.mem (α := Q.toExtension.Cotangent) Q.toExtension.cotangentComplex.ker
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)
y : Extension.Cotangent (toExtension (Q.comp P)) :=
  (Extension.Cotangent.mk : (a : ↥(Q.comp P).toExtension.ker) → (Q.comp P).toExtension.Cotangent)
    (Q.kerCompPreimage P x)
h :
  (Extension.Hom.toAlgHom (Hom.toExtensionHom (Q.ofComp P)) : (a : (Q.comp P).toExtension.Ring) → Q.toExtension.Ring)
      (↑(Q.kerCompPreimage P x) : (Q.comp P).toExtension.Ring) =
    (↑x : Q.toExtension.Ring)
⊢ Eq (α := 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)
          ((Extension.Hom.toAlgHom (Hom.toExtensionHom (Q.ofComp P)) :
              (a : (Q.comp P).toExtension.Ring) → Q.toExtension.Ring)
            (↑(Q.kerCompPreimage P x) : (Q.comp P).toExtension.Ring))
          ⋯) :
      Q.toExtension.Cotangent)
    ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent) x : Q.toExtension.Cotangent)

Tactic:
congr