Theorem: exercise6_1 (LeanCourse/Assignments/Assignment6.lean)

State before:
ι : Type u_1
α : Type u_2
p : ι → Prop
q : Prop
a b : α
L : Filter ι
F G : Filter α
hbF : ∀ᶠ (x : α) in F, x ≠ b
haG : ∀ᶠ (x : α) in G, x ≠ a
haF : pure a ≤ F
hbG : pure b ≤ G
⊢ (∀ᶠ (i : ι) in L, p i ↔ q) ↔ Tendsto (fun i => if p i then a else b) L (if q then F else G)
Tactic:
have hab : a ≠ b
State after:
case hab
ι : Type u_1
α : Type u_2
p : ι → Prop
q : Prop
a b : α
L : Filter ι
F G : Filter α
hbF : ∀ᶠ (x : α) in F, x ≠ b
haG : ∀ᶠ (x : α) in G, x ≠ a
haF : pure a ≤ F
hbG : pure b ≤ G
⊢ a ≠ b

ι : Type u_1
α : Type u_2
p : ι → Prop
q : Prop
a b : α
L : Filter ι
F G : Filter α
hbF : ∀ᶠ (x : α) in F, x ≠ b
haG : ∀ᶠ (x : α) in G, x ≠ a
haF : pure a ≤ F
hbG : pure b ≤ G
hab : a ≠ b
⊢ (∀ᶠ (i : ι) in L, p i ↔ q) ↔ Tendsto (fun i => if p i then a else b) L (if q then F else G)

State before:
ι : Type u_1
α : Type u_2
p : ι → Prop
q : Prop
a b : α
L : Filter ι
F G : Filter α
hbF : ∀ᶠ (x : α) in F, x ≠ b
haG : ∀ᶠ (x : α) in G, x ≠ a
haF : pure a ≤ F
hbG : pure b ≤ G
hab : a ≠ b
⊢ (∀ᶠ (i : ι) in L, p i ↔ q) ↔ Tendsto (fun i => if p i then a else b) L (if q then F else G)
Tactic:
rw [tendsto_iff_eventually]
State after:
ι : Type u_1
α : Type u_2
p : ι → Prop
q : Prop
a b : α
L : Filter ι
F G : Filter α
hbF : ∀ᶠ (x : α) in F, x ≠ b
haG : ∀ᶠ (x : α) in G, x ≠ a
haF : pure a ≤ F
hbG : pure b ≤ G
hab : a ≠ b
⊢ (∀ᶠ (i : ι) in L, p i ↔ q) ↔
    ∀ ⦃p_1 : α → Prop⦄, (∀ᶠ (y : α) in if q then F else G, p_1 y) → ∀ᶠ (x : ι) in L, p_1 (if p x then a else b)

State before:
ι : Type u_1
α : Type u_2
p : ι → Prop
q : Prop
a b : α
L : Filter ι
F G : Filter α
hbF : ∀ᶠ (x : α) in F, x ≠ b
haG : ∀ᶠ (x : α) in G, x ≠ a
haF : pure a ≤ F
hbG : pure b ≤ G
hab : a ≠ b
⊢ (∀ᶠ (i : ι) in L, p i ↔ q) ↔
    ∀ ⦃p_1 : α → Prop⦄, (∀ᶠ (y : α) in if q then F else G, p_1 y) → ∀ᶠ (x : ι) in L, p_1 (if p x then a else b)
Tactic:
sorry
State after:
no goals

State before:
case hab
ι : Type u_1
α : Type u_2
p : ι → Prop
q : Prop
a b : α
L : Filter ι
F G : Filter α
hbF : ∀ᶠ (x : α) in F, x ≠ b
haG : ∀ᶠ (x : α) in G, x ≠ a
haF : pure a ≤ F
hbG : pure b ≤ G
⊢ a ≠ b
Tactic:
sorry
State after:
no goals