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

Goal state before:
pp: β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
hfu : ∀ᶠ (n : ι) in cofinite, ∀ (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformly (fun t x ↦ ∑ n ∈ t, f n x) (fun x ↦ ∑' (n : ι), f n x) atTop

Tactic:
rw [← tendstoUniformlyOn_univ]

Goal state after:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
hfu : ∀ᶠ (n : ι) in cofinite, ∀ (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn (fun t x ↦ ∑ n ∈ t, f n x) (fun x ↦ ∑' (n : ι), f n x) atTop univ
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case mp.left
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ 0 ≤ t

pp: case mp.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ t ≤ 1 / a

pp: case mpr.left
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ 0 ≤ a * t

pp: case mpr.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ a * t ≤ 1

Tactic:
· exact nonneg_of_mul_nonneg_right h₁ ha

Goal state after:
case mp.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ t ≤ 1 / a

case mpr.left
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ 0 ≤ a * t

case mpr.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ a * t ≤ 1
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : X
y : Y
h : glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) = 0
⊢ False

Tactic:
linarith [le_glueDist_inl_inr Φ Ψ ε x y]

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

Goal state before:
pp: case mp.succ
α : Type u_2
x y : ℕ → α
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
h : res x (n + 1) = res y (n + 1)
m : ℕ
hm : m < n + 1
⊢ x m = y m

Tactic:
Nat.lt_succ_iff_lt_or_eq

Goal state after:
case mp.succ
α : Type u_2
x y : ℕ → α
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
h : res x (n + 1) = res y (n + 1)
m : ℕ
hm : m < n ∨ m = n
⊢ x m = y m
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mp.succ
α : Type u_2
x y : ℕ → α
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
h : res x (n + 1) = res y (n + 1)
m : ℕ
hm : m < n ∨ m = n
⊢ x m = y m

Tactic:
simp only [res_succ, cons.injEq] at h

Goal state after:
case mp.succ
α : Type u_2
x y : ℕ → α
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
hm : m < n ∨ m = n
h : x n = y n ∧ res x n = res y n
⊢ x m = y m
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ s ∈ 𝓤 (X ⊕ Y) ↔ ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s

Tactic:
by
  constructor
  · rintro ⟨hsX, hsY⟩
    rcases mem_uniformity_dist.1 hsX with ⟨εX, εX0, hX⟩
    rcases mem_uniformity_dist.1 hsY with ⟨εY, εY0, hY⟩
    refine ⟨min (min εX εY) 1, lt_min (lt_min εX0 εY0) zero_lt_one, ?_⟩
    rintro (a | a) (b | b) h
    · exact hX (lt_of_lt_of_le h (le_trans (min_le_left _ _) (min_le_left _ _)))
    · cases not_le_of_gt (lt_of_lt_of_le h (min_le_right _ _)) Sum.one_le_dist_inl_inr
    · cases not_le_of_gt (lt_of_lt_of_le h (min_le_right _ _)) Sum.one_le_dist_inr_inl
    · exact hY (lt_of_lt_of_le h (le_trans (min_le_left _ _) (min_le_right _ _)))
  · rintro ⟨ε, ε0, H⟩
    constructor <;> rw [Filter.mem_map, mem_uniformity_dist] <;> exact ⟨ε, ε0, fun _ _ h => H _ _ h⟩

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

Goal state before:
pp: case mp
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
⊢ IsOpen[Pi.topologicalSpace] s → ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s

Tactic:
intro hs

Goal state after:
case mp
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsOpen[Pi.topologicalSpace] s
⊢ ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
hs : IsClosed[Pi.topologicalSpace] ∅
hx : x ∉ ∅
⊢ ∃ n, Disjoint ∅ (cylinder x n)

Tactic:
exact ⟨0, by simp⟩

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

Goal state before:
pp: case neg
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬max x.fst y.fst = m + 1
this✝ : max x.fst y.fst ≤ m.succ
this : max x.fst y.fst ≤ m
xm : x.fst ≤ m
ym : y.fst ≤ m
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} ↦ f k) x.snd) (leRecOn hy (fun {k} ↦ f k) y.snd)

Tactic:
rw [leRecOn_succ xm, leRecOn_succ ym, (I m).dist_eq]

Goal state after:
case neg
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬max x.fst y.fst = m + 1
this✝ : max x.fst y.fst ≤ m.succ
this : max x.fst y.fst ≤ m
xm : x.fst ≤ m
ym : y.fst ≤ m
⊢ inductiveLimitDist f x y = dist (leRecOn xm (fun {k} ↦ f k) x.snd) (leRecOn ym (fun {k} ↦ f k) y.snd)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
n : ℕ
⊢ (eapprox f n).lintegral (Measure.map g μ) = (eapprox (f ∘ g) n).lintegral μ

Tactic:
convert! SimpleFunc.lintegral_map _ hg

Goal state after:
case e'_3
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
n : ℕ
⊢ eapprox (f ∘ g) n = (eapprox f n).comp g hg
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous[γtop, inst✝¹] g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ Continuous[γtop, inst✝] (f ∘ g)

Tactic:
apply hf.comp_continuous g_cont fun x => _

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous[γtop, inst✝¹] g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ ∀ (x : γ), g x ∈ s
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
⊢ ∃ s, μ = sum fun x ↦ μ (measurableAtom ↑x) • dirac ↑x

Tactic:
let measurableAtoms := measurableAtom '' (Set.univ : Set α)

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
⊢ ∃ s, μ = sum fun x ↦ μ (measurableAtom ↑x) • dirac ↑x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: case const.refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ∞
x : α
⊢ (piecewise t ht (const α c) (const α 0)) x ≤ (piecewise s hs (const α c) (const α 0)) x

Tactic:
refine indicator_le_indicator_of_subset ts (fun x => ?_) x
      exact zero_le

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

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
μ ν : Measure M
inst✝ : SFinite ν
s : ℝ≥0∞
⊢ (s • μ) ∗ₘ ν = s • μ ∗ₘ ν

Tactic:
unfold mconv
  rw [← Measure.map_smul, Measure.prod_smul_left]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(g₀ x) ≤ ↑(f x)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
⊢ ∫⁻ (x : α), ↑(g₀ x) ∂μ = ∫⁻ (a : α), (ofNNReal ∘ ⇑g₀) a ∂μ

Tactic:
simp only [Function.comp_apply]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.IsComplement' K
⊢ K.IsComplement' H

Tactic:
let ϕ : H × K ≃ K × H :=
    Equiv.mk (fun x => ⟨x.2⁻¹, x.1⁻¹⟩) (fun x => ⟨x.2⁻¹, x.1⁻¹⟩)
      (fun x => Prod.ext (inv_inv _) (inv_inv _)) fun x => Prod.ext (inv_inv _) (inv_inv _)

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.IsComplement' K
ϕ : ↥H × ↥K ≃ ↥K × ↥H :=
  { toFun := fun x ↦ (x.2⁻¹, x.1⁻¹), invFun := fun x ↦ (x.2⁻¹, x.1⁻¹), left_inv := ⋯, right_inv := ⋯ }
⊢ K.IsComplement' H
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
⊢ ∃ S, IsComplement S ↑H ∧ g ∈ S

Tactic:
refine ⟨Set.range (Function.update Quotient.out _ g), isComplement_range_left fun q ↦ ?_,
    QuotientGroup.mk g, Function.update_self (Quotient.mk'' g) g Quotient.out⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ ↑(update Quotient.out (Quotient.mk'' g) g q) = q
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
⊢ (hHT.equiv g₁).2 = (hHT.equiv g₂).2 → g₂ * g₁⁻¹ ∈ H

Tactic:
intro h
    rw [← hHT.equiv_fst_mul_equiv_snd g₂, ← hHT.equiv_fst_mul_equiv_snd g₁, ← h,
      mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← coe_inv, ← coe_mul]
    exact Subtype.property _

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
U : ℕ → Set α
hAU : ∀ (n : ℕ), U n ⊇ A n
hUo : ∀ (n : ℕ), IsOpen[inst✝¹] (U n)
hU : ∀ (n : ℕ), μ (U n) < μ (A n) + δ n
⊢ μ (⋃ n, U n) < r

Tactic:
calc
    μ (⋃ n, U n) ≤ ∑' n, μ (U n) := measure_iUnion_le _
    _ ≤ ∑' n, (μ (A n) + δ n) := ENNReal.tsum_le_tsum fun n => (hU n).le
    _ = ∑' n, μ (A n) + ∑' n, δ n := ENNReal.tsum_add
    _ = μ (⋃ n, A n) + ∑' n, δ n := (congr_arg₂ (· + ·) (measure_iUnion hAd hAm).symm rfl)
    _ < r := hδε

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
⊢ map Prod.swap (μ.prod ν) = ν.prod μ

Tactic:
have : sum (fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)))
       = sum (fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))) := by
    ext s hs
    rw [sum_apply _ hs, sum_apply _ hs]
    exact ((Equiv.prodComm ℕ ℕ).tsum_eq _).symm
  rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν, prod_sum, prod_sum,
    map_sum measurable_swap.aemeasurable, this]
  congr 1
  ext1 i
  refine (prod_eq ?_).symm
  intro s t hs ht
  simp_rw [map_apply measurable_swap (hs.prod ht), preimage_swap_prod, prod_prod, mul_comm]

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

Goal state before:
pp: M : Type uM
α : Type uα
β : Type uβ
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : MeasurableConstSMul M β
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
f : α → β
hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a
hf : Measurable f
m : M
S : Set β
hS : MeasurableSet S
⊢ μ ((fun x ↦ m • x) ⁻¹' f ⁻¹' S) = μ (f ⁻¹' S)

Tactic:
SMulInvariantMeasure.measure_preimage_smul m (hS.preimage hf)

Goal state after:
M : Type uM
α : Type uα
β : Type uβ
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : MeasurableConstSMul M β
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
f : α → β
hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a
hf : Measurable f
m : M
S : Set β
hS : MeasurableSet S
⊢ μ (f ⁻¹' S) = μ (f ⁻¹' S)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst✝¹]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst✝¹] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ μ s
hr : μ s - (ε + ε) < μ s
U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst✝¹] U
hUt : μ U < ∞
hμU : μ (U \ s) < ε
U' : Set α
hU'o : IsOpen[inst✝¹] U'
hμU' : μ U' < ε
hsU' : U \ U' ⊆ s
K : Set α
hKU : K ⊆ U
hKc : p K
hKr : μ U < μ K + ε
⊢ ∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ K

