mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
h' : ∀ (n : ℕ), ∃ s, μ s = 0 ∧ ν sᶜ ≤ (1 / 2) ^ n
⊢ μ ⟂ₘ ν

Tactic:
choose s hs₂ hs₃ using h'

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
s : ℕ → Set α
hs₂ : ∀ (n : ℕ), μ (s n) = 0
hs₃ : ∀ (n : ℕ), ν (s n)ᶜ ≤ (1 / 2) ^ n
⊢ μ ⟂ₘ ν
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s

Tactic:
have : s ∩ {a} = {a} := by simpa

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
this : s ∩ {a} = {a}
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
⊢ map f μ = sum fun b ↦ μ (f ⁻¹' {b}) • dirac b

Tactic:
ext s
  have : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y}) := fun y _ => hf (measurableSet_singleton _)
  simp [← tsum_measure_preimage_singleton (to_countable s) this, *,
    tsum_subtype s fun b => μ (f ⁻¹' {b}), ← indicator_mul_right s fun b => μ (f ⁻¹' {b})]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ sᶜ = 0
t : Set α
ht : ν tᶜ = 0
hst : Disjoint s t
this : ⊥ = 0
u : Set α
hu : MeasurableSet u
x✝ : u.Nonempty
⊢ ⊥ = μ (t ∩ u) + ν (tᶜ ∩ u)

Tactic:
simp [measure_mono_null (inter_subset_left.trans hst.subset_compl_left) hs,
    measure_mono_null inter_subset_left ht]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
⊢ count s = ∞ ↔ s.Infinite

Tactic:
by
  by_cases hs : s.Finite
  · simp [Set.Infinite, hs, count_apply_finite' hs s_mble]
  · change s.Infinite at hs
    simp [hs, count_apply_infinite]

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

Goal state before:
pp: α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
y : α
x : ℕ → ℕ
hx : ∀ (n : ℕ), y ∈ closedBall (u (x n)) ((1 / 2) ^ n)
I : (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty
J : ∀ (n : ℕ), dist (g ⟨x, I⟩) y ≤ (1 / 2) ^ n + (1 / 2) ^ n
L : Tendsto (fun n ↦ (1 / 2) ^ n + (1 / 2) ^ n) atTop (𝓝 0)
⊢ dist (g ⟨x, I⟩) y ≤ 0

Tactic:
exact ge_of_tendsto' L J

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : AEMeasurable f m.join
hfm : Measurable f
⊢ ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m

Tactic:
simp_rw [lintegral_eq_iSup_eapprox_lintegral hfm, SimpleFunc.lintegral,
    join_apply (SimpleFunc.measurableSet_preimage _ _)]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : AEMeasurable f m.join
hfm : Measurable f
⊢ ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * ∫⁻ (μ : Measure α), μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m =
    ∫⁻ (μ : Measure α), ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case left.hV
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
ε : ℝ≥0∞
hε : 0 < ε
K : Finset ι
hK : ∑' (i : { j // j ∉ K }), 2⁻¹ ^ encode ↑i < ε / 2
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ * ↑K.card < ε / 2
⊢ ∀ (i : ↑↑K), {p | edist (p.1 ↑i) (p.2 ↑i) < δ} ∈ ⨅ i_1, ⨅ (_ : 0 < i_1), 𝓟 {a | edist (a.1 ↑i) (a.2 ↑i) < i_1}

Tactic:
rintro ⟨i, hi⟩
        refine mem_iInf_of_mem δ (mem_iInf_of_mem δpos ?_)
        simp only [mem_principal, Subset.rfl]

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

Goal state before:
pp: case iUnion
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s : Set (α × β)
f : ℕ → Set (α × β)
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Measurable fun x ↦ ν (Prod.mk x ⁻¹' f i)
⊢ Measurable fun x ↦ ν (Prod.mk x ⁻¹' ⋃ i, f i)

Tactic:
have (a : α) : ν (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' i, ν (Prod.mk a ⁻¹' f i) := by
      rw [preimage_iUnion, measure_iUnion]
      exacts [hfd.mono fun _ _ ↦ .preimage _, fun i ↦ measurable_prodMk_left (hfm i)]

Goal state after:
case iUnion
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s : Set (α × β)
f : ℕ → Set (α × β)
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Measurable fun x ↦ ν (Prod.mk x ⁻¹' f i)
this : ∀ (a : α), ν (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' (i : ℕ), ν (Prod.mk a ⁻¹' f i)
⊢ Measurable fun x ↦ ν (Prod.mk x ⁻¹' ⋃ i, f i)
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hst : IsComplement S T
a : G
ha : a ∈ S
b : G
hb : b ∈ S
hab : a ≠ b
⊢ ∀ ⦃a_1 : G⦄, a_1 ∈ (fun x ↦ x • T) a → ∀ ⦃b_1 : G⦄, b_1 ∈ (fun x ↦ x • T) b → a_1 ≠ b_1

Tactic:
rintro _ ⟨c, hc, rfl⟩ _ ⟨d, hd, rfl⟩
  exact hst.1.ne (a₁ := (⟨a, ha⟩, ⟨c, hc⟩)) (a₂ := (⟨b, hb⟩, ⟨d, hd⟩)) (by simp [hab])

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ g * (↑⟨g, hg⟩)⁻¹ = ↑⟨1, h1⟩

Tactic:
mul_inv_cancel

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ 1 = ↑⟨1, h1⟩
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
⊢ ↑(hST.equiv g).2 = g ↔ g ∈ T

Tactic:
constructor
  · intro h
    rw [← h]
    exact Subtype.prop _
  · intro h
    rw [hST.equiv_snd_eq_self_of_mem_of_one_mem h1 h]

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst✝¹] (s n)
h'' : univ ⊆ ⋃ n, s n
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet (⋃ n, A n)
hr : r > μ (⋃ n, A n)
HA : μ (⋃ n, A n) < ∞
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : μ (⋃ n, A n) + ∑' (i : ℕ), δ i < r
n : ℕ
H₁ : ∀ (t : Set α), (μ.restrict (s n)) t = μ (t ∩ s n)
Ht : (μ.restrict (s n)) (A n) ≠ ∞
⊢ ∃ U ⊇ A n, IsOpen[inst✝¹] U ∧ μ U < μ (A n) + δ n

Tactic:
rcases (A n).exists_isOpen_lt_add Ht (δ0 n).ne' with ⟨U, hAU, hUo, hU⟩

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst✝¹] (s n)
h'' : univ ⊆ ⋃ n, s n
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet (⋃ n, A n)
hr : r > μ (⋃ n, A n)
HA : μ (⋃ n, A n) < ∞
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : μ (⋃ n, A n) + ∑' (i : ℕ), δ i < r
n : ℕ
H₁ : ∀ (t : Set α), (μ.restrict (s n)) t = μ (t ∩ s n)
Ht : (μ.restrict (s n)) (A n) ≠ ∞
U : Set α
hAU : U ⊇ A n
hUo : IsOpen[inst✝¹] U
hU : (μ.restrict (s n)) U < (μ.restrict (s n)) (A n) + δ n
⊢ ∃ U ⊇ A n, IsOpen[inst✝¹] U ∧ μ U < μ (A n) + δ n
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ μ (c • (s \ c⁻¹ • t)) = μ (c • s \ t)

Tactic:
smul_set_sdiff,

Goal state after:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ μ (c • s \ c • c⁻¹ • t) = μ (c • s \ t)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : ℕ → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : ℕ → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed[inst✝²] (F n)
hUo : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hF : ∀ (n : ℕ), μ (s n) ≤ μ (F n) + δ n
hU : ∀ (n : ℕ), μ (U n) ≤ μ (s n) + δ n
this : Tendsto (fun t ↦ ∑ k ∈ t, μ (s k) + ε / 2) atTop (𝓝 (μ (⋃ n, s n) + ε / 2))
t : Finset ℕ
ht : μ (⋃ n, s n) < ∑ k ∈ t, μ (s k) + ε / 2
⊢ ∑ k ∈ t, μ (s k) + ε / 2 ≤ ∑ k ∈ t, μ (F k) + ∑ k ∈ t, δ k + ε / 2

Tactic:
← sum_add_distrib

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : ℕ → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : ℕ → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed[inst✝²] (F n)
hUo : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hF : ∀ (n : ℕ), μ (s n) ≤ μ (F n) + δ n
hU : ∀ (n : ℕ), μ (U n) ≤ μ (s n) + δ n
this : Tendsto (fun t ↦ ∑ k ∈ t, μ (s k) + ε / 2) atTop (𝓝 (μ (⋃ n, s n) + ε / 2))
t : Finset ℕ
ht : μ (⋃ n, s n) < ∑ k ∈ t, μ (s k) + ε / 2
⊢ ∑ k ∈ t, μ (s k) + ε / 2 ≤ ∑ x ∈ t, (μ (F x) + δ x) + ε / 2
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
⊢ MeasurableSet {x | ∃ c, Tendsto (fun n ↦ f n x) l (𝓝 c)}

Tactic:
let := TopologicalSpace.upgradeIsCompletelyPseudoMetrizable γ

Goal state after:
case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
⊢ MeasurableSet {x | ∃ c, Tendsto (fun n ↦ f n x) l (𝓝 c)}
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ AEMeasurable (fun z ↦ f z.swap) ((ν.prod μ).restrict (t ×ˢ s))

Tactic:
refine AEMeasurable.comp_measurable ?_ measurable_swap
    convert! hf
    rw [← Measure.prod_restrict, Measure.prod_swap, Measure.prod_restrict]

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

Goal state before:
pp: X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst✝²] F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K

Tactic:
have hBU : ⋃ n, F ∩ B n = F := by rw [← inter_iUnion, iUnion_compactCovering, Set.inter_univ]

Goal state after:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst✝²] F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ n, F ∩ B n = F
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Mul G
inst✝³ : Inv G
inst✝² : MeasurableMul₂ G
inst✝¹ : MeasurableInv G
f g : G → ℝ≥0∞
μ : Measure G
inst✝ : SFinite μ
hf : Measurable f
hg : Measurable g
⊢ Measurable (f ⋆ₘₗ[μ] g)

Tactic:
unfold mlconvolution
  fun_prop

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SFinite μ
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable (f ⋆ₘₗ[μ] g) μ

Tactic:
unfold mlconvolution
  fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
inst✝ : IsFiniteMeasure μ
⊢ μ.InnerRegular

Tactic:
constructor
  convert! h.innerRegular with s
  simp [measure_ne_top μ s]

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

Goal state before:
pp: G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed[inst✝⁷] (L n)
M : ∀ (n : ℕ), μ (L n) = ↑(n + 1) * μ K
N : Tendsto (fun n ↦ μ (L n)) atTop (𝓝 ∞)
⊢ μ univ = ∞

Tactic:
apply top_le_iff.1

Goal state after:
G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := ⋯
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed[inst✝⁷] (L n)
M : ∀ (n : ℕ), μ (L n) = ↑(n + 1) * μ K
N : Tendsto (fun n ↦ μ (L n)) atTop (𝓝 ∞)
⊢ ∞ ≤ μ univ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ μ.withDensity (s.indicator f) = (μ.restrict s).withDensity f

Tactic:
ext1 t ht

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ (μ.withDensity (s.indicator f)) t = ((μ.restrict s).withDensity f) t
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ (μ.withDensity f).restrict s = (μ.restrict s).withDensity f

Tactic:
ext1 t ht

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ ((μ.withDensity f).restrict s) t = ((μ.restrict s).withDensity f) t
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → ℝ≥0∞
⊢ (μ.withDensity f).restrict s = (μ.restrict s).withDensity f

Tactic:
ext1 t ht

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ ((μ.withDensity f).restrict s) t = ((μ.restrict s).withDensity f) t
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
A : (μ.withDensity f) t = 0
⊢ μ ({x | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) = 0

Tactic:
withDensity_apply f (measurableSet_toMeasurable _ s),

Goal state after:
case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
A : ∫⁻ (a : α) in toMeasurable (μ.withDensity f) s, f a ∂μ = 0
⊢ μ ({x | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) = 0
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.WeaklyRegular
x : ℝ≥0∞
hx : x ≠ ∞
⊢ (x • μ).WeaklyRegular

Tactic:
by
  have := OuterRegular.smul μ hx
  exact ⟨WeaklyRegular.innerRegular.smul x⟩

Goal state after:
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha : a ≠ 0
x : R
⊢ a * (x * x) + b * x + c = 0 ↔ discrim a b c = (2 * a * x + b) ^ 2

Tactic:
refine ⟨discrim_eq_sq_of_quadratic_eq_zero, fun h ↦ ?_⟩

Goal state after:
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha : a ≠ 0
x : R
h : discrim a b c = (2 * a * x + b) ^ 2
⊢ a * (x * x) + b * x + c = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ ∫⁻ (a : α), (f' * g) a ∂μ = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
apply lintegral_congr_ae
      filter_upwards [hf.ae_eq_mk]
      intro x hx
      simp only [f', hx, Pi.mul_apply]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
⊢ √x / x = 1 / √x

Tactic:
← div_sqrt,

Goal state after:
x : ℝ
⊢ x / √x / x = 1 / (x / √x)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∫⁻ (a : α), (f' * g) a ∂μ = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
apply lintegral_congr_ae
      filter_upwards [hf.ae_eq_mk]
      intro x hx
      simp only [f', hx, Pi.mul_apply]

Goal state after:
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ normSq (↑x - I * ↑√(1 - x ^ 2)) = 1

Tactic:
rw [← normSq_neg, neg_sub', sub_neg_eq_add]
  simpa using normSq_ofReal_add_I_mul_sqrt_one_sub (x := -x) (by simpa)

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

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
⊢ ∀ (x : α), ∃ i, x ∈ spanningSets μ i ∩ f ⁻¹' Iic ↑i

Tactic:
refine fun x ↦ ⟨max (spanningSetsIndex μ x) ⌈f x⌉₊, ?_, ?_⟩

Goal state after:
case refine_2.refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
x : α
⊢ x ∈ spanningSets μ (max (spanningSetsIndex μ x) ⌈f x⌉₊)

case refine_2.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
x : α
⊢ x ∈ f ⁻¹' Iic ↑(max (spanningSetsIndex μ x) ⌈f x⌉₊)
Module: Mathlib.Algebra.Star.MonoidHom

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝⁷ : Monoid A
inst✝⁶ : Star A
inst✝⁵ : Monoid B
inst✝⁴ : Star B
inst✝³ : Monoid C
inst✝² : Star C
inst✝¹ : Monoid D
inst✝ : Star D
f : B →⋆* C
g : A →⋆* B
a : A
⊢ (↑(f.comp g.toMonoidHom)).toFun (star a) = star ((↑(f.comp g.toMonoidHom)).toFun a)

Tactic:
by simp [map_star]

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

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝¹¹ : SeminormedAddCommGroup V
inst✝¹⁰ : SeminormedAddCommGroup V₁
inst✝⁹ : SeminormedAddCommGroup V₂
inst✝⁸ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst✝⁷ : MonoidWithZero R
inst✝⁶ : DistribMulAction R V₂
inst✝⁵ : PseudoMetricSpace R
inst✝⁴ : IsBoundedSMul R V₂
inst✝³ : MonoidWithZero R'
inst✝² : DistribMulAction R' V₂
inst✝¹ : PseudoMetricSpace R'
inst✝ : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this : dist (r • f x) (r • 0) ≤ dist r 0 * dist (f x) 0
⊢ ‖(r • ⇑f) x‖ ≤ dist r 0 * b * ‖x‖

Tactic:
smul_zero,

Goal state after:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝¹¹ : SeminormedAddCommGroup V
inst✝¹⁰ : SeminormedAddCommGroup V₁
inst✝⁹ : SeminormedAddCommGroup V₂
inst✝⁸ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst✝⁷ : MonoidWithZero R
inst✝⁶ : DistribMulAction R V₂
inst✝⁵ : PseudoMetricSpace R
inst✝⁴ : IsBoundedSMul R V₂
inst✝³ : MonoidWithZero R'
inst✝² : DistribMulAction R' V₂
inst✝¹ : PseudoMetricSpace R'
inst✝ : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this : dist (r • f x) 0 ≤ dist r 0 * dist (f x) 0
⊢ ‖(r • ⇑f) x‖ ≤ dist r 0 * b * ‖x‖
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
v₁ v₂ : V₁
⊢ ↑⟨φ (v₁ + v₂), ⋯⟩ = ↑(⟨φ v₁, ⋯⟩ + ⟨φ v₂, ⋯⟩)

Tactic:
simp only [map_add, AddSubgroup.coe_add]

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

Goal state before:
pp: case neg.refine_2
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
L : SummationFilter ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f L
hf' : ¬Summable (fun z ↦ e (f z)) L
H : 0 = e.symm y
⊢ 0 = y

Tactic:
simpa using congr_arg (fun z ↦ e z) H

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
f g : ℂ →ₐ[ℝ] A
h : f I = g I
⊢ f = g

Tactic:
ext ⟨x, y⟩
  simp only [mk_eq_add_mul_I, map_add, AlgHom.map_coe_real_complex, map_mul, h]

Goal state after: