awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
hy : y ∈ I
z : R
hz : z ∈ J
w : ↥J
hw : w ∈ Submodule.comap (Submodule.subtype J) (I * J)
eqz :
  Eq (α := J.Cotangent) ((J.toCotangent : (a : ↥J) → J.Cotangent) w : J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz)) :
      J.Cotangent)
mem_bot : HMul.hMul (β := R) y ((Submodule.subtype J : (a : ↥J) → R) w : R) = 0
eq0 : y • w = 0
this : Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y * z) ⋯ = y • Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz
mem_mul_mem :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (y • Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz)) :
      J.Cotangent)
    (0 : J.Cotangent)
mem_mul_mem₁ :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        (HSMul.hSMul (β := J.Cotangent) y
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz) : J.Cotangent)) :
      J.Cotangent)
    (0 : J.Cotangent)
mem_mul_mem₂ :
  HSMul.hSMul (β := J.Cotangent) y
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz)) :
        J.Cotangent) =
    0
mem_mul_mem₃ : HSMul.hSMul (β := J.Cotangent) y ((J.toCotangent : (a : ↥J) → J.Cotangent) w : J.Cotangent) = 0
⊢ Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y * z) ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
have mem_mul_mem₄ : Eq (α := J.Cotangent) ((J.toCotangent : (a : ↥J) → J.Cotangent) (y • w) : J.Cotangent) (0 : J.Cotangent)
Tactic: rw [this, map_smul, map_smul, ← eqz, ← map_smul, eq0, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
hy : y ∈ I
z : R
hz : z ∈ J
w : ↥J
hw : w ∈ Submodule.comap (Submodule.subtype J) (I * J)
eqz :
  Eq (α := J.Cotangent) ((J.toCotangent : (a : ↥J) → J.Cotangent) w : J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz)) :
      J.Cotangent)
mem_bot : HMul.hMul (β := R) y ((Submodule.subtype J : (a : ↥J) → R) w : R) = 0
eq0 : y • w = 0
this : Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y * z) ⋯ = y • Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz
mem_mul_mem :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (y • Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz)) :
      J.Cotangent)
    (0 : J.Cotangent)
mem_mul_mem₁ :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        (HSMul.hSMul (β := J.Cotangent) y
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz) : J.Cotangent)) :
      J.Cotangent)
    (0 : J.Cotangent)
mem_mul_mem₂ :
  HSMul.hSMul (β := J.Cotangent) y
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz)) :
        J.Cotangent) =
    0
mem_mul_mem₃ : HSMul.hSMul (β := J.Cotangent) y ((J.toCotangent : (a : ↥J) → J.Cotangent) w : J.Cotangent) = 0
mem_mul_mem₄ : Eq (α := J.Cotangent) ((J.toCotangent : (a : ↥J) → J.Cotangent) (y • w) : J.Cotangent) (0 : J.Cotangent)
⊢ Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y * z) ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
have mem_mul_mem₅ : Eq (α := J.Cotangent) ((J.toCotangent : (a : ↥J) → J.Cotangent) 0) 0
Tactic: rw [this, map_smul, map_smul, ← eqz, ← map_smul, eq0, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
hy : y ∈ I
z : R
hz : z ∈ J
w : ↥J
hw : w ∈ Submodule.comap (Submodule.subtype J) (I * J)
eqz :
  Eq (α := J.Cotangent) ((J.toCotangent : (a : ↥J) → J.Cotangent) w : J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz)) :
      J.Cotangent)
mem_bot : HMul.hMul (β := R) y ((Submodule.subtype J : (a : ↥J) → R) w : R) = 0
eq0 : y • w = 0
this : Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y * z) ⋯ = y • Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz
mem_mul_mem :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (y • Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz)) :
      J.Cotangent)
    (0 : J.Cotangent)
mem_mul_mem₁ :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        (HSMul.hSMul (β := J.Cotangent) y
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz) : J.Cotangent)) :
      J.Cotangent)
    (0 : J.Cotangent)
mem_mul_mem₂ :
  HSMul.hSMul (β := J.Cotangent) y
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz)) :
        J.Cotangent) =
    0
mem_mul_mem₃ : HSMul.hSMul (β := J.Cotangent) y ((J.toCotangent : (a : ↥J) → J.Cotangent) w : J.Cotangent) = 0
mem_mul_mem₄ : Eq (α := J.Cotangent) ((J.toCotangent : (a : ↥J) → J.Cotangent) (y • w) : J.Cotangent) (0 : J.Cotangent)
mem_mul_mem₅ : Eq (α := J.Cotangent) ((J.toCotangent : (a : ↥J) → J.Cotangent) 0) 0
⊢ Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y * z) ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
have mem_mul_mem₆ : Eq.{u_1 + 1} (α := J.Cotangent) 0 0
Tactic: rw [this, map_smul, map_smul, ← eqz, ← map_smul, eq0, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Quotient (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
ymem : y ∈ I * J
z : R
zmem : z ∈ I * J
hy :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
hz :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
⊢ Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y + z) ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
have this : Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y + z) sorry =
  Subtype.mk (p := fun (x : R) ↦ x ∈ J) y sorry + Subtype.mk (p := fun (x : R) ↦ x ∈ J) z sorry
Tactic: have : (⟨y + z, Ideal.mul_le_left (add_mem ymem zmem)⟩ : J) =
        ⟨y, Ideal.mul_le_left ymem⟩ + ⟨z, Ideal.mul_le_left zmem⟩ := rfl
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
ymem : y ∈ I * J
z : R
zmem : z ∈ I * J
hy :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
hz :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
this :
  Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y + z) ⋯ =
    Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯ + Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯
⊢ Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y + z) ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
have add : Eq (α := J.Cotangent)
  ((f : (a : J.Cotangent) → J.Cotangent)
      ((J.toCotangent : (a : ↥J) → J.Cotangent)
        (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y sorry + Subtype.mk (p := fun (x : R) ↦ x ∈ J) z sorry)) :
    J.Cotangent)
  (0 : J.Cotangent)
Tactic: rw [this, map_add, map_add, hy, hz, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
ymem : y ∈ I * J
z : R
zmem : z ∈ I * J
hy :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
hz :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
this :
  Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y + z) ⋯ =
    Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯ + Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯
add :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent)
          (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯ + Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
⊢ Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y + z) ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
have add₁ : Eq (α := J.Cotangent)
  ((f : (a : J.Cotangent) → J.Cotangent)
      (HAdd.hAdd (α := J.Cotangent) (β := J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y sorry) : J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z sorry) : J.Cotangent)) :
    J.Cotangent)
  (0 : J.Cotangent)
Tactic: rw [this, map_add, map_add, hy, hz, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
ymem : y ∈ I * J
z : R
zmem : z ∈ I * J
hy :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
hz :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
this :
  Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y + z) ⋯ =
    Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯ + Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯
add :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent)
          (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯ + Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
add₁ :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        (HAdd.hAdd (α := J.Cotangent) (β := J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯) : J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯) : J.Cotangent)) :
      J.Cotangent)
    (0 : J.Cotangent)
⊢ Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y + z) ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
have add₂ : HAdd.hAdd (α := J.Cotangent) (β := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y sorry)) :
      J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z sorry)) :
      J.Cotangent) =
  0
Tactic: rw [this, map_add, map_add, hy, hz, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
ymem : y ∈ I * J
z : R
zmem : z ∈ I * J
hy :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
hz :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
this :
  Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y + z) ⋯ =
    Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯ + Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯
add :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent)
          (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯ + Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
add₁ :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        (HAdd.hAdd (α := J.Cotangent) (β := J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯) : J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯) : J.Cotangent)) :
      J.Cotangent)
    (0 : J.Cotangent)
add₂ :
  HAdd.hAdd (α := J.Cotangent) (β := J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯)) :
        J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
        J.Cotangent) =
    0
⊢ Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y + z) ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
have add₃ : HAdd.hAdd (α := J.Cotangent) (β := J.Cotangent) (0 : J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z sorry)) :
      J.Cotangent) =
  0
Tactic: rw [this, map_add, map_add, hy, hz, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
ymem : y ∈ I * J
z : R
zmem : z ∈ I * J
hy :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
hz :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
this :
  Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y + z) ⋯ =
    Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯ + Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯
add :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent)
          (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯ + Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
add₁ :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        (HAdd.hAdd (α := J.Cotangent) (β := J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯) : J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯) : J.Cotangent)) :
      J.Cotangent)
    (0 : J.Cotangent)
add₂ :
  HAdd.hAdd (α := J.Cotangent) (β := J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯)) :
        J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
        J.Cotangent) =
    0
add₃ :
  HAdd.hAdd (α := J.Cotangent) (β := J.Cotangent) (0 : J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
        J.Cotangent) =
    0
⊢ Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y + z) ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
have add₄ : HAdd.hAdd (α := J.Cotangent) 0 0 = 0
Tactic: rw [this, map_add, map_add, hy, hz, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
ymem : y ∈ I * J
z : R
zmem : z ∈ I * J
hy :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
hz :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
this :
  Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y + z) ⋯ =
    Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯ + Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯
add :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent)
          (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯ + Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
add₁ :
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        (HAdd.hAdd (α := J.Cotangent) (β := J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯) : J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯) : J.Cotangent)) :
      J.Cotangent)
    (0 : J.Cotangent)
add₂ :
  HAdd.hAdd (α := J.Cotangent) (β := J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y ⋯)) :
        J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
        J.Cotangent) =
    0
add₃ :
  HAdd.hAdd (α := J.Cotangent) (β := J.Cotangent) (0 : J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z ⋯)) :
        J.Cotangent) =
    0
add₄ : HAdd.hAdd (α := J.Cotangent) 0 0 = 0
⊢ Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y + z) ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
have add₅ : Eq.{u_1 + 1} (α := J.Cotangent) 0 0
Tactic: rw [this, map_add, map_add, hy, hz, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x : R
h : x ∈ I * J
⊢ Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) x ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
have mem_mul_mem : ∀ (y : R) (hy : y ∈ I) (z : R) (hz : z ∈ J),
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y * z) sorry)) :
      J.Cotangent)
    (0 : J.Cotangent)
Tactic: induction h using Submodule.mul_induction_on' with
    | mem_mul_mem y hy z hz =>
      rcases Submodule.mem_map.mp (le (f.mem_range_self (J.toCotangent ⟨z, hz⟩))) with ⟨w, hw, eqz⟩
      have mem_bot := Ideal.mul_mem_mul hy (Submodule.mem_comap.mp hw)
      simp only [← mul_assoc, sq, Submodule.bot_mul, Submodule.mem_bot] at mem_bot
      have eq0 : y • w = 0 := SetCoe.ext mem_bot
      have : ⟨y * z, Ideal.mul_le_left (Submodule.mul_mem_mul hy hz)⟩ = y • (⟨z, hz⟩ : J) := rfl
      rw [this, map_smul, map_smul, ← eqz, ← map_smul, eq0, map_zero]
    | add y ymem z zmem hy hz =>
      have : (⟨y + z, Ideal.mul_le_left (add_mem ymem zmem)⟩ : J) =
        ⟨y, Ideal.mul_le_left ymem⟩ + ⟨z, Ideal.mul_le_left zmem⟩ := rfl
      rw [this, map_add, map_add, hy, hz, add_zero]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x : R
h : x ∈ I * J
mem_mul_mem :
  ∀ (y : R) (hy : y ∈ I) (z : R) (hz : z ∈ J),
    Eq (α := J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y * z) ⋯)) :
        J.Cotangent)
      (0 : J.Cotangent)
⊢ Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) x ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
have add : ∀ (y : R) (ymem : y ∈ I * J) (z : R) (zmem : z ∈ I * J)
  (hy :
    Eq (α := J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) y sorry)) :
        J.Cotangent)
      (0 : J.Cotangent))
  (hz :
    Eq (α := J.Cotangent)
      ((f : (a : J.Cotangent) → J.Cotangent)
          ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) z sorry)) :
        J.Cotangent)
      (0 : J.Cotangent)),
  Eq (α := J.Cotangent)
    ((f : (a : J.Cotangent) → J.Cotangent)
        ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ J) (y + z) sorry)) :
      J.Cotangent)
    (0 : J.Cotangent)
Tactic: induction h using Submodule.mul_induction_on' with
    | mem_mul_mem y hy z hz =>
      rcases Submodule.mem_map.mp (le (f.mem_range_self (J.toCotangent ⟨z, hz⟩))) with ⟨w, hw, eqz⟩
      have mem_bot := Ideal.mul_mem_mul hy (Submodule.mem_comap.mp hw)
      simp only [← mul_assoc, sq, Submodule.bot_mul, Submodule.mem_bot] at mem_bot
      have eq0 : y • w = 0 := SetCoe.ext mem_bot
      have : ⟨y * z, Ideal.mul_le_left (Submodule.mul_mem_mul hy hz)⟩ = y • (⟨z, hz⟩ : J) := rfl
      rw [this, map_smul, map_smul, ← eqz, ← map_smul, eq0, map_zero]
    | add y ymem z zmem hy hz =>
      have : (⟨y + z, Ideal.mul_le_left (add_mem ymem zmem)⟩ : J) =
        ⟨y, Ideal.mul_le_left ymem⟩ + ⟨z, Ideal.mul_le_left zmem⟩ := rfl
      rw [this, map_add, map_add, hy, hz, add_zero]
Cleared hypotheses: h