mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : SeminormedRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
x y : β
⊢ edist (s • x) (s • y) = ‖s‖₊ • edist x y

Tactic:
by
  simp only [edist_nndist, nndist_smul₀, ENNReal.coe_mul, ENNReal.smul_def, smul_eq_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * (‖r‖⁻¹ * ‖r • x‖) = ‖r • x‖

Tactic:
← mul_assoc,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖r‖⁻¹ * ‖r • x‖ = ‖r • x‖
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
y : ι × X
hy₁ : y ∈ (fun y ↦ (f y.2, F y.1 y.2)) ⁻¹' {p | dist p.1 p.2 < r / 2}
⊢ y ∈ Prod.snd ⁻¹' U → (f y.2, F y.1 y.2) ∈ (closedBall 0 (r / 2))ᶜ ×ˢ (closedBall 0 (r / 2))ᶜ

Tactic:
hy₂

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
y : ι × X
hy₁ : y ∈ (fun y ↦ (f y.2, F y.1 y.2)) ⁻¹' {p | dist p.1 p.2 < r / 2}
hy₂ : y ∈ Prod.snd ⁻¹' U
⊢ (f y.2, F y.1 y.2) ∈ (closedBall 0 (r / 2))ᶜ ×ˢ (closedBall 0 (r / 2))ᶜ
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✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
s : 𝕜
x : E × F
⊢ ‖s • x‖ ≤ ‖s‖ * ‖x‖

Tactic:
by
      simp only [norm_smul, Prod.norm_def, le_rfl]

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜' E
c : 𝕜
x : E
⊢ ‖(algebraMap 𝕜 𝕜') c‖ * ‖x‖ = ‖c‖ * ‖x‖

Tactic:
rw [norm_algebraMap']

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

Goal state before:
pp: α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
⊢ m ((⋃ n, s n) \ s n) ≤ ∑' (k : ℕ), m (s (k + n + 1) \ s (k + n))

Tactic:
refine (m.mono ?_).trans (measure_iUnion_le _)

Goal state after:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
⊢ (⋃ n, s n) \ s n ⊆ ⋃ i, s (i + n + 1) \ s (i + n)
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: s : SignType
z : ℤ
hz : Odd z
⊢ s ^ z = s

Tactic:
by
  obtain rfl | hs := eq_or_ne s 0
  · rw [zero_zpow]
    rintro rfl
    simp at hz
  obtain ⟨k, rfl⟩ := hz
  rw [zpow_add₀ hs, zpow_one, zpow_mul, zpow_two]
  cases s <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : a < 0
⊢ sign a = -1

Tactic:
rwa [sign_apply, if_neg <| asymm ha, if_pos]

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

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

Tactic:
induction a with
  | bot => simp
  | 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: a : EReal
a_0 : a ∈ Ioi 0
b : EReal
b_0 : b ∈ Ioi 0
⊢ a < b → (fun x ↦ x⁻¹) b < (fun x ↦ x⁻¹) a

Tactic:
a_b

Goal state after:
a : EReal
a_0 : a ∈ Ioi 0
b : EReal
b_0 : b ∈ Ioi 0
a_b : a < b
⊢ (fun x ↦ x⁻¹) b < (fun x ↦ x⁻¹) a
Module: Mathlib.Data.EReal.Inv

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

Tactic:
by
  rw [mul_comm (a / b) b, ← mul_div_left_comm a b b, div_self h₁ h₂ h₃, mul_one]

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

Goal state before:
pp: b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ -b⁻¹ * a ≤ -(b⁻¹ * a')

Tactic:
← neg_mul b⁻¹ a',

Goal state after:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ -b⁻¹ * a ≤ -b⁻¹ * a'
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ a ≤ c / b ↔ a * b ≤ c

Tactic:
nth_rw 1 [← @mul_div_cancel a b (ne_bot_of_gt h) h' h.ne']

Goal state after:
a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * (a / b) ≤ c / b ↔ a * b ≤ c
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a < c / b ↔ a * b < c

Tactic:
nth_rw 1 [← @mul_div_cancel a b (ne_bot_of_gt h) h' h.ne']

Goal state after:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ b * (a / b) < c / b ↔ a * b < c
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
⊢ (boundedBy m) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (t n)

Tactic:
simp [boundedBy, ofFunction_apply]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
C : ℝ
f : ℕ → α
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ C / 2 ^ n

Tactic:
by
  convert! dist_le_tsum_of_dist_le_of_tendsto _ hu₂ (summable_geometric_two' C) ha n
  simp only [add_comm n, pow_add, ← div_div]
  symm
  exact ((hasSum_geometric_two' C).div_const _).tsum_eq

Goal state after:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ x ∈ ⋂ x, dissipate s x, x ∈ ⋂ x, s x

Tactic:
dissipate_def,

Goal state after:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ x ∈ ⋂ x, ⋂ y, ⋂ (_ : y ≤ x), s y, x ∈ ⋂ x, s x
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ x ∈ ⋂ x, s x, x ∈ ⋂ x, dissipate s x

Tactic:
dissipate_def,

Goal state after:
case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ x ∈ ⋂ x, s x, x ∈ ⋂ x, ⋂ y, ⋂ (_ : y ≤ x), s y
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inter
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t s✝ t✝ : Set α
h_s✝ : generatePiSystem S s✝
h_t✝ : generatePiSystem S t✝
h_nonempty : (s✝ ∩ t✝).Nonempty
h_s : s✝ ∈ generatePiSystem T
h_u : t✝ ∈ generatePiSystem T
⊢ s✝ ∩ t✝ ∈ generatePiSystem T

Tactic:
exact isPiSystem_generatePiSystem T _ h_s _ h_u h_nonempty

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
⊢ ⋂ b ∈ T, f b = ⋂ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b

Tactic:
ext a
    constructor <;>
      · simp -proj only
          [Set.mem_iInter, Subtype.forall, Finset.set_biInter_finset_image]
        intro h1 b h_b h_b_in_T
        have h2 := h1 b h_b h_b_in_T
        revert h2
        rw [Subtype.val_injective.extend_apply]
        apply id

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.refine_1
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
m : ι
hm : m ∈ ↑{k}
⊢ m ∈ S

Tactic:
rw [Finset.mem_coe, Finset.mem_singleton] at hm
      rwa [hm]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ generateFrom (piiUnionInter (fun k ↦ {s k}) S) = generateFrom {t | ∃ k ∈ S, s k = t}

Tactic:
by
  refine le_antisymm (generateFrom_le ?_) (generateFrom_mono ?_)
  · rintro _ ⟨I, hI, f, hf, rfl⟩
    refine Finset.measurableSet_biInter _ fun m hm => measurableSet_generateFrom ?_
    exact ⟨m, hI hm, (hf m hm).symm⟩
  · rintro _ ⟨k, hk, rfl⟩
    refine ⟨{k}, fun m hm => ?_, s, fun i _ => ?_, ?_⟩
    · rw [Finset.mem_coe, Finset.mem_singleton] at hm
      rwa [hm]
    · exact Set.mem_singleton _
    · simp only [Finset.mem_singleton, Set.iInter_iInter_eq_left]

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

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

Tactic:
· exact (measure_mono Set.subset_union_right).trans_lt h

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
h_inter : ∀ (s₁ s₂ : Set α), d.Has s₁ → d.Has s₂ → d.Has (s₁ ∩ s₂)
f : ℕ → Set α
hf : ∀ (i : ℕ), d.Has (f i)
⊢ d.Has (⋃ i, f i)

Tactic:
by
    rw [← iUnion_disjointed]
    exact
      d.has_iUnion (disjoint_disjointed _) fun n =>
        disjointedRec (fun (t : Set α) i h => h_inter _ _ h <| d.has_compl <| hf i) (hf n)

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : MeasurableSet s₂
this : extend m (s₁ ∪ s₂ \ s₁) = extend m s₁ + extend m (s₂ \ s₁)
⊢ extend m s₁ ≤ m s₂ h₂

Tactic:
rw [union_sdiff_cancel hs] at this

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : MeasurableSet s₂
this : extend m s₂ = extend m s₁ + extend m (s₂ \ s₁)
⊢ extend m s₁ ≤ m s₂ h₂
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:
by
  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.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
h : μ ≪ ν
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (map f ν) s = 0 → (map f μ) s = 0

Tactic:
by simpa [hf, hs] using @h _

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

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

Tactic:
exact ae_eq_image_of_ae_eq_comap f μ hfi hf h.symm

Goal state after:
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) μ
s : Set α
hs : MeasurableSet s
⊢ c • μ (f '' s) = c • (comap f μ) s

pp: α : 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) μ
s : Set α
hs : MeasurableSet s
⊢ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ)

Tactic:
comap_apply₀ f μ h.1 h.2 hs.nullMeasurableSet

Goal state after:
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) μ
s : Set α
hs : MeasurableSet s
⊢ c • μ (f '' s) = c • μ (f '' s)

α : 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) μ
s : Set α
hs : MeasurableSet s
⊢ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ)
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : X → α
h : a < b
hb : IsSuccPrelimit b
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto f (𝓝[<] b) l

Tactic:
rw [← map_coe_Ioo_atTop h hb, tendsto_map'_iff, Function.comp_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ (μ + ν) univ < ∞

Tactic:
rw [Measure.coe_add, Pi.add_apply, ENNReal.add_lt_top]

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ μ univ < ∞ ∧ ν univ < ∞
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

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

Tactic:
have hFAnti : Antitone F :=
      fun i j hij => measure_mono (biInter_subset_biInter_left fun k hki => le_trans hki hij)

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

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

Tactic:
← hzero

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t) = μ (f ⁻¹' t ∩ s)

pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : (μ.restrict sᶜ) {a | ¬f a = b} = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ NullMeasurableSet {a | ¬f a = b} (μ.restrict sᶜ)

Tactic:
· apply le_antisymm _ (measure_mono inter_subset_left)
    apply (measure_mono (Eq.symm (inter_union_compl (f ⁻¹' t) s)).le).trans
    apply (measure_union_le _ _).trans
    suffices μ ((f ⁻¹' t) ∩ sᶜ) = 0 by simp [this]
    rw [← nonpos_iff_eq_zero, ← hs]
    gcongr
    exact fun x hx hfx ↦ ht (hfx ▸ hx)

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : (μ.restrict sᶜ) {a | ¬f a = b} = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ NullMeasurableSet {a | ¬f a = b} (μ.restrict sᶜ)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
e : α ≃ᵐ β
μ : Measure β
s : Set α
⊢ μ (⇑e '' s) = μ (⇑e.symm ⁻¹' s)

Tactic:
e.image_eq_preimage_symm

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
e : α ≃ᵐ β
μ : Measure β
s : Set α
⊢ μ (⇑e.symm ⁻¹' s) = μ (⇑e.symm ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : atTop.IsCountablyGenerated
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
⊢ AEMeasurable g (μ.restrict (Ioi x))

Tactic:
have : Nonempty α := ⟨x⟩

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : atTop.IsCountablyGenerated
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
⊢ AEMeasurable g (μ.restrict (Ioi x))
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s univ
t_cl : IsClosed[inst✝¹] t
T_open : ∀ t ∈ ∅, IsOpen[inst✝¹] t
T_count : ∅.Countable
T_int : t = ⋂₀ ∅
⊢ HasSeparatingCover s t

Tactic:
rw [(s.disjoint_univ).mp st_dis]

Goal state after:
case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s univ
t_cl : IsClosed[inst✝¹] t
T_open : ∀ t ∈ ∅, IsOpen[inst✝¹] t
T_count : ∅.Countable
T_int : t = ⋂₀ ∅
⊢ HasSeparatingCover ∅ t
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ ∀ t ∈ range Iio, MeasurableSet t

Tactic:
· rw [forall_mem_range]
    intro a
    exact GenerateMeasurable.basic _ isOpen_Iio

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ borel α = MeasurableSpace.generateFrom {S | ∃ l u, l ≤ u ∧ Icc l u = S}

Tactic:
simpa only [exists_prop, mem_univ, true_and] using
    (@dense_univ α _).borel_eq_generateFrom_Icc_mem_aux (fun _ _ => mem_univ _) fun _ _ _ _ =>
      mem_univ _

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
⊢ borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S}

Tactic:
convert!
    hd.orderDual.borel_eq_generateFrom_Ico_mem_aux hbot fun x y hlt he => hIoo y x hlt _ using 2

Goal state after:
case e'_3.e'_2
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
⊢ {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S} =
    {S | ∃ l ∈ ⇑OrderDual.ofDual ⁻¹' s, ∃ u ∈ ⇑OrderDual.ofDual ⁻¹' s, l < u ∧ Ico l u = S}

α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsTop x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
x y : αᵒᵈ
hlt : x < y
he : Ioo x y = ∅
⊢ Ioo y x = ∅
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
hlt✝ : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
hlt : dist y x < dist x z
⊢ False

Tactic:
dist_comm y

Goal state after:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
hlt✝ : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
hlt : dist x y < dist x z
⊢ False
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case h
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
⊢ thickening δ s ⊆ cthickening δ s

Tactic:
exact thickening_subset_cthickening ..

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
⊢ infEDist x (cthickening δ s) ≤ ENNReal.ofReal ε → infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ

Tactic:
exact fun hx => infEDist_le_infEDist_cthickening_add.trans (by grw [hx])

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
⊢ Measurable g

Tactic:
rcases isEmpty_or_nonempty ι with hι | ⟨⟨i⟩⟩
  · rcases eq_empty_or_nonempty s with rfl | ⟨x, hx⟩
    · convert! g'_meas
      rwa [compl_empty, eqOn_univ] at hg'
    · have A : ∀ b ∈ s, IsBot (g b) := by simpa using hg
      have B : ∀ b ∈ s, g b = g x := by
        intro b hb
        apply le_antisymm (A b hb (g x)) (A x hx (g b))
      have : g = s.piecewise (fun _y ↦ g x) g' := by
        ext b
        by_cases hb : b ∈ s
        · simp [hb, B]
        · simp [hb, hg' hb]
      rw [this]
      exact Measurable.piecewise hs measurable_const g'_meas
  · have : Nonempty ι := ⟨i⟩
    let f' : ι → δ → α := fun i ↦ s.piecewise (f i) g'
    suffices ∀ b, IsLUB { a | ∃ i, f' i b = a } (g b) from
      Measurable.isLUB (fun i ↦ Measurable.piecewise hs (hf i) g'_meas) this
    intro b
    by_cases hb : b ∈ s
    · have A : ∀ i, f' i b = f i b := fun i ↦ by simp [f', hb]
      simpa [A] using hg b hb
    · have A : ∀ i, f' i b = g' b := fun i ↦ by simp [f', hb]
      simp [A, hg' hb, isLUB_singleton]

Goal state after: