awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (hypothesis)
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}
⊢ JoinedIn sᶜ a b
have B : Set.Countable (α := ℝ) {t : ℝ | ([c - x -[ℝ] c + t • y] ∩ s).Nonempty}
Tactic: have B : Set.Countable {t : ℝ | ([c - x -[ℝ] c + t • y] ∩ s).Nonempty} := by
    apply countable_setOf_nonempty_of_disjoint _ (fun t ↦ inter_subset_right) hs
    intro t t' htt'
    apply disjoint_iff_inter_eq_empty.2
    have N : {c - x} ∩ s = ∅ := by
      simpa only [singleton_inter_eq_empty, mem_compl_iff, Ia] using ha
    rw [inter_assoc, inter_comm s, inter_assoc, inter_self, ← inter_assoc, ← subset_empty_iff, ← N]
    apply inter_subset_inter_left
    rw [sub_eq_add_neg _ x]
    apply Eq.subset
    apply segment_inter_eq_endpoint_of_linearIndependent_of_ne _ htt'.symm
    convert! hy.units_smul ![-1, 1]
    simp [← List.ofFn_inj]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
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}
⊢ JoinedIn sᶜ a b
have inr : ∀ (t : ℝ)
  (ht :
    Membership.mem (γ := Set ℝ)
      ({t : ℝ | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty} ∪ {t : ℝ | ([c - x -[ℝ] c + t • y] ∩ s).Nonempty})ᶜ t),
  JoinedIn sᶜ a b
Tactic: obtain ⟨t, ht⟩ : Set.Nonempty ({t : ℝ | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}
      ∪ {t : ℝ | ([c - x -[ℝ] c + t • y] ∩ s).Nonempty})ᶜ := ((A.union B).dense_compl ℝ).nonempty
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (hypothesis)
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 : ℝ
ht :
  Membership.mem (γ := Set ℝ)
    ({t : ℝ | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty} ∪ {t : ℝ | ([c - x -[ℝ] c + t • y] ∩ s).Nonempty})ᶜ t