Tactic:
refine ⟨K \ U', fun x hx => hsU' ⟨hKU hx.1, hx.2⟩, hd hKc hU'o, ENNReal.sub_lt_of_lt_add hεs ?_⟩

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst✝¹]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst✝¹] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ μ s
hr : μ s - (ε + ε) < μ s
U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst✝¹] U
hUt : μ U < ∞
hμU : μ (U \ s) < ε
U' : Set α
hU'o : IsOpen[inst✝¹] U'
hμU' : μ U' < ε
hsU' : U \ U' ⊆ s
K : Set α
hKU : K ⊆ U
hKc : p K
hKr : μ U < μ K + ε
⊢ μ s < μ (K \ U') + (ε + ε)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace α
s : Set γ
f : γ → α
inst✝² : MeasurableSpace.CountablySeparated α
inst✝¹ : MeasurableSpace γ
inst✝ : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
τ : TopologicalSpace α
left✝¹ : SecondCountableTopology α
left✝ : T4Space α
right✝ : OpensMeasurableSpace α
t' : TopologicalSpace γ
t't : t' ≤ tγ
f_cont : Continuous[t', τ] f
t'_polish : PolishSpace γ
⊢ MeasurableSet s

Tactic:
← eq_borel_upgradeStandardBorel γ

Goal state after:
γ : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace α
s : Set γ
f : γ → α
inst✝² : MeasurableSpace.CountablySeparated α
inst✝¹ : MeasurableSpace γ
inst✝ : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
τ : TopologicalSpace α
left✝¹ : SecondCountableTopology α
left✝ : T4Space α
right✝ : OpensMeasurableSpace α
t' : TopologicalSpace γ
t't : t' ≤ tγ
f_cont : Continuous[t', τ] f
t'_polish : PolishSpace γ
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
μ : Measure G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : μ.Regular
s : Set G
hs : IsOpen[inst✝⁵] s
⊢ μ s = 0 ↔ s = ∅ ∨ μ = 0

Tactic:
rcases eq_zero_or_neZero μ with rfl | hμ
  · simp
  · simp only [or_false, hs.measure_eq_zero_iff μ, NeZero.ne μ]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ (μ.withDensity f) s

Tactic:
let t := toMeasurable (μ.withDensity f) s

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable (μ.withDensity f) s
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ (μ.withDensity f) s
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (∑' (n : ι), f n)) s = (sum fun n ↦ μ.withDensity (f n)) s

Tactic:
simp_rw [sum_apply _ hs, withDensity_apply _ hs]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (∑' (n : ι), f n) a ∂μ = ∑' (i : ι), ∫⁻ (a : α) in s, f i a ∂μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ (μ.withDensity f).trim hm = (μ.trim hm).withDensity f

Tactic:
refine @Measure.ext _ m _ _ (fun s hs ↦ ?_)
  rw [withDensity_apply _ hs, restrict_trim _ _ hs, lintegral_trim _ hf, trim_measurableSet_eq _ hs,
    withDensity_apply _ (hm s hs)]

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

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

Tactic:
intro hs

Goal state after:
case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
⊢ μ ({x | f x ≠ 0} ∩ s) = 0
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
⊢ μ ({x | f x ≠ 0} ∩ s) = 0

Tactic:
let t := toMeasurable (μ.withDensity f) 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
⊢ μ ({x | f x ≠ 0} ∩ s) = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

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

Tactic:
intro hs

Goal state after:
case mpr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : μ ({x | f x ≠ 0} ∩ s) = 0
⊢ (μ.withDensity f) s = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
⊢ AEMeasurable g (μ.withDensity fun x ↦ ↑(f x)) → AEMeasurable (fun x ↦ ↑(f x) * g x) μ

Tactic:
rintro ⟨g', g'meas, hg'⟩

Goal state after:
case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
⊢ AEMeasurable (fun x ↦ ↑(f x) * g x) μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case mpr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
⊢ AEMeasurable (fun x ↦ ↑(f x) * g x) μ → AEMeasurable g (μ.withDensity fun x ↦ ↑(f x))

Tactic:
rintro ⟨g', g'meas, hg'⟩

Goal state after:
case mpr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun x ↦ ↑(f x) * g x) =ᵐ[μ] g'
⊢ AEMeasurable g (μ.withDensity fun x ↦ ↑(f x))
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
h : ∃! x, discrim a b c = (2 * a * x + b) ^ 2
⊢ discrim a b c = 0

Tactic:
generalize discrim a b c = d at h

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
d : K
h : ∃! x, d = (2 * a * x + b) ^ 2
⊢ d = 0
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : HasFiniteIntegral f μ
⊢ IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal (f x))

Tactic:
by
  refine isFiniteMeasure_withDensity ((lintegral_mono fun x => ?_).trans_lt hfi).ne
  exact Real.ofReal_le_enorm (f x)

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
⊢ ∀ᵐ (a : α) ∂μ, i a ≤ (f * fun i_1 ↦ (f i_1)⁻¹ * i i_1) a

Tactic:
filter_upwards [hf]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
⊢ ∀ (a : α), f a < ∞ → i a ≤ (f * fun i_1 ↦ (f i_1)⁻¹ * i i_1) a
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ √(x ^ 2 + y ^ 2) ≤ √2 * m

Tactic:
calc
    √(x ^ 2 + y ^ 2) ≤ √(m ^ 2 + m ^ 2) := by
      gcongr √(?_ + ?_) <;> rw [sq_le_sq, abs_of_nonneg hm₀]
      exacts [le_max_left _ _, le_max_right _ _]
    _ = √2 * m := by
      rw [← two_mul, Real.sqrt_mul, Real.sqrt_sq] <;> positivity

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

Goal state before:
pp: E : Type u_2
inst✝¹ : NonUnitalNormedRing E
inst✝ : StarRing E
h : ∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖x * x⋆‖
x : E
⊢ ‖x⋆‖ ≤ ‖x‖

Tactic:
by
        obtain (hx | hx) := eq_zero_or_norm_pos x⋆
        · simp [hx]
        · refine le_of_mul_le_mul_right ?_ hx
          simpa [sq, mul_comm ‖x⋆‖] using h x⋆ |>.trans <| norm_mul_le _ _

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

Goal state before:
pp: ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : ↑a = ∑ i ∈ s, f i
hb : b = ∑ i ∈ s, ‖f i‖
⊢ ‖↑a‖ ≤ b

Tactic:
ha,

Goal state after:
ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : ↑a = ∑ i ∈ s, f i
hb : b = ∑ i ∈ s, ‖f i‖
⊢ ‖∑ i ∈ s, f i‖ ≤ b
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: case inl
𝕜 : Type u_2
inst✝ : RCLike 𝕜
a : 𝕜
h : RCLike.I = 0
⊢ ‖↑(RCLike.re a) + ↑(RCLike.im a) * I‖ = ‖a‖

Tactic:
rw [← RCLike.re_add_im a, RCLike.im_eq_zero h]

Goal state after:
case inl
𝕜 : Type u_2
inst✝ : RCLike 𝕜
a : 𝕜
h : RCLike.I = 0
⊢ ‖↑(RCLike.re (↑(RCLike.re a) + ↑0 * RCLike.I)) + ↑(RCLike.im (↑(RCLike.re a) + ↑0 * RCLike.I)) * I‖ =
    ‖↑(RCLike.re a) + ↑0 * RCLike.I‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∃ c, IsBigOWith c l f fun x ↦ ‖g' x‖) ↔ ∃ c, IsBigOWith c l f g'

Tactic:
exact exists_congr fun _ => isBigOWith_norm_right

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case cons
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s✝ : Finset ι
i : ι
s : Finset ι
is : i ∉ s
IH : (∀ i ∈ s, IsBigOWith (C i) l (A i) g) → IsBigOWith (∑ i ∈ s, C i) l (∑ i ∈ s, A i) g
h : IsBigOWith (C i) l (A i) g ∧ ∀ x ∈ s, IsBigOWith (C x) l (A x) g
⊢ IsBigOWith (C i + ∑ i ∈ s, C i) l (A i + ∑ i ∈ s, A i) g

Tactic:
exact h.1.add (IH h.2)

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s✝ : Finset ι
B : ι → α → ℝ
i : ι
s : Finset ι
his : i ∉ s
h : (∀ i ∈ s, A i =o[l] B i) → (fun H ↦ ∑ i ∈ s, A i H) =o[l] fun H ↦ ∑ i ∈ s, ‖B i H‖
hAB : ∀ i_1 ∈ Finset.cons i s his, A i_1 =o[l] B i_1
j : ι
hj : j ∈ s
⊢ j ∈ Finset.cons i s his

Tactic:
simp [hj]

Goal state after: