mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: case mp
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, μ {x | ε ≤ f x} = 0
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), u n ∈ Ioo 0 1
tu : ∀ ε > 0, ∃ N, ∀ n ≥ N, u n ≤ ε
x : α
h' : 0 < f x
⊢ ∃ i, x ∈ {x | u i ≤ f x}

Tactic:
obtain ⟨n, hn⟩ := tu _ h'

Goal state after:
case mp
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, μ {x | ε ≤ f x} = 0
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), u n ∈ Ioo 0 1
tu : ∀ ε > 0, ∃ N, ∀ n ≥ N, u n ≤ ε
x : α
h' : 0 < f x
n : ℕ
hn : ∀ n_1 ≥ n, u n_1 ≤ f x
⊢ ∃ i, x ∈ {x | u i ≤ f x}
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
⊢ 0 < ∫⁻ (a : α) in s, f a ∂μ ↔ 0 < μ (Function.support f ∩ s)

Tactic:
lintegral_pos_iff_support hf,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
⊢ 0 < (μ.restrict s) (Function.support f) ↔ 0 < μ (Function.support f ∩ s)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case pos
α : 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:
rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]

Goal state after:
case pos
α : 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
⊢ f b₁ x ≤ aeSeq hf p z x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case pos
α : 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
⊢ f b₁ x ≤ aeSeq hf p z x

Tactic:
rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]

Goal state after:
case pos
α : 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
⊢ f b₁ x ≤ f z x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case pos
α : 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
⊢ f b₁ x ≤ f z x

Tactic:
rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]

Goal state after:
case pos
α : 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
⊢ f b₁ x ≤ f z x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case pos
α : 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:
rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]

Goal state after:
case pos
α : 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
⊢ f b₂ x ≤ aeSeq hf p z x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case pos
α : 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
⊢ f b₂ x ≤ aeSeq hf p z x

Tactic:
rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]

Goal state after:
case pos
α : 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
⊢ f b₂ x ≤ f z x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case pos
α : 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
⊢ f b₂ x ≤ f z x

Tactic:
rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]

Goal state after:
case pos
α : 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
⊢ f b₂ x ≤ f z x
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, ∃ (_ : ⇑g ≤ f), ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ

Tactic:
by
      simpa only [← lt_iSup_iff, ← lintegral_def] using ENNReal.sub_lt_self hf hf₀ hε

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

Goal state before:
pp: case refine_2
α : 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 γ
H : StronglyMeasurable fun x ↦ g (f x)
⊢ IsSeparable (range f)

Tactic:
· have : IsSeparable (g ⁻¹' range (g ∘ f)) := hg.isSeparable_preimage H.isSeparable_range
    rwa [range_comp, hg.injective.preimage_image] at this

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
⊢ (μ.restrict (μ.sigmaFiniteSetWRT' ν)) (f (e n)) < ∞

pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
⊢ ⋃ i, f (e i) = Set.univ

Tactic:
· simp only [Nat.pairEquiv_symm_apply, measure_union_lt_top_iff, f, e]
    rw [Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT', Set.compl_inter_self,
      Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT']
    simp only [measure_empty, ENNReal.zero_lt_top, true_and]
    refine (measure_mono Set.inter_subset_left).trans_lt ?_
    rw [← Measure.restrict_apply' (measurableSet_sigmaFiniteSetGE _)]
    exact measure_spanningSets_lt_top _ _

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
⊢ ⋃ i, f (e i) = Set.univ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_3
inst✝ : MeasurableSpace β
ν : Measure β
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ ∫⁻ (x : α), ∫⁻ (y : β), f x * g y ∂ν ∂μ = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν

Tactic:
simp [lintegral_const_mul'' _ hg, lintegral_mul_const'' _ hf]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
this : ¬SigmaFinite (μ.restrict s)
h : ¬μ s = ∞
h_lt_top : Fact (μ s < ∞)
⊢ False

Tactic:
exact this inferInstance

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

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
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 ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) then h.choose else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))
hF'_le : F' ≤ᵐ[μ] F
⊢ ∫⁻ (a : α), F' a ∂μ = ∫⁻ (a : α), F a ∂μ

Tactic:
refine tendsto_nhds_unique ?_ hf_tendsto

Goal state after:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
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 ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) then h.choose else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))
hF'_le : F' ≤ᵐ[μ] F
⊢ Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case hs
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := ⋯
V : Set α := ⋯
D : Set α := ⋯
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : (E ∩ D).Countable
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
⊢ (E ∩ D ∪ V ∩ C).Countable

Tactic:
exact Countable.union h Vct

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : Y
y : X
⊢ ε ≤ glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y)

Tactic:
rw [glueDist_comm]

Goal state after:
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : Y
y : X
⊢ ε ≤ glueDist Φ Ψ ε (Sum.inl y) (Sum.inr x)
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: α : Type ?u.3
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
δ : α
s t : ↑unitInterval
⊢ 0 ≤ ↑s * (1 - ↑t) / (1 - ↑s * ↑t)

Tactic:
by
      apply div_nonneg
      · nlinarith [s.2.1, t.2.2]
      · nlinarith [s.2.2, t.2.2, t.2.1]

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

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) then h.choose else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))
hF'_le : F ≤ᵐ[μ] F'
⊢ ∫⁻ (a : α), F' a ∂μ = ∫⁻ (a : α), F a ∂μ

Tactic:
refine tendsto_nhds_unique ?_ hf_tendsto

Goal state after:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) then h.choose else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))
hF'_le : F ≤ᵐ[μ] F'
⊢ Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : IsCompletelyPseudoMetrizableSpace X
⊢ TopologicalSpace.PseudoMetrizableSpace X

Tactic:
let := upgradeIsCompletelyPseudoMetrizable X

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : IsCompletelyPseudoMetrizableSpace X
this : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
⊢ TopologicalSpace.PseudoMetrizableSpace X
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : IsCompletelyPseudoMetrizableSpace X
inst✝ : T0Space X
⊢ IsCompletelyMetrizableSpace X

Tactic:
let := upgradeIsCompletelyPseudoMetrizable X

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : IsCompletelyPseudoMetrizableSpace X
inst✝ : T0Space X
this : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
⊢ IsCompletelyMetrizableSpace X
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : IsTopologicalRing 𝕜
a b : 𝕜
h : a < b
⊢ ↑(Icc a b) ≃ₜ ↑(Icc 0 1)

Tactic:
let e := Homeomorph.image (affineHomeomorph (b - a) a (sub_pos.mpr h).ne.symm) (Set.Icc 0 1)
  refine (e.trans ?_).symm
  apply Homeomorph.setCongr
  rw [affineHomeomorph_image_I _ _ (sub_pos.2 h)]
  simp

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed[inst✝¹] s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
hle : coinduced (⇑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ IsOpen[coinduced (⇑f) instTopologicalSpaceSum] s

Tactic:
rw [isOpen_coinduced, isOpen_sum_iff]
    simp [preimage_preimage, f, t]

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

Goal state before:
pp: X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} ↦ f k) x.snd) (leRecOn hy (fun {k} ↦ f k) y.snd)

Tactic:
by_cases h : max x.1 y.1 = (m + 1)
    · generalize m + 1 = m' at *
      subst m'
      rfl
    · have : max x.1 y.1 ≤ succ m := by simp [hx, hy]
      have : max x.1 y.1 ≤ m := by simpa [h] using of_le_succ this
      have xm : x.1 ≤ m := le_trans (le_max_left _ _) this
      have ym : y.1 ≤ m := le_trans (le_max_right _ _) this
      rw [leRecOn_succ xm, leRecOn_succ ym, (I m).dist_eq]
      exact inductiveLimitDist_eq_dist I x y m xm ym

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

Goal state before:
pp: X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
⊢ inductiveLimitDist f x y = inductiveLimitDist f y x

Tactic:
let m := max x.1 y.1
    have hx : x.1 ≤ m := le_max_left _ _
    have hy : y.1 ≤ m := le_max_right _ _
    rw [inductiveLimitDist_eq_dist I x y m hx hy, inductiveLimitDist_eq_dist I y x m hy hx,
      dist_comm]

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

Goal state before:
pp: case pos
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : y ∈ s
⊢ firstDiff x y ≤ firstDiff x (f y)

Tactic:
fs y ys

Goal state after:
case pos
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : y ∈ s
⊢ firstDiff x y ≤ firstDiff x y
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ : p → Measure α
ν : ¬p → Measure α
inst✝¹ : ∀ (h : p), IsProbabilityMeasure (μ h)
inst✝ : ∀ (h : ¬p), IsProbabilityMeasure (ν h)
⊢ IsProbabilityMeasure (dite p μ ν)

Tactic:
split

Goal state after:
case isTrue
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ : p → Measure α
ν : ¬p → Measure α
inst✝¹ : ∀ (h : p), IsProbabilityMeasure (μ h)
inst✝ : ∀ (h : ¬p), IsProbabilityMeasure (ν h)
h✝ : p
⊢ IsProbabilityMeasure (μ h✝)

case isFalse
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ : p → Measure α
ν : ¬p → Measure α
inst✝¹ : ∀ (h : p), IsProbabilityMeasure (μ h)
inst✝ : ∀ (h : ¬p), IsProbabilityMeasure (ν h)
h✝ : ¬p
⊢ IsProbabilityMeasure (ν h✝)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ IsProbabilityMeasure (if p then μ else ν)

Tactic:
split

Goal state after:
case isTrue
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
h✝ : p
⊢ IsProbabilityMeasure μ

case isFalse
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
h✝ : ¬p
⊢ IsProbabilityMeasure ν
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case pos
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∈ s
A : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = A.some
I : cylinder A.some (firstDiff x y) = cylinder x (firstDiff x y)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)

Tactic:
fs y ys

Goal state after:
case pos
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∈ s
A : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = A.some
I : cylinder A.some (firstDiff x y) = cylinder x (firstDiff x y)
⊢ firstDiff x y ≤ firstDiff (f x) y
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder Ax.some (firstDiff x y) = cylinder x (firstDiff x y)
⊢ cylinder y (firstDiff x y) = cylinder Ay.some (firstDiff x y)

Tactic:
rw [eq_comm, ← mem_cylinder_iff_eq]

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
I1 : cylinder Ax.some (firstDiff x y) = cylinder x (firstDiff x y)
⊢ Ay.some ∈ cylinder y (firstDiff x y)