awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
b : M
⊢ (e.symm : (a : M₂) → M) ((e : (a : M) → M₂) b : M₂) = b

Tactic:
e.left_inv b

Premises used: LinearEquiv.left_inv
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
⊢ (↑e : M →ₛₗ[σ] M₂) ∘ₛₗ (↑e.symm : M₂ →ₛₗ[σ'] M) = LinearMap.id

Tactic:
LinearMap.ext e.apply_symm_apply

Premises used: LinearMap.ext, LinearEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
⊢ (↑e.symm : M₂ →ₛₗ[σ'] M) ∘ₛₗ (↑e : M →ₛₗ[σ] M₂) = LinearMap.id

Tactic:
LinearMap.ext e.symm_apply_apply

Premises used: LinearMap.ext, LinearEquiv.symm_apply_apply
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₂] M₂
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
h :
  ∀ (x : M₃),
    Eq.{u_9 + 1} (α := M₂) (((↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ f : (a : M₃) → M₂) x : M₂)
      ((f : (a : M₃) → M₂) x : M₂)
⊢ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ f = f

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₂] M₂
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
x : M₃
⊢ Eq.{u_9 + 1} (α := M₂) (((↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ f : (a : M₃) → M₂) x : M₂)
    ((f : (a : M₃) → M₂) x : M₂)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₁] M₁
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
h :
  ∀ (x : M₃),
    Eq.{u_8 + 1} (α := M₁) (((↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f : (a : M₃) → M₁) x : M₁)
      ((f : (a : M₃) → M₁) x : M₁)
⊢ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = f

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₁] M₁
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
x : M₃
⊢ Eq.{u_8 + 1} (α := M₁) (((↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f : (a : M₃) → M₁) x : M₁)
    ((f : (a : M₃) → M₁) x : M₁)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst_6 : RingHomInvPair σ₁₃ σ₃₁
inst_7 : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃
⊢ Eq (α := M₃ ≃ₛₗ[σ₃₁] M₁) (symm (e₁₂.trans e₂₃)) (e₂₃.symm.trans e₁₂.symm)

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearEquiv.trans, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst_6 : RingHomInvPair σ₁₃ σ₃₁
inst_7 : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃
c : M₃
⊢ Eq.{u_8 + 1} (α := M₁) ((symm (e₁₂.trans e₂₃) : (a : M₃) → M₁) c : M₁)
    ((e₁₂.symm : (a : M₂) → M₁) ((e₂₃.symm : (a : M₃) → M₂) c : M₂) : M₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
⊢ e.trans (refl S M₂) = e

Tactic:
toEquiv_injective e.toEquiv.trans_refl

Premises used: Equiv.trans_refl, LinearEquiv.toEquiv_injective, LinearEquiv.toEquiv
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
⊢ trans (refl R M) e = e

Tactic:
toEquiv_injective e.toEquiv.refl_trans

Premises used: LinearEquiv.toEquiv_injective, LinearEquiv.toEquiv, Equiv.refl_trans
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
x : M₂
y : M
⊢ (e.symm : (a : M₂) → M) x = y ↔ x = (e : (a : M) → M₂) y

Tactic:
e.toEquiv.symm_apply_eq

Premises used: Equiv.symm_apply_eq, LinearEquiv.toEquiv
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
x : M₂
y : M
⊢ y = (e.symm : (a : M₂) → M) x ↔ (e : (a : M) → M₂) y = x

Tactic:
e.toEquiv.eq_symm_apply

Premises used: LinearEquiv.toEquiv, Equiv.eq_symm_apply
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_8
M₂ : Type u_9
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
α : Type u_14
f : M₂ → α
g : M₁ → α
⊢ f = g ∘ (⇑e₁₂.symm : (a : M₂) → M₁) ↔ f ∘ (⇑e₁₂ : (a : M₁) → M₂) = g

Tactic:
e₁₂.toEquiv.eq_comp_symm f g

Premises used: Equiv.eq_comp_symm, LinearEquiv.toEquiv
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_8
M₂ : Type u_9
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
α : Type u_14
f : M₂ → α
g : M₁ → α
⊢ g ∘ (⇑e₁₂.symm : (a : M₂) → M₁) = f ↔ g = f ∘ (⇑e₁₂ : (a : M₁) → M₂)

Tactic:
e₁₂.toEquiv.comp_symm_eq f g

Premises used: LinearEquiv.toEquiv, Equiv.comp_symm_eq
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_8
M₂ : Type u_9
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
α : Type u_14
f : α → M₁
g : α → M₂
⊢ f = (⇑e₁₂.symm : (a : M₂) → M₁) ∘ g ↔ (⇑e₁₂ : (a : M₁) → M₂) ∘ f = g

Tactic:
e₁₂.toEquiv.eq_symm_comp f g

Premises used: Equiv.eq_symm_comp, LinearEquiv.toEquiv
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_8
M₂ : Type u_9
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
α : Type u_14
f : α → M₁
g : α → M₂
⊢ (⇑e₁₂.symm : (a : M₂) → M₁) ∘ g = f ↔ g = (⇑e₁₂ : (a : M₁) → M₂) ∘ f

Tactic:
e₁₂.toEquiv.symm_comp_eq f g

Premises used: Equiv.symm_comp_eq, LinearEquiv.toEquiv
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst_6 : RingHomInvPair σ₁₃ σ₃₁
inst_7 : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
f : M₁ ≃ₛₗ[σ₁₂] M₂
f' : M₂ ≃ₛₗ[σ₂₃] M₃
⊢ (↑f' : M₂ →ₛₗ[σ₂₃] M₃) ∘ₛₗ (↑f : M₁ →ₛₗ[σ₁₂] M₂) = (↑(f.trans f') : M₁ →ₛₗ[σ₁₃] M₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
R₄ : Type u_5
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
M₄ : Type u_11
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring R₄
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₃
inst_7 : AddCommMonoid M₄
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
module_M₄ : Module R₄ M₄
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst_8 : RingHomInvPair σ₁₃ σ₃₁
inst_9 : RingHomInvPair σ₃₁ σ₁₃
σ₁₄ : R₁ →+* R₄
σ₄₁ : R₄ →+* R₁
inst_10 : RingHomInvPair σ₁₄ σ₄₁
inst_11 : RingHomInvPair σ₄₁ σ₁₄
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
inst_12 : RingHomInvPair σ₂₄ σ₄₂
inst_13 : RingHomInvPair σ₄₂ σ₂₄
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst_14 : RingHomInvPair σ₃₄ σ₄₃
inst_15 : RingHomInvPair σ₄₃ σ₃₄
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst_16 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_17 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_18 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst_19 : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst_20 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_21 : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst_22 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_23 : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃
e₃₄ : M₃ ≃ₛₗ[σ₃₄] M₄
⊢ Eq (α := M₁ ≃ₛₗ[σ₁₄] M₄) (trans (re₁₂ := inst_8) (re₂₁ := inst_9) (e₁₂.trans e₂₃) e₃₄)
    (e₁₂.trans (re₂₃ := inst_12) (re₃₂ := inst_13) (e₂₃.trans e₃₄))

Tactic:
rfl

Premises used: LinearEquiv.toEquiv, LinearEquiv.trans, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
mp : f = g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) → f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g
mpr : f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g → f = g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁)
⊢ f = g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ↔ f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : f = g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁)
mp :
  ∀ (x : M₁),
    Eq.{u_10 + 1} (α := M₃) ((f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₃) x : M₃) ((g : (a : M₁) → M₃) x : M₃)
⊢ f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g
mpr :
  ∀ (x : M₂),
    Eq.{u_10 + 1} (α := M₃) ((f : (a : M₂) → M₃) x : M₃) ((g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) : (a : M₂) → M₃) x : M₃)
⊢ f = g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁)

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : f = g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁)
x : M₁
⊢ Eq.{u_10 + 1} (α := M₃) ((f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₃) x : M₃) ((g : (a : M₁) → M₃) x : M₃)

