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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l s
hG : TendstoLocallyUniformlyOn G g l s
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
⊢ TendstoLocallyUniformlyOn (F • G) (f • g) l s

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

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

Goal state before:
pp: G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ
⊢ c⁻¹ • closedBall x r = closedBall (c⁻¹ • x) r

Tactic:
smul_closedBall

Goal state after:
G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ
⊢ closedBall (c⁻¹ • x) r = closedBall (c⁻¹ • x) r
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist a (b * a) = ‖b‖

Tactic:
rw [← dist_one_left, ← dist_mul_left a 1 b, mul_one, mul_comm]

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ dist (a₁ * a₂) (b₁ * b₂) ≤ dist a₁ b₁ + dist a₂ b₂

Tactic:
by
  simpa only [dist_mul_left, dist_mul_right] using dist_triangle (a₁ * a₂) (b₁ * a₂) (b₁ * b₂)

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

Goal state before:
pp: 𝕜✝ : Type u_5
inst✝² : NormedDivisionRing 𝕜✝
ε : ℝ
εpos : ε > 0
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
h : ‖x‖ < 1
k : ℕ
hk : ‖x ^ k‖ < ε
⊢ ‖x‖ = 1

Tactic:
specialize h' _ hk

Goal state after:
𝕜✝ : Type u_5
inst✝² : NormedDivisionRing 𝕜✝
ε : ℝ
εpos : ε > 0
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
h : ‖x‖ < 1
k : ℕ
h' : x ^ k = 0
hk : ‖x ^ k‖ < ε
⊢ ‖x‖ = 1
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
l : List α
hl : l ≠ []
⊢ (map norm l).prod = ↑(map nnnorm l).prod

Tactic:
by simp [NNReal.coe_list_prod, List.map_map]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
l : List α
⊢ (map norm l).prod = ↑(map nnnorm l).prod

Tactic:
by simp [NNReal.coe_list_prod, List.map_map]

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 * (↑b - 1) - (↑b - 1) - (↑b * (↑a - 1) - (↑a - 1))‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖

Tactic:
mul_sub_one

Goal state after:
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖↑a * ↑b - ↑b * ↑a‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ = ‖↑a * ↑b - ↑a - (↑b - 1) - (↑b * ↑a - ↑b - (↑a - 1))‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: case pos
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
j : ι
hj : j = i
⊢ update x i y j = updateFinset x {i} (uniqueElim y) j

pp: case neg
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
j : ι
hj : ¬j = i
⊢ update x i y j = updateFinset x {i} (uniqueElim y) j

Tactic:
· cases hj
    simp only [dif_pos, Finset.mem_singleton, update_self, updateFinset]
    exact uniqueElim_default (α := fun j : ({i} : Finset ι) => π j) y

Goal state after:
case neg
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
j : ι
hj : ¬j = i
⊢ update x i y j = updateFinset x {i} (uniqueElim y) j
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: ι : Type u_1
π : ι → Type u_2
inst✝ : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
⊢ updateFinset x s (s.restrict x) = x

Tactic:
by
  ext i
  simp [updateFinset]

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

Goal state before:
pp: E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
⊢ dist (x + r • ‖y‖⁻¹ • y) (x - r • ‖y‖⁻¹ • y) ≤ diam (sphere x r)

Tactic:
apply dist_le_diam_of_mem isBounded_sphere

Goal state after:
case hx
E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
⊢ x + r • ‖y‖⁻¹ • y ∈ sphere x r

