awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
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''
⊢ TensorProduct.{w, v, w} P.Ring S ↥P.ker ≃ₗ[S] P.Cotangent
have refine_1 : Function.Injective (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker) (β := P.Cotangent)
  (⇑(LinearMap.liftBaseChange S Cotangent.mk) : (a : S ⊗[P.Ring] ↥P.ker) → P.Cotangent)
Tactic: refine .ofBijective (Cotangent.mk.liftBaseChange _) ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
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''
refine_1 :
  Function.Injective (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker) (β := P.Cotangent)
    (⇑(LinearMap.liftBaseChange S Cotangent.mk) : (a : S ⊗[P.Ring] ↥P.ker) → P.Cotangent)
⊢ TensorProduct.{w, v, w} P.Ring S ↥P.ker ≃ₗ[S] P.Cotangent
have refine_2 : Function.Surjective (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker) (β := P.Cotangent)
  (⇑(LinearMap.liftBaseChange S Cotangent.mk) : (a : S ⊗[P.Ring] ↥P.ker) → P.Cotangent)
Tactic: refine .ofBijective (Cotangent.mk.liftBaseChange _) ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
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''
⊢ Function.Injective (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker) (β := P.Cotangent)
    (⇑(LinearMap.liftBaseChange S Cotangent.mk) : (a : S ⊗[P.Ring] ↥P.ker) → P.Cotangent)
have refine_1 : ∀ (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)),
  x = 0
Tactic: refine (injective_iff_map_eq_zero _).mpr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
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)
⊢ x = 0
have 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)
Tactic: obtain ⟨x, rfl⟩ := TensorProduct.mk_surjective P.Ring P.ker S P.algebraMap_surjective x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (hypothesis)
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)
⊢ 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)
have hx₁ : (↑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 ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
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
have 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 sorry) 0)
    (r • n) sorry
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) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
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) ⋯
⊢ Eq (α := TensorProduct.{w, v, w} P.Ring S ↥P.ker) (1 ⊗ₜ[P.Ring] x) 0
have 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 sorry) 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 sorry) 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 sorry) 0)
        (x + y) sorry
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) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
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) ⋯) 0
have 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) sorry)
  (HSMul.hSMul (β := S) r 1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) s hs)
Tactic: trans (r • 1) ⊗ₜ[P.Ring] ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
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)
⊢ 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
have 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
Tactic: trans (r • 1) ⊗ₜ[P.Ring] ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
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) ⋯)
    (HSMul.hSMul (β := S) r 1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) s hs)
have 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) sorry)
  (1 ⊗ₜ[P.Ring] (r • Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) s hs))
Tactic: rw [smul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
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) ⋯) 0
have h : 1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) (a + b) sorry =
  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 sorry)
    (1 ⊗ₜ[P.Ring] Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) b sorry)
Tactic: convert! congr($ha' + $hb')
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
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
⊢ 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 ⋯)
have 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) sorry)
  (1 ⊗ₜ[P.Ring]
    (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) a sorry + Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ P.ker) b sorry))
Tactic: rw [← tmul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
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
⊢ ∃ (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
have 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)
Tactic: obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
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
⊢ 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)
have 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)
Tactic: rw [TensorProduct.algebraMap_apply, RingHom.algebraMap_toAlgebra,
        Algebra.TensorProduct.tmul_one_eq_one_tmul, IsScalarTower.algebraMap_apply R P.Ring]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
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_3 : Algebra P.Ring (T ⊗[R] S) := compHom (T ⊗[R] S) (algebraMap P.Ring S)
this : IsScalarTower R P.Ring (T ⊗[R] S)
PT : Extension T (T ⊗[R] S) := P.baseChange
⊢ IsPushout R T P.Ring PT.Ring
have h : PT.Ring = TensorProduct.{u_1, u_4, u} R T P.Ring →
  HEq (α := CommSemiring PT.Ring) CommRing.toCommSemiring (β := CommSemiring (TensorProduct.{u_1, u_4, u} R T P.Ring))
      TensorProduct.instCommSemiring →
    PT.instRingOfIsScalarTower = TensorProduct.instAlgebra
Tactic: convert! TensorProduct.isPushout (R := R) (T := P.Ring) (S := T)