mathlib-initiative/mathlib-tactics huggingface dataset:
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:
Measure.smul_apply,

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.Measure.WithDensity

Goal state before:
pp: case indicator
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
c : ℝ≥0∞
⊢ ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∫⁻ (a : α), s.indicator (fun x ↦ c) a ∂μ.withDensity f = ∫⁻ (a : α), (f * s.indicator fun x ↦ c) a ∂μ

Tactic:
s

Goal state after:
case indicator
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
c : ℝ≥0∞
s : Set α
⊢ MeasurableSet s →
    ∫⁻ (a : α), s.indicator (fun x ↦ c) a ∂μ.withDensity f = ∫⁻ (a : α), (f * s.indicator fun x ↦ c) a ∂μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case indicator
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s →
      ∫⁻ (a : α), s.indicator (fun x ↦ c) a ∂μ.withDensity f = ∫⁻ (a : α), (f * s.indicator fun x ↦ c) a ∂μ

pp: case add
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 g : α → ℝ≥0∞⦄,
    Disjoint (Function.support f_1) (Function.support g) →
      Measurable f_1 →
        Measurable g →
          ∫⁻ (a : α), f_1 a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1) a ∂μ →
            ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
              ∫⁻ (a : α), (f_1 + g) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (f_1 + g)) a ∂μ

pp: case iSup
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), ∫⁻ (a : α), f_1 n a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1 n) a ∂μ) →
          ∫⁻ (a : α), (fun x ↦ ⨆ n, f_1 n x) a ∂μ.withDensity f = ∫⁻ (a : α), (f * fun x ↦ ⨆ n, f_1 n x) a ∂μ

Tactic:
· intro c s h_ms
    simp [*, mul_comm _ c, ← indicator_mul_right]

Goal state after:
case add
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 g : α → ℝ≥0∞⦄,
    Disjoint (Function.support f_1) (Function.support g) →
      Measurable f_1 →
        Measurable g →
          ∫⁻ (a : α), f_1 a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1) a ∂μ →
            ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
              ∫⁻ (a : α), (f_1 + g) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (f_1 + g)) a ∂μ

case iSup
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), ∫⁻ (a : α), f_1 n a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1 n) a ∂μ) →
          ∫⁻ (a : α), (fun x ↦ ⨆ n, f_1 n x) a ∂μ.withDensity f = ∫⁻ (a : α), (f * fun x ↦ ⨆ n, f_1 n x) a ∂μ
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
⊢ ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖

Tactic:
filter_upwards [hnonneg, h] with a hn ha

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
a : α
hn : 0 ≤ f a
ha : f a ≤ g a
⊢ ‖f a‖ ≤ ‖g a‖
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
⊢ √x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2

Tactic:
rw [← and_iff_right_of_imp fun h => (sqrt_nonneg x).trans h, and_congr_right_iff]
  exact sqrt_le_left

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

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ √(x / y) = √x / √y

Tactic:
rw [division_def, sqrt_mul' x (inv_nonneg.2 hy), sqrt_inv, division_def]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝² : SFinite ν
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
s : Set (α × β)
hs : MeasurableSet s
A : ∀ (s : Set β), c • ν s = c • 1 * ν s
⊢ ∫⁻ (x : α), (c • ν) (Prod.mk x ⁻¹' s) ∂μ = (c • μ.prod ν) s

Tactic:
Measure.smul_apply,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝² : SFinite ν
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
s : Set (α × β)
hs : MeasurableSet s
A : ∀ (s : Set β), c • ν s = c • 1 * ν s
⊢ ∫⁻ (x : α), c • ν (Prod.mk x ⁻¹' s) ∂μ = c • (μ.prod ν) s
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_5
V₂ : Type u_6
inst✝¹ : NormedAddCommGroup V₁
inst✝ : NormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
hn : ‖f‖ = 0
x : V₁
⊢ ‖f‖ * ‖x‖ = 0

Tactic:
by rw [hn, zero_mul]

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
a b : Rˣ
⊢ ↑a * ↑b⁻¹ ∈ unitary R ↔ star a * a = star b * b

Tactic:
simp [← mul_inv_mem_iff, Units.unitary_eq]

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

Goal state before:
pp: E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
this : 0 < ‖1‖
⊢ ‖1‖ = 1

Tactic:
← mul_left_inj' this.ne',

Goal state after:
E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
this : 0 < ‖1‖
⊢ ‖1‖ * ‖1‖ = 1 * ‖1‖
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : E
⊢ restrictScalars ℝ (toSpanSingleton ℂ x) = reCLM.smulRight x + I • imCLM.smulRight x

Tactic:
by
  ext ⟨a, b⟩
  simp [map_add, mk_eq_add_mul_I, mul_smul, smul_comm I b x]

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

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ℑ (I • a) = ℜ a

Tactic:
by
  ext
  simp [realPart_apply_coe, imaginaryPart_apply_coe, smul_comm I (2⁻¹ : ℝ), smul_smul I]

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : K
r : ℝ
a : K
⊢ star (r • a) = star r • star a

Tactic:
by
    apply RCLike.ext <;> simp [RCLike.smul_re, RCLike.smul_im]

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

Goal state before:
pp: case mp.zero
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
x : α
h₀' : ‖f x‖ ≤ 1 * ‖g x‖
⊢ ↑0 * ‖f x‖ ≤ ‖g x‖

Tactic:
Nat.cast_zero,

Goal state after:
case mp.zero
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
x : α
h₀' : ‖f x‖ ≤ 1 * ‖g x‖
⊢ 0 * ‖f x‖ ≤ ‖g x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hgk : IsBigOWith c l g k
hc : 0 < c
hfg : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g
c' : ℝ
⊢ 0 < c' → IsBigOWith c' l f k

Tactic:
c'pos

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hgk : IsBigOWith c l g k
hc : 0 < c
hfg : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g
c' : ℝ
c'pos : 0 < c'
⊢ IsBigOWith c' l f k
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hc : 0 < c
hgk : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g k
c' : ℝ
⊢ 0 < c' → IsBigOWith c' l f k

Tactic:
c'pos

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hc : 0 < c
hgk : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g k
c' : ℝ
c'pos : 0 < c'
⊢ IsBigOWith c' l f k
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n : ℕ
pn : NormNum.IsNat n 0
⊢ List.range ↑0 = []

Tactic:
Nat.cast_zero,

Goal state after:
n : ℕ
pn : NormNum.IsNat n 0
⊢ List.range 0 = []
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n : ℕ
pn : NormNum.IsNat n 0
⊢ Multiset.range ↑0 = 0

Tactic:
Nat.cast_zero,

Goal state after:
n : ℕ
pn : NormNum.IsNat n 0
⊢ Multiset.range 0 = 0
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n : ℕ
pn : NormNum.IsNat n 0
⊢ Finset.range ↑0 = ∅

Tactic:
Nat.cast_zero,

Goal state after:
n : ℕ
pn : NormNum.IsNat n 0
⊢ Finset.range 0 = ∅
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
⊢ IsBigOWith c l (fun x ↦ (g x)⁻¹) fun x ↦ (f x)⁻¹

Tactic:
refine IsBigOWith.of_bound (h.bound.mp (h₀.mono fun x h₀ hle => ?_))

Goal state after:
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀✝ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
x : α
h₀ : f x = 0 → g x = 0
hle : ‖f x‖ ≤ c * ‖g x‖
⊢ ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
⊢ cexp (↑0 * x) = cexp x ^ 0

Tactic:
Nat.cast_zero,

Goal state after:
x : ℂ
⊢ cexp (0 * x) = cexp x ^ 0
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case h
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
⊢ (∀ᶠ (x : α) in l, ‖(fun x ↦ u x / v x) x‖ ≤ c) ∧ u =ᶠ[l] (fun x ↦ u x / v x) * v

Tactic:
refine ⟨Eventually.mono h.bound fun y hy => ?_, h.eventually_mul_div_cancel.symm⟩

Goal state after:
case h
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
y : α
hy : ‖u y‖ ≤ c * ‖v y‖
⊢ ‖(fun x ↦ u x / v x) y‖ ≤ c
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case hba
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
x : ℕ
a✝ : x ∈ range (j - n)
⊢ ↑n.factorial * ↑n.succ ^ x ≤ ↑(x + n).factorial

Tactic:
← Nat.cast_pow,

Goal state after:
case hba
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
x : ℕ
a✝ : x ∈ range (j - n)
⊢ ↑n.factorial * ↑(n.succ ^ x) ≤ ↑(x + n).factorial
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ ‖f₂ x‖ ≤ ‖f₂ x - f₁ x‖ / (1 - c)

Tactic:
le_div_iff₀,

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ ‖f₂ x‖ * (1 - c) ≤ ‖f₂ x - f₁ x‖

α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ 0 < 1 - c
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''
g : ℕ → F''
h : ∀ (x : ℕ), g x = 0 → f x = 0
⊢ f =O[atTop] g ↔ ∃ C, ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖

Tactic:
by
  rw [← Nat.cofinite_eq_atTop, isBigO_cofinite_iff h]

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

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
m : ℕ
hm : n ≤ m ∧ m < j
⊢ x ^ m / ↑m.factorial = x ^ (n + (m - n)) / ↑m.factorial

Tactic:
add_tsub_cancel_of_le hm.1

Goal state after:
x : ℂ
n j : ℕ
hj : j ≥ n
m : ℕ
hm : n ≤ m ∧ m < j
⊢ x ^ m / ↑m.factorial = x ^ m / ↑m.factorial
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
hx : 0 < cos x
⊢ (√(1 + tan x ^ 2))⁻¹ = √(cos x ^ 2)

Tactic:
← sqrt_inv,

Goal state after:
x : ℝ
hx : 0 < cos x
⊢ √(1 + tan x ^ 2)⁻¹ = √(cos x ^ 2)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : 0 < x
hx' : x < 2
⊢ rexp x < (2 + x) / (2 - x)

Tactic:
calc
  _ = exp (x / 2) ^ 2 := by grind [Real.exp_nat_mul (x / 2) 2]
  _ ≤ _ := by
    grw [Real.exp_bound' (x := x / 2) (by grind) (by grind) (n := 3) (by simp)]
    apply Real.exp_nonneg
  _ < (2 + x) / (2 - x) := by
    rw [lt_div_iff₀ (by linarith), ← sub_pos]
    simp only [Finset.sum_range_succ]
    ring_nf
    positivity

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x✝ : α
hx✝ : x✝ ∈ s
hs : IsCompact ((fun a ↦ ‖a‖) '' f '' s)
h_sInf : IsGLB ((fun a ↦ ‖a‖) '' f '' s) (sInf ((fun a ↦ ‖a‖) '' f '' s))
w✝ : E
hnormCx : (fun a ↦ ‖a‖) w✝ = sInf ((fun a ↦ ‖a‖) '' f '' s)
x : α
hx : x ∈ s
hCx : f x = w✝
⊢ 0 < sInf (Norm.norm '' f '' s)

Tactic:
rw [← hnormCx, ← hCx]

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x✝ : α
hx✝ : x✝ ∈ s
hs : IsCompact ((fun a ↦ ‖a‖) '' f '' s)
h_sInf : IsGLB ((fun a ↦ ‖a‖) '' f '' s) (sInf ((fun a ↦ ‖a‖) '' f '' s))
w✝ : E
hnormCx : (fun a ↦ ‖a‖) w✝ = sInf ((fun a ↦ ‖a‖) '' f '' s)
x : α
hx : x ∈ s
hCx : f x = w✝
⊢ 0 < (fun a ↦ ‖a‖) (f x)
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
⊢ IsCauSeq abs fun m ↦ (1 - abv x ^ m) / (1 - abv x)

Tactic:
have : 0 < 1 - abv x := sub_pos.2 hx1

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
⊢ IsCauSeq abs fun m ↦ (1 - abv x ^ m) / (1 - abv x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ 0 < x + π / 2

Tactic:
by linarith [hx.1]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ 0 ≤ x + π / 2

Tactic:
by linarith [hx.1]

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

Goal state before:
pp: R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
⊢ ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖r' ^ n‖ * ‖1‖

Tactic:
refine n.norm_cast_le.trans (mul_le_mul_of_nonneg_right ?_ (norm_nonneg _))

Goal state after:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
⊢ ↑n ≤ (r' - 1)⁻¹ * ‖r' ^ n‖
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
⊢ r • ball 0 1 = ball 0 r

Tactic:
rw [smul_unitBall hr.ne', Real.norm_of_nonneg hr.le]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ (4 • X ^ 2 - 2 • X - C 1).IsRoot (cos (π / 5))

Tactic:
simpa using quadratic_root_cos_pi_div_five

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

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n ↦ ↑(u n)) =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖‖↑(u n) * r ^ n‖‖ ≤ ‖1‖ * ‖↑(u n) * ‖r‖ ^ n‖

Tactic:
simp only [norm_mul, Real.norm_eq_abs, abs_cast, norm_pow, abs_norm]

Goal state after:
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n ↦ ↑(u n)) =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖↑(u n) * r ^ n‖ ≤ ‖1‖ * (↑(u n) * ‖r‖ ^ n)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
s : Set E
x : E
⊢ x ∈ cthickening (ε + δ) s → x ∈ cthickening ε (thickening δ s)

Tactic:
simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ.le, infEDist_thickening hδ]
    exact tsub_le_iff_right.2

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

Goal state before:
pp: 𝕜 : Type u_5
inst✝ : NormedDivisionRing 𝕜
r : 𝕜
hr : ‖r‖ < 1
⊢ HasSum (fun n ↦ ↑n * r ^ n) (r / (1 - r) ^ 2)

Tactic:
by
  convert! hasSum_coe_mul_geometric_of_norm_lt_one' hr using 1
  simp [div_eq_mul_inv]

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
⊢ IsPathConnected F ↔ ∃ x ∈ F, pathComponentIn F x = F

Tactic:
by
  constructor <;> rintro ⟨x, x_in, h⟩ <;> use x, x_in
  · ext y
    exact ⟨fun hy => hy.mem.2, @h _⟩
  · intro y y_in
    rwa [← h] at y_in

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

Goal state before:
pp: α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
r : ℝ
hr₀ : 1 < r
hr₁ : r < l
a✝¹ : ℕ
a✝ : r ≤ ‖f (a✝¹ + 1)‖ / ‖f a✝¹‖
h₁ : ‖f a✝¹‖ ≠ 0
⊢ r * ‖f a✝¹‖ ≤ ‖f (a✝¹ + 1)‖

Tactic:
← le_div_iff₀ (lt_of_le_of_ne (norm_nonneg _) h₁.symm)

Goal state after:
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
r : ℝ
hr₀ : 1 < r
hr₁ : r < l
a✝¹ : ℕ
a✝ : r ≤ ‖f (a✝¹ + 1)‖ / ‖f a✝¹‖
h₁ : ‖f a✝¹‖ ≠ 0
⊢ r ≤ ‖f (a✝¹ + 1)‖ / ‖f a✝¹‖
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
⊢ (γ₁.trans γ₂).extend t = γ₂.extend (2 * t - 1)

Tactic:
conv_lhs => rw [← sub_sub_cancel 1 t]
  rw [← extend_symm_apply, trans_symm, extend_trans_of_le_half _ _ (by linarith), extend_symm_apply]
  congr 1
  linarith

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
⊢ ∃ γ, ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ

Tactic:
have : IsPathConnected (univ : Set X) := pathConnectedSpace_iff_univ.mp (by infer_instance)
  rcases this.exists_path_through_family p fun _i => True.intro with ⟨γ, -, h⟩
  exact ⟨γ, h⟩

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

Goal state before:
pp: case inl
E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
upper : ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Even (2 * n)
⊢ |∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i| ≤ f (2 * n)

Tactic:
simp only [sum_range_succ, even_two, Even.mul_right, Even.neg_pow, one_pow, one_mul] at lower

Goal state after:
case inl
E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
upper : ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Even (2 * n)
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n)
⊢ |∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i| ≤ f (2 * n)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
hz : ‖z‖ = 1
⊢ cexp (↑z.arg * I) = ↑‖z‖ * cexp (↑z.arg * I)

Tactic:
by rw [hz, ofReal_one, one_mul]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
⊢ log (cexp x) = x - ↑(toIocDiv Real.two_pi_pos (-π) x.im) * (2 * ↑π * I)

Tactic:
rw [log_exp_eq_re_add_toIocMod, toIocMod, ofReal_sub, sub_mul, ← add_sub_assoc]

Goal state after:
x : ℂ
⊢ ↑x.re + ↑x.im * I - ↑(toIocDiv Real.two_pi_pos (-π) x.im • (2 * π)) * I =
    x - ↑(toIocDiv Real.two_pi_pos (-π) x.im) * (2 * ↑π * I)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ Real.log (‖x‖ * ‖y‖) = Real.log ‖x‖ + Real.log ‖y‖ ∧ (x * y).arg = x.arg + y.arg ↔ (x * y).arg = x.arg + y.arg

Tactic:
Real.log_mul (norm_ne_zero_iff.mpr hx₀) (norm_ne_zero_iff.mpr hy₀),

Goal state after:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ True ∧ (x * y).arg = x.arg + y.arg ↔ (x * y).arg = x.arg + y.arg
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ 2 ≠ 0

Tactic:
exact two_ne_zero

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ log x ≤ x - 1

Tactic:
rw [le_sub_iff_add_le]
  convert! add_one_le_exp (log x)
  rw [exp_log hx]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ x ≤ 1

Tactic:
exact h2

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ log ↑n = n.factorization.sum fun p t ↦ ↑t * log ↑p

Tactic:
· simp only [← log_pow, ← Nat.cast_pow]
    rw [← Finsupp.log_prod, ← Nat.cast_finsuppProd, Nat.prod_factorization_pow_eq_self hn]
    intro p hp
    rw [eq_zero_of_pow_eq_zero (Nat.cast_eq_zero.1 hp), Nat.factorization_zero_right]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case mpr
x a : ℂ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a

Tactic:
rintro (⟨h, rfl⟩ | ⟨rfl, rfl⟩)
    · exact zero_cpow h
    · exact cpow_zero _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
⊢ 0 < Real.log e

Tactic:
rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
    have : (n : ℝ) / d < -1 := by exact_mod_cast of_decide_eq_true h
    exact Real.log_pos_of_lt_neg_one this

Goal state after: