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

Goal state before:
pp: G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul G
H : Subgroup G
inst✝¹ : H.FiniteIndex
hH : MeasurableSet ↑H
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s ↑H
hs' : Finite ↑s
⊢ ↑H.index * μ ↑H = ∑' (a : ↑s), μ (↑a • ↑H)

Tactic:
simp [measure_smul, hs.encard_left]

Goal state after:
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
⊢ μ (⋃ n, s n) + ∑' (n : ℕ), δ n ≤ μ (⋃ n, s n) + ε

Tactic:
hδε,

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
⊢ μ (⋃ n, s n) + ε / 2 ≤ μ (⋃ n, s n) + ε
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
h : ¬Countable α
this : UpgradedStandardBorel α := upgradeStandardBorel α
⊢ ¬univ.Countable

Tactic:
by rwa [← countable_coe_iff, (Equiv.Set.univ _).countable_iff]

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

Goal state after:
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 fun x ↦ ∫⁻ (y : G), f y * g (y⁻¹ * x) ∂μ
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

Goal state after:
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 (fun x ↦ ∫⁻ (y : G), f y * g (y⁻¹ * x) ∂μ) μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = r • ∫⁻ (a : α) in s, f a ∂μ

Tactic:
smul_eq_mul,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = r * ∫⁻ (a : α) in s, f a ∂μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = r • ∫⁻ (a : α) in s, f a ∂μ

Tactic:
smul_eq_mul,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = r * ∫⁻ (a : α) in s, f a ∂μ
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁴] K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst✝⁴] U
hμU : μ U < μ K + ε / 2
⊢ μ (U ∆ s) < ε / 2 + ε / 2

Tactic:
measure_symmDiff_eq hUo.nullMeasurableSet hs.nullMeasurableSet

Goal state after:
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁴] K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst✝⁴] U
hμU : μ U < μ K + ε / 2
⊢ μ (U \ s) + μ (s \ U) < ε / 2 + ε / 2
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (μ.withDensity f) univ = 0 ↔ f =ᵐ[μ] 0

Tactic:
withDensity_apply _ .univ,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (a : α) in univ, f a ∂μ = 0 ↔ f =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : ¬c = ∞
s : Set α
⊢ MeasurableSet s ∧ (c • μ) s ≠ ∞ ↔ MeasurableSet s ∧ μ s ≠ ∞

Tactic:
have : (c • μ) s ≠ ∞ ↔ μ s ≠ ∞ := by simp [ENNReal.mul_eq_top, hc, h'c]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : ¬c = ∞
s : Set α
this : (c • μ) s ≠ ∞ ↔ μ s ≠ ∞
⊢ MeasurableSet s ∧ (c • μ) s ≠ ∞ ↔ MeasurableSet s ∧ μ s ≠ ∞
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
t : Set G
⊢ μ' t = (μ' s / ν' s) • ν' t

Tactic:
smul_eq_mul,

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
t : Set G
⊢ μ' t = μ' s / ν' s * ν' t
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F' n a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F' n a) atTop (𝓝 (f' a))
⊢ ∀ᵐ (a : α) ∂μ, ‖f' a‖ₑ ≤ bound' a

Tactic:
rw [← ae_all_iff] at h_bound

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F' n a) atTop (𝓝 (f' a))
⊢ ∀ᵐ (a : α) ∂μ, ‖f' a‖ₑ ≤ bound' a
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
a : α
h : Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
⊢ Tendsto (fun n ↦ ‖F n a - f a‖) atTop (𝓝 0)

Tactic:
← tendsto_iff_norm_sub_tendsto_zero

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
a : α
h : Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
⊢ Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ∞
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ ∫⁻ (a : α), b a ∂μ = 2 * ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ

Tactic:
by
          rw [lintegral_const_mul']
          finiteness

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

Goal state before:
pp: z : ℂ
h : z.re = 0
⊢ z.re ^ 2 - z.im ^ 2 ≤ 0 ∧ (z.re = 0 ∨ z.im = 0)

Tactic:
simpa [h] using sq_nonneg z.im

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

Goal state before:
pp: z : ℂ
⊢ z⁻¹.re = z.re / normSq z

Tactic:
simp [inv_def, division_def, ofReal]

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

Goal state before:
pp: z : ℂ
⊢ z⁻¹.im = -z.im / normSq z

Tactic:
simp [inv_def, division_def, ofReal]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : AddCommMonoid α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Module ℚ≥0 α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, f i ≤ 0
⊢ 𝔼 i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0

Tactic:
by
  simp +contextual [expect, sum_eq_zero_iff_of_nonpos hf]

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₂
z : ℤ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖z • f v‖ ≤ ‖z‖ • b * ‖v‖

Tactic:
smul_eq_mul,

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₂
z : ℤ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖z • f v‖ ≤ ‖z‖ * b * ‖v‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ re (↑r * z) = r * re z

Tactic:
by
  simp only [mul_re, ofReal_im, zero_mul, ofReal_re, sub_zero]

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

Goal state before:
pp: x : ℂ
hx : IsSelfAdjoint x
⊢ 0 ≤ RCLike.re x ↔ 0 ≤ x

Tactic:
exact RCLike.re_nonneg_of_nonneg hx

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z w : K
⊢ normSq (z + w) = normSq z + normSq w + 2 * re (z * (starRingEnd K) w)

Tactic:
simp only [normSq_apply, map_add, rclike_simps]
  ring

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

Goal state before:
pp: case refine_2
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : IsScalarTower ℂ A A
inst✝ : StarModule ℂ A
x : A
x✝ : IsStarNormal x ∧ ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1
hx : IsStarNormal x
h : ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1
⊢ star x * x = 1 ∧ x * star x = 1

Tactic:
· simp [← hx.star_comm_self.eq, star_mul_self_eq_realPart_sq_add_imaginaryPart_sq, ← sq, h]

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : ℝ
⊢ (AddMonoidHom.id ℝ) ((starRingEnd ℝ) z) = (AddMonoidHom.id ℝ) z

Tactic:
simp only [starRingEnd_apply, star_id_of_comm]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
a✝ : α
e₁ : f₁ a✝ = f₂ a✝
⊢ g₁ a✝ = g₂ a✝ → (‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖ ↔ ‖f₂ a✝‖ ≤ c₁ * ‖g₂ a✝‖)

Tactic:
e₂

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
a✝ : α
e₁ : f₁ a✝ = f₂ a✝
e₂ : g₁ a✝ = g₂ a✝
⊢ ‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖ ↔ ‖f₂ a✝‖ ≤ c₁ * ‖g₂ a✝‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
a✝ : α
e₁ : f₁ a✝ = f₂ a✝
e₂ : g₁ a✝ = g₂ a✝
⊢ ‖f₂ a✝‖ ≤ c₁ * ‖g₁ a✝‖ ↔ ‖f₂ a✝‖ ≤ c₁ * ‖g₂ a✝‖

Tactic:
e₂

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
a✝ : α
e₁ : f₁ a✝ = f₂ a✝
e₂ : g₁ a✝ = g₂ a✝
⊢ ‖f₂ a✝‖ ≤ c₁ * ‖g₂ a✝‖ ↔ ‖f₂ a✝‖ ≤ c₁ * ‖g₂ a✝‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (fun x ↦ ‖f' x‖) =O[l] g ↔ f' =O[l] g

Tactic:
by
  simp only [IsBigO_def]
  exact exists_congr fun _ => isBigOWith_norm_left

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

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
c : ℝ
t₁ : Set α
ht₁ : t₁ ∈ l
t₂ : Set β
ht₂ : t₂ ∈ l'
ht : t₁ ×ˢ t₂ ⊆ {x | ‖f x‖ ≤ c * ‖g x‖}
⊢ {b | ∃ c, {x | ‖f (x, b)‖ ≤ c * ‖g (x, b)‖} ∈ l} ∈ l'

Tactic:
exact mem_of_superset ht₂ fun _ hb ↦ ⟨c, mem_of_superset ht₁ fun _ ha ↦ ht ⟨ha, hb⟩⟩

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

Goal state before:
pp: case mp
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
h : (fun _x ↦ c) =O[l] f'
⊢ ∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖

Tactic:
rcases h.exists_pos with ⟨C, hC₀, hC⟩

Goal state after:
case mp
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
h : (fun _x ↦ c) =O[l] f'
C : ℝ
hC₀ : C > 0
hC : IsBigOWith C l (fun _x ↦ c) f'
⊢ ∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x y : ℝ
h : x < y
⊢ rexp x < rexp (y - x + x)

Tactic:
Real.exp_add

Goal state after:
x y : ℝ
h : x < y
⊢ rexp x < rexp (y - x) * rexp x
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : E'' → F''
x₀ : E''
n : ℕ
h : f =O[𝓝[univ] x₀] fun x ↦ ‖x - x₀‖ ^ n
hn : n ≠ 0
⊢ f x₀ = 0

Tactic:
exact h.eq_zero_of_norm_pow_within (mem_univ _) hn

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

Goal state before:
pp: x : ℂ
⊢ (starRingEnd ℂ) (cosh (-(x * I))) = (starRingEnd ℂ) (cosh (x * I))

Tactic:
cosh_neg

Goal state after:
x : ℂ
⊢ (starRingEnd ℂ) (cosh (x * I)) = (starRingEnd ℂ) (cosh (x * I))
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (starRingEnd ℂ) (cos ↑x) = cos ↑x

Tactic:
rw [← cos_conj, conj_ofReal]

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

Goal state before:
pp: x : ℂ
⊢ (starRingEnd ℂ) (cos x / sin x) = (starRingEnd ℂ) x.cot

Tactic:
cot

Goal state after:
x : ℂ
⊢ (starRingEnd ℂ) (cos x / sin x) = (starRingEnd ℂ) (cos x / sin x)
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2

Tactic:
exact tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm' hf h'f hg h'g

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: n : ℕ
this : (fun x ↦ Complex.exp ↑x - ∑ i ∈ Finset.range n, ↑x ^ i / ↑i !) =O[𝓝 0] fun x ↦ ↑x ^ n
⊢ (fun x ↦ rexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) =O[𝓝 0] fun x ↦ x ^ n

Tactic:
norm_cast at this

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
har1 : |r| < 1
m : ℕ
hmn : n.succ ≤ m
hr : 0 < r
k : ℕ
hk : m - n.succ = k
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m

Tactic:
replace hk : m = k + n.succ := (tsub_eq_iff_eq_add_of_le hmn).1 hk

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
har1 : |r| < 1
m : ℕ
hmn : n.succ ≤ m
hr : 0 < r
k : ℕ
hk : m = k + n.succ
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: n : ℕ
C : ℝ
hC₁ : 1 ≤ C
⊢ ∃ ia, True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C

Tactic:
have hC₀ : 0 < C := zero_lt_one.trans_le hC₁

Goal state after:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
⊢ ∃ ia, True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 2) = 0

Tactic:
Real.pi,

Goal state after:
⊢ cos (2 * Classical.choose exists_cos_eq_zero / 2) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ 1 ≤ π / 2

Tactic:
Real.pi,

Goal state after:
⊢ 1 ≤ 2 * Classical.choose exists_cos_eq_zero / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ π / 2 ≤ 2

Tactic:
Real.pi,

Goal state after:
⊢ 2 * Classical.choose exists_cos_eq_zero / 2 ≤ 2
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ (cthickening δ s)⁻¹ = cthickening δ s⁻¹

Tactic:
simp_rw [cthickening, ← infEDist_inv]
  rfl

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ ball (x • 1) δ = ball x δ

Tactic:
smul_eq_mul,

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ ball (x * 1) δ = ball x δ
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
⊢ ∃ x, 0 < ‖↑x‖

Tactic:
refine (Set.nonempty_compl.2 h).imp fun x hx ↦ ?_

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
x : M
hx : x ∈ (↑S.topologicalClosure)ᶜ
⊢ 0 < ‖↑x‖
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
⊢ (fun n ↦ ↑n ^ k) =o[atTop] fun n ↦ r ^ n

Tactic:
have : Tendsto (fun x : ℝ ↦ x ^ k) (𝓝[>] 1) (𝓝 1) :=
    ((continuous_id.pow k).tendsto' (1 : ℝ) 1 (one_pow _)).mono_left inf_le_left

Goal state after:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
⊢ (fun n ↦ ↑n ^ k) =o[atTop] fun n ↦ r ^ n
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this✝ : Function.Surjective fun x ↦ c • x
this : ↑‖c‖₊ ≠ 0
⊢ ⨅ y ∈ s, ↑‖c‖₊ • edist x y = ↑‖c‖₊ • ⨅ y ∈ s, edist x y

Tactic:
smul_eq_mul,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this✝ : Function.Surjective fun x ↦ c • x
this : ↑‖c‖₊ ≠ 0
⊢ ⨅ y ∈ s, ↑‖c‖₊ * edist x y = ↑‖c‖₊ * ⨅ y ∈ s, edist x y
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_2
inst✝¹ : SeminormedRing R
inst✝ : NormMulClass R
x : R
⊢ Tendsto (fun n ↦ x ^ n) atTop (𝓝 0) ↔ ‖x‖ < 1

Tactic:
refine ⟨?_, tendsto_pow_atTop_nhds_zero_of_norm_lt_one⟩
  rw [← abs_of_nonneg (norm_nonneg _), ← tendsto_pow_atTop_nhds_zero_iff,
    tendsto_zero_iff_norm_tendsto_zero]
  apply Tendsto.congr'
  filter_upwards [eventually_ge_atTop 1] with n hn
  induction n, hn using Nat.le_induction with
  | base => simp
  | succ n hn IH => simp [pow_succ, IH]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
⊢ ∃ y, dist x y ≤ δ ∧ dist y z ≤ ε

Tactic:
refine (exists_dist_eq x z (div_nonneg hε <| add_nonneg hε hδ)
    (div_nonneg hδ <| add_nonneg hε hδ) <| by
      rw [← add_div, div_self hεδ.ne']).imp
    fun y hy => ?_

Goal state after:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x y ≤ δ ∧ dist y z ≤ ε
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ Summable fun i ↦ ‖ξ ^ i‖

Tactic:
· simp [norm_pow, summable_geometric_of_lt_one (norm_nonneg _) h]

Goal state after: