mathlib-initiative/mathlib-tactics huggingface dataset:
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 𝕜 𝕜'
q : 𝕜
x✝ : PUnit.{?u.14 + 1}
⊢ ‖q • x✝‖ ≤ ‖q‖ * ‖x✝‖

Tactic:
simp only [norm_eq_zero, mul_zero, le_refl]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
t : β
ht : t ∈ Ioo 0 1
⊢ 1 - t ∈ Ioo 0 1

Tactic:
simp_all only [mem_Ioo, sub_pos, sub_lt_self_iff, and_self]

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
⊢ sign (-a) = -sign a

Tactic:
simp_rw [sign_apply, Left.neg_pos_iff, Left.neg_neg_iff]
  split_ifs with h h'
  · exact False.elim (lt_asymm h h')
  · simp
  · simp
  · simp

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

Goal state before:
pp: x : EReal
⊢ ↑(sign x) * ↑x.abs = x

Tactic:
EReal.sign_mul_abs

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

Goal state before:
pp: case neg
β : Type u_2
f : β → ℝ≥0
A : ∑' (b : β), f b = 0
h : ∑' (b : β), ↑(f b) = ∞
⊢ ∑' (b : β), f b = (∑' (b : β), ↑(f b)).toNNReal

Tactic:
simp only [h, ENNReal.toNNReal_top, A]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
hd : tsum d ≠ ∞
⊢ CauchySeq f

Tactic:
lift d to ℕ → NNReal using fun i => ENNReal.ne_top_of_tsum_ne_top hd i
  rw [ENNReal.tsum_coe_ne_top_iff_summable] at hd
  exact cauchySeq_of_edist_le_of_summable d hf hd

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

Tactic:
refine Filter.Eventually.of_forall fun x' => ?_
    by_cases h' : x' ∈ s <;> simp [h', hz, hz.trans_le hy]

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

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
⊢ d ≤ c

Tactic:
rcases lt_or_ge d 0 with d0 | d0

Goal state after:
case inl
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
d0 : d < 0
⊢ d ≤ c

case inr
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
d0 : 0 ≤ d
⊢ d ≤ c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
⊢ liminf (fun x ↦ c * u x) f = c * liminf u f

Tactic:
simpa [mul_neg, ← Pi.neg_def, limsup_neg] using
    limsup_const_mul_of_nonneg_of_ne_top (u := -u) (by aesop) (by aesop)

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

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
⊢ Tendsto (fun n ↦ r ^ n) atTop (𝓝 0) ↔ |r| < 1

Tactic:
rw [tendsto_zero_iff_abs_tendsto_zero]

Goal state after:
𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
⊢ Tendsto (abs ∘ fun n ↦ r ^ n) atTop (𝓝 0) ↔ |r| < 1
Module: Mathlib.Topology.Semicontinuity.Basic

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

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₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : f z > z₁
h₂z : g z > z₂
A1 : min (f z) (f x) ∈ u
H : g x < g z
⊢ min (g z) (g x) ∈ v

Tactic:
· simpa [H] using h₂ ⟨h₂z, H⟩

Goal state after:
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₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : f z > z₁
h₂z : g z > z₂
A1 : min (f z) (f x) ∈ u
H : g x < g z
⊢ min (g z) (g x) ∈ v
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < ↑n
⊢ ∑ i ∈ Finset.range n, 1 ≤ ∑ i ∈ Finset.range n, r ^ i

Tactic:
gcongr; apply one_le_pow₀ hr

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

Goal state before:
pp: case pos
α : 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 z ≤ g x
⊢ min (g z) (g x) ∈ v

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] using h₂ ⟨h₂z, H⟩

Goal state after:
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
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
⊢ boundedBy 0 = ⊥

Tactic:
eq_bot_iff

Goal state after:
α : Type u_1
⊢ boundedBy 0 ≤ ⊥
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
t : Finset ι
h : ∀ i ∈ ↑t, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i ∈ ↑t, s i)

Tactic:
induction t using Finset.induction_on with
  | empty => simp
  | insert i t hi IH =>
    simp only [Finset.mem_coe, Finset.mem_insert, iUnion_iUnion_eq_or_left] at h ⊢
    exact m.isCaratheodory_union (h _ <| Or.inl rfl) (IH fun _ hj ↦ h _ <| Or.inr hj)

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

Goal state before:
pp: case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
h₀ : m ∅ = 0
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
f : ℕ → Set α
hf : t ⊆ ⋃ i, f i
⊢ t ∩ s ⊆ ⋃ i, (fun i ↦ f i ∩ s) i

Tactic:
rw [← iUnion_inter]
    exact inter_subset_inter_left _ hf

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

Goal state before:
pp: case refine_1
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
s : Set α
hs : μ sᶜ = 0
⊢ sᶜ = ∅

Tactic:
← not_nonempty_iff_eq_empty

Goal state after:
case refine_1
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
s : Set α
hs : μ sᶜ = 0
⊢ ¬sᶜ.Nonempty
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 α
⊢ MeasurableSet s ↔
    ∀ (t : Set α),
      P t →
        (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t

Tactic:
rw [isCaratheodory_iff_le]
  constructor
  · intro h t _ht
    exact h t
  · intro h u
    conv_rhs => rw [inducedOuterMeasure_eq_iInf _ msU m_mono]
    refine le_iInf ?_
    intro t
    refine le_iInf ?_
    intro ht
    refine le_iInf ?_
    intro h2t
    refine le_trans ?_ ((h t ht).trans_eq <| inducedOuterMeasure_eq' _ msU m_mono ht)
    gcongr

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (bliminf s atTop p)

Tactic:
simp only [Filter.bliminf_eq_iSup_biInf_of_nat, iInf_eq_iInter, iSup_eq_iUnion]
  exact .iUnion fun n => .iInter fun m => .iInter fun hm => h m hm.1

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

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

Tactic:
(rightInverse_rangeSplitting hg.injective).comp_eq_id

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
⊢ ⇑e.toEquiv '' ⇑e.toEquiv ⁻¹' s = s

Tactic:
Equiv.image_preimage

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
⊢ s = s
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
⊢ μ (s ∪ sᶜ) = μ univ

Tactic:
union_compl_self

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
⊢ μ univ = μ univ
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : AEMeasurable f μ
⊢ NullMeasurableSet s (map f μ)

Tactic:
rwa [hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : ∀ᵐ (x : α) ∂comap f μ, s x = t x
⊢ ∀ᵐ (x : β) ∂μ, (f '' s) x = (f '' t) x

Tactic:
ae_iff

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : (comap f μ) {a | ¬s a = t a} = 0
⊢ μ {a | ¬(f '' s) a = (f '' t) a} = 0
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : s =ᵐ[comap f μ] t
⊢ f '' s =ᵐ[μ] f '' t

Tactic:
rw [EventuallyEq, ae_iff] at hst ⊢
  have h_eq_α : { a : α | ¬s a = t a } = s \ t ∪ t \ s := by
    ext1 x
    simp only [eq_iff_iff, mem_ofPred_eq, mem_union, Set.mem_sdiff]
    tauto
  have h_eq_β : { a : β | ¬(f '' s) a = (f '' t) a } = f '' s \ f '' t ∪ f '' t \ f '' s := by
    ext1 x
    simp only [eq_iff_iff, mem_ofPred_eq, mem_union, Set.mem_sdiff]
    tauto
  rw [← Set.image_sdiff hfi, ← Set.image_sdiff hfi, ← Set.image_union] at h_eq_β
  rw [h_eq_β]
  rw [h_eq_α] at hst
  exact measure_image_eq_zero_of_comap_eq_zero f μ hfi hf hst

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
hs : ⇑e '' s =ᵐ[μ] s
k : ℕ
⊢ ⇑e ⁻¹' s =ᵐ[μ] s ↔ ⇑e ⁻¹' s =ᵐ[μ] ⇑e ⁻¹' ⇑e '' s

Tactic:
rw [Equiv.preimage_image]

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
⊢ μ (⋂ i, s i) = ⨅ i, μ (s i)

Tactic:
have hMono : Monotone t := fun i j hij ω hω ↦ ⟨hω.2 hij hω.1, hω.2⟩

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)
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: α : Type u_1
f : ℕ → Set α
n : ℕ
⊢ ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v

Tactic:
induction n with
  | zero =>
    intro u v hu hv huv
    simp only [memPartition_zero, mem_singleton_iff] at hu hv
    rw [hu, hv] at huv
    exact absurd rfl huv
  | succ n ih =>
    intro u v hu hv huv
    rw [memPartition_succ] at hu hv
    obtain ⟨u', hu', hu'_eq⟩ := hu
    obtain ⟨v', hv', hv'_eq⟩ := hv
    rcases hu'_eq with rfl | rfl <;> rcases hv'_eq with rfl | rfl
    · refine Disjoint.mono inter_subset_left inter_subset_left (ih hu' hv' ?_)
      exact fun huv' ↦ huv (huv' ▸ rfl)
    · exact Disjoint.mono_left inter_subset_right Set.disjoint_sdiff_right
    · exact Disjoint.mono_right inter_subset_right Set.disjoint_sdiff_left
    · refine Disjoint.mono sdiff_subset sdiff_subset (ih hu' hv' ?_)
      exact fun huv' ↦ huv (huv' ▸ rfl)

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

Goal state before:
pp: α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ t n = ⋃ u ∈ memPartition t n, u ∩ t n

Tactic:
← iUnion_inter,

Goal state after:
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ t n = (⋃ i ∈ memPartition t n, i) ∩ t n
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_2
α : Type u_1
t : ℕ → Set α
u : Set α
hu : ∃ y, t y = u
⊢ MeasurableSet u

Tactic:
obtain ⟨n, rfl⟩ := hu

Goal state after:
case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ MeasurableSet (t n)
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
H : AEMeasurable (g ∘ f) μ
this : AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) μ
⊢ AEMeasurable f μ

Tactic:
(rightInverse_rangeSplitting hg.injective).comp_eq_id

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
H : AEMeasurable (g ∘ f) μ
this : AEMeasurable (_root_.id ∘ f) μ
⊢ AEMeasurable f μ
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case mpr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
A : s.indicator f =ᵐ[μ.restrict s] s.indicator (AEMeasurable.mk f h)
⊢ s.indicator f =ᵐ[μ] s.indicator (AEMeasurable.mk f h)

Tactic:
have B : s.indicator f =ᵐ[μ.restrict sᶜ] s.indicator (AEMeasurable.mk f h) :=
      (indicator_ae_eq_restrict_compl hs).trans (indicator_ae_eq_restrict_compl hs).symm

Goal state after:
case mpr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
A : s.indicator f =ᵐ[μ.restrict s] s.indicator (AEMeasurable.mk f h)
B : s.indicator f =ᵐ[μ.restrict sᶜ] s.indicator (AEMeasurable.mk f h)
⊢ s.indicator f =ᵐ[μ] s.indicator (AEMeasurable.mk f h)
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
Ts : Set (Set X)
hoTs : ∀ t ∈ Ts, IsOpen[inst✝²] t
hyK : y ∈ ⋂₀ Ts
⊢ x ∈ ⋂₀ Ts

Tactic:
rw [mem_sInter] at hyK ⊢

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
Ts : Set (Set X)
hoTs : ∀ t ∈ Ts, IsOpen[inst✝²] t
hyK : ∀ t ∈ Ts, y ∈ t
⊢ ∀ t ∈ Ts, x ∈ t
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
⊢ Bornology.IsBounded (thickening δ E)

Tactic:
by
  rcases E.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
  · simp
  · refine (isBounded_iff_subset_closedBall x).2 ⟨δ + diam E, fun y hy ↦ ?_⟩
    calc
      dist y x ≤ infDist y E + diam E := dist_le_infDist_add_diam (x := y) h hx
      _ ≤ δ + diam E := by grw [(mem_thickening_iff_infDist_lt ⟨x, hx⟩).1 hy]

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

Goal state before:
pp: case H1
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
⊢ ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ ENNReal.ofReal (max rs rt)

Tactic:
intro x xs
      exists ct, hct
      have : dist x ct ≤ max rs rt := le_trans (hrs xs) (le_max_left _ _)
      rwa [edist_dist, ENNReal.ofReal_le_ofReal_iff]
      exact le_trans dist_nonneg this

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist s t ≠ ∞
h : s = ∅
⊢ t = ∅

Tactic:
← not_nonempty_iff_eq_empty

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
fin : hausdorffEDist s t ≠ ∞
h : ¬s.Nonempty
⊢ ¬t.Nonempty
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
hs_nonempty : s.Nonempty
hs_ne_univ : s ≠ univ
x y : β
⊢ (piecewise s hs (const α x) (const α y)).range = {x, y}

Tactic:
by
  simp only [← Finset.coe_inj, coe_range, coe_piecewise, range_piecewise, coe_const,
    Finset.coe_insert, Finset.coe_singleton, hs_nonempty.image_const,
    (nonempty_compl.2 hs_ne_univ).image_const, singleton_union, Function.const]

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

Goal state before:
pp: case hunion
α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
s t : Set α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
⊢ thickening (min ε₁ ε₂) (f '' (V₁ ∪ V₂)) ⊆ U

Tactic:
image_union,

Goal state after:
case hunion
α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
s t : Set α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
⊢ thickening (min ε₁ ε₂) (f '' V₁ ∪ f '' V₂) ⊆ U
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
a b c : α
inst✝³ : AddCommMagma α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftMono α
inst✝ : IsLeftCancelAdd α
⊢ a ≤ b + c ↔ a < c ∨ ∃ d ≤ b, a = d + c

Tactic:
rw [add_comm, le_add_iff_lt_left_or_exists_le]

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
a b c : α
inst✝³ : AddCommMagma α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftMono α
inst✝ : IsLeftCancelAdd α
⊢ (a < c ∨ ∃ d ≤ b, a = c + d) ↔ a < c ∨ ∃ d ≤ b, a = d + c
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f✝ g✝ : α →ₛ ℝ≥0∞
h : f✝ ≤ g✝
f g : α →ₛ ℝ≥0∞
⊢ (map Prod.fst (f.pair g)).lintegral μ ≤ (map (fun p ↦ max p.1 p.2) (f.pair g)).lintegral μ

Tactic:
by
      simp only [map_lintegral]
      gcongr
      exact le_sup_left

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
h : f ≤ g
⊢ f.lintegral μ ≤ g.lintegral μ

Tactic:
by
  refine Monotone.of_left_le_map_sup (f := (lintegral · μ)) (fun f g ↦ ?_) h
  calc
    f.lintegral μ = ((pair f g).map Prod.fst).lintegral μ := by rw [map_fst_pair]
    _ ≤ ((pair f g).map fun p ↦ p.1 ⊔ p.2).lintegral μ := by
      simp only [map_lintegral]
      gcongr
      exact le_sup_left

Goal state after: