-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
S : Type u_1
R : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Algebra S R
inst_4 : Module S M
inst_5 : Module R M
inst_6 : Module.{u, v} Rᵐᵒᵖ M
inst_7 : SMulCommClass R Rᵐᵒᵖ M
inst_8 : IsScalarTower S R M
inst_9 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
A : Type u_2
inst_10 : Semiring A
inst_11 : Algebra S A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((g : (a : M) → A) y : A) = 0
hfg :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (r •> x) = HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r : A) ((g : (a : M) → A) x : A)
hgf :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (x <• r) = HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((f : (a : R) → A) r : A)
simp_rw :
  Subalgebra.map (lift f g hg hfg hgf) ⊤ =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₁ :
  Subalgebra.map (lift f g hg hfg hgf) (AlgHom.range (inlAlgHom S R M) ⊔ Algebra.adjoin S (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₂ :
  Subalgebra.map (lift f g hg hfg hgf) (AlgHom.range (inlAlgHom S R M)) ⊔
      Subalgebra.map (lift f g hg hfg hgf) (Algebra.adjoin S (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₃ :
  Subalgebra.map (lift f g hg hfg hgf) (AlgHom.range (inlAlgHom S R M)) ⊔
      Algebra.adjoin S (Set.image (α := tsze R M) (⇑(lift f g hg hfg hgf) : (a : tsze R M) → A) (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₄ :
  (AlgHom.comp (lift f g hg hfg hgf) (inlAlgHom S R M)).range ⊔
      Algebra.adjoin S (Set.image (α := tsze R M) (⇑(lift f g hg hfg hgf) : (a : tsze R M) → A) (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₅ :
  f.range ⊔ Algebra.adjoin S (Set.image (α := tsze R M) (⇑(lift f g hg hfg hgf) : (a : tsze R M) → A) (Set.range inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₆ :
  f.range ⊔
      Algebra.adjoin S
        (Set.range.{u_2, v + 1} (ι := M)
          (Function.comp (β := tsze R M) (⇑(lift f g hg hfg hgf) : (a : tsze R M) → A) inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₇ :
  f.range ⊔ Algebra.adjoin S (Set.range fun (x : M) ↦ (lift f g hg hfg hgf : (a : tsze R M) → A) (inr x)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
simp_rw₈ :
  f.range ⊔ Algebra.adjoin S (Set.range fun (x : M) ↦ (g : (a : M) → A) x) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))
⊢ AlgHom.range (lift f g hg hfg hgf) = f.range ⊔ Algebra.adjoin S (Set.range.{u_2, v + 1} (ι := M) (⇑g : (a : M) → A))

Tactic:
simp_rw [← Algebra.map_top, ← range_inlAlgHom_sup_adjoin_range_inr, Algebra.map_sup,
    AlgHom.map_adjoin, ← AlgHom.range_comp, lift_comp_inlHom, ← Set.range_comp, Function.comp_def,
    lift_apply_inr, Algebra.map_top]

Premises used: Set.range_comp, Algebra.map_sup, TrivSqZeroExt.lift_apply_inr, AlgHom.map_adjoin, Function.comp_def, TrivSqZeroExt.lift_comp_inlHom, Algebra.map_top, AlgHom.range_comp, TrivSqZeroExt.range_inlAlgHom_sup_adjoin_range_inr