awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L (if q then F else G)
⊢ ∀ᶠ (i : ι) in L, p i ↔ q
have pos : ∀ (hq : q), ∀ᶠ (i : ι) in L, p i ↔ q
Tactic: by_cases hq : q
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L (if q then F else G)
pos : ∀ (hq : q), ∀ᶠ (i : ι) in L, p i ↔ q
⊢ ∀ᶠ (i : ι) in L, p i ↔ q
have neg : ∀ (hq : ¬q), ∀ᶠ (i : ι) in L, p i ↔ q
Tactic: by_cases hq : q
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (hypothesis)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L (if q then F else G)
hq : q
⊢ ∀ᶠ (i : ι) in L, p i ↔ q
have h₁ : Tendsto (fun (i : ι) ↦ if p i then a else b) L F
Tactic: simp only [hq, ite_true] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : q
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L F
⊢ ∀ᶠ (i : ι) in L, p i ↔ q
have h₁ : ∀ (i : ι) (hi : Membership.mem (γ := Set ι) (Set.preimage (β := β) (fun (i : ι) ↦ if p i then a else b) {b}ᶜ) i),
  p i ↔ q
Tactic: filter_upwards [mem_map.mp (h hbF)] with i hi
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (hypothesis)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : q
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L F
i : ι
hi : Membership.mem (γ := Set ι) (Set.preimage (β := β) (fun (i : ι) ↦ if p i then a else b) {b}ᶜ) i
⊢ p i ↔ q
have hi₁ : p i ∧ ¬a = b
Tactic: simp only [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff,
        ite_eq_right_iff, not_forall, exists_prop] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : q
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L F
i : ι
hi : p i ∧ ¬a = b
⊢ p i ↔ q
have h₁ : p i → ¬a = b → (p i ↔ q)
Tactic: tauto
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : q
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L F
i : ι
hi : p i ∧ ¬a = b
h₁ h₂ : p i → ¬a = b → (p i ↔ q)
⊢ p i ↔ q
have h₃ : p i → ¬a = b → p i → q
Tactic: tauto
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : q
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L F
i : ι
hi : p i ∧ ¬a = b
h₁ h₂ : p i → ¬a = b → (p i ↔ q)
h₃ : p i → ¬a = b → p i → q
⊢ p i ↔ q
have h₄ : p i → ¬a = b → q → p i
Tactic: tauto
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (hypothesis)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L (if q then F else G)
hq : ¬q
⊢ ∀ᶠ (i : ι) in L, p i ↔ q
have h₁ : Tendsto (fun (i : ι) ↦ if p i then a else b) L G
Tactic: simp only [hq, ite_false] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : ¬q
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L G
⊢ ∀ᶠ (i : ι) in L, p i ↔ q
have h₁ : ∀ (i : ι) (hi : Membership.mem (γ := Set ι) (Set.preimage (β := β) (fun (i : ι) ↦ if p i then a else b) {a}ᶜ) i),
  p i ↔ q
Tactic: filter_upwards [mem_map.mp (h haG)] with i hi
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (hypothesis)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : ¬q
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L G
i : ι
hi : Membership.mem (γ := Set ι) (Set.preimage (β := β) (fun (i : ι) ↦ if p i then a else b) {a}ᶜ) i
⊢ p i ↔ q
have hi₁ : ¬p i ∧ ¬b = a
Tactic: simp only [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff,
        ite_eq_left_iff, not_forall, exists_prop] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : ¬q
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L G
i : ι
hi : ¬p i ∧ ¬b = a
⊢ p i ↔ q
have h₁ : ¬p i → ¬b = a → (p i ↔ q)
Tactic: tauto
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : ¬q
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L G
i : ι
hi : ¬p i ∧ ¬b = a
h₁ h₂ : ¬p i → ¬b = a → (p i ↔ q)
⊢ p i ↔ q
have h₃ : ¬p i → ¬b = a → p i → q
Tactic: tauto
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : ¬q
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L G
i : ι
hi : ¬p i ∧ ¬b = a
h₁ h₂ : ¬p i → ¬b = a → (p i ↔ q)
h₃ : ¬p i → ¬b = a → p i → q
⊢ p i ↔ q
have h₄ : ¬p i → ¬b = a → q → p i
Tactic: tauto
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
⊢ EventuallyEq.{u_3, u_4} (β := β) L (fun (x : ι) ↦ if q then a else b) fun (i : ι) ↦ if p i then a else b
have h₁ : ∀ (i : ι) (hi : p i ↔ q), (if q then a else b) = if p i then a else b
Tactic: filter_upwards [h] with i hi
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (hypothesis)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
⊢ Tendsto (fun (i : ι) ↦ if p i then a else b) L (if q then F else G)
have obs : EventuallyEq.{u_3, u_4} (β := β) L (fun (x : ι) ↦ if q then a else b) fun (i : ι) ↦ if p i then a else b
Tactic: have obs : (fun _ ↦ if q then a else b) =ᶠ[L] (fun i ↦ if p i then a else b) := by
      filter_upwards [h] with i hi
      simp only [hi]
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : EventuallyEq.{u_3, u_4} (β := β) L (fun (x : ι) ↦ if q then a else b) fun (i : ι) ↦ if p i then a else b
⊢ Tendsto (fun (i : ι) ↦ if p i then a else b) L (if q then F else G)
have mpr : Tendsto (fun (x : ι) ↦ if q then a else b) L (if q then F else G)
Tactic: apply Tendsto.congr' obs
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : EventuallyEq.{u_3, u_4} (β := β) L (fun (x : ι) ↦ if q then a else b) fun (i : ι) ↦ if p i then a else b
⊢ Tendsto (fun (x : ι) ↦ if q then a else b) L (if q then F else G)
have pos : ∀ (hq : q), Tendsto (fun (x : ι) ↦ if q then a else b) L (if q then F else G)
Tactic: by_cases hq : q
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : EventuallyEq.{u_3, u_4} (β := β) L (fun (x : ι) ↦ if q then a else b) fun (i : ι) ↦ if p i then a else b
pos : ∀ (hq : q), Tendsto (fun (x : ι) ↦ if q then a else b) L (if q then F else G)
⊢ Tendsto (fun (x : ι) ↦ if q then a else b) L (if q then F else G)
have neg : ∀ (hq : ¬q), Tendsto (fun (x : ι) ↦ if q then a else b) L (if q then F else G)
Tactic: by_cases hq : q
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : EventuallyEq.{u_3, u_4} (β := β) L (fun (x : ι) ↦ if q then a else b) fun (i : ι) ↦ if p i then a else b
hq : q
⊢ Tendsto (fun (x : ι) ↦ if q then a else b) L (if q then F else G)
have pos : Tendsto (fun (x : ι) ↦ a) L F
Tactic: simp only [hq, ite_true]
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : EventuallyEq.{u_3, u_4} (β := β) L (fun (x : ι) ↦ if q then a else b) fun (i : ι) ↦ if p i then a else b
hq : q
⊢ Tendsto (fun (x : ι) ↦ a) L F
have apply : LE.le (α := Filter β) (map (fun (x : ι) ↦ a) L) (𝓟 {a})
Tactic: apply le_trans _ haF
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : EventuallyEq.{u_3, u_4} (β := β) L (fun (x : ι) ↦ if q then a else b) fun (i : ι) ↦ if p i then a else b
hq : ¬q
⊢ Tendsto (fun (x : ι) ↦ if q then a else b) L (if q then F else G)
have neg : Tendsto (fun (x : ι) ↦ b) L G
Tactic: simp only [hq, ite_false]
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : EventuallyEq.{u_3, u_4} (β := β) L (fun (x : ι) ↦ if q then a else b) fun (i : ι) ↦ if p i then a else b
hq : ¬q
⊢ Tendsto (fun (x : ι) ↦ b) L G
have apply : LE.le (α := Filter β) (map (fun (x : ι) ↦ b) L) (𝓟 {b})
Tactic: apply le_trans _ hbG
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
x : α
⊢ Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
      (𝓝 (A.indicator (fun (x : α) ↦ b) x)) ↔
    ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
have refine_3 : ∀
  (heart :
    Tendsto (fun (i : ι) ↦ if (fun (i : ι) ↦ x ∈ As i) i then b else 0) L (if x ∈ A then 𝓝 b else 𝓝 0) ↔
      ∀ᶠ (i : ι) in L, (fun (i : ι) ↦ x ∈ As i) i ↔ x ∈ A),
  Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
      (𝓝 (A.indicator (fun (x : α) ↦ b) x)) ↔
    ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
Tactic: have heart := @tendsto_ite ι L β (fun i ↦ x ∈ As i) _ (x ∈ A) _ b 0 (𝓝 b) (𝓝 (0 : β))
                nhds_o nhds_b ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
x : α
refine_3 :
  ∀
    (heart :
      Tendsto (fun (i : ι) ↦ if (fun (i : ι) ↦ x ∈ As i) i then b else 0) L (if x ∈ A then 𝓝 b else 𝓝 0) ↔
        ∀ᶠ (i : ι) in L, (fun (i : ι) ↦ x ∈ As i) i ↔ x ∈ A),
    Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
        (𝓝 (A.indicator (fun (x : α) ↦ b) x)) ↔
      ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
      (𝓝 (A.indicator (fun (x : α) ↦ b) x)) ↔
    ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
have refine_1 : 𝓟 {b} ≤ 𝓝 b
Tactic: have heart := @tendsto_ite ι L β (fun i ↦ x ∈ As i) _ (x ∈ A) _ b 0 (𝓝 b) (𝓝 (0 : β))
                nhds_o nhds_b ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
x : α
refine_3 :
  ∀
    (heart :
      Tendsto (fun (i : ι) ↦ if (fun (i : ι) ↦ x ∈ As i) i then b else 0) L (if x ∈ A then 𝓝 b else 𝓝 0) ↔
        ∀ᶠ (i : ι) in L, (fun (i : ι) ↦ x ∈ As i) i ↔ x ∈ A),
    Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
        (𝓝 (A.indicator (fun (x : α) ↦ b) x)) ↔
      ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
refine_1 : 𝓟 {b} ≤ 𝓝 b
⊢ Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
      (𝓝 (A.indicator (fun (x : α) ↦ b) x)) ↔
    ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
have refine_2 : LE.le (α := Filter β) (𝓟 {0}) (𝓝 0)
Tactic: have heart := @tendsto_ite ι L β (fun i ↦ x ∈ As i) _ (x ∈ A) _ b 0 (𝓝 b) (𝓝 (0 : β))
                nhds_o nhds_b ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
x : α
heart :
  Tendsto (fun (i : ι) ↦ if (fun (i : ι) ↦ x ∈ As i) i then b else 0) L (if x ∈ A then 𝓝 b else 𝓝 0) ↔
    ∀ᶠ (i : ι) in L, (fun (i : ι) ↦ x ∈ As i) i ↔ x ∈ A
⊢ Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
      (𝓝 (A.indicator (fun (x : α) ↦ b) x)) ↔
    ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
have h : 𝓝 (A.indicator (fun (x : α) ↦ b) x) = if x ∈ A then 𝓝 b else 𝓝 0
Tactic: convert! heart
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
x : α
heart :
  Tendsto (fun (i : ι) ↦ if (fun (i : ι) ↦ x ∈ As i) i then b else 0) L (if x ∈ A then 𝓝 b else 𝓝 0) ↔
    ∀ᶠ (i : ι) in L, (fun (i : ι) ↦ x ∈ As i) i ↔ x ∈ A
⊢ 𝓝 (A.indicator (fun (x : α) ↦ b) x) = if x ∈ A then 𝓝 b else 𝓝 0
have pos : ∀ (hxA : x ∈ A), 𝓝 (A.indicator (fun (x : α) ↦ b) x) = if x ∈ A then 𝓝 b else 𝓝 0
Tactic: by_cases hxA : x ∈ A
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
x : α
heart :
  Tendsto (fun (i : ι) ↦ if (fun (i : ι) ↦ x ∈ As i) i then b else 0) L (if x ∈ A then 𝓝 b else 𝓝 0) ↔
    ∀ᶠ (i : ι) in L, (fun (i : ι) ↦ x ∈ As i) i ↔ x ∈ A
pos : ∀ (hxA : x ∈ A), 𝓝 (A.indicator (fun (x : α) ↦ b) x) = if x ∈ A then 𝓝 b else 𝓝 0
⊢ 𝓝 (A.indicator (fun (x : α) ↦ b) x) = if x ∈ A then 𝓝 b else 𝓝 0
have neg : ∀ (hxA : x ∉ A), 𝓝 (A.indicator (fun (x : α) ↦ b) x) = if x ∈ A then 𝓝 b else 𝓝 0
Tactic: by_cases hxA : x ∈ A
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
x : α
⊢ 𝓟 {b} ≤ 𝓝 b
have refine_1 : ∀ x ∈ 𝓝 b, b ∈ x
Tactic: simp only [principal_singleton, le_def, mem_pure]
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
x : α
⊢ LE.le (α := Filter β) (𝓟 {0}) (𝓝 0)
have refine_2 : ∀ (x : Set β), Membership.mem (γ := Filter β) (𝓝 0) x → 0 ∈ x
Tactic: simp only [principal_singleton, le_def, mem_pure]
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
x : α
⊢ Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
      (𝓝 (A.indicator (fun (x : α) ↦ b) x)) ↔
    ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
have refine_1 : 𝓟 {b} ≤ 𝓝 b
Tactic: classical
  have heart := @tendsto_ite ι L β (fun i ↦ x ∈ As i) _ (x ∈ A) _ b 0 (𝓝 b) (𝓝 (0 : β))
                nhds_o nhds_b ?_ ?_
  · convert! heart
    by_cases hxA : x ∈ A <;> simp [hxA]
  · simp only [principal_singleton, le_def, mem_pure]
    exact fun s s_nhds ↦ mem_of_mem_nhds s_nhds
  · simp only [principal_singleton, le_def, mem_pure]
    exact fun s s_nhds ↦ mem_of_mem_nhds s_nhds
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
x : α
refine_1 : 𝓟 {b} ≤ 𝓝 b
⊢ Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
      (𝓝 (A.indicator (fun (x : α) ↦ b) x)) ↔
    ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
have refine_2 : LE.le (α := Filter β) (𝓟 {0}) (𝓝 0)
Tactic: classical
  have heart := @tendsto_ite ι L β (fun i ↦ x ∈ As i) _ (x ∈ A) _ b 0 (𝓝 b) (𝓝 (0 : β))
                nhds_o nhds_b ?_ ?_
  · convert! heart
    by_cases hxA : x ∈ A <;> simp [hxA]
  · simp only [principal_singleton, le_def, mem_pure]
    exact fun s s_nhds ↦ mem_of_mem_nhds s_nhds
  · simp only [principal_singleton, le_def, mem_pure]
    exact fun s s_nhds ↦ mem_of_mem_nhds s_nhds
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
x : α
refine_1 : 𝓟 {b} ≤ 𝓝 b
refine_2 : LE.le (α := Filter β) (𝓟 {0}) (𝓝 0)
⊢ Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
      (𝓝 (A.indicator (fun (x : α) ↦ b) x)) ↔
    ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
have refine_3 : ∀
  (heart :
    Tendsto (fun (i : ι) ↦ if (fun (i : ι) ↦ x ∈ As i) i then b else 0) L (if x ∈ A then 𝓝 b else 𝓝 0) ↔
      ∀ᶠ (i : ι) in L, (fun (i : ι) ↦ x ∈ As i) i ↔ x ∈ A),
  Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
      (𝓝 (A.indicator (fun (x : α) ↦ b) x)) ↔
    ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
Tactic: classical
  have heart := @tendsto_ite ι L β (fun i ↦ x ∈ As i) _ (x ∈ A) _ b 0 (𝓝 b) (𝓝 (0 : β))
                nhds_o nhds_b ?_ ?_
  · convert! heart
    by_cases hxA : x ∈ A <;> simp [hxA]
  · simp only [principal_singleton, le_def, mem_pure]
    exact fun s s_nhds ↦ mem_of_mem_nhds s_nhds
  · simp only [principal_singleton, le_def, mem_pure]
    exact fun s s_nhds ↦ mem_of_mem_nhds s_nhds
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
⊢ Tendsto (β := (x : α) → β) (fun (i : ι) ↦ (As i).indicator fun (x : α) ↦ b) L (𝓝 (A.indicator fun (x : α) ↦ b)) ↔
    ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
have simp_rw : (∀ (x : α),
    Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
      (𝓝 (A.indicator (fun (x : α) ↦ b) x))) ↔
  ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
Tactic: simp_rw [tendsto_pi_nhds]
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
⊢ (∀ (x : α),
      Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
        (𝓝 (A.indicator (fun (x : α) ↦ b) x))) ↔
    ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
have h : ∀ (a : α),
  Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) a) L
      (𝓝 (A.indicator (fun (x : α) ↦ b) a)) ↔
    ∀ᶠ (i : ι) in L, a ∈ As i ↔ a ∈ A
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst_2 : T1Space β
b : β
inst_3 : NeZero b
x : α
⊢ Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
      (𝓝 (A.indicator (fun (x : α) ↦ b) x)) ↔
    ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
have nhds_b : {0}ᶜ ∈ 𝓝 b
Tactic: apply tendsto_indicator_const_apply_iff_eventually' _ b
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst_2 : T1Space β
b : β
inst_3 : NeZero b
x : α
nhds_b : {0}ᶜ ∈ 𝓝 b
⊢ Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
      (𝓝 (A.indicator (fun (x : α) ↦ b) x)) ↔
    ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
have nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
Tactic: apply tendsto_indicator_const_apply_iff_eventually' _ b
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst_2 : T1Space β
b : β
inst_3 : NeZero b
⊢ Tendsto (β := (x : α) → β) (fun (i : ι) ↦ (As i).indicator fun (x : α) ↦ b) L (𝓝 (A.indicator fun (x : α) ↦ b)) ↔
    ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
have nhds_b : {0}ᶜ ∈ 𝓝 b
Tactic: apply tendsto_indicator_const_iff_forall_eventually' _ b