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 : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l s
hG : TendstoLocallyUniformlyOn G g l s
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
⊢ TendstoLocallyUniformlyOn (F • G) (f • g) l s

Tactic:
by
  have H := hF.prodMk hG
  rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at *
  intro x hx
  rcases (hf x hx).sup (hg x hx) with ⟨C, hC⟩
  simp_rw [Filter.eventually_map, max_le_iff] at hC
  refine Tendsto.comp
    (Metric.isBounded_ball (x := (0 : α × β)) (r := C + 1)).uniformContinuousOn_smul
    (tendsto_inf.mpr ⟨H x hx, tendsto_principal.mpr ?_⟩)
  filter_upwards [hF x hx (Metric.dist_mem_uniformity one_pos),
    hG x hx (Metric.dist_mem_uniformity one_pos), tendsto_snd hC] with ⟨n, y⟩ hFn hGn hfg
  simp only [mem_prod, Metric.mem_ball, Prod.dist_eq, Prod.fst_zero, Prod.snd_zero, sup_lt_iff,
    mem_preimage, mem_ofPred] at hFn hGn hfg ⊢
  grw [dist_triangle_left (F n y) 0 (f y), dist_triangle_left (G n y) 0 (g y)]
  constructor <;> constructor <;> linarith

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

Goal state before:
pp: G : Type v
inst✝² : Group G
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x ↦ x * a) ⁻¹' eball b r = eball (b / a) r

Tactic:
rw [div_eq_mul_inv]
  exact preimage_smul_eball (MulOpposite.op a) b r

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Finset

Goal state before:
pp: case pos
ι : Type u_1
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
a : G₀
inst✝ : MulPosReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
h : 0 = a
⊢ s.sup' hs f * a = s.sup' hs fun i ↦ f i * a

Tactic:
simp [← h]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Finset

Goal state before:
pp: case pos
ι : Type u_1
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
a : G₀
inst✝ : PosMulReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
h : 0 = a
⊢ a * s.sup' hs f = s.sup' hs fun i ↦ a * f i

Tactic:
simp [← h]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Finset

Goal state before:
pp: case pos
ι : Type u_1
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
a : G₀
inst✝ : MulPosReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
h : 0 = a
⊢ s.sup' hs f / a = s.sup' hs fun i ↦ f i / a

Tactic:
simp [← h]

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq fun n ↦ ∏ k ∈ range (n + 1), v k
⊢ CauchySeq fun n ↦ ∏ k ∈ range (n + 1), u k

Tactic:
let d : ℕ → E := fun n => ∏ k ∈ range (n + 1), u k / v k
  rw [show (fun n => ∏ k ∈ range (n + 1), u k) = d * fun n => ∏ k ∈ range (n + 1), v k
      by ext n; simp [d]]
  suffices ∀ n ≥ N, d n = d N from (tendsto_atTop_of_eventually_const this).cauchySeq.mul hv
  intro n hn
  dsimp [d]
  rw [eventually_constant_prod (N := N + 1) _ (by gcongr)]
  intro m hm
  simp [huv m (le_of_lt hm)]

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

Goal state before:
pp: α : Type u_2
inst✝ : NontriviallyNormedField α
r : ℝ
hr : 0 < r
w : α
hw : r⁻¹ < ‖w‖
⊢ 0 < ‖w⁻¹‖ ∧ ‖w⁻¹‖ < r

Tactic:
← Set.mem_Ioo,

Goal state after:
α : Type u_2
inst✝ : NontriviallyNormedField α
r : ℝ
hr : 0 < r
w : α
hw : r⁻¹ < ‖w‖
⊢ ‖w⁻¹‖ ∈ Set.Ioo 0 r
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ ‖x‖₊ * y.toNNReal = ‖x * y‖₊

Tactic:
by
  rw [mul_comm, mul_comm x, toNNReal_mul_nnnorm x hy]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝⁵ : SeminormedAddCommGroup α
inst✝⁴ : One α
inst✝³ : NormOneClass α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : One β
inst✝ : NormOneClass β
⊢ ‖1‖ = 1

Tactic:
simp [Prod.norm_def]

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

Goal state before:
pp: α : Type u_2
inst✝³ : NormedAddCommGroup α
inst✝² : MulOneClass α
inst✝¹ : NormMulClass α
inst✝ : Nontrivial α
⊢ ‖1‖ = 1

Tactic:
obtain ⟨u, hu⟩ := exists_ne (0 : α)

Goal state after:
α : Type u_2
inst✝³ : NormedAddCommGroup α
inst✝² : MulOneClass α
inst✝¹ : NormMulClass α
inst✝ : Nontrivial α
u : α
hu : u ≠ 0
⊢ ‖1‖ = 1
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : ⋃ n, s n = univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
⊢ univ ×ˢ univ = univ

Tactic:
univ_prod_univ

Goal state after:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : ⋃ n, s n = univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
⊢ univ = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
ι : Sort u_7
m : ι → MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ ∀ (i : ι), MeasurableSet s

Tactic:
rw [iInf, measurableSet_sInf, forall_mem_range]

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:
by
  simpa using norm_natCast_eq_mul_norm_one α a

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
⊢ (fun a ↦ if 0 < a then 1 else if a < 0 then -1 else 0) a ≤ (fun a ↦ if 0 < a then 1 else if a < 0 then -1 else 0) b

Tactic:
by
    dsimp
    split_ifs with h₁ h₂ h₃ h₄ _ _ h₂ h₃ <;> try constructor
    · cases lt_irrefl 0 (h₁.trans <| h.trans_lt h₃)
    · cases h₂ (h₁.trans_le h)
    · cases h₄ (h.trans_lt h₃)

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 = a
⊢ 0 ≤ sign a ↔ 0 ≤ a

Tactic:
simp [← h]

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 = a
⊢ sign a ≤ 0 ↔ a ≤ 0

Tactic:
simp [← h]

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

Goal state before:
pp: α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ∞
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
have f_ne_top : ∀ n, f n ≠ ∞ := ENNReal.ne_top_of_tsum_ne_top hf

Goal state after:
α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ∞
f_ne_top : ∀ (n : α), f n ≠ ∞
⊢ Tendsto f cofinite (𝓝 0)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mp.pos
x y : EReal
h : ↑pos * ↑x.abs ≤ ↑pos * ↑y.abs
hs : sign x = sign y
hy : sign y = pos
⊢ pos = neg ∧ pos = neg ∧ y.abs ≤ x.abs ∨ pos = zero ∧ pos = zero ∨ pos = pos ∧ pos = pos ∧ x.abs ≤ y.abs

Tactic:
· right; right; simpa using h

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≠ ∞
⊢ (∑' (a : α), f a).toReal = ∑' (a : α), (f a).toReal

Tactic:
by
  simp only [ENNReal.toReal, tsum_toNNReal_eq hf, NNReal.coe_tsum]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → β
inst✝ : Preorder β
I : Set ι
hfy : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
M : α → ι
M_mem : ∀ x ∈ s, M x ∈ I
M_max : ∀ x ∈ s, IsMaxOn (fun y ↦ f y x) I (M x)
x : α
hx : x ∈ s
b : β
hb : (fun x ↦ f (M x) x) x > b
⊢ ∀ x_1 ∈ s, (fun x1 x2 ↦ f (M x) x1 > x2) x_1 b → (fun x1 x2 ↦ (fun x ↦ f (M x) x) x1 > x2) x_1 b

Tactic:
intro z hz h

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → β
inst✝ : Preorder β
I : Set ι
hfy : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
M : α → ι
M_mem : ∀ x ∈ s, M x ∈ I
M_max : ∀ x ∈ s, IsMaxOn (fun y ↦ f y x) I (M x)
x : α
hx : x ∈ s
b : β
hb : (fun x ↦ f (M x) x) x > b
z : α
hz : z ∈ s
h : f (M x) z > b
⊢ (fun x ↦ f (M x) x) z > b
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
h : SemicontinuousWithinAt (fun x1 x2 ↦ f x1 > x2) s x
hf : liminf f (𝓝[s] x) < f x
⊢ False

Tactic:
obtain ⟨z, ltz, y, ylt, h₁⟩ := hf.exists_disjoint_Iio_Ioi

Goal state after:
case mp
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
h : SemicontinuousWithinAt (fun x1 x2 ↦ f x1 > x2) s x
hf : liminf f (𝓝[s] x) < f x
z : γ
ltz : z > liminf f (𝓝[s] x)
y : γ
ylt : y < f x
h₁ : ∀ x < z, ∀ y_1 > y, x < y_1
⊢ False
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:
by
  rw [← lowerSemicontinuousWithinAt_univ_iff, lowerSemicontinuousWithinAt_iff_le_liminf,
    ← nhdsWithin_univ]

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

Goal state before:
pp: case neg
α : 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
hx : x ∉ s
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1

Tactic:
· filter_upwards [(continuous_fst.tendsto _).eventually (hs.isOpen_compl.eventually_mem hx)]
        with _ h₁ h₂ using (h₁ h₂).elim

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

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
a : EReal
ha : a ∈ Ioo 0 (liminf u f)
b : EReal
hb : b ∈ Ioo 0 (liminf v f)
c : EReal
c_ab : c < a * b
⊢ ∀ᶠ (a : α) in f, c < u a * v a

Tactic:
filter_upwards [eventually_lt_of_lt_liminf (mem_Ioo.1 ha).2,
    eventually_lt_of_lt_liminf (mem_Ioo.1 hb).2] with x xa xb

Goal state after:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
a : EReal
ha : a ∈ Ioo 0 (liminf u f)
b : EReal
hb : b ∈ Ioo 0 (liminf v f)
c : EReal
c_ab : c < a * b
x : α
xa : a < u x
xb : b < v x
⊢ c < u x * v x
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case e'_4
α : Type u_1
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)

Tactic:
simp only [pow_add, ENNReal.tsum_mul_left, ENNReal.tsum_geometric, div_eq_mul_inv, mul_assoc]

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

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ∞
x✝¹ : β
x✝ : α
⊢ x✝ ∈ ⋃ (_ : x✝¹ ∈ s), f x✝¹ ↔ x✝ ∈ ⋃ (_ : x✝¹ ∈ hs.toFinset), f x✝¹

Tactic:
rw [Finite.mem_toFinset]

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

Goal state before:
pp: case a
α : 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 α := ⋯
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := ⋯
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
⊢ y ∈ f '' iInter X

Tactic:
hf.injective.injOn.image_iInter_eq

Goal state after:
case a
α : 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
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
⊢ y ∈ ⋂ i, f '' F^[i] univ
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hd : AEDisjoint μ s t
⊢ μ (s ∪ t) = μ s + μ t

Tactic:
by rw [union_comm, measure_union₀ hs (AEDisjoint.symm hd), add_comm]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
k : ℕ
hs : f ⁻¹' s =ᵐ[μ] s
⊢ f^[k] ⁻¹' s =ᵐ[μ] s

Tactic:
induction k with

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
t s : Set α
hm : NullMeasurableSet t μ
h_fin : μ t ≠ ∞
⊢ μ (s \ t) + μ t = μ (s ∪ t)

Tactic:
by rw [add_comm, measure_add_sdiff hm, union_comm]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (t \ s) = 0
⊢ s ∪ t ≤ᵐ[μ] s

Tactic:
by rwa [ae_le_set, union_sdiff_left]

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

Goal state before:
pp: case inr
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✝ : Nonempty α
⊢ ∃ t ∈ 𝓝 x, {i | ((fun n ↦ Icc (f n) (g n)) i ∩ t).Nonempty}.Finite

Tactic:
obtain ⟨x_L, hx_L⟩ := exists_lt x

Goal state after:
case inr
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✝ : Nonempty α
x_L : X
hx_L : x_L < x
⊢ ∃ t ∈ 𝓝 x, {i | ((fun n ↦ Icc (f n) (g n)) i ∩ t).Nonempty}.Finite
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ u < μ s + μ t
⊢ ¬Disjoint s t

Tactic:
contrapose! h

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : Disjoint s t
⊢ μ s + μ t ≤ μ u
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ ¬IsFiniteMeasure μ ↔ μ univ = ∞

Tactic:
by simp [isFiniteMeasure_iff]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ.cofinite = ⊥ ↔ IsFiniteMeasure μ

Tactic:
by
  simp [← empty_mem_iff_bot, μ.mem_cofinite, isFiniteMeasure_iff]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
T : ℕ → Set α := fun n ↦ toMeasurable μ (t n)
Td : ℕ → Set α := disjointed T
hm : ∀ (n : ℕ), MeasurableSet (Td n)
I : Finset ℕ
⊢ ∑ n ∈ I, μ (Td n) ≤ ⨆ n, μ (t n)

Tactic:
by
      rcases hd.finset_le I with ⟨N, hN⟩
      calc
        (∑ n ∈ I, μ (Td n)) = μ (⋃ n ∈ I, Td n) :=
          (measure_biUnion_finset ((disjoint_disjointed T).set_pairwise I) fun n _ => hm n).symm
        _ ≤ μ (⋃ n ∈ I, T n) := measure_mono (iUnion₂_mono fun n _hn => disjointed_subset _ _)
        _ = μ (⋃ n ∈ I, t n) := measure_biUnion_toMeasurable I.countable_toSet _
        _ ≤ μ (t N) := measure_mono (iUnion₂_subset hN)
        _ ≤ ⨆ n, μ (t n) := le_iSup (μ ∘ t) N

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

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

Tactic:
rw [← toOuterMeasure_apply,
    Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict hs,
    OuterMeasure.restrict_apply s t _, toOuterMeasure_apply]

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

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⨆ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : ℕ → Set (Set α)
D_mem : ∀ (n : ℕ), D n ∈ {D | D ⊆ C ∧ D.Countable}
huD : ∀ (n : ℕ), u n < μ (⋃₀ D n)
hD : ⋃ n, D n ∈ {D | D ⊆ C ∧ D.Countable}
⊢ ∃ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D) = m

Tactic:
refine ⟨⋃ n, D n, hD, ?_⟩

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⨆ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : ℕ → Set (Set α)
D_mem : ∀ (n : ℕ), D n ∈ {D | D ⊆ C ∧ D.Countable}
huD : ∀ (n : ℕ), u n < μ (⋃₀ D n)
hD : ⋃ n, D n ∈ {D | D ⊆ C ∧ D.Countable}
⊢ μ (⋃₀ ⋃ n, D n) = m
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, μ s = ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : μ univ = ν univ
s : Set α
hs : MeasurableSet s
⊢ ν univ < ∞

Tactic:
← h_univ

Goal state after:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, μ s = ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : μ univ = ν univ
s : Set α
hs : MeasurableSet s
⊢ μ univ < ∞
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
this : ν (u ∩ t) = 0 → μ (f ⁻¹' u ∩ s) = 0
⊢ (ν.restrict t) u = 0 → (map f (μ.restrict s)) u = 0

Tactic:
by simpa [hum, hf.measurable, hf.measurable hum]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ∞
h_eq : ∀ s ∈ S, μ s = ν s
⊢ ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)

Tactic:
intro t ht s hs

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ∞
h_eq : ∀ s ∈ S, μ s = ν s
t : Set α
ht : t ∈ T
s : Set α
hs : s ∈ S
⊢ μ (s ∩ t) = ν (s ∩ t)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case inl
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ∞
h_eq : ∀ s ∈ S, μ s = ν s
t : Set α
ht : t ∈ T
s : Set α
hs : s ∈ S
H : s ∩ t = ∅
⊢ μ (s ∩ t) = ν (s ∩ t)

Tactic:
simp only [H, measure_empty]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
⊢ ofMeasurable (fun x x_1 ↦ 0) ⋯ ⋯ = 0

Tactic:
ext s
  simp [ofMeasurable, ← toOuterMeasure_apply, inducedOuterMeasure_zero MeasurableSet.iUnion]

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:
OuterMeasure.sInf_eq_boundedBy_sInfGen

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : Set (Measure α)
x✝ : MeasurableSpace α
f : ℕ → Set α
a✝¹ : ∀ (i : ℕ), MeasurableSet (f i)
a✝ : Pairwise (Disjoint on f)
hne : ¬(⋃ i, f i).Nonempty
⊢ ∑' (i : ℕ), ⊤ (f i) ≤ ⊤ (⋃ i, f i)

Tactic:
simp_all [Set.not_nonempty_iff_eq_empty]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hc : S.Countable
hμ : ∀ s ∈ S, μ s < ∞
hU : ⋃₀ S = univ
⊢ SigmaFinite μ

Tactic:
by
  obtain ⟨s, hμ, hs⟩ : ∃ s : ℕ → Set α, (∀ n, μ (s n) < ∞) ∧ ⋃ n, s n = univ :=
    (@exists_seq_cover_iff_countable _ (fun x => μ x < ∞) ⟨∅, by simp⟩).2 ⟨S, hc, hμ, hU⟩
  exact ⟨⟨⟨fun n => s n, fun _ => trivial, hμ, hs⟩⟩⟩

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

Goal state before:
pp: case refine_3.refine_1
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
q : (ℕ → Prop) → Prop
htq : t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
x : α
h : ∀ (i : ℕ → Prop), q i → x ∉ countablyGeneratedAtom α i
⊢ ¬q fun n ↦ x ∈ natGeneratingSequence α n

Tactic:
contrapose! h

Goal state after:
case refine_3.refine_1
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
q : (ℕ → Prop) → Prop
htq : t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
x : α
h : q fun n ↦ x ∈ natGeneratingSequence α n
⊢ ∃ i, q i ∧ x ∈ countablyGeneratedAtom α i
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
⊢ (∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) ↔ s.indicator f =ᵐ[μ] s.indicator g

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩ <;> filter_upwards [h] with x hx

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
x : α
hx : x ∈ s → f x = g x
⊢ s.indicator f x = s.indicator g x

α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : s.indicator f =ᵐ[μ] s.indicator g
x : α
hx : s.indicator f x = s.indicator g x
⊢ x ∈ s → f x = g x
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : SeparatesPoints α
x y : α
h : x ≠ y
⊢ ∃ s, MeasurableSet s ∧ x ∈ s ∧ y ∉ s

Tactic:
contrapose! h

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : SeparatesPoints α
x y : α
h : ∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s
⊢ x = y
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1.succ.inl
α : Type u_1
t : ℕ → Set α
n : ℕ
ih : ∀ u ∈ memPartition t n, MeasurableSet u
v : Set α
hv : v ∈ memPartition t n
⊢ MeasurableSet (v ∩ t n)

pp: case refine_1.succ.inr
α : Type u_1
t : ℕ → Set α
n : ℕ
ih : ∀ u ∈ memPartition t n, MeasurableSet u
v : Set α
hv : v ∈ memPartition t n
⊢ MeasurableSet (v \ t n)

Tactic:
· exact (ih v hv).inter (measurableSet_generateFrom ⟨n, rfl⟩)

Goal state after:
case refine_1.succ.inr
α : Type u_1
t : ℕ → Set α
n : ℕ
ih : ∀ u ∈ memPartition t n, MeasurableSet u
v : Set α
hv : v ∈ memPartition t n
⊢ MeasurableSet (v \ t n)