-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fe : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }
simp_rw :
  Subalgebra.map.{u_1, u_4, u_3} (A := A[ε])
      ((lift :
          (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
            A[ε] →ₐ[R] B)
        fe)
      ⊤ =
    Subalgebra.map (↑fe : (A →ₐ[R] B) × B).1 ⊤ ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
simp_rw₁ :
  Subalgebra.map
      ((lift :
          (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
            A[ε] →ₐ[R] B)
        fe)
      (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) =
    Subalgebra.map (↑fe : (A →ₐ[R] B) × B).1 ⊤ ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
simp_rw₂ :
  Subalgebra.map
        ((lift :
            (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
              A[ε] →ₐ[R] B)
          fe)
        (AlgHom.range (inlAlgHom R A A)) ⊔
      Subalgebra.map (A := A[ε])
        ((lift :
            (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
              A[ε] →ₐ[R] B)
          fe)
        R[ ε] =
    Subalgebra.map (↑fe : (A →ₐ[R] B) × B).1 ⊤ ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
simp_rw₃ :
  Subalgebra.map
        ((lift :
            (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
              A[ε] →ₐ[R] B)
          fe)
        (AlgHom.range (inlAlgHom R A A)) ⊔
      adjoin R
        (Set.image (α := A[ε])
          (⇑((lift :
                    (a :
                        { fe : (A →ₐ[R] B) × B //
                          fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                      A[ε] →ₐ[R] B)
                  fe :
                AlgHom.{u_1, u_4, u_3} R A[ε] B) :
            (a : A[ε]) → B)
          {ε}) =
    Subalgebra.map (↑fe : (A →ₐ[R] B) × B).1 ⊤ ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
simp_rw₄ :
  AlgHom.range
        (AlgHom.comp
          ((lift :
              (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                A[ε] →ₐ[R] B)
            fe)
          (inlAlgHom R A A)) ⊔
      adjoin R
        (Set.image (α := A[ε])
          (⇑((lift :
                    (a :
                        { fe : (A →ₐ[R] B) × B //
                          fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                      A[ε] →ₐ[R] B)
                  fe :
                AlgHom.{u_1, u_4, u_3} R A[ε] B) :
            (a : A[ε]) → B)
          {ε}) =
    Subalgebra.map (↑fe : (A →ₐ[R] B) × B).1 ⊤ ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
simp_rw₅ :
  AlgHom.range
        (AlgHom.comp
          ((lift :
              (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                A[ε] →ₐ[R] B)
            fe)
          (inlAlgHom R A A)) ⊔
      R[((((lift :
                    (a :
                        { fe : (A →ₐ[R] B) × B //
                          fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                      A[ε] →ₐ[R] B)
                  fe :
                AlgHom.{u_1, u_4, u_3} R A[ε] B) :
              (a : A[ε]) → B)
            ε :
          B)] =
    Subalgebra.map (↑fe : (A →ₐ[R] B) × B).1 ⊤ ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
simp_rw₆ :
  AlgHom.range
        (AlgHom.comp
          ((lift :
              (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                A[ε] →ₐ[R] B)
            fe)
          (inlAlgHom R A A)) ⊔
      R[(↑fe : (A →ₐ[R] B) × B).2] =
    Subalgebra.map (↑fe : (A →ₐ[R] B) × B).1 ⊤ ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
simp_rw₇ :
  (↑fe : (A →ₐ[R] B) × B).1.range ⊔ R[(↑fe : (A →ₐ[R] B) × B).2] =
    Subalgebra.map (↑fe : (A →ₐ[R] B) × B).1 ⊤ ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
⊢ AlgHom.range.{u_1, u_4, u_3} (A := A[ε])
      ((lift :
          (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
            A[ε] →ₐ[R] B)
        fe) =
    (↑fe : (A →ₐ[R] B) × B).1.range ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]

Tactic:
simp_rw [← Algebra.map_top, ← range_inlAlgHom_sup_adjoin_eps, Algebra.map_sup,
    AlgHom.map_adjoin, ← AlgHom.range_comp, Set.image_singleton, lift_apply_eps, lift_comp_inlHom,
    Algebra.map_top]

Premises used: Set.image_singleton, Algebra.map_sup, DualNumber.lift_apply_eps, AlgHom.map_adjoin, DualNumber.range_inlAlgHom_sup_adjoin_eps, Algebra.map_top, DualNumber.lift_comp_inlHom, AlgHom.range_comp