mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case inl
r : ℝ≥0∞
hr : r < 1
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

Tactic:
rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩

Goal state after:
case inl
r : ℝ≥0
hr' : ↑r < 1
hr : ↑r < 1
⊢ ∑' (n : ℕ), ↑r ^ n = (1 - ↑r)⁻¹
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : Type u_3
I : Set ι
hI : I.Nonempty
f : α → β
m : ι → OuterMeasure β
this : Nonempty ↑I
⊢ (map f) (⨅ i, (comap f) (m ↑i)) = ⨅ i, (map f) ((comap f) (m ↑i))

Tactic:
exact map_iInf_comap _

Goal state after:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case zero
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
⊢ ∃ m, s m ⊆ dissipate s 0

Tactic:
use 0

Goal state after:
case h
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
⊢ s 0 ⊆ dissipate s 0
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case pos
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
s : ℕ → Set α
h : ∀ (i : ℕ), P (s i)
⊢ m (⋃ i, s i) ⋯ ≤ tsum ?m.89

Tactic:
apply msU h

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
s : ℕ → Set α
⊢ extend m (⋃ i, s i) ≤ ∑' (i : ℕ), extend m (s i)

Tactic:
by_cases! h : ∀ i, P (s i)
  · rw [extend_eq _ (PU h), congr_arg tsum _]
    · apply msU h
    funext i
    apply extend_eq _ (h i)
  · obtain ⟨i, hi⟩ := h
    exact le_trans (le_iInf fun h => hi.elim h) (ENNReal.le_tsum i)

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.AE

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
ι : Sort u_4
p : α → ι → Prop
hp : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i
i : ι
⊢ ∀ᵐ (a : α) ∂μ, p a i

Tactic:
filter_upwards [hp] with a ha using ha i

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
t : Set α
ht : t ∈ piiUnionInter (fun n ↦ {s | MeasurableSet s}) S
⊢ MeasurableSet t

Tactic:
rcases ht with ⟨pt, hpt, ft, ht_m, rfl⟩

Goal state after:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ x ∈ pt, ft x ∈ (fun n ↦ {s | MeasurableSet s}) x
⊢ MeasurableSet (⋂ x ∈ pt, ft x)
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ⋂ i, U i ⊆ ⋂ i, V i

Tactic:
exact iInter_mono fun i => (hU i).2

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ m.trim s = ⨅ t, ⨅ (_ : MeasurableSet t), ⨅ (_ : s ⊆ t), m t

Tactic:
exact
    inducedOuterMeasure_eq_iInf MeasurableSet.iUnion (fun f _ => measure_iUnion_le f)
      (fun _ _ _ _ h => measure_mono h) s

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable ((range f).domRestrict (extend f g g'))

Tactic:
domRestrict_extend_range

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable fun x ↦ g (Exists.choose ⋯)
Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : β → γ
f : α → β
hg : QuasiMeasurePreserving g μb μc
hf : QuasiMeasurePreserving f μa μb
⊢ map (g ∘ f) μa ≪ μc

Tactic:
← map_map hg.1 hf.1

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : β → γ
f : α → β
hg : QuasiMeasurePreserving g μb μc
hf : QuasiMeasurePreserving f μa μb
⊢ map g (map f μa) ≪ μc
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nullsdiff : μ (s₃ \ s₁) = 0
le12 : μ s₁ ≤ μ s₂
le23 : μ s₂ ≤ μ s₃
⊢ μ (s₃ \ s₁) + μ s₁ = μ s₁

Tactic:
simp only [h_nullsdiff, zero_add]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
US : Set α
hsub : u ∩ s ⊆ US
hm : MeasurableSet US
hμ : μ US = μ (u ∩ s)
hν : ν US = ν (u ∩ s)
⊢ (μ.restrict s) u + (μ.restrict t) (u \ US) = (ν.restrict s) u + (ν.restrict t) (u \ US)

Tactic:
hs,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ.restrict s = ν.restrict s
ht : μ.restrict t = ν.restrict t
u : Set α
hu : MeasurableSet u
US : Set α
hsub : u ∩ s ⊆ US
hm : MeasurableSet US
hμ : μ US = μ (u ∩ s)
hν : ν US = ν (u ∩ s)
⊢ (ν.restrict s) u + (μ.restrict t) (u \ US) = (ν.restrict s) u + (ν.restrict t) (u \ US)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable ι
s : ι → Set α
hs : ⋃ i, s i = univ
⊢ μ = ν ↔ μ.restrict (⋃ i, s i) = ν.restrict (⋃ i, s i)

Tactic:
hs,

Goal state after:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable ι
s : ι → Set α
hs : ⋃ i, s i = univ
⊢ μ = ν ↔ μ.restrict univ = ν.restrict univ
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
S : Set ι
s : ι → Set α
hc : S.Countable
hs : ⋃ i ∈ S, s i = univ
⊢ μ = ν ↔ μ.restrict (⋃ i ∈ S, s i) = ν.restrict (⋃ i ∈ S, s i)

Tactic:
hs,

Goal state after:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
S : Set ι
s : ι → Set α
hc : S.Countable
hs : ⋃ i ∈ S, s i = univ
⊢ μ = ν ↔ μ.restrict univ = ν.restrict univ
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case compl
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, μ t ≠ ∞
ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)
T_eq : ∀ t ∈ T, μ t = ν t
t : Set α
ht : t ∈ T
u✝ u : Set α
hu : MeasurableSet u
ihu : μ (t ∩ u) = ν (t ∩ u)
this : μ t = ν t
⊢ μ (t ∩ uᶜ) = ν (t ∩ uᶜ)

Tactic:
rwa [← measure_inter_add_sdiff t hu, ← measure_inter_add_sdiff t hu, ← ihu,
      ENNReal.add_right_inj] at this

Goal state after:
case compl
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, μ t ≠ ∞
ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)
T_eq : ∀ t ∈ T, μ t = ν t
t : Set α
ht : t ∈ T
u✝ u : Set α
hu : MeasurableSet u
ihu : μ (t ∩ u) = ν (t ∩ u)
this : μ (t ∩ u) + μ (t \ u) = μ (t ∩ u) + ν (t \ u)
⊢ μ (t ∩ u) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t ⊆ u
_hu : MeasurableSet u
⊢ ∀ {s t : Set α}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ μ t

