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
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) ∈ 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
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) ∈ 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
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

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
-- 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
this : HMul.hMul (α := B) (↑((f : (a : A) → ↥I) x) : B) (↑((f : (a : A) → ↥I) y) : B) = 0
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))
⊢ 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)

Tactic:
simp only [map_mul, f.leibniz, add_mul, mul_add, Submodule.coe_add,
        Submodule.coe_smul_of_tower, Algebra.smul_def, this]

Premises used: Submodule.coe_add, add_mul, Derivation.leibniz, map_mul, Submodule.coe_smul_of_tower, Algebra.smul_def, mul_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
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
⊢ 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:
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_1 : HPow.hPow (β := ℕ) I 2 = ⊥
inst_6 : IsScalarTower R A B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : Derivation.{u, v, w} R A ↥I
r : R
⊢ HAdd.hAdd (α := B) (β := B) ((↑((f : (a : A) → ↥I) ((algebraMap R A : (a : R) → A) r)) : B) : B)
      ((algebraMap A B : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B) =
    (algebraMap R B : (a : R) → B) r

Tactic:
simp only [Derivation.map_algebraMap, zero_add, Submodule.coe_zero, ←
        IsScalarTower.algebraMap_apply R A B r]

Premises used: zero_add, Submodule.coe_zero, Derivation.map_algebraMap, IsScalarTower.algebraMap_apply
-- 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
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)
rw₄ 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)
⊢ 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)

Tactic:
rw [liftOfDerivationToSquareZero_apply, map_add, Ideal.Quotient.eq_zero_iff_mem.mpr (d x).prop,
    zero_add, Ideal.Quotient.mk_algebraMap]

Premises used: Iff.mpr, map_add, zero_add, Ideal.Quotient.eq_zero_iff_mem, liftOfDerivationToSquareZero_apply, Subtype.prop, DFunLike.coe, Ideal.Quotient.mk_algebraMap
-- 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
d : Derivation.{u, v, w} R A ↥I
x : A
⊢ HAdd.hAdd (α := B ⧸ I) (β := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) (↑((d : (a : A) → ↥I) x) : B))
      ((algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x : B ⧸ I) =
    (algebraMap A (B ⧸ I) : (a : A) → B ⧸ I) x

Tactic:
simp only [Ideal.Quotient.eq_zero_iff_mem.mpr (d x).prop, zero_add]

Premises used: Iff.mpr, zero_add, Ideal.Quotient.eq_zero_iff_mem, Subtype.prop, DFunLike.coe
-- 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
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))
refine_2 :
  Function.LeftInverse
    (fun
        (f :
          { 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)) }) ↦
      derivationToSquareZeroOfLift I hI (↑f : A →ₐ[R] B) ⋯)
    fun (d : Derivation.{u, v, w} R A ↥I) ↦
    Subtype.mk (p := fun (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)))
      (liftOfDerivationToSquareZero I hI d) ⋯
refine_3 :
  Function.RightInverse
    (fun
        (f :
          { 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)) }) ↦
      derivationToSquareZeroOfLift I hI (↑f : A →ₐ[R] B) ⋯)
    fun (d : Derivation.{u, v, w} R A ↥I) ↦
    Subtype.mk (p := fun (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)))
      (liftOfDerivationToSquareZero I hI d) ⋯
⊢ 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)) }

Tactic:
refine ⟨fun d => ⟨liftOfDerivationToSquareZero I hI d, ?_⟩, fun f =>
    (derivationToSquareZeroOfLift I hI f.1 f.2 :), ?_, ?_⟩
-- 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
d : Derivation.{u, v, w} R A ↥I
refine_1 :
  ∀ (x : A),
    Eq.{w + 1} (α := B ⧸ I)
      (((AlgHom.comp (Ideal.Quotient.mkₐ R I) (liftOfDerivationToSquareZero I hI d) : AlgHom.{u, v, w} R A (B ⧸ I)) :
            (a : A) → B ⧸ I)
          x :
        B ⧸ I)
      ((IsScalarTower.toAlgHom 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) (liftOfDerivationToSquareZero I hI d))
    (IsScalarTower.toAlgHom R A (B ⧸ I))

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

Tactic:
liftOfDerivationToSquareZero_mk_apply I hI d x

Premises used: Submodule.Quotient.mk, liftOfDerivationToSquareZero_mk_apply
-- 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
d : Derivation.{u, v, w} R A ↥I
x : A
⊢ Eq.{w + 1} (α := B ⧸ I)
    (((AlgHom.comp (Ideal.Quotient.mkₐ R I) (liftOfDerivationToSquareZero I hI d) : AlgHom.{u, v, w} R A (B ⧸ I)) :
          (a : A) → B ⧸ I)
        x :
      B ⧸ I)
    ((IsScalarTower.toAlgHom R A (B ⧸ I) : (a : A) → B ⧸ I) x : B ⧸ I)

Tactic:
exact liftOfDerivationToSquareZero_mk_apply I hI d x

Premises used: liftOfDerivationToSquareZero_mk_apply
-- 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
d : Derivation.{u, v, w} R A ↥I
refine_2 :
  ∀ (x : A),
    Eq.{w + 1} (α := B)
      (↑((((fun
                      (f :
                        { 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)) }) ↦
                    derivationToSquareZeroOfLift I hI (↑f : A →ₐ[R] B) ⋯)
                  ((fun (d : Derivation.{u, v, w} R A ↥I) ↦
                      (Subtype.mk (p := fun (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)))
                          (liftOfDerivationToSquareZero I hI d) ⋯ :
                        { 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)) }))
                    d) :
                Derivation.{u, v, w} R A ↥I) :
              (a : A) → ↥I)
            x) :
        B)
      (↑((d : (a : A) → ↥I) x) : B)
⊢ (fun
          (f :
            { 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)) }) ↦
        derivationToSquareZeroOfLift I hI (↑f : A →ₐ[R] B) ⋯)
      ((fun (d : Derivation.{u, v, w} R A ↥I) ↦
          (Subtype.mk (p := fun (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)))
              (liftOfDerivationToSquareZero I hI d) ⋯ :
            { 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)) }))
        d) =
    d

Tactic:
ext x
-- 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
d : Derivation.{u, v, w} R A ↥I
x : A
⊢ Eq.{w + 1} (α := B)
    (↑((((fun
                    (f :
                      { 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)) }) ↦
                  derivationToSquareZeroOfLift I hI (↑f : A →ₐ[R] B) ⋯)
                ((fun (d : Derivation.{u, v, w} R A ↥I) ↦
                    (Subtype.mk (p := fun (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)))
                        (liftOfDerivationToSquareZero I hI d) ⋯ :
                      { 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)) }))
                  d) :
              Derivation.{u, v, w} R A ↥I) :
            (a : A) → ↥I)
          x) :
      B)
    (↑((d : (a : A) → ↥I) x) : B)

Tactic:
add_sub_cancel_right (d x : B) (algebraMap A B x)

Premises used: Algebra.algebraMap, add_sub_cancel_right, Subtype.val, DFunLike.coe
-- 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
d : Derivation.{u, v, w} R A ↥I
x : A
⊢ Eq.{w + 1} (α := B)
    (↑((((fun
                    (f :
                      { 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)) }) ↦
                  derivationToSquareZeroOfLift I hI (↑f : A →ₐ[R] B) ⋯)
                ((fun (d : Derivation.{u, v, w} R A ↥I) ↦
                    (Subtype.mk (p := fun (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)))
                        (liftOfDerivationToSquareZero I hI d) ⋯ :
                      { 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)) }))
                  d) :
              Derivation.{u, v, w} R A ↥I) :
            (a : A) → ↥I)
          x) :
      B)
    (↑((d : (a : A) → ↥I) x) : B)

Tactic:
exact add_sub_cancel_right (d x : B) (algebraMap A B x)

Premises used: Algebra.algebraMap, add_sub_cancel_right, Subtype.val, DFunLike.coe
-- 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
hf :
  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)
    (((↑((fun (d : Derivation.{u, v, w} R A ↥I) ↦
                  (Subtype.mk (p := fun (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)))
                      (liftOfDerivationToSquareZero I hI d) ⋯ :
                    { 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)) }))
                ((fun
                      (f :
                        { 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)) }) ↦
                    derivationToSquareZeroOfLift I hI (↑f : A →ₐ[R] B) ⋯)
                  (Subtype.mk (p := fun (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)))
                    f hf))) :
            A →ₐ[R] B) :
          (a : A) → B)
        x :
      B)
    (((↑(Subtype.mk (p := fun (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)))
                f hf) :
            A →ₐ[R] B) :
          (a : A) → B)
        x :
      B)

Tactic:
sub_add_cancel (f x) (algebraMap A B x)

Premises used: Algebra.algebraMap, sub_add_cancel, DFunLike.coe
-- 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
hf :
  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)
    (((↑((fun (d : Derivation.{u, v, w} R A ↥I) ↦
                  (Subtype.mk (p := fun (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)))
                      (liftOfDerivationToSquareZero I hI d) ⋯ :
                    { 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)) }))
                ((fun
                      (f :
                        { 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)) }) ↦
                    derivationToSquareZeroOfLift I hI (↑f : A →ₐ[R] B) ⋯)
                  (Subtype.mk (p := fun (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)))
                    f hf))) :
            A →ₐ[R] B) :
          (a : A) → B)
        x :
      B)
    (((↑(Subtype.mk (p := fun (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)))
                f hf) :
            A →ₐ[R] B) :
          (a : A) → B)
        x :
      B)

Tactic:
exact sub_add_cancel (f x) (algebraMap A B x)

Premises used: Algebra.algebraMap, sub_add_cancel, DFunLike.coe
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
⊢ Ne (α := Ideal R) (maximalIdeal R) ⊥

Tactic:
not_a_field'

Premises used: IsDiscreteValuationRing.not_a_field'
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
⊢ ¬IsField R

Tactic:
IsLocalRing.isField_iff_maximalIdeal_eq.not.mpr (not_a_field R)

Premises used: Iff.mpr, Iff.not, IsDiscreteValuationRing.not_a_field, IsLocalRing.isField_iff_maximalIdeal_eq
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})
⊢ ¬IsUnit ϖ

Tactic:
have h2 : ¬IsUnit ϖ := show ϖ ∈ maximalIdeal R from h.symm ▸ Submodule.mem_span_singleton_self ϖ
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})
h2 : ¬IsUnit ϖ
⊢ Irreducible ϖ

Tactic:
⟨h2, ?_⟩

Premises used: Irreducible.mk
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})
h2 : ¬IsUnit ϖ
refine : ∀ ⦃a b : R⦄, ϖ = a * b → IsUnit a ∨ IsUnit b
⊢ Irreducible ϖ

Tactic:
refine ⟨h2, ?_⟩
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})
h2 : ¬IsUnit ϖ
a b : R
hab : ϖ = a * b
by_contra! :
  ∀ (ha : Membership.mem (γ := Ideal R) (maximalIdeal R) a) (hb : Membership.mem (γ := Ideal R) (maximalIdeal R) b),
    False
⊢ IsUnit a ∨ IsUnit b

Tactic:
by_contra! ⟨ha : a ∈ maximalIdeal R, hb : b ∈ maximalIdeal R⟩

Premises used: IsLocalRing.maximalIdeal
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : Eq (α := Ideal R) (maximalIdeal R) (span {ϖ})
h2 : ¬IsUnit ϖ
a b : R
hab : ϖ = a * b
ha : Membership.mem (γ := Ideal R) (maximalIdeal R) a
hb : Membership.mem (γ := Ideal R) (maximalIdeal R) b
⊢ ∃ (a_1 : R), a_1 * ϖ = a

Tactic:
rw [h, mem_span_singleton'] at ha hb

Premises used: Ideal.mem_span_singleton'