internlm/Lean-Github huggingface dataset:
Theorem: Submodule_cutspace
Proof state before:
case right.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
⊢ x ∈ ↑p → x ∈ cutSpace (Submodule_cut p)
Tactic:
rintro hx Hi_ ⟨ H, ⟨ _, ⟨ v, ⟨ i, hi ⟩, rfl ⟩ , hHHalfpair ⟩, rfl ⟩
Proof state after:
case right.h.mp.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hx : x ∈ ↑p
H : Halfspace E
v : { x // x ≠ 0 }
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
hi : (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i = ↑v
hHHalfpair : H ∈ orthoHyperplane v
⊢ x ∈ ↑H
Theorem: Submodule_cutspace
Proof state before:
case right.h.mp.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hx : x ∈ ↑p
H : Halfspace E
v : { x // x ≠ 0 }
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
hi : (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i = ↑v
hHHalfpair : H ∈ orthoHyperplane v
⊢ x ∈ ↑H
Tactic:
rw [Halfspace_mem]
Proof state after:
case right.h.mp.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hx : x ∈ ↑p
H : Halfspace E
v : { x // x ≠ 0 }
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
hi : (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i = ↑v
hHHalfpair : H ∈ orthoHyperplane v
⊢ ↑H.f x ≤ H.α
Theorem: Submodule_cutspace
Proof state before:
case right.h.mp.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hx : x ∈ ↑p
H : Halfspace E
v : { x // x ≠ 0 }
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
hi : (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i = ↑v
hHHalfpair : H ∈ orthoHyperplane v
⊢ ↑H.f x ≤ H.α
Tactic:
revert hHHalfpair H
Proof state after:
case right.h.mp.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hx : x ∈ ↑p
v : { x // x ≠ 0 }
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
hi : (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i = ↑v
⊢ ∀ H ∈ orthoHyperplane v, ↑H.f x ≤ H.α
Theorem: Submodule_cutspace
Proof state before:
case right.h.mp.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hx : x ∈ ↑p
v : { x // x ≠ 0 }
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
hi : (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i = ↑v
⊢ ∀ H ∈ orthoHyperplane v, ↑H.f x ≤ H.α
Tactic:
rw [← mem_cutSpace,  orthoHyperplane_mem, ← hi, Submodule.inner_left_of_mem_orthogonal hx]
Proof state after:
case right.h.mp.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hx : x ∈ ↑p
v : { x // x ≠ 0 }
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
hi : (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i = ↑v
⊢ (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i ∈ pᗮ
Theorem: Submodule_cutspace
Proof state before:
case right.h.mp.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hx : x ∈ ↑p
v : { x // x ≠ 0 }
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
hi : (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i = ↑v
⊢ (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)) i ∈ pᗮ
Tactic:
exact Submodule.coe_mem ((FiniteDimensional.finBasis ℝ { x // x ∈ pᗮ }) i)
Proof state after:
no goals
Theorem: Submodule_cutspace
Proof state before:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
⊢ x ∈ cutSpace (Submodule_cut p) → x ∈ ↑p
Tactic:
rintro hHi_
Proof state after:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : x ∈ cutSpace (Submodule_cut p)
⊢ x ∈ ↑p
Theorem: Submodule_cutspace
Proof state before:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : x ∈ cutSpace (Submodule_cut p)
⊢ x ∈ ↑p
Tactic:
rw [Submodule_cut, orthoHyperplanes_mem] at hHi_
Proof state after:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
⊢ x ∈ ↑p
Theorem: Submodule_cutspace
Proof state before:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
⊢ x ∈ ↑p
Tactic:
rw [SetLike.mem_coe, ← Submodule.orthogonal_orthogonal p]
Proof state after:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
⊢ x ∈ pᗮᗮ
Theorem: Submodule_cutspace
Proof state before:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
⊢ x ∈ pᗮᗮ
Tactic:
intro y hy
Proof state after:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
⊢ ⟪y, x⟫_ℝ = 0
Theorem: Submodule_cutspace
Proof state before:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
⊢ ⟪y, x⟫_ℝ = 0
Tactic:
have : ∀ i, inner (Subtype.val (FiniteDimensional.finBasis ℝ { x // x ∈ pᗮ } i)) x = (0:ℝ) := by
  intro i
  let v : E := (FiniteDimensional.finBasis ℝ { x // x ∈ pᗮ }) i
  let v' : { x // x ≠ 0 } := ⟨ v, fun hv => (Basis.ne_zero (FiniteDimensional.finBasis ℝ { x // x ∈ pᗮ }) i) (Submodule.coe_eq_zero.mp hv) ⟩
  exact hHi_ v' ⟨ i, rfl ⟩
Proof state after:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
this : ∀ (i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)), ⟪↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i), x⟫_ℝ = 0
⊢ ⟪y, x⟫_ℝ = 0
Theorem: Submodule_cutspace
Proof state before:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
this : ∀ (i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)), ⟪↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i), x⟫_ℝ = 0
⊢ ⟪y, x⟫_ℝ = 0
Tactic:
rw [← Submodule.mem_orthogonal_Basis] at this
Proof state after:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
this : x ∈ pᗮᗮ
⊢ ⟪y, x⟫_ℝ = 0
Theorem: Submodule_cutspace
Proof state before:
case right.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
this : x ∈ pᗮᗮ
⊢ ⟪y, x⟫_ℝ = 0
Tactic:
exact this _ hy
Proof state after:
no goals
Theorem: Submodule_cutspace
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
⊢ ∀ (i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)), ⟪↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i), x⟫_ℝ = 0
Tactic:
intro i
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
⊢ ⟪↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i), x⟫_ℝ = 0
Theorem: Submodule_cutspace
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
⊢ ⟪↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i), x⟫_ℝ = 0
Tactic:
let v : E := (FiniteDimensional.finBasis ℝ { x // x ∈ pᗮ }) i
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
v : E := ↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i)
⊢ ⟪↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i), x⟫_ℝ = 0
Theorem: Submodule_cutspace
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
v : E := ↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i)
⊢ ⟪↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i), x⟫_ℝ = 0
Tactic:
let v' : { x // x ≠ 0 } := ⟨ v, fun hv => (Basis.ne_zero (FiniteDimensional.finBasis ℝ { x // x ∈ pᗮ }) i) (Submodule.coe_eq_zero.mp hv) ⟩
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
v : E := ↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i)
v' : { x // x ≠ 0 } := { val := v, property := ⋯ }
⊢ ⟪↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i), x⟫_ℝ = 0
Theorem: Submodule_cutspace
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
p : Subspace ℝ E
x : E
hHi_ : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(FiniteDimensional.finBasis ℝ ↥pᗮ)), ⟪↑x_1, x⟫_ℝ = 0
y : E
hy : y ∈ pᗮ
i : Fin (FiniteDimensional.finrank ℝ ↥pᗮ)
v : E := ↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i)
v' : { x // x ≠ 0 } := { val := v, property := ⋯ }
⊢ ⟪↑((FiniteDimensional.finBasis ℝ ↥pᗮ) i), x⟫_ℝ = 0
Tactic:
exact hHi_ v' ⟨ i, rfl ⟩
Proof state after:
no goals
Theorem: hxSegBallInterSeg
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
⊢ ∀ (x1 x2 : E) (ε : ℝ),
    x ∈ openSegment ℝ x1 x2 ∧ ¬(x1 = x ∧ x2 = x) →
      0 < ε →
        ∃ x1' x2',
          x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Tactic:
rintro x1 x2 ε ⟨ hxseg, hne ⟩ hε
Proof state after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hxseg : x ∈ openSegment ℝ x1 x2
hne : ¬(x1 = x ∧ x2 = x)
hε : 0 < ε
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Theorem: hxSegBallInterSeg
Proof state before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hxseg : x ∈ openSegment ℝ x1 x2
hne : ¬(x1 = x ∧ x2 = x)
hε : 0 < ε
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Tactic:
push_neg at hne
Proof state after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hxseg : x ∈ openSegment ℝ x1 x2
hε : 0 < ε
hne : x1 = x → x2 ≠ x
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Theorem: hxSegBallInterSeg
Proof state before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hxseg : x ∈ openSegment ℝ x1 x2
hε : 0 < ε
hne : x1 = x → x2 ≠ x
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Tactic:
have hxseg' := hxseg
Proof state after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hxseg : x ∈ openSegment ℝ x1 x2
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Theorem: hxSegBallInterSeg
Proof state before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hxseg : x ∈ openSegment ℝ x1 x2
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Tactic:
rw [openSegment_eq_image', Set.mem_image] at hxseg
Proof state after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hxseg : ∃ x_1 ∈ Set.Ioo 0 1, x1 + x_1 • (x2 - x1) = x
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Theorem: hxSegBallInterSeg
Proof state before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hxseg : ∃ x_1 ∈ Set.Ioo 0 1, x1 + x_1 • (x2 - x1) = x
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Tactic:
rcases hxseg with ⟨ t, ht, htt ⟩
Proof state after:
case intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Theorem: hxSegBallInterSeg
Proof state before:
case intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Tactic:
let v := x2 - x1
Proof state after:
case intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Theorem: hxSegBallInterSeg
Proof state before:
case intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Tactic:
let t1 := (-(min t (ε/norm v)/2))
Proof state after:
case intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Theorem: hxSegBallInterSeg
Proof state before:
case intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Tactic:
let t2 := ((min (1-t) (ε/norm v))/2)
Proof state after:
case intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Theorem: hxSegBallInterSeg
Proof state before:
case intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Tactic:
use t1 • v + x
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
⊢ ∃ x2',
    x ∈ openSegment ℝ (t1 • v + x) x2' ∧
      segment ℝ (t1 • v + x) x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ x2' = x)
Theorem: hxSegBallInterSeg
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
⊢ ∃ x2',
    x ∈ openSegment ℝ (t1 • v + x) x2' ∧
      segment ℝ (t1 • v + x) x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ x2' = x)
Tactic:
use t2 • v + x
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
⊢ x ∈ openSegment ℝ (t1 • v + x) (t2 • v + x) ∧
    segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ t2 • v + x = x)
Theorem: hxSegBallInterSeg
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
⊢ x ∈ openSegment ℝ (t1 • v + x) (t2 • v + x) ∧
    segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ t2 • v + x = x)
Tactic:
have hx12 : x1 ≠ x2 := by
  intro h
  rw [←h, openSegment_same] at hxseg'
  exact (h.symm ▸ hne) (Set.eq_of_mem_singleton hxseg').symm (Set.eq_of_mem_singleton hxseg').symm
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
⊢ x ∈ openSegment ℝ (t1 • v + x) (t2 • v + x) ∧
    segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ t2 • v + x = x)
Theorem: hxSegBallInterSeg
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
⊢ x ∈ openSegment ℝ (t1 • v + x) (t2 • v + x) ∧
    segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ t2 • v + x = x)
Tactic:
have ht1pos: 0 < min t (ε / ‖x2 - x1‖) := lt_min ht.1 <| div_pos hε <| norm_sub_pos_iff.mpr (Ne.symm hx12)
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
⊢ x ∈ openSegment ℝ (t1 • v + x) (t2 • v + x) ∧
    segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ t2 • v + x = x)