Tactic:
intro s t hst

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s✝ : Set α
hs : MeasurableSet s✝
t✝ : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t✝ ⊆ u
_hu : MeasurableSet u
s t : Set α
hst : s ⊆ t
⊢ OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ μ t
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : s ∈ countableGeneratingSet α
⊢ MeasurableSet s

Tactic:
rw [← generateFrom_countableGeneratingSet (α := α)]
  exact measurableSet_generateFrom hs

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
m m' : MeasurableSpace α
hsep : CountablySeparated α
h : m ≤ m'
⊢ CountablySeparated α

Tactic:
countablySeparated_def

Goal state after:
α : Type u_1
m m' : MeasurableSpace α
h : m ≤ m'
hsep : HasCountableSeparatingOn α MeasurableSet univ
⊢ HasCountableSeparatingOn α MeasurableSet univ
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
⊢ CountablySeparated ↑s ↔ HasCountableSeparatingOn α MeasurableSet s

Tactic:
countablySeparated_def

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
⊢ HasCountableSeparatingOn (↑s) MeasurableSet univ ↔ HasCountableSeparatingOn α MeasurableSet s
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_2.refine_2
α : Type u_1
t✝ : ℕ → Set α
n : ℕ
s : Set α
x✝ : ∃ S, ↑S ⊆ memPartition t✝ n ∧ s = ⋃₀ ↑S
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t✝ n
hS_eq : s = ⋃₀ ↑S
t : Set α
ht : t ∈ ↑S
⊢ MeasurableSet t

Tactic:
· exact measurableSet_generateFrom (hS_subset ht)

Goal state after:
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₁ : Finset ι
hC₁ : C₁ ∈ ↑Cs
C₂ : Finset ι
hC₂ : C₂ ∈ ↑Cs
hC : C₁ ≠ C₂
x : α
hx : x ∈ P C₁ ∩ P C₂
⊢ C₁ = C₂

Tactic:
exact subset_antisymm (C_subset_C hC₁ hx) (C_subset_C hC₂ (Set.inter_comm _ _ ▸ hx))

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

Goal state before:
pp: case pos
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a✝ : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha✝ : ∀ b < a✝, (Ioo b a✝).Nonempty
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a < b
x✝ : b < a✝
⊢ MeasurableSet (Icc a b)

Tactic:
exact .basic _ ⟨a, hts ha, b, hts hb, hab.le, mem_singleton _⟩

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n ↦ (fun x ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
⊢ ∃ F,
    (∀ (n : ℕ), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (F n)) ∧
      (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F

Tactic:
have F_subset : ∀ n, F n ⊆ U := fun n x hx ↦ by
    by_contra h
    have : infEDist x Uᶜ ≠ 0 := ((ENNReal.pow_pos a_pos _).trans_le hx).ne'
    exact this (infEDist_zero_of_mem h)

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n ↦ (fun x ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ ∃ F,
    (∀ (n : ℕ), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (F n)) ∧
      (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n ↦ (fun x ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this : ¬infEDist x Uᶜ = 0
⊢ 0 < infEDist x Uᶜ

Tactic:
simpa [pos_iff_ne_zero] using this

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ ∀ i ∈ s, infEDist i s = 0

Tactic:
exact fun x hx => infEDist_zero_of_mem hx

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : 0 ≤ δ
x : α
hx : infEDist x (thickening δ s) ≤ ENNReal.ofReal ε
⊢ infEDist x (thickening (?m.52 hx) s) + ENNReal.ofReal (?m.52 hx) ≤ ENNReal.ofReal ε + ENNReal.ofReal δ

Tactic:
grw [hx]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
fin : hausdorffEDist s t ≠ ∞
⊢ hausdorffDist s t = 0 ↔ s = t

Tactic:
by
  simp [← _root_.IsClosed.hausdorffEDist_zero_iff hs ht, hausdorffDist, ENNReal.toReal_eq_zero_iff,
    fin]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
hx : infEDist x (cthickening δ s) ≤ ENNReal.ofReal ε
⊢ infEDist x (cthickening (?m.38 hx) s) + ENNReal.ofReal (?m.38 hx) ≤ ENNReal.ofReal ε + ENNReal.ofReal δ

Tactic:
grw [hx]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ (f.restrict s).range
h0 : r ≠ 0
hs : ¬MeasurableSet s
⊢ r ∈ ⇑f '' s

Tactic:
rw [restrict_of_not_measurable hs] at hr

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ SimpleFunc.range 0
h0 : r ≠ 0
hs : ¬MeasurableSet s
⊢ r ∈ ⇑f '' s
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
X : α → β
Y : α → γ
⊢ MeasurableSpace.comap (fun ω ↦ (X ω, Y ω)) (mβ.prod mγ) = MeasurableSpace.comap X mβ ⊔ MeasurableSpace.comap Y mγ

Tactic:
MeasurableSpace.prod,

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
X : α → β
Y : α → γ
⊢ MeasurableSpace.comap (fun ω ↦ (X ω, Y ω)) (MeasurableSpace.comap Prod.fst mβ ⊔ MeasurableSpace.comap Prod.snd mγ) =
    MeasurableSpace.comap X mβ ⊔ MeasurableSpace.comap Y mγ
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
X : α → β
Y : α → γ
⊢ MeasurableSpace.comap (fun ω ↦ (X ω, Y ω)) (mβ.prod mγ) = MeasurableSpace.comap X mβ ⊔ MeasurableSpace.comap Y mγ

Tactic:
simp_rw [MeasurableSpace.prod, comap_sup, comap_comp]

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
X : α → β
Y : α → γ
⊢ MeasurableSpace.comap (Prod.fst ∘ fun ω ↦ (X ω, Y ω)) mβ ⊔ MeasurableSpace.comap (Prod.snd ∘ fun ω ↦ (X ω, Y ω)) mγ =
    MeasurableSpace.comap X mβ ⊔ MeasurableSpace.comap Y mγ
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
X : γ → α
Y : δ → β
⊢ MeasurableSpace.comap (Prod.map X Y) (mα.prod mβ) = (MeasurableSpace.comap X mα).prod (MeasurableSpace.comap Y mβ)

Tactic:
MeasurableSpace.prod,

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
X : γ → α
Y : δ → β
⊢ MeasurableSpace.comap (Prod.map X Y) (MeasurableSpace.comap Prod.fst mα ⊔ MeasurableSpace.comap Prod.snd mβ) =
    MeasurableSpace.comap Prod.fst (MeasurableSpace.comap X mα) ⊔
      MeasurableSpace.comap Prod.snd (MeasurableSpace.comap Y mβ)
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
X : γ → α
Y : δ → β
⊢ MeasurableSpace.comap (Prod.map X Y) (mα.prod mβ) = (MeasurableSpace.comap X mα).prod (MeasurableSpace.comap Y mβ)

Tactic:
simp_rw [MeasurableSpace.prod, comap_sup, comap_comp]

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
X : γ → α
Y : δ → β
⊢ MeasurableSpace.comap (Prod.fst ∘ Prod.map X Y) mα ⊔ MeasurableSpace.comap (Prod.snd ∘ Prod.map X Y) mβ =
    MeasurableSpace.comap (X ∘ Prod.fst) mα ⊔ MeasurableSpace.comap (Y ∘ Prod.snd) mβ
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
s t : Set α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
⊢ thickening (min ε₁ ε₂) (f '' V₁) ∪ thickening (min ε₁ ε₂) (f '' V₂) ⊆
    thickening ε₁ (f '' V₁) ∪ thickening ε₂ (f '' V₂)

Tactic:
gcongr <;> norm_num

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
a b c : α
inst✝³ : Add α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftReflectLT α
inst✝ : IsLeftCancelAdd α
⊢ a < b + c ↔ a < b ∨ ∃ d < c, a = b + d

Tactic:
obtain h | h := lt_or_ge a b
  · have : a < b + c := h.trans_le (le_self_add ..)
    tauto
  · obtain ⟨a, rfl⟩ := exists_add_of_le h
    simp

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

Goal state before:
pp: case neg
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this : Encodable ↑s
H : ¬∀ (i : ι), i ∈ s
⊢ Measurable fun b ↦ ⨆ i ∈ s, f i b

Tactic:
have : ∀ b, ⨆ i ∈ s, f i b = (⨆ (i : s), f i b) ⊔ sSup ∅ :=
      fun b ↦ cbiSup_eq_of_not_forall (f := fun i ↦ f i b) H

Goal state after:
case neg
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this✝ : Encodable ↑s
H : ¬∀ (i : ι), i ∈ s
this : ∀ (b : δ), ⨆ i ∈ s, f i b = Max.max (⨆ i, f (↑i) b) (sSup ∅)
⊢ Measurable fun b ↦ ⨆ i ∈ s, f i b
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Goal state before:
pp: α : Type u_3
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
inst✝ : L.NeBot
μ : Measure α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ NullMeasurableSet A μ

Tactic:
simp_rw [← aemeasurable_indicator_const_iff (1 : ℝ≥0∞)] at As_mble ⊢

Goal state after:
α : Type u_3
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
inst✝ : L.NeBot
μ : Measure α
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
As_mble : ∀ (i : ι), AEMeasurable ((As i).indicator fun x ↦ 1) μ
⊢ AEMeasurable (A.indicator fun x ↦ 1) μ
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
hx : f x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (Subtype.val '' univ)
this : Nonempty ↑s
⊢ Tendsto (fun n ↦ (approxOn f hf s y₀ h₀ n) x) atTop (𝓝 (f x))

Tactic:
← (denseRange_denseSeq s).closure_eq

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
this : Nonempty ↑s
hx :
  f x ∈
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      (Subtype.val '' closure[instTopologicalSpaceSubtype] (range (denseSeq ↑s)))
⊢ Tendsto (fun n ↦ (approxOn f hf s y₀ h₀ n) x) atTop (𝓝 (f x))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case hbc
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n ↦ (hf.approx n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n ↦ ‖(hf.approx n) x‖) atTop (𝓝 0)
n : ℕ
⊢ ‖min 1 (c / ‖(hf.approx n) x‖)‖ ≤ 1

Tactic:
Real.norm_of_nonneg

Goal state after:
case hbc
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n ↦ (hf.approx n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n ↦ ‖(hf.approx n) x‖) atTop (𝓝 0)
n : ℕ
⊢ min 1 (c / ‖(hf.approx n) x‖) ≤ 1

case hbc
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n ↦ (hf.approx n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n ↦ ‖(hf.approx n) x‖) atTop (𝓝 0)
n : ℕ
⊢ 0 ≤ min 1 (c / ‖(hf.approx n) x‖)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
ε : ℝ≥0∞
εpos : ε > 0
⊢ μ {x | ε ≤ f x} = 0

Tactic:
by_contra! h'
    refine ((ENNReal.mul_pos εpos.ne' h').trans_le ?_).ne' h
    calc
      _ ≥ ∫⁻ a in {x | ε ≤ f x}, f a ∂μ := setLIntegral_le_lintegral _ _
      _ ≥ ∫⁻ _ in {x | ε ≤ f x}, ε ∂μ :=
        setLIntegral_mono_ae hf.restrict (ae_of_all μ fun _ ↦ id)
      _ = _ := setLIntegral_const _ _

Goal state after: