-- Mathlib/Analysis/Normed/Affine/Isometry.lean
theorem AffineMap.isOpenMap_linear_iff {f : P →ᵃ[𝕜] P₂} : IsOpenMap f.linear ↔ IsOpenMap f

Proof state:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
this :
  ⇑f.linear =
    ⇑(AffineIsometryEquiv.vaddConst 𝕜 (f default)).toHomeomorph.symm ∘
      ⇑f ∘ ⇑(AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph
⊢ IsOpenMap
      (⇑(AffineIsometryEquiv.vaddConst 𝕜 (f default)).toHomeomorph.symm ∘
        ⇑f ∘ ⇑(AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph) ↔
    IsOpenMap ⇑f

Tactic:
simp only [Homeomorph.comp_isOpenMap_iff, Homeomorph.comp_isOpenMap_iff']

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃ[𝕜] P₂
⊢ IsOpenMap ⇑f.linear ↔ IsOpenMap ⇑f

Tactic:
inhabit P

Result:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
⊢ IsOpenMap ⇑f.linear ↔ IsOpenMap ⇑f

Proof state:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
⊢ ⇑f.linear =
    ⇑(AffineIsometryEquiv.vaddConst 𝕜 (f default)).toHomeomorph.symm ∘
      ⇑f ∘ ⇑(AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph

Tactic:
ext v

Result:
case h
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
v : V
⊢ f.linear v =
    (⇑(AffineIsometryEquiv.vaddConst 𝕜 (f default)).toHomeomorph.symm ∘
        ⇑f ∘ ⇑(AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph)
      v

Proof state:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
⊢ IsOpenMap ⇑f.linear ↔ IsOpenMap ⇑f

Tactic:
have :
  (f.linear : V → V₂) =
    (AffineIsometryEquiv.vaddConst 𝕜 <| f default).toHomeomorph.symm ∘
      f ∘ (AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph := by
  ext v
  simp

Result:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
this :
  ⇑f.linear =
    ⇑(AffineIsometryEquiv.vaddConst 𝕜 (f default)).toHomeomorph.symm ∘
      ⇑f ∘ ⇑(AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph
⊢ IsOpenMap ⇑f.linear ↔ IsOpenMap ⇑f

Proof state:
case h
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
v : V
⊢ f.linear v =
    (⇑(AffineIsometryEquiv.vaddConst 𝕜 (f default)).toHomeomorph.symm ∘
        ⇑f ∘ ⇑(AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph)
      v

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
this :
  ⇑f.linear =
    ⇑(AffineIsometryEquiv.vaddConst 𝕜 (f default)).toHomeomorph.symm ∘
      ⇑f ∘ ⇑(AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph
⊢ IsOpenMap ⇑f.linear ↔ IsOpenMap ⇑f

Tactic:
rw [this]

Result:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
this :
  ⇑f.linear =
    ⇑(AffineIsometryEquiv.vaddConst 𝕜 (f default)).toHomeomorph.symm ∘
      ⇑f ∘ ⇑(AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph
⊢ IsOpenMap
      (⇑(AffineIsometryEquiv.vaddConst 𝕜 (f default)).toHomeomorph.symm ∘
        ⇑f ∘ ⇑(AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph) ↔
    IsOpenMap ⇑f