Theorem: FilterGame.Basis.le_and_le_iff_filter_eq (FilterGame/Solutions/Order.lean)

State before:
α : Type u_1
b c : Basis α
⊢ b ≤' c ∧ c ≤' b ↔ as_filter b = as_filter c
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
b c : Basis α
⊢ b ≤' c ∧ c ≤' b → as_filter b = as_filter c

case mpr
α : Type u_1
b c : Basis α
⊢ as_filter b = as_filter c → b ≤' c ∧ c ≤' b

State before:
case mp
α : Type u_1
b c : Basis α
⊢ b ≤' c ∧ c ≤' b → as_filter b = as_filter c

case mpr
α : Type u_1
b c : Basis α
⊢ as_filter b = as_filter c → b ≤' c ∧ c ≤' b
Tactic:
. intros h
  apply le_antisymm
  . exact Basis.as_filter_le h.1
  . exact Basis.as_filter_le h.2
State after:
case mpr
α : Type u_1
b c : Basis α
⊢ as_filter b = as_filter c → b ≤' c ∧ c ≤' b

State before:
case mpr
α : Type u_1
b c : Basis α
⊢ as_filter b = as_filter c → b ≤' c ∧ c ≤' b
Tactic:
. suffices h : ∀ b c, Basis.as_filter b = Basis.as_filter c → b ≤' c
  . intros heq
    exact ⟨h _ _ heq, h _ _ heq.symm⟩
  intros b c hbc s hs
  have hs' := Basis.mem_as_filter_of_mem hs
  rw [← hbc] at hs'
  exact hs'
State after:
no goals

State before:
case mp
α : Type u_1
b c : Basis α
⊢ b ≤' c ∧ c ≤' b → as_filter b = as_filter c
Tactic:
intros h
State after:
case mp
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter b = as_filter c

State before:
case mp
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter b = as_filter c
Tactic:
apply le_antisymm
State after:
case mp.a
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter b ≤ as_filter c

case mp.a
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter c ≤ as_filter b

State before:
case mp.a
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter b ≤ as_filter c

case mp.a
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter c ≤ as_filter b
Tactic:
. exact Basis.as_filter_le h.1
State after:
case mp.a
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter c ≤ as_filter b

State before:
case mp.a
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter c ≤ as_filter b
Tactic:
. exact Basis.as_filter_le h.2
State after:
no goals

State before:
case mp.a
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter b ≤ as_filter c
Tactic:
exact Basis.as_filter_le h.1
State after:
no goals

State before:
case mp.a
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter c ≤ as_filter b
Tactic:
exact Basis.as_filter_le h.2
State after:
no goals

State before:
case mpr
α : Type u_1
b c : Basis α
⊢ as_filter b = as_filter c → b ≤' c ∧ c ≤' b
Tactic:
suffices h : ∀ b c, Basis.as_filter b = Basis.as_filter c → b ≤' c
State after:
case mpr
α : Type u_1
b c : Basis α
h : ∀ (b c : Basis ?m.10532), as_filter b = as_filter c → b ≤' c
⊢ as_filter b = as_filter c → b ≤' c ∧ c ≤' b

case h
α : Type u_1
b c : Basis α
⊢ ∀ (b c : Basis ?m.10532), as_filter b = as_filter c → b ≤' c

State before:
case mpr
α : Type u_1
b c : Basis α
h : ∀ (b c : Basis ?m.10532), as_filter b = as_filter c → b ≤' c
⊢ as_filter b = as_filter c → b ≤' c ∧ c ≤' b

case h
α : Type u_1
b c : Basis α
⊢ ∀ (b c : Basis ?m.10532), as_filter b = as_filter c → b ≤' c
Tactic:
. intros heq
  exact ⟨h _ _ heq, h _ _ heq.symm⟩
State after:
case h
α : Type u_1
b c : Basis α
⊢ ∀ (b c : Basis α), as_filter b = as_filter c → b ≤' c

State before:
case h
α : Type u_1
b c : Basis α
⊢ ∀ (b c : Basis α), as_filter b = as_filter c → b ≤' c
Tactic:
intros b c hbc s hs
State after:
case h
α : Type u_1
b✝ c✝ b c : Basis α
hbc : as_filter b = as_filter c
s : Set α
hs : s ∈ c
⊢ ∃ t, t ∈ b ∧ t ⊆ s

State before:
case h
α : Type u_1
b✝ c✝ b c : Basis α
hbc : as_filter b = as_filter c
s : Set α
hs : s ∈ c
⊢ ∃ t, t ∈ b ∧ t ⊆ s
Tactic:
have hs' := Basis.mem_as_filter_of_mem hs
State after:
case h
α : Type u_1
b✝ c✝ b c : Basis α
hbc : as_filter b = as_filter c
s : Set α
hs : s ∈ c
hs' : s ∈ as_filter c
⊢ ∃ t, t ∈ b ∧ t ⊆ s

State before:
case h
α : Type u_1
b✝ c✝ b c : Basis α
hbc : as_filter b = as_filter c
s : Set α
hs : s ∈ c
hs' : s ∈ as_filter c
⊢ ∃ t, t ∈ b ∧ t ⊆ s
Tactic:
rw [← hbc] at hs'
State after:
case h
α : Type u_1
b✝ c✝ b c : Basis α
hbc : as_filter b = as_filter c
s : Set α
hs : s ∈ c
hs' : s ∈ as_filter b
⊢ ∃ t, t ∈ b ∧ t ⊆ s

State before:
case h
α : Type u_1
b✝ c✝ b c : Basis α
hbc : as_filter b = as_filter c
s : Set α
hs : s ∈ c
hs' : s ∈ as_filter b
⊢ ∃ t, t ∈ b ∧ t ⊆ s
Tactic:
exact hs'
State after:
no goals

State before:
case mpr
α : Type u_1
b c : Basis α
h : ∀ (b c : Basis ?m.10532), as_filter b = as_filter c → b ≤' c
⊢ as_filter b = as_filter c → b ≤' c ∧ c ≤' b
Tactic:
intros heq
State after:
case mpr
α : Type u_1
b c : Basis α
h : ∀ (b c : Basis ?m.10532), as_filter b = as_filter c → b ≤' c
heq : as_filter b = as_filter c
⊢ b ≤' c ∧ c ≤' b

State before:
case mpr
α : Type u_1
b c : Basis α
h : ∀ (b c : Basis ?m.10532), as_filter b = as_filter c → b ≤' c
heq : as_filter b = as_filter c
⊢ b ≤' c ∧ c ≤' b
Tactic:
exact ⟨h _ _ heq, h _ _ heq.symm⟩
State after:
no goals