mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inl
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hβ : CountableOrCountablyGenerated β γ
hα : Countable α
⊢ CountableOrCountablyGenerated (α × β) γ

Tactic:
rcases hβ with (hβ | hβ)

Goal state after:
case inl.inl
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hα : Countable α
hβ : Countable β
⊢ CountableOrCountablyGenerated (α × β) γ

case inl.inr
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hα : Countable α
hβ : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (α × β) γ
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inr
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hβ : CountableOrCountablyGenerated β γ
hα : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (α × β) γ

Tactic:
rcases hβ with (hβ | hβ)

Goal state after:
case inr.inl
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hα : CountablyGenerated γ
hβ : Countable β
⊢ CountableOrCountablyGenerated (α × β) γ

case inr.inr
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hα hβ : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (α × β) γ
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
⊢ ∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᵐ[μ] g

Tactic:
let g : α → β := piecewise s (fun _ => h₀.some) (H.mk f)

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
⊢ ∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᵐ[μ] g
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : atTop.IsCountablyGenerated
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
⊢ Ioi x = ⋃ n, Ioc x (u n)

Tactic:
iUnion_Ioc_eq_Ioi_self_iff.mpr _

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : atTop.IsCountablyGenerated
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
⊢ Ioi x = Ioi x

α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : atTop.IsCountablyGenerated
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
⊢ ∀ (x_1 : α), x < x_1 → ∃ i, x_1 ≤ u i
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
mem_C : ∀ {i : ι}, i ∈ F → ∀ {C : Finset ι} {x : α}, x ∈ P C → x ∈ s i → i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι}, C₁ ∈ Cs → ∀ {x : α}, x ∈ P C₁ ∩ P C₂ → C₁ ⊆ C₂
⊢ ∑ C ∈ Cs, #({a ∈ F | a ∈ C}) • (μ.restrict (P C)) t ≤ ∑ C ∈ Cs, M • (μ.restrict (P C)) t

Tactic:
by
      refine sum_le_sum fun C hC ↦ ?_
      by_cases hPC : P C = ∅
      · simp [hPC]
      have hCM : (C : Set ι).encard ≤ M :=
        have ⟨x, hx⟩ := Set.nonempty_iff_ne_empty.mpr hPC
        (encard_mono (mem_iInter₂.mp hx.1)).trans (hs x)
      exact nsmul_le_nsmul_left zero_le <| calc {a ∈ F | a ∈ C}.card
        _ ≤ C.card := card_mono <| fun i hi ↦ (F.mem_filter.mp hi).2
        _ = (C : Set ι).ncard := (ncard_coe_finset C).symm
        _ ≤ M := ENat.toNat_le_of_le_natCast hCM

Goal state after:
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst✝¹] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst✝¹] (g' n) ⊆ ↑(g n)
⊢ t = ⋂ i, closure[inst✝¹] (g' i)

Tactic:
apply (subset_iInter fun n ↦ (clt_sub_g' n).trans subset_closure).antisymm

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst✝¹] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst✝¹] (g' n) ⊆ ↑(g n)
⊢ ⋂ i, closure[inst✝¹] (g' i) ⊆ t
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
⊢ MeasurableSet s

Tactic:
have huopen : IsOpen u := isOpen_biUnion fun _ _ => isOpen_biUnion fun _ _ => isOpen_Ioo

Goal state after:
α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen[inst✝³] u
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: case h₁
α : Type u_1
γ : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst✝³] t
u : Set α
u_open : IsOpen[inst✝⁶] u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ MeasurableSet (u ∩ s)

Tactic:
exact u_open.measurableSet.inter hs

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
fin : hausdorffEDist s t ≠ ∞
hs : s.Nonempty
⊢ s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty

Tactic:
exact Or.inr ⟨hs, nonempty_of_hausdorffEDist_ne_top hs fin⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case left
α : Type u
inst✝ : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
i : ι
x : α
hx : x ∈ s i
⊢ infEDist x (t i) ≤ max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i))

Tactic:
exact le_max_of_le_left <| le_iSup₂_of_le x hx le_rfl

Goal state after:
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
E : Set α
δ δ' : ℝ
hδ₀ : 0 < δ'
hδδ' : δ < δ'
⊢ cthickening δ E ⊆ ⋃ x ∈ E, closedBall x δ'

Tactic:
refine (cthickening_subset_thickening' hδ₀ hδδ' E).trans fun x hx => ?_
  obtain ⟨y, hy₁, hy₂⟩ := mem_thickening_iff.mp hx
  exact mem_iUnion₂.mpr ⟨y, hy₁, hy₂.le⟩

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

Goal state before:
pp: case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ ν (Iic a) ≠ ∞

Tactic:
rw [← h a]

Goal state after:
case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ μ (Iic a) ≠ ∞
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
k : ℕ
hk : i k ≤ f a
⊢ i k ≤ ⨆ n, (approx i f n) a

Tactic:
refine le_iSup_of_le (k + 1) ?_

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
k : ℕ
hk : i k ≤ f a
⊢ i k ≤ (approx i f (k + 1)) a
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: K : Subfield ℝ
hc : IsClosed ↑K
⊢ ↑K = univ

Tactic:
← hc.closure_eq

Goal state after:
K : Subfield ℝ
hc : IsClosed ↑K
⊢ closure ↑K = univ
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
h_mon : MonotoneOn f (Ici k)
h_bdd : BddAbove (f '' Ici k)
⊢ Tendsto f atTop (𝓝 (sSup (f '' Ici k)))

Tactic:
rw [← range_add_eq_image_Ici] at h_bdd

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

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
h_ant : AntitoneOn f (Ici k)
h_bdd : BddBelow (f '' Ici k)
⊢ Tendsto f atTop (𝓝 (sInf (f '' Ici k)))

Tactic:
rw [← range_add_eq_image_Ici] at h_bdd

Goal state after:
f : ℕ → ℝ
k : ℕ
h_ant : AntitoneOn f (Ici k)
h_bdd : BddBelow (range fun x ↦ f (x + k))
⊢ Tendsto f atTop (𝓝 (sInf (f '' Ici k)))
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_ant : AntitoneOn f (Ici k)
h_bdd : BddBelow (f '' Ici k)
⊢ IsGLB (f '' Ici k) x

Tactic:
by
  rw [tendsto_nhds_unique h_tto
    (Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici h_ant h_bdd)]
  exact isGLB_csInf (image_nonempty.mpr nonempty_Ici) h_bdd

Goal state after:
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: case refine_1
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : {b}ᶜ ∈ 𝓝 0
x : α
⊢ ∀ x ∈ 𝓝 b, b ∈ x

Tactic:
exact fun s s_nhds ↦ mem_of_mem_nhds s_nhds

Goal state after:
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: case refine_2
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : {b}ᶜ ∈ 𝓝 0
x : α
⊢ ∀ x ∈ 𝓝 0, 0 ∈ x

Tactic:
exact fun s s_nhds ↦ mem_of_mem_nhds s_nhds

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

Goal state before:
pp: case empty
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
f : α →ₛ γ
h : range ⇑f ⊆ {0}
⊢ motive f

Tactic:
range_subset_singleton

Goal state after:
case empty
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
f : α →ₛ γ
h : ⇑f = Function.const α 0
⊢ motive f
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case empty
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
f : α →ₛ γ
h : range ⇑f ⊆ {c}
⊢ P f

Tactic:
range_subset_singleton

Goal state after:
case empty
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
f : α →ₛ γ
h : ⇑f = Function.const α c
⊢ P f
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: case refine_1
α : 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 γ
H : AEStronglyMeasurable (fun x ↦ g (f x)) μ
G : β → ↑(range g) := rangeFactorization g
hG : IsClosedEmbedding G
⊢ AEMeasurable f μ

Tactic:
have : AEMeasurable (G ∘ f) μ := AEMeasurable.subtype_mk H.aemeasurable

Goal state after:
case refine_1
α : 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 γ
H : AEStronglyMeasurable (fun x ↦ g (f x)) μ
G : β → ↑(range g) := rangeFactorization g
hG : IsClosedEmbedding G
this : AEMeasurable (G ∘ f) μ
⊢ AEMeasurable f μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
φ : α →ₛ ℝ≥0
hle : ∀ (x : α), ↑(φ x) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
x : α
⊢ ↑((φ + (ψ - φ)) x) ≤ max ↑(φ x) ↑(ψ x)

Tactic:
simp only [SimpleFunc.add_apply, SimpleFunc.sub_apply, add_tsub_eq_max]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
φ : α →ₛ ℝ≥0
hle : ∀ (x : α), ↑(φ x) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb : ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
x : α
⊢ ↑(max (φ x) (ψ x)) ≤ max ↑(φ x) ↑(ψ x)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), (fs n) x = c
cs : ℕ → β := fun n ↦ ⋯.choose
h_fs_tendsto : ∀ (x : α), Tendsto (fun n ↦ (fun x ↦ cs n) x) atTop (𝓝 (f x))
h_cs_eq : ∀ (n : ℕ), ⇑(fs n) = fun x ↦ cs n
h_tendsto : Tendsto cs atTop (𝓝 (f hα.some))
x : α
⊢ f x = f hα.some

Tactic:
exact tendsto_nhds_unique (h_fs_tendsto x) h_tendsto

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
G₀ : Type u_7
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : MulAction G₀ β
inst✝³ : TopologicalSpace G₀
inst✝² : ContinuousInv₀ G₀
inst✝¹ : MetrizableSpace G₀
inst✝ : ContinuousSMul G₀ β
c : α → G₀
hc : AEStronglyMeasurable c μ
hc0 : ∀ᵐ (x : α) ∂μ, c x ≠ 0
⊢ AEStronglyMeasurable (fun x ↦ c x • f x) μ ↔ AEStronglyMeasurable f μ

Tactic:
refine ⟨fun h => (hc.fun_inv₀.fun_smul h).congr ?_, fun h => hc.fun_smul h⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
G₀ : Type u_7
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : MulAction G₀ β
inst✝³ : TopologicalSpace G₀
inst✝² : ContinuousInv₀ G₀
inst✝¹ : MetrizableSpace G₀
inst✝ : ContinuousSMul G₀ β
c : α → G₀
hc : AEStronglyMeasurable c μ
hc0 : ∀ᵐ (x : α) ∂μ, c x ≠ 0
h : AEStronglyMeasurable (fun x ↦ c x • f x) μ
⊢ (fun i ↦ (c i)⁻¹ • c i • f i) =ᵐ[μ] f
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs : {a | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧ MeasurableSet s ∧ μ s = 0
g : ℕ → α → ℝ≥0∞ := fun n a ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
⊢ ∫⁻ (a : α), ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
calc
    ∫⁻ a, ⨆ n, f n a ∂μ = ∫⁻ a, ⨆ n, g n a ∂μ :=
      lintegral_congr_ae <| g_eq_f.mono fun a ha => by simp only [ha]
    _ = ⨆ n, ∫⁻ a, g n a ∂μ :=
      (lintegral_iSup (fun n => measurable_const.piecewise hs.2.1 (hf n))
        (monotone_nat_of_le_succ fun n a => ?_))
    _ = ⨆ n, ∫⁻ a, f n a ∂μ := by simp only [lintegral_congr_ae (g_eq_f.mono fun _a ha => ha _)]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs : {a | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧ MeasurableSet s ∧ μ s = 0
g : ℕ → α → ℝ≥0∞ := fun n a ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
n : ℕ
a : α
⊢ g n a ≤ g (n + 1) a
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h_le : f ≤ᵐ[μ] g
h : ∃ᵐ (x : α) ∂μ, f x ≠ g x
⊢ ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ

Tactic:
contrapose! h

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h_le : f ≤ᵐ[μ] g
h : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
⊢ ∀ᵐ (x : α) ∂μ, f x = g x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∉ aeSeqSet hf p
⊢ aeSeq hf p b₁ x ≤ aeSeq hf p z x

Tactic:
· simp only [aeSeq, hx, if_false]
          exact le_rfl

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

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

Tactic:
Measure.restrict_restrict hs

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in s ∩ t, f a ∂μ = ∫⁻ (a : α) in s ∩ t, f a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∉ aeSeqSet hf p
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z x

Tactic:
· simp only [aeSeq, hx, if_false]
          exact le_rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : GroupWithZero β
inst✝² : ContinuousMul β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ StronglyMeasurable (f / g)

Tactic:
refine ⟨fun n => hf.approx n / (hg.approx n).restrict {x | g x ≠ 0}, fun x => ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : GroupWithZero β
inst✝² : ContinuousMul β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
⊢ Tendsto (fun n ↦ ((fun n ↦ hf.approx n / (hg.approx n).restrict {x | g x ≠ 0}) n) x) atTop (𝓝 ((f / g) x))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
s : β → Set α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ i, s i, f a ∂μ ≤ ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ

Tactic:
by
  rw [← lintegral_sum_measure]
  exact lintegral_mono' restrict_iUnion_le le_rfl

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
⊢ Perfect (closure[inst✝] C)

Tactic:
constructor; · exact isClosed_closure
  intro x hx
  by_cases h : x ∈ C <;> apply AccPt.mono _ (principal_mono.mpr subset_closure)
  · exact hC _ h
  have : {x}ᶜ ∩ C = C := by simp [h]
  rw [AccPt, nhdsWithin, inf_assoc, inf_principal, this]
  rw [closure_eq_cluster_pts] at hx
  exact hx

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure[inst✝¹] C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure[inst✝¹] C
y : α
hyx : y ≠ x
yC : y ∈ closure[inst✝¹] C
⊢ y ∈ closure[inst✝¹] C

Tactic:
exact yC

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

Goal state before:
pp: case a
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
g : ℕ → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ := ⋯
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
n : ℕ
⊢ ∫⁻ (x : α), f n x ∂μ ≤ ∫⁻ (x : α), g' n x ∂μ

Tactic:
· rw [hg n]
      exact lintegral_mono (I n)

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: i j : ↑I
h : i ≤ j * i
⊢ i = 0 ∨ j = 1

Tactic:
contrapose! h

Goal state after:
i j : ↑I
h : i ≠ 0 ∧ j ≠ 1
⊢ j * i < i