mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
x : α × β
⊢ Metric.ball 0 (dist x 0 + 1) ∈ 𝓝 x

Tactic:
exact Metric.isOpen_ball.mem_nhds (by simp)

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ ratio (Dilation.id α) = 1

pp: case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
h : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (Dilation.id α) = 1

Tactic:
· rw [ratio, if_pos h]

Goal state after:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
h : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (Dilation.id α) = 1
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ diam (⇑f '' s) = ↑(ratio f) * diam s

Tactic:
by
  simp [diam, ediam_image, ENNReal.toReal_mul]

Goal state after:
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Finset ι
hf : DependsOn f ↑s
i : ι
y : π i
⊢ DependsOn (fun x ↦ f (updateFinset x {i} (uniqueElim y))) ↑(s.erase i)

Tactic:
erase_eq,

Goal state after:
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Finset ι
hf : DependsOn f ↑s
i : ι
y : π i
⊢ DependsOn (fun x ↦ f (updateFinset x {i} (uniqueElim y))) ↑(s \ {i})
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: case neg
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : ¬j = i
⊢ (TProd.mk (i :: is) f).elim hj = f j

Tactic:
· rw [TProd.elim_of_ne _ hji, snd_mk, elim_mk is]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
a b c : IterateMulAct f
⊢ (a * b * c).val = (a * (b * c)).val

Tactic:
apply Nat.add_assoc

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : MeasurableSet s
⊢ Measurable (s.indicator fun x ↦ b)

Tactic:
exact measurable_const.indicator h

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ ∩ s₂)

Tactic:
by
  rw [inter_eq_compl_compl_union_compl]
  exact (h₁.compl.union h₂.compl).compl

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

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst✝⁵ : NormedField 𝕜✝
inst✝⁴ : SeminormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜✝ 𝕜'
𝕜 : Type ?u.15
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : CharZero 𝕜
inst✝ : NormedAlgebra ℝ 𝕜
q : ℚ
x : 𝕜
⊢ ‖(q • 1) • x‖ ≤ ‖q‖ * ‖x‖

Tactic:
Rat.smul_one_eq_cast,

Goal state after:
𝕜✝ : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst✝⁵ : NormedField 𝕜✝
inst✝⁴ : SeminormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜✝ 𝕜'
𝕜 : Type ?u.15
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : CharZero 𝕜
inst✝ : NormedAlgebra ℝ 𝕜
q : ℚ
x : 𝕜
⊢ ‖↑q • x‖ ≤ ‖q‖ * ‖x‖
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_3
ι : Sort u_4
f : α → β
m : ι → OuterMeasure β
s : Set α
⊢ ((comap f) (⨆ i, m i)) s = (⨆ i, (comap f) (m i)) s

Tactic:
by simp only [comap_apply, iSup_apply]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : α → Prop
h : Measurable p
⊢ MeasurableSet {a | p a}

Tactic:
simpa using h (measurableSet_singleton True)

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
t : ι → Set α
h : univ.PairwiseDisjoint t
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x = ∑' (i : ι) (x : ↑(t i)), f ↑x

Tactic:
← tsum_univ

Goal state after:
α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
t : ι → Set α
h : univ.PairwiseDisjoint t
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x = ∑' (x : ↑univ) (x_1 : ↑(t ↑x)), f ↑x_1
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:
by
    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.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case mpr
f : ℕ → ℝ≥0
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop atTop → ¬Summable f

Tactic:
· rintro hnat ⟨r, hr⟩
    exact not_tendsto_nhds_of_tendsto_atTop hnat _ (hasSum_iff_tendsto_nat.1 hr)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ (∀ (x_1 : Set β), IsClosed[inst✝] x_1 → (f x ∩ x_1ᶜ).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ x_1ᶜ).Nonempty) ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t

Tactic:
refine forall₂_congr fun t ht ↦ ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
s : Set α
t : Set β
ht : IsClosed[inst✝] t
⊢ ((f x ∩ tᶜ).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ tᶜ).Nonempty) ↔ (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case neg
α : Type u_1
g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
hsf : sf ≠ ∞
hg : HasSum g sg
hsg : ¬sg = ∞
hg' : ∀ (x : α), g x ≠ ∞
f : α → ℝ≥0
h : ∀ (a : α), (fun i ↦ ↑(f i)) a ≤ g a
hi : (fun i ↦ ↑(f i)) i < g i
hf : HasSum (fun i ↦ ↑(f i)) sf
⊢ sf < sg

Tactic:
lift g to α → ℝ≥0 using hg'

Goal state after:
case neg
α : Type u_1
sf sg : ℝ≥0∞
i : α
hsf : sf ≠ ∞
hsg : ¬sg = ∞
f : α → ℝ≥0
hf : HasSum (fun i ↦ ↑(f i)) sf
g : α → ℝ≥0
hg : HasSum (fun i ↦ ↑(g i)) sg
h : ∀ (a : α), (fun i ↦ ↑(f i)) a ≤ (fun i ↦ ↑(g i)) a
hi : (fun i ↦ ↑(f i)) i < (fun i ↦ ↑(g i)) i
⊢ sf < sg
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
⊢ a * 0 = 0

Tactic:
mul_zero a

Goal state after:
a : EReal
⊢ 0 = 0
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case inl
α : Type u_4
s : Finset α
⊢ ∑' (x : ↑↑s), 1 = ↑(↑s).encard

Tactic:
simp [tsum_fintype]

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

Goal state before:
pp: α : Type u_4
⊢ ∑' (x : α), 1 = ↑(ENat.card α)

Tactic:
← tsum_univ

Goal state after:
α : Type u_4
⊢ ∑' (x : ↑univ), 1 = ↑(ENat.card α)
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_4
c : ℝ≥0∞
⊢ ∑' (x : α), c = ↑(ENat.card α) * c

Tactic:
← tsum_univ

Goal state after:
α : Type u_4
c : ℝ≥0∞
⊢ ∑' (x : ↑univ), c = ↑(ENat.card α) * c
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
⊢ LowerSemicontinuousAt f x ↔ f x ≤ liminf f (𝓝 x)

Tactic:
rw [← lowerSemicontinuousWithinAt_univ_iff, lowerSemicontinuousWithinAt_iff_le_liminf,
    ← nhdsWithin_univ]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y

Tactic:
obtain ⟨u, v, u_open, xu, v_open, xv, h⟩ :
    ∃ u v : Set γ,
      IsOpen u ∧ f x ∈ u ∧ IsOpen v ∧ g x ∈ v ∧ u ×ˢ v ⊆ { p : γ × γ | y < p.fst + p.snd } :=
    mem_nhds_prod_iff'.1 (hcont (isOpen_Ioi.mem_nhds hy))

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
⊢ (Monotone fun s ↦ ⨆ (_ : s.Nonempty), m s) ∨ Surjective f

pp: case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
⊢ OuterMeasure.ofFunction (fun s ↦ ⨆ (_ : (f '' s).Nonempty), m (f '' s)) ⋯ = boundedBy fun s ↦ m (f '' s)

Tactic:
· refine h.imp (fun H s t hst => iSup_le fun hs => ?_) id
    have ht : t.Nonempty := hs.mono hst
    exact (@H ⟨s, hs⟩ ⟨t, ht⟩ hst).trans (le_iSup (fun _ : t.Nonempty => m t) ht)

Goal state after:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
⊢ OuterMeasure.ofFunction (fun s ↦ ⨆ (_ : (f '' s).Nonempty), m (f '' s)) ⋯ = boundedBy fun s ↦ m (f '' s)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
ht_empty : t = ∅
⊢ ⋂ x ∈ t, f x ∈ π i ∨ ⋂ x ∈ t, f x ∈ {univ}

Tactic:
simp [ht_empty, iInter_univ, Set.mem_singleton univ]

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

Goal state before:
pp: α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 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) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
hs : (inducedOuterMeasure m P0 m0) s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
h1t : P t
h2t : s ⊆ t
h3t : m t ⋯ < (inducedOuterMeasure m P0 m0) s + ε
⊢ ∃ t, P t ∧ s ⊆ t ∧ (inducedOuterMeasure m P0 m0) t ≤ (inducedOuterMeasure m P0 m0) s + ε

Tactic:
exact
    ⟨t, h1t, h2t, le_trans (le_of_eq <| inducedOuterMeasure_eq' _ msU m_mono h1t) (le_of_lt h3t)⟩

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∉ p2
⊢ f1 n ∩ univ ∈ π n

Tactic:
simp [hf1m n hn1]

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

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

Tactic:
refine ⟨fun h => ⟨?_, ?_⟩, fun h => measure_union_lt_top h.1 h.2⟩
  · exact (measure_mono Set.subset_union_left).trans_lt h
  · exact (measure_mono Set.subset_union_right).trans_lt h

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s t : Set α
left✝¹ : s ⊆ t
left✝ : MeasurableSet t
hμt : (⨆ i, μ i.down) t = (⨆ i, μ i.down).trim s ∧ ∀ (x : PLift ι), ((μ ∘ PLift.down) x) t = ((μ ∘ PLift.down) x).trim s
⊢ ⨆ i, (μ i.down) t = ⨆ i, (μ i.down).trim s

Tactic:
exact iSup_congr hμt.2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
⊢ f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) ∪ ∅ = toMeasurable μ (f ⁻¹' s)

Tactic:
union_empty,

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
⊢ f ⁻¹' f '' toMeasurable μ (f ⁻¹' s) = toMeasurable μ (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
h : map f μ = map f ν
s : Set α
hs : MeasurableSet s
⊢ μ (f ⁻¹' f '' s) = ν (f ⁻¹' f '' s)

Tactic:
← hf.map_apply,

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
h : map f μ = map f ν
s : Set α
hs : MeasurableSet s
⊢ (map f μ) (f '' s) = ν (f ⁻¹' f '' s)
Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : ℕ → Set α
t : Set α
h : ∀ (n : ℕ), s n =ᵐ[μ] t
⊢ limsup s atTop =ᵐ[μ] t

Tactic:
by
  simp only [eventuallyEq_set, ← eventually_countable_forall] at h
  refine eventuallyEq_set.2 <| h.mono fun x hx ↦ ?_
  simp [mem_limsup_iff_frequently_mem, hx]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
⊢ μ (s₁ ∩ s₂) + μ (s₁ \ s₂) ≤ μ s₂ + μ (s₁ \ s₂)

Tactic:
by
    gcongr; apply inter_subset_right

Goal state after:
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: case neg
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
h : Tendsto Subtype.val atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
⊢ False

Tactic:
rcases h.eventually eventually_mem_nhdsWithin |>.and (eventually_ge_atTop ⟨a, has⟩) |>.exists
      with ⟨⟨c, hcs⟩, hcb, hac⟩

Goal state after:
case neg
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
h : Tendsto Subtype.val atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
c : X
hcs : c ∈ s
hcb : ↑⟨c, hcs⟩ ∈ Iio b
hac : ⟨a, has⟩ ≤ ⟨c, hcs⟩
⊢ False
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
⊢ map Subtype.val atTop = 𝓝[<] b

Tactic:
rcases eq_empty_or_nonempty (Iio b) with (hb' | ⟨a, ha⟩)

Goal state after:
case inl
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
hb' : Iio b = ∅
⊢ map Subtype.val atTop = 𝓝[<] b

case inr
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
a : X
ha : a ∈ Iio b
⊢ map Subtype.val atTop = 𝓝[<] b
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc : ∑' (i : ℕ), (sfiniteSeq μ i) univ * ↑(c i) < ∞
s : Set α
| (sum (sfiniteSeq μ)) s = 0

Tactic:
sum_apply_of_countable

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc : ∑' (i : ℕ), (sfiniteSeq μ i) univ * ↑(c i) < ∞
s : Set α
| ∑' (i : ℕ), (sfiniteSeq μ i) s = 0
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite ν
⊢ μ.restrict (⋃ i, spanningSets ν i) = μ

Tactic:
iUnion_spanningSets,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite ν
⊢ μ.restrict univ = μ
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ μ.toOuterMeasure (t ∩ s) = μ (t ∩ s)

Tactic:
toOuterMeasure_apply

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ μ (t ∩ s) = μ (t ∩ s)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ s = s ∩ ⋃ i, spanningSets μ i

Tactic:
iUnion_spanningSets,

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ s = s ∩ univ
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ ≤ ν
h_univ : μ univ = ν univ
s : Set α
hs : MeasurableSet s
x✝ : s.Nonempty
h_lt : μ s < ν s
h_disj : Disjoint s sᶜ
⊢ False

Tactic:
← union_compl_self s,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ ≤ ν
s : Set α
h_univ : μ (s ∪ sᶜ) = ν (s ∪ sᶜ)
hs : MeasurableSet s
x✝ : s.Nonempty
h_lt : μ s < ν s
h_disj : Disjoint s sᶜ
⊢ False
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

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
⊢ IsFiniteMeasure (↑c • μ)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝³ : TopologicalSpace β
inst✝² : T1Space β
inst✝¹ : SecondCountableTopology β
inst✝ : Nonempty β
f : α → β
m : OuterMeasure β := (OuterMeasure.map f) μ.toOuterMeasure
h : ∀ (b : β), m {b}ᶜ ≠ 0
inhabited_h : Inhabited β
⊢ ∃ a b, a ≠ b ∧ (∀ s ∈ 𝓝 a, 0 < μ (f ⁻¹' s)) ∧ ∀ t ∈ 𝓝 b, 0 < μ (f ⁻¹' t)

Tactic:
have : m univ ≠ 0 := ne_bot_of_le_ne_bot (h default) (measure_mono <| subset_univ _)

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝³ : TopologicalSpace β
inst✝² : T1Space β
inst✝¹ : SecondCountableTopology β
inst✝ : Nonempty β
f : α → β
m : OuterMeasure β := (OuterMeasure.map f) μ.toOuterMeasure
h : ∀ (b : β), m {b}ᶜ ≠ 0
inhabited_h : Inhabited β
this : m univ ≠ 0
⊢ ∃ a b, a ≠ b ∧ (∀ s ∈ 𝓝 a, 0 < μ (f ⁻¹' s)) ∧ ∀ t ∈ 𝓝 b, 0 < μ (f ⁻¹' t)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ∞
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m ↦ μ (⋂ n, ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
hzero : μ (⋂ n, f n) = 0
⊢ Tendsto F atTop (𝓝 0)

Tactic:
rw [← hzero]

Goal state after:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
ε : ℝ≥0∞
hε : 0 < ε
hfin : ∃ i, μ (f i) ≠ ∞
hfem : ⋂ n, f n = ∅
F : ι → ℝ≥0∞ := fun m ↦ μ (⋂ n, ⋂ (_ : n ≤ m), f n)
hFAnti : Antitone F
hzero : μ (⋂ n, f n) = 0
⊢ Tendsto F atTop (𝓝 (μ (⋂ n, f n)))
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
x : α
hx : x ∈ t
⊢ x ∈ ⋃ i, t ∩ w i

Tactic:
rcases mem_iUnion.1 (hv hx) with ⟨n, hn⟩

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
x : α
hx : x ∈ t
n : ℕ
hn : x ∈ v n
⊢ x ∈ ⋃ i, t ∩ w i
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
⊢ ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)

Tactic:
refine ⟨t', tt', MeasurableSet.iUnion fun n => measurableSet_toMeasurable μ _, fun u hu => ?_⟩

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ μ (t' ∩ u) = μ (t ∩ u)
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (Measure.map f (μ.trim ⋯)) s = (Measure.map f μ) s

Tactic:
rw [Measure.map_apply hf hs, Measure.map_apply _ hs, trim_measurableSet_eq]

Goal state after:
case hs
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)

α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable f
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
inst✝ : Countable ι
μ : ι → Measure α
s t : Set α
ht : MeasurableSet t
⊢ (sum μ) (t ∩ s) = ∑' (i : ι), (μ i) (t ∩ s)

Tactic:
sum_apply_of_countable

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
⊢ MeasurableSet s

Tactic:
refine OuterMeasure.boundedBy_caratheodory fun t => ?_

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
⊢ OuterMeasure.sInfGen (toOuterMeasure '' m) (t ∩ s) + OuterMeasure.sInfGen (toOuterMeasure '' m) (t \ s) ≤
    OuterMeasure.sInfGen (toOuterMeasure '' m) t
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
hs : MeasurableSet s
⊢ (μ.restrict (⋃ i, spanningSets μ i)) s = μ s

Tactic:
iUnion_spanningSets,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
hs : MeasurableSet s
⊢ (μ.restrict univ) s = μ s