z : E := c + t • y
⊢ JoinedIn sᶜ a b
have ht₁ : [c + x -[ℝ] c + t • y] ∩ s = ∅ ∧ [c - x -[ℝ] c + t • y] ∩ s = ∅
Tactic: simp only [compl_union, mem_inter_iff, mem_compl_iff, mem_setOf_eq, not_nonempty_iff_eq_empty]
    at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
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 = ∅
⊢ JoinedIn sᶜ a z
have h₁ : [a -[ℝ] z] ⊆ sᶜ
Tactic: apply JoinedIn.of_segment_subset
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
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 = ∅
⊢ [a -[ℝ] z] ⊆ sᶜ
have h₁ : [a -[ℝ] z] ∩ s = ∅
Tactic: rw [subset_compl_iff_disjoint_right, disjoint_iff_inter_eq_empty]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
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 = ∅
⊢ [a -[ℝ] z] ∩ s = ∅
have h₁ : a = c - x
Tactic: convert! ht.2
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (hypothesis)
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 = ∅
⊢ JoinedIn sᶜ a b
have JA : JoinedIn sᶜ a z
Tactic: have JA : JoinedIn sᶜ a z := by
    apply JoinedIn.of_segment_subset
    rw [subset_compl_iff_disjoint_right, disjoint_iff_inter_eq_empty]
    convert! ht.2
    exact Ia.symm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
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
have h₁ : [b -[ℝ] z] ⊆ sᶜ
Tactic: apply JoinedIn.of_segment_subset
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
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 -[ℝ] z] ⊆ sᶜ
have h₁ : [b -[ℝ] z] ∩ s = ∅
Tactic: rw [subset_compl_iff_disjoint_right, disjoint_iff_inter_eq_empty]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
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 -[ℝ] z] ∩ s = ∅
have h₁ : b = c + x
Tactic: convert! ht.1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (hypothesis)
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ᶜ a b
have JB : 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
⊢ IsPathConnected (sphere x r)
have inl : ∀ (hr : LE.le (α := ℝ) 0 0), IsPathConnected (sphere x 0)
Tactic: rcases hr.eq_or_lt with rfl | rpos
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
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)
⊢ IsPathConnected (sphere x r)
have inr : ∀ (rpos : 0 < r), IsPathConnected (sphere x r)
Tactic: rcases hr.eq_or_lt with rfl | rpos
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
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
⊢ ContinuousWithinAt f {0}ᶜ y
have apply : ContinuousAt (Y := E) (fun (y : E) ↦ (r * ‖y‖⁻¹) • y) y
Tactic: apply (continuousAt_const.add _).continuousWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
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
⊢ ContinuousAt (Y := E) (fun (y : E) ↦ (r * ‖y‖⁻¹) • y) y
have apply : ‖id y‖ ≠ 0
Tactic: apply (continuousAt_const.mul (ContinuousAt.inv₀ continuousAt_id.norm ?_)).smul continuousAt_id
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (hypothesis)
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
⊢ IsPathConnected (sphere x r)
have A : 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (hypothesis)
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 (sphere x r)
have B : IsPathConnected (X := E) {0}ᶜ
Tactic: have B : IsPathConnected ({0}ᶜ : Set E) := isPathConnected_compl_singleton_of_one_lt_rank h 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (hypothesis)
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 (sphere x r)
have C : IsPathConnected (f '' {0}ᶜ)
Tactic: have C : IsPathConnected (f '' {0}ᶜ) := B.image' A
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
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
have h₁ : f '' {0}ᶜ ⊆ sphere x r
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
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
⊢ f '' {0}ᶜ = sphere x r
have h₂ : sphere x r ⊆ f '' {0}ᶜ
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (hypothesis)
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
⊢ f y ∈ sphere x r
have this : ‖y‖ ≠ 0
Tactic: have : ‖y‖ ≠ 0 := by simpa using hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
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}ᶜ
have h₂ : Membership.mem (γ := Set E) {0}ᶜ (y - x)
Tactic: refine ⟨y - x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
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 ∈ f '' {0}ᶜ
have h₃ : f (y - x) = y
Tactic: refine ⟨y - x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (hypothesis)
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)
⊢ False
have H₁ : y = x
Tactic: simp only [mem_singleton_iff, sub_eq_zero] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (hypothesis)
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
⊢ False
have hy₁ : 0 = r
Tactic: simp only [H, mem_sphere_iff_norm, sub_self, norm_zero] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (hypothesis)
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}ᶜ)
⊢ IsPathConnected (sphere x r)
have this : 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']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
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
⊢ IsPathConnected (sphere x r)
have inr : ∀ (C : IsPathConnected (sphere x r)) (this : f '' {0}ᶜ = sphere x r), IsPathConnected (sphere x r)
Tactic: rwa [this] at C
Cleared hypotheses: C, this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
⊢ IsPreconnected (sphere x r)
have inl : ∀ (hr : 0 ≤ r), IsPreconnected (sphere x r)
Tactic: rcases le_or_gt 0 r with hr | hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
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)
⊢ IsPreconnected (sphere x r)
have inr : ∀ (hr : r < 0), IsPreconnected (sphere x r)
Tactic: rcases le_or_gt 0 r with hr | hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
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)
⊢ IsPathConnected (↑E : Set F)ᶜ
have rcases : ∀ (E' : Submodule ℝ F) (hE' : IsCompl E E'), IsPathConnected (↑E : Set F)ᶜ
Tactic: rcases E.exists_isCompl with ⟨E', hE'⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Connected (goal)
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)ᶜ
have refine : 1 < Module.rank ℝ ↥E'
Tactic: refine isPathConnected_compl_of_isPathConnected_compl_zero hE'.symm
    (isPathConnected_compl_singleton_of_one_lt_rank ?_ 0)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
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
⊢ ⋯.leftInverse = (↑f.symm : F →L[R] E)
have h : ∀ (y : F), Eq.{u_2 + 1} (α := E) ((sorry.leftInverse : (a : F) → E) y : E) (((↑f.symm : F →L[R] E) : (a : F) → E) y : E)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
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
y : F
⊢ Eq.{u_2 + 1} (α := E) ((⋯.leftInverse : (a : F) → E) y : E) (((↑f.symm : F →L[R] E) : (a : F) → E) y : E)
have calc : Eq.{u_2 + 1} (α := E) ((sorry.leftInverse : (a : F) → E) y : E)
  ((sorry.leftInverse : (a : F) → E) ((f : (a : E) → F) ((f.symm : (a : F) → E) y : E) : F) : E)
Tactic: calc f.hasLeftInverse.leftInverse y
    _ = f.hasLeftInverse.leftInverse (f (f.symm y)) := by simp
    _ = f.symm y := f.hasLeftInverse.leftInverse_leftInverse (f.symm y)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
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
hf : f.IsInvertible
⊢ f.HasLeftInverse
have obtain : ∀ (e : E ≃L[R] F), (↑e : E →L[R] F).HasLeftInverse
Tactic: obtain ⟨e, rfl⟩ := hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
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
g : E' →L[R] F'
hf : f.HasLeftInverse
hg : g.HasLeftInverse
⊢ (f.prodMap g).HasLeftInverse
have obtain : ∀ (finv : F →L[R] E)
  (hfinv : LeftInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)),
  (f.prodMap g).HasLeftInverse
Tactic: obtain ⟨finv, hfinv⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
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
g : E' →L[R] F'
hg : g.HasLeftInverse
finv : F →L[R] E
hfinv : LeftInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)
⊢ (f.prodMap g).HasLeftInverse
have obtain : ∀ (ginv : F' →L[R] E')
  (hginv : LeftInverse.{u_3 + 1, u_5 + 1} (α := E') (β := F') (⇑ginv : (a : F') → E') (⇑g : (a : E') → F')),
  (f.prodMap g).HasLeftInverse
Tactic: obtain ⟨ginv, hginv⟩ := hg
Cleared hypotheses: hg