[GOAL]
α : Type ?u.597
V : Type ?u.600
P : Type ?u.603
W : Type u_2
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
s : AffineSubspace 𝕜 Q
⊢ IsClosed ↑(direction s) ↔ IsClosed ↑s
[PROOFSTEP]
rcases s.eq_bot_or_nonempty with (rfl | ⟨x, hx⟩)
[GOAL]
case inl
α : Type ?u.597
V : Type ?u.600
P : Type ?u.603
W : Type u_2
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
⊢ IsClosed ↑(direction ⊥) ↔ IsClosed ↑⊥
[PROOFSTEP]
simp [isClosed_singleton]
[GOAL]
case inr.intro
α : Type ?u.597
V : Type ?u.600
P : Type ?u.603
W : Type u_2
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
s : AffineSubspace 𝕜 Q
x : Q
hx : x ∈ ↑s
⊢ IsClosed ↑(direction s) ↔ IsClosed ↑s
[PROOFSTEP]
rw [← (IsometryEquiv.vaddConst x).toHomeomorph.symm.isClosed_image, AffineSubspace.coe_direction_eq_vsub_set_right hx]
[GOAL]
case inr.intro
α : Type ?u.597
V : Type ?u.600
P : Type ?u.603
W : Type u_2
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
s : AffineSubspace 𝕜 Q
x : Q
hx : x ∈ ↑s
⊢ IsClosed ((fun x_1 => x_1 -ᵥ x) '' ↑s) ↔
    IsClosed (↑(Homeomorph.symm (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst x))) '' ↑s)
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.5475
V : Type u_2
P : Type u_1
W : Type ?u.5484
Q : Type ?u.5487
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
p₁ p₂ : P
c : 𝕜
⊢ dist p₁ (↑(homothety p₁ c) p₂) = ‖c‖ * dist p₁ p₂
[PROOFSTEP]
rw [homothety_def, dist_eq_norm_vsub V]
[GOAL]
α : Type ?u.5475
V : Type u_2
P : Type u_1
W : Type ?u.5484
Q : Type ?u.5487
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
p₁ p₂ : P
c : 𝕜
⊢ ‖p₁ -ᵥ ↑(c • (AffineMap.id 𝕜 P -ᵥ const 𝕜 P p₁) +ᵥ const 𝕜 P p₁) p₂‖ = ‖c‖ * dist p₁ p₂
[PROOFSTEP]
simp [norm_smul, ← dist_eq_norm_vsub V, dist_comm]
[GOAL]
α : Type ?u.14492
V : Type u_2
P : Type u_1
W : Type ?u.14501
Q : Type ?u.14504
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
p₁ p₂ : P
c : 𝕜
⊢ dist (↑(homothety p₁ c) p₂) p₁ = ‖c‖ * dist p₁ p₂
[PROOFSTEP]
rw [dist_comm, dist_center_homothety]
[GOAL]
α : Type ?u.16780
V : Type u_3
P : Type u_1
W : Type ?u.16789
Q : Type ?u.16792
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
p₁ p₂ : P
c₁ c₂ : 𝕜
⊢ dist (↑(lineMap p₁ p₂) c₁) (↑(lineMap p₁ p₂) c₂) = dist c₁ c₂ * dist p₁ p₂
[PROOFSTEP]
rw [dist_comm p₁ p₂]
  -- Porting note: was `simp only [lineMap_apply, dist_eq_norm_vsub, vadd_vsub_vadd_cancel_right,`
    -- `← sub_smul, norm_smul, vsub_eq_sub]`
[GOAL]
α : Type ?u.16780
V : Type u_3
P : Type u_1
W : Type ?u.16789
Q : Type ?u.16792
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
p₁ p₂ : P
c₁ c₂ : 𝕜
⊢ dist (↑(lineMap p₁ p₂) c₁) (↑(lineMap p₁ p₂) c₂) = dist c₁ c₂ * dist p₂ p₁
[PROOFSTEP]
rw [lineMap_apply, lineMap_apply, dist_eq_norm_vsub V, vadd_vsub_vadd_cancel_right, ← sub_smul, norm_smul, ←
  vsub_eq_sub, ← dist_eq_norm_vsub V, ← dist_eq_norm_vsub 𝕜]
