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.388327
S' : Type ?u.388330
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.388454
S'' : Type ?u.388457
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'
inst_17 : Algebra R R''
inst_18 : IsScalarTower R R' R''
inst_19 : IsScalarTower R' R'' S''
inst_20 : Algebra R S''
inst_21 : IsScalarTower R R'' S''
inst_22 : IsScalarTower S S' S''
x : TensorProduct.{w, v, w} P.Ring S ↥P.ker
hx :
  Eq.{w + 1} (α := P.Cotangent)
    ((LinearMap.liftBaseChange S Cotangent.mk : (a : S ⊗[P.Ring] ↥P.ker) → P.Cotangent) x : P.Cotangent)
    (0 : P.Cotangent)
refine_1 :
  ∀ (x : ↥P.ker)
    (hx :
      Eq.{w + 1} (α := P.Cotangent)
        ((LinearMap.liftBaseChange S Cotangent.mk : (a : S ⊗[P.Ring] ↥P.ker) → P.Cotangent)
            (((TensorProduct.mk P.Ring S ↥P.ker : (a : S) → ↥P.ker →ₗ[P.Ring] S ⊗[P.Ring] ↥P.ker) 1 :
                (a : ↥P.ker) → S ⊗[P.Ring] ↥P.ker)
              x) :
          P.Cotangent)
        (0 : P.Cotangent)),
    Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker)
      (((TensorProduct.mk P.Ring S ↥P.ker : (a : S) → ↥P.ker →ₗ[P.Ring] S ⊗[P.Ring] ↥P.ker) 1 :
            (a : ↥P.ker) → S ⊗[P.Ring] ↥P.ker)
          x :
        TensorProduct.{w, v, w} P.Ring S ↥P.ker)
      (0 : TensorProduct.{w, v, w} P.Ring S ↥P.ker)
⊢ x = 0

Tactic:
obtain ⟨x, rfl⟩ := TensorProduct.mk_surjective P.Ring P.ker S P.algebraMap_surjective x

Premises used: Algebra.Extension.ker, Membership.mem, Algebra.Extension.algebraMap_surjective, Subtype, Algebra.Extension.Ring, TensorProduct.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.388327
S' : Type ?u.388330
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.388454
S'' : Type ?u.388457
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'
inst_17 : Algebra R R''
inst_18 : IsScalarTower R R' R''
inst_19 : IsScalarTower R' R'' S''
inst_20 : Algebra R S''
inst_21 : IsScalarTower R R'' S''
inst_22 : IsScalarTower S S' S''
x : ↥P.ker
hx :
  Eq.{w + 1} (α := P.Cotangent)
    ((LinearMap.liftBaseChange S Cotangent.mk : (a : S ⊗[P.Ring] ↥P.ker) → P.Cotangent)
        (((TensorProduct.mk P.Ring S ↥P.ker : (a : S) → ↥P.ker →ₗ[P.Ring] S ⊗[P.Ring] ↥P.ker) 1 :
            (a : ↥P.ker) → S ⊗[P.Ring] ↥P.ker)
          x) :
      P.Cotangent)
    (0 : P.Cotangent)
⊢ (↑x : P.Ring) ∈ P.ker * P.ker

Tactic:
simp only [mk_apply, LinearMap.liftBaseChange_tmul, one_smul, Cotangent.mk_eq_zero_iff,
      pow_two] at hx ⊢

Premises used: pow_two, TensorProduct.mk_apply, Algebra.Extension.Cotangent.mk_eq_zero_iff, one_smul, LinearMap.liftBaseChange_tmul
-- 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.388327
S' : Type ?u.388330
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.388454
S'' : Type ?u.388457
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'
inst_17 : Algebra R R''
inst_18 : IsScalarTower R R' R''
inst_19 : IsScalarTower R' R'' S''
inst_20 : Algebra R S''
inst_21 : IsScalarTower R R'' S''
inst_22 : IsScalarTower S S' S''
x : ↥P.ker
hx : (↑x : P.Ring) ∈ P.ker * P.ker
⊢ Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker) (1 ⊗ₜ[P.Ring] x) 0

Tactic:
Submodule.smul_induction_on' (p := fun x (hx : x ∈ P.ker * P.ker) ↦
      (1 : S) ⊗ₜ[P.Ring] (⟨x, Ideal.mul_le_right hx⟩ : P.ker) = 0) (hx := hx) ?_ ?_

Premises used: Submodule.smul_induction_on'
-- 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.388327
S' : Type ?u.388330
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.388454
S'' : Type ?u.388457
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'
inst_17 : Algebra R R''
inst_18 : IsScalarTower R R' R''
inst_19 : IsScalarTower R' R'' S''
inst_20 : Algebra R S''
inst_21 : IsScalarTower R R'' S''
inst_22 : IsScalarTower S S' S''
x : ↥P.ker
hx : (↑x : P.Ring) ∈ P.ker * P.ker
refine_1 :
  ∀ (r : P.Ring) (hr : r ∈ P.ker) (n : P.Ring) (hn : n ∈ P.ker),
    (fun (x : P.Ring) (hx : x ∈ P.ker * P.ker) ↦
        Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker)
          (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) x ⋯) 0)
      (r • n) ⋯
refine_1₁ :
  ∀ (x : P.Ring) (hx : x ∈ P.ker • P.ker) (y : P.Ring) (hy : y ∈ P.ker • P.ker),
    (fun (x : P.Ring) (hx : x ∈ P.ker * P.ker) ↦
          Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker)
            (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) x ⋯) 0)
        x hx →
      (fun (x : P.Ring) (hx : x ∈ P.ker * P.ker) ↦
            Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker)
              (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) x ⋯) 0)
          y hy →
        (fun (x : P.Ring) (hx : x ∈ P.ker * P.ker) ↦
            Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker)
              (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) x ⋯) 0)
          (x + y) ⋯
⊢ Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker) (1 ⊗ₜ[P.Ring] x) 0

Tactic:
refine Submodule.smul_induction_on' (p := fun x (hx : x ∈ P.ker * P.ker) ↦
      (1 : S) ⊗ₜ[P.Ring] (⟨x, Ideal.mul_le_right hx⟩ : P.ker) = 0) (hx := hx) ?_ ?_

Premises used: Submodule.smul_induction_on'
-- 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.388327
S' : Type ?u.388330
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.388454
S'' : Type ?u.388457
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'
inst_17 : Algebra R R''
inst_18 : IsScalarTower R R' R''
inst_19 : IsScalarTower R' R'' S''
inst_20 : Algebra R S''
inst_21 : IsScalarTower R R'' S''
inst_22 : IsScalarTower S S' S''
x : ↥P.ker
hx : (↑x : P.Ring) ∈ P.ker * P.ker
r : P.Ring
hr : r ∈ P.ker
s : P.Ring
hs : s ∈ P.ker
trans :
  Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker)
    (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (r • s) ⋯)
    (HSMul.hSMul (β := S) r 1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) s hs)
trans₁ :
  Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker)
    (HSMul.hSMul (β := S) r 1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) s hs) 0
⊢ Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker)
    (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (r • s) ⋯) 0

Tactic:
trans (r • 1) ⊗ₜ[P.Ring] ⟨s, hs⟩

Premises used: Algebra.Extension.Ring, HSMul.hSMul, OfNat.ofNat
-- 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.388327
S' : Type ?u.388330
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.388454
S'' : Type ?u.388457
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'
inst_17 : Algebra R R''
inst_18 : IsScalarTower R R' R''
inst_19 : IsScalarTower R' R'' S''
inst_20 : Algebra R S''
inst_21 : IsScalarTower R R'' S''
inst_22 : IsScalarTower S S' S''
x : ↥P.ker
hx : (↑x : P.Ring) ∈ P.ker * P.ker
r : P.Ring
hr : r ∈ P.ker
s : P.Ring
hs : s ∈ P.ker
rw :
  Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker)
    (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (r • s) ⋯)
    (1 ⊗ₜ[P.Ring] (r • Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) s hs))
⊢ Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker)
    (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (r • s) ⋯)
    (HSMul.hSMul (β := S) r 1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) s hs)

Tactic:
rw [smul_tmul]

Premises used: TensorProduct.smul_tmul
-- 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.388327
S' : Type ?u.388330
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.388454
S'' : Type ?u.388457
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'
inst_17 : Algebra R R''
inst_18 : IsScalarTower R R' R''
inst_19 : IsScalarTower R' R'' S''
inst_20 : Algebra R S''
inst_21 : IsScalarTower R R'' S''
inst_22 : IsScalarTower S S' S''
x : ↥P.ker
hx : (↑x : P.Ring) ∈ P.ker * P.ker
r : P.Ring
hr : r ∈ P.ker
s : P.Ring
hs : s ∈ P.ker
⊢ Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker)
    (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (r • s) ⋯)
    (1 ⊗ₜ[P.Ring] (r • Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) s hs))

