[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
f₁ f₂ : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
⊢ ∀ (c : A), ↑(AlgHom.toLinearMap f₁ - AlgHom.toLinearMap f₂) c ∈ Submodule.restrictScalars R I
[PROOFSTEP]
intro x
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
f₁ f₂ : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
x : A
⊢ ↑(AlgHom.toLinearMap f₁ - AlgHom.toLinearMap f₂) x ∈ Submodule.restrictScalars R I
[PROOFSTEP]
change f₁ x - f₂ x ∈ I
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
f₁ f₂ : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
x : A
⊢ ↑f₁ x - ↑f₂ x ∈ I
[PROOFSTEP]
rw [← Ideal.Quotient.eq, ← Ideal.Quotient.mkₐ_eq_mk R, ← AlgHom.comp_apply, e]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
f₁ f₂ : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
x : A
⊢ ↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂) x = ↑(Ideal.Quotient.mkₐ R I) (↑f₂ x)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
⊢ Derivation R A { x // x ∈ I }
[PROOFSTEP]
refine'
  {
    diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
      _ with
    map_one_eq_zero' := _
    leibniz' := _ }
[GOAL]
case refine'_1
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B)
[PROOFSTEP]
rw [e]
[GOAL]
case refine'_1
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
⊢ IsScalarTower.toAlgHom R A (B ⧸ I) = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B)
[PROOFSTEP]
ext
[GOAL]
case refine'_1.H
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
x✝ : A
⊢ ↑(IsScalarTower.toAlgHom R A (B ⧸ I)) x✝ = ↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B)) x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
src✝ : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
⊢ ↑{ toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : A),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
      1 =
    0
[PROOFSTEP]
ext
[GOAL]
case refine'_2.a
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
src✝ : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
⊢ ↑(↑{ toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : A),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
        1) =
    ↑0
[PROOFSTEP]
change f 1 - algebraMap A B 1 = 0
[GOAL]
case refine'_2.a
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
src✝ : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
⊢ ↑f 1 - ↑(algebraMap A B) 1 = 0
[PROOFSTEP]
rw [map_one, map_one, sub_self]
[GOAL]
case refine'_3
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
src✝ : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
⊢ ∀ (a b : A),
    ↑{ toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : A),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
        (a * b) =
      a •
          ↑{ toAddHom := src✝.toAddHom,
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : A),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
            b +
        b •
          ↑{ toAddHom := src✝.toAddHom,
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : A),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
            a
[PROOFSTEP]
intro x y
[GOAL]
case refine'_3
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
src✝ : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
x y : A
⊢ ↑{ toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : A),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
      (x * y) =
    x •
        ↑{ toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : A),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
          y +
      y •
        ↑{ toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : A),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
          x
[PROOFSTEP]
let F := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) (by rw [e]; ext; rfl)
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
src✝ : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
x y : A
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B)
[PROOFSTEP]
rw [e]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
src✝ : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
x y : A
⊢ IsScalarTower.toAlgHom R A (B ⧸ I) = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B)
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
src✝ : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
x y x✝ : A
⊢ ↑(IsScalarTower.toAlgHom R A (B ⧸ I)) x✝ = ↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B)) x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
src✝ : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
x y : A
F : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
⊢ ↑{ toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : A),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
      (x * y) =
    x •
        ↑{ toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : A),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
          y +
      y •
        ↑{ toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : A),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
          x
[PROOFSTEP]
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
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
src✝ : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
x y : A
F : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
⊢ (↑f x - ↑(algebraMap A B) x) * (↑f y - ↑(algebraMap A B) y) = 0
[PROOFSTEP]
rw [← Ideal.mem_bot, ← hI, pow_two]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
src✝ : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
x y : A
F : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
⊢ (↑f x - ↑(algebraMap A B) x) * (↑f y - ↑(algebraMap A B) y) ∈ I * I
[PROOFSTEP]
convert Ideal.mul_mem_mul (F x).2 (F y).2 using 1
[GOAL]
case refine'_3
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
src✝ : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
x y : A
F : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
this : (↑f x - ↑(algebraMap A B) x) * (↑f y - ↑(algebraMap A B) y) = 0
⊢ ↑{ toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : A),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
      (x * y) =
    x •
        ↑{ toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : A),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
          y +
      y •
        ↑{ toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : A),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
          x
[PROOFSTEP]
ext
[GOAL]
case refine'_3.a
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
src✝ : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
x y : A
F : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
this : (↑f x - ↑(algebraMap A B) x) * (↑f y - ↑(algebraMap A B) y) = 0
⊢ ↑(↑{ toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : A),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
        (x * y)) =
    ↑(x •
          ↑{ toAddHom := src✝.toAddHom,
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : A),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
            y +
        y •
          ↑{ toAddHom := src✝.toAddHom,
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : A),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
            x)
[PROOFSTEP]
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]
[GOAL]
case refine'_3.a
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
src✝ : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
x y : A
F : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
this : (↑f x - ↑(algebraMap A B) x) * (↑f y - ↑(algebraMap A B) y) = 0
⊢ ↑(↑(diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
              (_ :
                AlgHom.comp (Ideal.Quotient.mkₐ R I) f =
                  AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))).toAddHom
        (x * y)) =
    x •
        ↑(↑(diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
                  (_ :
                    AlgHom.comp (Ideal.Quotient.mkₐ R I) f =
                      AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))).toAddHom
            y) +
      y •
        ↑(↑(diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
                  (_ :
                    AlgHom.comp (Ideal.Quotient.mkₐ R I) f =
                      AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))).toAddHom
            x)
[PROOFSTEP]
simp only [map_mul, sub_mul, mul_sub, Algebra.smul_def] at this ⊢
[GOAL]
case refine'_3.a
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
src✝ : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
x y : A
F : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
this :
  ↑f x * ↑f y - ↑(algebraMap A B) x * ↑f y - (↑f x * ↑(algebraMap A B) y - ↑(algebraMap A B) x * ↑(algebraMap A B) y) =
    0
⊢ ↑(↑(diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
              (_ :
                AlgHom.comp (Ideal.Quotient.mkₐ R I) f =
                  AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))).toAddHom
        (x * y)) =
    ↑(algebraMap A B) x *
        ↑(↑(diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
                  (_ :
                    AlgHom.comp (Ideal.Quotient.mkₐ R I) f =
                      AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))).toAddHom
            y) +
      ↑(algebraMap A B) y *
        ↑(↑(diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
                  (_ :
                    AlgHom.comp (Ideal.Quotient.mkₐ R I) f =
                      AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))).toAddHom
            x)
[PROOFSTEP]
rw [sub_eq_iff_eq_add, sub_eq_iff_eq_add] at this
[GOAL]
case refine'_3.a
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
src✝ : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
x y : A
F : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
this :
  ↑f x * ↑f y =
    0 + (↑f x * ↑(algebraMap A B) y - ↑(algebraMap A B) x * ↑(algebraMap A B) y) + ↑(algebraMap A B) x * ↑f y
⊢ ↑(↑(diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
              (_ :
                AlgHom.comp (Ideal.Quotient.mkₐ R I) f =
                  AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))).toAddHom
        (x * y)) =
    ↑(algebraMap A B) x *
        ↑(↑(diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
                  (_ :
                    AlgHom.comp (Ideal.Quotient.mkₐ R I) f =
                      AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))).toAddHom
            y) +
      ↑(algebraMap A B) y *
        ↑(↑(diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
                  (_ :
                    AlgHom.comp (Ideal.Quotient.mkₐ R I) f =
                      AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))).toAddHom
            x)
[PROOFSTEP]
simp only [LinearMap.coe_toAddHom, diffToIdealOfQuotientCompEq_apply, map_mul, this, IsScalarTower.coe_toAlgHom']
[GOAL]
case refine'_3.a
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
src✝ : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
x y : A
F : A →ₗ[R] { x // x ∈ I } :=
  diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B)
    (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A B))
this :
  ↑f x * ↑f y =
    0 + (↑f x * ↑(algebraMap A B) y - ↑(algebraMap A B) x * ↑(algebraMap A B) y) + ↑(algebraMap A B) x * ↑f y
