awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : A →ₐ[R] B
e : Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f) (IsScalarTower.toAlgHom R A (B ⧸ I))
x y : A
F : LinearMap.{u, u, v, w} (RingHom.id R) A ↥I := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯
this :
  HSub.hSub (α := B) (β := B) ((f : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) x : B) *
      HSub.hSub (α := B) (β := B) ((f : (a : A) → B) y : B) ((algebraMap A B : (a : A) → B) y : B) =
    0
⊢ (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯ : (a : A) → ↥I) (x * y) =
    HSMul.hSMul (β := ↥I) x ((diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯ : (a : A) → ↥I) y : ↥I) +
      HSMul.hSMul (β := ↥I) y ((diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯ : (a : A) → ↥I) x : ↥I)
have refine_3 : (↑((diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) sorry : (a : A) → ↥I) (x * y)) : B) =
  (↑(HSMul.hSMul (β := ↥I) x
          ((diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) sorry : (a : A) → ↥I) y : ↥I) +
        HSMul.hSMul (β := ↥I) y
          ((diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) sorry : (a : A) → ↥I) x : ↥I)) :
    B)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : A →ₐ[R] B
e : Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f) (IsScalarTower.toAlgHom R A (B ⧸ I))
x y : A
F : LinearMap.{u, u, v, w} (RingHom.id R) A ↥I := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯
this :
  HSub.hSub (α := B) (β := B) ((f : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) x : B) *
      HSub.hSub (α := B) (β := B) ((f : (a : A) → B) y : B) ((algebraMap A B : (a : A) → B) y : B) =
    0
⊢ (↑((diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯ : (a : A) → ↥I) (x * y)) : B) =
    (↑(HSMul.hSMul (β := ↥I) x
            ((diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯ : (a : A) → ↥I) y : ↥I) +
          HSMul.hSMul (β := ↥I) y
            ((diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯ : (a : A) → ↥I) x : ↥I)) :
      B)
have refine_3 : HSub.hSub (α := B) (β := B) ((f : (a : A) → B) (x * y) : B) ((algebraMap A B : (a : A) → B) (x * y) : B) =
  x • HSub.hSub (α := B) (β := B) ((f : (a : A) → B) y : B) ((algebraMap A B : (a : A) → B) y : B) +
    y • HSub.hSub (α := B) (β := B) ((f : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) x : B)
Tactic: dsimp only [Submodule.coe_add, Submodule.coe_mk, LinearMap.coe_mk,
      diffToIdealOfQuotientCompEq_apply, Submodule.coe_smul_of_tower, IsScalarTower.coe_toAlgHom',
      LinearMap.toFun_eq_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : A →ₐ[R] B
e : Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f) (IsScalarTower.toAlgHom R A (B ⧸ I))
x y : A
F : LinearMap.{u, u, v, w} (RingHom.id R) A ↥I := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯
this :
  HSub.hSub (α := B) (β := B) ((f : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) x : B) *
      HSub.hSub (α := B) (β := B) ((f : (a : A) → B) y : B) ((algebraMap A B : (a : A) → B) y : B) =
    0
⊢ HSub.hSub (α := B) (β := B) ((f : (a : A) → B) (x * y) : B) ((algebraMap A B : (a : A) → B) (x * y) : B) =
    x • HSub.hSub (α := B) (β := B) ((f : (a : A) → B) y : B) ((algebraMap A B : (a : A) → B) y : B) +
      y • HSub.hSub (α := B) (β := B) ((f : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) x : B)
have refine_3 : ∀
  (this :
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) -
          HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((f : (a : A) → B) y : B) -
        (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B) -
          HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B)) =
      0),
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) -
      HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B) =
    HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((f : (a : A) → B) y : B) -
        HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B) +
      (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) y : B) ((f : (a : A) → B) x : B) -
        HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) y : B) ((algebraMap A B : (a : A) → B) x : B))
Tactic: simp only [map_mul, sub_mul, mul_sub, Algebra.smul_def] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (hypothesis)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : A →ₐ[R] B
e : Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f) (IsScalarTower.toAlgHom R A (B ⧸ I))
x y : A
F : LinearMap.{u, u, v, w} (RingHom.id R) A ↥I := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯
this :
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) -
        HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((f : (a : A) → B) y : B) -
      (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B) -
        HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B)) =
    0
⊢ HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) -
      HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B) =
    HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((f : (a : A) → B) y : B) -
        HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B) +
      (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) y : B) ((f : (a : A) → B) x : B) -
        HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) y : B) ((algebraMap A B : (a : A) → B) x : B))
have this₁ : HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) =
  0 +
      (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B) -
        HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B)) +
    HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
Tactic: rw [sub_eq_iff_eq_add, sub_eq_iff_eq_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : A →ₐ[R] B
e : Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f) (IsScalarTower.toAlgHom R A (B ⧸ I))
x y : A
F : LinearMap.{u, u, v, w} (RingHom.id R) A ↥I := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯
this :
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) =
    0 +
        (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B) -
          HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B)) +
      HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
⊢ HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) -
      HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B) =
    HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((f : (a : A) → B) y : B) -
        HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B) +
      (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) y : B) ((f : (a : A) → B) x : B) -
        HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) y : B) ((algebraMap A B : (a : A) → B) x : B))
have refine_3 : 0 +
        (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B) -
          HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B)) +
      HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((f : (a : A) → B) y : B) -
    HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B) =
  HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((f : (a : A) → B) y : B) -
      HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B) +
    (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) y : B) ((f : (a : A) → B) x : B) -
      HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) y : B) ((algebraMap A B : (a : A) → B) x : B))
Tactic: simp only [this]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
hI_1 : HPow.hPow (β := ℕ) I 2 = ⊥
inst_6 : IsScalarTower R A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : Derivation.{u, v, w} R A ↥I
⊢ HAdd.hAdd (α := B) (β := B) ((↑((f : (a : A) → ↥I) 1) : B) : B) ((algebraMap A B : (a : A) → B) 1 : B) = 1
have rw : HAdd.hAdd (α := B) (↑((f : (a : A) → ↥I) 1) : B) 1 = 1
Tactic: rw [map_one (algebraMap _ _), f.map_one_eq_zero, Submodule.coe_zero, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
hI_1 : HPow.hPow (β := ℕ) I 2 = ⊥
inst_6 : IsScalarTower R A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : Derivation.{u, v, w} R A ↥I
rw : HAdd.hAdd (α := B) (↑((f : (a : A) → ↥I) 1) : B) 1 = 1
⊢ HAdd.hAdd (α := B) (β := B) ((↑((f : (a : A) → ↥I) 1) : B) : B) ((algebraMap A B : (a : A) → B) 1 : B) = 1
have rw₁ : HAdd.hAdd (α := B) (↑0 : B) 1 = 1
Tactic: rw [map_one (algebraMap _ _), f.map_one_eq_zero, Submodule.coe_zero, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
hI_1 : HPow.hPow (β := ℕ) I 2 = ⊥
inst_6 : IsScalarTower R A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : Derivation.{u, v, w} R A ↥I
rw : HAdd.hAdd (α := B) (↑((f : (a : A) → ↥I) 1) : B) 1 = 1
rw₁ : HAdd.hAdd (α := B) (↑0 : B) 1 = 1
⊢ HAdd.hAdd (α := B) (β := B) ((↑((f : (a : A) → ↥I) 1) : B) : B) ((algebraMap A B : (a : A) → B) 1 : B) = 1
have rw₂ : HAdd.hAdd (α := B) 0 1 = 1
Tactic: rw [map_one (algebraMap _ _), f.map_one_eq_zero, Submodule.coe_zero, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
hI_1 : HPow.hPow (β := ℕ) I 2 = ⊥
inst_6 : IsScalarTower R A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : Derivation.{u, v, w} R A ↥I
rw : HAdd.hAdd (α := B) (↑((f : (a : A) → ↥I) 1) : B) 1 = 1
rw₁ : HAdd.hAdd (α := B) (↑0 : B) 1 = 1
rw₂ : HAdd.hAdd (α := B) 0 1 = 1
⊢ HAdd.hAdd (α := B) (β := B) ((↑((f : (a : A) → ↥I) 1) : B) : B) ((algebraMap A B : (a : A) → B) 1 : B) = 1
have rw₃ : Eq.{w + 1} (α := B) 1 1
Tactic: rw [map_one (algebraMap _ _), f.map_one_eq_zero, Submodule.coe_zero, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
hI_1 : HPow.hPow (β := ℕ) I 2 = ⊥
inst_6 : IsScalarTower R A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : Derivation.{u, v, w} R A ↥I
x y : A
⊢ HMul.hMul (α := B) (↑((f : (a : A) → ↥I) x) : B) (↑((f : (a : A) → ↥I) y) : B) = 0
have rw : HMul.hMul (α := B) (↑((f : (a : A) → ↥I) x) : B) (↑((f : (a : A) → ↥I) y) : B) ∈ I * I
Tactic: rw [← Ideal.mem_bot, ← hI, pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (hypothesis)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
hI_1 : HPow.hPow (β := ℕ) I 2 = ⊥
inst_6 : IsScalarTower R A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : Derivation.{u, v, w} R A ↥I
x y : A
⊢ HAdd.hAdd (α := B) (β := B) ((↑((f : (a : A) → ↥I) (x * y)) : B) : B) ((algebraMap A B : (a : A) → B) (x * y) : B) =
    HAdd.hAdd (α := B) (β := B) ((↑((f : (a : A) → ↥I) x) : B) : B) ((algebraMap A B : (a : A) → B) x : B) *
      HAdd.hAdd (α := B) (β := B) ((↑((f : (a : A) → ↥I) y) : B) : B) ((algebraMap A B : (a : A) → B) y : B)
have this : HMul.hMul (α := B) (↑((f : (a : A) → ↥I) x) : B) (↑((f : (a : A) → ↥I) y) : B) = 0
Tactic: have : (f x : B) * f y = 0 := by
        rw [← Ideal.mem_bot, ← hI, pow_two]
        convert! Ideal.mul_mem_mul (f x).2 (f y).2 using 1
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
hI_1 : HPow.hPow (β := ℕ) I 2 = ⊥
inst_6 : IsScalarTower R A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : Derivation.{u, v, w} R A ↥I
x y : A
this : HMul.hMul (α := B) (↑((f : (a : A) → ↥I) x) : B) (↑((f : (a : A) → ↥I) y) : B) = 0
⊢ HAdd.hAdd (α := B) (β := B) ((↑((f : (a : A) → ↥I) (x * y)) : B) : B) ((algebraMap A B : (a : A) → B) (x * y) : B) =
    HAdd.hAdd (α := B) (β := B) ((↑((f : (a : A) → ↥I) x) : B) : B) ((algebraMap A B : (a : A) → B) x : B) *
      HAdd.hAdd (α := B) (β := B) ((↑((f : (a : A) → ↥I) y) : B) : B) ((algebraMap A B : (a : A) → B) y : B)
have simp : HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((↑((f : (a : A) → ↥I) y) : B) : B) +
      HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) y : B) ((↑((f : (a : A) → ↥I) x) : B) : B) +
    HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B) =
  0 + HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((↑((f : (a : A) → ↥I) y) : B) : B) +
    (HMul.hMul (α := B) (β := B) ((↑((f : (a : A) → ↥I) x) : B) : B) ((algebraMap A B : (a : A) → B) y : B) +
      HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) y : B))
