mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
x : α
hx : x ∈ s
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K (fun x ↦ f x * g x) t

Tactic:
by
  obtain ⟨Kf, t, ht, hKf⟩ := hf hx
  obtain ⟨Kg, u, hu, hKg⟩ := hg hx
  exact ⟨Kf + Kg, t ∩ u, inter_mem ht hu,
    (hKf.mono Set.inter_subset_left).mul (hKg.mono Set.inter_subset_right)⟩

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : SeminormedGroup E
f : α → E
l : Filter α
⊢ Tendsto (fun x ↦ ‖f x‖) l atTop ↔ Tendsto f l (cobounded E)

Tactic:
by
  rw [← comap_norm_atTop', tendsto_comap_iff]; rfl

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedGroup E
⊢ (cobounded E)⁻¹ = cobounded E

Tactic:
by
  simp only [← comap_norm_atTop', ← Filter.comap_inv, comap_comap, Function.comp_def, norm_inv']

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
F : Type u_3
inst✝³ : PseudoMetricSpace X
inst✝² : PseudoMetricSpace Y
inst✝¹ : EquivLike F X Y
inst✝ : DilationEquivClass F X Y
e : F
⊢ map (⇑e) (cobounded X) = cobounded Y

Tactic:
← Dilation.comap_cobounded e,

Goal state after:
X : Type u_1
Y : Type u_2
F : Type u_3
inst✝³ : PseudoMetricSpace X
inst✝² : PseudoMetricSpace Y
inst✝¹ : EquivLike F X Y
inst✝ : DilationEquivClass F X Y
e : F
⊢ map (⇑e) (comap (⇑e) (cobounded Y)) = cobounded Y
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: ι : Type u_4
α : Type u_5
inst✝ : NormedCommRing α
s : Finset ι
hs : s.Nonempty
f : ι → α
⊢ ∏ i ∈ s, ‖f i‖ = ↑(∏ i ∈ s, ‖f i‖₊)

Tactic:
by simp [NNReal.coe_prod]

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: ι : Type u_4
α : Type u_5
inst✝¹ : NormedCommRing α
inst✝ : NormOneClass α
s : Finset ι
f : ι → α
⊢ ∏ i ∈ s, ‖f i‖ = ↑(∏ i ∈ s, ‖f i‖₊)

Tactic:
by simp [NNReal.coe_prod]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: α : Type u_6
inst✝² : SeminormedRing α
inst✝¹ : NormOneClass α
inst✝ : NormSMulClass ℤ α
a : ℕ
⊢ ‖↑a‖ = ↑a

Tactic:
simpa using norm_natCast_eq_mul_norm_one α a

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
hs : ∀ x ∈ s, ∃ u ∈ 𝓝[s] x, μ u = 0
⊢ μ s = 0

Tactic:
choose! u hxu hu₀ using hs
  choose t ht using TopologicalSpace.countable_cover_nhdsWithin hxu
  rcases ht with ⟨ts, t_count, ht⟩
  apply measure_mono_null ht
  exact (measure_biUnion_null_iff t_count).2 fun x hx => hu₀ x (ts hx)

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n m : ℕ
h : n ≤ m
⊢ 1 / (↑m + 1) ≤ 1 / (↑n + 1)

Tactic:
refine one_div_le_one_div_of_le ?_ ?_

Goal state after:
case refine_1
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n m : ℕ
h : n ≤ m
⊢ 0 < ↑n + 1

case refine_2
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n m : ℕ
h : n ≤ m
⊢ ↑n + 1 ≤ ↑m + 1
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ (⊤ * ↑x✝).abs = ⊤.abs * (↑x✝).abs

Tactic:
top_mul_coe_of_pos h,

Goal state after:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ⊤.abs = ⊤.abs * (↑x✝).abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ sign (⊤ * ↑x✝) = sign ⊤ * sign ↑x✝

Tactic:
top_mul_coe_of_pos h,

Goal state after:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ sign ⊤ = sign ⊤ * sign ↑x✝
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
⊢ SemicontinuousAt r x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝 x, ¬r x' y) → ¬r x y

Tactic:
by
  simp only [← not_eventually, not_imp_not, SemicontinuousAt]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: β : Type u_2
γ : Type u_3
f : β → ℝ≥0∞
g : β → γ
⊢ ∑' (x : γ) (b : ↑(g ⁻¹' {x})), f ↑b = ∑' (i : β), f i

Tactic:
apply HasSum.tsum_eq

Goal state after:
β : Type u_2
γ : Type u_3
f : β → ℝ≥0∞
g : β → γ
⊢ HasSum (fun b ↦ ∑' (b_1 : ↑(g ⁻¹' {b})), f ↑b_1) (∑' (i : β), f i)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe.inl
a : ℝ
a_neg : a < 0
⊢ -↑(ENNReal.ofReal |a|)⁻¹ = (↑a)⁻¹

Tactic:
← ofReal_inv_of_pos (abs_pos_of_neg a_neg),

Goal state after:
case coe.inl
a : ℝ
a_neg : a < 0
⊢ -↑(ENNReal.ofReal |a|⁻¹) = (↑a)⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
⊢ c / b = a ↔ c = a * b

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c / b = a
⊢ c = a * b

case refine_2
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c = a * b
⊢ c / b = a
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
x✝¹ : Nonempty α
x✝ : Nonempty ↑s
φ : β → Filter α := ⋯
ℱ : Filter α := ⋯
⊢ ∀ (i : ↑s), (φ (f ↑i)).NeBot

Tactic:
intro x
      have : (pure x : Filter α) ≤ φ (f x) := le_principal_iff.mpr ⟨x.2, le_refl (f x)⟩
      exact neBot_of_le this

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ edist (f n) a ≤ ∑' (m : ℕ), d (n + m)

Tactic:
refine le_of_tendsto (tendsto_const_nhds.edist ha) (mem_atTop_sets.2 ⟨n, fun m hnm => ?_⟩)

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : n ≤ m
⊢ m ∈ {x | (fun c ↦ edist (f n) (f c) ≤ ∑' (m : ℕ), d (n + m)) x}
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ 0
hc : b * a < c
⊢ ∃ b' ∈ Ioo b ⊤, b' * a < c

Tactic:
exact exists_mul_left_lt h₂.symm h₁.symm hc

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

Goal state before:
pp: ⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ⊤)

Tactic:
by
  simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_top]
  refine fun r ↦ ((lt_mem_nhds (coe_lt_top 0)).prod_nhds
    (lt_mem_nhds <| coe_lt_top r)).mono fun _ h ↦ ?_
  simpa only [coe_zero, zero_add] using add_lt_add h.1 h.2

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

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
h : (↑a✝¹, ↑a✝).1 ≠ ⊤ ∨ (↑a✝¹, ↑a✝).2 ≠ ⊥
h' : (↑a✝¹, ↑a✝).1 ≠ ⊥ ∨ (↑a✝¹, ↑a✝).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a✝¹, ↑a✝)

pp: case coe.top
a✝ : ℝ
h : (↑a✝, ⊤).1 ≠ ⊤ ∨ (↑a✝, ⊤).2 ≠ ⊥
h' : (↑a✝, ⊤).1 ≠ ⊥ ∨ (↑a✝, ⊤).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a✝, ⊤)

pp: case top.bot
h : (⊤, ⊥).1 ≠ ⊤ ∨ (⊤, ⊥).2 ≠ ⊥
h' : (⊤, ⊥).1 ≠ ⊥ ∨ (⊤, ⊥).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ⊥)

pp: case top.coe
a✝ : ℝ
h : (⊤, ↑a✝).1 ≠ ⊤ ∨ (⊤, ↑a✝).2 ≠ ⊥
h' : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ↑a✝)

pp: case top.top
h : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ ⊥
h' : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ⊤)

Tactic:
· exact continuousAt_add_coe_coe _ _

Goal state after:
case coe.top
a✝ : ℝ
h : (↑a✝, ⊤).1 ≠ ⊤ ∨ (↑a✝, ⊤).2 ≠ ⊥
h' : (↑a✝, ⊤).1 ≠ ⊥ ∨ (↑a✝, ⊤).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a✝, ⊤)

case top.bot
h : (⊤, ⊥).1 ≠ ⊤ ∨ (⊤, ⊥).2 ≠ ⊥
h' : (⊤, ⊥).1 ≠ ⊥ ∨ (⊤, ⊥).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ⊥)

case top.coe
a✝ : ℝ
h : (⊤, ↑a✝).1 ≠ ⊤ ∨ (⊤, ↑a✝).2 ≠ ⊥
h' : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ↑a✝)

case top.top
h : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ ⊥
h' : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ⊤)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_1
x : ℝ
⊢ ∀ y ∈ Ioi (max (↑x) 0) ×ˢ Ioi 1, ↑x < y.1 * y.2

Tactic:
intro p

Goal state after:
case h.refine_1
x : ℝ
p : EReal × EReal
⊢ p ∈ Ioi (max (↑x) 0) ×ˢ Ioi 1 → ↑x < p.1 * p.2
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ ∀ y ∈ Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2), ↑x < y.1 * y.2

Tactic:
intro p

Goal state after:
case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
⊢ p ∈ Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2) → ↑x < p.1 * p.2
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
⊢ Summable fun i ↦ 1 / m ^ f i

Tactic:
refine .of_nonneg_of_le (fun a ↦ by positivity) (fun a ↦ ?_)
      (summable_geometric_of_lt_one (one_div_nonneg.mpr (zero_le_one.trans hm.le))
        ((one_div_lt (zero_lt_one.trans hm) zero_lt_one).mpr (one_div_one.le.trans_lt hm)))

Goal state after:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 1 / m ^ f a ≤ (1 / m) ^ a
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_4
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorSemiring α
⊢ Tendsto (fun x ↦ ⌈x⌉₊) atTop atTop

Tactic:
by
  refine Nat.ceil_mono.tendsto_atTop_atTop (fun x ↦ ⟨x, ?_⟩)
  simp only [Nat.ceil_natCast, le_refl]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (s ∪ t) < ∞
⊢ μ s < ∞

pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (s ∪ t) < ∞
⊢ μ t < ∞

Tactic:
· exact (measure_mono Set.subset_union_left).trans_lt h

Goal state after:
case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (s ∪ t) < ∞
⊢ μ t < ∞
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
⊢ x ⊆ ∅

Tactic:
intro p

Goal state after:
case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
p : Prop
⊢ p ∈ x → p ∈ ∅
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ MeasurableSet t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

Tactic:
by
  simp_rw +instances [MeasurableSpace.generateFrom_singleton]
  unfold MeasurableSet MeasurableSpace.MeasurableSet' MeasurableSpace.comap
  simp_rw [MeasurableSpace.measurableSet_top, true_and]
  constructor
  · rintro ⟨x, rfl⟩
    by_cases hT : True ∈ x
    · by_cases hF : False ∈ x
      · suffices x = univ by grind
        grind [univ_eq_true_false]
      · grind
    · by_cases hF : False ∈ x
      · grind
      · suffices x ⊆ ∅ by grind
        intro p hp
        fin_cases p <;> contradiction
  · rintro (rfl | rfl | rfl | rfl)
    on_goal 1 => use ∅
    on_goal 2 => use {True}
    on_goal 3 => use {False}
    on_goal 4 => use Set.univ
    all_goals
      simp [compl_def]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ms = ∞
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ms

Tactic:
simp only [hs]
    simp only [iInf_eq_top, ms] at hs
    exact ⟨univ, subset_univ s, MeasurableSet.univ, hs _ (subset_univ s) MeasurableSet.univ⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
⊢ Measurable (g ∘ f) ↔ Measurable f

Tactic:
refine ⟨fun H => ?_, hg.measurable.comp⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
⊢ Measurable f
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
h : MeasurableSet (⇑e ⁻¹' s)
⊢ MeasurableSet s

Tactic:
by simpa only [symm_preimage_preimage] using e.symm.measurable h

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

Goal state before:
pp: case refine_1.succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n : ℕ
ih : MeasurableSet (F^[n] univ)
⊢ MeasurableSet (F^[n + 1] univ)

Tactic:
rw [Function.iterate_succ', Function.comp_apply]

Goal state after:
case refine_1.succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n : ℕ
ih : MeasurableSet (F^[n] univ)
⊢ MeasurableSet (F (F^[n] univ))
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case refine_2.a.succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n✝ : ℕ
⊢ F (iInter X) ⊆ F^[n✝ + 1] univ

Tactic:
rw [Function.iterate_succ', Function.comp_apply]

Goal state after:
case refine_2.a.succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n✝ : ℕ
⊢ F (iInter X) ⊆ F (F^[n✝] univ)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : μ s ≤ μ t + ε
⊢ μ tᶜ ≤ μ sᶜ + ε

Tactic:
measure_compl ht (by finiteness),

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : μ s ≤ μ t + ε
⊢ μ univ - μ t ≤ μ sᶜ + ε
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
⊢ IsFiniteMeasure (map f μ)

Tactic:
by
  by_cases hf : AEMeasurable f μ
  · constructor
    rw [map_apply_of_aemeasurable hf MeasurableSet.univ]
    exact measure_lt_top μ _
  · rw [map_of_not_aemeasurable hf]
    exact MeasureTheory.isFiniteMeasureZero

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
h✝ : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s | IsOpen[inst✝²] s ∧ μ s < ∞}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
x : α
this : x ∈ ⋃₀ T
⊢ ∃ t ∈ range f, x ∈ t

Tactic:
simpa only [mem_sUnion, exists_prop, ← hf]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x | p x} (μ.restrict s)
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x

Tactic:
by
  simp only [ae_iff, ← compl_ofPred, Measure.restrict_apply₀ hp.compl]
  rw [iff_iff_eq]; congr with x; simp [and_comm]

Goal state after:
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 α
hst : s ⊆ t
⊢ ⨅ b ∈ m, b.toOuterMeasure s ≤ μ t

Tactic:
exact iInf₂_le_of_le μ hμ <| measure_mono hst

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
⊢ NullMeasurableSet t (μ.restrict s) ↔ NullMeasurableSet (t ∩ s) μ

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
⊢ NullMeasurableSet (t ∩ s) μ

case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet (t ∩ s) μ
⊢ NullMeasurableSet t (μ.restrict s)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
⊢ Pairwise (Function.onFun Disjoint (countablyGeneratedAtom α))

Tactic:
intro p

Goal state after:
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
p : ℕ → Prop
⊢ ∀ ⦃j : ℕ → Prop⦄, p ≠ j → Function.onFun Disjoint (countablyGeneratedAtom α) p j
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
A : ℕ → Set α := natGeneratingSequence α
hA : ∀ (n : ℕ), MeasurableSet (A n)
hA_gen : generateFrom (range A) = mα
s : Set α
hs : MeasurableSet s
q : (ℕ → Prop) → Prop
hq : s = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
p : ℕ → Prop
hpq : q p
hpx : x ∈ countablyGeneratedAtom α p
this : p = fun x_1 ↦ x ∈ A x_1
⊢ q fun x_1 ↦ x ∈ A x_1

Tactic:
by rwa [← this]

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

Goal state before:
pp: α : Type u_1
m m' : MeasurableSpace α
h : m ≤ m'
hsep : HasCountableSeparatingOn α MeasurableSet univ
⊢ HasCountableSeparatingOn α MeasurableSet univ

Tactic:
rcases hsep with ⟨S, Sct, Smeas, hS⟩

Goal state after:
α : Type u_1
m m' : MeasurableSpace α
h : m ≤ m'
S : Set (Set α)
Sct : S.Countable
Smeas : ∀ s ∈ S, MeasurableSet s
hS : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ HasCountableSeparatingOn α MeasurableSet univ
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
i : ι
x : α
hx : f x ≠ mk f ⋯ x
⊢ x ∈ s i

Tactic:
exact subset_toMeasurable _ _ hx

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

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
h : ∀ᵐ (x : α) (y : α) ∂0, f x = f y
⊢ AEMeasurable f 0

Tactic:
exact aemeasurable_zero_measure

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

Goal state before:
pp: case inr
α : 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_eq_iUnion : Ioi x = ⋃ n, Ioc x (u n)
n : ℕ
h : u n ≤ x
⊢ AEMeasurable g 0

Tactic:
exact aemeasurable_zero_measure

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
ι' : Type u_8
μ : ι → ι' → Measure α
⊢ (sum fun n ↦ sum (μ n)) = sum fun p ↦ μ p.1 p.2

Tactic:
by
  ext1 s hs
  simp [sum_apply _ hs, ENNReal.tsum_prod']

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsClosed s
⊢ IsGδ s

Tactic:
let := pseudoMetrizableSpaceUniformity X

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsClosed s
this : UniformSpace X := pseudoMetrizableSpaceUniformity X
⊢ IsGδ s
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableMul G
g : G
⊢ Measurable fun h ↦ h / g

Tactic:
simp_rw [div_eq_mul_inv, measurable_mul_const]

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

Goal state before:
pp: α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
f : Set (Set α)
hf : ∀ s_1 ∈ f, GenerateOpen s s_1
ih : ∀ s_1 ∈ f, MeasurableSet s_1
⊢ ∀ s ∈ f, IsOpen[t] s

Tactic:
by rwa [hs]

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
ι : Type u_3
α : Type u_4
β : Type u_5
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
mβ : MeasurableSpace β
f : ι → α → β → M
g : α → β
s : Finset ι
hf : ∀ i ∈ s, Measurable ↿(f i)
hg : Measurable g
⊢ Measurable fun a ↦ (∏ i ∈ s, f i a) (g a)

Tactic:
simp only [prod_apply]; fun_prop

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

Goal state before:
pp: case refine_1.inl.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a b : α
hb : a ⋖ b
⊢ MeasurableSet (Ici b)

Tactic:
← compl_Iio

Goal state after:
case refine_1.inl.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a b : α
hb : a ⋖ b
⊢ MeasurableSet (Iio b)ᶜ
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
hne : s.Nonempty
x : α
A : Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun y ↦ edist x y
y : α
ys : y ∈ s
hy : IsMinOn (fun y ↦ edist x y) s y
⊢ edist x y ≤ infEDist x s

Tactic:
rwa [le_infEDist]

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

Goal state before:
pp: δ : ℝ
X : Type u
inst✝ : PseudoMetricSpace X
E : Set X
x : X
key_iff : ∀ (z : X), edist x z < ENNReal.ofReal δ ↔ dist x z < δ
⊢ x ∈ thickening δ E ↔ ∃ z ∈ E, dist x z < δ

Tactic:
mem_thickening_iff_exists_edist_lt,

Goal state after:
δ : ℝ
X : Type u
inst✝ : PseudoMetricSpace X
E : Set X
x : X
key_iff : ∀ (z : X), edist x z < ENNReal.ofReal δ ↔ dist x z < δ
⊢ (∃ z ∈ E, edist x z < ENNReal.ofReal δ) ↔ ∃ z ∈ E, dist x z < δ