awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Pi (goal)
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
⊢ A i →ₐ[R]
    ((i : I) → A i) ⧸
      HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
        (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2
have g : Eq (α :=
  ((i : I) → A i) ⧸
    HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
      (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
  ((AlgHom.toLinearMap
          (Ideal.Quotient.mkₐ R
            (HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
              (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)) ∘ₗ
        LinearMap.single R A i :
      (a : A i) → ((i : I) → A i) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)
    1)
  1
Tactic: apply AlgHom.ofLinearMap
      ((Ideal.Quotient.mkₐ R _).toLinearMap.comp (LinearMap.single _ _ i))
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Pi (goal)
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
g :
  Eq (α :=
    ((i : I) → A i) ⧸
      HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
        (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
    ((AlgHom.toLinearMap
            (Ideal.Quotient.mkₐ R
              (HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
                (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)) ∘ₗ
          LinearMap.single R A i :
        (a : A i) → ((i : I) → A i) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)
      1)
    1
⊢ A i →ₐ[R]
    ((i : I) → A i) ⧸
      HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
        (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2
have g₁ : ∀ (x y : A i),
  (AlgHom.toLinearMap
            (Ideal.Quotient.mkₐ R
              (HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
                (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)) ∘ₗ
          LinearMap.single R A i :
        (a : A i) → ((i : I) → A i) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)
      (x * y) =
    HMul.hMul (α :=
      ((i : I) → A i) ⧸
        HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
          (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
      (β :=
      ((i : I) → A i) ⧸
        HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
          (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
      ((AlgHom.toLinearMap
                (Ideal.Quotient.mkₐ R
                  (HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
                    (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)) ∘ₗ
              LinearMap.single R A i :
            (a : A i) → ((i : I) → A i) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)
          x :
        ((i : I) → A i) ⧸
          HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
            (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
      ((AlgHom.toLinearMap
                (Ideal.Quotient.mkₐ R
                  (HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
                    (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)) ∘ₗ
              LinearMap.single R A i :
            (a : A i) → ((i : I) → A i) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)
          y :
        ((i : I) → A i) ⧸
          HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
            (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
Tactic: apply AlgHom.ofLinearMap
      ((Ideal.Quotient.mkₐ R _).toLinearMap.comp (LinearMap.single _ _ i))
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Pi (goal)
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
⊢ Eq (α :=
    ((i : I) → A i) ⧸
      HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
        (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
    ((AlgHom.toLinearMap
            (Ideal.Quotient.mkₐ R
              (HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
                (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)) ∘ₗ
          LinearMap.single R A i :
        (a : A i) → ((i : I) → A i) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)
      1)
    1
have g : Eq (α :=
  ((j : I) → A j) ⧸
    HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
      (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
  ((Ideal.Quotient.mk
          (HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
            (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2) :
        (a : (j : I) → A j) → ((j : I) → A j) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)
      (Pi.single (M := A) i 1) :
    ((j : I) → A j) ⧸
      HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
        (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
  (1 :
    ((j : I) → A j) ⧸
      HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
        (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
Tactic: change Ideal.Quotient.mk _ (Pi.single i 1) = 1
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Pi (goal)
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
⊢ Eq (α :=
    ((j : I) → A j) ⧸
      HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
        (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
    ((Ideal.Quotient.mk
            (HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
              (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2) :
          (a : (j : I) → A j) → ((j : I) → A j) ⧸ RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)
        (Pi.single (M := A) i 1) :
      ((j : I) → A j) ⧸
        HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
          (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
    (1 :
      ((j : I) → A j) ⧸
        HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
          (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2)
have g : HSub.hSub (α := (j : I) → A j) (Pi.single (M := A) i 1) 1 ∈
  HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
    (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2
Tactic: rw [← (Ideal.Quotient.mk _).map_one, ← sub_eq_zero, ← map_sub,
        Ideal.Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Pi (hypothesis)
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
⊢ HSub.hSub (α := (j : I) → A j) (Pi.single (M := A) i 1) 1 ∈
    HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
      (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2
have this : Membership.mem (γ := Ideal ((i : I) → A i))
  (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i)))
  (HSub.hSub (α := (j : I) → A j) (Pi.single (M := A) i 1) 1)
Tactic: have : Pi.single i 1 - 1 ∈ RingHom.ker (Pi.evalAlgHom R A i).toRingHom := by
        simp [RingHom.mem_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Pi (goal)
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
this :
  Membership.mem (γ := Ideal ((i : I) → A i))
    (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i)))
    (HSub.hSub (α := (j : I) → A j) (Pi.single (M := A) i 1) 1)
⊢ HSub.hSub (α := (j : I) → A j) (Pi.single (M := A) i 1) 1 ∈
    HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
      (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2
have h : HSub.hSub (α := (j : I) → A j) (Pi.single (M := A) i 1) 1 =
  -HPow.hPow (β := ℕ) (HSub.hSub (α := (j : I) → A j) (Pi.single (M := A) i 1) 1) 2
Tactic: convert! neg_mem (Ideal.pow_mem_pow this 2) using 1
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Pi (goal)
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Pi (goal)
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
x : A i
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : Pi.single (M := A) i x i = x
Tactic: change (Pi.single i x) i = x
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
R' : Type u_3
S' : Type u_4
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R' S'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
surjRS : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
eqmap :
  Eq (α := Ideal S) (RingHom.ker (F := S →+* S') (algebraMap S S'))
    (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker (F := R →+* R') (algebraMap R R')))
⊢ Eq (α := Ideal R) (Ideal.comap (F := R →+* R') (algebraMap R R') (RingHom.ker (F := R' →+* S') (algebraMap R' S')))
    (RingHom.ker (F := R →+* R') (algebraMap R R') ⊔ RingHom.ker (F := R →+* S) (algebraMap R S))
have rw : Eq (α := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) (RingHom.ker (F := S →+* S') (algebraMap S S')))
  (RingHom.ker (F := R →+* R') (algebraMap R R') ⊔ RingHom.ker (F := R →+* S) (algebraMap R S))
Tactic: rw [RingHom.comap_ker, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq _ S,
      ← RingHom.comap_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
J I : Ideal R
sq : HPow.hPow (β := ℕ) I 2 = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
⊢ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J)) ≤ f.ker
have rw : ∀ (sq : I * I = ⊥) (f : J.Cotangent →ₗ[R] J.Cotangent)
  (le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))),
  Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J)) ≤ f.ker
Tactic: rw [pow_two] at sq
Cleared hypotheses: sq, f, le
-- 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
⊢ 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 : ∀ (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)),
  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: rcases Submodule.mem_map.mp (le (f.mem_range_self (J.toCotangent ⟨z, hz⟩))) with ⟨w, hw, eqz⟩
-- 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
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)
⊢ 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_bot : HMul.hMul (β := R) y ((Submodule.subtype J : (a : ↥J) → R) w : R) ∈ I * (I * J)
Tactic: have mem_bot := Ideal.mul_mem_mul hy (Submodule.mem_comap.mp hw)
-- 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
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) ∈ I * (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) (y * z) ⋯)) :
      J.Cotangent)
    (0 : J.Cotangent)
have mem_bot₁ : HMul.hMul (β := R) y ((Submodule.subtype J : (a : ↥J) → R) w : R) = 0
Tactic: simp only [← mul_assoc, sq, Submodule.bot_mul, Submodule.mem_bot] at mem_bot
Cleared hypotheses: mem_bot
-- 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
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
⊢ 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 eq0 : y • w = 0
Tactic: have eq0 : y • w = 0 := SetCoe.ext mem_bot
-- 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
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
⊢ 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 = y • Subtype.mk (p := fun (x : R) ↦ x ∈ J) z hz
Tactic: have : ⟨y * z, Ideal.mul_le_left (Submodule.mul_mem_mul hy hz)⟩ = y • (⟨z, hz⟩ : J) := 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
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
⊢ 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)
  ((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)
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)
⊢ 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)
  ((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)
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)
⊢ 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₂ : 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
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
⊢ 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₃ : HSMul.hSMul (β := J.Cotangent) y ((J.toCotangent : (a : ↥J) → J.Cotangent) w : J.Cotangent) = 0
Tactic: rw [this, map_smul, map_smul, ← eqz, ← map_smul, eq0, map_zero]