awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
h :
  ∀ (x : P.Cotangent),
    Eq.{w' + 1} (α := P'.ker.Cotangent) (val ((map f - map g : (a : P.Cotangent) → P'.Cotangent) x))
      (val ((f.sub g ∘ₗ P.cotangentComplex : (a : P.Cotangent) → P'.Cotangent) x))
⊢ map f - map g = f.sub g ∘ₗ P.cotangentComplex

Tactic:
ext x
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
x : P.Cotangent
h :
  ∀ (x : ↥P.ker),
    Eq.{w' + 1} (α := P'.ker.Cotangent)
      (val ((map f - map g : (a : P.Cotangent) → P'.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x)))
      (val ((f.sub g ∘ₗ P.cotangentComplex : (a : P.Cotangent) → P'.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x)))
⊢ Eq.{w' + 1} (α := P'.ker.Cotangent) (val ((map f - map g : (a : P.Cotangent) → P'.Cotangent) x))
    (val ((f.sub g ∘ₗ P.cotangentComplex : (a : P.Cotangent) → P'.Cotangent) x))

Tactic:
obtain ⟨x, rfl⟩ := mk_surjective x

Premises used: Algebra.Extension.Cotangent.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
x : ↥P.ker
h :
  (HSub.hSub (α := P'.Cotangent) (β := P'.Cotangent)
        ((mk : (a : ↥P'.ker) → P'.Cotangent)
            (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
              (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯) :
          P'.Cotangent)
        ((mk : (a : ↥P'.ker) → P'.Cotangent)
            (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
              (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯) :
          P'.Cotangent)).val =
    (P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
      (((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker) (↑x : P.Ring))
⊢ Eq.{w' + 1} (α := P'.ker.Cotangent)
    (val ((map f - map g : (a : P.Cotangent) → P'.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x)))
    (val ((f.sub g ∘ₗ P.cotangentComplex : (a : P.Cotangent) → P'.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x)))

Tactic:
simp only [LinearMap.sub_apply, map_mk, LinearMap.coe_comp, Function.comp_apply,
    cotangentComplex_mk, Hom.sub_tmul, one_smul, val_mk]

Premises used: Algebra.Extension.Cotangent.val_mk, one_smul, LinearMap.coe_comp, LinearMap.sub_apply, Function.comp_apply, Algebra.Extension.Hom.sub_tmul, Algebra.Extension.Cotangent.map_mk, Algebra.Extension.cotangentComplex_mk
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
x : ↥P.ker
h :
  Eq (α := ↥P'.ker.cotangentIdeal)
    ((P'.ker.cotangentEquivIdeal : (a : P'.ker.Cotangent) → ↥P'.ker.cotangentIdeal)
        (HSub.hSub (α := P'.Cotangent) (β := P'.Cotangent)
            ((mk : (a : ↥P'.ker) → P'.Cotangent)
                (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
                  (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯) :
              P'.Cotangent)
            ((mk : (a : ↥P'.ker) → P'.Cotangent)
                (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
                  (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯) :
              P'.Cotangent)).val :
      ↥P'.ker.cotangentIdeal)
    ((P'.ker.cotangentEquivIdeal : (a : P'.ker.Cotangent) → ↥P'.ker.cotangentIdeal)
        ((P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
          (((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker)
            (↑x : P.Ring))) :
      ↥P'.ker.cotangentIdeal)
⊢ (HSub.hSub (α := P'.Cotangent) (β := P'.Cotangent)
        ((mk : (a : ↥P'.ker) → P'.Cotangent)
            (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
              (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯) :
          P'.Cotangent)
        ((mk : (a : ↥P'.ker) → P'.Cotangent)
            (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
              (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯) :
          P'.Cotangent)).val =
    (P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
      (((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker) (↑x : P.Ring))

Tactic:
apply (Ideal.cotangentEquivIdeal _).injective

Premises used: Ideal.cotangentEquivIdeal, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
x : ↥P.ker
h :
  Eq.{w' + 1} (α := P'.Ring ⧸ HPow.hPow (β := ℕ) P'.ker 2)
    (↑((P'.ker.cotangentEquivIdeal : (a : P'.ker.Cotangent) → ↥P'.ker.cotangentIdeal)
          (HSub.hSub (α := P'.Cotangent) (β := P'.Cotangent)
              ((mk : (a : ↥P'.ker) → P'.Cotangent)
                  (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
                    (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯) :
                P'.Cotangent)
              ((mk : (a : ↥P'.ker) → P'.Cotangent)
                  (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
                    (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯) :
                P'.Cotangent)).val) :
      P'.Ring ⧸ P'.ker ^ 2)
    (↑((P'.ker.cotangentEquivIdeal : (a : P'.ker.Cotangent) → ↥P'.ker.cotangentIdeal)
          ((P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
            (((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker)
              (↑x : P.Ring)))) :
      P'.Ring ⧸ P'.ker ^ 2)
⊢ Eq (α := ↥P'.ker.cotangentIdeal)
    ((P'.ker.cotangentEquivIdeal : (a : P'.ker.Cotangent) → ↥P'.ker.cotangentIdeal)
        (HSub.hSub (α := P'.Cotangent) (β := P'.Cotangent)
            ((mk : (a : ↥P'.ker) → P'.Cotangent)
                (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
                  (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯) :
              P'.Cotangent)
            ((mk : (a : ↥P'.ker) → P'.Cotangent)
                (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
                  (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯) :
              P'.Cotangent)).val :
      ↥P'.ker.cotangentIdeal)
    ((P'.ker.cotangentEquivIdeal : (a : P'.ker.Cotangent) → ↥P'.ker.cotangentIdeal)
        ((P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
          (((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker)
            (↑x : P.Ring))) :
      ↥P'.ker.cotangentIdeal)

Tactic:
ext
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
x : ↥P.ker
⊢ Eq.{w' + 1} (α := P'.Ring ⧸ HPow.hPow (β := ℕ) P'.ker 2)
    (↑((P'.ker.cotangentEquivIdeal : (a : P'.ker.Cotangent) → ↥P'.ker.cotangentIdeal)
          (HSub.hSub (α := P'.Cotangent) (β := P'.Cotangent)
              ((mk : (a : ↥P'.ker) → P'.Cotangent)
                  (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
                    (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯) :
                P'.Cotangent)
              ((mk : (a : ↥P'.ker) → P'.Cotangent)
                  (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
                    (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯) :
                P'.Cotangent)).val) :
      P'.Ring ⧸ P'.ker ^ 2)
    (↑((P'.ker.cotangentEquivIdeal : (a : P'.ker.Cotangent) → ↥P'.ker.cotangentIdeal)
          ((P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
            (((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker)
              (↑x : P.Ring)))) :
      P'.Ring ⧸ P'.ker ^ 2)

Tactic:
simp only [val_sub, val_mk, map_sub, AddSubgroupClass.coe_sub, Ideal.cotangentEquivIdeal_apply,
    Ideal.toCotangent_to_quotient_square, Submodule.mkQ_apply, Ideal.Quotient.mk_eq_mk,
    Hom.subToKer_apply_coe, Hom.toAlgHom_apply]

Premises used: Ideal.toCotangent_to_quotient_square, AddSubgroupClass.coe_sub, Algebra.Extension.Cotangent.val_sub, map_sub, Algebra.Extension.Cotangent.val_mk, Submodule.mkQ_apply, Ideal.cotangentEquivIdeal_apply, Algebra.Extension.Hom.subToKer_apply_coe, Ideal.Quotient.mk_eq_mk, Algebra.Extension.Hom.toAlgHom_apply
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
⊢ Function.Surjective (α := P.CotangentSpace) (β := Ω[S⁄R]) (⇑P.toKaehler : (a : P.CotangentSpace) → Ω[S⁄R])

Tactic:
mapBaseChange_surjective _ _ _ P.algebraMap_surjective

Premises used: Algebra.Extension.algebraMap_surjective, KaehlerDifferential.mapBaseChange_surjective
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
⊢ Function.Exact (M := P.Cotangent) (N := P.CotangentSpace) (P := Ω[S⁄R])
    (⇑P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace) (⇑P.toKaehler : (a : P.CotangentSpace) → Ω[S⁄R])

Tactic:
exact_kerCotangentToTensor_mapBaseChange _ _ _ P.algebraMap_surjective

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, Ideal.Cotangent, Algebra.Extension.algebraMap_surjective, KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange, Submodule.quotientRel, Algebra.Extension.Cotangent
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
⊢ AddCommGroup ↥P.cotangentComplex.ker

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
R₀ : Type u_2
inst_24 : CommRing R₀
inst_25 : Algebra R₀ S
inst_26 : Module.{u_2, u_1} R₀ P.Cotangent
inst_27 : IsScalarTower.{u_2, v, u_1} R₀ S P.Cotangent
⊢ Module.{u_2, u_1} R₀ ↥P.cotangentComplex.ker

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u_1, u, v} R S
x y : P.H1Cotangent
⊢ (↑(x + y) : P.Cotangent) = (↑x : P.Cotangent) + (↑y : P.Cotangent)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u_1, u, v} R S
⊢ Eq.{u_1 + 1} (α := P.Cotangent) (↑0 : P.Cotangent) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u_2, u, v} R S
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ S
inst_5 : Module.{u_1, u_2} R₀ P.Cotangent
inst_6 : IsScalarTower.{u_1, v, u_2} R₀ S P.Cotangent
r : R₀
x : P.H1Cotangent
⊢ (↑(r • x) : P.Cotangent) = r • (↑x : P.Cotangent)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
P : Extension.{u_3, u, v} R S
R₁ : Type u_1
R₂ : Type u_2
inst_24 : CommRing R₁
inst_25 : CommRing R₂
inst_26 : Algebra R₁ R₂
inst_27 : Algebra R₁ S
inst_28 : Algebra R₂ S
inst_29 : Module.{u_1, u_3} R₁ P.Cotangent
inst_30 : IsScalarTower.{u_1, v, u_3} R₁ S P.Cotangent
inst_31 : Module.{u_2, u_3} R₂ P.Cotangent
inst_32 : IsScalarTower.{u_2, v, u_3} R₂ S P.Cotangent
inst_33 : IsScalarTower.{u_1, u_2, u_3} R₁ R₂ P.Cotangent
⊢ IsScalarTower.{u_1, u_2, u_3} R₁ R₂ ↥P.cotangentComplex.ker

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u_1, u, v} R S
rw : (∀ (y : ↥P.cotangentComplex.ker), y = 0) ↔ ∀ (x : ↥P.cotangentComplex.ker), (↑x : P.Cotangent) = 0
⊢ Subsingleton.{u_1 + 1} ↥P.cotangentComplex.ker ↔
    Function.Injective (α := P.Cotangent) (β := P.CotangentSpace)
      (⇑P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace)

Tactic:
rw [← LinearMap.ker_eq_bot, Submodule.eq_bot_iff, subsingleton_iff_forall_eq 0, Subtype.forall']

Premises used: LinearMap.ker_eq_bot, subsingleton_iff_forall_eq, Submodule.eq_bot_iff, OfNat.ofNat, Subtype.forall'
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u_1, u, v} R S
⊢ (∀ (y : ↥P.cotangentComplex.ker), y = 0) ↔ ∀ (x : ↥P.cotangentComplex.ker), (↑x : P.Cotangent) = 0

Tactic:
simp only [Subtype.ext_iff, Submodule.coe_zero]

Premises used: Submodule.coe_zero, Subtype.ext_iff
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u_1, u, v} R S
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := P.H1Cotangent) (β := P.Cotangent)
    (⇑h1Cotangentι : (a : P.H1Cotangent) → P.Cotangent)

Tactic:
Subtype.val_injective

Premises used: Subtype.val_injective, Algebra.Extension.H1Cotangent
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u_1, u, v} R S
x y : P.H1Cotangent
e : (↑x : P.Cotangent) = (↑y : P.Cotangent)
⊢ x = y

Tactic:
Subtype.ext e

Premises used: Algebra.Extension.H1Cotangent, Subtype.ext
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u_1, u, v} R S
rw : P.cotangentComplex.ker = LinearMap.range h1Cotangentι
⊢ Function.Exact (M := P.H1Cotangent) (N := P.Cotangent) (P := P.CotangentSpace)
    (⇑h1Cotangentι : (a : P.H1Cotangent) → P.Cotangent) (⇑P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace)

Tactic:
rw [LinearMap.exact_iff]

Premises used: LinearMap.exact_iff
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u_1, u, v} R S
⊢ P.cotangentComplex.ker = LinearMap.range h1Cotangentι

Tactic:
(Submodule.range_subtype _).symm

Premises used: Set.Mem, Algebra.Extension.H1Cotangent, Algebra.Extension.h1Cotangentι, Eq.symm, Submodule.range_subtype
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u_1, u, v} R S
⊢ P.cotangentComplex.ker = LinearMap.range h1Cotangentι

Tactic:
exact (Submodule.range_subtype _).symm

Premises used: Eq.symm, Submodule.range_subtype
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
f : P.Hom P'
refine :
  ∀ (x : P.Cotangent) (hx : x ∈ P.cotangentComplex.ker),
    Membership.mem (α := P'.Cotangent) (γ := Submodule S P'.Cotangent)
      (Submodule.restrictScalars S P'.cotangentComplex.ker)
      ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) x : P'.Cotangent)
⊢ LinearMap.{v, v, u_1, w'} (RingHom.id S) P.H1Cotangent P'.H1Cotangent

Tactic:
refine (Cotangent.map f).restrict (p := LinearMap.ker P.cotangentComplex)
    (q := (LinearMap.ker P'.cotangentComplex).restrictScalars S) fun x hx ↦ ?_

Premises used: LinearMap.restrict, Algebra.Extension.Cotangent.map
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
f : P.Hom P'
x : P.Cotangent
hx : x ∈ P.cotangentComplex.ker
⊢ Eq (α := P.CotangentSpace) ((P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace) x : P.CotangentSpace)
    (0 : P.CotangentSpace)

Tactic:
simp only [LinearMap.mem_ker, Submodule.restrictScalars_mem] at hx ⊢

Premises used: LinearMap.mem_ker, Submodule.restrictScalars_mem
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
f : P.Hom P'
x : P.Cotangent
hx :
  Eq (α := P.CotangentSpace) ((P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace) x : P.CotangentSpace)
    (0 : P.CotangentSpace)
⊢ Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace)
        ((P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace) x) :
      P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace) 0 : P'.CotangentSpace)

Tactic:
apply_fun (CotangentSpace.map f) at hx

Premises used: Algebra.Extension.CotangentSpace.map