α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝¹ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f✝ : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f✝ ↑a
hd : StronglyMeasurable fun a => f✝ ↑a
f : ℕ → α →ₛ β :=
  fun n =>
    {
      toFun := fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) },
      measurableSet_fiber' :=
        (_ :
          ∀ (x : β),
            MeasurableSet
              ((fun x =>
                  if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
                  else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
                {x})),
      finite_range' :=
        (_ :
          Set.Finite
            (range fun x =>
              if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
              else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })) }
y : α
⊢ Tendsto (fun n => ↑(f n) y) atTop (𝓝 (f✝ y))
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝¹ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f✝ : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f✝ ↑a
hd : StronglyMeasurable fun a => f✝ ↑a
f : ℕ → α →ₛ β :=
  fun n =>
    {
      toFun := fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) },
      measurableSet_fiber' :=
        (_ :
          ∀ (x : β),
            MeasurableSet
              ((fun x =>
                  if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
                  else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
                {x})),
      finite_range' :=
        (_ :
          Set.Finite
            (range fun x =>
              if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
              else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })) }
⊢ StronglyMeasurable f✝
refine' ⟨f, fun y => _⟩
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝¹ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f✝ : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f✝ ↑a
hd : StronglyMeasurable fun a => f✝ ↑a
f : ℕ → α →ₛ β :=
  fun n =>
    {
      toFun := fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) },
      measurableSet_fiber' :=
        (_ :
          ∀ (x : β),
            MeasurableSet
              ((fun x =>
                  if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
                  else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
                {x})),
      finite_range' :=
        (_ :
          Set.Finite
            (range fun x =>
              if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
              else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })) }
y : α
hy : y ∈ s
⊢ Tendsto (fun n => ↑(f n) y) atTop (𝓝 (f✝ y))

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝¹ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f✝ : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f✝ ↑a
hd : StronglyMeasurable fun a => f✝ ↑a
f : ℕ → α →ₛ β :=
  fun n =>
    {
      toFun := fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) },
      measurableSet_fiber' :=
        (_ :
          ∀ (x : β),
            MeasurableSet
              ((fun x =>
                  if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
                  else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
                {x})),
      finite_range' :=
        (_ :
          Set.Finite
            (range fun x =>
              if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
              else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })) }
y : α
hy : ¬y ∈ s
⊢ Tendsto (fun n => ↑(f n) y) atTop (𝓝 (f✝ y))
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝¹ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f✝ : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f✝ ↑a
hd : StronglyMeasurable fun a => f✝ ↑a
f : ℕ → α →ₛ β :=
  fun n =>
    {
      toFun := fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) },
      measurableSet_fiber' :=
        (_ :
          ∀ (x : β),
            MeasurableSet
              ((fun x =>
                  if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
                  else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
                {x})),
      finite_range' :=
        (_ :
          Set.Finite
            (range fun x =>
              if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
              else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })) }
y : α
⊢ Tendsto (fun n => ↑(f n) y) atTop (𝓝 (f✝ y))
by_cases hy : y ∈ s
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : α
hx : ¬x ∈ s
⊢ x ∈ t
simpa [hx] using h (mem_univ x)
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : β
⊢ MeasurableSet
    ((fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
      {x})
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
⊢ ∀ (x : β),
    MeasurableSet
      ((fun x =>
          if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
          else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
        {x})
intro x
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : β
⊢ (fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
      {x} =
    Subtype.val '' (↑(StronglyMeasurable.approx hc n) ⁻¹' {x}) ∪
      Subtype.val '' (↑(StronglyMeasurable.approx hd n) ⁻¹' {x}) \ s
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : β
⊢ MeasurableSet
    ((fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
      {x})
convert(hs.subtype_image ((hc.approx n).measurableSet_fiber x)).union
    ((ht.subtype_image ((hd.approx n).measurableSet_fiber x)).diff hs)
case h.e'_3.h
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : β
y : α
⊢ y ∈
      (fun x =>
          if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
          else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
        {x} ↔
    y ∈
      Subtype.val '' (↑(StronglyMeasurable.approx hc n) ⁻¹' {x}) ∪
        Subtype.val '' (↑(StronglyMeasurable.approx hd n) ⁻¹' {x}) \ s
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : β
⊢ (fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
      {x} =
    Subtype.val '' (↑(StronglyMeasurable.approx hc n) ⁻¹' {x}) ∪
      Subtype.val '' (↑(StronglyMeasurable.approx hd n) ⁻¹' {x}) \ s
ext1 y
case h.e'_3.h
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : β
y : α
⊢ (if hx : y ∈ s then ↑(StronglyMeasurable.approx hc n) { val := y, property := hx }
      else ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) }) =
      x ↔
    (∃ x_1, ↑(StronglyMeasurable.approx hc n) { val := y, property := (_ : y ∈ s) } = x) ∨
      (∃ x_1, ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) } = x) ∧ ¬y ∈ s
case h.e'_3.h
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : β
y : α
⊢ y ∈
      (fun x =>
          if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
          else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
        {x} ↔
    y ∈
      Subtype.val '' (↑(StronglyMeasurable.approx hc n) ⁻¹' {x}) ∪
        Subtype.val '' (↑(StronglyMeasurable.approx hd n) ⁻¹' {x}) \ s
simp only [mem_union, mem_preimage, mem_singleton_iff, mem_image, SetCoe.exists,
  Subtype.coe_mk, exists_and_right, exists_eq_right, mem_diff]
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : β
y : α
hy : y ∈ s
⊢ (if hx : y ∈ s then ↑(StronglyMeasurable.approx hc n) { val := y, property := hx }
      else ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) }) =
      x ↔
    (∃ x_1, ↑(StronglyMeasurable.approx hc n) { val := y, property := (_ : y ∈ s) } = x) ∨
      (∃ x_1, ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) } = x) ∧ ¬y ∈ s

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : β
y : α
hy : ¬y ∈ s
⊢ (if hx : y ∈ s then ↑(StronglyMeasurable.approx hc n) { val := y, property := hx }
      else ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) }) =
      x ↔
    (∃ x_1, ↑(StronglyMeasurable.approx hc n) { val := y, property := (_ : y ∈ s) } = x) ∨
      (∃ x_1, ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) } = x) ∧ ¬y ∈ s
case h.e'_3.h
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : β
y : α
⊢ (if hx : y ∈ s then ↑(StronglyMeasurable.approx hc n) { val := y, property := hx }
      else ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) }) =
      x ↔
    (∃ x_1, ↑(StronglyMeasurable.approx hc n) { val := y, property := (_ : y ∈ s) } = x) ∨
      (∃ x_1, ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) } = x) ∧ ¬y ∈ s
by_cases hy : y ∈ s
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : β
y : α
hy : y ∈ s
⊢ ↑(StronglyMeasurable.approx hc n) { val := y, property := hy } = x ↔
    (∃ x_1, ↑(StronglyMeasurable.approx hc n) { val := y, property := (_ : y ∈ s) } = x) ∨
      (∃ x_1, ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) } = x) ∧ ¬y ∈ s
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : β
y : α
hy : y ∈ s
⊢ (if hx : y ∈ s then ↑(StronglyMeasurable.approx hc n) { val := y, property := hx }
      else ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) }) =
      x ↔
    (∃ x_1, ↑(StronglyMeasurable.approx hc n) { val := y, property := (_ : y ∈ s) } = x) ∨
      (∃ x_1, ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) } = x) ∧ ¬y ∈ s
rw [dif_pos hy]
no goals
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : β
y : α
hy : y ∈ s
⊢ ↑(StronglyMeasurable.approx hc n) { val := y, property := hy } = x ↔
    (∃ x_1, ↑(StronglyMeasurable.approx hc n) { val := y, property := (_ : y ∈ s) } = x) ∨
      (∃ x_1, ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) } = x) ∧ ¬y ∈ s