Tactic: simp only [map_mul, f.leibniz, add_mul, mul_add, Submodule.coe_add,
        Submodule.coe_smul_of_tower, Algebra.smul_def, this]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
inst_6 : IsScalarTower R A B
d : Derivation.{u, v, w} R A ↥I
x : A
⊢ Eq (α := B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((liftOfDerivationToSquareZero I hI d : (a : A) → B) x) : B ⧸ I)
    ((algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x : B ⧸ I)
have rw : Eq (α := B ⧸ I)
  ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
      (HAdd.hAdd (α := B) (β := B) ((↑((d : (a : A) → ↥I) x) : B) : B) ((algebraMap A B : (a : A) → B) x : B)) :
    B ⧸ I)
  ((algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x : B ⧸ I)
Tactic: rw [liftOfDerivationToSquareZero_apply, map_add, Ideal.Quotient.eq_zero_iff_mem.mpr (d x).prop,
    zero_add, Ideal.Quotient.mk_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
inst_6 : IsScalarTower R A B
d : Derivation.{u, v, w} R A ↥I
x : A
rw :
  Eq (α := B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
        (HAdd.hAdd (α := B) (β := B) ((↑((d : (a : A) → ↥I) x) : B) : B) ((algebraMap A B : (a : A) → B) x : B)) :
      B ⧸ I)
    ((algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x : B ⧸ I)
⊢ Eq (α := B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((liftOfDerivationToSquareZero I hI d : (a : A) → B) x) : B ⧸ I)
    ((algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x : B ⧸ I)
have rw₁ : HAdd.hAdd (α := B ⧸ I) (β := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) (↑((d : (a : A) → ↥I) x) : B) : B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((algebraMap A B : (a : A) → B) x) : B ⧸ I) =
  (algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x
Tactic: rw [liftOfDerivationToSquareZero_apply, map_add, Ideal.Quotient.eq_zero_iff_mem.mpr (d x).prop,
    zero_add, Ideal.Quotient.mk_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
inst_6 : IsScalarTower R A B
d : Derivation.{u, v, w} R A ↥I
x : A
rw :
  Eq (α := B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
        (HAdd.hAdd (α := B) (β := B) ((↑((d : (a : A) → ↥I) x) : B) : B) ((algebraMap A B : (a : A) → B) x : B)) :
      B ⧸ I)
    ((algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x : B ⧸ I)
rw₁ :
  HAdd.hAdd (α := B ⧸ I) (β := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) (↑((d : (a : A) → ↥I) x) : B) : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((algebraMap A B : (a : A) → B) x) : B ⧸ I) =
    (algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x
⊢ Eq (α := B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((liftOfDerivationToSquareZero I hI d : (a : A) → B) x) : B ⧸ I)
    ((algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x : B ⧸ I)
have rw₂ : HAdd.hAdd (α := B ⧸ I) (β := B ⧸ I) (0 : B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((algebraMap A B : (a : A) → B) x) : B ⧸ I) =
  (algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x
Tactic: rw [liftOfDerivationToSquareZero_apply, map_add, Ideal.Quotient.eq_zero_iff_mem.mpr (d x).prop,
    zero_add, Ideal.Quotient.mk_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
inst_6 : IsScalarTower R A B
d : Derivation.{u, v, w} R A ↥I
x : A
rw :
  Eq (α := B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
        (HAdd.hAdd (α := B) (β := B) ((↑((d : (a : A) → ↥I) x) : B) : B) ((algebraMap A B : (a : A) → B) x : B)) :
      B ⧸ I)
    ((algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x : B ⧸ I)
rw₁ :
  HAdd.hAdd (α := B ⧸ I) (β := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) (↑((d : (a : A) → ↥I) x) : B) : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((algebraMap A B : (a : A) → B) x) : B ⧸ I) =
    (algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x
rw₂ :
  HAdd.hAdd (α := B ⧸ I) (β := B ⧸ I) (0 : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((algebraMap A B : (a : A) → B) x) : B ⧸ I) =
    (algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x
⊢ Eq (α := B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((liftOfDerivationToSquareZero I hI d : (a : A) → B) x) : B ⧸ I)
    ((algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x : B ⧸ I)
have rw₃ : Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((algebraMap A B : (a : A) → B) x) : B ⧸ I)
  ((algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x : B ⧸ I)
Tactic: rw [liftOfDerivationToSquareZero_apply, map_add, Ideal.Quotient.eq_zero_iff_mem.mpr (d x).prop,
    zero_add, Ideal.Quotient.mk_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
inst_6 : IsScalarTower R A B
d : Derivation.{u, v, w} R A ↥I
x : A
rw :
  Eq (α := B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
        (HAdd.hAdd (α := B) (β := B) ((↑((d : (a : A) → ↥I) x) : B) : B) ((algebraMap A B : (a : A) → B) x : B)) :
      B ⧸ I)
    ((algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x : B ⧸ I)
rw₁ :
  HAdd.hAdd (α := B ⧸ I) (β := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) (↑((d : (a : A) → ↥I) x) : B) : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((algebraMap A B : (a : A) → B) x) : B ⧸ I) =
    (algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x
rw₂ :
  HAdd.hAdd (α := B ⧸ I) (β := B ⧸ I) (0 : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((algebraMap A B : (a : A) → B) x) : B ⧸ I) =
    (algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x
rw₃ :
  Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((algebraMap A B : (a : A) → B) x) : B ⧸ I)
    ((algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x : B ⧸ I)
⊢ Eq (α := B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((liftOfDerivationToSquareZero I hI d : (a : A) → B) x) : B ⧸ I)
    ((algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x : B ⧸ I)
have rw₄ : Eq.{w + 1} (α := B ⧸ I) ((algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x : B ⧸ I)
  ((algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x : B ⧸ I)
Tactic: rw [liftOfDerivationToSquareZero_apply, map_add, Ideal.Quotient.eq_zero_iff_mem.mpr (d x).prop,
    zero_add, Ideal.Quotient.mk_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.ToSquareZero (goal)
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
I : Ideal B
inst_5 : Algebra A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
inst_6 : IsScalarTower R A B
⊢ Derivation.{u, v, w} R A ↥I ≃
    { f : A →ₐ[R] B //
      Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
        (IsScalarTower.toAlgHom R A (B ⧸ I)) }
have refine_1 : ∀ (d : Derivation.{u, v, w} R A ↥I),
  Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) (liftOfDerivationToSquareZero I hI d))
    (IsScalarTower.toAlgHom R A (B ⧸ I))
Tactic: refine ⟨fun d => ⟨liftOfDerivationToSquareZero I hI d, ?_⟩, fun f =>
    (derivationToSquareZeroOfLift I hI f.1 f.2 :), ?_, ?_⟩