Tactic:
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.388327
S' : Type ?u.388330
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.388454
S'' : Type ?u.388457
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'
inst_17 : Algebra R R''
inst_18 : IsScalarTower R R' R''
inst_19 : IsScalarTower R' R'' S''
inst_20 : Algebra R S''
inst_21 : IsScalarTower R R'' S''
inst_22 : IsScalarTower S S' S''
x : ↥P.ker
hx : (↑x : P.Ring) ∈ P.ker * P.ker
r : P.Ring
hr : r ∈ P.ker
s : P.Ring
hs : s ∈ P.ker
⊢ Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker)
    (HSMul.hSMul (β := S) r 1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) s hs) 0

Tactic:
simp_all [Algebra.smul_def]

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.388327
S' : Type ?u.388330
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.388454
S'' : Type ?u.388457
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'
inst_17 : Algebra R R''
inst_18 : IsScalarTower R R' R''
inst_19 : IsScalarTower R' R'' S''
inst_20 : Algebra R S''
inst_21 : IsScalarTower R R'' S''
inst_22 : IsScalarTower S S' S''
x : ↥P.ker
hx : (↑x : P.Ring) ∈ P.ker * P.ker
a : P.Ring
ha : a ∈ P.ker • P.ker
b : P.Ring
hb : b ∈ P.ker • P.ker
ha' :
  Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker) (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) a ⋯) 0
hb' :
  Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker) (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) b ⋯) 0
⊢ HAdd.hAdd (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker)
      (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) a ⋯)
      (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) b ⋯) =
    HAdd.hAdd (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker) 0 0

Tactic:
congr($ha' + $hb')

Premises used: congrArg, id, HAdd.hAdd, congr
-- 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.388327
S' : Type ?u.388330
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.388454
S'' : Type ?u.388457
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'
inst_17 : Algebra R R''
inst_18 : IsScalarTower R R' R''
inst_19 : IsScalarTower R' R'' S''
inst_20 : Algebra R S''
inst_21 : IsScalarTower R R'' S''
inst_22 : IsScalarTower S S' S''
x : ↥P.ker
hx : (↑x : P.Ring) ∈ P.ker * P.ker
a : P.Ring
ha : a ∈ P.ker • P.ker
b : P.Ring
hb : b ∈ P.ker • P.ker
ha' :
  Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker) (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) a ⋯) 0
hb' :
  Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker) (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) b ⋯) 0
h :
  1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (a + b) ⋯ =
    HAdd.hAdd (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker)
      (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) a ⋯)
      (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) b ⋯)
⊢ Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker)
    (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (a + b) ⋯) 0

Tactic:
convert! congr($ha' + $hb')
-- 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.388327
S' : Type ?u.388330
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.388454
S'' : Type ?u.388457
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'
inst_17 : Algebra R R''
inst_18 : IsScalarTower R R' R''
inst_19 : IsScalarTower R' R'' S''
inst_20 : Algebra R S''
inst_21 : IsScalarTower R R'' S''
inst_22 : IsScalarTower S S' S''
x : ↥P.ker
hx : (↑x : P.Ring) ∈ P.ker * P.ker
a : P.Ring
ha : a ∈ P.ker • P.ker
b : P.Ring
hb : b ∈ P.ker • P.ker
ha' :
  Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker) (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) a ⋯) 0
hb' :
  Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker) (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) b ⋯) 0
h :
  Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker)
    (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (a + b) ⋯)
    (1 ⊗ₜ[P.Ring]
      (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) a ⋯ + Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) b ⋯))
⊢ 1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (a + b) ⋯ =
    HAdd.hAdd (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker)
      (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) a ⋯)
      (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) b ⋯)

Tactic:
rw [← tmul_add]

Premises used: TensorProduct.tmul_add
-- 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.388327
S' : Type ?u.388330
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.388454
S'' : Type ?u.388457
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'
inst_17 : Algebra R R''
inst_18 : IsScalarTower R R' R''
inst_19 : IsScalarTower R' R'' S''
inst_20 : Algebra R S''
inst_21 : IsScalarTower R R'' S''
inst_22 : IsScalarTower S S' S''
x : ↥P.ker
hx : (↑x : P.Ring) ∈ P.ker * P.ker
a : P.Ring
ha : a ∈ P.ker • P.ker
b : P.Ring
hb : b ∈ P.ker • P.ker
ha' :
  Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker) (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) a ⋯) 0
hb' :
  Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker) (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) b ⋯) 0
⊢ Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker)
    (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (a + b) ⋯)
    (1 ⊗ₜ[P.Ring]
      (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) a ⋯ + Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) b ⋯))

Tactic:
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.388327
S' : Type ?u.388330
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.388454
S'' : Type ?u.388457
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'
inst_17 : Algebra R R''
inst_18 : IsScalarTower R R' R''
inst_19 : IsScalarTower R' R'' S''
inst_20 : Algebra R S''
inst_21 : IsScalarTower R R'' S''
inst_22 : IsScalarTower S S' S''
x : P.Cotangent
refine_2 :
  ∀ (x : ↥P.ker),
    ∃ (a : TensorProduct.{w, v, w} P.Ring S ↥P.ker),
      Eq.{w + 1} (α := P.Cotangent)
        ((LinearMap.liftBaseChange S Cotangent.mk : (a : S ⊗[P.Ring] ↥P.ker) → P.Cotangent) a : P.Cotangent)
        ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x : P.Cotangent)
⊢ ∃ (a : TensorProduct.{w, v, w} P.Ring S ↥P.ker),
    (LinearMap.liftBaseChange S Cotangent.mk : (a : S ⊗[P.Ring] ↥P.ker) → P.Cotangent) a = x

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.388327
S' : Type ?u.388330
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.388454
S'' : Type ?u.388457
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'
inst_17 : Algebra R R''
inst_18 : IsScalarTower R R' R''
inst_19 : IsScalarTower R' R'' S''
inst_20 : Algebra R S''
inst_21 : IsScalarTower R R'' S''
inst_22 : IsScalarTower S S' S''
x : ↥P.ker
⊢ Eq.{w + 1} (α := P.Cotangent)
    ((LinearMap.liftBaseChange S Cotangent.mk : (a : S ⊗[P.Ring] ↥P.ker) → P.Cotangent) (1 ⊗ₜ[P.Ring] x) : P.Cotangent)
    ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x : P.Cotangent)

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.388327
S' : Type ?u.388330
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.388454
S'' : Type ?u.388457
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'
inst_17 : Algebra R R''
inst_18 : IsScalarTower R R' R''
inst_19 : IsScalarTower R' R'' S''
inst_20 : Algebra R S''
inst_21 : IsScalarTower R R'' S''
inst_22 : IsScalarTower S S' S''
x : ↥P.ker
⊢ ∃ (a : TensorProduct.{w, v, w} P.Ring S ↥P.ker),
    Eq.{w + 1} (α := P.Cotangent)
      ((LinearMap.liftBaseChange S Cotangent.mk : (a : S ⊗[P.Ring] ↥P.ker) → P.Cotangent) a : P.Cotangent)
      ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x : P.Cotangent)

Tactic:
exact ⟨1 ⊗ₜ x, by 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
s : S
x : ↥P.ker
⊢ (P.cotangentEquiv : (a : S ⊗[P.Ring] ↥P.ker) → P.Cotangent) (s ⊗ₜ[P.Ring] x) =
    HSMul.hSMul (β := P.Cotangent) s ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x : P.Cotangent)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, Quot.map, Quotient.map', FreeAddMonoid.sumAux, rfl, Algebra.Extension.Cotangent.of
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{u, u_1, u_2} R S
T_1 : Type u_3
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
P : Extension.{u, u_1, u_2} R S
T : Type u_4
inst_5 : CommRing T
inst_6 : Algebra R T
this_1 : Algebra P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) := P.algebraBaseChange T
this_2 : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
this : Algebra P.Ring (T ⊗[R] S) := compHom (T ⊗[R] S) (algebraMap P.Ring S)
x : R
rw :
  Eq (α := T ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap P.Ring S : (a : P.Ring) → S) ((algebraMap R P.Ring : (a : R) → P.Ring) x : P.Ring) : T ⊗[R] S)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (T ⊗[R] S)) (algebraMap P.Ring S) :
          (a : P.Ring) → T ⊗[R] S)
        ((algebraMap R P.Ring : (a : R) → P.Ring) x) :
      T ⊗[R] S)
⊢ Eq (α := T ⊗[R] S) ((algebraMap R (T ⊗[R] S) : (a : R) → T ⊗[R] S) x : T ⊗[R] S)
    ((algebraMap P.Ring (T ⊗[R] S) : (a : P.Ring) → T ⊗[R] S) ((algebraMap R P.Ring : (a : R) → P.Ring) x) : T ⊗[R] S)

Tactic:
rw [TensorProduct.algebraMap_apply, RingHom.algebraMap_toAlgebra,
        Algebra.TensorProduct.tmul_one_eq_one_tmul, IsScalarTower.algebraMap_apply R P.Ring]

Premises used: Algebra.TensorProduct.algebraMap_apply, Algebra.Extension.Ring, Algebra.TensorProduct.tmul_one_eq_one_tmul, RingHom.algebraMap_toAlgebra, IsScalarTower.algebraMap_apply