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
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l univ
hG : TendstoLocallyUniformlyOn G g l univ
hf : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (f y) 0
hg : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (g y) 0
⊢ TendstoLocallyUniformlyOn (F • G) (f • g) l univ

Tactic:
apply hF.smul₀_of_isBoundedUnder hG

Goal state after:
case hf
α : 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
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l univ
hG : TendstoLocallyUniformlyOn G g l univ
hf : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (f y) 0
hg : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (g y) 0
⊢ ∀ x ∈ univ, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[univ] x) fun y ↦ dist (f y) 0

case hg
α : 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
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l univ
hG : TendstoLocallyUniformlyOn G g l univ
hf : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (f y) 0
hg : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (g y) 0
⊢ ∀ x ∈ univ, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[univ] x) fun y ↦ dist (g y) 0
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: case mpr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
this : ∃ ε > 0, ∀ (y : 𝕜), ‖y‖ < ε → y = 0
⊢ ‖x‖ = 1

Tactic:
obtain ⟨ε, εpos, h'⟩ := this

Goal state after:
case mpr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
⊢ ‖x‖ = 1
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f✝ : F
g : β →ᵈ γ
f : α →ᵈ β
x y : α
⊢ edist ((⇑g ∘ ⇑f) x) ((⇑g ∘ ⇑f) y) = ↑(ratio g * ratio f) * edist x y

Tactic:
simp_rw [Function.comp, edist_eq, ENNReal.coe_mul, mul_assoc]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝ : SeminormedRing α
z : ℤ
hz : z = -↑z.natAbs
⊢ ‖↑z.natAbs‖ = ‖↑z‖

Tactic:
· rw [← Int.cast_natCast, ← norm_neg, ← Int.cast_neg, ← hz]

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖↑a * ↑b - ↑b * ↑a‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ = ‖(↑a - 1) * (↑b - 1) - (↑b - 1) * (↑a - 1)‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖

Tactic:
by
      simp_rw [sub_one_mul, mul_sub_one]; abel_nf

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

Goal state before:
pp: ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s : Finset ι
y : (i : ↥s) → π ↑i
i : ι
z : π i
hi : i ∉ s
⊢ update (updateFinset x s y) i z = updateFinset x (s ∪ {i}) ((piFinsetUnion π ⋯) (y, uniqueElim z))

Tactic:
by
  rw [update_eq_updateFinset, updateFinset_updateFinset]

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

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
⊢ (comap norm atTop)⁻¹ = 𝓝[≠] 0

Tactic:
← Filter.comap_inv,

Goal state after:
α : Type u_1
inst✝ : NormedDivisionRing α
⊢ comap Inv.inv (comap norm atTop) = 𝓝[≠] 0
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedDivisionRing α
x : α
hx : x ≠ 0
⊢ closedBall x (‖x‖ / 2) ∈ 𝓝 x

Tactic:
apply Metric.closedBall_mem_nhds

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedDivisionRing α
x : α
hx : x ≠ 0
⊢ 0 < ‖x‖ / 2
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: K : Type u_4
inst✝ : NormedField K
⊢ CompleteSpace K ↔ IsComplete (closedBall 0 1)

Tactic:
constructor <;> intro h
  · exact Metric.isClosed_closedBall.isComplete
  rcases NormedField.discreteTopology_or_nontriviallyNormedField K with _ | ⟨_, rfl⟩
  · rwa [completeSpace_iff_isComplete_univ,
         ← NormedDivisionRing.unitClosedBall_eq_univ_of_discrete]
  refine Metric.complete_of_cauchySeq_tendsto fun u hu ↦ ?_
  obtain ⟨k, hk⟩ := hu.norm_bddAbove
  have kpos : 0 ≤ k := (_root_.norm_nonneg (u 0)).trans (hk (by simp))
  obtain ⟨x, hx⟩ := NormedField.exists_lt_norm K k
  have hu' : CauchySeq ((· / x) ∘ u) := (uniformContinuous_div_const' x).comp_cauchySeq hu
  have hb : ∀ n, ((· / x) ∘ u) n ∈ Metric.closedBall 0 1 := by
    intro
    simp only [Function.comp_apply, Metric.mem_closedBall, dist_zero_right, norm_div]
    rw [div_le_one (kpos.trans_lt hx)]
    exact hx.le.trans' (hk (by simp))
  obtain ⟨a, -, ha'⟩ := cauchySeq_tendsto_of_isComplete h hb hu'
  refine ⟨a * x, (((continuous_mul_const x).tendsto a).comp ha').congr ?_⟩
  have hx' : x ≠ 0 := by
    contrapose! hx
    simp [hx, kpos]
  simp [div_mul_cancel₀ _ hx']

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : s.Countable
⊢ MeasurableSet s

Tactic:
by
  rw [← biUnion_of_singleton s]
  exact .biUnion hs fun b _ => .singleton b

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

Goal state before:
pp: α : Type u_6
inst✝¹ : SeminormedRing α
inst✝ : NormSMulClass ℤ α
n : ℕ
⊢ ‖↑n‖ = ↑n * ‖1‖

Tactic:
simpa using norm_intCast_eq_abs_mul_norm_one α n

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

Goal state before:
pp: G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < ↑n
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → ‖f x‖ < ε

Tactic:
have hnpos : 0 < (n : ℝ) := (div_pos hC₀ hε).trans hn

Goal state after:
G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < ↑n
hnpos : 0 < ↑n
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → ‖f x‖ < ε
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
⊢ measurableAtom x = measurableAtom y

Tactic:
refine subset_antisymm (measurableAtom_subset_of_mem hx) ?_
  by_cases hy : y ∈ measurableAtom x
  · exact measurableAtom_subset_of_mem hy
  exfalso
  simp only [measurableAtom, mem_iInter, not_forall] at hx hy ⊢
  obtain ⟨s, hxs, hs, hys⟩ := hy
  specialize hx sᶜ hys hs.compl
  exact hx hxs

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
⊢ sign a ≤ 0 ↔ a ≤ 0

Tactic:
by
  rcases lt_trichotomy 0 a with (h | h | h)
  · simp [h, h.not_ge]
  · simp [← h]
  · simp [h, h.le]

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

Goal state before:
pp: case neg_left
x✝ y✝ : EReal
h : sign (x✝ * y✝) = sign x✝ * sign y✝
⊢ -(sign x✝ * sign y✝) = -sign x✝ * sign y✝

Tactic:
neg_mul

Goal state after:
case neg_left
x✝ y✝ : EReal
h : sign (x✝ * y✝) = sign x✝ * sign y✝
⊢ -(sign x✝ * sign y✝) = -(sign x✝ * sign y✝)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_bot
⊢ (⊤ * ⊥)⁻¹ = ⊤⁻¹ * ⊥⁻¹

Tactic:
| top_bot =>

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

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

Tactic:
_root_.sign_pos a_pos,

Goal state after:
case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑1 * (↑(↑a).abs)⁻¹ = (↑a)⁻¹
Module: Mathlib.Data.EReal.Inv

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

Tactic:
_root_.sign_pos a_pos,

Goal state after:
case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑1 * ↑(↑a).abs⁻¹ = (↑a)⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b : EReal
h₁ : b ≠ ⊥
h₂ : b ≠ ⊤
h₃ : b ≠ 0
⊢ b * (a / b) = a

Tactic:
← mul_div_left_comm a b b,

Goal state after:
a b : EReal
h₁ : b ≠ ⊥
h₂ : b ≠ ⊤
h₃ : b ≠ 0
⊢ a * (b / b) = a
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
m_empty : m ∅ = 0
m_mono : ∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t
m_subadd : ∀ (s : ℕ → Set α), m (⋃ i, s i) ≤ ∑' (i : ℕ), m (s i)
⊢ (boundedBy m) s = m s

Tactic:
boundedBy_eq_ofFunction m_empty,

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
m_empty : m ∅ = 0
m_mono : ∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t
m_subadd : ∀ (s : ℕ → Set α), m (⋃ i, s i) ≤ ∑' (i : ℕ), m (s i)
⊢ (OuterMeasure.ofFunction m m_empty) s = m s
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f g : α → β
a : α
hf : LowerSemicontinuousAt f a
hg : LowerSemicontinuousAt g a
⊢ LowerSemicontinuousAt (fun x ↦ max (f x) (g x)) a

Tactic:
by
  rw [← lowerSemicontinuousWithinAt_univ_iff] at *
  exact hf.sup hg

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

Goal state before:
pp: k : ℕ
hn : 0 < k.succ
⊢ ↑(∏ i ∈ Finset.range k.succ, (i + 1)) * (∏ _k ∈ Finset.range k.succ, ↑k.succ)⁻¹ ≤ (↑k.succ)⁻¹

Tactic:
prod_natCast,

Goal state after:
k : ℕ
hn : 0 < k.succ
⊢ (∏ i ∈ Finset.range k.succ, ↑(i + 1)) * (∏ _k ∈ Finset.range k.succ, ↑k.succ)⁻¹ ≤ (↑k.succ)⁻¹
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case hfh
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a + x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, ↑⌈a * b⌉₊ / b ≤ a + b⁻¹

Tactic:
· refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
    simp [div_le_iff₀ (zero_lt_one.trans_le hx), inv_mul_cancel₀ (zero_lt_one.trans_le hx).ne',
      (Nat.ceil_lt_add_one (mul_nonneg ha (zero_le_one.trans hx))).le, add_mul]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ IsPiSystem (Iic '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ -
  exact ⟨a ⊓ b, inf_ind a b ha hb, Iic_inter_Iic.symm⟩

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x : Set α
h : x ∈ generatePiSystem S
⊢ x ∈ S

Tactic:
induction h with
  | base h_s => exact h_s
  | inter _ _ h_nonempty h_s h_u => exact h_S _ h_s _ h_u h_nonempty

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

Goal state before:
pp: case inr
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : t.Nonempty
⊢ (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) + ⨆ (_ : (t \ s).Nonempty), m (t \ s) ≤ ⨆ (_ : t.Nonempty), m t

Tactic:
· convert! le_trans _ (hs t)
    · simp [h]
    exact add_le_add iSup_const_le iSup_const_le

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case iUnion
α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ i, f i) ⋯
eq : MeasurableSet = DynkinSystem.GenerateHas s
t : Set α
f : ℕ → Set α
hfd : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), DynkinSystem.GenerateHas s (f i)
ihf : ∀ (i : ℕ), C (f i) ⋯
⊢ C (⋃ i, f i) ⋯

Tactic:
| @iUnion f hfd hf ihf =>

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable ((range f)ᶜ.domRestrict (extend f g g'))

Tactic:
· rw [domRestrict_extend_compl_range]
    exact hg'.comp measurable_subtype_coe

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i) μ
⊢ μ (⋃ i, f i) = ∑' (i : ι), μ (f i)

Tactic:
by
  rcases exists_subordinate_pairwise_disjoint h hd with ⟨t, _ht_sub, ht_eq, htm, htd⟩
  calc
    μ (⋃ i, f i) = μ (⋃ i, t i) := measure_congr (.countable_iUnion ht_eq)
    _ = ∑' i, μ (t i) := measure_iUnion htd htm
    _ = ∑' i, μ (f i) := tsum_congr fun i => measure_congr (ht_eq _).symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure α
⊢ (mapₗ f) μ = map f μ

Tactic:
by
  simp only [← mapₗ_mk_apply_of_aemeasurable hf.aemeasurable]
  exact mapₗ_congr hf hf.aemeasurable.measurable_mk hf.aemeasurable.ae_eq_mk

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 ⁻¹' t = toMeasurable μ (f ⁻¹' s)

Tactic:
rw [preimage_union, preimage_compl, preimage_range, compl_univ, union_empty,
      hf.injective.preimage_image]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hs : NullMeasurableSet s (comap f μ)
hf : Injective f ∧ ∀ (t : Set α), MeasurableSet t → NullMeasurableSet (f '' t) μ
⊢ (comap f μ) s ≤ μ (f '' s)

pp: case neg
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hs : NullMeasurableSet s (comap f μ)
hf : ¬(Injective f ∧ ∀ (t : Set α), MeasurableSet t → NullMeasurableSet (f '' t) μ)
⊢ (comap f μ) s ≤ μ (f '' s)

Tactic:
· rw [comap_apply₀ _ _ hf.1 hf.2 hs]

Goal state after:
case neg
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hs : NullMeasurableSet s (comap f μ)
hf : ¬(Injective f ∧ ∀ (t : Set α), MeasurableSet t → NullMeasurableSet (f '' t) μ)
⊢ (comap f μ) s ≤ μ (f '' s)
Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

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

Tactic:
zpow_natCast

Goal state after:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
hs : ⇑e '' s =ᵐ[μ] s
k : ℕ
⊢ ⇑(e ^ k)⁻¹.symm ⁻¹' s =ᵐ[μ] s
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
h : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
⊢ comap f (c • μ) = c • comap f μ

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
h : ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ)
⊢ comap f (c • μ) = c • comap f μ

Tactic:
· ext s hs
    rw [comap_apply₀ f _ h.1 _ hs.nullMeasurableSet, smul_apply, smul_apply,
      comap_apply₀ f μ h.1 h.2 hs.nullMeasurableSet]
    simpa [nullMeasurableSet_smul_measure_iff hc] using h.2

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
c : ℝ≥0∞
hc : c ≠ 0
h : ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ)
⊢ comap f (c • μ) = c • comap f μ
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure β
s : Set α
hs : MeasurableSet s
⊢ (Measure.comap f (μ + ν)) s = (Measure.comap f μ + Measure.comap f ν) s

Tactic:
simp only [← comapₗ_eq_comap _ hf.injective (fun _ ↦ hf.measurableSet_image.mpr) _ hs,
    map_add, add_apply]

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → t i ∩ t j = ∅
⊢ (↑s).Pairwise (AEDisjoint μ on t)

Tactic:
intro i hi j hj hij

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → t i ∩ t j = ∅
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
hij : i ≠ j
⊢ (AEDisjoint μ on t) i j
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : μ univ < ∑ i ∈ s, μ (t i)
⊢ ∃ i ∈ s, ∃ j ∈ s, ∃ (_ : i ≠ j), (t i ∩ t j).Nonempty

Tactic:
contrapose! H
  apply sum_measure_le_measure_univ h
  intro i hi j hj hij
  exact (disjoint_iff_inter_eq_empty.mpr (H i hi j hj hij)).aedisjoint

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs_zero : μ sᶜ = 0
⊢ (fun x ↦ if x ∈ s then f x else g x) =ᵐ[μ] f

Tactic:
rw [← mem_ae_iff] at hs_zero
  filter_upwards [hs_zero]
  intros
  split_ifs
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
⊢ (μ.trim hm) Set.univ < ∞

Tactic:
rw [trim_measurableSet_eq hm (@MeasurableSet.univ _ m)]
    exact measure_lt_top _ _

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᵐ[μ.restrict s] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t') = (x ∈ t)
y : α
hy : y ∈ s → (y ∈ t') = (y ∈ t)
⊢ (y ∈ t' ∩ s) = (y ∈ t ∩ s)

Tactic:
simpa only [eq_iff_iff, mem_inter_iff, and_congr_left_iff] using hy

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

Goal state before:
pp: case compl
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
t' : Set ↑s
ht✝ : MeasurableSet t'
ht' : NullMeasurableSet (Subtype.val '' t') μ
⊢ NullMeasurableSet (s \ (fun a ↦ ↑a) '' t') μ

Tactic:
exact hs.diff ht'

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

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
inst✝ : CountablyGenerated α
⊢ generateFrom (⋃ n, countablePartition α n) = m

Tactic:
by
  rw [countablePartition, generateFrom_iUnion_memPartition,
    range_enumerateCountable_of_mem _ empty_mem_countableGeneratingSet,
    generateFrom_countableGeneratingSet]

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
f : ι → Measure α
s : Set α
hs : NullMeasurableSet s (sum f)
⊢ (sum f) s = ∑' (i : ι), (f i) s

Tactic:
apply le_antisymm ?_ (le_sum_apply _ _)

Goal state after:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
f : ι → Measure α
s : Set α
hs : NullMeasurableSet s (sum f)
⊢ (sum f) s ≤ ∑' (i : ι), (f i) s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst✝ : Countable ι
f : ι → Measure α
s : Set α
⊢ (sum f) s = ∑' (i : ι), (f i) s

Tactic:
apply le_antisymm ?_ (le_sum_apply _ _)

Goal state after:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst✝ : Countable ι
f : ι → Measure α
s : Set α
⊢ (sum f) s ≤ ∑' (i : ι), (f i) s
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: case ofNat
α : Type u_1
G : Type u
inst✝³ : DivInvMonoid G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableMul₂ G
inst✝ : MeasurableInv G
n : ℕ
⊢ Measurable fun x ↦ x ^ ↑n

Tactic:
zpow_natCast

Goal state after:
case ofNat
α : Type u_1
G : Type u
inst✝³ : DivInvMonoid G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableMul₂ G
inst✝ : MeasurableInv G
n : ℕ
⊢ Measurable fun x ↦ x ^ n
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
⊢ ∀ t ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, MeasurableSet t

Tactic:
rintro _ ⟨a, rfl | rfl⟩

Goal state after:
case refine_1.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
⊢ MeasurableSet (Ioi a)

case refine_1.inr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
⊢ MeasurableSet (Iio a)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_1.inl.inr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this✝ : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
hcovBy : ¬∃ b, a ⋖ b
t : Set α
hat : t ⊆ Ioi a
htc : t.Countable
htU : ⋃ i ∈ t, Ioi i = ⋃ i ∈ Ioi a, Ioi i
this : Ioi a = ⋃ b ∈ t, Ici b
⊢ MeasurableSet (⋃ b ∈ t, (Iio b)ᶜ)

Tactic:
exact .biUnion htc <| fun _ _ ↦ (H _).compl

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
⊢ x ∈ (thickening δ (thickening δ E)ᶜ)ᶜ

Tactic:
simp only [thickening, mem_compl_iff, mem_ofPred_eq, not_lt]

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
⊢ ENNReal.ofReal δ ≤ infEDist x {x | infEDist x E < ENNReal.ofReal δ}ᶜ
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
⊢ ⨆ i, ⨆ a ∈ s i, infEDist a (⋃ i, t i) ≤ ⨆ i, max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i)) ∧
    ⨆ i, ⨆ a ∈ t i, infEDist a (⋃ i, s i) ≤ ⨆ i, max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i))

Tactic:
iSup_le_iff,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
⊢ (∀ (i : ι),
      ∀ i_1 ∈ s i, infEDist i_1 (⋃ i, t i) ≤ ⨆ i, max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i))) ∧
    ∀ (i : ι),
      ∀ i_1 ∈ t i, infEDist i_1 (⋃ i, s i) ≤ ⨆ i, max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i))