-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem eventually_homothety_mem_of_mem_interior (x : Q) {s : Set Q} {y : Q} (hy : y ∈ interior s) :
    ∀ᶠ δ in 𝓝 (1 : 𝕜), homothety x δ y ∈ s

Proof state:
case inr.intro.intro.intro
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
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

Tactic:
obtain ⟨ε, hε, hyε⟩ := Metric.isOpen_iff.mp hu₂ y hu₃

Result:
case inr.intro.intro.intro.intro.intro
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
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

Proof state:
case inr
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
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

Tactic:
have hxy : 0 < ‖y -ᵥ x‖ := by rwa [norm_pos_iff, vsub_ne_zero]

Result:
case inr
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
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

Proof state:
case inl
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
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

Tactic:
use 1

Result:
case h
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
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

Proof state:
case inr.intro.intro.intro.intro.intro
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
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

Tactic:
refine ⟨ε / ‖y -ᵥ x‖, div_pos hε hxy, fun δ (hδ : ‖δ - 1‖ < ε / ‖y -ᵥ x‖) => hu₁ (hyε ?_)⟩

Result:
case inr.intro.intro.intro.intro.intro
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
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 ε

Proof state:
case inr.intro.intro.intro.intro.intro
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
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 ε

Tactic:
rw [lt_div_iff₀ hxy, ← norm_smul, sub_smul, one_smul] at hδ

Result:
case inr.intro.intro.intro.intro.intro
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
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δ : ‖δ • (y -ᵥ x) - (y -ᵥ x)‖ < ε
⊢ (homothety x δ) y ∈ Metric.ball y ε

Proof state:
case inr
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
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

Tactic:
obtain ⟨u, hu₁, hu₂, hu₃⟩ := mem_interior.mp hy

Result:
case inr.intro.intro.intro
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
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

Proof state:
case inr.intro.intro.intro.intro.intro
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
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δ : ‖δ • (y -ᵥ x) - (y -ᵥ x)‖ < ε
⊢ (homothety x δ) y ∈ Metric.ball y ε

Tactic:
rwa [homothety_apply, Metric.mem_ball, dist_eq_norm_vsub W, vadd_vsub_eq_sub_vsub]

Result:
no goals

Proof state:
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
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

Tactic:
rcases eq_or_ne y x with h | h

Result:
case inl
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
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

case inr
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
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

Proof state:
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 W
x : Q
s : Set Q
y : Q
hy : y ∈ interior s
h : y ≠ x
⊢ 0 < ‖y -ᵥ x‖

Tactic:
rwa [norm_pos_iff, vsub_ne_zero]

Result:
no goals

Proof state:
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 W
x : Q
s : Set Q
y : Q
hy : y ∈ interior s
⊢ ∀ᶠ (δ : 𝕜) in 𝓝 1, (homothety x δ) y ∈ s

Tactic:
rw [(NormedAddCommGroup.nhds_basis_norm_lt (1 : 𝕜)).eventually_iff]

Result:
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
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