case hy
E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
⊢ x - r • ‖y‖⁻¹ • y ∈ sphere x r
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
⊢ ‖(algebraMap 𝕜 𝕜') x‖ = ‖x‖ * ‖1‖

Tactic:
rw [Algebra.algebraMap_eq_smul_one]
  exact norm_smul _ _

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
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Norm E
inst✝ : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x : E
⊢ ‖-x + x‖ = 0

Tactic:
by
    show ‖-x + x‖ = 0
    simp only [add_comm, ← sub_eq_add_neg, sub_self]
    have : (0 : E) = (0 : 𝕜) • (0 : E) := by simp
    rw [this, core.norm_smul]
    simp

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

Goal state before:
pp: case h₁
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
s : β → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
⊢ measurableAtom x ⊆ ⋂ y ∈ (measurableAtom x)ᶜ, s y

Tactic:
intro z hz

Goal state after:
case h₁
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
s : β → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
z : β
hz : z ∈ measurableAtom x
⊢ z ∈ ⋂ y ∈ (measurableAtom x)ᶜ, s y
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case h₂
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
s : β → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
⊢ (measurableAtom x)ᶜ ⊆ (⋂ y ∈ (measurableAtom x)ᶜ, s y)ᶜ

Tactic:
intro z hz

Goal state after:
case h₂
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
s : β → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
z : β
hz : z ∈ (measurableAtom x)ᶜ
⊢ z ∈ (⋂ y ∈ (measurableAtom x)ᶜ, s y)ᶜ
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:
intro z hz

Goal state after:
β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
z : β
hz : z ∈ measurableAtom x
⊢ z ∈ measurableAtom y
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case pos
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (i : δ) → MeasurableSpace (X i)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : j = i
⊢ Measurable fun v ↦ v.elim hj

Tactic:
subst hji
      simpa using measurable_fst

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

Goal state before:
pp: x : EReal
⊢ x.abs = 0 ↔ x = 0

Tactic:
by
  induction x
  · simp
  · simp only [abs_def, coe_eq_zero, ENNReal.ofReal_eq_zero, abs_nonpos_iff]
  · simp only [abs_top, ENNReal.top_ne_zero, top_ne_zero]

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

Goal state before:
pp: f : ℕ → ℝ≥0∞
hf : ∑' (x : ℕ), f x ≠ ∞
⊢ Tendsto f atTop (𝓝 0)

Tactic:
rw [← Nat.cofinite_eq_atTop]

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

Goal state before:
pp: b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
⊢ a < a' → (fun a ↦ a / b) a < (fun a ↦ a / b) a'

Tactic:
a_lt_a'

Goal state after:
b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
⊢ (fun a ↦ a / b) a < (fun a ↦ a / b) a'
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
⊢ a < a' → (fun a ↦ a / b) a' < (fun a ↦ a / b) a

Tactic:
a_lt_a'

Goal state after:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
⊢ (fun a ↦ a / b) a' < (fun a ↦ a / b) a
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inl
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
h₁ : limsup u ⊥ ≠ 0 ∨ limsup v ⊥ ≠ ⊤
h₂ : limsup u ⊥ ≠ ⊤ ∨ limsup v ⊥ ≠ 0
⊢ limsup (u * v) ⊥ ≤ limsup u ⊥ * limsup v ⊥

pp: case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
h✝ : f.NeBot
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

Tactic:
· rw [limsup_bot]; exact bot_le

Goal state after:
case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
h✝ : f.NeBot
⊢ limsup (u * v) f ≤ limsup u f * limsup v f
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ i, f ⁻¹' t i
⊢ ∃ (_ : s ⊆ ⋃ k, f ⁻¹' t k), ∑' (n : ℕ), m (f '' (fun k ↦ f ⁻¹' t k) n) ≤ ∑' (n : ℕ), m (t n)

Tactic:
refine ⟨ht, ENNReal.tsum_le_tsum fun n => ?_⟩

Goal state after:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ i, f ⁻¹' t i
n : ℕ
⊢ m (f '' (fun k ↦ f ⁻¹' t k) n) ≤ m (t n)
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ (restrict s) (OuterMeasure.ofFunction m m_empty) = OuterMeasure.ofFunction (fun t ↦ m (t ∩ s)) ⋯

Tactic:
by
      rw [restrict]
      simp only [inter_comm _ s, LinearMap.comp_apply]
      rw [comap_ofFunction _ (Or.inl hm)]
      simp only [map_ofFunction Subtype.coe_injective, Subtype.image_preimage_coe]

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

Goal state before:
pp: α : Type u_4
inst✝³ : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
a : α
inst✝² : PartialOrder β
inst✝¹ : CommGroup β
inst✝ : IsOrderedMonoid β
⊢ (∀ y < f⁻¹ a, ∀ᶠ (x' : α) in 𝓝[s] a, y < f⁻¹ x') ↔ UpperSemicontinuousWithinAt f s a

Tactic:
inv_surjective.forall,

Goal state after:
α : Type u_4
inst✝³ : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
a : α
inst✝² : PartialOrder β
inst✝¹ : CommGroup β
inst✝ : IsOrderedMonoid β
⊢ (∀ (x : β), x⁻¹ < f⁻¹ a → ∀ᶠ (x' : α) in 𝓝[s] a, x⁻¹ < f⁻¹ x') ↔ UpperSemicontinuousWithinAt f s a
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
s₁ : Set α
hs₁ : s₁ ∈ C
t₁ : Set β
ht₁ : t₁ ∈ D
s₂ : Set α
hs₂ : s₂ ∈ C
t₂ : Set β
ht₂ : t₂ ∈ D
hst : ((fun x1 x2 ↦ x1 ×ˢ x2) s₁ t₁ ∩ (fun x1 x2 ↦ x1 ×ˢ x2) s₂ t₂).Nonempty
⊢ (fun x1 x2 ↦ x1 ×ˢ x2) s₁ t₁ ∩ (fun x1 x2 ↦ x1 ×ˢ x2) s₂ t₂ ∈ image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D

Tactic:
prod_inter_prod

Goal state after:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
s₁ : Set α
hs₁ : s₁ ∈ C
t₁ : Set β
ht₁ : t₁ ∈ D
s₂ : Set α
hs₂ : s₂ ∈ C
t₂ : Set β
ht₂ : t₂ ∈ D
hst : ((s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)).Nonempty
⊢ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂) ∈ image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ x ∈ pt, ft x ∈ (fun n ↦ {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
⊢ MeasurableSet (ft i)

Tactic:
suffices h_le : m i ≤ ⨆ i ∈ S, m i from h_le (ft i) (ht_m i hi)

Goal state after:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ x ∈ pt, ft x ∈ (fun n ↦ {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
⊢ m i ≤ ⨆ i ∈ S, m i
Module: Mathlib.MeasureTheory.Measure.AEDisjoint

Goal state before:
pp: ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
⊢ ∃ t, (∀ (i : ι), MeasurableSet (t i)) ∧ (∀ (i : ι), μ (t i) = 0) ∧ Pairwise (Disjoint on fun i ↦ s i \ t i)

Tactic:
refine ⟨fun i => toMeasurable μ (s i ∩ ⋃ j ∈ ({i}ᶜ : Set ι), s j), fun i =>
    measurableSet_toMeasurable _ _, fun i => ?_, ?_⟩

Goal state after:
case refine_1
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i : ι
⊢ μ ((fun i ↦ toMeasurable μ (s i ∩ ⋃ j ∈ {i}ᶜ, s j)) i) = 0

case refine_2
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
⊢ Pairwise (Disjoint on fun i ↦ s i \ (fun i ↦ toMeasurable μ (s i ∩ ⋃ j ∈ {i}ᶜ, s j)) i)
Module: Mathlib.MeasureTheory.Measure.AEDisjoint

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
⊢ AEDisjoint μ t s

Tactic:
rwa [AEDisjoint, inter_comm]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
g : α → β
hf : NullMeasurable f μ
hg : f =ᵐ[μ] g
⊢ EventuallyMeasurable m (ae μ) g

Tactic:
exact EventuallyMeasurable.congr hf hg.symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
R : Type u_5
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
hf : QuasiMeasurePreserving f μa μb
c : R
⊢ map f (c • μa) ≪ c • μb

Tactic:
rw [Measure.map_smul]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
R : Type u_5
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
hf : QuasiMeasurePreserving f μa μb
c : R
⊢ c • map f μa ≪ c • μb
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: case pos
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : s ⊆ Iio b
⊢ comap Subtype.val (𝓝[<] b) = atTop ↔ s ⊆ Iio b ∧ ∀ a < b, (s ∩ Ioo a b).Nonempty

pp: case neg
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
⊢ comap Subtype.val (𝓝[<] b) = atTop ↔ s ⊆ Iio b ∧ ∀ a < b, (s ∩ Ioo a b).Nonempty

Tactic:
· simp only [hsub, true_and]
    constructor
    · intro h a ha
      have := preimage_mem_comap (m := ((↑) : s → X)) (Ioo_mem_nhdsLT ha)
      rw [h] at this
      rcases Filter.nonempty_of_mem this with ⟨⟨c, hcs⟩, hc⟩
      exact ⟨c, hcs, hc⟩
    · intro h
      refine (nhdsLT_basis_of_exists_lt (hsne.mono hsub)).comap _ |>.ext atTop_basis ?_ ?_
      · intro a hab
        rcases h a hab with ⟨c, hcs, hc⟩
        use ⟨c, hcs⟩
        simp_all [subset_def, hc.1.trans_le]
      · rintro ⟨a, has⟩ -
        use a, hsub has
        simp_all [subset_def, le_of_lt]

Goal state after:
case neg
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
⊢ comap Subtype.val (𝓝[<] b) = atTop ↔ s ⊆ Iio b ∧ ∀ a < b, (s ∩ Ioo a b).Nonempty
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : μ (s \ t) = 0
⊢ μ (s ∩ t) = μ s

Tactic:
rw [← sdiff_compl, measure_sdiff_null']; rwa [← sdiff_eq]

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
Union_As_finite : μ (⋃ i, As i) ≠ ∞
posmeas : Set ι := {i | 0 < μ (As i)}
posmeas_def : posmeas = {i | 0 < μ (As i)}
as : ℕ → ℝ≥0∞
left✝ : StrictAnti as
as_mem : ∀ (n : ℕ), as n ∈ Ioo 0 1
as_lim : Tendsto as atTop (𝓝 0)
fairmeas : ℕ → Set ι := fun n ↦ {i | as n ≤ μ (As i)}
countable_union : posmeas = ⋃ n, fairmeas n
⊢ (⋃ n, fairmeas n).Countable

Tactic:
refine countable_iUnion fun n => Finite.countable ?_

Goal state after:
α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
Union_As_finite : μ (⋃ i, As i) ≠ ∞
posmeas : Set ι := {i | 0 < μ (As i)}
posmeas_def : posmeas = {i | 0 < μ (As i)}
as : ℕ → ℝ≥0∞
left✝ : StrictAnti as
as_mem : ∀ (n : ℕ), as n ∈ Ioo 0 1
as_lim : Tendsto as atTop (𝓝 0)
fairmeas : ℕ → Set ι := fun n ↦ {i | as n ≤ μ (As i)}
countable_union : posmeas = ⋃ n, fairmeas n
n : ℕ
⊢ (fairmeas n).Finite
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Antitone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ∞
⊢ μ (⋂ i, s i) = ⨅ i, μ (s i)

Tactic:
refine measure_iInter_of_ae_monotone (ι := ιᵒᵈ) ?_ hsm hfin
  filter_upwards [hs] with ω hω using hω.dual_left

Goal state after:
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
⊢ Tendsto F atTop (𝓝 0)

Tactic:
have hzero : μ (⋂ n, f n) = 0 := by
    simp only [hfem, measure_empty]

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 (𝓝 0)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S : Set (Set α)
hc : S.Countable
hs : ⋃₀ S = univ
⊢ ⋃ i ∈ S, i = univ

Tactic:
rwa [← sUnion_eq_biUnion]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
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 : Set α
hu : MeasurableSet u
⊢ (μ.restrict t) u = (ν.restrict t) u

Tactic:
simp only [restrict_apply hu]

Goal state after:
α : 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 : Set α
hu : MeasurableSet u
⊢ μ (u ∩ t) = ν (u ∩ t)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : μ t = μ u
htu : t ⊆ u
ht_ne_top : μ u ≠ ∞
A : μ (u ∩ s) + μ (u \ s) ≤ μ (t ∩ s) + μ (u \ s)
B : μ (u \ s) ≠ ∞
⊢ μ (u ∩ s) ≤ μ (t ∩ s)

Tactic:
exact ENNReal.le_of_add_le_add_right B A

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

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
inst✝ : Countable ι
μ : ι → Measure α
s t : Set α
ht : MeasurableSet t
⊢ ((sum μ).restrict s) t = (sum fun i ↦ (μ i).restrict s) t

Tactic:
sum_apply _ ht,

Goal state after:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
inst✝ : Countable ι
μ : ι → Measure α
s t : Set α
ht : MeasurableSet t
⊢ ((sum μ).restrict s) t = ∑' (i : ι), ((μ i).restrict s) t
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
⊢ (memPartition f (n + 1)).Finite

Tactic:
rw [memPartition_succ]
    have : Finite (memPartition f n) := Set.finite_coe_iff.mp ih
    rw [← Set.finite_coe_iff]
    simp_rw [ofPred_exists, ← exists_prop, ofPred_exists, ofPred_or]
    refine Finite.Set.finite_biUnion (memPartition f n) _ (fun u _ ↦ ?_)
    rw [Set.finite_coe_iff]
    simp

Goal state after:
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
h_disj : Disjoint s (memPartitionSet f n a)
⊢ ¬Disjoint s (memPartitionSet f n a)

Tactic:
rw [not_disjoint_iff_nonempty_inter]

Goal state after:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
h_disj : Disjoint s (memPartitionSet f n a)
⊢ (s ∩ memPartitionSet f n a).Nonempty
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : μ ∈ m
this : sInf (toOuterMeasure '' m) ≤ μ.toOuterMeasure
s : Set α
hs : MeasurableSet s
⊢ (sInf m) s ≤ μ s

Tactic:
sInf_apply hs

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : μ ∈ m
this : sInf (toOuterMeasure '' m) ≤ μ.toOuterMeasure
s : Set α
hs : MeasurableSet s
⊢ (sInf (toOuterMeasure '' m)) s ≤ μ s
Module: Mathlib.MeasureTheory.Measure.Restrict

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

Tactic:
ext t

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ t ∈ ae (μ.restrict s) ↔ t ∈ ae μ ⊓ 𝓟 s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : ∀ μ' ∈ m, μ ≤ μ'
this : μ.toOuterMeasure ≤ sInf (toOuterMeasure '' m)
s : Set α
hs : MeasurableSet s
⊢ μ s ≤ (sInf m) s

Tactic:
sInf_apply hs

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : ∀ μ' ∈ m, μ ≤ μ'
this : μ.toOuterMeasure ≤ sInf (toOuterMeasure '' m)
s : Set α
hs : MeasurableSet s
⊢ μ s ≤ (sInf (toOuterMeasure '' m)) s