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

Goal state before:
pp: case inl
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
i : ι
⊢ f i ≤ g (e i)

Tactic:
exact h _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith K₁ fun a ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
h : Bornology.IsBounded (image2 f s {b})
⊢ Bornology.IsBounded s

Tactic:
rw [Set.image2_singleton_right] at h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith K₁ fun a ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
h : Bornology.IsBounded ((fun a ↦ f a b) '' s)
⊢ Bornology.IsBounded s
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
j a c : ℕ
hc : ∀ (b : ℕ), c ≤ b → ∀ i ≤ a, y b ∉ closure[inst✝¹] {x i}
b : ℕ
hb : y (c + j) ∈ closure[inst✝¹] {x b}
⊢ ∃ b, a ≤ b ∧ ∃ n ≥ j, y n ∈ closure[inst✝¹] {x b}

Tactic:
refine ⟨b, ?_, c + j, j.le_add_left c, hb⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
j a c : ℕ
hc : ∀ (b : ℕ), c ≤ b → ∀ i ≤ a, y b ∉ closure[inst✝¹] {x i}
b : ℕ
hb : y (c + j) ∈ closure[inst✝¹] {x b}
⊢ a ≤ b
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ map Prod.swap ((𝓤 α).lift' gen) ≤ (𝓤 α).lift' gen

Tactic:
let f := fun s : SetRel α α =>
        { p : CauchyFilter α × CauchyFilter α | s ∈ (p.2.val ×ˢ p.1.val : Filter (α × α)) }
  have h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f := by
    delta gen
    simp [f, map_lift'_eq, monotone_ofPred, Filter.monotone_mem, Function.comp_def,
      image_swap_eq_preimage_swap]
  have h₂ : (𝓤 α).lift' f ≤ (𝓤 α).lift' gen :=
    uniformity_lift_le_swap
      (monotone_principal.comp
        (monotone_ofPred fun p => @Filter.monotone_mem _ (p.2.val ×ˢ p.1.val)))
      (by
        have h := fun p : CauchyFilter α × CauchyFilter α => @Filter.prod_comm _ _ p.2.val p.1.val
        simp only [Function.comp, h, mem_map, f]
        exact le_rfl)
  exact h₁.trans_le h₂

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
t'' : Set (α × α)
ht''₁ : t'' ∈ 𝓤 α
ht''₂ : gen t'' ⊆ s
t' : Set (α × α)
ht'₁ : t' ∈ 𝓤 α
ht'₂ : t' ○ t' ⊆ t''
this✝ : t' ∈ ↑f ×ˢ ↑f
t : Set α
ht : t ∈ ↑f
h : t ×ˢ t ⊆ t'
x : α
hx : x ∈ t
this : t'' ∈ ↑f ×ˢ pure x
⊢ (f, pureCauchy x) ∈ gen t''

Tactic:
dsimp [gen]

Goal state after:
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
t'' : Set (α × α)
ht''₁ : t'' ∈ 𝓤 α
ht''₂ : gen t'' ⊆ s
t' : Set (α × α)
ht'₁ : t' ∈ 𝓤 α
ht'₂ : t' ○ t' ⊆ t''
this✝ : t' ∈ ↑f ×ˢ ↑f
t : Set α
ht : t ∈ ↑f
h : t ×ˢ t ⊆ t'
x : α
hx : x ∈ t
this : t'' ∈ ↑f ×ˢ pure x
⊢ t'' ∈ ↑f ×ˢ ↑(pureCauchy x)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a : ℝ≥0∞
⊢ Continuous fun x ↦ x - a

Tactic:
by_cases a_infty : a = ∞
  · simp [a_infty, continuous_const, tsub_eq_zero_of_le]
  · rw [show (fun x => x - a) = (fun p : ℝ≥0∞ × ℝ≥0∞ => p.fst - p.snd) ∘ fun x => ⟨x, a⟩ by rfl]
    apply continuousOn_sub.comp_continuous (by fun_prop)
    intro x
    simp only [a_infty, Ne, mem_ofPred_eq, Prod.mk_inj, and_false, not_false_iff]

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

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
r : ℝ≥0
⊢ (∀ y < r, ∀ᶠ (a : ι) in f, y < u a) ↔ ↑r ≤ liminf (fun i ↦ ↑(u i)) f

Tactic:
le_liminf_iff

Goal state after:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
r : ℝ≥0
⊢ (∀ y < r, ∀ᶠ (a : ι) in f, y < u a) ↔ ∀ y < ↑r, ∀ᶠ (a : ι) in f, y < ↑(u a)
Module: Mathlib.Topology.MetricSpace.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
x₁ x₂ y₁ y₂ : ℝ≥0
⊢ edist ((fun p ↦ p.1 + p.2) (x₁, x₂)) ((fun p ↦ p.1 + p.2) (y₁, y₂)) ≤ ↑(LipschitzAdd.C ℝ) * edist (x₁, x₂) (y₁, y₂)

Tactic:
exact lipschitzWith_lipschitz_const_add_edist ⟨(x₁ : ℝ), x₂⟩ ⟨y₁, y₂⟩

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

Goal state before:
pp: α : Type u_5
inst✝¹ : Fintype α
ι : α → Type u
inst✝ : ∀ (a : α), Finite (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : Nonempty ((a : α) → ι a)
i : (a : α) → ι a
⊢ ∀ i_1 ∈ Finset.univ, 0 ≤ f i_1 (i i_1)

Tactic:
by simp [hf₀]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
⊢ (fun x ↦ s • x) '' closedBall x ε = closedBall (s • x) (‖s‖ * ε)

Tactic:
by
  ext p
  simp_rw [Set.mem_image, mem_closedBall]
  constructor
  · rintro ⟨y, h1, rfl⟩
    simpa [dist_smul₀] using mul_le_mul_of_nonneg_left h1 (norm_nonneg s)
  · refine fun h ↦ ⟨s⁻¹ • p, ?_, by simp [smul_smul, hs]⟩
    refine le_of_mul_le_mul_of_pos_left ?_ (norm_pos_iff.mpr hs)
    rw [← dist_smul₀]
    simpa [smul_smul, hs] using h

Goal state after:
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ TProd.elim' h ⁻¹' univ.pi t = Set.tprod l t

Tactic:
rw [← h2, ← mk_preimage_tprod, preimage_preimage]

Goal state after:
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ (fun x ↦ TProd.mk l (TProd.elim' h x)) ⁻¹' Set.tprod l t = Set.tprod l t
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case neg
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
⊢ Measurable fun x ↦ x.2 ⟨j, ⋯⟩

Tactic:
have : Measurable fun (f : ∀ i : { x // ¬p x }, X i.1) => f ⟨j, hj⟩ :=
      measurable_pi_apply (X := fun i : {x // ¬p x} => X i.1) ⟨j, hj⟩

Goal state after:
case neg
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
this : Measurable fun f ↦ f ⟨j, hj⟩
⊢ Measurable fun x ↦ x.2 ⟨j, ⋯⟩
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
x : α
| a = f x

Tactic:
rw [eq_comm]

Goal state after:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
x : α
| f x = a
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul R A
⊢ Continuous[inst✝², inst✝¹] ⇑(algebraMap R A)

Tactic:
rw [algebraMap_eq_smul_one']
  fun_prop

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
h✝¹ : ¬0 < a
h✝ : a < 0
h : -1 = -1
⊢ a < 0

Tactic:
assumption

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

Goal state before:
pp: case zero_bot
⊢ (0 * ⊥)⁻¹ = 0⁻¹ * ⊥⁻¹

Tactic:
| zero_bot =>

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

Goal state before:
pp: a : EReal
⊢ ↑(sign a) * (↑a.abs)⁻¹ = a⁻¹

Tactic:
by
  induction a with
  | bot | top => simp
  | coe a =>
    rcases lt_trichotomy a 0 with (a_neg | rfl | a_pos)
    · rw [sign_coe, _root_.sign_neg a_neg, coe_neg_one, neg_one_mul, ← inv_neg, abs_def a,
        coe_ennreal_ofReal, max_eq_left (abs_nonneg a), ← coe_neg |a|, abs_of_neg a_neg, neg_neg]
    · simp
    · rw [sign_coe, _root_.sign_pos a_pos, SignType.coe_one, one_mul]
      simp only [abs_def a, coe_ennreal_ofReal, abs_nonneg, max_eq_left]
      congr
      exact abs_of_pos a_pos

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

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

Tactic:
rw [sign_coe, _root_.sign_neg a_neg, coe_neg_one, neg_one_mul, abs_def a,
        ← ofReal_inv_of_pos (abs_pos_of_neg a_neg), coe_ennreal_ofReal,
        max_eq_left (inv_nonneg.2 (abs_nonneg a)), ← coe_neg |a|⁻¹, ← coe_inv a, abs_of_neg a_neg,
        ← _root_.inv_neg, neg_neg]

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 α
⊢ UpperHemicontinuousWithinAt f s x ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty

Tactic:
by
  rw [UpperHemicontinuousWithinAt, semicontinuousWithinAt_iff_frequently, compl_surjective.forall]
  simp [← subset_interior_iff_mem_nhdsSet, not_subset, forall_isClosed_iff, inter_nonempty]

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

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup (u + v) f = ⊥

Tactic:
apply le_bot_iff.1 ((limsup_add_le (.inr h') _).trans _)

Goal state after:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥

α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup u f + limsup v f ≤ ⊥
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ s ⊆ ⋃ n, (range f)ᶜ ∪ f '' t n

Tactic:
← union_iUnion,

Goal state after:
case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ s ⊆ (range f)ᶜ ∪ ⋃ i, f '' t i
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
left✝ : 0 < C
r₀ : 0 ≤ r
⊢ HasSum (HPow.hPow r) (1 - r)⁻¹

Tactic:
simpa using hasSum_geometric_of_lt_one r₀ hr

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
left✝ : 0 < C
r₀ : 0 ≤ r
⊢ HasSum (fun n ↦ C * r ^ n) (C / (1 - r))

Tactic:
· refine HasSum.mul_left C ?_
    simpa using hasSum_geometric_of_lt_one r₀ hr

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

Goal state before:
pp: case neg
α : 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}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : g z > z₂
H : g x < g z
⊢ min (g z) (g x) ∈ v

Tactic:
simpa [H.le] using h₂ ⟨z₂lt, le_rfl⟩

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

Goal state before:
pp: ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i ↦ ε' ↑i) c
hcε : c ≤ ε
t : Finset ι
ht : ↑t ⊆ s
⊢ ∑ i ∈ t, ε' i ≤ ε

Tactic:
← sum_subtype_of_mem _ ht

Goal state after:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i ↦ ε' ↑i) c
hcε : c ≤ ε
t : Finset ι
ht : ↑t ⊆ s
⊢ ∑ x ∈ Finset.subtype (Membership.mem s) t, ε' ↑x ≤ ε
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_4
inst✝³ : TopologicalSpace α
β : Type u_5
f : α → β
a : α
inst✝² : PartialOrder β
inst✝¹ : CommGroup β
inst✝ : IsOrderedMonoid β
⊢ LowerSemicontinuousAt f⁻¹ a ↔ UpperSemicontinuousAt f a

Tactic:
by
  simp [← lowerSemicontinuousWithinAt_univ_iff, ← upperSemicontinuousWithinAt_univ_iff]

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

Goal state before:
pp: α : Type u_4
inst✝³ : TopologicalSpace α
β : Type u_5
f : α → β
a : α
inst✝² : PartialOrder β
inst✝¹ : CommGroup β
inst✝ : IsOrderedMonoid β
⊢ UpperSemicontinuousAt f⁻¹ a ↔ LowerSemicontinuousAt f a

Tactic:
by
  simp [← lowerSemicontinuousWithinAt_univ_iff, ← upperSemicontinuousWithinAt_univ_iff]

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

Goal state before:
pp: case coe.top
a✝ : ℝ
h₁ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊥
h₂ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊤
h₃ : (↑a✝, ⊤).1 ≠ ⊥ ∨ (↑a✝, ⊤).2 ≠ 0
h₄ : (↑a✝, ⊤).1 ≠ ⊤ ∨ (↑a✝, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊤)

Tactic:
simp only [ne_eq, EReal.coe_eq_zero, not_true_eq_false, or_false] at h₂
    exact continuousAt_mul_swap (continuousAt_mul_top_ne_zero h₂)

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ s = μ.toOuterMeasure s

Tactic:
μ.coe_toOuterMeasure

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ s = μ s
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

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

Tactic:
μ.coe_toOuterMeasure

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), μ t = ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), μ t
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
s : Set α
⊢ sᶜ ∈ ae μ ↔ μ s = 0

Tactic:
simp only [mem_ae_iff, compl_compl]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ∩ s ⊆ t'
ht' : MeasurableSet t'
hμt' : μ t' = μ.trim (t ∩ s)
⊢ ((restrict s) μ).trim t ≤ μ t'

Tactic:
rw [inter_subset] at htt'

Goal state after:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : μ t' = μ.trim (t ∩ s)
⊢ ((restrict s) μ).trim t ≤ μ t'
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:

Tactic:
μ.map f s ≤ μ.map f t := by gcongr
    _ = μ (f ⁻¹' s) := by rw [map_apply hf.measurable htm, hft, measure_toMeasurable]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
I : Set β
hc : I.Countable
s : β → Set α
this : Encodable ↑I
⊢ μ (⋃ b ∈ I, toMeasurable μ (s b)) = μ (⋃ b ∈ I, s b)

Tactic:
simp only [biUnion_eq_iUnion, measure_iUnion_toMeasurable]

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : Pairwise (AEDisjoint μ on s)
⊢ ⨆ s_1, ∑ a ∈ s_1, μ (s a) ≤ μ univ

Tactic:
exact iSup_le fun s =>
    sum_measure_le_measure_univ (fun i _hi => hs i) fun i _hi j _hj hij => H hij

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
H : μ.restrict s = ν.restrict s
t : Set α
hts : t ⊆ s
ht : MeasurableSet t
⊢ μ t = ν t

Tactic:
rw [← inter_eq_self_of_subset_left hts, ← restrict_apply ht, H, restrict_apply ht]

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

Goal state before:
pp: case h₂
α : 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
hu : ν (u ∩ t) = 0
⊢ s ⊆ f ⁻¹' t

Tactic:
assumption

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

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

Tactic:
exact ne_top_of_le_ne_top (htop t ht) (measure_mono Set.inter_subset_left)

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ SigmaFinite (μ.trim ⋯) ↔ IsFiniteMeasure μ

Tactic:
rw [sigmaFinite_bot_iff]
  refine ⟨fun h => ⟨?_⟩, fun h => ⟨?_⟩⟩ <;> have h_univ := h.measure_univ_lt_top
  · rwa [trim_measurableSet_eq bot_le MeasurableSet.univ] at h_univ
  · rwa [trim_measurableSet_eq bot_le MeasurableSet.univ]

Goal state after:
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: case refine_2.inl
α : 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.1.2 s ⟨hsS, hsl⟩, hy.1.2 s ⟨hsS, hsl⟩]

Goal state after:
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: α : Type u_1
l : Filter α
inst✝¹ : CountableInterFilter l
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hne : s.Nonempty
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
⊢ ∃ a ∈ s, {a} ∈ l

Tactic:
by
  rcases exists_subset_subsingleton_mem_of_forall_separating p hs hl with ⟨t, hts, ht, htl⟩
  rcases ht.eq_empty_or_singleton with rfl | ⟨x, rfl⟩
  · exact hne.imp fun a ha ↦ ⟨ha, mem_of_superset htl (empty_subset _)⟩
  · exact ⟨x, hts rfl, htl⟩

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

Goal state before:
pp: case refine_2
α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
i : ι
hi : i ∈ F
x : α
hx : x ∈ s i
⊢ x ∈ P ({x_1 ∈ F | x ∈ s x_1})

Tactic:
simp_rw [P, mem_inter_iff, mem_iInter, Finset.mem_sdiff, mem_filter]

Goal state after:
case refine_2
α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
i : ι
hi : i ∈ F
x : α
hx : x ∈ s i
⊢ (∀ (i : ι), i ∈ F ∧ x ∈ s i → x ∈ s i) ∧ ∀ (i : ι), i ∈ F ∧ ¬(i ∈ F ∧ x ∈ s i) → x ∈ (s i)ᶜ
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
⊢ range g ⊆ t

pp: case refine_3
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
⊢ f =ᵐ[μ] g

Tactic:
· rintro _ ⟨x, rfl⟩
    by_cases hx : x ∈ s
    · simpa [g, hx] using h₀.some_mem
    · simp only [g, hx, piecewise_eq_of_notMem, not_false_iff]
      contrapose hx
      apply subset_toMeasurable
      simp +contextual only [hx, mem_compl_iff, mem_ofPred_eq, not_and,
        not_false_iff, imp_true_iff]

Goal state after:
case refine_3
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
⊢ f =ᵐ[μ] g
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
inst✝² : Zero β
s : Set α
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
⊢ AEMeasurable (s.indicator fun x ↦ b) μ ↔ NullMeasurableSet s μ

Tactic:
by
  classical
  constructor <;> intro h
  · convert! h.nullMeasurable (MeasurableSet.singleton (0 : β)).compl
    rw [indicator_const_preimage_eq_union s {0}ᶜ b]
    simp [NeZero.ne b]
  · exact (aemeasurable_indicator_iff₀ h).mpr aemeasurable_const

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
ι' : Type u_9
e : ι' ≃ ι
m : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum (m ∘ ⇑e)) s = (sum m) s

Tactic:
simpa [hs, sum_apply] using e.tsum_eq (fun n ↦ m n s)

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
ι : Type u_7
β : Type u_8
mβ : MeasurableSpace β
m : ι → Measure α
f : α → β
s : Finset ι
hf : AEMeasurable f (∑ i ∈ s, m i)
⊢ map f (∑ i ∈ s, m i) = ∑ i ∈ s, map f (m i)

Tactic:
← sum_coe_finset,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
ι : Type u_7
β : Type u_8
mβ : MeasurableSpace β
m : ι → Measure α
f : α → β
s : Finset ι
hf : AEMeasurable f (∑ i ∈ s, m i)
⊢ map f (sum fun i ↦ m ↑i) = ∑ i ∈ s, map f (m i)