Theorem: FilterGame.Filter.as_basis_as_filter_eq_self (FilterGame/Solutions/Basis.lean)

State before:
α : Type u_1
f : Filter α
⊢ Basis.as_filter (as_basis f) = f
Tactic:
rw [eq_def]
State after:
α : Type u_1
f : Filter α
⊢ (Basis.as_filter (as_basis f)).sets = f.sets

State before:
α : Type u_1
f : Filter α
⊢ (Basis.as_filter (as_basis f)).sets = f.sets
Tactic:
apply Set.ext
State after:
case h
α : Type u_1
f : Filter α
⊢ ∀ (x : Set α), x ∈ (Basis.as_filter (as_basis f)).sets ↔ x ∈ f.sets

State before:
case h
α : Type u_1
f : Filter α
⊢ ∀ (x : Set α), x ∈ (Basis.as_filter (as_basis f)).sets ↔ x ∈ f.sets
Tactic:
intros x
State after:
case h
α : Type u_1
f : Filter α
x : Set α
⊢ x ∈ (Basis.as_filter (as_basis f)).sets ↔ x ∈ f.sets

State before:
case h
α : Type u_1
f : Filter α
x : Set α
⊢ x ∈ (Basis.as_filter (as_basis f)).sets ↔ x ∈ f.sets
Tactic:
simp_rw [← mem_def, Basis.mem_as_filter_def, mem_as_basis_def]
State after:
case h
α : Type u_1
f : Filter α
x : Set α
⊢ (∃ t, t ∈ f ∧ t ⊆ x) ↔ x ∈ f

State before:
case h
α : Type u_1
f : Filter α
x : Set α
⊢ (∃ t, t ∈ f ∧ t ⊆ x) ↔ x ∈ f
Tactic:
apply Iff.intro
State after:
case h.mp
α : Type u_1
f : Filter α
x : Set α
⊢ (∃ t, t ∈ f ∧ t ⊆ x) → x ∈ f

case h.mpr
α : Type u_1
f : Filter α
x : Set α
⊢ x ∈ f → ∃ t, t ∈ f ∧ t ⊆ x

State before:
case h.mp
α : Type u_1
f : Filter α
x : Set α
⊢ (∃ t, t ∈ f ∧ t ⊆ x) → x ∈ f

case h.mpr
α : Type u_1
f : Filter α
x : Set α
⊢ x ∈ f → ∃ t, t ∈ f ∧ t ⊆ x
Tactic:
. intros hx; have ⟨t, ht⟩ := hx; exact superset_mem ht.1 ht.2
State after:
case h.mpr
α : Type u_1
f : Filter α
x : Set α
⊢ x ∈ f → ∃ t, t ∈ f ∧ t ⊆ x

State before:
case h.mpr
α : Type u_1
f : Filter α
x : Set α
⊢ x ∈ f → ∃ t, t ∈ f ∧ t ⊆ x
Tactic:
. intros hx; exact ⟨x, hx, subset_rfl⟩
State after:
no goals

State before:
case h.mp
α : Type u_1
f : Filter α
x : Set α
⊢ (∃ t, t ∈ f ∧ t ⊆ x) → x ∈ f
Tactic:
intros hx
State after:
case h.mp
α : Type u_1
f : Filter α
x : Set α
hx : ∃ t, t ∈ f ∧ t ⊆ x
⊢ x ∈ f

State before:
case h.mp
α : Type u_1
f : Filter α
x : Set α
hx : ∃ t, t ∈ f ∧ t ⊆ x
⊢ x ∈ f
Tactic:
have ⟨t, ht⟩ := hx
State after:
case h.mp
α : Type u_1
f : Filter α
x : Set α
hx : ∃ t, t ∈ f ∧ t ⊆ x
t : Set α
ht : t ∈ f ∧ t ⊆ x
⊢ x ∈ f

State before:
case h.mp
α : Type u_1
f : Filter α
x : Set α
hx : ∃ t, t ∈ f ∧ t ⊆ x
t : Set α
ht : t ∈ f ∧ t ⊆ x
⊢ x ∈ f
Tactic:
exact superset_mem ht.1 ht.2
State after:
no goals

State before:
case h.mpr
α : Type u_1
f : Filter α
x : Set α
⊢ x ∈ f → ∃ t, t ∈ f ∧ t ⊆ x
Tactic:
intros hx
State after:
case h.mpr
α : Type u_1
f : Filter α
x : Set α
hx : x ∈ f
⊢ ∃ t, t ∈ f ∧ t ⊆ x

State before:
case h.mpr
α : Type u_1
f : Filter α
x : Set α
hx : x ∈ f
⊢ ∃ t, t ∈ f ∧ t ⊆ x
Tactic:
exact ⟨x, hx, subset_rfl⟩
State after:
no goals