case h
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type ?u.1589189
inst✝²⁴ : Semiring R₁
inst✝²³ : Semiring R₂
inst✝²² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝²¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁰ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝¹⁹ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹⁸ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝¹⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁴ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_3
inst✝¹³ : TopologicalSpace M₁
inst✝¹² : AddCommMonoid M₁
M'₁ : Type ?u.1590043
inst✝¹¹ : TopologicalSpace M'₁
inst✝¹⁰ : AddCommMonoid M'₁
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
M₃ : Type ?u.1590061
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
M₄ : Type ?u.1590070
inst✝⁵ : TopologicalSpace M₄
inst✝⁴ : AddCommMonoid M₄
inst✝³ : Module R₁ M₁
inst✝² : Module R₁ M'₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
e : M₁ ≃SL[σ₁₂] M₂
x : M₂
⊢ (↑e ∘ ↑(ContinuousLinearEquiv.symm e)) x = id x
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type ?u.1589189
inst✝²⁴ : Semiring R₁
inst✝²³ : Semiring R₂
inst✝²² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝²¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁰ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝¹⁹ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹⁸ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝¹⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁴ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_3
inst✝¹³ : TopologicalSpace M₁
inst✝¹² : AddCommMonoid M₁
M'₁ : Type ?u.1590043
inst✝¹¹ : TopologicalSpace M'₁
inst✝¹⁰ : AddCommMonoid M'₁
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
M₃ : Type ?u.1590061
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
M₄ : Type ?u.1590070
inst✝⁵ : TopologicalSpace M₄
inst✝⁴ : AddCommMonoid M₄
inst✝³ : Module R₁ M₁
inst✝² : Module R₁ M'₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
e : M₁ ≃SL[σ₁₂] M₂
⊢ ↑e ∘ ↑(ContinuousLinearEquiv.symm e) = id
ext x
no goals
case h
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type ?u.1589189
inst✝²⁴ : Semiring R₁
inst✝²³ : Semiring R₂
inst✝²² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝²¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁰ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝¹⁹ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹⁸ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝¹⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁴ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_3
inst✝¹³ : TopologicalSpace M₁
inst✝¹² : AddCommMonoid M₁
M'₁ : Type ?u.1590043
inst✝¹¹ : TopologicalSpace M'₁
inst✝¹⁰ : AddCommMonoid M'₁
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
M₃ : Type ?u.1590061
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
M₄ : Type ?u.1590070
inst✝⁵ : TopologicalSpace M₄
inst✝⁴ : AddCommMonoid M₄
inst✝³ : Module R₁ M₁
inst✝² : Module R₁ M'₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
e : M₁ ≃SL[σ₁₂] M₂
x : M₂
⊢ (↑e ∘ ↑(ContinuousLinearEquiv.symm e)) x = id x
exact apply_symm_apply e x