case pos
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : ∃ e', ↑e' = f
⊢ inverse f = comp (Ring.inverse (comp (↑(ContinuousLinearEquiv.symm e)) f)) ↑(ContinuousLinearEquiv.symm e)

case neg
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : ¬∃ e', ↑e' = f
⊢ inverse f = comp (Ring.inverse (comp (↑(ContinuousLinearEquiv.symm e)) f)) ↑(ContinuousLinearEquiv.symm e)
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
⊢ inverse f = comp (Ring.inverse (comp (↑(ContinuousLinearEquiv.symm e)) f)) ↑(ContinuousLinearEquiv.symm e)
by_cases h₁ : ∃ e' : M ≃L[R] M₂, e' = f
case pos.intro
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
⊢ inverse f = comp (Ring.inverse (comp (↑(ContinuousLinearEquiv.symm e)) f)) ↑(ContinuousLinearEquiv.symm e)
case pos
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : ∃ e', ↑e' = f
⊢ inverse f = comp (Ring.inverse (comp (↑(ContinuousLinearEquiv.symm e)) f)) ↑(ContinuousLinearEquiv.symm e)
obtain ⟨e', he'⟩ := h₁
case pos.intro
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
⊢ inverse ↑e' = comp (Ring.inverse (comp ↑(ContinuousLinearEquiv.symm e) ↑e')) ↑(ContinuousLinearEquiv.symm e)
case pos.intro
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
⊢ inverse f = comp (Ring.inverse (comp (↑(ContinuousLinearEquiv.symm e)) f)) ↑(ContinuousLinearEquiv.symm e)
rw [← he']
case pos.intro
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
⊢ inverse ↑e' =
    comp (Ring.inverse ↑(ContinuousLinearEquiv.trans e' (ContinuousLinearEquiv.symm e))) ↑(ContinuousLinearEquiv.symm e)
case pos.intro
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
⊢ inverse ↑e' = comp (Ring.inverse (comp ↑(ContinuousLinearEquiv.symm e) ↑e')) ↑(ContinuousLinearEquiv.symm e)
change _ = Ring.inverse (e'.trans e.symm : M →L[R] M) ∘L (e.symm : M₂ →L[R] M)
case pos.intro.h
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
x✝ : M₂
⊢ ↑(inverse ↑e') x✝ =
    ↑(comp (Ring.inverse ↑(ContinuousLinearEquiv.trans e' (ContinuousLinearEquiv.symm e)))
          ↑(ContinuousLinearEquiv.symm e))
      x✝
case pos.intro
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
⊢ inverse ↑e' =
    comp (Ring.inverse ↑(ContinuousLinearEquiv.trans e' (ContinuousLinearEquiv.symm e))) ↑(ContinuousLinearEquiv.symm e)
ext
no goals
case pos.intro.h
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
x✝ : M₂
⊢ ↑(inverse ↑e') x✝ =
    ↑(comp (Ring.inverse ↑(ContinuousLinearEquiv.trans e' (ContinuousLinearEquiv.symm e)))
          ↑(ContinuousLinearEquiv.symm e))
      x✝
simp
case neg
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : ¬∃ e', ↑e' = f
⊢ ¬IsUnit (comp (↑(ContinuousLinearEquiv.symm e)) f)
case neg
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : ¬∃ e', ↑e' = f
⊢ inverse f = comp (Ring.inverse (comp (↑(ContinuousLinearEquiv.symm e)) f)) ↑(ContinuousLinearEquiv.symm e)
suffices ¬IsUnit ((e.symm : M₂ →L[R] M).comp f) by simp [this, h₁]
case neg
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : IsUnit (comp (↑(ContinuousLinearEquiv.symm e)) f)
⊢ ∃ e', ↑e' = f
case neg
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : ¬∃ e', ↑e' = f
⊢ ¬IsUnit (comp (↑(ContinuousLinearEquiv.symm e)) f)
contrapose! h₁
case neg.intro
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = comp (↑(ContinuousLinearEquiv.symm e)) f
⊢ ∃ e', ↑e' = f
case neg
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : IsUnit (comp (↑(ContinuousLinearEquiv.symm e)) f)
⊢ ∃ e', ↑e' = f
rcases h₁ with ⟨F, hF⟩
case neg.intro
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = comp (↑(ContinuousLinearEquiv.symm e)) f
⊢ ↑(ContinuousLinearEquiv.trans (↑(ContinuousLinearEquiv.unitsEquiv R M) F) e) = f
case neg.intro
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = comp (↑(ContinuousLinearEquiv.symm e)) f
⊢ ∃ e', ↑e' = f
use (ContinuousLinearEquiv.unitsEquiv _ _ F).trans e
case neg.intro.h
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = comp (↑(ContinuousLinearEquiv.symm e)) f
x✝ : M
⊢ ↑↑(ContinuousLinearEquiv.trans (↑(ContinuousLinearEquiv.unitsEquiv R M) F) e) x✝ = ↑f x✝
case neg.intro
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = comp (↑(ContinuousLinearEquiv.symm e)) f
⊢ ↑(ContinuousLinearEquiv.trans (↑(ContinuousLinearEquiv.unitsEquiv R M) F) e) = f
ext
case neg.intro.h
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = comp (↑(ContinuousLinearEquiv.symm e)) f
x✝ : M
⊢ ↑e (↑↑F x✝) = ↑f x✝
case neg.intro.h
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = comp (↑(ContinuousLinearEquiv.symm e)) f
x✝ : M
⊢ ↑↑(ContinuousLinearEquiv.trans (↑(ContinuousLinearEquiv.unitsEquiv R M) F) e) x✝ = ↑f x✝
dsimp
case neg.intro.h
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = comp (↑(ContinuousLinearEquiv.symm e)) f
x✝ : M
⊢ ↑e (↑(comp (↑(ContinuousLinearEquiv.symm e)) f) x✝) = ↑f x✝
case neg.intro.h
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = comp (↑(ContinuousLinearEquiv.symm e)) f
x✝ : M
⊢ ↑e (↑↑F x✝) = ↑f x✝
rw [hF]
no goals
case neg.intro.h
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = comp (↑(ContinuousLinearEquiv.symm e)) f
x✝ : M
⊢ ↑e (↑(comp (↑(ContinuousLinearEquiv.symm e)) f) x✝) = ↑f x✝
simp
no goals
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : ¬∃ e', ↑e' = f
this : ¬IsUnit (comp (↑(ContinuousLinearEquiv.symm e)) f)
⊢ inverse f = comp (Ring.inverse (comp (↑(ContinuousLinearEquiv.symm e)) f)) ↑(ContinuousLinearEquiv.symm e)
simp [this, h₁]