simp only [hy, exists_true_left, not_true, and_false_iff, or_false_iff]
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : β
y : α
hy : ¬y ∈ s
⊢ ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) } = x ↔
    (∃ x_1, ↑(StronglyMeasurable.approx hc n) { val := y, property := (_ : y ∈ s) } = x) ∨
      (∃ x_1, ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) } = x) ∧ ¬y ∈ s
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : β
y : α
hy : ¬y ∈ s
⊢ (if hx : y ∈ s then ↑(StronglyMeasurable.approx hc n) { val := y, property := hx }
      else ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) }) =
      x ↔
    (∃ x_1, ↑(StronglyMeasurable.approx hc n) { val := y, property := (_ : y ∈ s) } = x) ∨
      (∃ x_1, ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) } = x) ∧ ¬y ∈ s
rw [dif_neg hy]
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : β
y : α
hy : ¬y ∈ s
A : y ∈ t
⊢ ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) } = x ↔
    (∃ x_1, ↑(StronglyMeasurable.approx hc n) { val := y, property := (_ : y ∈ s) } = x) ∨
      (∃ x_1, ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) } = x) ∧ ¬y ∈ s
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : β
y : α
hy : ¬y ∈ s
⊢ ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) } = x ↔
    (∃ x_1, ↑(StronglyMeasurable.approx hc n) { val := y, property := (_ : y ∈ s) } = x) ∨
      (∃ x_1, ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) } = x) ∧ ¬y ∈ s
have A : y ∈ t := by simpa [hy] using h (mem_univ y)
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : β
y : α
hy : ¬y ∈ s
A : y ∈ t
⊢ ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) } = x ↔
    (∃ x_1, ↑(StronglyMeasurable.approx hc n) { val := y, property := (_ : y ∈ s) } = x) ∨
      (∃ x_1, ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) } = x) ∧ ¬y ∈ s
simp only [A, hy, false_or_iff, IsEmpty.exists_iff, not_false_iff, and_true_iff,
  exists_true_left]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
x : β
y : α
hy : ¬y ∈ s
⊢ y ∈ t
simpa [hy] using h (mem_univ y)
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
⊢ (range fun x =>
      if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
      else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⊆
    range ↑(StronglyMeasurable.approx hc n) ∪ range ↑(StronglyMeasurable.approx hd n)
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
⊢ Set.Finite
    (range fun x =>
      if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
      else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })
apply ((hc.approx n).finite_range.union (hd.approx n).finite_range).subset
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
y : α
⊢ (fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })
      y ∈
    range ↑(StronglyMeasurable.approx hc n) ∪ range ↑(StronglyMeasurable.approx hd n)
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
⊢ (range fun x =>
      if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
      else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⊆
    range ↑(StronglyMeasurable.approx hc n) ∪ range ↑(StronglyMeasurable.approx hd n)
rintro - ⟨y, rfl⟩
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
y : α
⊢ (if hx : y ∈ s then ↑(StronglyMeasurable.approx hc n) { val := y, property := hx }
    else ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) }) ∈
    range ↑(StronglyMeasurable.approx hc n) ∪ range ↑(StronglyMeasurable.approx hd n)
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
y : α
⊢ (fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })
      y ∈
    range ↑(StronglyMeasurable.approx hc n) ∪ range ↑(StronglyMeasurable.approx hd n)
dsimp
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
y : α
hy : y ∈ s
⊢ (if hx : y ∈ s then ↑(StronglyMeasurable.approx hc n) { val := y, property := hx }
    else ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) }) ∈
    range ↑(StronglyMeasurable.approx hc n) ∪ range ↑(StronglyMeasurable.approx hd n)

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
y : α
hy : ¬y ∈ s
⊢ (if hx : y ∈ s then ↑(StronglyMeasurable.approx hc n) { val := y, property := hx }
    else ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) }) ∈
    range ↑(StronglyMeasurable.approx hc n) ∪ range ↑(StronglyMeasurable.approx hd n)
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
y : α
⊢ (if hx : y ∈ s then ↑(StronglyMeasurable.approx hc n) { val := y, property := hx }
    else ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) }) ∈
    range ↑(StronglyMeasurable.approx hc n) ∪ range ↑(StronglyMeasurable.approx hd n)
by_cases hy : y ∈ s
case pos.h
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
y : α
hy : y ∈ s
⊢ (if hx : y ∈ s then ↑(StronglyMeasurable.approx hc n) { val := y, property := hx }
    else ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) }) ∈
    range ↑(StronglyMeasurable.approx hc n)
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
y : α
hy : y ∈ s
⊢ (if hx : y ∈ s then ↑(StronglyMeasurable.approx hc n) { val := y, property := hx }
    else ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) }) ∈
    range ↑(StronglyMeasurable.approx hc n) ∪ range ↑(StronglyMeasurable.approx hd n)
left
case pos.h
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
y : α
hy : y ∈ s
⊢ ↑(StronglyMeasurable.approx hc n) { val := y, property := hy } ∈ range ↑(StronglyMeasurable.approx hc n)
case pos.h
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
y : α
hy : y ∈ s
⊢ (if hx : y ∈ s then ↑(StronglyMeasurable.approx hc n) { val := y, property := hx }
    else ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) }) ∈
    range ↑(StronglyMeasurable.approx hc n)
rw [dif_pos hy]
no goals
case pos.h
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
y : α
hy : y ∈ s
⊢ ↑(StronglyMeasurable.approx hc n) { val := y, property := hy } ∈ range ↑(StronglyMeasurable.approx hc n)
exact mem_range_self _
case neg.h
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
y : α
hy : ¬y ∈ s
⊢ (if hx : y ∈ s then ↑(StronglyMeasurable.approx hc n) { val := y, property := hx }
    else ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) }) ∈
    range ↑(StronglyMeasurable.approx hd n)
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
y : α
hy : ¬y ∈ s
⊢ (if hx : y ∈ s then ↑(StronglyMeasurable.approx hc n) { val := y, property := hx }
    else ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) }) ∈
    range ↑(StronglyMeasurable.approx hc n) ∪ range ↑(StronglyMeasurable.approx hd n)
right
case neg.h
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
y : α
hy : ¬y ∈ s
⊢ ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) } ∈ range ↑(StronglyMeasurable.approx hd n)
case neg.h
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
y : α
hy : ¬y ∈ s
⊢ (if hx : y ∈ s then ↑(StronglyMeasurable.approx hc n) { val := y, property := hx }
    else ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) }) ∈
    range ↑(StronglyMeasurable.approx hd n)
rw [dif_neg hy]
no goals
case neg.h
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f ↑a
hd : StronglyMeasurable fun a => f ↑a
n : ℕ
y : α
hy : ¬y ∈ s
⊢ ↑(StronglyMeasurable.approx hd n) { val := y, property := (_ : y ∈ t) } ∈ range ↑(StronglyMeasurable.approx hd n)
exact mem_range_self _
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝¹ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f✝ : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f✝ ↑a
hd : StronglyMeasurable fun a => f✝ ↑a
f : ℕ → α →ₛ β :=
  fun n =>
    {
      toFun := fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) },
      measurableSet_fiber' :=
        (_ :
          ∀ (x : β),
            MeasurableSet
              ((fun x =>
                  if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
                  else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
                {x})),
      finite_range' :=
        (_ :
          Set.Finite
            (range fun x =>
              if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
              else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })) }
y : α
hy : y ∈ s
⊢ (fun n => ↑(f n) y) = fun n => ↑(StronglyMeasurable.approx hc n) { val := y, property := hy }
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝¹ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f✝ : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f✝ ↑a
hd : StronglyMeasurable fun a => f✝ ↑a
f : ℕ → α →ₛ β :=
  fun n =>
    {
      toFun := fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) },
      measurableSet_fiber' :=
        (_ :
          ∀ (x : β),
            MeasurableSet
              ((fun x =>
                  if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
                  else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
                {x})),
      finite_range' :=
        (_ :
          Set.Finite
            (range fun x =>
              if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
              else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })) }
y : α
hy : y ∈ s
⊢ Tendsto (fun n => ↑(f n) y) atTop (𝓝 (f✝ y))
convert hc.tendsto_approx ⟨y, hy⟩ using 1
case h.e'_3.h
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝¹ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f✝ : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f✝ ↑a
hd : StronglyMeasurable fun a => f✝ ↑a
f : ℕ → α →ₛ β :=
  fun n =>
    {
      toFun := fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) },
      measurableSet_fiber' :=
        (_ :
          ∀ (x : β),
            MeasurableSet
              ((fun x =>
                  if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
                  else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
                {x})),
      finite_range' :=
        (_ :
          Set.Finite
            (range fun x =>
              if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
              else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })) }
y : α
hy : y ∈ s
n : ℕ
⊢ ↑(f n) y = ↑(StronglyMeasurable.approx hc n) { val := y, property := hy }
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝¹ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f✝ : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f✝ ↑a
hd : StronglyMeasurable fun a => f✝ ↑a
f : ℕ → α →ₛ β :=
  fun n =>
    {
      toFun := fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) },
      measurableSet_fiber' :=
        (_ :
          ∀ (x : β),
            MeasurableSet
              ((fun x =>
                  if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
                  else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
                {x})),
      finite_range' :=
        (_ :
          Set.Finite
            (range fun x =>
              if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
              else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })) }
y : α
hy : y ∈ s
⊢ (fun n => ↑(f n) y) = fun n => ↑(StronglyMeasurable.approx hc n) { val := y, property := hy }
ext1 n
no goals
case h.e'_3.h
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝¹ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f✝ : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f✝ ↑a
hd : StronglyMeasurable fun a => f✝ ↑a
f : ℕ → α →ₛ β :=
  fun n =>
    {
      toFun := fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) },
      measurableSet_fiber' :=
        (_ :
          ∀ (x : β),
            MeasurableSet
              ((fun x =>
                  if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
                  else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
                {x})),
      finite_range' :=
        (_ :
          Set.Finite
            (range fun x =>
              if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
              else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })) }
y : α
hy : y ∈ s
n : ℕ
⊢ ↑(f n) y = ↑(StronglyMeasurable.approx hc n) { val := y, property := hy }
simp only [dif_pos hy, SimpleFunc.apply_mk]
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝¹ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f✝ : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f✝ ↑a
hd : StronglyMeasurable fun a => f✝ ↑a
f : ℕ → α →ₛ β :=
  fun n =>
    {
      toFun := fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) },
      measurableSet_fiber' :=
        (_ :
          ∀ (x : β),
            MeasurableSet
              ((fun x =>
                  if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
                  else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
                {x})),
      finite_range' :=
        (_ :
          Set.Finite
            (range fun x =>
              if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
              else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })) }
y : α
hy : ¬y ∈ s
A : y ∈ t
⊢ Tendsto (fun n => ↑(f n) y) atTop (𝓝 (f✝ y))
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝¹ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f✝ : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f✝ ↑a
hd : StronglyMeasurable fun a => f✝ ↑a
f : ℕ → α →ₛ β :=
  fun n =>
    {
      toFun := fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) },
      measurableSet_fiber' :=
        (_ :
          ∀ (x : β),
            MeasurableSet
              ((fun x =>
                  if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
                  else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
                {x})),
      finite_range' :=
        (_ :
          Set.Finite
            (range fun x =>
              if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
              else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })) }
y : α
hy : ¬y ∈ s
⊢ Tendsto (fun n => ↑(f n) y) atTop (𝓝 (f✝ y))
have A : y ∈ t := by simpa [hy] using h (mem_univ y)
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝¹ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f✝ : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f✝ ↑a
hd : StronglyMeasurable fun a => f✝ ↑a
f : ℕ → α →ₛ β :=
  fun n =>
    {
      toFun := fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) },
      measurableSet_fiber' :=
        (_ :
          ∀ (x : β),
            MeasurableSet
              ((fun x =>
                  if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
                  else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
                {x})),
      finite_range' :=
        (_ :
          Set.Finite
            (range fun x =>
              if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
              else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })) }
y : α
hy : ¬y ∈ s
A : y ∈ t
⊢ (fun n => ↑(f n) y) = fun n => ↑(StronglyMeasurable.approx hd n) { val := y, property := A }
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝¹ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f✝ : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f✝ ↑a
hd : StronglyMeasurable fun a => f✝ ↑a
f : ℕ → α →ₛ β :=
  fun n =>
    {
      toFun := fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) },
      measurableSet_fiber' :=
        (_ :
          ∀ (x : β),
            MeasurableSet
              ((fun x =>
                  if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
                  else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
                {x})),
      finite_range' :=
        (_ :
          Set.Finite
            (range fun x =>
              if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
              else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })) }
y : α
hy : ¬y ∈ s
A : y ∈ t
⊢ Tendsto (fun n => ↑(f n) y) atTop (𝓝 (f✝ y))
convert hd.tendsto_approx ⟨y, A⟩ using 1
case h.e'_3.h
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝¹ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f✝ : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f✝ ↑a
hd : StronglyMeasurable fun a => f✝ ↑a
f : ℕ → α →ₛ β :=
  fun n =>
    {
      toFun := fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) },
      measurableSet_fiber' :=
        (_ :
          ∀ (x : β),
            MeasurableSet
              ((fun x =>
                  if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
                  else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
                {x})),
      finite_range' :=
        (_ :
          Set.Finite
            (range fun x =>
              if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
              else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })) }
y : α
hy : ¬y ∈ s
A : y ∈ t
n : ℕ
⊢ ↑(f n) y = ↑(StronglyMeasurable.approx hd n) { val := y, property := A }
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝¹ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f✝ : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f✝ ↑a
hd : StronglyMeasurable fun a => f✝ ↑a
f : ℕ → α →ₛ β :=
  fun n =>
    {
      toFun := fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) },
      measurableSet_fiber' :=
        (_ :
          ∀ (x : β),
            MeasurableSet
              ((fun x =>
                  if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
                  else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
                {x})),
      finite_range' :=
        (_ :
          Set.Finite
            (range fun x =>
              if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
              else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })) }
y : α
hy : ¬y ∈ s
A : y ∈ t
⊢ (fun n => ↑(f n) y) = fun n => ↑(StronglyMeasurable.approx hd n) { val := y, property := A }
ext1 n
no goals
case h.e'_3.h
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝¹ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f✝ : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f✝ ↑a
hd : StronglyMeasurable fun a => f✝ ↑a
f : ℕ → α →ₛ β :=
  fun n =>
    {
      toFun := fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) },
      measurableSet_fiber' :=
        (_ :
          ∀ (x : β),
            MeasurableSet
              ((fun x =>
                  if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
                  else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
                {x})),
      finite_range' :=
        (_ :
          Set.Finite
            (range fun x =>
              if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
              else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })) }
y : α
hy : ¬y ∈ s
A : y ∈ t
n : ℕ
⊢ ↑(f n) y = ↑(StronglyMeasurable.approx hd n) { val := y, property := A }
simp only [dif_neg hy, SimpleFunc.apply_mk]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.197809
ι : Type ?u.197812
inst✝¹ : Countable ι
f✝¹ g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f✝ : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a => f✝ ↑a
hd : StronglyMeasurable fun a => f✝ ↑a
f : ℕ → α →ₛ β :=
  fun n =>
    {
      toFun := fun x =>
        if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
        else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) },
      measurableSet_fiber' :=
        (_ :
          ∀ (x : β),
            MeasurableSet
              ((fun x =>
                  if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
                  else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) }) ⁻¹'
                {x})),
      finite_range' :=
        (_ :
          Set.Finite
            (range fun x =>
              if hx : x ∈ s then ↑(StronglyMeasurable.approx hc n) { val := x, property := hx }
              else ↑(StronglyMeasurable.approx hd n) { val := x, property := (_ : x ∈ t) })) }
y : α
hy : ¬y ∈ s
⊢ y ∈ t
simpa [hy] using h (mem_univ y)