[GOAL]
α : Type ?u.28725
V : Type u_3
P : Type u_1
W : Type ?u.28734
Q : Type ?u.28737
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
p₁ p₂ : P
c : 𝕜
⊢ dist (↑(lineMap p₁ p₂) c) p₁ = ‖c‖ * dist p₁ p₂
[PROOFSTEP]
rw [← dist_zero_right, ← dist_lineMap_lineMap, lineMap_apply_zero]
[GOAL]
α : Type ?u.37626
V : Type u_3
P : Type u_1
W : Type ?u.37635
Q : Type ?u.37638
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
p₁ p₂ : P
c : 𝕜
⊢ dist (↑(lineMap p₁ p₂) c) p₂ = ‖1 - c‖ * dist p₁ p₂
[PROOFSTEP]
rw [← dist_eq_norm', ← dist_lineMap_lineMap, lineMap_apply_one]
[GOAL]
α : Type ?u.47659
V : Type u_2
P : Type u_1
W : Type ?u.47668
Q : Type ?u.47671
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
p₁ p₂ : P
c : 𝕜
⊢ dist (↑(homothety p₁ c) p₂) p₂ = ‖1 - c‖ * dist p₁ p₂
[PROOFSTEP]
rw [homothety_eq_lineMap, dist_lineMap_right]
[GOAL]
α : Type ?u.51220
V : Type u_2
P : Type u_1
W : Type ?u.51229
Q : Type ?u.51232
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
p₁ p₂ : P
c : 𝕜
⊢ dist p₂ (↑(homothety p₁ c) p₂) = ‖1 - c‖ * dist p₁ p₂
[PROOFSTEP]
rw [dist_comm, dist_homothety_self]
[GOAL]
α : Type ?u.54860
V : Type u_2
P : Type u_1
W : Type ?u.54869
Q : Type ?u.54872
inst✝⁹ : SeminormedAddCommGroup V
inst✝⁸ : PseudoMetricSpace P
inst✝⁷ : NormedAddTorsor V P
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : MetricSpace Q
inst✝⁴ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : Invertible 2
p₁ p₂ : P
⊢ dist p₁ (midpoint 𝕜 p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂
[PROOFSTEP]
rw [midpoint, dist_comm, dist_lineMap_left, invOf_eq_inv, ← norm_inv]
[GOAL]
α : Type ?u.59357
V : Type u_2
P : Type u_1
W : Type ?u.59366
Q : Type ?u.59369
inst✝⁹ : SeminormedAddCommGroup V
inst✝⁸ : PseudoMetricSpace P
inst✝⁷ : NormedAddTorsor V P
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : MetricSpace Q
inst✝⁴ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : Invertible 2
p₁ p₂ : P
⊢ dist (midpoint 𝕜 p₁ p₂) p₁ = ‖2‖⁻¹ * dist p₁ p₂
[PROOFSTEP]
rw [dist_comm, dist_left_midpoint]
[GOAL]
α : Type ?u.63410
V : Type u_2
P : Type u_1
W : Type ?u.63419
Q : Type ?u.63422
inst✝⁹ : SeminormedAddCommGroup V
inst✝⁸ : PseudoMetricSpace P
inst✝⁷ : NormedAddTorsor V P
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : MetricSpace Q
inst✝⁴ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : Invertible 2
p₁ p₂ : P
⊢ dist (midpoint 𝕜 p₁ p₂) p₂ = ‖2‖⁻¹ * dist p₁ p₂
[PROOFSTEP]
rw [midpoint_comm, dist_midpoint_left, dist_comm]
[GOAL]
α : Type ?u.68130
V : Type u_2
P : Type u_1
W : Type ?u.68139
Q : Type ?u.68142
inst✝⁹ : SeminormedAddCommGroup V
inst✝⁸ : PseudoMetricSpace P
inst✝⁷ : NormedAddTorsor V P
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : MetricSpace Q
inst✝⁴ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : Invertible 2
p₁ p₂ : P
⊢ dist p₂ (midpoint 𝕜 p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂
[PROOFSTEP]
rw [dist_comm, dist_midpoint_right]
[GOAL]
α : Type ?u.72183
V : Type u_2
P : Type u_1
W : Type ?u.72192
Q : Type ?u.72195
inst✝⁹ : SeminormedAddCommGroup V
inst✝⁸ : PseudoMetricSpace P
inst✝⁷ : NormedAddTorsor V P
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : MetricSpace Q
inst✝⁴ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : Invertible 2
p₁ p₂ p₃ p₄ : P
⊢ dist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / ‖2‖
[PROOFSTEP]
rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, midpoint_vsub_midpoint]
[GOAL]
α : Type ?u.72183
V : Type u_2
P : Type u_1
W : Type ?u.72192
Q : Type ?u.72195
inst✝⁹ : SeminormedAddCommGroup V
inst✝⁸ : PseudoMetricSpace P
inst✝⁷ : NormedAddTorsor V P
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : MetricSpace Q
inst✝⁴ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : Invertible 2
p₁ p₂ p₃ p₄ : P
⊢ ‖midpoint 𝕜 (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / ‖2‖
[PROOFSTEP]
try infer_instance
[GOAL]
α : Type ?u.72183
V : Type u_2
P : Type u_1
W : Type ?u.72192
Q : Type ?u.72195
inst✝⁹ : SeminormedAddCommGroup V
inst✝⁸ : PseudoMetricSpace P
inst✝⁷ : NormedAddTorsor V P
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : MetricSpace Q
inst✝⁴ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : Invertible 2
p₁ p₂ p₃ p₄ : P
⊢ ‖midpoint 𝕜 (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / ‖2‖
[PROOFSTEP]
infer_instance
[GOAL]
α : Type ?u.72183
V : Type u_2
P : Type u_1
W : Type ?u.72192
Q : Type ?u.72195
inst✝⁹ : SeminormedAddCommGroup V
inst✝⁸ : PseudoMetricSpace P
inst✝⁷ : NormedAddTorsor V P
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : MetricSpace Q
inst✝⁴ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : Invertible 2
p₁ p₂ p₃ p₄ : P
⊢ ‖midpoint 𝕜 (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / ‖2‖
[PROOFSTEP]
rw [midpoint_eq_smul_add, norm_smul, invOf_eq_inv, norm_inv, ← div_eq_inv_mul]
[GOAL]
α : Type ?u.72183
V : Type u_2
P : Type u_1
W : Type ?u.72192
Q : Type ?u.72195
inst✝⁹ : SeminormedAddCommGroup V
inst✝⁸ : PseudoMetricSpace P
inst✝⁷ : NormedAddTorsor V P
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : MetricSpace Q
inst✝⁴ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : Invertible 2
p₁ p₂ p₃ p₄ : P
⊢ ‖p₁ -ᵥ p₃ + (p₂ -ᵥ p₄)‖ / ‖2‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / ‖2‖
[PROOFSTEP]
exact div_le_div_of_le_of_nonneg (norm_add_le _ _) (norm_nonneg _)
[GOAL]
α : Type ?u.79698
V : Type u_2
P : Type u_1
W : Type ?u.79707
Q : Type ?u.79710
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type ?u.79957
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
p q : P
⊢ dist (↑(Equiv.pointReflection p) q) p = dist p q
[PROOFSTEP]
simp [dist_eq_norm_vsub V, Equiv.pointReflection_vsub_left (G := V)]
[GOAL]
α : Type ?u.82730
V : Type u_2
P : Type u_1
W : Type ?u.82739
Q : Type ?u.82742
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
p q : P
⊢ dist (↑(Equiv.pointReflection p) q) q = ‖2‖ * dist p q
[PROOFSTEP]
simp [dist_eq_norm_vsub V, Equiv.pointReflection_vsub_right (G := V), nsmul_eq_smul_cast 𝕜, norm_smul]
[GOAL]
α : Type ?u.88928
V : Type ?u.88931
P : Type ?u.88934
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
p₁ p₂ : Q
h : p₁ ≠ p₂
c₁ c₂ : 𝕜
⊢ dist c₁ c₂ ≤ ↑(nndist p₁ p₂)⁻¹ * dist (↑(lineMap p₁ p₂) c₁) (↑(lineMap p₁ p₂) c₂)
[PROOFSTEP]
rw [dist_lineMap_lineMap, NNReal.coe_inv, ← dist_nndist, mul_left_comm, inv_mul_cancel (dist_ne_zero.2 h), mul_one]
[GOAL]
α : Type ?u.92785
V : Type ?u.92788
P : Type ?u.92791
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s : Set Q
y : Q
hy : y ∈ interior s
⊢ ∀ᶠ (δ : 𝕜) in 𝓝 1, ↑(homothety x δ) y ∈ s
[PROOFSTEP]
rw [(NormedAddCommGroup.nhds_basis_norm_lt (1 : 𝕜)).eventually_iff]
[GOAL]
α : Type ?u.92785
V : Type ?u.92788
P : Type ?u.92791
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s : Set Q
y : Q
hy : y ∈ interior s
⊢ ∃ i, 0 < i ∧ ∀ ⦃x_1 : 𝕜⦄, x_1 ∈ {y | ‖y - 1‖ < i} → ↑(homothety x x_1) y ∈ s
[PROOFSTEP]
cases' eq_or_ne y x with h h
[GOAL]
case inl
α : Type ?u.92785
V : Type ?u.92788
P : Type ?u.92791
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s : Set Q
y : Q
hy : y ∈ interior s
h : y = x
⊢ ∃ i, 0 < i ∧ ∀ ⦃x_1 : 𝕜⦄, x_1 ∈ {y | ‖y - 1‖ < i} → ↑(homothety x x_1) y ∈ s
[PROOFSTEP]
use 1
[GOAL]
case h
α : Type ?u.92785
V : Type ?u.92788
P : Type ?u.92791
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s : Set Q
y : Q
hy : y ∈ interior s
h : y = x
⊢ 0 < 1 ∧ ∀ ⦃x_1 : 𝕜⦄, x_1 ∈ {y | ‖y - 1‖ < 1} → ↑(homothety x x_1) y ∈ s
[PROOFSTEP]
simp [h.symm, interior_subset hy]
[GOAL]
case inr
α : Type ?u.92785
V : Type ?u.92788
P : Type ?u.92791
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s : Set Q
y : Q
hy : y ∈ interior s
h : y ≠ x
⊢ ∃ i, 0 < i ∧ ∀ ⦃x_1 : 𝕜⦄, x_1 ∈ {y | ‖y - 1‖ < i} → ↑(homothety x x_1) y ∈ s
[PROOFSTEP]
have hxy : 0 < ‖y -ᵥ x‖ := by rwa [norm_pos_iff, vsub_ne_zero]
[GOAL]
α : Type ?u.92785
V : Type ?u.92788
P : Type ?u.92791
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s : Set Q
y : Q
hy : y ∈ interior s
h : y ≠ x
⊢ 0 < ‖y -ᵥ x‖
[PROOFSTEP]
rwa [norm_pos_iff, vsub_ne_zero]
[GOAL]
case inr
α : Type ?u.92785
V : Type ?u.92788
P : Type ?u.92791
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s : Set Q
y : Q
hy : y ∈ interior s
h : y ≠ x
hxy : 0 < ‖y -ᵥ x‖
⊢ ∃ i, 0 < i ∧ ∀ ⦃x_1 : 𝕜⦄, x_1 ∈ {y | ‖y - 1‖ < i} → ↑(homothety x x_1) y ∈ s
[PROOFSTEP]
obtain ⟨u, hu₁, hu₂, hu₃⟩ := mem_interior.mp hy
[GOAL]
case inr.intro.intro.intro
α : Type ?u.92785
V : Type ?u.92788
P : Type ?u.92791
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s : Set Q
y : Q
hy : y ∈ interior s
h : y ≠ x
hxy : 0 < ‖y -ᵥ x‖
u : Set Q
hu₁ : u ⊆ s
hu₂ : IsOpen u
hu₃ : y ∈ u
⊢ ∃ i, 0 < i ∧ ∀ ⦃x_1 : 𝕜⦄, x_1 ∈ {y | ‖y - 1‖ < i} → ↑(homothety x x_1) y ∈ s
[PROOFSTEP]
obtain ⟨ε, hε, hyε⟩ := Metric.isOpen_iff.mp hu₂ y hu₃
[GOAL]
case inr.intro.intro.intro.intro.intro
α : Type ?u.92785
V : Type ?u.92788
P : Type ?u.92791
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s : Set Q
y : Q
hy : y ∈ interior s
h : y ≠ x
hxy : 0 < ‖y -ᵥ x‖
u : Set Q
hu₁ : u ⊆ s
hu₂ : IsOpen u
hu₃ : y ∈ u
ε : ℝ
hε : ε > 0
hyε : Metric.ball y ε ⊆ u
⊢ ∃ i, 0 < i ∧ ∀ ⦃x_1 : 𝕜⦄, x_1 ∈ {y | ‖y - 1‖ < i} → ↑(homothety x x_1) y ∈ s
[PROOFSTEP]
refine' ⟨ε / ‖y -ᵥ x‖, div_pos hε hxy, fun δ (hδ : ‖δ - 1‖ < ε / ‖y -ᵥ x‖) => hu₁ (hyε _)⟩
[GOAL]
case inr.intro.intro.intro.intro.intro
α : Type ?u.92785
V : Type ?u.92788
P : Type ?u.92791
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s : Set Q
y : Q
hy : y ∈ interior s
h : y ≠ x
hxy : 0 < ‖y -ᵥ x‖
u : Set Q
hu₁ : u ⊆ s
hu₂ : IsOpen u
hu₃ : y ∈ u
ε : ℝ
hε : ε > 0
hyε : Metric.ball y ε ⊆ u
δ : 𝕜
hδ : ‖δ - 1‖ < ε / ‖y -ᵥ x‖
⊢ ↑(homothety x δ) y ∈ Metric.ball y ε
[PROOFSTEP]
rw [lt_div_iff hxy, ← norm_smul, sub_smul, one_smul] at hδ 
[GOAL]
case inr.intro.intro.intro.intro.intro
α : Type ?u.92785
V : Type ?u.92788
P : Type ?u.92791
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s : Set Q
y : Q
hy : y ∈ interior s
h : y ≠ x
hxy : 0 < ‖y -ᵥ x‖
u : Set Q
hu₁ : u ⊆ s
hu₂ : IsOpen u
hu₃ : y ∈ u
ε : ℝ
hε : ε > 0
hyε : Metric.ball y ε ⊆ u
δ : 𝕜
hδ✝ : ‖δ - 1‖ * ‖y -ᵥ x‖ < ε
hδ : ‖δ • (y -ᵥ x) - (y -ᵥ x)‖ < ε
⊢ ↑(homothety x δ) y ∈ Metric.ball y ε
[PROOFSTEP]
rwa [homothety_apply, Metric.mem_ball, dist_eq_norm_vsub W, vadd_vsub_eq_sub_vsub]
[GOAL]
α : Type ?u.102650
V : Type ?u.102653
P : Type ?u.102656
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : Set.Finite t
h : t ⊆ interior s
⊢ ∀ᶠ (δ : 𝕜) in 𝓝 1, ↑(homothety x δ) '' t ⊆ s
[PROOFSTEP]
suffices ∀ y ∈ t, ∀ᶠ δ in 𝓝 (1 : 𝕜), homothety x δ y ∈ s
  by
  simp_rw [Set.image_subset_iff]
  exact (Filter.eventually_all_finite ht).mpr this
[GOAL]
α : Type ?u.102650
V : Type ?u.102653
P : Type ?u.102656
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : Set.Finite t
h : t ⊆ interior s
this : ∀ (y : Q), y ∈ t → ∀ᶠ (δ : 𝕜) in 𝓝 1, ↑(homothety x δ) y ∈ s
⊢ ∀ᶠ (δ : 𝕜) in 𝓝 1, ↑(homothety x δ) '' t ⊆ s
[PROOFSTEP]
simp_rw [Set.image_subset_iff]
[GOAL]
α : Type ?u.102650
V : Type ?u.102653
P : Type ?u.102656
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : Set.Finite t
h : t ⊆ interior s
this : ∀ (y : Q), y ∈ t → ∀ᶠ (δ : 𝕜) in 𝓝 1, ↑(homothety x δ) y ∈ s
⊢ ∀ᶠ (δ : 𝕜) in 𝓝 1, t ⊆ (fun a => ↑(homothety x δ) a) ⁻¹' s
[PROOFSTEP]
exact (Filter.eventually_all_finite ht).mpr this
[GOAL]
α : Type ?u.102650
V : Type ?u.102653
P : Type ?u.102656
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : Set.Finite t
h : t ⊆ interior s
⊢ ∀ (y : Q), y ∈ t → ∀ᶠ (δ : 𝕜) in 𝓝 1, ↑(homothety x δ) y ∈ s
[PROOFSTEP]
intro y hy
[GOAL]
α : Type ?u.102650
V : Type ?u.102653
P : Type ?u.102656
W : Type u_3
Q : Type u_1
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
x : Q
s t : Set Q
ht : Set.Finite t
h : t ⊆ interior s
y : Q
hy : y ∈ t
⊢ ∀ᶠ (δ : 𝕜) in 𝓝 1, ↑(homothety x δ) y ∈ s
[PROOFSTEP]
exact eventually_homothety_mem_of_mem_interior 𝕜 x (h hy)
[GOAL]
α : Type ?u.107060
V : Type u_1
P : Type ?u.107066
W : Type ?u.107069
Q : Type ?u.107072
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : PseudoMetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
inst✝¹ : NormedSpace ℝ V
inst✝ : NormedSpace ℝ W
p₁ p₂ p₃ p₄ : V
⊢ dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2
[PROOFSTEP]
have := dist_midpoint_midpoint_le' (𝕜 := ℝ) p₁ p₂ p₃ p₄
[GOAL]
α : Type ?u.107060
V : Type u_1
P : Type ?u.107066
W : Type ?u.107069
Q : Type ?u.107072
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : PseudoMetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
inst✝¹ : NormedSpace ℝ V
inst✝ : NormedSpace ℝ W
p₁ p₂ p₃ p₄ : V
this : dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / ‖2‖
⊢ dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2
[PROOFSTEP]
rw [Real.norm_eq_abs, abs_two] at this 
[GOAL]
α : Type ?u.107060
V : Type u_1
P : Type ?u.107066
W : Type ?u.107069
Q : Type ?u.107072
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : PseudoMetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
inst✝¹ : NormedSpace ℝ V
inst✝ : NormedSpace ℝ W
p₁ p₂ p₃ p₄ : V
this : dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2
⊢ dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2
[PROOFSTEP]
exact this
[GOAL]
α : Type ?u.111434
V : Type ?u.111437
P : Type ?u.111440
W : Type ?u.111443
Q : Type ?u.111446
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : PseudoMetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
inst✝¹ : NormedSpace ℝ V
inst✝ : NormedSpace ℝ W
f : P → Q
h : ∀ (x y : P), f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
hfc : Continuous f
c : P := Classical.arbitrary P
⊢ (↑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f c))) ∘ f ∘ ↑(AffineEquiv.vaddConst ℝ c)) 0 = 0
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.111434
V : Type ?u.111437
P : Type ?u.111440
W : Type ?u.111443
Q : Type ?u.111446
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : PseudoMetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
inst✝¹ : NormedSpace ℝ V
inst✝ : NormedSpace ℝ W
f : P → Q
h : ∀ (x y : P), f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
hfc : Continuous f
c : P := Classical.arbitrary P
x y : V
⊢ (↑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f c))) ∘ f ∘ ↑(AffineEquiv.vaddConst ℝ c)) (midpoint ℝ x y) =
    midpoint ℝ ((↑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f c))) ∘ f ∘ ↑(AffineEquiv.vaddConst ℝ c)) x)
      ((↑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f c))) ∘ f ∘ ↑(AffineEquiv.vaddConst ℝ c)) y)
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.111434
V : Type ?u.111437
P : Type ?u.111440
W : Type ?u.111443
Q : Type ?u.111446
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : PseudoMetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
inst✝¹ : NormedSpace ℝ V
inst✝ : NormedSpace ℝ W
f : P → Q
h : ∀ (x y : P), f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
hfc : Continuous f
c : P := Classical.arbitrary P
x y : V
⊢ f (midpoint ℝ x y +ᵥ Classical.arbitrary P) -ᵥ f (Classical.arbitrary P) =
    midpoint ℝ (f (x +ᵥ Classical.arbitrary P) -ᵥ f (Classical.arbitrary P))
      (f (y +ᵥ Classical.arbitrary P) -ᵥ f (Classical.arbitrary P))
[PROOFSTEP]
conv_lhs => rw [(midpoint_self ℝ (Classical.arbitrary P)).symm, midpoint_vadd_midpoint, h, h, midpoint_vsub_midpoint]
[GOAL]
α : Type ?u.111434
V : Type ?u.111437
P : Type ?u.111440
W : Type ?u.111443
Q : Type ?u.111446
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : PseudoMetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
inst✝¹ : NormedSpace ℝ V
inst✝ : NormedSpace ℝ W
f : P → Q
h : ∀ (x y : P), f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
hfc : Continuous f
c : P := Classical.arbitrary P
x y : V
| f (midpoint ℝ x y +ᵥ Classical.arbitrary P) -ᵥ f (Classical.arbitrary P)
[PROOFSTEP]
rw [(midpoint_self ℝ (Classical.arbitrary P)).symm, midpoint_vadd_midpoint, h, h, midpoint_vsub_midpoint]
[GOAL]
α : Type ?u.111434
V : Type ?u.111437
P : Type ?u.111440
W : Type ?u.111443
Q : Type ?u.111446
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : PseudoMetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
inst✝¹ : NormedSpace ℝ V
inst✝ : NormedSpace ℝ W
f : P → Q
h : ∀ (x y : P), f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
hfc : Continuous f
c : P := Classical.arbitrary P
x y : V
| f (midpoint ℝ x y +ᵥ Classical.arbitrary P) -ᵥ f (Classical.arbitrary P)
[PROOFSTEP]
rw [(midpoint_self ℝ (Classical.arbitrary P)).symm, midpoint_vadd_midpoint, h, h, midpoint_vsub_midpoint]
[GOAL]
α : Type ?u.111434
V : Type ?u.111437
P : Type ?u.111440
W : Type ?u.111443
Q : Type ?u.111446
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : PseudoMetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
inst✝¹ : NormedSpace ℝ V
inst✝ : NormedSpace ℝ W
f : P → Q
h : ∀ (x y : P), f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
hfc : Continuous f
c : P := Classical.arbitrary P
x y : V
| f (midpoint ℝ x y +ᵥ Classical.arbitrary P) -ᵥ f (Classical.arbitrary P)
[PROOFSTEP]
rw [(midpoint_self ℝ (Classical.arbitrary P)).symm, midpoint_vadd_midpoint, h, h, midpoint_vsub_midpoint]
[GOAL]
α : Type ?u.111434
V : Type ?u.111437
P : Type ?u.111440
W : Type ?u.111443
Q : Type ?u.111446
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : PseudoMetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
inst✝¹ : NormedSpace ℝ V
inst✝ : NormedSpace ℝ W
f : P → Q
h : ∀ (x y : P), f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
hfc : Continuous f
c : P := Classical.arbitrary P
⊢ Continuous
    ↑(AddMonoidHom.ofMapMidpoint ℝ ℝ
        (↑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f c))) ∘ f ∘ ↑(AffineEquiv.vaddConst ℝ c))
        (_ :
          ↑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f (Classical.arbitrary P)))) (f (0 +ᵥ Classical.arbitrary P)) =
            0)
        (_ :
          ∀ (x y : V),
            (↑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f c))) ∘ f ∘ ↑(AffineEquiv.vaddConst ℝ c)) (midpoint ℝ x y) =
              midpoint ℝ ((↑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f c))) ∘ f ∘ ↑(AffineEquiv.vaddConst ℝ c)) x)
                ((↑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f c))) ∘ f ∘ ↑(AffineEquiv.vaddConst ℝ c)) y)))
[PROOFSTEP]
apply_rules [Continuous.vadd, Continuous.vsub, continuous_const, hfc.comp, continuous_id]
[GOAL]
α : Type ?u.111434
V : Type ?u.111437
P : Type ?u.111440
W : Type ?u.111443
Q : Type ?u.111446
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : PseudoMetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
inst✝¹ : NormedSpace ℝ V
inst✝ : NormedSpace ℝ W
f : P → Q
h : ∀ (x y : P), f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
hfc : Continuous f
c : P := Classical.arbitrary P
p : P
⊢ f p =
    ↑↑(AddMonoidHom.toRealLinearMap
              (AddMonoidHom.ofMapMidpoint ℝ ℝ
                (↑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f c))) ∘ f ∘ ↑(AffineEquiv.vaddConst ℝ c))
                (_ :
                  ↑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f (Classical.arbitrary P))))
                      (f (0 +ᵥ Classical.arbitrary P)) =
                    0)
                (_ :
                  ∀ (x y : V),
                    (↑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f c))) ∘ f ∘ ↑(AffineEquiv.vaddConst ℝ c))
                        (midpoint ℝ x y) =
                      midpoint ℝ
                        ((↑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f c))) ∘ f ∘ ↑(AffineEquiv.vaddConst ℝ c)) x)
                        ((↑(AffineEquiv.symm (AffineEquiv.vaddConst ℝ (f c))) ∘ f ∘ ↑(AffineEquiv.vaddConst ℝ c)) y)))
              (_ : Continuous ((fun i => (f ∘ ↑(AffineEquiv.vaddConst ℝ c)) i) -ᵥ fun i => f c)))
        (p -ᵥ c) +ᵥ
      f c
[PROOFSTEP]
simp