⊢ 0 + (↑f x * ↑(algebraMap A B) y - ↑(algebraMap A B) x * ↑(algebraMap A B) y) + ↑(algebraMap A B) x * ↑f y -
      ↑(algebraMap A B) x * ↑(algebraMap A B) y =
    ↑(algebraMap A B) x * (↑f y - ↑(algebraMap A B) y) + ↑(algebraMap A B) y * (↑f x - ↑(algebraMap A B) x)
[PROOFSTEP]
ring
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : Derivation R A { x // x ∈ I }
src✝ : A →ₗ[R] B :=
  LinearMap.comp (Submodule.subtype (Submodule.restrictScalars R I)) ↑f +
    AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)
⊢ (fun x => ↑(↑f x) + ↑(algebraMap A B) x) 1 = 1
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : Derivation R A { x // x ∈ I }
src✝ : A →ₗ[R] B :=
  LinearMap.comp (Submodule.subtype (Submodule.restrictScalars R I)) ↑f +
    AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)
⊢ ↑(↑f 1) + ↑(algebraMap A B) 1 = 1
[PROOFSTEP]
rw [map_one, f.map_one_eq_zero, Submodule.coe_zero, zero_add]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : Derivation R A { x // x ∈ I }
src✝ : A →ₗ[R] B :=
  LinearMap.comp (Submodule.subtype (Submodule.restrictScalars R I)) ↑f +
    AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)
x y : A
⊢ OneHom.toFun
      { toFun := fun x => ↑(↑f x) + ↑(algebraMap A B) x,
        map_one' := (_ : (fun x => ↑(↑f x) + ↑(algebraMap A B) x) 1 = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := fun x => ↑(↑f x) + ↑(algebraMap A B) x,
          map_one' := (_ : (fun x => ↑(↑f x) + ↑(algebraMap A B) x) 1 = 1) }
        x *
      OneHom.toFun
        { toFun := fun x => ↑(↑f x) + ↑(algebraMap A B) x,
          map_one' := (_ : (fun x => ↑(↑f x) + ↑(algebraMap A B) x) 1 = 1) }
        y
[PROOFSTEP]
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
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : Derivation R A { x // x ∈ I }
src✝ : A →ₗ[R] B :=
  LinearMap.comp (Submodule.subtype (Submodule.restrictScalars R I)) ↑f +
    AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)
x y : A
⊢ ↑(↑f x) * ↑(↑f y) = 0
[PROOFSTEP]
rw [← Ideal.mem_bot, ← hI, pow_two]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : Derivation R A { x // x ∈ I }
src✝ : A →ₗ[R] B :=
  LinearMap.comp (Submodule.subtype (Submodule.restrictScalars R I)) ↑f +
    AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)
x y : A
⊢ ↑(↑f x) * ↑(↑f y) ∈ I * I
[PROOFSTEP]
convert Ideal.mul_mem_mul (f x).2 (f y).2 using 1
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : Derivation R A { x // x ∈ I }
src✝ : A →ₗ[R] B :=
  LinearMap.comp (Submodule.subtype (Submodule.restrictScalars R I)) ↑f +
    AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)
x y : A
this : ↑(↑f x) * ↑(↑f y) = 0
⊢ OneHom.toFun
      { toFun := fun x => ↑(↑f x) + ↑(algebraMap A B) x,
        map_one' := (_ : (fun x => ↑(↑f x) + ↑(algebraMap A B) x) 1 = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := fun x => ↑(↑f x) + ↑(algebraMap A B) x,
          map_one' := (_ : (fun x => ↑(↑f x) + ↑(algebraMap A B) x) 1 = 1) }
        x *
      OneHom.toFun
        { toFun := fun x => ↑(↑f x) + ↑(algebraMap A B) x,
          map_one' := (_ : (fun x => ↑(↑f x) + ↑(algebraMap A B) x) 1 = 1) }
        y
[PROOFSTEP]
simp only [map_mul, f.leibniz, add_mul, mul_add, Submodule.coe_add, Submodule.coe_smul_of_tower, Algebra.smul_def, this]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : Derivation R A { x // x ∈ I }
src✝ : A →ₗ[R] B :=
  LinearMap.comp (Submodule.subtype (Submodule.restrictScalars R I)) ↑f +
    AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)
x y : A
this : ↑(↑f x) * ↑(↑f y) = 0
⊢ ↑(algebraMap A B) x * ↑(↑f y) + ↑(algebraMap A B) y * ↑(↑f x) + ↑(algebraMap A B) x * ↑(algebraMap A B) y =
    0 + ↑(algebraMap A B) x * ↑(↑f y) + (↑(↑f x) * ↑(algebraMap A B) y + ↑(algebraMap A B) x * ↑(algebraMap A B) y)
[PROOFSTEP]
ring
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : Derivation R A { x // x ∈ I }
src✝ : A →ₗ[R] B :=
  LinearMap.comp (Submodule.subtype (Submodule.restrictScalars R I)) ↑f +
    AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B)
r : R
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := fun x => ↑(↑f x) + ↑(algebraMap A B) x,
                    map_one' := (_ : (fun x => ↑(↑f x) + ↑(algebraMap A B) x) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : A),
                      OneHom.toFun
                          { toFun := fun x => ↑(↑f x) + ↑(algebraMap A B) x,
                            map_one' := (_ : (fun x => ↑(↑f x) + ↑(algebraMap A B) x) 1 = 1) }
                          (x * y) =
                        OneHom.toFun
                            { toFun := fun x => ↑(↑f x) + ↑(algebraMap A B) x,
                              map_one' := (_ : (fun x => ↑(↑f x) + ↑(algebraMap A B) x) 1 = 1) }
                            x *
                          OneHom.toFun
                            { toFun := fun x => ↑(↑f x) + ↑(algebraMap A B) x,
                              map_one' := (_ : (fun x => ↑(↑f x) + ↑(algebraMap A B) x) 1 = 1) }
                            y) },
            map_zero' :=
              (_ :
                ↑(LinearMap.comp (Submodule.subtype (Submodule.restrictScalars R I)) ↑f +
                        AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B))
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x y : A),
                  AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) })
      (↑(algebraMap R A) r) =
    ↑(algebraMap R B) r
[PROOFSTEP]
simp only [Derivation.map_algebraMap, eq_self_iff_true, zero_add, Submodule.coe_zero, ←
  IsScalarTower.algebraMap_apply R A B r]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
d : Derivation R A { x // x ∈ I }
x : A
⊢ ↑(Ideal.Quotient.mk I) (↑(liftOfDerivationToSquareZero I hI d) x) = ↑(algebraMap A (B ⧸ I)) x
[PROOFSTEP]
rw [liftOfDerivationToSquareZero_apply, map_add, Ideal.Quotient.eq_zero_iff_mem.mpr (d x).prop, zero_add]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
d : Derivation R A { x // x ∈ I }
x : A
⊢ ↑(Ideal.Quotient.mk I) (↑(algebraMap A B) x) = ↑(algebraMap A (B ⧸ I)) x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
d : Derivation R A { x // x ∈ I }
x : A
⊢ ↑(Ideal.Quotient.mk I) ↑(↑d x) + ↑(algebraMap A (B ⧸ I)) x = ↑(algebraMap A (B ⧸ I)) x
[PROOFSTEP]
simp only [Ideal.Quotient.eq_zero_iff_mem.mpr (d x).prop, zero_add]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
⊢ Derivation R A { x // x ∈ I } ≃ { f // AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I) }
[PROOFSTEP]
refine'
  ⟨fun d => ⟨liftOfDerivationToSquareZero I hI d, _⟩, fun f => (derivationToSquareZeroOfLift I hI f.1 f.2 : _), _, _⟩
[GOAL]
case refine'_1
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
d : Derivation R A { x // x ∈ I }
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I) (liftOfDerivationToSquareZero I hI d) = IsScalarTower.toAlgHom R A (B ⧸ I)
[PROOFSTEP]
ext x
[GOAL]
case refine'_1.H
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
d : Derivation R A { x // x ∈ I }
x : A
⊢ ↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) (liftOfDerivationToSquareZero I hI d)) x =
    ↑(IsScalarTower.toAlgHom R A (B ⧸ I)) x
[PROOFSTEP]
exact liftOfDerivationToSquareZero_mk_apply I hI d x
[GOAL]
case refine'_2
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
⊢ Function.LeftInverse
    (fun f =>
      derivationToSquareZeroOfLift I hI ↑f
        (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) ↑f = IsScalarTower.toAlgHom R A (B ⧸ I)))
    fun d =>
    { val := liftOfDerivationToSquareZero I hI d,
      property :=
        (_ :
          AlgHom.comp (Ideal.Quotient.mkₐ R I) (liftOfDerivationToSquareZero I hI d) =
            IsScalarTower.toAlgHom R A (B ⧸ I)) }
[PROOFSTEP]
intro d
[GOAL]
case refine'_2
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
d : Derivation R A { x // x ∈ I }
⊢ (fun f =>
        derivationToSquareZeroOfLift I hI ↑f
          (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) ↑f = IsScalarTower.toAlgHom R A (B ⧸ I)))
      ((fun d =>
          { val := liftOfDerivationToSquareZero I hI d,
            property :=
              (_ :
                AlgHom.comp (Ideal.Quotient.mkₐ R I) (liftOfDerivationToSquareZero I hI d) =
                  IsScalarTower.toAlgHom R A (B ⧸ I)) })
        d) =
    d
[PROOFSTEP]
ext x
[GOAL]
case refine'_2.H.a
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
d : Derivation R A { x // x ∈ I }
x : A
⊢ ↑(↑((fun f =>
              derivationToSquareZeroOfLift I hI ↑f
                (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) ↑f = IsScalarTower.toAlgHom R A (B ⧸ I)))
            ((fun d =>
                { val := liftOfDerivationToSquareZero I hI d,
                  property :=
                    (_ :
                      AlgHom.comp (Ideal.Quotient.mkₐ R I) (liftOfDerivationToSquareZero I hI d) =
                        IsScalarTower.toAlgHom R A (B ⧸ I)) })
              d))
        x) =
    ↑(↑d x)
[PROOFSTEP]
exact add_sub_cancel (d x : B) (algebraMap A B x)
[GOAL]
case refine'_3
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
⊢ Function.RightInverse
    (fun f =>
      derivationToSquareZeroOfLift I hI ↑f
        (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) ↑f = IsScalarTower.toAlgHom R A (B ⧸ I)))
    fun d =>
    { val := liftOfDerivationToSquareZero I hI d,
      property :=
        (_ :
          AlgHom.comp (Ideal.Quotient.mkₐ R I) (liftOfDerivationToSquareZero I hI d) =
            IsScalarTower.toAlgHom R A (B ⧸ I)) }
[PROOFSTEP]
rintro ⟨f, hf⟩
[GOAL]
case refine'_3.mk
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
hf : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
⊢ (fun d =>
        { val := liftOfDerivationToSquareZero I hI d,
          property :=
            (_ :
              AlgHom.comp (Ideal.Quotient.mkₐ R I) (liftOfDerivationToSquareZero I hI d) =
                IsScalarTower.toAlgHom R A (B ⧸ I)) })
      ((fun f =>
          derivationToSquareZeroOfLift I hI ↑f
            (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) ↑f = IsScalarTower.toAlgHom R A (B ⧸ I)))
        { val := f, property := hf }) =
    { val := f, property := hf }
[PROOFSTEP]
ext x
[GOAL]
case refine'_3.mk.a.H
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : A →ₐ[R] B
hf : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)
x : A
⊢ ↑↑((fun d =>
              { val := liftOfDerivationToSquareZero I hI d,
                property :=
                  (_ :
                    AlgHom.comp (Ideal.Quotient.mkₐ R I) (liftOfDerivationToSquareZero I hI d) =
                      IsScalarTower.toAlgHom R A (B ⧸ I)) })
            ((fun f =>
                derivationToSquareZeroOfLift I hI ↑f
                  (_ : AlgHom.comp (Ideal.Quotient.mkₐ R I) ↑f = IsScalarTower.toAlgHom R A (B ⧸ I)))
              { val := f, property := hf }))
      x =
    ↑↑{ val := f, property := hf } x
[PROOFSTEP]
exact sub_add_cancel (f x) (algebraMap A B x)