mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: f : ℕ → ℂ
t : ℂ
hf : (fun n ↦ f n - (1 + t / ↑n)) =o[atTop] fun n ↦ 1 / ↑n
⊢ Tendsto (fun n ↦ f n ^ n) atTop (𝓝 (cexp t))

Tactic:
rw [show (fun n ↦ f n ^ n) = (fun n ↦ (1 + (f n - 1)) ^ n) by ext; simp]
  refine tendsto_one_add_pow_exp_of_tendsto (tendsto_sub_nhds_zero_iff.1 ?_)
  convert! hf.tendsto_inv_smul_nhds_zero.congr' ?_
  filter_upwards [eventually_ne_atTop 0] with n h0
  simp
  field_simp [n.cast_ne_zero.2 h0]
  ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s t : ℂ
a : ℝ
ha : 0 < a
⊢ ∫ (x : ℝ) in 0..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) = ↑a ^ (s + t - 1) * s.betaIntegral t

Tactic:
have ha' : (a : ℂ) ≠ 0 := ofReal_ne_zero.mpr ha.ne'

Goal state after:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
⊢ ∫ (x : ℝ) in 0..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) = ↑a ^ (s + t - 1) * s.betaIntegral t
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case succ
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + ↑n) = f x + ∑ m ∈ Finset.range n, log (x + ↑m)
this : x + ↑n.succ = x + ↑n + 1
⊢ 0 < x + ↑n

Tactic:
· linarith [(Nat.cast_nonneg n : 0 ≤ (n : ℝ))]

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

Goal state before:
pp: z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * n.succ = 2 * n + 2
this✝² : ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝¹ :
  ↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ) =
    ↑π * z * A * ((1 - z ^ 2 / ↑n.succ ^ 2) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ))
this✝ :
  (1 - z ^ 2 / ↑n.succ ^ 2) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
this : ↑C ≠ 0
⊢ 2 * ↑n + 1 ≠ 0

Tactic:
convert! (Nat.cast_add_one_ne_zero (2 * n) : (↑(2 * n) + 1 : ℂ) ≠ 0)

Goal state after:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * n.succ = 2 * n + 2
this✝² : ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝¹ :
  ↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ) =
    ↑π * z * A * ((1 - z ^ 2 / ↑n.succ ^ 2) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ))
this✝ :
  (1 - z ^ 2 / ↑n.succ ^ 2) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
this : ↑C ≠ 0
⊢ 2 * ↑n = ↑(2 * n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_5
x : ℝ
⊢ 𝓝 (sin (π * x)) = 𝓝 (Complex.sin (↑π * ↑x)).re

Tactic:
· rw [← Complex.ofReal_mul, ← Complex.ofReal_sin, Complex.ofReal_re]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_1
⊢ ConvexOn ℝ (Ioi 0) fun s ↦ log (Γ (s / 2))

Tactic:
convert!
      convexOn_log_Gamma.comp_affineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2 : ℝ)).toAffineMap
      using 1

Goal state after:
case e'_11
⊢ Ioi 0 = ⇑(DistribSMul.toLinearMap ℝ ℝ (1 / 2)).toAffineMap ⁻¹' Ioi 0

case e'_12
⊢ (fun s ↦ log (Γ (s / 2))) = (log ∘ Γ) ∘ ⇑(DistribSMul.toLinearMap ℝ ℝ (1 / 2)).toAffineMap
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case e'_12
x : ℝ
⊢ log (Γ (x / 2)) = ((log ∘ Γ) ∘ ⇑(DistribSMul.toLinearMap ℝ ℝ (1 / 2)).toAffineMap) x

Tactic:
simp only [LinearMap.coe_toAffineMap, Function.comp_apply, DistribSMul.toLinearMap_apply]

Goal state after:
case e'_12
x : ℝ
⊢ log (Γ (x / 2)) = log (Γ ((1 / 2) • x))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / ↑n * ↑n
| ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)

Tactic:
enter [

Goal state after:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / ↑n * ↑n
| ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
n : ℕ
⊢ Integrable (f n) (volume.restrict (Ioi 0))

Tactic:
integrable_indicator_iff (measurableSet_Ioc : MeasurableSet (Ioc (_ : ℝ) _)),

Goal state after:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
n : ℕ
⊢ IntegrableOn (fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) (Ioc 0 ↑n) (volume.restrict (Ioi 0))
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : AddCommGroup M
inst✝¹³ : Algebra ℚ R
inst✝¹² : Module ℚ M
inst✝¹¹ : Module R M
inst✝¹⁰ : Module Rᵐᵒᵖ M
inst✝⁹ : IsCentralScalar R M
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : IsTopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : T2Space R
inst✝¹ : T2Space M
x : tsze R M
inst✝ : Invertible x.fst
⊢ x = inl x.fst + inr x.snd

Tactic:
inl_fst_add_inr_snd_eq

Goal state after:
R : Type u_3
M : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : AddCommGroup M
inst✝¹³ : Algebra ℚ R
inst✝¹² : Module ℚ M
inst✝¹¹ : Module R M
inst✝¹⁰ : Module Rᵐᵒᵖ M
inst✝⁹ : IsCentralScalar R M
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : IsTopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : T2Space R
inst✝¹ : T2Space M
x : tsze R M
inst✝ : Invertible x.fst
⊢ x = x
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: case e_a.inr
q : ℍ
hv : ‖q.im‖ ≠ 0
⊢ normSq (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) = Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2

Tactic:
normSq_add,

Goal state after:
case e_a.inr
q : ℍ
hv : ‖q.im‖ ≠ 0
⊢ normSq ↑(Real.cos ‖q.im‖) + normSq ((Real.sin ‖q.im‖ / ‖q.im‖) • q.im) +
      2 * (↑(Real.cos ‖q.im‖) * star ((Real.sin ‖q.im‖ / ‖q.im‖) • q.im)).re =
    Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x - 1‖ ≤ 1
⊢ IsUltrametricDist R

Tactic:
have (x : R) (hx : ‖x‖ ≤ 1) : ‖x + 1‖ ≤ 1 := by
    simpa only [← neg_add', norm_neg] using h (-x) (norm_neg x ▸ hx)
  exact isUltrametricDist_of_forall_norm_add_one_of_norm_le_one this

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : IsUnit x
hfx : f x ≠ 0
n : ℕ
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
⊢ f (x ^ n) ≠ 0

Tactic:
have h1 : f 1 ≠ 0 := map_one_ne_zero (Function.ne_iff.mpr ⟨x, hfx⟩) f_nonneg f_mul
  intro hxn
  have : f 1 ≤ 0 := by simpa [← mul_pow, hxn] using f_mul (x ^ n) (hx.unit⁻¹ ^ n)
  exact h1 <| this.antisymm (f_nonneg 1)

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝ : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx : f.toFun x = 0
⊢ x = 0

Tactic:
obtain ⟨c, hc⟩ := RingSeminorm.ne_zero_iff.mp hnt
      by_contra hn0
      have hc0 : f c = 0 := by
        rw [← mul_one c, ← mul_inv_cancel₀ hn0, ← mul_assoc, mul_comm c, mul_assoc]
        exact
          le_antisymm
            (le_trans (map_mul_le_mul f _ _)
              (by rw [← RingSeminorm.toFun_eq_coe, ← AddGroupSeminorm.toFun_eq_coe, hx,
                zero_mul]))
            (apply_nonneg f _)
      exact hc hc0

Goal state after:
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : AddCommSemigroup R
inst✝² : Sub R
inst✝¹ : ContinuousSub R
inst✝ : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) ⊥ f
cobdd : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) ⊥ f
⊢ limsup (fun i ↦ f i - c) ⊥ = limsup f ⊥ - c

Tactic:
have {a : R} : sInf Set.univ ≤ a := by
      apply csInf_le _ (Set.mem_univ a)
      simp only [IsCoboundedUnder, IsCobounded, map_bot, eventually_bot, true_implies] at cobdd
      rcases cobdd with ⟨x, hx⟩
      refine ⟨x, mem_lowerBounds.2 fun y ↦ ?_⟩
      simp only [Set.mem_univ, hx y, implies_true]

Goal state after:
case inl
ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : AddCommSemigroup R
inst✝² : Sub R
inst✝¹ : ContinuousSub R
inst✝ : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) ⊥ f
cobdd : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) ⊥ f
this : ∀ {a : R}, sInf Set.univ ≤ a
⊢ limsup (fun i ↦ f i - c) ⊥ = limsup f ⊥ - c
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
⊢ seminormFromBounded' f 1 = 1

Tactic:
simp_rw [seminormFromBounded', one_mul]
  apply le_antisymm
  · refine ciSup_le (fun x ↦ ?_)
    by_cases hx : f x = 0
    · rw [hx, div_zero]; exact zero_le_one
    · rw [div_self hx]
  · rw [← div_self (map_one_ne_zero f_ne_zero f_nonneg f_mul)]
    have h_bdd : BddAbove (Set.range fun y ↦ f y / f y) := by
      use (1 : ℝ)
      rintro r ⟨y, rfl⟩
      by_cases hy : f y = 0
      · simp only [hy, div_zero, zero_le_one]
      · simp only [div_self hy, le_refl]
    exact le_ciSup h_bdd (1 : R)

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq : ∀ (y : S), ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥R[y]), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
x : S
g₁ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₁
g₂ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₂
hg₁_pm : IsPowMul ⇑g₁
hg₂_pm : IsPowMul ⇑g₂
y : ↥R[x] := ⟨x, ⋯⟩
hy : x = ↑y
h1 : f₁ ↑y = g₁ y
h2 : f₂ ↑y = g₂ y
C₁ C₂ : ℝ
hC₁_pos : 0 < C₁
hC₂_pos : 0 < C₂
hC : ∀ (x_1 : ↥R[x]), f₁ ↑x_1 ≤ C₁ * f₂ ↑x_1 ∧ f₂ ↑x_1 ≤ C₂ * f₁ ↑x_1
hC₁ : ∀ (x_1 : ↥R[x]), f₁ ↑x_1 ≤ C₁ * f₂ ↑x_1
hC₂ : ∀ (x_1 : ↥R[x]), f₂ ↑x_1 ≤ C₂ * f₁ ↑x_1
⊢ g₁ y = g₂ y

Tactic:
eq_seminorms hg₁_pm hg₂_pm ⟨C₁, hC₁_pos, hC₁⟩ ⟨C₂, hC₂_pos, hC₂⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq : ∀ (y : S), ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥R[y]), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
x : S
g₁ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₁
g₂ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₂
hg₁_pm : IsPowMul ⇑g₁
hg₂_pm : IsPowMul ⇑g₂
y : ↥R[x] := ⟨x, ⋯⟩
hy : x = ↑y
h1 : f₁ ↑y = g₁ y
h2 : f₂ ↑y = g₂ y
C₁ C₂ : ℝ
hC₁_pos : 0 < C₁
hC₂_pos : 0 < C₂
hC : ∀ (x_1 : ↥R[x]), f₁ ↑x_1 ≤ C₁ * f₂ ↑x_1 ∧ f₂ ↑x_1 ≤ C₂ * f₁ ↑x_1
hC₁ : ∀ (x_1 : ↥R[x]), f₁ ↑x_1 ≤ C₁ * f₂ ↑x_1
hC₂ : ∀ (x_1 : ↥R[x]), f₂ ↑x_1 ≤ C₂ * f₁ ↑x_1
⊢ g₂ y = g₂ y
Module: Mathlib.Analysis.Normed.Field.Krasner

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Normal K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this✝¹ : FiniteDimensional K ↥K⟮y⟯
this✝ : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : z ∈ K⟮y⟯ ↔ z ∈ ⊥
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
σ : Gal(L/↥K⟮y⟯)
hσ : z' = σ.symm z
⊢ max ‖z‖ ‖z'‖ ≤ ‖x - y‖

Tactic:
simp only [NormedAlgebra.norm_eq_spectralNorm K, hσ, sup_le_iff]
          rw [← AlgEquiv.restrictScalars_apply K,
              ← spectralNorm_eq_of_equiv (σ.symm.restrictScalars K)]
          simp [z]

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

Goal state before:
pp: G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun n ↦ ∑ k ∈ range (n + 1), u k
this✝ : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
this : ‖v 0‖ ≤ ‖h‖ + b 0
⊢ C * (b 0 + ‖h‖) = C * b 0 + C * ‖h‖

Tactic:
mul_add

Goal state after:
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun n ↦ ∑ k ∈ range (n + 1), u k
this✝ : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
this : ‖v 0‖ ≤ ‖h‖ + b 0
⊢ C * b 0 + C * ‖h‖ = C * b 0 + C * ‖h‖
Module: Mathlib.Analysis.Normed.Group.ControlledClosure

Goal state before:
pp: G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun n ↦ ∑ k ∈ range (n + 1), u k
this✝ : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
⊢ ∑ k ∈ range (n + 1), C * b k + C * ‖h‖ ≤ (C + ε) * ‖h‖

Tactic:
rw [add_comm, add_mul]

Goal state after:
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun n ↦ ∑ k ∈ range (n + 1), u k
this✝ : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
⊢ C * ‖h‖ + ∑ k ∈ range (n + 1), C * b k ≤ C * ‖h‖ + ε * ‖h‖
Module: Mathlib.Analysis.Normed.Group.ControlledClosure

Goal state before:

Tactic:
‖s n‖ ≤ ∑ k ∈ range (n + 1), ‖u k‖ := norm_sum_le _ _
      _ = (∑ k ∈ range n, ‖u (k + 1)‖) + ‖u 0‖ := sum_range_succ' _ _
      _ ≤ (∑ k ∈ range n, C * ‖v (k + 1)‖) + ‖u 0‖ := by gcongr; apply hnorm_u
      _ ≤ (∑ k ∈ range n, C * b (k + 1)) + (C * b 0 + C * ‖h‖) := by
        gcongr with k; exact (hv _ k.succ_pos).le
      _ = (∑ k ∈ range (n + 1), C * b k) + C * ‖h‖ := by rw [← add_assoc, sum_range_succ']
      _ ≤ (C + ε) * ‖h‖ := by
        rw [add_comm, add_mul]
        gcongr

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
y : L
hy : y ≠ 0
hy_alg : IsAlgebraic K y
⊢ 0 ≠ spectralNorm K L y

Tactic:
rw [spectralNorm, ne_eq, eq_comm, spectralValue_eq_zero_iff (minpoly.monic hy_alg.isIntegral)]

Goal state after:
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
y : L
hy : y ≠ 0
hy_alg : IsAlgebraic K y
⊢ ¬minpoly K y = X ^ (minpoly K y).natDegree
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
n✝ : R
n : ℕ+
hneg : (-1) ^ ↑n = -1
⊢ μ (-1 * n✝ ^ ↑n) ^ (1 / ↑↑n) = μ (n✝ ^ ↑n) ^ (1 / ↑↑n)

Tactic:
neg_one_mul,

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
n✝ : R
n : ℕ+
hneg : (-1) ^ ↑n = -1
⊢ μ (-n✝ ^ ↑n) ^ (1 / ↑↑n) = μ (n✝ ^ ↑n) ^ (1 / ↑↑n)
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
n : ℕ
hn : 1 ≤ n
⊢ μ (x ^ n) ^ (1 / ↑n) = μ x

Tactic:
by_cases hx0 : μ x = 0

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
n : ℕ
hn : 1 ≤ n
hx0 : μ x = 0
⊢ μ (x ^ n) ^ (1 / ↑n) = μ x

case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
n : ℕ
hn : 1 ≤ n
hx0 : ¬μ x = 0
⊢ μ (x ^ n) ^ (1 / ↑n) = μ x
Module: Mathlib.Analysis.Normed.Lp.LpEquiv

Goal state before:
pp: α : Type u_1
E : Type u_2
R : Type u_3
A : Type u_4
𝕜 : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : DiscreteTopology α
inst✝⁶ : NormedRing A
inst✝⁵ : NormOneClass A
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NonUnitalNormedRing R
f : ↥(lp (fun x ↦ E) ∞)
⊢ ‖{ toFun := AddEquiv.lpBCF.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := AddEquiv.lpBCF.invFun, left_inv := ⋯,
          right_inv := ⋯ }
        f‖ =
    ‖f‖

Tactic:
by simp only [norm_eq_iSup_norm, lp.norm_eq_ciSup]; rfl

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
x : L
E : Type v := ((mapAlg K L) (minpoly K x)).SplittingField
hspl : ((mapAlg K E) (minpoly K x)).Splits
this✝ : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
⊢ ↑(minpoly K x).natDegree ≠ 0

Tactic:
exact_mod_cast (minpoly.natDegree_pos (Algebra.IsIntegral.isIntegral x)).ne'

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
hf : Summable fun i ↦ ‖f i‖
| Multipliable fun i ↦ ‖1 + f i‖

Tactic:
enter [

Goal state after:
ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
hf : Summable fun i ↦ ‖f i‖
| Multipliable fun i ↦ ‖1 + f i‖
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
t : Finset ι
f : ι → R
⊢ ‖∏ i ∈ t, (1 + f i) - 1‖ ≤ Real.exp (∑ i ∈ t, ‖f i‖) - 1

Tactic:
classical
  induction t using Finset.induction_on with
  | empty => simp
  | insert x t hx IH =>
    rw [Finset.prod_insert hx, Finset.sum_insert hx, Real.exp_add,
      show (1 + f x) * ∏ i ∈ t, (1 + f i) - 1 =
        (∏ i ∈ t, (1 + f i) - 1) + f x * ∏ x ∈ t, (1 + f x) by ring]
    refine (norm_add_le_of_le IH (norm_mul_le _ _)).trans ?_
    generalize h : Real.exp (∑ i ∈ t, ‖f i‖) = A at ⊢ IH
    rw [sub_add_eq_add_sub, sub_le_sub_iff_right]
    transitivity A + ‖f x‖ * A
    · grw [norm_le_norm_sub_add (∏ x ∈ t, (1 + f x)) 1, IH, norm_one, sub_add_cancel]
    rw [← one_add_mul, add_comm]
    exact mul_le_mul_of_nonneg_right (Real.add_one_le_exp _) (h ▸ Real.exp_nonneg _)

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Module

Goal state before:
pp: R : Type u_1
M : Type u_3
Nₗ : Type u_5
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup Nₗ
inst✝³ : Module R M
inst✝² : Module R Nₗ
fₗ : M →ₗ[R] Nₗ
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace Nₗ
⊢ IsStrictMap ⇑fₗ ↔ IsHomeomorph ⇑fₗ.quotKerEquivRange

Tactic:
by
  -- Note: right now, this cannot easily be deduced from the `AddMonoidHom` statement, because
  -- `fₗ.quotKerEquivRange.toAddEquiv` is not def-eq to
  -- `QuotientAddGroup.quotientKerEquivRange fₗ.toAddMonoidHom`. This would require
  -- fixing the definition of `LinearMap.quotKerEquivRange`.
  simp_rw [isHomeomorph_iff_isStrictMap_bijective, EquivLike.bijective, and_true,
    fₗ.ker.isQuotientMap_mkQ.isStrictMap_iff, IsEmbedding.subtypeVal.isStrictMap_iff]
  rfl

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: case inr.inl
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
q r : ℝ≥0∞
e : (i : ι) → E i
f : (i : ι) → F i
hf : Memℓp f q
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
h : Nonempty ι
hK : 0 ≤ K
hpqr : HolderTriple 0 q 0
he : Memℓp e 0
hpqr' : r = 0
⊢ Memℓp (fun i ↦ ((B i) (e i)) (f i)) 0

Tactic:
exact he.bilin_of_zero_left B

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace 𝕜 V
inst✝⁷ : CompleteSpace V
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : InnerProductSpace 𝕜 W
inst✝⁴ : CompleteSpace W
F : Type u_4
inst✝³ : EquivLike F (V →L[𝕜] V) (W →L[𝕜] W)
inst✝² : NonUnitalAlgEquivClass F 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
inst✝¹ : StarHomClass F (V →L[𝕜] V) (W →L[𝕜] W)
inst✝ : ContinuousMapClass F (V →L[𝕜] V) (W →L[𝕜] W)
f : F
x y : V →L[𝕜] V
U : V ≃ₗᵢ[𝕜] W
hU : ↑f = U.conjStarAlgEquiv
a : V →L[𝕜] V
⊢ f a = U.conjStarAlgEquiv a

Tactic:
simpa using! congr($hU a)

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r
t : ↑(Icc tmin tmax)
⊢ ‖α.toFun t - α.toFun t₀‖ + ‖α.toFun t₀ - x₀‖ ≤ ↑L * |↑t - ↑t₀| + ↑r

Tactic:
by
      apply add_le_add _ <| mem_closedBall_iff_norm.mp α.mem_closedBall₀
      rw [← dist_eq_norm]
      exact α.lipschitzWith.dist_le_mul t t₀

Goal state after:
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: case e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (a⁻¹ • s)
⊢ s = {t | t * a⁻¹ ∈ a⁻¹ • s}

Tactic:
simp only [mul_comm _ a⁻¹, ← smul_eq_mul, mem_inv_smul_set_iff₀ ha, smul_inv_smul₀ ha,
      ofPred_mem_eq]

Goal state after: