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

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
s : Finset α
hs : ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
⊢ f ⁻¹' e ∈ cofinite

Tactic:
refine s.eventually_cofinite_notMem.mono fun x hx ↦ ?_

Goal state after:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
s : Finset α
hs : ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
x : α
hx : x ∉ s
⊢ f x ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2

Tactic:
exact hf.tsum_mul_tsum_eq_tsum_sum_antidiagonal hg hfg

Goal state after:
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ ‖a ⊓ b - c ⊓ d‖ ≤ ‖a - c‖ + ‖b - d‖

Tactic:
← norm_abs_eq_norm (a - c),

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ ‖a ⊓ b - c ⊓ d‖ ≤ ‖|a - c|‖ + ‖b - d‖
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ ‖a ⊔ b - c ⊔ d‖ ≤ ‖a - c‖ + ‖b - d‖

Tactic:
← norm_abs_eq_norm (a - c),

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ ‖a ⊔ b - c ⊔ d‖ ≤ ‖|a - c|‖ + ‖b - d‖
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 : ‖x‖ < 1
k : ℕ
h' : x ^ k = 0
hk : ‖x ^ k‖ < ε
⊢ ‖x‖ = 1

Tactic:
simp [hx] at h'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ edist x y ≤ ↑(ratio f)⁻¹ * edist (f x) (f y)

Tactic:
have hr : ratio f ≠ 0 := ratio_ne_zero f
  exact mod_cast
    (ENNReal.mul_le_iff_le_inv (ENNReal.coe_ne_zero.2 hr) ENNReal.coe_ne_top).1 (edist_eq f x y).ge

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Ring R
v : AbsoluteValue R ℝ
x y : R
⊢ v (y + -x) = v (-y + x)

Tactic:
add_comm (-y),

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Ring R
v : AbsoluteValue R ℝ
x y : R
⊢ v (y + -x) = v (x + -y)
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: case inl
𝕜 : 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
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
this : IsAddTorsionFree E
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples 0)

Tactic:
rw [AddSubgroup.zmultiples_zero_eq_bot]
    exact Subsingleton.discreteTopology (α := ↑(⊥ : Subspace ℚ E))

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
a : ℝ
ha : a ≥ 0
ha' : a < 2
r' : ℝ
hr' : r' ≥ 0
hr'' : r' < r
⊢ a * r' ≤ diam (ball x r)

Tactic:
calc a * r' ≤ 2 * r' := by gcongr
    _ ≤ _ := by simpa only [← Metric.diam_sphere_eq x hr'.le]
      using diam_mono (sphere_subset_ball hr'') isBounded_ball

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

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

Tactic:
norm_algebraMap'

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x y : 𝕜
⊢ ‖x - y‖ = ‖x - y‖
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:
norm_algebraMap'

Goal state after:
𝕜 : 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
⊢ ‖c‖ * ‖x‖ = ‖c‖ * ‖x‖
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✝⁴ : Module 𝕜✝ E✝
inst✝³ : Norm E✝
𝕜 : Type u_8
E : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : Module 𝕜 E
core : Core 𝕜 E
r : 𝕜
x : E
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
by rw [core.norm_smul r x]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m a : OuterMeasure α
s : Set α
⊢ 0 s ≤ a s

Tactic:
simp only [zero_apply, zero_le]

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

Goal state before:
pp: α : Type u_1
f : SignType → α
⊢ Set.range f = {f zero, f neg, f pos}

Tactic:
classical rw [← Fintype.coe_image_univ, univ_eq]
  simp [Finset.coe_insert]

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

Goal state before:
pp: ⊢ IsClosed (range ENNReal.toEReal)

Tactic:
rw [range_coe_ennreal]; exact isClosed_Ici

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
⊢ LowerSemicontinuousWithinAt f s x ↔ f x ≤ liminf f (𝓝[s] x)

Tactic:
by
  constructor
  · intro h; unfold LowerSemicontinuousWithinAt at h
    by_contra! hf
    obtain ⟨z, ltz, y, ylt, h₁⟩ := hf.exists_disjoint_Iio_Ioi
    exact ltz.not_ge
      (le_liminf_of_le (by isBoundedDefault) ((h y ylt).mono fun _ h₂ =>
        le_of_not_gt fun h₃ => (h₁ _ h₃ _ h₂).false))
  exact fun hf y ylt => eventually_lt_of_lt_liminf (ylt.trans_le hf)

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

Goal state before:
pp: x : EReal
⊢ ContinuousAt toENNReal x

Tactic:
by_cases h_top : x = ⊤

Goal state after:
case pos
x : EReal
h_top : x = ⊤
⊢ ContinuousAt toENNReal x

case neg
x : EReal
h_top : ¬x = ⊤
⊢ ContinuousAt toENNReal x
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case neg
x : EReal
h_top : ¬x = ⊤
⊢ ContinuousAt toENNReal x

Tactic:
refine ContinuousOn.continuousAt ?_ (compl_singleton_mem_nhds_iff.mpr h_top)

Goal state after:
case neg
x : EReal
h_top : ¬x = ⊤
⊢ ContinuousOn toENNReal {⊤}ᶜ
Module: Mathlib.Topology.Instances.EReal.Lemmas

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

Tactic:
EReal.mul_comm (x := c)

Goal state after:
case inr
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ limsup (fun x ↦ u x * c) f = limsup u f * c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inr.a
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ ∀ y > limsup u f * c, ∀ᶠ (a : α) in f, u a * c < y

Tactic:
simpa [← EReal.lt_div_iff (by aesop) (by aesop)]
      using fun _ ↦ eventually_lt_of_limsup_lt

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

Goal state before:
pp: case coe.bot
a✝ : ℝ
h : (↑a✝, ⊥).1 ≠ ⊤ ∨ (↑a✝, ⊥).2 ≠ ⊥
h' : (↑a✝, ⊥).1 ≠ ⊥ ∨ (↑a✝, ⊥).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a✝, ⊥)

Tactic:
exact continuousAt_add_coe_bot _

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : Type u_3
I : Set ι
hI : I.Nonempty
f : α → β
m : ι → OuterMeasure β
this : Nonempty ↑I
⊢ (map f) (⨅ i ∈ I, (comap f) (m i)) = ⨅ i ∈ I, (map f) ((comap f) (m i))

Tactic:
← iInf_subtype'',

Goal state after:
α : Type u_1
ι : Type u_2
β : Type u_3
I : Set ι
hI : I.Nonempty
f : α → β
m : ι → OuterMeasure β
this : Nonempty ↑I
⊢ (map f) (⨅ i, (comap f) (m ↑i)) = ⨅ i ∈ I, (map f) ((comap f) (m i))
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
s : Set α
m : ι → OuterMeasure α
this : Nonempty ↑I
⊢ (restrict s) (⨅ i ∈ I, m i) = ⨅ i ∈ I, (restrict s) (m i)

Tactic:
← iInf_subtype'',

Goal state after:
α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
s : Set α
m : ι → OuterMeasure α
this : Nonempty ↑I
⊢ (restrict s) (⨅ i, m ↑i) = ⨅ i ∈ I, (restrict s) (m i)
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
t : Set α
⊢ m t = m (t ∩ (s₁ ∪ s₂)) + m (t \ (s₁ ∪ s₂))

Tactic:
rw [h₁ t, h₂ (t ∩ s₁), h₂ (t \ s₁), h₁ (t ∩ (s₁ ∪ s₂)), inter_sdiff_assoc _ _ s₁,
    Set.inter_assoc _ _ s₁, inter_eq_self_of_subset_right Set.subset_union_left,
    union_sdiff_left, h₂ (t ∩ s₁)]
  simp [sdiff_eq, add_assoc]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.inr
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ {univ}
⊢ ↑∅ ⊆ {i} ∧ ∃ f, (∀ x ∈ ∅, f x ∈ π x) ∧ s = ⋂ x ∈ ∅, f x

Tactic:
simpa only [Finset.coe_empty, subset_singleton_iff, mem_empty_iff_false, IsEmpty.forall_iff,
        imp_true_iff, Finset.notMem_empty, iInter_false, iInter_univ, true_and,
        exists_const] using! hs

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f n x
⊢ μ (aeSeqSet hf p)ᶜ = 0

Tactic:
rw [aeSeqSet, compl_compl, measure_toMeasurable]
  have hf_eq := fun i => (hf i).ae_eq_mk
  simp_rw [Filter.EventuallyEq, ← ae_all_iff] at hf_eq
  exact Filter.Eventually.and hf_eq hp

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

Goal state before:
pp: α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
⊢ MeasurableSpace.comap (fun x ↦ x ∈ s) ⊤ ≤ generateFrom {s}

Tactic:
rintro _ ⟨u, -, rfl⟩

Goal state after:
α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
u : Set Prop
⊢ MeasurableSet ((fun x ↦ x ∈ s) ⁻¹' u)
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) ⋯
⊢ ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯

Tactic:
intro f h

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) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
⊢ m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: β : Type u_2
γ : Type u_3
δ : Type u_4
x✝ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : Countable δ
l : Filter δ
inst✝¹ : l.IsCountablyGenerated
l' : Filter γ
inst✝ : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
u : ℕ → Set δ
hu : l.HasAntitoneBasis u
⊢ MeasurableSet {x | Tendsto (fun n ↦ f n x) l l'}

Tactic:
rcases (Filter.hasBasis_self.mpr hl'.exists_measurable_subset).exists_antitone_subbasis with
    ⟨v, v_meas, hv⟩

Goal state after:
β : Type u_2
γ : Type u_3
δ : Type u_4
x✝ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : Countable δ
l : Filter δ
inst✝¹ : l.IsCountablyGenerated
l' : Filter γ
inst✝ : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
u : ℕ → Set δ
hu : l.HasAntitoneBasis u
v : ℕ → Set γ
v_meas : ∀ (i : ℕ), v i ∈ l' ∧ MeasurableSet (v i)
hv : l'.HasAntitoneBasis fun i ↦ id (v i)
⊢ MeasurableSet {x | Tendsto (fun n ↦ f n x) l l'}
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 : ℕ → Set α), extend m (⋃ i, s i) ≤ ∑' (i : ℕ), extend m (s i)

Tactic:
refine extend_iUnion_le_tsum_nat' MeasurableSet.iUnion ?_; intro f h
  simp +singlePass only [iUnion_disjointed.symm]
  rw [mU (MeasurableSet.disjointed h) (disjoint_disjointed _)]
  refine ENNReal.tsum_le_tsum fun i => ?_
  rw [← extend_eq m, ← extend_eq m]
  exact extend_mono m0 mU (MeasurableSet.disjointed h _) (disjointed_le f _)

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

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

Tactic:
suffices ∀ c : ℝ≥0∞, (c • μ).map f = c • μ.map f by simpa using this (c • 1)
  clear c; intro c
  rcases eq_or_ne c 0 with (rfl | hc); · simp
  by_cases hf : AEMeasurable f μ
  · have hfc : AEMeasurable f (c • μ) :=
      ⟨hf.mk f, hf.measurable_mk, (ae_ennreal_smul_measure_iff hc).2 hf.ae_eq_mk⟩
    simp only [← mapₗ_mk_apply_of_aemeasurable hf, ← mapₗ_mk_apply_of_aemeasurable hfc, map_smulₛₗ,
      RingHom.id_apply]
    congr 1
    apply mapₗ_congr hfc.measurable_mk hf.measurable_mk
    exact .trans ((ae_ennreal_smul_measure_iff hc).1 hfc.ae_eq_mk.symm) hf.ae_eq_mk
  · have hfc : ¬AEMeasurable f (c • μ) := by
      intro hfc
      exact hf ⟨hfc.mk f, hfc.measurable_mk, (ae_ennreal_smul_measure_iff hc).1 hfc.ae_eq_mk⟩
    simp [map_of_not_aemeasurable hf, map_of_not_aemeasurable hfc]

Goal state after:
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 : α → ↑(Ioo a b)
ha : IsPredPrelimit a
⊢ Tendsto f l atBot ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝[>] a)

Tactic:
rw [← comap_coe_Ioo_nhdsGT a b ha, tendsto_comap_iff, Function.comp_def]

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
e : ι → ℕ
he : Injective e
t : ℕ → Set α
ht : Function.extend e s ⊥ = t
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)

Tactic:
suffices μ (⋃ n, t n) = ⨆ n, μ (t n) by
    simp only [← ht, Function.apply_extend μ, ← iSup_eq_iUnion, iSup_extend_bot he,
      Function.comp_def, Pi.bot_apply, bot_eq_empty, measure_empty] at this
    exact this.trans (iSup_extend_bot he _)

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
e : ι → ℕ
he : Injective e
t : ℕ → Set α
ht : Function.extend e s ⊥ = t
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
⊢ μ (⋃ n, t n) = ⨆ n, μ (t n)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
hC : IsCountablySpanning C
hm : ∀ t ∈ C, MeasurableSet t
ht : ∀ t ∈ C, (μ.restrict t) s = 0
⊢ μ s = 0

Tactic:
rw [← forall_measure_inter_isCountablySpanning_eq_zero hC]

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
hC : IsCountablySpanning C
hm : ∀ t ∈ C, MeasurableSet t
ht : ∀ t ∈ C, (μ.restrict t) s = 0
⊢ ∀ t ∈ C, μ (s ∩ t) = 0
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
⊢ (μ.restrict s) t = μ (t ∩ s)

Tactic:
by
  rw [← restrict_congr_set hs.toMeasurable_ae_eq,
    restrict_apply' (measurableSet_toMeasurable _ _),
    measure_congr ((ae_eq_refl t).inter hs.toMeasurable_ae_eq)]

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

Goal state before:
pp: α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ SigmaFinite (μ.trim hm)

Tactic:
by
  have : SigmaFinite ((μ.trim hm).trim hm₂) := by simpa [trim_trim]
  exact ⟨⟨
    { set := spanningSets ((μ.trim hm).trim hm₂)
      set_mem := fun _ => Set.mem_univ _
      finite := fun i => measure_spanningSets_trim_lt_top hm₂ (μ.trim hm) i
      spanning := iUnion_spanningSets _ }⟩⟩

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
⊢ (μ ⊓ ν) s = sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}

Tactic:
← sInf_pair,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
⊢ (sInf {μ, ν}) s = sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
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
hf : f =ᵐ[μ.restrict s] 0
⊢ s.indicator f =ᵐ[μ] 0

Tactic:
by
  rw [Filter.EventuallyEq, ae_restrict_iff' hs] at hf
  filter_upwards [hf] with x hx
  by_cases hxs : x ∈ s
  · simp only [hxs, hx hxs, Set.indicator_of_mem]
  · simp [hxs]

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

Goal state before:
pp: case refine_1.empty
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
⊢ ∃ S, ↑S ⊆ memPartition t n ∧ ∅ = ⋃₀ ↑S

Tactic:
exact ⟨∅, by simp, by simp⟩

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

Goal state before:
pp: case neg
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
⊢ MeasurableSet (Iio a)

Tactic:
convert_to MeasurableSet (⋃ (l ∈ t) (_ : l ≤ b), Icc l b)

Goal state after:
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
⊢ Iio a = ⋃ l ∈ t, ⋃ (_ : l ≤ b), Icc l b

case neg
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
⊢ MeasurableSet (⋃ l ∈ t, ⋃ (_ : l ≤ b), Icc l b)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case inl.inr
α : Type u
inst✝ : PseudoEMetricSpace α
t : Set α
fin : hausdorffEDist ∅ t ≠ ∞
ht : t.Nonempty
⊢ ∅ = ∅ ∧ t = ∅ ∨ ∅.Nonempty ∧ t.Nonempty

Tactic:
· rw [hausdorffEDist_comm] at fin
      exact Or.inr ⟨nonempty_of_hausdorffEDist_ne_top ht fin, ht⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
ε δ : ℝ
⊢ thickening ε (ball x δ) ⊆ ball x (ε + δ)

Tactic:
by
  rw [← thickening_singleton, ← thickening_singleton]
  apply thickening_thickening_subset

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 α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)
⊢ Measurable f

Tactic:
apply measurable_of_Ioi
  simp_rw [← compl_Iic, preimage_compl, MeasurableSet.compl_iff]
  assumption

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

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, f a ≠ ∞
a : ℝ≥0∞
ha✝ : a ∈ f.range
ha : a ≠ ∞
ha0 : a = 0
⊢ a * μ (⇑f ⁻¹' {a}) < ∞

Tactic:
subst a
      simp

Goal state after:
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : {b}ᶜ ∈ 𝓝 0
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ Tendsto (fun i x ↦ x ∈ As i) L (pi fun x ↦ pure (x ∈ A))

Tactic:
tendsto_pi

Goal state after:
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : {b}ᶜ ∈ 𝓝 0
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun x ↦ i ∈ As x) L (pure (i ∈ A))
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ Tendsto (fun i x ↦ x ∈ As i) L (pi fun x ↦ pure (x ∈ A))

Tactic:
tendsto_pi

Goal state after:
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun x ↦ i ∈ As x) L (pure (i ∈ A))