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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
s : Set E
f : E → F
C : ℝ≥0
⊢ LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖(f x)⁻¹ * f y‖ ≤ ↑C * ‖x⁻¹ * y‖

Tactic:
by
  simp only [lipschitzOnWith_iff_dist_le_mul, dist_eq_norm_inv_mul]

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
p : E
⊢ mk p = 1 ↔ ‖p‖ = 0

Tactic:
rw [← norm_mk', norm_eq_zero']

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

Goal state before:
pp: α : Type u_1
inst✝² : SeminormedRing α
inst✝¹ : NormOneClass α
inst✝ : NormMulClass α
m : ℕ
hm : m ≠ 0
⊢ Tendsto (fun x ↦ x ^ m) (cobounded α) (cobounded α)

Tactic:
by
  simpa [← tendsto_norm_atTop_iff_cobounded] using!
    (tendsto_pow_atTop hm).comp (tendsto_norm_cobounded_atTop (E := α))

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

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (e.trans e') = ratio e * ratio e'

Tactic:
exact (Dilation.ratio_comp' (g := e'.toDilation) (f := e.toDilation) hX).trans (mul_comm _ _)

Goal state after:
Module: Mathlib.Data.ENNReal.Action

Goal state before:
pp: R : Type u_1
r : R
s : ℝ≥0
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ≥0∞
⊢ ↑(r • s) = (r • 1) • ↑s

Tactic:
smul_def,

Goal state after:
R : Type u_1
r : R
s : ℝ≥0
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ≥0∞
⊢ ↑(r • s) = ↑(r • 1) • ↑s
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
⊢ TProd.mk (i :: l) ⁻¹' Set.tprod (i :: l) t = {i_1 | i_1 ∈ i :: l}.pi t

Tactic:
ext f

Goal state after:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ TProd.mk (i :: l) ⁻¹' Set.tprod (i :: l) t ↔ f ∈ {i_1 | i_1 ∈ i :: l}.pi t
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort uι
s✝ : Set α
m✝ m₁ m₂ : MeasurableSpace α
m' : MeasurableSpace β
f✝ : α → β
g : β → α
f : α → β
m : MeasurableSpace β
s : ℕ → Set α
hs : ∀ (i : ℕ), ∃ s', MeasurableSet s' ∧ f ⁻¹' s' = s i
s' : ℕ → Set β
hs' : ∀ (x : ℕ), MeasurableSet (s' x) ∧ f ⁻¹' s' x = s x
⊢ f ⁻¹' ⋃ i, s' i = ⋃ i, s i

Tactic:
by simp [hs']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : {x | f x ≠ g x}.Countable
t : Set β
ht : MeasurableSet t
⊢ g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}

Tactic:
simp [← inter_union_distrib_left]

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
s t : Set α
⊢ μ s ≤ μ (s ∩ t) + μ (s \ t)

Tactic:
simpa using measure_union_le (s ∩ t) (s \ t)

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ ⨆ i, ∑ a ∈ s i, f a = ⨆ s, ∑ a ∈ s, f a

Tactic:
change ⨆ i : ι, (fun t : Finset α => ∑ a ∈ t, f a) (s i) = ⨆ s : Finset α, ∑ a ∈ s, f a

Goal state after:
α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ ⨆ i, (fun t ↦ ∑ a ∈ t, f a) (s i) = ⨆ s, ∑ a ∈ s, f a
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n ↦ ↑n * c) atTop (𝓝 (∞ * c))
n : ℕ
⊢ ↑n * c ≤ ∑' (x : α), c

Tactic:
rcases Infinite.exists_subset_card_eq α n with ⟨s, hs⟩
    simpa [hs] using @ENNReal.sum_le_tsum α (fun _ => c) s

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f : α → β
⊢ LowerSemicontinuous f ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y

Tactic:
by
  simp [semicontinuous_iff_frequently]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f : α → β
⊢ UpperSemicontinuous f ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≥ y) → f x ≥ y

Tactic:
by
  simp [semicontinuous_iff_frequently]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case bot
⊢ ⊤⁻¹ = -⊥⁻¹

Tactic:
inv_top,

Goal state after:
case bot
⊢ 0 = -⊥⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top
⊢ 0 = -⊤⁻¹

Tactic:
inv_top,

Goal state after:
case top
⊢ 0 = -0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_pos
x : ℝ
x_pos : 0 < x
⊢ ⊤⁻¹ = ⊤⁻¹ * (↑x)⁻¹

Tactic:
inv_top,

Goal state after:
case top_pos
x : ℝ
x_pos : 0 < x
⊢ 0 = 0 * (↑x)⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_neg
x : ℝ
x_neg : x < 0
⊢ 0 = ⊤⁻¹ * (↑x)⁻¹

Tactic:
inv_top,

Goal state after:
case top_neg
x : ℝ
x_neg : x < 0
⊢ 0 = 0 * (↑x)⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case neg_bot
x : ℝ
x_neg : x < 0
⊢ ⊤⁻¹ = (↑x)⁻¹ * ⊥⁻¹

Tactic:
inv_top,

Goal state after:
case neg_bot
x : ℝ
x_neg : x < 0
⊢ 0 = (↑x)⁻¹ * ⊥⁻¹
Module: Mathlib.Data.EReal.Inv

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

Tactic:
abs_def a,

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

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

Tactic:
abs_def a,

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

Goal state before:
pp: case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑(↑a).abs⁻¹ = (↑a)⁻¹

Tactic:
abs_def a,

Goal state after:
case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑(ENNReal.ofReal |a|)⁻¹ = (↑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 α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
⊢ ℱ.NeBot

Tactic:
apply iInf_neBot_of_directed _ _

Goal state after:
α : 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 α := ⋯
⊢ Directed (fun x1 x2 ↦ x1 ≥ x2) fun a ↦ φ (f ↑a)

α : 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
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
⊢ (∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x) →
    ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1

Tactic:
intro hf ⟨x, y⟩ h

Goal state after:
case mp
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_2
r : ℝ≥0∞
r_gt_one : 1 < r
obs : Tendsto (fun n ↦ r⁻¹ ^ n) atTop (𝓝 0) → Tendsto (fun x ↦ (r⁻¹ ^ x)⁻¹) atTop (𝓝 0⁻¹)
⊢ Tendsto (fun n ↦ r ^ n) atTop (𝓝 ∞)

Tactic:
simp only [ENNReal.tendsto_pow_atTop_nhds_zero_iff, inv_zero] at obs

Goal state after:
case refine_2
r : ℝ≥0∞
r_gt_one : 1 < r
obs : r⁻¹ < 1 → Tendsto (fun x ↦ (r⁻¹ ^ x)⁻¹) atTop (𝓝 ∞)
⊢ Tendsto (fun n ↦ r ^ n) atTop (𝓝 ∞)
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ (restrict s) (OuterMeasure.ofFunction m m_empty) = OuterMeasure.ofFunction (fun t ↦ m (t ∩ s)) ⋯

Tactic:
rw [restrict]

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ (map Subtype.val ∘ₗ comap Subtype.val) (OuterMeasure.ofFunction m m_empty) =
    OuterMeasure.ofFunction (fun t ↦ m (t ∩ s)) ⋯
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε

Tactic:
by
  cases nonempty_encodable ι
  obtain ⟨a, a0, aε⟩ := exists_between (pos_iff_ne_zero.2 hε)
  obtain ⟨ε', hε', c, hc, hcε⟩ := posSumOfEncodable a0 ι
  exact
    ⟨fun i ↦ ⟨ε' i, (hε' i).le⟩, fun i ↦ NNReal.coe_lt_coe.1 <| hε' i,
      ⟨c, hasSum_le (fun i ↦ (hε' i).le) hasSum_zero hc⟩, NNReal.hasSum_coe.1 hc,
      aε.trans_le' <| NNReal.coe_le_coe.1 hcε⟩

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i, s i)

Tactic:
rw [← iUnion_disjointed]
  exact m.isCaratheodory_iUnion_of_disjoint (m.isCaratheodory_disjointed h)
    (disjoint_disjointed _)

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

Goal state before:
pp: α : Type u_1
P : Set α → Prop
P0 : P ∅
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
Pu : P univ
s : Set α
⊢ (inducedOuterMeasure (fun x x_1 ↦ 0) P0 inducedOuterMeasure_zero._proof_1) s = 0 s

Tactic:
inducedOuterMeasure_eq_iInf PU (fun _ _ => by simp) (fun _ _ => by simp)

Goal state after:
α : Type u_1
P : Set α → Prop
P0 : P ∅
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
Pu : P univ
s : Set α
⊢ ⨅ t, ⨅ (_ : P t), ⨅ (_ : s ⊆ t), 0 = 0 s
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
inst✝ : Countable α
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ, p x) ↔ ∀ (x : α), μ {x} ≠ 0 → p x

Tactic:
ae_iff,

Goal state after:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable α
p : α → Prop
⊢ μ {a | ¬p a} = 0 ↔ ∀ (x : α), μ {x} ≠ 0 → p x
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
i : ι
hi : i ∈ S
⊢ m i ≤ generateFrom (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S)

Tactic:
← @generateFrom_measurableSet α (m i)

Goal state after:
case refine_2
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
i : ι
hi : i ∈ S
⊢ generateFrom {s | MeasurableSet s} ≤ generateFrom (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S)
Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f n x
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ aeSeq hf p i x = AEMeasurable.mk (f i) ⋯ x

Tactic:
by simp only [aeSeq, hx, if_true]

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

Goal state before:
pp: α : Type u_1
α₁ : Type u_6
α₂ : Type u_7
mα : MeasurableSpace α
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
i₁ : α₁ → α
i₂ : α₂ → α
s : Set α
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
h : univ ⊆ range i₁ ∪ range i₂
hs₁ : MeasurableSet (i₁ ⁻¹' s)
hs₂ : MeasurableSet (i₂ ⁻¹' s)
⊢ MeasurableSet s

Tactic:
convert! (hi₁.measurableSet_image' hs₁).union (hi₂.measurableSet_image' hs₂)
  simp [image_preimage_eq_range_inter, ← union_inter_distrib_right, univ_subset_iff.1 h]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable α
μ : Measure (α × β)
y : β
⊢ Prod.snd ⁻¹' {y} = ⋃ x, {(x, y)}

Tactic:
ext y

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable α
μ : Measure (α × β)
y✝ : β
y : α × β
⊢ y ∈ Prod.snd ⁻¹' {y✝} ↔ y ∈ ⋃ x, {(x, y✝)}
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
hf : AEMeasurable f μ
⊢ map f (c • μ) = c • map f μ

Tactic:
have hfc : AEMeasurable f (c • μ) :=
      ⟨hf.mk f, hf.measurable_mk, (ae_ennreal_smul_measure_iff hc).2 hf.ae_eq_mk⟩
    simp only [← mapₗ_mk_apply_of_aemeasurable hf, ← mapₗ_mk_apply_of_aemeasurable hfc, map_smulₛₗ,
      RingHom.id_apply]
    congr 1
    apply mapₗ_congr hfc.measurable_mk hf.measurable_mk
    exact .trans ((ae_ennreal_smul_measure_iff hc).1 hfc.ae_eq_mk.symm) hf.ae_eq_mk

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
h : ∑' (i : ι), μ (s i) ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, {i | x ∈ s i}.Finite

Tactic:
ae_iff,

Goal state after:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
h : ∑' (i : ι), μ (s i) ≠ ∞
⊢ μ {a | ¬{i | a ∈ s i}.Finite} = 0
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: case h
X : Type u_1
inst✝⁶ : LinearOrder X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : OrderTopology X
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : NoMaxOrder X
inst✝ : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h✝ : IsEmpty α
⊢ univ ∈ 𝓝 x ∧ {i | ((fun n ↦ Icc (f n) (g n)) i ∩ univ).Nonempty}.Finite

Tactic:
simp [Subsingleton.elim _ (∅ : Set α)]

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ∞
this : ∀ t ⊆ s k, μ t ≠ ∞
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) fun i ↦ s k \ s i

Tactic:
· exact hd.mono_comp _ fun _ _ => sdiff_subset_sdiff_right

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : μ (s i) ≠ ∞
this : Nonempty ι
t : ι → Set α := fun i ↦ s i ∩ {ω | Monotone fun x ↦ ω ∈ s x}
hst : ∀ (i : ι), s i =ᵐ[μ] t i
hMono : Monotone t
⊢ ⋂ i, s i =ᵐ[μ] ⋂ i, t i

Tactic:
← iInter_inter,

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : μ (s i) ≠ ∞
this : Nonempty ι
t : ι → Set α := fun i ↦ s i ∩ {ω | Monotone fun x ↦ ω ∈ s x}
hst : ∀ (i : ι), s i =ᵐ[μ] t i
hMono : Monotone t
⊢ ⋂ i, s i =ᵐ[μ] (⋂ i, s i) ∩ {ω | Monotone fun x ↦ ω ∈ s x}
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
c : ℝ≥0∞
hc : c ≠ ∞
⊢ IsFiniteMeasure (c • μ)

Tactic:
lift c to ℝ≥0 using hc
  exact MeasureTheory.isFiniteMeasureSMulNNReal

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
⊢ s = ⋃ x ∈ s, measurableAtom x

Tactic:
ext y

Goal state after:
α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
y : α
⊢ y ∈ s ↔ y ∈ ⋃ x ∈ s, measurableAtom x
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
m : ℕ → Measure α
hv : ∀ (n : ℕ), (m n) t ≠ ∞
hμ : μ = sum m
⊢ μ (toMeasurable μ t ∩ s) = μ (t ∩ s)

Tactic:
by
  -- we show that there is a measurable superset of `t` satisfying the conclusion for any
  -- measurable set `s`. It is built for each measure `mₙ` using `toMeasurable`
  -- (which is well behaved for finite measure sets thanks to `measure_toMeasurable_inter`), and
  -- then taking the intersection over `n`.
  have A : ∃ t', t' ⊇ t ∧ MeasurableSet t' ∧ ∀ u, MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u) := by
    let w n := toMeasurable (m n) t
    have T : t ⊆ ⋂ n, w n := subset_iInter (fun i ↦ subset_toMeasurable (m i) t)
    have M : MeasurableSet (⋂ n, w n) :=
      MeasurableSet.iInter (fun i ↦ measurableSet_toMeasurable (m i) t)
    refine ⟨⋂ n, w n, T, M, fun u hu ↦ ?_⟩
    refine le_antisymm ?_ (by gcongr)
    rw [hμ, sum_apply _ (M.inter hu)]
    apply le_trans _ (le_sum_apply _ _)
    apply ENNReal.tsum_le_tsum (fun i ↦ ?_)
    calc
    m i ((⋂ n, w n) ∩ u) ≤ m i (w i ∩ u) := by gcongr; apply iInter_subset
    _ = m i (t ∩ u) := measure_toMeasurable_inter hu (hv i)
  -- thanks to the definition of `toMeasurable`, the previous property will also be shared
  -- by `toMeasurable μ t`, which is enough to conclude the proof.
  rw [toMeasurable]
  split_ifs with ht
  · apply measure_congr
    exact ae_eq_set_inter ht.choose_spec.2.2 (ae_eq_refl _)
  · exact A.choose_spec.2.2 s hs

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

Goal state before:
pp: α : Type u_3
β : Type u_4
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableEq β
hm : m ≤ m0
f g : α → β
hf : Measurable f
hg : Measurable g
hfg : f =ᵐ[μ] g
⊢ ∀ᵐ (x : α) ∂μ.trim hm, f x = g x

Tactic:
ae_iff,

Goal state after:
α : Type u_3
β : Type u_4
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableEq β
hm : m ≤ m0
f g : α → β
hf : Measurable f
hg : Measurable g
hfg : f =ᵐ[μ] g
⊢ (μ.trim hm) {a | ¬f a = g a} = 0
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : ∀ᵐ (x : α) ∂μ.restrict sᶜ, f x = b
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t) = μ (f ⁻¹' t ∩ s)

Tactic:
ae_iff,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : (μ.restrict sᶜ) {a | ¬f a = b} = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t) = μ (f ⁻¹' t ∩ s)
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: case refine_2.inr
α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s✝ : Set α
h : HasCountableSeparatingOn α p s✝
hs : s✝ ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s✝, ∀ y ∈ s✝, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x y : α
hx : (x ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ i ∈ S, iᶜ ∈ l → x ∉ i
hy : (y ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ i ∈ S, iᶜ ∈ l → y ∉ i
s : Set α
hsS : s ∈ S
hsl : sᶜ ∈ l
⊢ x ∈ s ↔ y ∈ s

Tactic:
simp only [hx.2 s hsS hsl, hy.2 s hsS hsl]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∈ t
hs : MeasurableSet s
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ t ∈ Filter.map f (ae (μ.restrict s))

Tactic:
classical
  simp_rw [mem_map, mem_ae_iff]
  rw [Measure.restrict_apply' hs, Set.indicator_preimage, Set.ite]
  simp_rw [Set.compl_union, Set.compl_inter]
  change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun _ => (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0
  simp only [ht, ← Set.compl_eq_univ_sdiff, compl_compl, if_true,
    Set.preimage_const]
  simp_rw [Set.union_inter_distrib_right, Set.compl_inter_self s, Set.union_empty]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
⊢ MeasurableSet (measurableAtom x)

Tactic:
rw [measurableAtom_eq_countablyGeneratedAtom_natGeneratingSequence]
  exact measurableSet_countablyGeneratedAtom _

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
this : MeasurableSpace α := generateFrom S
x y : α
hxy : ∀ s ∈ S, x ∈ s ↔ y ∈ s
⊢ x = y

Tactic:
rw [← forall_generateFrom_mem_iff_mem_iff] at hxy

Goal state after:
α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
this : MeasurableSpace α := generateFrom S
x y : α
hxy : ∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)
⊢ x = y
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : Nonempty β
inst✝ : SeparatesPoints β
f : α → β
hf : Measurable f
a₁ a₂ : α
h : f a₁ ≠ f a₂
s : Set β
hs : MeasurableSet s
hx : f a₁ ∈ s
hy : f a₂ ∉ s
h' : f ⁻¹' s = ∅
⊢ False

Tactic:
absurd hx
      simp [← mem_preimage, h']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : SeparatesPoints α
x : α
s : (y : α) → x ≠ y → Set α
hsm : ∀ (y : α) (h : x ≠ y), MeasurableSet (s y h)
hxs : ∀ (y : α) (h : x ≠ y), x ∈ s y h
hys : ∀ (y : α) (h : x ≠ y), y ∉ s y h
⊢ {x} = ⋂ b, ⋂ (b_1 : x ≠ b), s b b_1

Tactic:
ext y

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : SeparatesPoints α
x : α
s : (y : α) → x ≠ y → Set α
hsm : ∀ (y : α) (h : x ≠ y), MeasurableSet (s y h)
hxs : ∀ (y : α) (h : x ≠ y), x ∈ s y h
hys : ∀ (y : α) (h : x ≠ y), y ∉ s y h
y : α
⊢ y ∈ {x} ↔ y ∈ ⋂ b, ⋂ (b_1 : x ≠ b), s b b_1
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case refine_2.refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n
hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n)
heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ
⊢ ∀ (b : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑b) = min (μ (t' ↑b)) (ν (t' ↑b))

Tactic:
rw [Subtype.forall]
        intro n hn; simpa

Goal state after: