awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : M₃
⊢ Eq.{u_9 + 1} (α := M₂) (((↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f : (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 : (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = g
x : M₃
⊢ Eq.{u_8 + 1} (α := M₁) ((f : (a : M₃) → M₁) x : M₁) (((↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] 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₂
mp : (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g = f → g = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f
mpr : g = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f → (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g = f
⊢ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g = f ↔ g = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f

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 : (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g = f
mp :
  ∀ (x : M₃),
    Eq.{u_9 + 1} (α := M₂) ((g : (a : M₃) → M₂) x : M₂) (((↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f : (a : M₃) → M₂) x : M₂)
⊢ g = (↑e₁₂ : 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₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f
mpr :
  ∀ (x : M₃),
    Eq.{u_8 + 1} (α := M₁) (((↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g : (a : M₃) → M₁) x : M₁) ((f : (a : M₃) → M₁) x : M₁)
⊢ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g = 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 : (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g = f
x : M₃
⊢ Eq.{u_9 + 1} (α := M₂) ((g : (a : M₃) → M₂) x : M₂) (((↑e₁₂ : M₁ →ₛₗ[σ₁₂] 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₂
H : g = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f
x : M₃
⊢ Eq.{u_8 + 1} (α := M₁) (((↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ g : (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 g : M₃ →ₛₗ[σ₃₁] M₁
⊢ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ g ↔ f = g

Tactic:
⟨fun h => ?_, congrArg e₁₂.comp⟩

Premises used: congrArg, LinearMap.comp, LinearEquiv.toLinearMap, Iff.intro
-- 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 g : M₃ →ₛₗ[σ₃₁] M₁
refine : ∀ (h : (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ g), f = g
⊢ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ g ↔ f = g

Tactic:
refine ⟨fun h => ?_, congrArg e₁₂.comp⟩
-- 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 g : M₃ →ₛₗ[σ₃₁] M₁
h : (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ g
rw : f = (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f
rw₁ rw₂ : (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f
⊢ f = g

Tactic:
rw [← (toLinearMap_symm_comp_eq g (e₁₂.toLinearMap.comp f)).mpr h, eq_toLinearMap_symm_comp]

Premises used: Iff.mpr, LinearEquiv.eq_toLinearMap_symm_comp, LinearEquiv.toLinearMap_symm_comp_eq, LinearMap.comp, LinearEquiv.toLinearMap
-- 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 g : M₂ →ₛₗ[σ₂₃] M₃
⊢ f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ↔ f = g

Tactic:
⟨fun h => ?_, fun a ↦ congrFun (congrArg LinearMap.comp a) e₁₂.toLinearMap⟩

Premises used: congrArg, LinearMap.comp, LinearEquiv.toLinearMap, congrFun, Iff.intro
-- 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 g : M₂ →ₛₗ[σ₂₃] M₃
refine : ∀ (h : f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)), f = g
⊢ f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ↔ f = g

Tactic:
refine ⟨fun h => ?_, fun a ↦ congrFun (congrArg LinearMap.comp a) e₁₂.toLinearMap⟩
-- 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 g : M₂ →ₛₗ[σ₂₃] M₃
h : f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)
rw : f = (f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)) ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁)
rw₁ rw₂ : f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)
⊢ f = g

Tactic:
rw [(eq_comp_toLinearMap_symm g (f.comp e₁₂.toLinearMap)).mpr h.symm, eq_comp_toLinearMap_symm]

Premises used: Iff.mpr, LinearEquiv.eq_comp_toLinearMap_symm, LinearMap.comp, LinearEquiv.toLinearMap, Eq.symm
-- 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 σ₃₂ σ₂₁ σ₃₁
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₂] M₂
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 σ₃₂ σ₂₁ σ₃₁
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₂] M₂
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 σ₃₂ σ₂₁ σ₃₁
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₁] M₁
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 σ₃₂ σ₂₁ σ₃₁
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₁] M₁
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₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₂ →ₛₗ[σ₂₃] M₃
h :
  ∀ (x : M₂),
    Eq.{u_10 + 1} (α := M₃) (((f ∘ₛₗ (↑e : M₁ →ₛₗ[σ₁₂] M₂)) ∘ₛₗ (↑e.symm : M₂ →ₛₗ[σ₂₁] M₁) : (a : M₂) → M₃) x : M₃)
      ((f : (a : M₂) → M₃) x : M₃)
⊢ (f ∘ₛₗ (↑e : M₁ →ₛₗ[σ₁₂] M₂)) ∘ₛₗ (↑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 σ₁₂ σ₂₃ σ₁₃
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₂ →ₛₗ[σ₂₃] M₃
x : M₂
⊢ Eq.{u_10 + 1} (α := M₃) (((f ∘ₛₗ (↑e : M₁ →ₛₗ[σ₁₂] M₂)) ∘ₛₗ (↑e.symm : M₂ →ₛₗ[σ₂₁] M₁) : (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 σ₁₂ σ₂₃ σ₁₃
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₁ →ₛₗ[σ₁₃] M₃
h :
  ∀ (x : M₁),
    Eq.{u_10 + 1} (α := M₃) (((f ∘ₛₗ (↑e.symm : M₂ →ₛₗ[σ₂₁] M₁)) ∘ₛₗ (↑e : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₃) x : M₃)
      ((f : (a : M₁) → M₃) x : M₃)
⊢ (f ∘ₛₗ (↑e.symm : M₂ →ₛₗ[σ₂₁] M₁)) ∘ₛₗ (↑e : 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 σ₁₂ σ₂₃ σ₁₃
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₁ →ₛₗ[σ₁₃] M₃
x : M₁
⊢ Eq.{u_10 + 1} (α := M₃) (((f ∘ₛₗ (↑e.symm : M₂ →ₛₗ[σ₂₁] M₁)) ∘ₛₗ (↑e : M₁ →ₛₗ[σ₁₂] M₂) : (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 σ₃₂ σ₂₁ σ₃₁
inst_10 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst_11 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₁ ≃ₛₗ[σ₁₃] M₃
h :
  ∀ (x : M₁),
    Eq.{u_10 + 1} (α := M₃) ((e.trans (re₂₃ := re₂₃) (re₃₂ := re₃₂) (e.symm.trans f) : (a : M₁) → M₃) x : M₃)
      ((f : (a : M₁) → M₃) x : M₃)
⊢ e.trans (re₂₃ := re₂₃) (re₃₂ := re₃₂) (e.symm.trans 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₁
inst_6 : RingHomInvPair σ₁₃ σ₃₁
inst_7 : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_10 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst_11 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₁ ≃ₛₗ[σ₁₃] M₃
x : M₁
⊢ Eq.{u_10 + 1} (α := M₃) ((e.trans (re₂₃ := re₂₃) (re₃₂ := re₃₂) (e.symm.trans 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 σ₃₂ σ₂₁ σ₃₁
inst_10 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst_11 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₂ ≃ₛₗ[σ₂₃] M₃
h :
  ∀ (x : M₂),
    Eq.{u_10 + 1} (α := M₃) ((e.symm.trans (re₂₃ := inst_6) (re₃₂ := inst_7) (e.trans f) : (a : M₂) → M₃) x : M₃)
      ((f : (a : M₂) → M₃) x : M₃)
⊢ e.symm.trans (re₂₃ := inst_6) (re₃₂ := inst_7) (e.trans 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₁
inst_6 : RingHomInvPair σ₁₃ σ₃₁
inst_7 : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_10 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst_11 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₂ ≃ₛₗ[σ₂₃] M₃
x : M₂
⊢ Eq.{u_10 + 1} (α := M₃) ((e.symm.trans (re₂₃ := inst_6) (re₃₂ := inst_7) (e.trans 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 σ₃₂ σ₂₁ σ₃₁
inst_10 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst_11 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ ≃ₛₗ[σ₃₁] M₁
h :
  ∀ (x : M₃),
    Eq.{u_8 + 1} (α := M₁) ((trans (re₁₂ := re₃₂) (re₂₁ := re₂₃) (f.trans e) e.symm : (a : M₃) → M₁) x : M₁)
      ((f : (a : M₃) → M₁) x : M₁)
⊢ trans (re₁₂ := re₃₂) (re₂₁ := re₂₃) (f.trans e) e.symm = 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₁
inst_6 : RingHomInvPair σ₁₃ σ₃₁
inst_7 : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_10 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst_11 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ ≃ₛₗ[σ₃₁] M₁
x : M₃
⊢ Eq.{u_8 + 1} (α := M₁) ((trans (re₁₂ := re₃₂) (re₂₁ := re₂₃) (f.trans e) e.symm : (a : M₃) → M₁) x : M₁)
    ((f : (a : M₃) → M₁) x : M₁)

Tactic:
simp