mathlib-initiative/mathlib-tactics huggingface dataset:
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 μ ≠ ∞
⊢ (SimpleFunc.map ofNNReal φ).lintegral μ + (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ <
    (SimpleFunc.map ofNNReal φ).lintegral μ + ε

Tactic:
← add_lintegral,

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 μ ≠ ∞
⊢ (SimpleFunc.map ofNNReal φ + SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ <
    (SimpleFunc.map ofNNReal φ).lintegral μ + ε
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a ↦ f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : μ t = 0
this : ∀ᵐ (x : α) ∂μ, x ∉ t
s : α →ₛ ℝ≥0∞
hfs : ⇑s ≤ fun a ↦ f a
a : α
hnt : a ∉ t
⊢ s a = (s.restrict tᶜ) a

Tactic:
simp [restrict_apply s ht.compl, hnt]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
m m' : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
h_mono : m' ≤ m
f_approx : ℕ → α →ₛ β := fun n ↦ { toFun := ⇑(hf.approx n), measurableSet_fiber' := ⋯, finite_range' := ⋯ }
⊢ StronglyMeasurable f

Tactic:
exact ⟨f_approx, hf.tendsto_approx⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst✝ : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
⊢ ∫⁻ (a : α), liminf (fun i ↦ f i a) u ∂μ ≤ liminf (fun i ↦ ∫⁻ (a : α), f i a ∂μ) u

Tactic:
by
  by_cases! hu : ¬ u.NeBot
  · simp_all
  · obtain ⟨g, hg⟩ : ∃ g : ℕ → ι,
        Tendsto (fun n => ∫⁻ a, f (g n) a ∂μ) atTop (𝓝 (liminf (fun i => ∫⁻ a, f i a ∂μ) u)) ∧
        Tendsto g atTop u :=
      exists_seq_tendsto_liminf
    calc
    _ ≤ ∫⁻ a, liminf (fun n => f (g n) a) atTop ∂μ :=
      lintegral_mono fun a => hg.2.liminf_le_liminf_comp
    _ ≤ liminf (fun n => ∫⁻ a, f (g n) a ∂μ) atTop :=
      lintegral_liminf_nat_le' (fun n => h_meas (g n))
    _ = _ := hg.1.liminf_eq

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ (⨆ n, (eapprox f n).lintegral μ) + ⨆ n, (eapprox g n).lintegral μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Tactic:
by
      rw [lintegral_eq_iSup_eapprox_lintegral hf, lintegral_eq_iSup_eapprox_lintegral hg]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
⊢ ∫⁻ (a : α), ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), f i a ∂μ = ∫⁻ (a : α), limsup (fun n ↦ f n a) atTop ∂μ

Tactic:
simp only [limsup_eq_iInf_iSup_of_nat]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
n : ℕ
hC_lt : 1 / ↑n < ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s
h_lt_top : ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s < ∞
t : Set α
h_notMem : ¬MeasurableSet t
ht :
  (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n <
    ⨆ (_ : False), ⨆ (_ : SigmaFinite (μ.restrict t)), ν t
⊢ False

Tactic:
simp at ht

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

Goal state before:
pp: case h_directed
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun s a ↦ ∑ i ∈ s, f i a

Tactic:
intro s t

Goal state after:
case h_directed
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) ((fun s a ↦ ∑ i ∈ s, f i a) s) ((fun s a ↦ ∑ i ∈ s, f i a) z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) ((fun s a ↦ ∑ i ∈ s, f i a) t) ((fun s a ↦ ∑ i ∈ s, f i a) z)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
n : ℕ
hC_lt : 1 / ↑n < ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s
h_lt_top : ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s < ∞
t : Set α
ht_meas : MeasurableSet t
h_notMem : ¬SigmaFinite (μ.restrict t)
ht :
  (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n <
    ⨆ (_ : MeasurableSet t), ⨆ (_ : False), ν t
⊢ False

Tactic:
simp at ht

Goal state after:
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
⊢ CauchySeq fun s ↦ ∑ i ∈ s, f i

Tactic:
refine cauchySeq_finset_iff_vanishing_norm.2 fun ε hε => ?_

Goal state after:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
⊢ ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
i : ι
hi : i ∈ t
⊢ ‖f i‖ ≤ g i

Tactic:
simp only [disjoint_left, mem_union, not_or, h.mem_toFinset, Set.mem_compl_iff,
      Classical.not_not] at ht

Goal state after:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, g i‖ < ε
t : Finset ι
i : ι
hi : i ∈ t
ht : ∀ ⦃a : ι⦄, a ∈ t → a ∉ s ∧ a ∈ {x | ‖f x‖ ≤ g x}
⊢ ‖f i‖ ≤ g i
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: case neg
ι : Type u_1
ε : Type u_5
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddCommMonoid ε
f : ι → ε
g : ι → ℝ≥0∞
a : ℝ≥0∞
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ₑ ≤ g i
hf : ¬Summable f
⊢ ‖∑' (i : ι), f i‖ₑ ≤ a

Tactic:
simp [tsum_eq_zero_of_not_summable hf]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.FunctionSeries

Goal state before:
pp: β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
N : Set ι
hN : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε

Tactic:
refine ⟨hN.toFinset ∪ t, fun n hn x hx => ?_⟩

Goal state after:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
N : Set ι
hN : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
⊢ dist (∑' (n : ι), f n x) (∑ n ∈ n, f n x) < ε
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this : UpgradedIsCompletelyMetrizableSpace β := upgradeIsCompletelyMetrizable β
⊢ PolishSpace α

Tactic:
let : MetricSpace α := hf.isEmbedding.comapMetricSpace f

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this✝ : UpgradedIsCompletelyMetrizableSpace β := upgradeIsCompletelyMetrizable β
this : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
⊢ PolishSpace α
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
⊢ dist ⟨i, x⟩ ⟨k, z⟩ ≤ dist ⟨i, x⟩ ⟨j, y⟩ + dist ⟨j, y⟩ ⟨k, z⟩

Tactic:
rcases eq_or_ne i k with (rfl | hik)

Goal state after:
case inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
z : E i
⊢ dist ⟨i, x⟩ ⟨i, z⟩ ≤ dist ⟨i, x⟩ ⟨j, y⟩ + dist ⟨j, y⟩ ⟨i, z⟩

case inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
hik : i ≠ k
⊢ dist ⟨i, x⟩ ⟨k, z⟩ ≤ dist ⟨i, x⟩ ⟨j, y⟩ + dist ⟨j, y⟩ ⟨k, z⟩
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mp
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
⊢ IsOpen[instTopologicalSpaceSigma] s → ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s

Tactic:
rintro hs ⟨i, x⟩ hx

Goal state after:
case mp
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : ⟨i, x⟩ ∈ s
⊢ ∃ ε > 0, ∀ (y : (i : ι) × E i), dist ⟨i, x⟩ y < ε → y ∈ s
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
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ n, Disjoint s (cylinder x n)
⊢ firstDiff x y < shortestPrefixDiff x s

Tactic:
shortestPrefixDiff,

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
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ n, Disjoint s (cylinder x n)
⊢ firstDiff x y < if h : ∃ n, Disjoint s (cylinder x n) then Nat.find h else 0
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case neg
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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ n, Disjoint s (cylinder x n)
B : shortestPrefixDiff x s - 1 < shortestPrefixDiff x s
⊢ (s ∩ cylinder x (shortestPrefixDiff x s - 1)).Nonempty

Tactic:
shortestPrefixDiff,

Goal state after:
case neg
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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ n, Disjoint s (cylinder x n)
B :
  (if h : ∃ n, Disjoint s (cylinder x n) then Nat.find h else 0) - 1 <
    if h : ∃ n, Disjoint s (cylinder x n) then Nat.find h else 0
⊢ (s ∩ cylinder x ((if h : ∃ n, Disjoint s (cylinder x n) then Nat.find h else 0) - 1)).Nonempty
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
DP : List Bool → P :=
  fun l ↦
    List.rec ⟨C, ⋯⟩
      (fun a l ih ↦ Bool.casesOn (motive := fun t ↦ a = t → P) a (fun h ↦ ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h ↦ ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l
D : List Bool → Set α := fun l ↦ ↑(DP l)
hanti : ClosureAntitone D
hdiam : VanishingDiam D
hdisj' : CantorScheme.Disjoint D
hdom : ∀ {x : ℕ → Bool}, x ∈ (inducedMap D).fst
⊢ (range fun x ↦ (inducedMap D).snd ⟨x, ⋯⟩) ⊆ C

Tactic:
rintro y ⟨x, rfl⟩
    exact map_mem ⟨_, hdom⟩ 0

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case mp
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
obs : A.indicator 1 x = A.indicator 1 y
⊢ x ∈ A ↔ y ∈ A

Tactic:
by_cases x_in_A : x ∈ A

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
obs : A.indicator 1 x = A.indicator 1 y
x_in_A : x ∈ A
⊢ x ∈ A ↔ y ∈ A

case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
obs : A.indicator 1 x = A.indicator 1 y
x_in_A : x ∉ A
⊢ x ∈ A ↔ y ∈ A
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
⊢ (dirac x) A = (dirac y) A

Tactic:
by_cases x_in_A : x ∈ A

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∈ A
⊢ (dirac x) A = (dirac y) A

case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∉ A
⊢ (dirac x) A = (dirac y) A
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
A : Set α
A_mble : MeasurableSet A
⊢ x ∈ A ↔ y ∈ A

Tactic:
by_cases x_in_A : x ∈ A

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∈ A
⊢ x ∈ A ↔ y ∈ A

case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∉ A
⊢ x ∈ A ↔ y ∈ A
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ≥0∞
f_bdd : ∃ c, ∀ (x : α), f x ≤ ↑c
⊢ ∫⁻ (x : α), f x ∂μ < ∞

Tactic:
by
  rw [← μ.restrict_univ]
  refine setLIntegral_lt_top_of_le_nnreal (measure_ne_top _ _) ?_
  simpa using f_bdd

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

Tactic:
wlog h : IsFiniteMeasure μ generalizing μ

Goal state after:
case inr
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
this :
  ∀ (μ : Measure α) [SFinite μ],
    IsFiniteMeasure μ → ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
h : ¬IsFiniteMeasure μ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
n : ℕ
hn : ∀ (x : α), ψ x ≤ ↑n
this : ∫⁻ (a : α) in (toMeasurable μ s)ᶜ, min (f a) ↑n ∂μ ≠ ∞
hsm : MeasurableSet (toMeasurable μ s)
⊢ ∫⁻ (x : α) in toMeasurable μ s, g n x ∂μ + ∫⁻ (x : α) in (toMeasurable μ s)ᶜ, g n x ∂μ ≤
    ∫⁻ (a : α) in toMeasurable μ s, g n a ∂μ + ∫⁻ (a : α) in (toMeasurable μ s)ᶜ, min (f a) ↑n ∂μ

Tactic:
gcongr with x

Goal state after:
case hfg
α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
n : ℕ
hn : ∀ (x : α), ψ x ≤ ↑n
this : ∫⁻ (a : α) in (toMeasurable μ s)ᶜ, min (f a) ↑n ∂μ ≠ ∞
hsm : MeasurableSet (toMeasurable μ s)
x : α
⊢ g n x ≤ min (f x) ↑n
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
hf : AEMeasurable f m
⊢ (m.bind f) s = ∫⁻ (a : α), (f a) s ∂m

Tactic:
rw [bind, join_apply hs, lintegral_map' (measurable_coe hs).aemeasurable hf]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
C : ℝ≥0∞
f : α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ∞ → ∫⁻ (x : α) in s, f x ∂μ ≤ C
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
trim_eq_self

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
C : ℝ≥0∞
f : α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ∞ → ∫⁻ (x : α) in s, f x ∂μ ≤ C
⊢ SigmaFinite μ
Module: Mathlib.MeasureTheory.Measure.OpenPos

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
F : Set X
inst✝¹ : OpensMeasurableSpace X
inst✝ : IsProbabilityMeasure μ
hF : IsClosed[inst✝³] F
⊢ μ F = 1 ↔ F = univ

Tactic:
← measure_univ (μ := μ),

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
F : Set X
inst✝¹ : OpensMeasurableSpace X
inst✝ : IsProbabilityMeasure μ
hF : IsClosed[inst✝³] F
⊢ μ F = μ univ ↔ F = univ
Module: Mathlib.MeasureTheory.Measure.OpenPos

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
s : Set X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : T2Space X
h₂s : μ s = 0
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ n, K n = s
h : ∀ (n : ℕ), IsNowhereDense (K n)
⊢ IsMeagre s

Tactic:
rw [isMeagre_iff_countable_union_isNowhereDense]

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
s : Set X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : T2Space X
h₂s : μ s = 0
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ n, K n = s
h : ∀ (n : ℕ), IsNowhereDense (K n)
⊢ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
Module: Mathlib.MeasureTheory.Measure.Doubling

Goal state before:
pp: α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
⊢ ∃ C, ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑C * μ (closedBall x ε)

Tactic:
let C := doublingConstant μ
  suffices ∀ n,
      ∀ᶠ ε in 𝓝[>] 0, ∀ x, μ (closedBall x ((2 : ℝ) ^ n * ε)) ≤ C ^ n * μ (closedBall x ε) by
    rcases pow_unbounded_of_one_lt K one_lt_two with ⟨n, hn⟩
    use C ^ n
    filter_upwards [eventually_mem_nhdsWithin, this n] with ε hε₀ hε x t ht
    rw [mem_Ioi] at hε₀
    grw [ht, hn, ENNReal.coe_pow]
    exact hε x
  intro n
  induction n with
  | zero => simp
  | succ n ihn =>
    replace ihn := eventually_nhdsGT_zero_mul_left (two_pos : 0 < (2 : ℝ)) ihn
    filter_upwards [ihn, eventually_measure_le_doublingConstant_mul μ] with ε hεn hε x
    grw [pow_succ, mul_assoc, hεn, hε, ← mul_assoc, pow_succ]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
⊢ map Prod.snd (μ.prod ν) = μ univ • ν

Tactic:
by
  ext s hs
  simp [Measure.map_apply measurable_snd hs, ← univ_prod]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case hs
X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
inst✝ : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left✝¹ : SecondCountableTopology Z
left✝ : T4Space Z
right✝ : OpensMeasurableSpace Z
⊢ AnalyticSet s

pp: case hsc
X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
inst✝ : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left✝¹ : SecondCountableTopology Z
left✝ : T4Space Z
right✝ : OpensMeasurableSpace Z
⊢ AnalyticSet sᶜ

Tactic:
· rw [← image_preimage_eq s hsurj]
    exact h.analyticSet_image hf

Goal state after:
case hsc
X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
inst✝ : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left✝¹ : SecondCountableTopology Z
left✝ : T4Space Z
right✝ : OpensMeasurableSpace Z
⊢ AnalyticSet sᶜ
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
ι : Type u_4
ι' : Type u_5
inst✝¹ : Countable ι'
m : ι → Measure α
m' : ι' → Measure β
inst✝ : ∀ (n : ι'), SFinite (m' n)
⊢ (sum fun i ↦ (m i).prod (sum m')) = sum fun p ↦ (m p.1).prod (m' p.2)

Tactic:
prod_sum_right,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
ι : Type u_4
ι' : Type u_5
inst✝¹ : Countable ι'
m : ι → Measure α
m' : ι' → Measure β
inst✝ : ∀ (n : ι'), SFinite (m' n)
⊢ (sum fun i ↦ sum fun p ↦ (m i).prod (m' p)) = sum fun p ↦ (m p.1).prod (m' p.2)
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
⊢ ∃ S, ↑H' * S = ↑H ∧ Nat.card ↥H' * Nat.card ↑S = Nat.card ↥H

Tactic:
by
  let H'' : Subgroup H := H'.comap H.subtype
  have : H' = H''.map H.subtype := by simp [H'', h]
  rw [this]
  obtain ⟨S, cmem, -⟩ := H''.exists_isComplement_right 1
  refine ⟨H.subtype '' S, ?_, ?_⟩
  · have : H.subtype '' (H'' * S) = H''.map H.subtype * H.subtype '' S := image_mul H.subtype
    rw [← this, cmem.mul_eq]
    simp
  · have : Nat.card H'' * Nat.card S = Nat.card H := cmem.card_mul_card
    rw [← this]
    refine congr_arg₂ (· * ·) ?_ ?_ <;>
      exact Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm

Goal state after: