awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
_ :
  norm.{u_7} (E := H) ((f : (a : G) → H) x : H) =
    ‖HSMul.hSMul (α := ℝ) (β := H) (↑n : ℝ)⁻¹ ((f : (a : G) → H) (n • x) : H)‖
_₁ : norm (E := ℝ) (↑n : ℝ)⁻¹ * norm.{u_7} (E := H) ((f : (a : G) → H) (n • x) : H) < norm (E := ℝ) (↑n : ℝ)⁻¹ * C
_₂ : norm (E := ℝ) (↑n : ℝ)⁻¹ * C = (↑n : ℝ)⁻¹ * C
⊢ norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε
have _₃ : (↑n : ℝ)⁻¹ * C < (C / ε)⁻¹ * C
Tactic: calc
    ‖f x‖
    _ = ‖(n : ℝ)⁻¹ • f (n • x)‖ := by simp [← Nat.cast_smul_eq_nsmul ℝ, hn₀]
    _ ≤ ‖(n : ℝ)⁻¹‖ * ‖f (n • x)‖ := norm_smul_le ..
    _ < ‖(n : ℝ)⁻¹‖ * C := by
      gcongr
      · simpa [pos_iff_ne_zero]
      · refine hC _ <| norm_nsmul_le.trans_lt ?_
        simpa only [norm_mul, Real.norm_natCast, lt_div_iff₀ hnpos, mul_comm] using hxδ
    _ = (n : ℝ)⁻¹ * C := by simp
    _ < (C / ε : ℝ)⁻¹ * C := by gcongr
    _ = ε := by simp [hC₀.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
_ :
  norm.{u_7} (E := H) ((f : (a : G) → H) x : H) =
    ‖HSMul.hSMul (α := ℝ) (β := H) (↑n : ℝ)⁻¹ ((f : (a : G) → H) (n • x) : H)‖
_₁ : norm (E := ℝ) (↑n : ℝ)⁻¹ * norm.{u_7} (E := H) ((f : (a : G) → H) (n • x) : H) < norm (E := ℝ) (↑n : ℝ)⁻¹ * C
_₂ : norm (E := ℝ) (↑n : ℝ)⁻¹ * C = (↑n : ℝ)⁻¹ * C
_₃ : (↑n : ℝ)⁻¹ * C < (C / ε)⁻¹ * C
⊢ norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε
have _₄ : (C / ε)⁻¹ * C = ε
Tactic: calc
    ‖f x‖
    _ = ‖(n : ℝ)⁻¹ • f (n • x)‖ := by simp [← Nat.cast_smul_eq_nsmul ℝ, hn₀]
    _ ≤ ‖(n : ℝ)⁻¹‖ * ‖f (n • x)‖ := norm_smul_le ..
    _ < ‖(n : ℝ)⁻¹‖ * C := by
      gcongr
      · simpa [pos_iff_ne_zero]
      · refine hC _ <| norm_nsmul_le.trans_lt ?_
        simpa only [norm_mul, Real.norm_natCast, lt_div_iff₀ hnpos, mul_comm] using hxδ
    _ = (n : ℝ)⁻¹ * C := by simp
    _ < (C / ε : ℝ)⁻¹ * C := by gcongr
    _ = ε := by simp [hC₀.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Complemented (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed (↑p : Set E)
hq : IsClosed (↑q : Set E)
⊢ (↥p × ↥q) ≃L[𝕜] E
have this : CompleteSpace.{u_2} (↑(↑p : Set E) : Type u_2)
Tactic: haveI := hp.completeSpace_coe
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Complemented (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed (↑p : Set E)
hq : IsClosed (↑q : Set E)
this : CompleteSpace.{u_2} (↑(↑p : Set E) : Type u_2)
⊢ (↥p × ↥q) ≃L[𝕜] E
have this₁ : CompleteSpace.{u_2} (↑(↑q : Set E) : Type u_2)
Tactic: haveI := hq.completeSpace_coe
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Complemented (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed (↑p : Set E)
hq : IsClosed (↑q : Set E)
this_1 : CompleteSpace.{u_2} (↑(↑p : Set E) : Type u_2)
this : CompleteSpace.{u_2} (↑(↑q : Set E) : Type u_2)
⊢ (↥p × ↥q) ≃L[𝕜] E
have refine : Continuous (X := ↥p × ↥q) (Y := E) (⇑(prodEquivOfIsCompl p q h) : (a : ↥p × ↥q) → E)
Tactic: refine (p.prodEquivOfIsCompl q h).toContinuousLinearEquivOfContinuous ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Completion (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst : SeminormedRing A
⊢ IsClosed.{u_3} (X := Completion A × Completion A) {x : Completion A × Completion A | ‖x.1 * x.2‖ ≤ ‖x.1‖ * ‖x.2‖}
have hp : Continuous (Y := ℝ) fun (b : Completion A × Completion A) ↦ ‖b.1 * b.2‖
Tactic: apply isClosed_le
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Completion (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst : SeminormedRing A
hp : Continuous (Y := ℝ) fun (b : Completion A × Completion A) ↦ ‖b.1 * b.2‖
⊢ IsClosed.{u_3} (X := Completion A × Completion A) {x : Completion A × Completion A | ‖x.1 * x.2‖ ≤ ‖x.1‖ * ‖x.2‖}
have hp₁ : Continuous (Y := ℝ) fun (b : Completion A × Completion A) ↦ ‖b.1‖ * ‖b.2‖
Tactic: apply isClosed_le
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Completion (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst : SeminormedRing A
x y : Completion A
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖
have hp : IsClosed.{u_3} (X := Completion A × Completion A) {x : Completion A × Completion A | ‖x.1 * x.2‖ ≤ ‖x.1‖ * ‖x.2‖}
Tactic: induction x, y using induction_on₂ with
    | hp => apply isClosed_le <;> fun_prop
    | ih x y => simpa only [← coe_mul, norm_coe] using norm_mul_le x y
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Completion (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst : SeminormedRing A
x y : Completion A
hp : IsClosed.{u_3} (X := Completion A × Completion A) {x : Completion A × Completion A | ‖x.1 * x.2‖ ≤ ‖x.1‖ * ‖x.2‖}
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖
have ih : ∀ (x y : A),
  ‖HMul.hMul (α := Completion A) (↑x : Completion A) (↑y : Completion A)‖ ≤
    norm (E := Completion A) (↑x : Completion A) * norm (E := Completion A) (↑y : Completion A)
Tactic: induction x, y using induction_on₂ with
    | hp => apply isClosed_le <;> fun_prop
    | ih x y => simpa only [← coe_mul, norm_coe] using norm_mul_le x y
Cleared hypotheses: x, y
-- 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
⊢ IsPathConnected sᶜ
have this : Nontrivial E
Tactic: have : Nontrivial E := (rank_pos_iff_nontrivial (R := ℝ)).1 (zero_lt_one.trans h)
-- 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
⊢ IsPathConnected sᶜ
have obtain : ∀ (a : E) (ha : a ∈ sᶜ), IsPathConnected sᶜ
Tactic: obtain ⟨a, ha⟩ : sᶜ.Nonempty := (hs.dense_compl ℝ).nonempty
-- 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ᶜ
⊢ IsPathConnected sᶜ
have refine : ∀ ⦃y : E⦄, y ∈ sᶜ → JoinedIn sᶜ a y
Tactic: refine ⟨a, ha, ?_⟩
-- 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ᶜ
⊢ JoinedIn sᶜ a b
have inl : ∀ (hb : a ∈ sᶜ), JoinedIn sᶜ a a
Tactic: rcases eq_or_ne a b with rfl | hab
Cleared hypotheses: b, hb
-- 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ᶜ
inl : ∀ (hb : a ∈ sᶜ), JoinedIn sᶜ a a
⊢ JoinedIn sᶜ a b
have inr : ∀ (hab : a ≠ b), JoinedIn sᶜ a b
Tactic: rcases eq_or_ne a b with rfl | hab
-- 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)
⊢ JoinedIn sᶜ a b
have Ia : c - x = a
Tactic: have Ia : c - x = a := by
    simp only [c, x]
    module
-- 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
⊢ JoinedIn sᶜ a b
have Ib : c + x = b
Tactic: have Ib : c + x = b := by
    simp only [c, x]
    module
-- 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
⊢ JoinedIn sᶜ a b
have x_ne_zero : x ≠ 0
Tactic: have x_ne_zero : x ≠ 0 := by simpa [x] using sub_ne_zero.2 hab.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]
⊢ Set.Countable (α := ℝ) {t : ℝ | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}
have apply : Pairwise (α := ℝ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (t : ℝ) ↦ [c + x -[ℝ] c + t • y] ∩ s)
Tactic: apply countable_setOf_nonempty_of_disjoint _ (fun t ↦ inter_subset_right) hs
-- 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]
t t' : ℝ
htt' : t ≠ t'
⊢ Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint (fun (t : ℝ) ↦ [c + x -[ℝ] c + t • y] ∩ s) t t'
have apply : Eq.{u_1 + 1} (α := Set E) ((fun (t : ℝ) ↦ [c + x -[ℝ] c + t • y] ∩ s) t ∩ (fun (t : ℝ) ↦ [c + x -[ℝ] c + t • y] ∩ s) t')
  ∅
Tactic: apply disjoint_iff_inter_eq_empty.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]
t t' : ℝ
htt' : t ≠ t'
⊢ Eq.{u_1 + 1} (α := Set E)
    ((fun (t : ℝ) ↦ [c + x -[ℝ] c + t • y] ∩ s) t ∩ (fun (t : ℝ) ↦ [c + x -[ℝ] c + t • y] ∩ s) t') ∅
have N : {c + x} ∩ s = ∅
Tactic: have N : {c + x} ∩ s = ∅ := by
      simpa only [singleton_inter_eq_empty, mem_compl_iff, Ib] using hb
-- 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]
t t' : ℝ
htt' : t ≠ t'
N : {c + x} ∩ s = ∅
⊢ Eq.{u_1 + 1} (α := Set E)
    ((fun (t : ℝ) ↦ [c + x -[ℝ] c + t • y] ∩ s) t ∩ (fun (t : ℝ) ↦ [c + x -[ℝ] c + t • y] ∩ s) t') ∅
have rw : [c + x -[ℝ] c + t • y] ∩ [c + x -[ℝ] c + t' • y] ∩ s ⊆ {c + x} ∩ s
Tactic: rw [inter_assoc, inter_comm s, inter_assoc, inter_self, ← inter_assoc, ← subset_empty_iff, ← N]
-- 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]
t t' : ℝ
htt' : t ≠ t'
N : {c + x} ∩ s = ∅
⊢ [c + x -[ℝ] c + t • y] ∩ [c + x -[ℝ] c + t' • y] ∩ s ⊆ {c + x} ∩ s
have H : [c + x -[ℝ] c + t • y] ∩ [c + x -[ℝ] c + t' • y] ⊆ {c + x}
Tactic: apply inter_subset_inter_left
-- 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]
t t' : ℝ
htt' : t ≠ t'
N : {c + x} ∩ s = ∅
⊢ [c + x -[ℝ] c + t • y] ∩ [c + x -[ℝ] c + t' • y] ⊆ {c + x}
have H : [c + x -[ℝ] c + t • y] ∩ [c + x -[ℝ] c + t' • y] = {c + x}
Tactic: apply Eq.subset
-- 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]
⊢ JoinedIn sᶜ a b
have A : Set.Countable (α := ℝ) {t : ℝ | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}
Tactic: have A : 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, Ib] using hb
    rw [inter_assoc, inter_comm s, inter_assoc, inter_self, ← inter_assoc, ← subset_empty_iff, ← N]
    apply inter_subset_inter_left
    apply Eq.subset
    apply segment_inter_eq_endpoint_of_linearIndependent_of_ne hy htt'.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}
⊢ Set.Countable (α := ℝ) {t : ℝ | ([c - x -[ℝ] c + t • y] ∩ s).Nonempty}
have apply : Pairwise (α := ℝ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (t : ℝ) ↦ [c - x -[ℝ] c + t • y] ∩ s)
Tactic: apply countable_setOf_nonempty_of_disjoint _ (fun t ↦ inter_subset_right) hs
-- 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}
t t' : ℝ
htt' : t ≠ t'
⊢ Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint (fun (t : ℝ) ↦ [c - x -[ℝ] c + t • y] ∩ s) t t'
have apply : Eq.{u_1 + 1} (α := Set E) ((fun (t : ℝ) ↦ [c - x -[ℝ] c + t • y] ∩ s) t ∩ (fun (t : ℝ) ↦ [c - x -[ℝ] c + t • y] ∩ s) t')
  ∅
Tactic: apply disjoint_iff_inter_eq_empty.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}
t t' : ℝ
htt' : t ≠ t'
⊢ Eq.{u_1 + 1} (α := Set E)
    ((fun (t : ℝ) ↦ [c - x -[ℝ] c + t • y] ∩ s) t ∩ (fun (t : ℝ) ↦ [c - x -[ℝ] c + t • y] ∩ s) t') ∅
have N : {c - x} ∩ s = ∅
Tactic: have N : {c - x} ∩ s = ∅ := by
      simpa only [singleton_inter_eq_empty, mem_compl_iff, Ia] using ha
-- 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}
t t' : ℝ
htt' : t ≠ t'
N : {c - x} ∩ s = ∅
⊢ Eq.{u_1 + 1} (α := Set E)
    ((fun (t : ℝ) ↦ [c - x -[ℝ] c + t • y] ∩ s) t ∩ (fun (t : ℝ) ↦ [c - x -[ℝ] c + t • y] ∩ s) t') ∅
have rw : [c - x -[ℝ] c + t • y] ∩ [c - x -[ℝ] c + t' • y] ∩ s ⊆ {c - x} ∩ s
Tactic: rw [inter_assoc, inter_comm s, inter_assoc, inter_self, ← inter_assoc, ← subset_empty_iff, ← N]
-- 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}
t t' : ℝ
htt' : t ≠ t'
N : {c - x} ∩ s = ∅
⊢ [c - x -[ℝ] c + t • y] ∩ [c - x -[ℝ] c + t' • y] ∩ s ⊆ {c - x} ∩ s
have H : [c - x -[ℝ] c + t • y] ∩ [c - x -[ℝ] c + t' • y] ⊆ {c - x}
Tactic: apply inter_subset_inter_left
-- 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}
t t' : ℝ
htt' : t ≠ t'
N : {c - x} ∩ s = ∅
⊢ [c - x -[ℝ] c + t • y] ∩ [c - x -[ℝ] c + t' • y] ⊆ {c - x}
have H : [c + -x -[ℝ] c + t • y] ∩ [c + -x -[ℝ] c + t' • y] ⊆ {c + -x}
Tactic: rw [sub_eq_add_neg _ x]
-- 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}
t t' : ℝ
htt' : t ≠ t'
N : {c - x} ∩ s = ∅
⊢ [c + -x -[ℝ] c + t • y] ∩ [c + -x -[ℝ] c + t' • y] ⊆ {c + -x}
have H : [c + -x -[ℝ] c + t • y] ∩ [c + -x -[ℝ] c + t' • y] = {c + -x}
Tactic: apply Eq.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}
t t' : ℝ
htt' : t ≠ t'
N : {c - x} ∩ s = ∅
⊢ [c + -x -[ℝ] c + t • y] ∩ [c + -x -[ℝ] c + t' • y] = {c + -x}
have apply : LinearIndependent ℝ ![-x, y]
Tactic: apply segment_inter_eq_endpoint_of_linearIndependent_of_ne _ htt'.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}
t t' : ℝ
htt' : t ≠ t'
N : {c - x} ∩ s = ∅
⊢ LinearIndependent ℝ ![-x, y]
have h₁ : ![-x, y] = HSMul.hSMul (α := Fin (Nat.succ 0).succ → ℝˣ) ![-1, 1] ![x, y]
Tactic: convert! hy.units_smul ![-1, 1]