mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
⊢ ∀ b ∈ s, b * μ (⇑f ⁻¹' {b}) ≠ 0 → ∃ a, ∃ (_ : a ∈ f.range) (_ : a * μ (⇑f ⁻¹' {a}) ≠ 0), a = b

Tactic:
intro b _ hb
    refine ⟨b, ?_, hb, rfl⟩
    rw [mem_range, ← preimage_singleton_nonempty]
    exact nonempty_of_measure_ne_zero (mul_ne_zero_iff.1 hb).2

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case inr
α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : α → α
hM : ∀ x ∈ s, x < M x
y : α → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x' < x
⊢ Function.onFun Disjoint (fun x ↦ Ioo x (y x)) x x'

Tactic:
refine disjoint_left.2 fun z hz h'z => ?_
      have : x ∈ interior s :=
        mem_interior.2 ⟨Ioo x' (y x'), h'y _ hx'.1, isOpen_Ioo, ⟨h', hz.1.trans h'z.2⟩⟩
      exact False.elim (hx.2 this)

Goal state after:
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
h_mon : Monotone fun n ↦ f (n + k)
h_bdd : BddAbove (range fun x ↦ f (x + k))
⊢ Tendsto f atTop (𝓝 (sSup (f '' Ici k)))

Tactic:
← tendsto_add_atTop_iff_nat k,

Goal state after:
f : ℕ → ℝ
k : ℕ
h_mon : Monotone fun n ↦ f (n + k)
h_bdd : BddAbove (range fun x ↦ f (x + k))
⊢ Tendsto (fun n ↦ f (n + k)) atTop (𝓝 (sSup (f '' Ici k)))
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
h_ant : Antitone fun n ↦ f (n + k)
h_bdd : BddBelow (range fun x ↦ f (x + k))
⊢ Tendsto f atTop (𝓝 (sInf (f '' Ici k)))

Tactic:
← tendsto_add_atTop_iff_nat k,

Goal state after:
f : ℕ → ℝ
k : ℕ
h_ant : Antitone fun n ↦ f (n + k)
h_bdd : BddBelow (range fun x ↦ f (x + k))
⊢ Tendsto (fun n ↦ f (n + k)) atTop (𝓝 (sInf (f '' Ici k)))
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Tendsto f' atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f (v n) x
⊢ AEMeasurable g μ

Tactic:
classical
  set aeSeqLim := fun x ↦ ite (x ∈ aeSeqSet h'f p) (g x) (⟨f (v 0) x⟩ : Nonempty ℝ≥0∞).some
  refine ⟨aeSeqLim, measurable_of_tendsto' atTop (aeSeq.measurable h'f p)
    (tendsto_pi_nhds.mpr fun x ↦ ?_), ?_⟩
  · unfold aeSeqLim
    simp_rw [aeSeq]
    split_ifs with hx
    · simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx]
      exact aeSeq.fun_prop_of_mem_aeSeqSet h'f hx
    · exact tendsto_const_nhds
  · exact (ite_ae_eq_of_measure_compl_zero g (fun x ↦ (⟨f (v 0) x⟩ : Nonempty ℝ≥0∞).some)
      (aeSeqSet h'f p) (aeSeq.measure_compl_aeSeqSet_eq_zero h'f hp)).symm

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_1
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α✝
mα✝ : MeasurableSpace α✝
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable fun p ↦ (↑p.1, ↑p.2).1 * (↑p.1, ↑p.2).2

pp: case refine_2
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α✝
mα✝ : MeasurableSpace α✝
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable fun r ↦ (⊥, ↑r).1 * (⊥, ↑r).2

pp: case refine_3
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α✝
mα✝ : MeasurableSpace α✝
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable fun r ↦ (⊤, ↑r).1 * (⊤, ↑r).2

pp: case refine_4
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α✝
mα✝ : MeasurableSpace α✝
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable fun r ↦ (↑r, ⊥).1 * (↑r, ⊥).2

pp: case refine_5
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α✝
mα✝ : MeasurableSpace α✝
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable fun r ↦ (↑r, ⊤).1 * (↑r, ⊤).2

Tactic:
· exact (measurable_fst.mul measurable_snd).coe_real_ereal

Goal state after:
case refine_2
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α✝
mα✝ : MeasurableSpace α✝
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable fun r ↦ (⊥, ↑r).1 * (⊥, ↑r).2

case refine_3
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α✝
mα✝ : MeasurableSpace α✝
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable fun r ↦ (⊤, ↑r).1 * (⊤, ↑r).2

case refine_4
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α✝
mα✝ : MeasurableSpace α✝
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable fun r ↦ (↑r, ⊥).1 * (↑r, ⊥).2

case refine_5
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α✝
mα✝ : MeasurableSpace α✝
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable fun r ↦ (↑r, ⊤).1 * (↑r, ⊤).2
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
⊢ Measurable fun x ↦ liminf (fun x_1 ↦ f x_1 x) v

Tactic:
have : Countable (Subtype p) := hv.countable
  rcases isEmpty_or_nonempty (Subtype p) with hp | hp
  · simp [hv.liminf_eq_sSup_iUnion_iInter]
  by_cases H : ∃ (j : Subtype p), s j = ∅
  · simp_rw [hv.liminf_eq_ite, if_pos H, measurable_const]
  simp_rw [hv.liminf_eq_ite, if_neg H]
  have : ∀ i, Countable (s i) := fun i ↦ countable_coe_iff.2 (hs i)
  let m : Subtype p → Set δ := fun j ↦ {x | BddBelow (range (fun (i : s j) ↦ f i x))}
  have m_meas : ∀ j, MeasurableSet (m j) :=
    fun j ↦ measurableSet_bddBelow_range (fun (i : s j) ↦ hf i)
  have mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j} := by
    rw [ofPred_forall]
    exact MeasurableSet.iInter (fun j ↦ (m_meas j).compl)
  refine measurable_const.piecewise mc_meas <| .iSup fun j ↦ ?_
  let reparam : δ → Subtype p → Subtype p := fun x ↦ liminfReparam (fun i ↦ f i x) s p
  let F0 : Subtype p → δ → α := fun j x ↦ ⨅ (i : s j), f i x
  have F0_meas : ∀ j, Measurable (F0 j) := fun j ↦ .iInf (fun (i : s j) ↦ hf i)
  set F1 : δ → α := fun x ↦ F0 (reparam x j) x with hF1
  change Measurable F1
  let g : ℕ → Subtype p := Classical.choose (exists_surjective_nat (Subtype p))
  have Z : ∀ x, ∃ n, x ∈ m (g n) ∨ ∀ k, x ∉ m k := by
    intro x
    by_cases! H : ∃ k, x ∈ m k
    · rcases H with ⟨k, hk⟩
      rcases Classical.choose_spec (exists_surjective_nat (Subtype p)) k with ⟨n, rfl⟩
      exact ⟨n, Or.inl hk⟩
    · exact ⟨0, Or.inr H⟩
  have : F1 = fun x ↦ if x ∈ m j then F0 j x else F0 (g (Nat.find (Z x))) x := by
    ext x
    have A : reparam x j = if x ∈ m j then j else g (Nat.find (Z x)) := rfl
    split_ifs with hjx
    · have : reparam x j = j := by rw [A, if_pos hjx]
      simp only [hF1, this]
    · have : reparam x j = g (Nat.find (Z x)) := by rw [A, if_neg hjx]
      simp only [hF1, this]
  rw [this]
  apply Measurable.piecewise (m_meas j) (F0_meas j)
  apply Measurable.find (fun n ↦ F0_meas (g n)) (fun n ↦ ?_)
  exact (m_meas (g n)).union mc_meas

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
motive : (α → ℝ≥0∞) → Prop
indicator : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (support f) (support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g)
iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun x ↦ ⨆ n, f n x
f : α → ℝ≥0∞
hf : Measurable f
⊢ motive f

Tactic:
refine Measurable.ennreal_induction (fun c s hs ↦ ?_) add iSup hf

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
motive : (α → ℝ≥0∞) → Prop
indicator : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (support f) (support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g)
iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun x ↦ ⨆ n, f n x
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ motive (s.indicator fun x ↦ c)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ ∫⁻ (x : α), 1 ∂μ = μ univ

Tactic:
by rw [lintegral_const, one_mul]

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
⊢ AEStronglyMeasurable (fun x ↦ g (f x)) μ ↔ AEStronglyMeasurable f μ

Tactic:
borelize β γ

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
⊢ AEStronglyMeasurable (fun x ↦ g (f x)) μ ↔ AEStronglyMeasurable f μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case neg.inr
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖(hf.approx n) x‖ = 0
h : c ≤ ‖(hf.approx n) x‖
⊢ ‖(hf.approx n) x‖⁻¹ * (‖(hf.approx n) x‖ * ‖c‖) ≤ c

Tactic:
← mul_assoc,

Goal state after:
case neg.inr
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖(hf.approx n) x‖ = 0
h : c ≤ ‖(hf.approx n) x‖
⊢ ‖(hf.approx n) x‖⁻¹ * ‖(hf.approx n) x‖ * ‖c‖ ≤ c
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
⊢ StronglyMeasurable f ↔ ∃ c, f = fun x ↦ c

Tactic:
by
  rcases isEmpty_or_nonempty α with hα | hα
  · simp [eq_iff_true_of_subsingleton]
  refine ⟨fun hf => ?_, fun hf_eq => ?_⟩
  · refine ⟨f hα.some, ?_⟩
    let fs := hf.approx
    have h_fs_tendsto : ∀ x, Tendsto (fun n => fs n x) atTop (𝓝 (f x)) := hf.tendsto_approx
    have : ∀ n, ∃ c, ∀ x, fs n x = c := fun n => SimpleFunc.simpleFunc_bot (fs n)
    let cs n := (this n).choose
    have h_cs_eq : ∀ n, ⇑(fs n) = fun _ => cs n := fun n => funext (this n).choose_spec
    conv at h_fs_tendsto => enter [x, 1, n]; rw [h_cs_eq]
    have h_tendsto : Tendsto cs atTop (𝓝 (f hα.some)) := h_fs_tendsto hα.some
    ext1 x
    exact tendsto_nhds_unique (h_fs_tendsto x) h_tendsto
  · obtain ⟨c, rfl⟩ := hf_eq
    exact stronglyMeasurable_const

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
x : α
hxt : x ∉ t
⊢ Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))

Tactic:
rw [funext fun n => h_fs_t_compl n x hxt, hft_zero x hxt]

Goal state after:
case neg
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
x : α
hxt : x ∉ t
⊢ Tendsto (fun n ↦ 0) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
hs : NullMeasurableSet s (μ.restrict t)
⊢ ∫⁻ (a : α) in t, s.indicator f a ∂μ = ∫⁻ (a : α) in s ∩ t, f a ∂μ

Tactic:
by
  rw [lintegral_indicator₀ hs, Measure.restrict_restrict₀ hs]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α → ℝ≥0∞
hgf : g ≤ f
hg_meas : Measurable g
hgsupp : μ (support g) < ∞
hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
⊢ Set.EqOn f (fun a ↦ f a - g a) (support g)ᶜ

Tactic:
by intro; simp_all

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
⊢ (StronglyMeasurable fun x ↦ g (f x)) ↔ StronglyMeasurable f

Tactic:
borelize β γ

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
⊢ (StronglyMeasurable fun x ↦ g (f x)) ↔ StronglyMeasurable f
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : StronglyMeasurable f
g : ↑sᶜ → β
hg : StronglyMeasurable g
hs : MeasurableSet s
⊢ StronglyMeasurable fun x ↦ if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩

Tactic:
refine ⟨fun n ↦ SimpleFunc.dite s hs (hf.approx n) (hg.approx n), fun x ↦ ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : StronglyMeasurable f
g : ↑sᶜ → β
hg : StronglyMeasurable g
hs : MeasurableSet s
x : α
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.dite s hs (hf.approx n) (hg.approx n)) n) x) atTop
    (𝓝 ((fun x ↦ if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩) x))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ∞
h_approx : ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n ↦ support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
n : ℕ
x : α
hxt : ¬∃ i, x ∈ T i
⊢ (fs n) x = 0

Tactic:
not_exists

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ∞
h_approx : ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n ↦ support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
n : ℕ
x : α
hxt : ∀ (x_1 : ℕ), x ∉ T x_1
⊢ (fs n) x = 0
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
t : Set α
inst✝ : SFinite μ
ht_subset : t ⊆ μ.sigmaFiniteSetᶜ
⊢ μ t = 0 ∨ μ t = ∞

Tactic:
by
  rw [or_iff_not_imp_left]
  exact measure_eq_top_of_subset_compl_sigmaFiniteSetWRT ht_subset

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D.Nonempty

pp: case right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ⊆ C

Tactic:
· rw [nonempty_iff_ne_empty]
    by_contra h
    rw [h, union_empty] at VD
    rw [VD] at hunc
    contradiction

Goal state after:
case right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ⊆ C
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
n : ℕ
h_meas : Measurable fun p ↦ u (↑p.1) p.2
⊢ Measurable (U n)

Tactic:
have :
    (fun p : ι × α => u (t_sf n p.fst) p.snd) =
      (fun p : ↥(t_sf n).range × α => u p.fst p.snd) ∘ fun p : ι × α =>
        (⟨t_sf n p.fst, SimpleFunc.mem_range_self _ _⟩, p.snd) :=
    rfl

Goal state after:
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
n : ℕ
h_meas : Measurable fun p ↦ u (↑p.1) p.2
this : (fun p ↦ u ((t_sf n) p.1) p.2) = (fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨(t_sf n) p.1, ⋯⟩, p.2)
⊢ Measurable (U n)
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ≥0
a : ℝ≥0
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖₊ ≤ g i
⊢ ‖∑' (i : ι), f i‖₊ ≤ a

Tactic:
simp only [← NNReal.coe_le_coe, ← NNReal.hasSum_coe, coe_nnnorm] at *

Goal state after:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ≥0
a : ℝ≥0
hg : HasSum (fun a ↦ ↑(g a)) ↑a
h : ∀ (i : ι), ‖f i‖ ≤ ↑(g i)
⊢ ‖∑' (i : ι), f i‖ ≤ ↑a
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
n : ℕ
h_str_meas : StronglyMeasurable fun p ↦ u (↑p.1) p.2
⊢ StronglyMeasurable (U n)

Tactic:
have :
    (fun p : ι × α => u (t_sf n p.fst) p.snd) =
      (fun p : ↥(t_sf n).range × α => u p.fst p.snd) ∘ fun p : ι × α =>
        (⟨t_sf n p.fst, SimpleFunc.mem_range_self _ _⟩, p.snd) :=
    rfl

Goal state after:
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
n : ℕ
h_str_meas : StronglyMeasurable fun p ↦ u (↑p.1) p.2
this : (fun p ↦ u ((t_sf n) p.1) p.2) = (fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨(t_sf n) p.1, ⋯⟩, p.2)
⊢ StronglyMeasurable (U n)
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → x ∈ s → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ ↑(K' x hx) * edist x y
t : Finset ↑s
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x) (ε ↑x ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : ↑s
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z) (ε ↑z ⋯ / 2)
hy' : y ∉ ball (↑z) (ε ↑z ⋯)
⊢ edist (↑z) y ≤ edist x ↑z + edist x y

Tactic:
exact edist_triangle_left z.1 y x

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case inr
x : ℝ
h₀ : 0 ≤ x
⊢ ↑(σ (projIcc 0 1 ⋯ x)) = ↑(projIcc 0 1 ⋯ (1 - x))

Tactic:
· rcases le_total x 1 with h₁ | h₁
    · lift x to I using ⟨h₀, h₁⟩
      simp_rw [← coe_symm_eq, projIcc_val]
    · simp [projIcc_of_le_left, projIcc_of_right_le, h₁]

Goal state after: