internlm/Lean-Github huggingface dataset:
Theorem: Set.merge_length
Proof state before:
case inl
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : isLE (compare h1 h2) = true
⊢ List.length (h1 :: merge t1 (h2 :: t2)) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Tactic:
rw [List.length_cons, merge_length t1 (h2 :: t2)]
Proof state after:
case inl
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : isLE (compare h1 h2) = true
⊢ Nat.succ (List.length t1 + List.length (h2 :: t2)) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Theorem: Set.merge_length
Proof state before:
case inl
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : isLE (compare h1 h2) = true
⊢ Nat.succ (List.length t1 + List.length (h2 :: t2)) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Tactic:
simp only [List.length_cons]
Proof state after:
case inl
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : isLE (compare h1 h2) = true
⊢ Nat.succ (List.length t1 + Nat.succ (List.length t2)) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Theorem: Set.merge_length
Proof state before:
case inl
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : isLE (compare h1 h2) = true
⊢ Nat.succ (List.length t1 + Nat.succ (List.length t2)) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Tactic:
omega
Proof state after:
no goals
Theorem: Set.merge_length
Proof state before:
case inr
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : ¬isLE (compare h1 h2) = true
⊢ List.length (h2 :: merge (h1 :: t1) t2) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Tactic:
rw [List.length_cons, merge_length (h1 :: t1) t2]
Proof state after:
case inr
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : ¬isLE (compare h1 h2) = true
⊢ Nat.succ (List.length (h1 :: t1) + List.length t2) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Theorem: Set.merge_length
Proof state before:
case inr
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : ¬isLE (compare h1 h2) = true
⊢ Nat.succ (List.length (h1 :: t1) + List.length t2) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Tactic:
simp only [List.length_cons]
Proof state after:
case inr
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : ¬isLE (compare h1 h2) = true
⊢ Nat.succ (Nat.succ (List.length t1) + List.length t2) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Theorem: Set.merge_length
Proof state before:
case inr
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : ¬isLE (compare h1 h2) = true
⊢ Nat.succ (Nat.succ (List.length t1) + List.length t2) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Tactic:
omega
Proof state after:
no goals
Theorem: length_backtrack
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
⊢ ∀ (tr : Trail α), List.length (backtrack tr) ≤ List.length tr
Tactic:
intro t
Proof state after:
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
t : Trail α
⊢ List.length (backtrack t) ≤ List.length t
Theorem: length_backtrack
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
t : Trail α
⊢ List.length (backtrack t) ≤ List.length t
Tactic:
induction t with
| nil => unfold backtrack; apply Nat.le_refl
| cons d ds ih =>
  simp [backtrack]
  cases d.decision == .Deduced
  . simp
  . simp; apply Nat.le_succ_of_le; assumption
Proof state after:
no goals
Theorem: length_backtrack
Proof state before:
case nil
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
⊢ List.length (backtrack []) ≤ List.length []
Tactic:
unfold backtrack
Proof state after:
case nil
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
⊢ List.length [] ≤ List.length []
Theorem: length_backtrack
Proof state before:
case nil
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
⊢ List.length [] ≤ List.length []
Tactic:
apply Nat.le_refl
Proof state after:
no goals
Theorem: length_backtrack
Proof state before:
case cons
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (backtrack (d :: ds)) ≤ List.length (d :: ds)
Tactic:
simp [backtrack]
Proof state after:
case cons
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if (d.decision == LitState.Deduced) = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)
Theorem: length_backtrack
Proof state before:
case cons
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if (d.decision == LitState.Deduced) = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)
Tactic:
cases d.decision == .Deduced
Proof state after:
case cons.false
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if false = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)

case cons.true
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if true = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)
Theorem: length_backtrack
Proof state before:
case cons.false
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if false = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)

