Theorem: Filter.frequently_congr' (Sion/ForMathlib/Misc.lean)

State before:
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ (∃ᶠ (a : α) in f, p a) ↔ ∃ᶠ (a : α) in f, q a
Tactic:
dsimp only [Filter.Frequently]
State after:
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ (¬∀ᶠ (x : α) in f, ¬p x) ↔ ¬∀ᶠ (x : α) in f, ¬q x

State before:
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ (¬∀ᶠ (x : α) in f, ¬p x) ↔ ¬∀ᶠ (x : α) in f, ¬q x
Tactic:
rw [not_iff_not]
State after:
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ (∀ᶠ (x : α) in f, ¬p x) ↔ ∀ᶠ (x : α) in f, ¬q x

State before:
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ (∀ᶠ (x : α) in f, ¬p x) ↔ ∀ᶠ (x : α) in f, ¬q x
Tactic:
apply Filter.eventually_congr
State after:
case h
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ ∀ᶠ (x : α) in f, ¬p x ↔ ¬q x

State before:
case h
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ ∀ᶠ (x : α) in f, ¬p x ↔ ¬q x
Tactic:
simp_rw [not_iff_not]
State after:
case h
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ ∀ᶠ (x : α) in f, p x ↔ q x

State before:
case h
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ ∀ᶠ (x : α) in f, p x ↔ q x
Tactic:
exact h
State after:
no goals