awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.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_1
S' : Type u_2
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{u_3, u_1, u_2} R' S'
R'' : Type ?u.163370
S'' : Type ?u.163373
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R R''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : Algebra R S'
inst_16 : IsScalarTower R R' S'
f : P.Hom P'
⊢ ∀ (r : R),
    (↑(↑f.toRingHom : P.Ring →* P'.Ring) : OneHom P.Ring P'.Ring).toFun ((algebraMap R P.Ring : (a : R) → P.Ring) r) =
      (algebraMap R P'.Ring : (a : R) → P'.Ring) r

Tactic:
simp [← IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Extension.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_2
S' : Type u_1
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{u_3, u_2, u_1} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
f : P.Hom P'
x : P.Ring
⊢ Eq.{u_3 + 1} (α := P'.Ring)
    (((f.toAlgHom : AlgHom.{u, w, u_3} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
    ((f.toRingHom : (a : P.Ring) → P'.Ring) x : P'.Ring)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Extension.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_2
S' : Type u_1
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{u_3, u_2, u_1} 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 : AlgHom.{u, w, u_3} R P.Ring P'.Ring
H :
  Eq (α := AlgHom.{u, w, u_1} R P.Ring S') (AlgHom.comp (IsScalarTower.toAlgHom R P'.Ring S') f)
    (AlgHom.comp (IsScalarTower.toAlgHom R S S') (IsScalarTower.toAlgHom R P.Ring S))
⊢ (ofAlgHom f H).toAlgHom = f

Tactic:
rfl

Premises used: Algebra.Extension.Hom.toAlgHom, rfl
-- Module: Mathlib.RingTheory.Extension.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.175505
S' : Type ?u.175508
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.175632
S'' : Type ?u.175635
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R R''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
⊢ ∀ (x : R),
    Eq (α := P.Ring)
      ((RingHom.id P.Ring : (a : P.Ring) → P.Ring) ((algebraMap R P.Ring : (a : R) → P.Ring) x : P.Ring) : P.Ring)
      ((algebraMap R P.Ring : (a : R) → P.Ring) ((algebraMap R R : (a : R) → R) x) : P.Ring)

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.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.175505
S' : Type ?u.175508
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.175632
S'' : Type ?u.175635
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R R''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
⊢ ∀ (x : P.Ring),
    Eq.{v + 1} (α := S)
      ((algebraMap P.Ring S : (a : P.Ring) → S) ((RingHom.id P.Ring : (a : P.Ring) → P.Ring) x : P.Ring) : S)
      ((algebraMap S S : (a : S) → S) ((algebraMap P.Ring S : (a : P.Ring) → S) x : S) : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.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
H :
  ∀ (x : P.Ring),
    Eq (α := P.Ring) (((Hom.id P).toAlgHom : (a : P.Ring) → P.Ring) x : P.Ring)
      ((AlgHom.id R P.Ring : (a : P.Ring) → P.Ring) x : P.Ring)
⊢ (Hom.id P).toAlgHom = AlgHom.id R P.Ring

Tactic:
ext1
-- Module: Mathlib.RingTheory.Extension.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
x : P.Ring
⊢ Eq (α := P.Ring) (((Hom.id P).toAlgHom : (a : P.Ring) → P.Ring) x : P.Ring)
    ((AlgHom.id R P.Ring : (a : P.Ring) → P.Ring) x : P.Ring)

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.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_1
S' : Type u_2
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{u_3, u_1, u_2} R' S'
R'' : Type u_4
S'' : Type u_5
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension.{u_6, u_4, u_5} R'' S''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R R''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : IsScalarTower R R' R''
inst_16 : IsScalarTower S S' S''
f : P'.Hom P''
g : P.Hom P'
⊢ ∀ (x : R),
    Eq.{u_6 + 1} (α := P''.Ring)
      ((f.toRingHom.comp g.toRingHom : (a : P.Ring) → P''.Ring) ((algebraMap R P.Ring : (a : R) → P.Ring) x) : P''.Ring)
      ((algebraMap R'' P''.Ring : (a : R'') → P''.Ring) ((algebraMap R R'' : (a : R) → R'') x) : P''.Ring)

Tactic:
simp [← IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Extension.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_1
S' : Type u_2
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{u_3, u_1, u_2} R' S'
R'' : Type u_4
S'' : Type u_5
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension.{u_6, u_4, u_5} R'' S''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R R''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : IsScalarTower R R' R''
inst_16 : IsScalarTower S S' S''
f : P'.Hom P''
g : P.Hom P'
⊢ ∀ (x : P.Ring),
    Eq.{u_5 + 1} (α := S'')
      ((algebraMap P''.Ring S'' : (a : P''.Ring) → S'')
          ((f.toRingHom.comp g.toRingHom : (a : P.Ring) → P''.Ring) x : P''.Ring) :
        S'')
      ((algebraMap S S'' : (a : S) → S'') ((algebraMap P.Ring S : (a : P.Ring) → S) x : S) : S'')

Tactic:
simp [← IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Extension.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_1
S' : Type u_2
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{u_3, u_1, u_2} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
f : P.Hom P'
toRingHom :
  ∀ (x : P.Ring),
    Eq.{u_3 + 1} (α := P'.Ring) ((Hom.toRingHom (f.comp (Hom.id P)) : (a : P.Ring) → P'.Ring) x : P'.Ring)
      ((f.toRingHom : (a : P.Ring) → P'.Ring) x : P'.Ring)
⊢ f.comp (Hom.id P) = f

Tactic:
ext
-- Module: Mathlib.RingTheory.Extension.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_1
S' : Type u_2
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{u_3, u_1, u_2} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
f : P.Hom P'
x : P.Ring
⊢ Eq.{u_3 + 1} (α := P'.Ring) ((toRingHom (f.comp (Hom.id P)) : (a : P.Ring) → P'.Ring) x : P'.Ring)
    ((f.toRingHom : (a : P.Ring) → P'.Ring) x : P'.Ring)

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.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_1
S' : Type u_2
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{u_3, u_1, u_2} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
f : P.Hom P'
toRingHom :
  ∀ (x : P.Ring),
    Eq.{u_3 + 1} (α := P'.Ring) ((Hom.toRingHom ((Hom.id P').comp f) : (a : P.Ring) → P'.Ring) x : P'.Ring)
      ((f.toRingHom : (a : P.Ring) → P'.Ring) x : P'.Ring)
⊢ (Hom.id P').comp f = f

Tactic:
ext
-- Module: Mathlib.RingTheory.Extension.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_1
S' : Type u_2
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{u_3, u_1, u_2} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
f : P.Hom P'
x : P.Ring
⊢ Eq.{u_3 + 1} (α := P'.Ring) ((toRingHom ((Hom.id P').comp f) : (a : P.Ring) → P'.Ring) x : P'.Ring)
    ((f.toRingHom : (a : P.Ring) → P'.Ring) x : P'.Ring)

Tactic:
simp [Hom.id]

Premises used: Algebra.Extension.Hom.id
-- Module: Mathlib.RingTheory.Extension.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_1
S' : Type u_2
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{u_3, u_1, u_2} R' S'
R'' : Type ?u.193588
S'' : Type ?u.193591
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R R''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
f : P.Hom P'
alg : Algebra.{w, u_3} P.Ring P'.Ring
halg : algebraMap P.Ring P'.Ring = f.toRingHom
x : ↥P.ker
⊢ Membership.mem (α := P'.Ring) P'.ker ((f.toRingHom : (a : P.Ring) → P'.Ring) (↑x : P.Ring) : P'.Ring)

Tactic:
simp [show algebraMap P.Ring S x = 0 from x.2]

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.Extension.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_1
S' : Type u_2
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{u_3, u_1, u_2} R' S'
R'' : Type ?u.193588
S'' : Type ?u.193591
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R R''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
f : P.Hom P'
alg : Algebra.{w, u_3} P.Ring P'.Ring
halg : algebraMap P.Ring P'.Ring = f.toRingHom
⊢ ∀ (m : P.Ring) (x : ↥P.ker),
    Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker) ((f.toRingHom : (a : P.Ring) → P'.Ring) (↑(m • x) : P.Ring)) ⋯ =
      HSMul.hSMul (α := P.Ring) (β := ↥P'.ker) ((RingHom.id P.Ring : (a : P.Ring) → P.Ring) m : P.Ring)
        (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker) ((f.toRingHom : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯ :
          ↥P'.ker)

Tactic:
simp [Algebra.smul_def, ← halg]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Extension.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.212472
S' : Type ?u.212475
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.212599
S'' : Type ?u.212602
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R R''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
T : Type u_1
inst_15 : CommRing T
inst_16 : Algebra R T
x : R
⊢ Eq (α := Ring (R := T) (S := T ⊗[R] S) P.baseChange)
    ((AlgHom.toRingHom TensorProduct.includeRight : (a : P.Ring) → P.baseChange.Ring)
        ((algebraMap R P.Ring : (a : R) → P.Ring) x) :
      Ring (R := T) (S := T ⊗[R] S) P.baseChange)
    ((algebraMap T (Ring (R := T) (S := T ⊗[R] S) P.baseChange) : (a : T) → P.baseChange.Ring)
        ((algebraMap R T : (a : R) → T) x) :
      Ring (R := T) (S := T ⊗[R] S) P.baseChange)

Tactic:
simp [baseChange]

Premises used: Algebra.Extension.baseChange
-- Module: Mathlib.RingTheory.Extension.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.217031
S' : Type ?u.217034
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.217158
S'' : Type ?u.217161
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
P : Extension.{u_1, u, v} R S
x : S
dsimp :
  (algebraMap (P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2) S : (a : P.Ring ⧸ P.ker ^ 2) → S)
      ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ x) :
        P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2) =
    x
⊢ (algebraMap (P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2) S : (a : P.Ring ⧸ P.ker ^ 2) → S)
      (((⇑(Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2)) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) ∘ P.σ) x) =
    x

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Extension.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.217031
S' : Type ?u.217034
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.217158
S'' : Type ?u.217161
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
P : Extension.{u_1, u, v} R S
x : S
⊢ (algebraMap (P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2) S : (a : P.Ring ⧸ P.ker ^ 2) → S)
      ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ x) :
        P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2) =
    x

Tactic:
P.algebraMap_σ x

Premises used: Quotient.liftOn', AddCon.liftOn, Algebra.Extension.algebraMap_σ
-- Module: Mathlib.RingTheory.Extension.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.217031
S' : Type ?u.217034
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.217158
S'' : Type ?u.217161
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
P : Extension.{u_1, u, v} R S
x : S
⊢ (algebraMap (P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2) S : (a : P.Ring ⧸ P.ker ^ 2) → S)
      ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ x) :
        P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2) =
    x

Tactic:
exact P.algebraMap_σ x

Premises used: Algebra.Extension.algebraMap_σ
-- Module: Mathlib.RingTheory.Extension.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.infinitesimal.ker = P.ker.cotangentIdeal

Tactic:
AlgHom.ker_kerSquareLift _

Premises used: AlgHom.ker_kerSquareLift
-- Module: Mathlib.RingTheory.Extension.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
x y : P.Cotangent
e : x.val = y.val
⊢ x = y

Tactic:
e

Premises used: Algebra.Extension.Cotangent.val, Algebra.Extension.Cotangent
-- Module: Mathlib.RingTheory.Extension.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
x y : P.Cotangent
⊢ (x + y).val = x.val + y.val

Tactic:
rfl

Premises used: Algebra.Extension.Cotangent.val, rfl
-- Module: Mathlib.RingTheory.Extension.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
⊢ Eq.{w + 1} (α := P.ker.Cotangent) (val 0) 0

Tactic:
rfl

Premises used: Algebra.Extension.Cotangent.val, rfl
-- Module: Mathlib.RingTheory.Extension.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
w z : P.ker.Cotangent
⊢ of (w + z) = of w + of z

Tactic:
rfl

Premises used: rfl, Algebra.Extension.Cotangent.of
-- Module: Mathlib.RingTheory.Extension.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
⊢ Eq.{w + 1} (α := P.Cotangent) (of 0) 0

Tactic:
rfl

Premises used: rfl, Algebra.Extension.Cotangent.of
-- Module: Mathlib.RingTheory.Extension.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
x : P.Cotangent
⊢ of x.val = x

Tactic:
rfl

Premises used: Algebra.Extension.Cotangent.val, rfl, Algebra.Extension.Cotangent.of
-- Module: Mathlib.RingTheory.Extension.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
w : P.ker.Cotangent
⊢ (of w).val = w

Tactic:
rfl

Premises used: Algebra.Extension.Cotangent.val, rfl, Algebra.Extension.Cotangent.of
-- Module: Mathlib.RingTheory.Extension.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
x y : P.Cotangent
⊢ (x - y).val = x.val - y.val

Tactic:
rfl

Premises used: Algebra.Extension.Cotangent.val, rfl
-- Module: Mathlib.RingTheory.Extension.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
p : P.Ring
hp : p ∈ P.ker
m : P.ker.Cotangent
⊢ p • m = 0

Tactic:
Ideal.Cotangent.smul_eq_zero_of_mem hp m

Premises used: Ideal.Cotangent.smul_eq_zero_of_mem
-- Module: Mathlib.RingTheory.Extension.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.238586
S' : Type ?u.238589
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.238713
S'' : Type ?u.238716
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
r s : S
x : P.Cotangent
⊢ P.σ (r * s) - P.σ r * P.σ s ∈ P.ker

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.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.238586
S' : Type ?u.238589
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.238713
S'' : Type ?u.238716
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
r s : S
x : P.Cotangent
⊢ (P.σ (r * s) - P.σ r * P.σ s) • x = 0

Tactic:
have := smul_eq_zero_of_mem (P.σ (r * s) - (P.σ r * P.σ s) : P.Ring) (by simp) x
-- Module: Mathlib.RingTheory.Extension.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.238586
S' : Type ?u.238589
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.238713
S'' : Type ?u.238716
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
r s : S
x : P.Cotangent
this : (P.σ (r * s) - P.σ r * P.σ s) • x = 0
⊢ (r * s) • x = r • s • x

Tactic:
simpa only [sub_smul, mul_smul, sub_eq_zero] using this

Premises used: sub_eq_zero, sub_smul, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Extension.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.238586
S' : Type ?u.238589
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.238713
S'' : Type ?u.238716
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
x : P.Cotangent
⊢ P.σ 1 - 1 ∈ P.ker

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.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.238586
S' : Type ?u.238589
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.238713
S'' : Type ?u.238716
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
x : P.Cotangent
⊢ (P.σ 1 - 1) • x = 0

Tactic:
have := smul_eq_zero_of_mem (P.σ 1 - 1 : P.Ring) (by simp) x
-- Module: Mathlib.RingTheory.Extension.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.238586
S' : Type ?u.238589
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.238713
S'' : Type ?u.238716
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
x : P.Cotangent
this : (P.σ 1 - 1) • x = 0
⊢ HSMul.hSMul.{v, w, w} (α := S) 1 x = x

Tactic:
simpa [sub_eq_zero, sub_smul]

Premises used: sub_eq_zero, sub_smul
-- Module: Mathlib.RingTheory.Extension.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.238586
S' : Type ?u.238589
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.238713
S'' : Type ?u.238716
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
r s : S
x : P.Cotangent
⊢ P.σ (r + s) - (P.σ r + P.σ s) ∈ P.ker

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.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.238586
S' : Type ?u.238589
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.238713
S'' : Type ?u.238716
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
r s : S
x : P.Cotangent
⊢ (P.σ (r + s) - (P.σ r + P.σ s)) • x = 0

Tactic:
have := smul_eq_zero_of_mem (P.σ (r + s) - (P.σ r + P.σ s) : P.Ring) (by simp) x
-- Module: Mathlib.RingTheory.Extension.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.238586
S' : Type ?u.238589
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.238713
S'' : Type ?u.238716
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
r s : S
x : P.Cotangent
this : (P.σ (r + s) - (P.σ r + P.σ s)) • x = 0
⊢ (r + s) • x = r • x + s • x

Tactic:
simpa only [sub_smul, add_smul, sub_eq_zero]

Premises used: sub_eq_zero, sub_smul, add_smul
-- Module: Mathlib.RingTheory.Extension.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.238586
S' : Type ?u.238589
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.238713
S'' : Type ?u.238716
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
x : P.Cotangent
⊢ P.σ 0 ∈ P.ker

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.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.279762
S' : Type ?u.279765
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.279889
S'' : Type ?u.279892
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
R₁ : Type u_1
R₂ : Type u_2
inst_9 : CommRing R₁
inst_10 : CommRing R₂
inst_11 : Algebra R₁ S
inst_12 : Algebra R₂ S
inst_13 : Algebra R₁ R₂
inst_14 : IsScalarTower R₁ R₂ S
smul_assoc : ∀ (x : R₁) (y : R₂) (z : P.Cotangent), (x • y) • z = x • y • z
⊢ IsScalarTower.{u_1, u_2, w} R₁ R₂ P.Cotangent

Tactic:
constructor