case cons.true
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if true = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)
Tactic:
. simp
Proof state after:
case cons.true
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if true = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)
Theorem: length_backtrack
Proof state before:
case cons.true
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if true = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)
Tactic:
. simp; apply Nat.le_succ_of_le; assumption
Proof state after:
no goals
Theorem: length_backtrack
Proof state before:
case cons.false
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if false = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)
Tactic:
simp
Proof state after:
no goals
Theorem: length_backtrack
Proof state before:
case cons.true
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if true = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)
Tactic:
simp
Proof state after:
case cons.true
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (backtrack ds) ≤ Nat.succ (List.length ds)
Theorem: length_backtrack
Proof state before:
case cons.true
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (backtrack ds) ≤ Nat.succ (List.length ds)
Tactic:
apply Nat.le_succ_of_le
Proof state after:
case cons.true.h
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (backtrack ds) ≤ List.length ds
Theorem: length_backtrack
Proof state before:
case cons.true.h
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (backtrack ds) ≤ List.length ds
Tactic:
assumption
Proof state after:
no goals
Theorem: unitSphereDual_neg
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
⊢ ↑(-f) = -↑f
Tactic:
change (⟨-f.1, _ ⟩: {f : (NormedSpace.Dual ℝ E) // norm f = 1}).1 = -f.1
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
⊢ ↑{ val := -↑f, property := ⋯ } = -↑f
Theorem: unitSphereDual_neg
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
⊢ ↑{ val := -↑f, property := ⋯ } = -↑f
Tactic:
simp
Proof state after:
no goals
Theorem: unitSphereDual_surj
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ ∀ (f : { f // ‖f‖ = 1 }), Function.Surjective ⇑↑f
Tactic:
intro f
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
⊢ Function.Surjective ⇑↑f
Theorem: unitSphereDual_surj
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
⊢ Function.Surjective ⇑↑f
Tactic:
apply LinearMap.surjective_of_ne_zero
Proof state after:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
⊢ ↑↑f ≠ 0
Theorem: unitSphereDual_surj
Proof state before:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
⊢ ↑↑f ≠ 0
Tactic:
intro h
Proof state after:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
h : ↑↑f = 0
⊢ False
Theorem: unitSphereDual_surj
Proof state before:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
h : ↑↑f = 0
⊢ False
Tactic:
rw [← ContinuousLinearMap.coe_zero, ContinuousLinearMap.coe_inj] at h
Proof state after:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
h : ↑f = 0
⊢ False
Theorem: unitSphereDual_surj
Proof state before:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
h : ↑f = 0
⊢ False
Tactic:
have := h ▸ f.2
Proof state after:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
h : ↑f = 0
this : ‖0‖ = 1
⊢ False
Theorem: unitSphereDual_surj
Proof state before:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
h : ↑f = 0
this : ‖0‖ = 1
⊢ False
Tactic:
simp only [norm_zero, zero_ne_one] at this
Proof state after:
no goals
Theorem: Halfspace_mem
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ ∀ (x : E), x ∈ ↑H_ ↔ ↑H_.f x ≤ H_.α
Tactic:
intro x
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
⊢ x ∈ ↑H_ ↔ ↑H_.f x ≤ H_.α
Theorem: Halfspace_mem
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
⊢ x ∈ ↑H_ ↔ ↑H_.f x ≤ H_.α
Tactic:
rw [H_.h]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
⊢ x ∈ ⇑↑H_.f ⁻¹' {x | x ≤ H_.α} ↔ ↑H_.f x ≤ H_.α
Theorem: Halfspace_mem
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
⊢ x ∈ ⇑↑H_.f ⁻¹' {x | x ≤ H_.α} ↔ ↑H_.f x ≤ H_.α
Tactic:
rfl
Proof state after:
no goals
Theorem: Halfspace_convex
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Convex ℝ ↑H_
Tactic:
rw [H_.h]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Convex ℝ (⇑↑H_.f ⁻¹' {x | x ≤ H_.α})
Theorem: Halfspace_convex
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Convex ℝ (⇑↑H_.f ⁻¹' {x | x ≤ H_.α})
Tactic:
exact convex_halfspace_le (LinearMap.isLinear H_.f.1.1) H_.α
Proof state after:
no goals
Theorem: Halfspace_closed
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ IsClosed ↑H_
Tactic:
rw [H_.h]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ IsClosed (⇑↑H_.f ⁻¹' {x | x ≤ H_.α})
Theorem: Halfspace_closed
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ IsClosed (⇑↑H_.f ⁻¹' {x | x ≤ H_.α})
Tactic:
exact IsClosed.preimage (H_.f.1.cont) isClosed_Iic
Proof state after:
no goals
Theorem: Halfspace_span
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ affineSpan ℝ ↑H_ = ⊤
Tactic:
apply affineSpan_eq_top_of_nonempty_interior
Proof state after:
case hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Set.Nonempty (interior ((convexHull ℝ) ↑H_))
Theorem: Halfspace_span
Proof state before:
case hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Set.Nonempty (interior ((convexHull ℝ) ↑H_))
Tactic:
apply Set.Nonempty.mono (?_ : H_.f.1 ⁻¹' (Metric.ball (H_.α -1) (1/2)) ⊆ (interior ((convexHull ℝ) H_.S)))
Proof state after:
case hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Set.Nonempty (⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2))

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2) ⊆ interior ((convexHull ℝ) (Halfspace.S H_))
Theorem: Halfspace_span
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2) ⊆ interior ((convexHull ℝ) (Halfspace.S H_))
Tactic:
rw [IsOpen.subset_interior_iff (IsOpen.preimage (?_) Metric.isOpen_ball)]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2) ⊆ (convexHull ℝ) (Halfspace.S H_)

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f
Theorem: Halfspace_span
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2) ⊆ (convexHull ℝ) (Halfspace.S H_)

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f
Tactic:
apply subset_trans ?_ (subset_convexHull ℝ (SetLike.coe H_))
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2) ⊆ ↑H_

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f
Theorem: Halfspace_span
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2) ⊆ ↑H_

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f
Tactic:
intro x hx
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : x ∈ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2)
⊢ x ∈ ↑H_

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f
Theorem: Halfspace_span
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : x ∈ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2)
⊢ x ∈ ↑H_

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f
Tactic:
rw [Set.mem_preimage, Real.ball_eq_Ioo, Set.mem_Ioo] at hx
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : H_.α - 1 - 1 / 2 < ↑H_.f x ∧ ↑H_.f x < H_.α - 1 + 1 / 2
⊢ x ∈ ↑H_

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f
Theorem: Halfspace_span
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : H_.α - 1 - 1 / 2 < ↑H_.f x ∧ ↑H_.f x < H_.α - 1 + 1 / 2
⊢ x ∈ ↑H_

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f
Tactic:
rw [Halfspace_mem H_]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : H_.α - 1 - 1 / 2 < ↑H_.f x ∧ ↑H_.f x < H_.α - 1 + 1 / 2
⊢ ↑H_.f x ≤ H_.α

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f
Theorem: Halfspace_span
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : H_.α - 1 - 1 / 2 < ↑H_.f x ∧ ↑H_.f x < H_.α - 1 + 1 / 2
⊢ ↑H_.f x ≤ H_.α

E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f
Tactic:
linarith
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f
Theorem: Halfspace_span
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Continuous ⇑↑H_.f
Tactic:
exact H_.f.1.cont
Proof state after:
no goals
Theorem: Halfspace_span
Proof state before:
case hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Set.Nonempty (⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2))
Tactic:
cases' unitSphereDual_surj H_.f (H_.α -1) with x hx
Proof state after:
case hs.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : ↑H_.f x = H_.α - 1
⊢ Set.Nonempty (⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2))
Theorem: Halfspace_span
Proof state before:
case hs.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : ↑H_.f x = H_.α - 1
⊢ Set.Nonempty (⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2))
Tactic:
use x
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : ↑H_.f x = H_.α - 1
⊢ x ∈ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2)
Theorem: Halfspace_span
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : ↑H_.f x = H_.α - 1
⊢ x ∈ ⇑↑H_.f ⁻¹' Metric.ball (H_.α - 1) (1 / 2)
Tactic:
rw [Set.mem_preimage, Metric.mem_ball, dist_sub_eq_dist_add_right, hx, sub_add_cancel, dist_self]
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : ↑H_.f x = H_.α - 1
⊢ 0 < 1 / 2
Theorem: Halfspace_span
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
x : E
hx : ↑H_.f x = H_.α - 1
⊢ 0 < 1 / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: Halfspace_translation.S
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H_ : Halfspace E
⊢ ↑(Halfspace_translation x H_) = (fun x_1 => x_1 + x) '' ↑H_
Tactic:
ext y
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H_ : Halfspace E
y : E
⊢ y ∈ ↑(Halfspace_translation x H_) ↔ y ∈ (fun x_1 => x_1 + x) '' ↑H_
Theorem: Halfspace_translation.S
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H_ : Halfspace E
y : E
⊢ y ∈ ↑(Halfspace_translation x H_) ↔ y ∈ (fun x_1 => x_1 + x) '' ↑H_
Tactic:
rw [Halfspace_translation, Halfspace_mem, Set.image_add_right, Set.mem_preimage, ← sub_eq_add_neg,
  Halfspace_mem, ContinuousLinearMap.map_sub, sub_le_iff_le_add]
Proof state after:
no goals
Theorem: mem_Halfspace_translation
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H_ : Halfspace E
⊢ ∀ (y : E), y ∈ ↑(Halfspace_translation x H_) ↔ y - x ∈ ↑H_
Tactic:
intro y
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H_ : Halfspace E
y : E
⊢ y ∈ ↑(Halfspace_translation x H_) ↔ y - x ∈ ↑H_
Theorem: mem_Halfspace_translation
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H_ : Halfspace E
y : E
⊢ y ∈ ↑(Halfspace_translation x H_) ↔ y - x ∈ ↑H_
Tactic:
rw [Halfspace_translation.S, Set.image_add_right, Set.mem_preimage, sub_eq_add_neg]
Proof state after:
no goals
Theorem: Halfspace_translation.injective
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
⊢ Function.Injective fun x_1 => Halfspace_translation x x_1
Tactic:
intro H1 H2 h
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
h : (fun x_1 => Halfspace_translation x x_1) H1 = (fun x_1 => Halfspace_translation x x_1) H2
⊢ H1 = H2
Theorem: Halfspace_translation.injective
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
h : (fun x_1 => Halfspace_translation x x_1) H1 = (fun x_1 => Halfspace_translation x x_1) H2
⊢ H1 = H2
Tactic:
rw [SetLike.ext_iff]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
h : (fun x_1 => Halfspace_translation x x_1) H1 = (fun x_1 => Halfspace_translation x x_1) H2
⊢ ∀ (x : E), x ∈ H1 ↔ x ∈ H2
Theorem: Halfspace_translation.injective
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
h : (fun x_1 => Halfspace_translation x x_1) H1 = (fun x_1 => Halfspace_translation x x_1) H2
⊢ ∀ (x : E), x ∈ H1 ↔ x ∈ H2
Tactic:
intro y
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
H1 H2 : Halfspace E
h : (fun x_1 => Halfspace_translation x x_1) H1 = (fun x_1 => Halfspace_translation x x_1) H2
y : E
⊢ y ∈ H1 ↔ y ∈ H2