Tactic:
simp [H]
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g
x : M₂
⊢ Eq.{u_10 + 1} (α := M₃) ((f : (a : M₂) → M₃) x : M₃) ((g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) : (a : M₂) → M₃) x : M₃)

Tactic:
simp [← H]
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
mp : g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) = f → g = f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)
mpr : g = f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) → g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) = f
⊢ g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) = f ↔ g = f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) = f
mp :
  ∀ (x : M₁),
    Eq.{u_10 + 1} (α := M₃) ((g : (a : M₁) → M₃) x : M₃) ((f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₃) x : M₃)
⊢ g = f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : g = f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)
mpr :
  ∀ (x : M₂),
    Eq.{u_10 + 1} (α := M₃) ((g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) : (a : M₂) → M₃) x : M₃) ((f : (a : M₂) → M₃) x : M₃)
⊢ g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) = f

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) = f
x : M₁
⊢ Eq.{u_10 + 1} (α := M₃) ((g : (a : M₁) → M₃) x : M₃) ((f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₃) x : M₃)

Tactic:
simp [← H]
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : g = f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)
x : M₂
⊢ Eq.{u_10 + 1} (α := M₃) ((g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) : (a : M₂) → M₃) x : M₃) ((f : (a : M₂) → M₃) x : M₃)

Tactic:
simp [H]
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
mp : f = (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g → (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = g
mpr : (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = g → f = (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g
⊢ f = (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g ↔ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = g

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
H : f = (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g
mp :
  ∀ (x : M₃),
    Eq.{u_9 + 1} (α := M₂) (((↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f : (a : M₃) → M₂) x : M₂) ((g : (a : M₃) → M₂) x : M₂)
⊢ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = g

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
H : (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = g
mpr :
  ∀ (x : M₃),
    Eq.{u_8 + 1} (α := M₁) ((f : (a : M₃) → M₁) x : M₁) (((↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g : (a : M₃) → M₁) x : M₁)
⊢ f = (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g

Tactic:
ext