Theorem: bijective_iff_inverses' (Sard/ManifoldAux.lean)

State before:
E : Type u_1
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace ℝ E
H : Type u_2
inst✝¹³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹² : TopologicalSpace M
inst✝¹¹ : ChartedSpace H M
inst✝¹⁰ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : SmoothManifoldWithCorners J N
X : Type u_7
Y : Type u_8
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f : X →L[ℝ] Y
g : Y →L[ℝ] X
h1 : g.comp f = ContinuousLinearMap.id ℝ X
h2 : f.comp g = ContinuousLinearMap.id ℝ Y
⊢ Bijective ⇑f
Tactic:
have h : f.toFun ∘ g.toFun = id := calc f.toFun ∘ g.toFun
  _ = (f.comp g).toFun := rfl
  _ = (ContinuousLinearMap.id ℝ Y).toFun := by rw [h2]
  _ = id := rfl
State after:
E : Type u_1
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace ℝ E
H : Type u_2
inst✝¹³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹² : TopologicalSpace M
inst✝¹¹ : ChartedSpace H M
inst✝¹⁰ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : SmoothManifoldWithCorners J N
X : Type u_7
Y : Type u_8
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f : X →L[ℝ] Y
g : Y →L[ℝ] X
h1 : g.comp f = ContinuousLinearMap.id ℝ X
h2 : f.comp g = ContinuousLinearMap.id ℝ Y
h : f.toFun ∘ g.toFun = id
⊢ Bijective ⇑f

State before:
E : Type u_1
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace ℝ E
H : Type u_2
inst✝¹³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹² : TopologicalSpace M
inst✝¹¹ : ChartedSpace H M
inst✝¹⁰ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : SmoothManifoldWithCorners J N
X : Type u_7
Y : Type u_8
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f : X →L[ℝ] Y
g : Y →L[ℝ] X
h1 : g.comp f = ContinuousLinearMap.id ℝ X
h2 : f.comp g = ContinuousLinearMap.id ℝ Y
h : f.toFun ∘ g.toFun = id
⊢ Bijective ⇑f
Tactic:
have : g.toFun ∘ f.toFun = id := by calc g.toFun ∘ f.toFun
  _ = (g.comp f).toFun := rfl
  _ = (ContinuousLinearMap.id ℝ X).toFun := by rw [h1]
  _ = id := rfl
State after:
E : Type u_1
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace ℝ E
H : Type u_2
inst✝¹³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹² : TopologicalSpace M
inst✝¹¹ : ChartedSpace H M
inst✝¹⁰ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : SmoothManifoldWithCorners J N
X : Type u_7
Y : Type u_8
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f : X →L[ℝ] Y
g : Y →L[ℝ] X
h1 : g.comp f = ContinuousLinearMap.id ℝ X
h2 : f.comp g = ContinuousLinearMap.id ℝ Y
h : f.toFun ∘ g.toFun = id
this : g.toFun ∘ f.toFun = id
⊢ Bijective ⇑f

State before:
E : Type u_1
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace ℝ E
H : Type u_2
inst✝¹³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹² : TopologicalSpace M
inst✝¹¹ : ChartedSpace H M
inst✝¹⁰ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : SmoothManifoldWithCorners J N
X : Type u_7
Y : Type u_8
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f : X →L[ℝ] Y
g : Y →L[ℝ] X
h1 : g.comp f = ContinuousLinearMap.id ℝ X
h2 : f.comp g = ContinuousLinearMap.id ℝ Y
h : f.toFun ∘ g.toFun = id
this : g.toFun ∘ f.toFun = id
⊢ Bijective ⇑f
Tactic:
exact bijective_iff_inverses this h
State after:
no goals

State before:
E : Type u_1
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace ℝ E
H : Type u_2
inst✝¹³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹² : TopologicalSpace M
inst✝¹¹ : ChartedSpace H M
inst✝¹⁰ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : SmoothManifoldWithCorners J N
X : Type u_7
Y : Type u_8
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f : X →L[ℝ] Y
g : Y →L[ℝ] X
h1 : g.comp f = ContinuousLinearMap.id ℝ X
h2 : f.comp g = ContinuousLinearMap.id ℝ Y
⊢ (f.comp g).toFun = (ContinuousLinearMap.id ℝ Y).toFun
Tactic:
rw [h2]
State after:
no goals

State before:
E : Type u_1
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace ℝ E
H : Type u_2
inst✝¹³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹² : TopologicalSpace M
inst✝¹¹ : ChartedSpace H M
inst✝¹⁰ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : SmoothManifoldWithCorners J N
X : Type u_7
Y : Type u_8
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f : X →L[ℝ] Y
g : Y →L[ℝ] X
h1 : g.comp f = ContinuousLinearMap.id ℝ X
h2 : f.comp g = ContinuousLinearMap.id ℝ Y
h : f.toFun ∘ g.toFun = id
⊢ g.toFun ∘ f.toFun = id
Tactic:
calc g.toFun ∘ f.toFun
_ = (g.comp f).toFun := rfl
_ = (ContinuousLinearMap.id ℝ X).toFun := by rw [h1]
_ = id := rfl
State after:
no goals

State before:
E : Type u_1
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace ℝ E
H : Type u_2
inst✝¹³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹² : TopologicalSpace M
inst✝¹¹ : ChartedSpace H M
inst✝¹⁰ : SmoothManifoldWithCorners I M
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : SmoothManifoldWithCorners J N
X : Type u_7
Y : Type u_8
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f : X →L[ℝ] Y
g : Y →L[ℝ] X
h1 : g.comp f = ContinuousLinearMap.id ℝ X
h2 : f.comp g = ContinuousLinearMap.id ℝ Y
h : f.toFun ∘ g.toFun = id
⊢ (g.comp f).toFun = (ContinuousLinearMap.id ℝ X).toFun
Tactic:
rw [h1]
State after:
no goals