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

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
⊢ ratio (e.trans e') = ratio e * ratio e'

pp: case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (e.trans e') = ratio e * ratio e'

Tactic:
· have hY : ∀ x y : Y, edist x y = 0 ∨ edist x y = ∞ := e.surjective.forall₂.2 fun x y ↦ by
      refine (hX x y).imp (fun h ↦ ?_) fun h ↦ ?_ <;> simp [*, Dilation.ratio_ne_zero]
    simp [Dilation.ratio_of_trivial, *]

Goal state after:
case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (e.trans e') = ratio e * ratio e'
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: case inr.refine_2
α : Type u_5
inst✝¹ : Fintype α
ι : α → Type u
inst✝ : ∀ (a : α), Finite (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : ∀ (i : α), Nonempty (ι i)
i : (a : α) → ι a
hi : ∀ (a : α), f a (i a) = ⨆ i, f a i
⊢ ∏ a, ⨆ i, f a i ≤ ⨆ i, ∏ a, f a (i a)

Tactic:
simp only [← hi]

Goal state after:
case inr.refine_2
α : Type u_5
inst✝¹ : Fintype α
ι : α → Type u
inst✝ : ∀ (a : α), Finite (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : ∀ (i : α), Nonempty (ι i)
i : (a : α) → ι a
hi : ∀ (a : α), f a (i a) = ⨆ i, f a i
⊢ ∏ x, f x (i x) ≤ ⨆ i, ∏ a, f a (i a)
Module: Mathlib.Data.Finset.Update

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

Tactic:
simp [updateFinset]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
f : α → β
g : β → γ
⊢ Measurable f ↔ Measurable (g ∘ f)

Tactic:
by
  simp [measurable_iff_comap_le]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : Measurable (s.indicator fun x ↦ b)
⊢ MeasurableSet s

pp: case mpr
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : MeasurableSet s
⊢ Measurable (s.indicator fun x ↦ b)

Tactic:
· convert! h (MeasurableSet.singleton (0 : β)).compl
    ext a
    simp [NeZero.ne b]

Goal state after:
case mpr
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : MeasurableSet s
⊢ Measurable (s.indicator fun x ↦ b)
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

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

Tactic:
rw [← biUnion_of_singleton s]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : s.Countable
⊢ MeasurableSet (⋃ x ∈ s, {x})
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (inclusion h '' Subtype.val ⁻¹' u)

Tactic:
convert! (measurable_subtype_coe hu).inter hs

Goal state after:
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
⊢ inclusion h '' Subtype.val ⁻¹' u = Subtype.val ⁻¹' u ∩ Subtype.val ⁻¹' s
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)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑f

Tactic:
by
  obtain ⟨δ, hδ, hUε⟩ := Metric.mem_nhds_iff.mp hs
  obtain ⟨C, hC⟩ := (isBounded_iff_subset_ball 0).1 (hbounded.subset <| image_mono hUε)
  refine continuous_of_continuousAt_zero _ (continuousAt_iff.2 fun ε (hε : _ < _) => ?_)
  simp only [dist_zero_right, map_zero]
  simp only [subset_def, mem_image, mem_ball, dist_zero_right, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂] at hC
  have hC₀ : 0 < C := (norm_nonneg _).trans_lt <| hC 0 (by simpa)
  obtain ⟨n, hn⟩ := exists_nat_gt (C / ε)
  have hnpos : 0 < (n : ℝ) := (div_pos hC₀ hε).trans hn
  have hn₀ : n ≠ 0 := by rintro rfl; simp at hnpos
  refine ⟨δ / n, div_pos hδ hnpos, fun {x} hxδ => ?_⟩
  calc
    ‖f x‖
    _ = ‖(n : ℝ)⁻¹ • f (n • x)‖ := by simp [← Nat.cast_smul_eq_nsmul ℝ, hn₀]
    _ ≤ ‖(n : ℝ)⁻¹‖ * ‖f (n • x)‖ := norm_smul_le ..
    _ < ‖(n : ℝ)⁻¹‖ * C := by
      gcongr
      · simpa [pos_iff_ne_zero]
      · refine hC _ <| norm_nsmul_le.trans_lt ?_
        simpa only [norm_mul, Real.norm_natCast, lt_div_iff₀ hnpos, mul_comm] using hxδ
    _ = (n : ℝ)⁻¹ * C := by simp
    _ < (C / ε : ℝ)⁻¹ * C := by gcongr
    _ = ε := by simp [hC₀.ne']

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

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β
m m' : OuterMeasure α
s : Set β
⊢ ((map f) (m ⊔ m')) s = ((map f) m ⊔ (map f) m') s

Tactic:
simp only [map_apply, sup_apply]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →A[R] B
h : (fun f ↦ ⇑f.toAlgHom) f = (fun f ↦ ⇑f.toAlgHom) g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
g : A →A[R] B
toAlgHom✝ : A →ₐ[R] B
cont✝ : Continuous[inst✝⁴, inst✝²] (↑↑toAlgHom✝.toRingHom).toFun
h : (fun f ↦ ⇑f.toAlgHom) { toAlgHom := toAlgHom✝, cont := cont✝ } = (fun f ↦ ⇑f.toAlgHom) g
⊢ { toAlgHom := toAlgHom✝, cont := cont✝ } = g
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →A[R] B
⊢ ↑f = ↑g ↔ f = g

Tactic:
cases f

Goal state after:
case mk
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
B : Type u_3
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
g : A →A[R] B
toAlgHom✝ : A →ₐ[R] B
cont✝ : Continuous[inst✝⁴, inst✝²] (↑↑toAlgHom✝.toRingHom).toFun
⊢ ↑{ toAlgHom := toAlgHom✝, cont := cont✝ } = ↑g ↔ { toAlgHom := toAlgHom✝, cont := cont✝ } = g
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: case zero
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m : ℕ
⊢ ↑0 ≤ 0

Tactic:
cast_zero

Goal state after:
case zero
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m : ℕ
⊢ 0 ≤ 0
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case neg
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∑' (i : α), f i = 0
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

Tactic:
have : Tendsto (fun s : Finset α => ∑ j ∈ s, a * f j) atTop (𝓝 (a * ∑' i, f i)) := by
      simp only [← Finset.mul_sum]
      exact ENNReal.Tendsto.const_mul ENNReal.summable.hasSum (Or.inl hf)

Goal state after:
case neg
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∑' (i : α), f i = 0
this : Tendsto (fun s ↦ ∑ j ∈ s, a * f j) atTop (𝓝 (a * ∑' (i : α), f i))
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x : ℝ
⊢ sign (-x) = -sign x

Tactic:
Left.sign_neg

Goal state after:
x : ℝ
⊢ -sign x = -sign x
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
s : Set α
⊢ Semicontinuous (s.domRestrict r) ↔ ∀ x ∈ s, SemicontinuousWithinAt r s x

Tactic:
Semicontinuous,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
s : Set α
⊢ (∀ (x : ↑s), SemicontinuousAt (s.domRestrict r) x) ↔ ∀ x ∈ s, SemicontinuousWithinAt r s x
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace γ
inst✝ : Preorder β
f g : α → β
x : α
s t : Set α
y z : β
⊢ (Semicontinuous fun x1 x2 ↦ ¬f x1 ≤ x2) ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y

Tactic:
Semicontinuous,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace γ
inst✝ : Preorder β
f g : α → β
x : α
s t : Set α
y z : β
⊢ (∀ (x : α), SemicontinuousAt (fun x1 x2 ↦ ¬f x1 ≤ x2) x) ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
a_0 : a ∈ Ioi 0
b : EReal
⊢ b ∈ Ioi 0 → a < b → (fun x ↦ x⁻¹) b < (fun x ↦ x⁻¹) a

Tactic:
b_0

Goal state after:
a : EReal
a_0 : a ∈ Ioi 0
b : EReal
b_0 : b ∈ Ioi 0
⊢ a < b → (fun x ↦ x⁻¹) b < (fun x ↦ x⁻¹) a
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
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ edist (f n) a ≤ ∑' (m : ℕ), d (n + m)

Tactic:
by
  refine le_of_tendsto (tendsto_const_nhds.edist ha) (mem_atTop_sets.2 ⟨n, fun m hnm => ?_⟩)
  change edist _ _ ≤ _
  refine le_trans (edist_le_Ico_sum_of_edist_le hnm fun _ _ => hf _) ?_
  rw [Finset.sum_Ico_eq_sum_range]
  exact ENNReal.summable.sum_le_tsum _ (fun _ _ => zero_le)

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

Goal state before:
pp: s : Set EReal
⊢ (∃ i, True ∧ Ioi ↑i ⊆ s) ↔ ∃ y, Ioi ↑y ⊆ s

Tactic:
simp only [true_and]

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

Goal state before:
pp: s : Set EReal
⊢ (∃ i, True ∧ Iio ↑i ⊆ s) ↔ ∃ y, Iio ↑y ⊆ s

Tactic:
simp only [true_and]

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

Goal state before:
pp: case pos
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : x = ⊥
⊢ ContinuousAt (fun x ↦ ENNReal.ofReal x.toReal) x

Tactic:
refine tendsto_nhds_of_eventually_eq ?_

Goal state after:
case pos
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : x = ⊥
⊢ ∀ᶠ (x' : EReal) in 𝓝 x, ENNReal.ofReal x'.toReal = (fun x ↦ ENNReal.ofReal x.toReal) x
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
rcases f.eq_or_neBot with rfl | _
  · rw [limsup_bot, limsup_bot, liminf_bot, bot_mul_top]
  have u0 : 0 ≤ limsup u f := le_limsup_of_frequently_le hu
  have uv0 : 0 ≤ limsup (u * v) f :=
    le_limsup_of_frequently_le <| (hu.and_eventually hv).mono fun _ ⟨hu, hv⟩ ↦ mul_nonneg hu hv
  refine mul_le_of_forall_lt_of_nonneg u0 uv0 fun a ha b hb ↦ (le_limsup_iff).2 fun c c_ab ↦ ?_
  refine (((frequently_lt_of_lt_limsup) (mem_Ioo.1 ha).2).and_eventually
    <| (eventually_lt_of_lt_liminf (mem_Ioo.1 hb).2).and
    <| hv).mono fun x ⟨xa, ⟨xb, vx⟩⟩ ↦ ?_
  exact c_ab.trans_le (mul_le_mul xa.le xb.le (mem_Ioo.1 hb).1.le ((mem_Ioo.1 ha).1.le.trans xa.le))

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

Goal state before:
pp: ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
⊢ (fun i ↦ ↑(w i)) i * ↑((fun i ↦ δ' i / max 1 (w i)) i) ≤ ↑(δ' i)

Tactic:
coe_div (this i).ne'

Goal state after:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
⊢ (fun i ↦ ↑(w i)) i * (↑(δ' i) / ↑(max 1 (w i))) ≤ ↑(δ' i)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
ι : Sort u_3
ι' : Sort u_4
inst✝ : LinearOrder α
Ixx : α → α → Set α
p : α → α → Prop
Hne : ∀ {a b : α}, (Ixx a b).Nonempty → p a b
Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)
f : ι → α
g : ι' → α
⊢ IsPiSystem {S | ∃ i j, p (f i) (g j) ∧ Ixx (f i) (g j) = S}

Tactic:
by
  simpa only [exists_range_iff] using isPiSystem_Ixx_mem (@Hne) (@Hi) (range f) (range g)

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f μ
⊢ ∀ᵐ (x : β) ∂map f μ, x ∈ range f

Tactic:
change range f ∈ ae (μ.map f)
    rw [mem_ae_map_iff h hf]
    filter_upwards using mem_range_self

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

Goal state before:
pp: case hc
α : Type u_1
β : Type u_2
s : Set α
x✝¹ : MeasurableSpace α
x✝ : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)

Tactic:
exact ⟨hfi, hf⟩

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

Goal state before:
pp: α : 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 (((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯)
⊢ (((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯) s = μ (f '' s)

Tactic:
toMeasure_apply₀ _ _ hs,

Goal state after:
α : 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 (((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯)
⊢ ((OuterMeasure.comap f) μ.toOuterMeasure) s = μ (f '' s)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ (μ.restrict t) (u ∩ s) = μ (u ∩ s)

Tactic:
restrict_eq_self

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ μ (u ∩ s) = μ (u ∩ s)

case h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ u ∩ s ⊆ t
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
s : Set α
hs : NullMeasurableSet s (m.toMeasure h)
⊢ (m.toMeasure h) s ≤ m s

Tactic:
rcases hs.exists_measurable_subset_ae_eq with ⟨t, hts, htm, heq⟩

Goal state after:
α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
s : Set α
hs : NullMeasurableSet s (m.toMeasure h)
t : Set α
hts : t ⊆ s
htm : MeasurableSet t
heq : t =ᵐ[m.toMeasure h] s
⊢ (m.toMeasure h) s ≤ m s
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 ≠ ∞
⊢ μ (t ∩ s) = μ (u ∩ s)

Tactic:
refine le_antisymm (by gcongr) ?_

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : μ t = μ u
htu : t ⊆ u
ht_ne_top : μ u ≠ ∞
⊢ μ (u ∩ s) ≤ μ (t ∩ s)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ μ (t' ∩ u) = μ (t ∩ u)

Tactic:
apply le_antisymm _ (by gcongr)

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := ⋯
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋯
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ μ (t' ∩ u) ≤ μ (t ∩ u)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : IsEmpty α
m : MeasurableSpace α
μ ν : Measure α
⊢ μ = ν

Tactic:
ext1 s _

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : IsEmpty α
m : MeasurableSpace α
μ ν : Measure α
s : Set α
a✝ : MeasurableSet s
⊢ μ s = ν s
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x | p x} (μ.restrict s)
⊢ μ ({x | p x}ᶜ ∩ s) = 0 ↔ μ {x | x ∈ s → p x}ᶜ = 0

Tactic:
rw [iff_iff_eq]

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x | p x} (μ.restrict s)
⊢ (μ ({x | p x}ᶜ ∩ s) = 0) = (μ {x | x ∈ s → p x}ᶜ = 0)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
⊢ μ ({x | p x}ᶜ ∩ s) = 0 ↔ μ {x | x ∈ s → p x}ᶜ = 0

Tactic:
rw [iff_iff_eq]

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
⊢ (μ ({x | p x}ᶜ ∩ s) = 0) = (μ {x | x ∈ s → p x}ᶜ = 0)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : Group β
inst✝¹ : LE β
inst✝ : MulRightMono β
f g : α → β
⊢ 1 ≤ᵐ[μ] g / f ↔ f ≤ᵐ[μ] g

Tactic:
by
  refine ⟨fun h ↦ h.mono fun a ha ↦ ?_, fun h ↦ h.mono fun a ha ↦ ?_⟩
  · rwa [Pi.one_apply, Pi.div_apply, one_le_div'] at ha
  · rwa [Pi.one_apply, Pi.div_apply, one_le_div']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : Set (Measure α)
x✝ : MeasurableSpace α
f : ℕ → Set α
a✝¹ : ∀ (i : ℕ), MeasurableSet (f i)
a✝ : Pairwise (Disjoint on f)
⊢ ⊤ (⋃ i, f i) = ∑' (i : ℕ), ⊤ (f i)

Tactic:
refine (measure_iUnion_le _).antisymm ?_

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : Set (Measure α)
x✝ : MeasurableSpace α
f : ℕ → Set α
a✝¹ : ∀ (i : ℕ), MeasurableSet (f i)
a✝ : Pairwise (Disjoint on f)
⊢ ∑' (i : ℕ), ⊤ (f i) ≤ ⊤ (⋃ i, f i)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (toMeasurable μ s)) t = (μ.restrict s) t

Tactic:
rw [restrict_apply ht, inter_comm t, measure_toMeasurable_inter_of_sFinite ht,
      restrict_apply ht, inter_comm t]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
⊢ s.indicator f =ᵐ[μ.restrict s] f

Tactic:
by
  classical exact piecewise_ae_eq_restrict hs

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

Goal state before:
pp: β : Type u_2
α : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty β
h : CountableOrCountablyGenerated (α × β) γ
⊢ CountableOrCountablyGenerated α γ

Tactic:
rcases h.countableOrCountablyGenerated with (h | h)

Goal state after:
case inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty β
h✝ : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
⊢ CountableOrCountablyGenerated α γ

case inr
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty β
h✝ : CountableOrCountablyGenerated (α × β) γ
h : CountablyGenerated γ
⊢ CountableOrCountablyGenerated α γ
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: β : Type u_2
α : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty α
h : CountableOrCountablyGenerated (α × β) γ
⊢ CountableOrCountablyGenerated β γ

Tactic:
rcases h.countableOrCountablyGenerated with (h | h)

Goal state after:
case inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty α
h✝ : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
⊢ CountableOrCountablyGenerated β γ

case inr
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty α
h✝ : CountableOrCountablyGenerated (α × β) γ
h : CountablyGenerated γ
⊢ CountableOrCountablyGenerated β γ
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
mem_C : ∀ {i : ι}, i ∈ F → ∀ {C : Finset ι} {x : α}, x ∈ P C → x ∈ s i → i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι}, C₁ ∈ Cs → ∀ {x : α}, x ∈ P C₁ ∩ P C₂ → C₁ ⊆ C₂
⊢ ∑' (C : Finset ι), ∑ i ∈ F, (G i).indicator (fun C ↦ (μ.restrict (P C)) t) C =
    ∑ C ∈ Cs, ∑ i ∈ F, (↑C).indicator (fun x ↦ (μ.restrict (P C)) t) i

Tactic:
by
      rw [sum_eq_tsum_indicator]
      congr with C
      by_cases hC : C ∈ F.powerset <;> by_cases hC' : C = ∅ <;>
        simp [hC, hC', Cs, G, indicator, -Finset.mem_powerset, -coe_powerset]

Goal state after:
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:
(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