awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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))
refine_1 :
  Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
refine_2 : Eq.{w + 1} (α := ↥I) ((diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯ : (a : A) → ↥I) 1) 0
refine_3 :
  ∀ (a b : A),
    (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯ : (a : A) → ↥I) (a * b) =
      HSMul.hSMul (β := ↥I) a
          ((diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯ : (a : A) → ↥I) b : ↥I) +
        HSMul.hSMul (β := ↥I) b
          ((diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯ : (a : A) → ↥I) a : ↥I)
⊢ Derivation.{u, v, w} R A ↥I

Tactic:
refine
    { diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ?_ with
      map_one_eq_zero' := ?_
      leibniz' := ?_ }

Premises used: IsScalarTower.toAlgHom, diffToIdealOfQuotientCompEq
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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))
refine_1 :
  ∀ (x : A),
    Eq.{w + 1} (α := B ⧸ I)
      (((AlgHom.comp (Ideal.Quotient.mkₐ R I) f : AlgHom.{u, v, w} R A (B ⧸ I)) : (a : A) → B ⧸ I) x : B ⧸ I)
      (((AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B) : AlgHom.{u, v, w} R A (B ⧸ I)) :
            (a : A) → B ⧸ I)
          x :
        B ⧸ I)
⊢ Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))

Tactic:
ext
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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 : A
⊢ Eq.{w + 1} (α := B ⧸ I)
    (((AlgHom.comp (Ideal.Quotient.mkₐ R I) f : AlgHom.{u, v, w} R A (B ⧸ I)) : (a : A) → B ⧸ I) x : B ⧸ I)
    (((AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B) : AlgHom.{u, v, w} R A (B ⧸ I)) :
          (a : A) → B ⧸ I)
        x :
      B ⧸ I)

Tactic:
simp [e]
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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))
refine_2 :
  Eq (α := B) ((↑((diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯ : (a : A) → ↥I) 1) : B) : B)
    ((↑0 : B) : B)
⊢ Eq.{w + 1} (α := ↥I) ((diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯ : (a : A) → ↥I) 1) 0

Tactic:
ext
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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))
⊢ Eq (α := B) ((↑((diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯ : (a : A) → ↥I) 1) : B) : B)
    ((↑0 : B) : B)

Tactic:
simp
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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
rw :
  Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (IsScalarTower.toAlgHom R A (B ⧸ I))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
⊢ Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))

Tactic:
rw [e]
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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
H :
  ∀ (x : A),
    Eq.{w + 1} (α := B ⧸ I) ((IsScalarTower.toAlgHom R A (B ⧸ I) : (a : A) → B ⧸ I) x : B ⧸ I)
      (((AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B) : AlgHom.{u, v, w} R A (B ⧸ I)) :
            (a : A) → B ⧸ I)
          x :
        B ⧸ I)
⊢ Eq (α := AlgHom.{u, v, w} R A (B ⧸ I)) (IsScalarTower.toAlgHom R A (B ⧸ I))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))

Tactic:
ext
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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 x_1 : A
⊢ Eq.{w + 1} (α := B ⧸ I) ((IsScalarTower.toAlgHom R A (B ⧸ I) : (a : A) → B ⧸ I) x_1 : B ⧸ I)
    (((AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B) : AlgHom.{u, v, w} R A (B ⧸ I)) :
          (a : A) → B ⧸ I)
        x_1 :
      B ⧸ I)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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) ⋯
rw :
  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) ∈
    I * I
⊢ 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

Tactic:
rw [← Ideal.mem_bot, ← hI, pow_two]

Premises used: Ideal.mem_bot, pow_two
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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) ⋯
⊢ HMul.hMul (α := B) (↑((F : (a : A) → ↥I) x) : B) (↑((F : (a : A) → ↥I) y) : B) ∈ I * I

Tactic:
Ideal.mul_mem_mul (F x).2 (F y).2

Premises used: Ideal.mul_mem_mul, DFunLike.coe, Subtype.property
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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) ⋯
⊢ 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) ∈
    I * I

Tactic:
convert! Ideal.mul_mem_mul (F x).2 (F y).2 using 1

Premises used: Ideal.mul_mem_mul, DFunLike.coe, Subtype.property
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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) ⋯
⊢ 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

Tactic:
have : (f x - algebraMap A B x) * (f y - algebraMap A B y) = 0 := by
      rw [← Ideal.mem_bot, ← hI, pow_two]
      convert! Ideal.mul_mem_mul (F x).2 (F y).2 using 1
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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
refine_3 :
  (↑((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)
⊢ (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)

Tactic:
ext
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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
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)
⊢ (↑((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)

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]

Premises used: Submodule.coe_add, LinearMap.coe_mk, IsScalarTower.coe_toAlgHom', LinearMap.toFun_eq_coe, Submodule.coe_mk, diffToIdealOfQuotientCompEq_apply, Submodule.coe_smul_of_tower
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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
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))
⊢ 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:
simp only [map_mul, sub_mul, mul_sub, Algebra.smul_def] at this ⊢

Premises used: mul_sub, sub_mul, map_mul, Algebra.smul_def
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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) =
    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

Premises used: sub_eq_iff_eq_add
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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)
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))
⊢ 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 [this]
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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)
⊢ 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:
ring
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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
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 : A
⊢ (↑((derivationToSquareZeroOfLift I hI f e : (a : A) → ↥I) x) : B) =
    HSub.hSub (α := B) (β := B) ((f : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) x : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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
rw₃ rw₄ : Eq.{w + 1} (α := B) 1 1
⊢ HAdd.hAdd (α := B) (β := B) ((↑((f : (a : A) → ↥I) 1) : B) : B) ((algebraMap A B : (a : A) → B) 1 : B) = 1

Tactic:
rw [map_one (algebraMap _ _), f.map_one_eq_zero, Submodule.coe_zero, zero_add]

Premises used: Algebra.algebraMap, Derivation.map_one_eq_zero, zero_add, Submodule.coe_zero, map_one
-- Module: Mathlib.RingTheory.Derivation.ToSquareZero
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
rw : HMul.hMul (α := B) (↑((f : (a : A) → ↥I) x) : B) (↑((f : (a : A) → ↥I) y) : B) ∈ I * I
⊢ HMul.hMul (α := B) (↑((f : (a : A) → ↥I) x) : B) (↑((f : (a : A) → ↥I) y) : B) = 0

Tactic:
rw [← Ideal.mem_bot, ← hI, pow_two]

Premises used: Ideal.mem_bot, pow_two