[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
⊢ EventuallyConst f l ↔ ∃ x, Tendsto f l (pure x)
[PROOFSTEP]
simp_rw [EventuallyConst, EventuallyEq, tendsto_pure]
[GOAL]
α : Type u_1
β : Sort ?u.805
l : Filter α
f : α → β
p : α → Prop
⊢ EventuallyConst p l ↔ (p =ᶠ[l] fun x => False) ∨ p =ᶠ[l] fun x => True
[PROOFSTEP]
simp only [EventuallyConst, Prop.exists_iff]
[GOAL]
α : Type u_1
β : Sort ?u.958
l : Filter α
f : α → β
p : α → Prop
⊢ EventuallyConst p l ↔ (∀ᶠ (x : α) in l, p x) ∨ ∀ᶠ (x : α) in l, ¬p x
[PROOFSTEP]
simp [eventuallyConst_pred', or_comm, EventuallyEq]
[GOAL]
α : Type u_2
β : Type u_1
l : Filter α
f : α → β
inst✝ : Nonempty β
⊢ EventuallyConst f ⊥
[PROOFSTEP]
simp [EventuallyConst, EventuallyEq]
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : Subsingleton α
inst✝ : Nonempty β
⊢ EventuallyConst f l
[PROOFSTEP]
rcases isEmpty_or_nonempty α with h | h
[GOAL]
case inl
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : Subsingleton α
inst✝ : Nonempty β
h : IsEmpty α
⊢ EventuallyConst f l
[PROOFSTEP]
simp only [l.filter_eq_bot_of_isEmpty, EventuallyConst.bot]
[GOAL]
case inr
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : Subsingleton α
inst✝ : Nonempty β
h : Nonempty α
⊢ EventuallyConst f l
[PROOFSTEP]
inhabit α
[GOAL]
case inr
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : Subsingleton α
inst✝ : Nonempty β
h : Nonempty α
inhabited_h : Inhabited α
⊢ EventuallyConst f l
[PROOFSTEP]
refine ⟨f default, eventually_of_forall fun x ↦ congr_arg f <| Subsingleton.elim _ _⟩
[GOAL]
α : Type u_2
β : Type u_1
l : Filter α
f : α → β
inst✝ : One β
s : Set α
c : β
hc : c ≠ 1
h : EventuallyConst (mulIndicator s fun x => c) l
⊢ EventuallyConst s l
[PROOFSTEP]
rw [eventuallyConst_set]
[GOAL]
α : Type u_2
β : Type u_1
l : Filter α
f : α → β
inst✝ : One β
s : Set α
c : β
hc : c ≠ 1
h : EventuallyConst (mulIndicator s fun x => c) l
⊢ (∀ᶠ (x : α) in l, x ∈ s) ∨ ∀ᶠ (x : α) in l, ¬x ∈ s
[PROOFSTEP]
rcases h with ⟨d, hd⟩
[GOAL]
case intro
α : Type u_2
β : Type u_1
l : Filter α
f : α → β
inst✝ : One β
s : Set α
c : β
hc : c ≠ 1
d : β
hd : (mulIndicator s fun x => c) =ᶠ[l] fun x => d
⊢ (∀ᶠ (x : α) in l, x ∈ s) ∨ ∀ᶠ (x : α) in l, ¬x ∈ s
[PROOFSTEP]
rcases eq_or_ne d 1 with rfl | hd₁
[GOAL]
case intro.inl
α : Type u_2
β : Type u_1
l : Filter α
f : α → β
inst✝ : One β
s : Set α
c : β
hc : c ≠ 1
hd : (mulIndicator s fun x => c) =ᶠ[l] fun x => 1
⊢ (∀ᶠ (x : α) in l, x ∈ s) ∨ ∀ᶠ (x : α) in l, ¬x ∈ s
[PROOFSTEP]
refine .inr <| hd.mono fun x hx ↦ ?_
[GOAL]
case intro.inl
α : Type u_2
β : Type u_1
l : Filter α
f : α → β
inst✝ : One β
s : Set α
c : β
hc : c ≠ 1
hd : (mulIndicator s fun x => c) =ᶠ[l] fun x => 1
x : α
hx : mulIndicator s (fun x => c) x = (fun x => 1) x
⊢ ¬x ∈ s
[PROOFSTEP]
simpa only [mulIndicator_apply_eq_one, hc] using hx
[GOAL]
case intro.inr
α : Type u_2
β : Type u_1
l : Filter α
f : α → β
inst✝ : One β
s : Set α
c : β
hc : c ≠ 1
d : β
hd : (mulIndicator s fun x => c) =ᶠ[l] fun x => d
hd₁ : d ≠ 1
⊢ (∀ᶠ (x : α) in l, x ∈ s) ∨ ∀ᶠ (x : α) in l, ¬x ∈ s
[PROOFSTEP]
refine .inl <| hd.mono fun x hx ↦ ?_
[GOAL]
case intro.inr
α : Type u_2
β : Type u_1
l : Filter α
f : α → β
inst✝ : One β
s : Set α
c : β
hc : c ≠ 1
d : β
hd : (mulIndicator s fun x => c) =ᶠ[l] fun x => d
hd₁ : d ≠ 1
x : α
hx : mulIndicator s (fun x => c) x = (fun x => d) x
⊢ x ∈ s
[PROOFSTEP]
simpa [hc] using ne_of_eq_of_ne hx hd₁
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
⊢ EventuallyConst f atTop ↔ ∃ i, ∀ (j : α), i ≤ j → f j = f i
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
⊢ EventuallyConst f atTop → ∃ i, ∀ (j : α), i ≤ j → f j = f i
[PROOFSTEP]
rintro ⟨c, hc⟩
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
c : β
hc : f =ᶠ[atTop] fun x => c
⊢ ∃ i, ∀ (j : α), i ≤ j → f j = f i
[PROOFSTEP]
rcases eventually_atTop.1 hc with ⟨i, hi⟩
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
c : β
hc : f =ᶠ[atTop] fun x => c
i : α
hi : ∀ (b : α), b ≥ i → f b = (fun x => c) b
⊢ ∃ i, ∀ (j : α), i ≤ j → f j = f i
[PROOFSTEP]
exact ⟨i, fun j hj ↦ (hi j hj).trans (hi i le_rfl).symm⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
⊢ (∃ i, ∀ (j : α), i ≤ j → f j = f i) → EventuallyConst f atTop
[PROOFSTEP]
rintro ⟨i, hi⟩
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
i : α
hi : ∀ (j : α), i ≤ j → f j = f i
⊢ EventuallyConst f atTop
[PROOFSTEP]
exact ⟨f i, eventually_atTop.2 ⟨i, hi⟩⟩
[GOAL]
α : Type u_1
β : Sort ?u.10621
l : Filter α
f✝ : α → β
f : ℕ → α
⊢ EventuallyConst f atTop ↔ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
[PROOFSTEP]
rw [eventuallyConst_atTop]
[GOAL]
α : Type u_1
β : Sort ?u.10621
l : Filter α
f✝ : α → β
f : ℕ → α
⊢ (∃ i, ∀ (j : ℕ), i ≤ j → f j = f i) ↔ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
[PROOFSTEP]
refine exists_congr fun n ↦ ⟨fun h m hm ↦ ?_, fun h m hm ↦ ?_⟩
[GOAL]
case refine_1
α : Type u_1
β : Sort ?u.10621
l : Filter α
f✝ : α → β
f : ℕ → α
n : ℕ
h : ∀ (j : ℕ), n ≤ j → f j = f n
m : ℕ
hm : n ≤ m
⊢ f (m + 1) = f m
[PROOFSTEP]
exact (h (m + 1) (hm.trans m.le_succ)).trans (h m hm).symm
[GOAL]
case refine_2
α : Type u_1
β : Sort ?u.10621
l : Filter α
f✝ : α → β
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
hm : n ≤ m
⊢ f m = f n
[PROOFSTEP]
induction m, hm using Nat.le_induction with
| base => rfl
| succ m hm ihm => exact (h m hm).trans ihm
[GOAL]
case refine_2
α : Type u_1
β : Sort ?u.10621
l : Filter α
f✝ : α → β
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
hm : n ≤ m
⊢ f m = f n
[PROOFSTEP]
induction m, hm using Nat.le_induction with
| base => rfl
| succ m hm ihm => exact (h m hm).trans ihm
[GOAL]
case refine_2.base
α : Type u_1
β : Sort ?u.10621
l : Filter α
f✝ : α → β
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
⊢ f n = f n
[PROOFSTEP]

| base => rfl
[GOAL]
case refine_2.base
α : Type u_1
β : Sort ?u.10621
l : Filter α
f✝ : α → β
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
⊢ f n = f n
[PROOFSTEP]
rfl
[GOAL]
case refine_2.succ
α : Type u_1
β : Sort ?u.10621
l : Filter α
f✝ : α → β
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m✝ m : ℕ
hm : n ≤ m
ihm : f m = f n
⊢ f (m + 1) = f n
[PROOFSTEP]

| succ m hm ihm => exact (h m hm).trans ihm
[GOAL]
case refine_2.succ
α : Type u_1
β : Sort ?u.10621
l : Filter α
f✝ : α → β
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m✝ m : ℕ
hm : n ≤ m
ihm : f m = f n
⊢ f (m + 1) = f n
[PROOFSTEP]
exact (h m hm).trans ihm
