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.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
r : R₁
s : R₂
m : P.Cotangent
smul_assoc :
  HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) (r • s) : S) m =
    HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
      (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
⊢ (r • s) • m = r • s • m

Tactic:
change algebraMap R₂ S (r • s) • m = (algebraMap _ S r) • (algebraMap _ S s) • m

Premises used: Algebra.algebraMap, HSMul.hSMul, DFunLike.coe
-- 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
r : R₁
s : R₂
m : P.Cotangent
smul_assoc :
  HSMul.hSMul.{v, w, w} (α := S)
      ((algebraMap R₂ S : (a : R₂) → S) (HMul.hMul (α := R₂) ((algebraMap R₁ R₂ : (a : R₁) → R₂) r : R₂) s) : S) m =
    HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
      (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
smul_assoc₁ :
  HMul.hMul (α := S) (β := S) ((algebraMap R₂ S : (a : R₂) → S) ((algebraMap R₁ R₂ : (a : R₁) → R₂) r : R₂) : S)
        ((algebraMap R₂ S : (a : R₂) → S) s : S) •
      m =
    HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
      (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
smul_assoc₂ :
  HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) ((algebraMap R₁ R₂ : (a : R₁) → R₂) r : R₂) : S)
      (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m) =
    HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
      (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
smul_assoc₃ smul_assoc₄ :
  HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
      (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m) =
    HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
      (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)
⊢ HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) (r • s) : S) m =
    HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₁ S : (a : R₁) → S) r : S)
      (HSMul.hSMul.{v, w, w} (α := S) ((algebraMap R₂ S : (a : R₂) → S) s : S) m)

Tactic:
rw [Algebra.smul_def, map_mul, mul_smul, ← IsScalarTower.algebraMap_apply]

Premises used: map_mul, Algebra.smul_def, IsScalarTower.algebraMap_apply, 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_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ S
r : R₀
x : P.Cotangent
⊢ (r • x).val = P.σ ((algebraMap R₀ S : (a : R₀) → S) r) • x.val

Tactic:
rfl

Premises used: Algebra.Extension.Cotangent.val, Quot.map, Quotient.map', 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
r : S
x : P.Cotangent
⊢ (r • x).val = P.σ r • x.val

Tactic:
rfl

Premises used: Algebra.Extension.Cotangent.val, Quot.map, Quotient.map', 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
r : P.Ring
x : P.Cotangent
rw : (P.σ ((algebraMap P.Ring S : (a : P.Ring) → S) r) - r) • x.val = 0
⊢ (r • x).val = r • x.val

Tactic:
rw [val_smul''', ← sub_eq_zero, ← sub_smul]

Premises used: sub_eq_zero, Algebra.Extension.Cotangent.val_smul''', 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 : P.Ring
x : P.Cotangent
⊢ P.σ ((algebraMap P.Ring S : (a : P.Ring) → S) r) - r ∈ 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 : P.Ring
x : P.Cotangent
⊢ (P.σ ((algebraMap P.Ring S : (a : P.Ring) → S) r) - r) • x.val = 0

Tactic:
exact Cotangent.smul_eq_zero_of_mem _ (by simp) _

Premises used: Algebra.Extension.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 : R
x : P.Cotangent
rw : (HSMul.hSMul (α := P.Ring) ((algebraMap R P.Ring : (a : R) → P.Ring) r : P.Ring) x).val = r • x.val
rw₁ : HSMul.hSMul (α := P.Ring) ((algebraMap R P.Ring : (a : R) → P.Ring) r : P.Ring) x.val = r • x.val
rw₂ rw₃ : r • x.val = r • x.val
⊢ (r • x).val = r • x.val

Tactic:
rw [← algebraMap_smul P.Ring, val_smul', algebraMap_smul]

Premises used: algebraMap_smul, Algebra.Extension.Cotangent.val_smul', Algebra.Extension.Ring
-- 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.307683
S' : Type ?u.307686
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.307810
S'' : Type ?u.307813
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
x y : P.Cotangent
⊢ (x + y).val = x.val + y.val

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.307683
S' : Type ?u.307686
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.307810
S'' : Type ?u.307813
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
x : P.Ring
y : P.Cotangent
⊢ (x • y).val = HSMul.hSMul (α := P.Ring) ((RingHom.id P.Ring : (a : P.Ring) → P.Ring) x : P.Ring) y.val

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.310168
S' : Type ?u.310171
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.310295
S'' : Type ?u.310298
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
x y : ↥P.ker
⊢ of ((P.ker.toCotangent : (a : ↥P.ker) → P.ker.Cotangent) (x + y)) =
    HAdd.hAdd (α := P.Cotangent) (of ((P.ker.toCotangent : (a : ↥P.ker) → P.ker.Cotangent) x))
      (of ((P.ker.toCotangent : (a : ↥P.ker) → P.ker.Cotangent) y))

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.310168
S' : Type ?u.310171
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.310295
S'' : Type ?u.310298
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Extension R'' S''
x : P.Ring
y : ↥P.ker
⊢ val (of ((P.ker.toCotangent : (a : ↥P.ker) → P.ker.Cotangent) (x • y))) =
    (HSMul.hSMul (α := P.Ring) (β := P.Cotangent) ((RingHom.id P.Ring : (a : P.Ring) → P.Ring) x : P.Ring)
        (of ((P.ker.toCotangent : (a : ↥P.ker) → P.ker.Cotangent) y))).val

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
x : ↥P.ker
⊢ Eq.{w + 1} (α := P.ker.Cotangent) (val ((mk : (a : ↥P.ker) → P.Cotangent) x))
    ((P.ker.toCotangent : (a : ↥P.ker) → P.ker.Cotangent) x)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, 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
⊢ Function.Surjective.{w + 1, w + 1} (α := ↥P.ker) (β := P.Cotangent) (⇑mk : (a : ↥P.ker) → P.Cotangent)

Tactic:
fun x ↦ Ideal.toCotangent_surjective P.ker x.val

Premises used: Algebra.Extension.ker, Submodule.Quotient.mk, Algebra.Extension.Cotangent.val, Ideal.toCotangent_surjective, Function.Surjective, Algebra.Extension.Cotangent.of, 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.{u_1, u, v} R S
x : ↥P.ker
⊢ Eq (α := P.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x : P.Cotangent) (0 : P.Cotangent) ↔
    (↑x : P.Ring) ∈ HPow.hPow (β := ℕ) P.ker 2

Tactic:
simp [Cotangent.ext_iff, Ideal.toCotangent_eq_zero]

Premises used: Ideal.toCotangent_eq_zero, Algebra.Extension.Cotangent.ext_iff
-- 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.ker
⊢ Eq (α := P.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x : P.Cotangent)
      ((mk : (a : ↥P.ker) → P.Cotangent) y : P.Cotangent) ↔
    (↑x : P.Ring) - (↑y : P.Ring) ∈ HPow.hPow (β := ℕ) P.ker 2

Tactic:
simp [Extension.Cotangent.ext_iff, Ideal.toCotangent_eq]

Premises used: Ideal.toCotangent_eq, Algebra.Extension.Cotangent.ext_iff
-- 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) (hx : x ∈ P.ker),
    Membership.mem (γ := Submodule P.Ring ↥P.ker) (LinearMap.ker mk)
        (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) x hx) ↔
      Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) x hx ∈ HSMul.hSMul (β := Submodule P.Ring ↥P.ker) P.ker ⊤
⊢ LinearMap.ker mk = HSMul.hSMul (β := Submodule P.Ring ↥P.ker) P.ker ⊤

Tactic:
ext ⟨x, hx⟩
-- 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
hx : x ∈ P.ker
⊢ Membership.mem (γ := Submodule P.Ring ↥P.ker) (LinearMap.ker mk)
      (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) x hx) ↔
    Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) x hx ∈ HSMul.hSMul (β := Submodule P.Ring ↥P.ker) P.ker ⊤

Tactic:
simp [LinearMap.mem_ker, mk_eq_zero_iff, Submodule.mem_smul_top_iff, sq]

Premises used: Algebra.Extension.Cotangent.mk_eq_zero_iff, sq, LinearMap.mem_ker, Submodule.mem_smul_top_iff
-- 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
ι : Type u_1
s : ι → P.Ring
hs : Ideal.span (Set.range s) = P.ker
rw :
  ∀ (hs_1 : Submodule.span P.Ring (Set.range s) = P.ker)
    (hs_2 :
      Eq.{w + 1} (α := Submodule P.Ring ↥P.ker)
        (Submodule.span P.Ring (Set.range fun (i : ι) ↦ Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)) ⊤),
    Eq.{w + 1} (α := Submodule S P.Cotangent)
      (Submodule.span S
        (Set.range fun (i : ι) ↦
          (mk : (a : ↥P.ker) → P.Cotangent) (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)))
      ⊤
hs₁ : ∀ (hs : Submodule.span P.Ring (Set.range s) = P.ker) (i : ι), s i ∈ P.ker
⊢ Eq.{w + 1} (α := Submodule S P.Cotangent)
    (Submodule.span S
      (Set.range fun (i : ι) ↦
        (mk : (a : ↥P.ker) → P.Cotangent) (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)))
    ⊤

Tactic:
rw [Ideal.span, ← Submodule.span_range_subtype_eq_top_iff] at hs

Premises used: Ideal.span, Submodule.span_range_subtype_eq_top_iff
-- 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
ι : Type u_1
s : ι → P.Ring
hs_1 : Ideal.span (Set.range s) = P.ker
hs_2 : Submodule.span P.Ring (Set.range s) = P.ker
hs :
  Eq.{w + 1} (α := Submodule P.Ring ↥P.ker)
    (Submodule.span P.Ring (Set.range fun (i : ι) ↦ Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)) ⊤
hs₁ :
  Eq.{w + 1} (α := Submodule P.Ring P.Cotangent)
    (Submodule.span P.Ring
      (Set.range fun (i : ι) ↦
        (mk : (a : ↥P.ker) → P.Cotangent) (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)))
    ⊤
⊢ Eq.{w + 1} (α := Submodule S P.Cotangent)
    (Submodule.span S
      (Set.range fun (i : ι) ↦
        (mk : (a : ↥P.ker) → P.Cotangent) (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)))
    ⊤

Tactic:
apply Submodule.span_eq_top_of_span_eq_top (R := P.Ring)

Premises used: Submodule.span_eq_top_of_span_eq_top, Algebra.Extension.Ring
-- 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
ι : Type u_1
s : ι → P.Ring
hs_1 : Ideal.span (Set.range s) = P.ker
hs_2 : Submodule.span P.Ring (Set.range s) = P.ker
hs :
  Eq.{w + 1} (α := Submodule P.Ring ↥P.ker)
    (Submodule.span P.Ring (Set.range fun (i : ι) ↦ Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)) ⊤
hs₁ :
  Eq.{w + 1} (α := Submodule P.Ring P.Cotangent)
    (Submodule.span P.Ring
      (Set.range.{w, u_1 + 1} (ι := ι)
        (Function.comp (β := ↥P.ker) (⇑mk : (a : ↥P.ker) → P.Cotangent) fun (i : ι) ↦
          Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)))
    ⊤
hs₂ :
  Eq.{w + 1} (α := Submodule P.Ring P.Cotangent)
    (Submodule.span P.Ring
      (Set.image (α := ↥P.ker) (⇑mk : (a : ↥P.ker) → P.Cotangent)
        (Set.range fun (i : ι) ↦ Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)))
    ⊤
hs₃ :
  Eq.{w + 1} (α := Submodule P.Ring P.Cotangent)
    (Submodule.map mk
      (Submodule.span P.Ring (Set.range fun (i : ι) ↦ Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)))
    ⊤
hs₄ : Eq.{w + 1} (α := Submodule P.Ring P.Cotangent) (Submodule.map mk ⊤) ⊤
hs₅ : Eq.{w + 1} (α := Submodule P.Ring P.Cotangent) (LinearMap.range mk) ⊤
hs₆ hs₇ : Eq.{w + 1} (α := Submodule P.Ring P.Cotangent) ⊤ ⊤
⊢ Eq.{w + 1} (α := Submodule P.Ring P.Cotangent)
    (Submodule.span P.Ring
      (Set.range fun (i : ι) ↦
        (mk : (a : ↥P.ker) → P.Cotangent) (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (s i) ⋯)))
    ⊤

Tactic:
rw [← Function.comp_def, Set.range_comp, ← Submodule.map_span, hs, Submodule.map_top,
      LinearMap.range_eq_top_of_surjective _ mk_surjective]

Premises used: Set.range_comp, LinearMap.range_eq_top_of_surjective, Submodule.map_top, Function.comp_def, Algebra.Extension.Cotangent.mk_surjective, Submodule.map_span
-- 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
ι : Type u_1
s : ι → P.Ring
hs_1 : Ideal.span (Set.range s) = P.ker
hs : Submodule.span P.Ring (Set.range s) = P.ker
⊢ ∀ (i : ι), s i ∈ P.ker

Tactic:
simp [← hs, Ideal.mem_span_range_self]

Premises used: Ideal.mem_span_range_self
-- 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.337215
S'' : Type ?u.337218
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' S''
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'
x_1 : P.Cotangent
x : P.Ring
hx : x ∈ P.ker
⊢ Membership.mem (γ := Submodule P.Ring P.Ring)
    (Ideal.comap (F := AlgHom.{u, w, u_3} R P.Ring P'.Ring) f.toAlgHom P'.ker) x

Tactic:
simpa using RingHom.congr_arg (algebraMap S S') hx

Premises used: Algebra.algebraMap, RingHom.congr_arg
-- 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.337215
S'' : Type ?u.337218
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' S''
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 : S
x : P.Cotangent
e :
  ∀ (x : ↥P.ker),
    val
        (of
          (((P.ker.mapCotangent P'.ker f.toAlgHom ⋯ :
                LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
              (a : P.ker.Cotangent) → P'.ker.Cotangent)
            (HSMul.hSMul (β := P.Cotangent) r ((mk : (a : ↥P.ker) → P.Cotangent) x : P.Cotangent)).val)) =
      (HSMul.hSMul (α := S) (β := P'.Cotangent) ((RingHom.id S : (a : S) → S) r : S)
          (of
            (((P.ker.mapCotangent P'.ker f.toAlgHom ⋯ :
                  LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
                (a : P.ker.Cotangent) → P'.ker.Cotangent)
              (val ((mk : (a : ↥P.ker) → P.Cotangent) x))))).val
⊢ val
      (of
        (((P.ker.mapCotangent P'.ker f.toAlgHom ⋯ :
              LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
            (a : P.ker.Cotangent) → P'.ker.Cotangent)
          (r • x).val)) =
    (HSMul.hSMul (α := S) (β := P'.Cotangent) ((RingHom.id S : (a : S) → S) r : S)
        (of
          (((P.ker.mapCotangent P'.ker f.toAlgHom ⋯ :
                LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
              (a : P.ker.Cotangent) → P'.ker.Cotangent)
            x.val))).val

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

Premises used: Algebra.Extension.Cotangent.mk_surjective, 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_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.337215
S'' : Type ?u.337218
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' S''
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 : S
x : ↥P.ker
e :
  ∀ (r : P.Ring),
    val
        (of
          (((P.ker.mapCotangent P'.ker f.toAlgHom ⋯ :
                LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
              (a : P.ker.Cotangent) → P'.ker.Cotangent)
            (HSMul.hSMul.{v, w, w} (α := S) (β := P.Cotangent) ((algebraMap P.Ring S : (a : P.Ring) → S) r : S)
                ((mk : (a : ↥P.ker) → P.Cotangent) x : P.Cotangent)).val)) =
      (HSMul.hSMul (α := S) (β := P'.Cotangent)
          ((RingHom.id S : (a : S) → S) ((algebraMap P.Ring S : (a : P.Ring) → S) r : S) : S)
          (of
            (((P.ker.mapCotangent P'.ker f.toAlgHom ⋯ :
                  LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
                (a : P.ker.Cotangent) → P'.ker.Cotangent)
              (val ((mk : (a : ↥P.ker) → P.Cotangent) x))))).val
⊢ val
      (of
        (((P.ker.mapCotangent P'.ker f.toAlgHom ⋯ :
              LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
            (a : P.ker.Cotangent) → P'.ker.Cotangent)
          (HSMul.hSMul (β := P.Cotangent) r ((mk : (a : ↥P.ker) → P.Cotangent) x : P.Cotangent)).val)) =
    (HSMul.hSMul (α := S) (β := P'.Cotangent) ((RingHom.id S : (a : S) → S) r : S)
        (of
          (((P.ker.mapCotangent P'.ker f.toAlgHom ⋯ :
                LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
              (a : P.ker.Cotangent) → P'.ker.Cotangent)
            (val ((mk : (a : ↥P.ker) → P.Cotangent) x))))).val

Tactic:
obtain ⟨r, rfl⟩ := P.algebraMap_surjective r

Premises used: Algebra.Extension.algebraMap_surjective, 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_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.337215
S'' : Type ?u.337218
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' S''
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'
x : ↥P.ker
r : P.Ring
e :
  (P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
      (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
        (((f.toAlgHom : AlgHom.{u, w, u_3} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑(r • x) : P.Ring)) ⋯) =
    (HSMul.hSMul.{v, u_3, u_3} (α := S) (β := P'.Cotangent) ((algebraMap P.Ring S : (a : P.Ring) → S) r : S)
        (of
          ((P'.ker.toCotangent : (a : ↥P'.ker) → P'.ker.Cotangent)
            (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
              (((f.toAlgHom : AlgHom.{u, w, u_3} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯)))).val
⊢ val
      (of
        (((P.ker.mapCotangent P'.ker f.toAlgHom ⋯ :
              LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
            (a : P.ker.Cotangent) → P'.ker.Cotangent)
          (HSMul.hSMul.{v, w, w} (α := S) (β := P.Cotangent) ((algebraMap P.Ring S : (a : P.Ring) → S) r : S)
              ((mk : (a : ↥P.ker) → P.Cotangent) x : P.Cotangent)).val)) =
    (HSMul.hSMul (α := S) (β := P'.Cotangent)
        ((RingHom.id S : (a : S) → S) ((algebraMap P.Ring S : (a : P.Ring) → S) r : S) : S)
        (of
          (((P.ker.mapCotangent P'.ker f.toAlgHom ⋯ :
                LinearMap.{u, u, w, u_3} (RingHom.id R) P.ker.Cotangent P'.ker.Cotangent) :
              (a : P.ker.Cotangent) → P'.ker.Cotangent)
            (val ((mk : (a : ↥P.ker) → P.Cotangent) x))))).val

Tactic:
simp only [algebraMap_smul, val_smul', val_mk, val_of, Ideal.mapCotangent_toCotangent,
      RingHomCompTriple.comp_apply, ← (Ideal.toCotangent _).map_smul]

Premises used: Algebra.Extension.Cotangent.val_mk, Ideal.mapCotangent_toCotangent, algebraMap_smul, Algebra.Extension.Cotangent.val_smul', LinearMap.map_smul, RingHomCompTriple.comp_apply, Ideal.toCotangent, Algebra.Extension.Cotangent.val_of