-- Module: Mathlib.Algebra.Central.End
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : CommSemiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
inst_7 : Algebra S R
inst_8 : IsScalarTower S R M
M₂ : Type u_4
inst_9 : AddCommMonoid M₂
inst_10 : Module R M₂
inst_11 : Module S M₂
inst_12 : SMulCommClass R S M₂
inst_13 : IsScalarTower S R M₂
inst_14 : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
simp_rw :
  (∀ (a : End R M),
      Eq.{u_4 + 1} (α := End R M₂)
        (((conjAlgEquiv S g : AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) : (a : End R M) → End R M₂) a : End R M₂)
        (((conjAlgEquiv S f : AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) : (a : End R M) → End R M₂) a :
          End R M₂)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₁ :
  (∀ (a : End R M),
      (↑g : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) = (↑f : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑f.symm : M₂ →ₗ[R] M)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₂ :
  (∀ (a : End R M),
      a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) = (↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂) ∘ₗ a ∘ₗ (↑f.symm : M₂ →ₗ[R] M)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₃ :
  (∀ (a : End R M),
      a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) = (((↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂)) ∘ₗ a) ∘ₗ (↑f.symm : M₂ →ₗ[R] M)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₄ :
  (∀ (a : End R M),
      (a ∘ₗ (↑g.symm : M₂ →ₗ[R] M)) ∘ₗ (↑f : M →ₗ[R] M₂) = ((↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂)) ∘ₗ a) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₅ :
  (∀ (a : End R M),
      a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂) = (↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂) ∘ₗ a) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₆ :
  (∀ (a : End R M),
      a ∘ₗ (↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂) = ((↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂)) ∘ₗ a) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₇ :
  (∀ (a : End R M), a ∘ₗ (↑(f ≪≫ₗ g.symm) : M →ₗ[R] M) = (↑(f ≪≫ₗ g.symm) : M →ₗ[R] M) ∘ₗ a) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₈ :
  (∀ (a : End R M), a * (↑(f ≪≫ₗ g.symm) : M →ₗ[R] M) = (↑(f ≪≫ₗ g.symm) : M →ₗ[R] M) * a) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₉ :
  Membership.mem (γ := Subalgebra S (End R M)) (Subalgebra.center S (End R M)) (↑(f ≪≫ₗ g.symm) : M →ₗ[R] M) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₁₀ :
  Membership.mem (γ := Subalgebra S (End R M)) ⊥ (↑(f ≪≫ₗ g.symm) : M →ₗ[R] M) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₁₁ :
  Membership.mem (γ := Subalgebra S (End R M)) ⊥ ((↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₁₂ :
  Membership.mem (γ := Set (End R M))
      (Set.range.{u_3, u_2 + 1} (ι := S) (⇑(algebraMap S (End R M)) : (a : S) → End R M))
      ((↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₁₃ :
  (∃ (y : S), (algebraMap S (End R M) : (a : S) → End R M) y = (↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₁₄ :
  (∃ (y : S), HSMul.hSMul (β := End R M) y 1 = (↑g.symm : M₂ →ₗ[R] M) ∘ₗ (↑f : M →ₗ[R] M₂)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₁₅ :
  (∃ (y : S), (↑g : M →ₗ[R] M₂) ∘ₗ HSMul.hSMul (β := End R M) y 1 = (↑f : M →ₗ[R] M₂)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₁₆ :
  (∃ (y : S), (↑f : M →ₗ[R] M₂) = (↑g : M →ₗ[R] M₂) ∘ₗ HSMul.hSMul (β := End R M) y 1) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₁₇ :
  (∃ (y : S),
      ∀ (x : M),
        Eq.{u_4 + 1} (α := M₂) (((↑f : M →ₗ[R] M₂) : (a : M) → M₂) x : M₂)
          (((↑g : M →ₗ[R] M₂) ∘ₗ HSMul.hSMul (β := End R M) y 1 : (a : M) → M₂) x : M₂)) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)
simp_rw₁₈ :
  (∃ (y : S),
      ∀ (x : M),
        Eq.{u_4 + 1} (α := M₂) (((↑f : M →ₗ[R] M₂) : (a : M) → M₂) x : M₂)
          (((↑g : M →ₗ[R] M₂) ∘ₗ HSMul.hSMul (β := End R M) y 1 : (a : M) → M₂) x : M₂)) ↔
    ∃ (α : S), ∀ (x : M), (f : (a : M) → M₂) x = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂) x
simp_rw₁₉ :
  (∃ (y : S),
      ∀ (x : M),
        Eq.{u_4 + 1} (α := M₂) (((↑f : M →ₗ[R] M₂) : (a : M) → M₂) x : M₂)
          (((↑g : M →ₗ[R] M₂) : (a : M) → M₂) ((HSMul.hSMul (β := End R M) y 1 : (a : M) → M) x : M) : M₂)) ↔
    ∃ (α : S), ∀ (x : M), (f : (a : M) → M₂) x = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂) x
simp_rw₂₀ :
  (∃ (y : S),
      ∀ (x : M),
        Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂)
          ((g : (a : M) → M₂) ((HSMul.hSMul (β := End R M) y 1 : (a : M) → M) x : M) : M₂)) ↔
    ∃ (α : S), ∀ (x : M), (f : (a : M) → M₂) x = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂) x
simp_rw₂₁ :
  (∃ (y : S),
      ∀ (x : M),
        Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂)
          ((g : (a : M) → M₂) (HSMul.hSMul (β := M) y ((1 : (a : M) → M) x : M)) : M₂)) ↔
    ∃ (α : S), ∀ (x : M), (f : (a : M) → M₂) x = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂) x
simp_rw₂₂ :
  (∃ (y : S), ∀ (x : M), Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((g : (a : M) → M₂) (y • x) : M₂)) ↔
    ∃ (α : S), ∀ (x : M), (f : (a : M) → M₂) x = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂) x
simp_rw₂₃ :
  (∃ (y : S), ∀ (x : M), Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((g : (a : M) → M₂) (y • x) : M₂)) ↔
    ∃ (α : S), ∀ (x : M), (f : (a : M) → M₂) x = HSMul.hSMul (β := M₂) α ((g : (a : M) → M₂) x : M₂)
⊢ Eq (α := AlgEquiv.{u_2, u_3, u_4} S (End R M) (End R M₂)) (conjAlgEquiv S g) (conjAlgEquiv S f) ↔
    ∃ (α : S), (⇑f : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) α (⇑g : (a : M) → M₂)

Tactic:
simp_rw [AlgEquiv.ext_iff, conjAlgEquiv_apply, ← eq_toLinearMap_symm_comp, ← comp_assoc,
    eq_comp_toLinearMap_symm, comp_assoc, ← comp_assoc _ _ g.symm.toLinearMap, comp_coe,
    ← End.mul_eq_comp, ← Subalgebra.mem_center_iff (R := S), Algebra.IsCentral.center_eq_bot,
    ← comp_coe, Algebra.mem_bot, Set.mem_range, Algebra.algebraMap_eq_smul_one,
    eq_toLinearMap_symm_comp, eq_comm, LinearMap.ext_iff, funext_iff, comp_apply, coe_coe,
    LinearMap.smul_apply, End.one_apply, Pi.smul_apply, LinearMapClass.map_smul_of_tower g]

Premises used: Set.mem_range, LinearEquiv.symm, Module.End.mul_eq_comp, Subalgebra.mem_center_iff, LinearMap.smul_apply, LinearEquiv.conjAlgEquiv_apply, Algebra.mem_bot, LinearMap.comp_assoc, AlgEquiv.ext_iff, funext_iff, LinearMap.comp_apply, LinearMapClass.map_smul_of_tower, LinearEquiv.eq_toLinearMap_symm_comp, LinearMap.ext_iff, LinearEquiv.eq_comp_toLinearMap_symm, eq_comm, Algebra.algebraMap_eq_smul_one, Module.End.one_apply, LinearEquiv.comp_coe, LinearEquiv.toLinearMap, Algebra.IsCentral.center_eq_bot, LinearEquiv.coe_coe, Pi.smul_apply