awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 2⁻¹ (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : Set.Countable (α := ℝ) {t : ℝ | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}
B : Set.Countable (α := ℝ) {t : ℝ | ([c - x -[ℝ] c + t • y] ∩ s).Nonempty}
t : ℝ
z : E := c + t • y
ht : [c + x -[ℝ] c + t • y] ∩ s = ∅ ∧ [c - x -[ℝ] c + t • y] ∩ s = ∅
JA : JoinedIn sᶜ a z
⊢ b = c + x

Tactic:
exact Ib.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 2⁻¹ (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : Set.Countable (α := ℝ) {t : ℝ | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}
B : Set.Countable (α := ℝ) {t : ℝ | ([c - x -[ℝ] c + t • y] ∩ s).Nonempty}
t : ℝ
z : E := c + t • y
ht : [c + x -[ℝ] c + t • y] ∩ s = ∅ ∧ [c - x -[ℝ] c + t • y] ∩ s = ∅
JA : JoinedIn sᶜ a z
⊢ JoinedIn sᶜ b z

Tactic:
have JB : JoinedIn sᶜ b z := by
    apply JoinedIn.of_segment_subset
    rw [subset_compl_iff_disjoint_right, disjoint_iff_inter_eq_empty]
    convert! ht.1
    exact Ib.symm
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 2⁻¹ (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : Set.Countable (α := ℝ) {t : ℝ | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}
B : Set.Countable (α := ℝ) {t : ℝ | ([c - x -[ℝ] c + t • y] ∩ s).Nonempty}
t : ℝ
z : E := c + t • y
ht : [c + x -[ℝ] c + t • y] ∩ s = ∅ ∧ [c - x -[ℝ] c + t • y] ∩ s = ∅
JA : JoinedIn sᶜ a z
JB : JoinedIn sᶜ b z
⊢ JoinedIn sᶜ a b

Tactic:
JA.trans JB.symm

Premises used: JoinedIn.symm, JoinedIn.trans
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 2⁻¹ (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : Set.Countable (α := ℝ) {t : ℝ | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}
B : Set.Countable (α := ℝ) {t : ℝ | ([c - x -[ℝ] c + t • y] ∩ s).Nonempty}
t : ℝ
z : E := c + t • y
ht : [c + x -[ℝ] c + t • y] ∩ s = ∅ ∧ [c - x -[ℝ] c + t • y] ∩ s = ∅
JA : JoinedIn sᶜ a z
JB : JoinedIn sᶜ b z
⊢ JoinedIn sᶜ a b

Tactic:
exact JA.trans JB.symm

Premises used: JoinedIn.symm, JoinedIn.trans
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
⊢ IsConnected sᶜ

Tactic:
(hs.isPathConnected_compl_of_one_lt_rank h).isConnected

Premises used: IsPathConnected.isConnected, Set.Countable.isPathConnected_compl_of_one_lt_rank
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
x : E
⊢ IsPathConnected (X := E) {x}ᶜ

Tactic:
Set.Countable.isPathConnected_compl_of_one_lt_rank h (countable_singleton x)

Premises used: Set.Countable.isPathConnected_compl_of_one_lt_rank, Set.countable_singleton
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
x : E
⊢ IsConnected (α := E) {x}ᶜ

Tactic:
(isPathConnected_compl_singleton_of_one_lt_rank h x).isConnected

Premises used: IsPathConnected.isConnected, isPathConnected_compl_singleton_of_one_lt_rank
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : 0 < r
⊢ (ball x r).Nonempty

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ≥0∞
hr : 0 < r
⊢ x ∈ eball x r

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : 0 ≤ r
⊢ (closedBall x r).Nonempty

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ≥0∞
⊢ x ∈ closedEBall x r

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : 0 ≤ r
⊢ x ∈ closedBall x r

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ≥0∞
⊢ IsPathConnected (closedEBall x r)

Tactic:
isPathConnected_iff_pathConnectedSpace.mpr inferInstance

Premises used: Iff.mpr, inferInstance, isPathConnected_iff_pathConnectedSpace
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
⊢ IsPreconnected (ball x r)

Tactic:
(convex_ball _ _).isPreconnected

Premises used: convex_ball, Convex.isPreconnected
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ≥0∞
⊢ IsPreconnected (eball x r)

Tactic:
(convex_eball _ _).isPreconnected

Premises used: convex_eball, Convex.isPreconnected
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
⊢ IsPreconnected (closedBall x r)

Tactic:
(convex_closedBall _ _).isPreconnected

Premises used: convex_closedBall, Convex.isPreconnected
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ≥0∞
⊢ IsPreconnected (closedEBall x r)

Tactic:
(convex_closedEBall _ _).isPreconnected

Premises used: convex_closedEBall, Convex.isPreconnected
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : 0 < r
⊢ IsConnected (ball x r)

Tactic:
(isPathConnected_ball hr).isConnected

Premises used: IsPathConnected.isConnected, Metric.isPathConnected_ball
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ≥0∞
hr : 0 < r
⊢ IsConnected (eball x r)

Tactic:
(isPathConnected_eball hr).isConnected

Premises used: IsPathConnected.isConnected, Metric.isPathConnected_eball
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ≥0∞
⊢ IsConnected (closedEBall x r)

Tactic:
⟨⟨x, mem_closedEBall_self⟩, isPreconnected_closedEBall⟩

Premises used: IsConnected, Metric.isPreconnected_closedEBall, Metric.mem_closedEBall_self, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
inl : ∀ (hr : LE.le (α := ℝ) 0 0), IsPathConnected (sphere x 0)
inr : ∀ (rpos : 0 < r), IsPathConnected (sphere x r)
⊢ IsPathConnected (sphere x r)

Tactic:
rcases hr.eq_or_lt with rfl | rpos

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
hr : LE.le (α := ℝ) 0 0
⊢ IsPathConnected (sphere x 0)

Tactic:
simpa using isPathConnected_singleton x

Premises used: isPathConnected_singleton
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun (y : E) ↦ x + (r * ‖y‖⁻¹) • y
y : E
hy : Membership.mem (γ := Set E) {0}ᶜ y
apply : ContinuousAt (Y := E) (fun (y : E) ↦ (r * ‖y‖⁻¹) • y) y
⊢ ContinuousWithinAt f {0}ᶜ y

Tactic:
apply (continuousAt_const.add _).continuousWithinAt

Premises used: ContinuousAt.add, ContinuousAt.continuousWithinAt, continuousAt_const
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun (y : E) ↦ x + (r * ‖y‖⁻¹) • y
y : E
hy : Membership.mem (γ := Set E) {0}ᶜ y
apply : ‖id y‖ ≠ 0
⊢ ContinuousAt (Y := E) (fun (y : E) ↦ (r * ‖y‖⁻¹) • y) y

Tactic:
apply (continuousAt_const.mul (ContinuousAt.inv₀ continuousAt_id.norm ?_)).smul continuousAt_id

Premises used: ContinuousAt.smul, continuousAt_const, ContinuousAt.inv₀, ContinuousAt.mul, ContinuousAt.norm, continuousAt_id
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun (y : E) ↦ x + (r * ‖y‖⁻¹) • y
y : E
hy : Membership.mem (γ := Set E) {0}ᶜ y
⊢ ‖id y‖ ≠ 0

Tactic:
simpa using hy
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun (y : E) ↦ x + (r * ‖y‖⁻¹) • y
⊢ ContinuousOn f {0}ᶜ

Tactic:
have A : ContinuousOn f {0}ᶜ := by
    intro y hy
    apply (continuousAt_const.add _).continuousWithinAt
    apply (continuousAt_const.mul (ContinuousAt.inv₀ continuousAt_id.norm ?_)).smul continuousAt_id
    simpa using hy
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun (y : E) ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
⊢ IsPathConnected (X := E) {0}ᶜ

Tactic:
have B : IsPathConnected ({0}ᶜ : Set E) := isPathConnected_compl_singleton_of_one_lt_rank h 0
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun (y : E) ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected (X := E) {0}ᶜ
⊢ IsPathConnected (f '' {0}ᶜ)

Tactic:
have C : IsPathConnected (f '' {0}ᶜ) := B.image' A
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun (y : E) ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected (X := E) {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
h₁ : f '' {0}ᶜ ⊆ sphere x r
h₂ : sphere x r ⊆ f '' {0}ᶜ
⊢ f '' {0}ᶜ = sphere x r

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun (y : E) ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected (X := E) {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
y : E
hy : Membership.mem (γ := Set E) {0}ᶜ y
⊢ ‖y‖ ≠ 0

Tactic:
simpa using hy
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun (y : E) ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected (X := E) {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
y : E
hy : Membership.mem (γ := Set E) {0}ᶜ y
⊢ ‖y‖ ≠ 0

Tactic:
have : ‖y‖ ≠ 0 := by simpa using hy
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun (y : E) ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected (X := E) {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
y : E
hy : Membership.mem (γ := Set E) {0}ᶜ y
this : ‖y‖ ≠ 0
⊢ f y ∈ sphere x r

Tactic:
simp [f, norm_smul, abs_of_nonneg hr, mul_assoc, inv_mul_cancel₀ this]

Premises used: norm_smul, mul_assoc, abs_of_nonneg, inv_mul_cancel₀
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun (y : E) ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected (X := E) {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
y : E
hy : y ∈ sphere x r
⊢ y ∈ f '' {0}ᶜ

Tactic:
⟨y - x, ?_, ?_⟩

Premises used: Set.Mem, setOf, HSub.hSub, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun (y : E) ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected (X := E) {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
y : E
hy : y ∈ sphere x r
h₂ : Membership.mem (γ := Set E) {0}ᶜ (y - x)
h₃ : f (y - x) = y
⊢ y ∈ f '' {0}ᶜ

Tactic:
refine ⟨y - x, ?_, ?_⟩
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun (y : E) ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected (X := E) {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
y : E
hy : y ∈ sphere x r
H : Membership.mem (γ := Set E) {0} (y - x)
⊢ y = x

Tactic:
simp only [mem_singleton_iff, sub_eq_zero] at H

Premises used: sub_eq_zero, Set.mem_singleton_iff
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun (y : E) ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected (X := E) {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
y : E
hy : y ∈ sphere x r
H : y = x
⊢ 0 = r

Tactic:
simp only [H, mem_sphere_iff_norm, sub_self, norm_zero] at hy

Premises used: sub_self, norm_zero, mem_sphere_iff_norm
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun (y : E) ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected (X := E) {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
y : E
H : y = x
hy : 0 = r
⊢ False

Tactic:
rpos.ne hy

Premises used: LT.lt.ne
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun (y : E) ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected (X := E) {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
y : E
H : y = x
hy : 0 = r
⊢ False

Tactic:
exact rpos.ne hy

Premises used: LT.lt.ne
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun (y : E) ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected (X := E) {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
y : E
hy : y ∈ sphere x r
⊢ f (y - x) = y

Tactic:
simp [f, mem_sphere_iff_norm.1 hy, mul_inv_cancel₀ rpos.ne']

Premises used: mul_inv_cancel₀, LT.lt.ne', mem_sphere_iff_norm, Iff.mp
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun (y : E) ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected (X := E) {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
⊢ f '' {0}ᶜ = sphere x r

Tactic:
have : f '' {0}ᶜ = sphere x r := by
    apply Subset.antisymm
    · rintro - ⟨y, hy, rfl⟩
      have : ‖y‖ ≠ 0 := by simpa using hy
      simp [f, norm_smul, abs_of_nonneg hr, mul_assoc, inv_mul_cancel₀ this]
    · intro y hy
      refine ⟨y - x, ?_, ?_⟩
      · intro H
        simp only [mem_singleton_iff, sub_eq_zero] at H
        simp only [H, mem_sphere_iff_norm, sub_self, norm_zero] at hy
        exact rpos.ne hy
      · simp [f, mem_sphere_iff_norm.1 hy, mul_inv_cancel₀ rpos.ne']
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun (y : E) ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected (X := E) {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
this : f '' {0}ᶜ = sphere x r
inr inr₁ inr₂ inr₃ : ∀ (C : IsPathConnected (sphere x r)) (this : f '' {0}ᶜ = sphere x r), IsPathConnected (sphere x r)
⊢ IsPathConnected (sphere x r)

Tactic:
rwa [this] at C
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
⊢ IsConnected (sphere x r)

Tactic:
(isPathConnected_sphere h x hr).isConnected

Premises used: IsPathConnected.isConnected, isPathConnected_sphere
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
inl : ∀ (hr : 0 ≤ r), IsPreconnected (sphere x r)
inr : ∀ (hr : r < 0), IsPreconnected (sphere x r)
⊢ IsPreconnected (sphere x r)

Tactic:
rcases le_or_gt 0 r with hr | hr

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
⊢ IsPreconnected (sphere x r)

Tactic:
(isConnected_sphere h x hr).isPreconnected

Premises used: isConnected_sphere, IsConnected.isPreconnected
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
⊢ IsPreconnected (sphere x r)

Tactic:
exact (isConnected_sphere h x hr).isPreconnected

Premises used: isConnected_sphere, IsConnected.isPreconnected
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : r < 0
⊢ IsPreconnected (sphere x r)

Tactic:
simpa [hr] using isPreconnected_empty

Premises used: isPreconnected_empty
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
rcases : ∀ (E' : Submodule ℝ F) (hE' : IsCompl E E'), IsPathConnected (↑E : Set F)ᶜ
⊢ IsPathConnected (↑E : Set F)ᶜ

Tactic:
rcases E.exists_isCompl with ⟨E', hE'⟩

Premises used: Submodule.exists_isCompl
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
E' : Submodule ℝ F
hE' : IsCompl E E'
⊢ IsPathConnected (↑E : Set F)ᶜ

Tactic:
isPathConnected_compl_of_isPathConnected_compl_zero hE'.symm
    (isPathConnected_compl_singleton_of_one_lt_rank ?_ 0)

Premises used: isPathConnected_compl_singleton_of_one_lt_rank, isPathConnected_compl_of_isPathConnected_compl_zero, OfNat.ofNat, IsCompl.symm
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
E' : Submodule ℝ F
hE' : IsCompl E E'
refine : 1 < Module.rank ℝ ↥E'
⊢ IsPathConnected (↑E : Set F)ᶜ

Tactic:
refine isPathConnected_compl_of_isPathConnected_compl_zero hE'.symm
    (isPathConnected_compl_singleton_of_one_lt_rank ?_ 0)

Premises used: isPathConnected_compl_singleton_of_one_lt_rank, isPathConnected_compl_of_isPathConnected_compl_zero, OfNat.ofNat, IsCompl.symm
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
E' : Submodule ℝ F
hE' : IsCompl E E'
rwa rwa₁ rwa₂ rwa₃ : 1 < Module.rank ℝ (F ⧸ E)
⊢ 1 < Module.rank ℝ ↥E'

Tactic:
rwa [← (E.quotientEquivOfIsCompl E' hE').rank_eq]

Premises used: Submodule.quotientEquivOfIsCompl, LinearEquiv.rank_eq
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
⊢ IsConnected (↑E : Set F)ᶜ

Tactic:
(isPathConnected_compl_of_one_lt_codim hcodim).isConnected

Premises used: IsPathConnected.isConnected, isPathConnected_compl_of_one_lt_codim
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∉ E
⊢ connectedComponentIn (↑E : Set F)ᶜ x = (↑E : Set F)ᶜ

Tactic:
(isConnected_compl_of_one_lt_codim hcodim).2.connectedComponentIn hx

Premises used: isConnected_compl_of_one_lt_codim, IsPreconnected.connectedComponentIn, And.right
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
h : f.HasLeftInverse
⊢ LeftInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑h.leftInverse : (a : F) → E) (⇑f : (a : E) → F)

Tactic:
Classical.choose_spec h

Premises used: Classical.choose_spec
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
h : f.HasLeftInverse
⊢ Injective.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)

Tactic:
h.leftInverse_leftInverse.injective

Premises used: Function.LeftInverse.injective, ContinuousLinearMap.HasLeftInverse.leftInverse_leftInverse
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
G : Type u_6
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace E'
inst_5 : AddCommMonoid E'
inst_6 : Module R E'
inst_7 : TopologicalSpace F
inst_8 : AddCommMonoid F
inst_9 : Module R F
inst_10 : TopologicalSpace F'
inst_11 : AddCommMonoid F'
inst_12 : Module R F'
f : E →L[R] F
h : f.HasLeftInverse
x : E
⊢ (h.leftInverse : (a : F) → E) ((f : (a : E) → F) x : F) = x

Tactic:
h.leftInverse_leftInverse x

Premises used: ContinuousLinearMap.HasLeftInverse.leftInverse_leftInverse