Theorem: atInf_basis (Ray/Misc/AtInf.lean)

State before:
X : Type
inst✝ : Norm X
⊢ atInf.HasBasis (fun x => True) fun r => {x | r < ‖x‖}
Tactic:
apply Filter.hasBasis_iInf_principal
State after:
case h
X : Type
inst✝ : Norm X
⊢ Directed (fun x x_1 => x ≥ x_1) fun i => {x | i < ‖x‖}

State before:
case h
X : Type
inst✝ : Norm X
⊢ Directed (fun x x_1 => x ≥ x_1) fun i => {x | i < ‖x‖}
Tactic:
apply directed_of_isDirected_le
State after:
case h.H
X : Type
inst✝ : Norm X
⊢ ∀ ⦃i j : ℝ⦄, i ≤ j → {x | i < ‖x‖} ≥ {x | j < ‖x‖}

State before:
case h.H
X : Type
inst✝ : Norm X
⊢ ∀ ⦃i j : ℝ⦄, i ≤ j → {x | i < ‖x‖} ≥ {x | j < ‖x‖}
Tactic:
intro a b ab
State after:
case h.H
X : Type
inst✝ : Norm X
a b : ℝ
ab : a ≤ b
⊢ {x | a < ‖x‖} ≥ {x | b < ‖x‖}

State before:
case h.H
X : Type
inst✝ : Norm X
a b : ℝ
ab : a ≤ b
⊢ {x | a < ‖x‖} ≥ {x | b < ‖x‖}
Tactic:
simp only [ge_iff_le, le_eq_subset, setOf_subset_setOf]
State after:
case h.H
X : Type
inst✝ : Norm X
a b : ℝ
ab : a ≤ b
⊢ ∀ (a_1 : X), b < ‖a_1‖ → a < ‖a_1‖

State before:
case h.H
X : Type
inst✝ : Norm X
a b : ℝ
ab : a ≤ b
⊢ ∀ (a_1 : X), b < ‖a_1‖ → a < ‖a_1‖
Tactic:
intro x h
State after:
case h.H
X : Type
inst✝ : Norm X
a b : ℝ
ab : a ≤ b
x : X
h : b < ‖x‖
⊢ a < ‖x‖

State before:
case h.H
X : Type
inst✝ : Norm X
a b : ℝ
ab : a ≤ b
x : X
h : b < ‖x‖
⊢ a < ‖x‖
Tactic:
linarith
State after:
no goals