mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series

Goal state before:
pp: case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦ ((z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! + (-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) / 2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
⊢ (z * I) ^ (2 * k) / ↑(2 * k)! =
    ((z * I) ^ (2 * k + 0) / ↑(2 * k + 0)! + (-z * I) ^ (2 * k + 0) / ↑(2 * k + 0)!) / 2 +
      ((z * I) ^ (2 * k + 1) / ↑(2 * k + 1)! + (-z * I) ^ (2 * k + 1) / ↑(2 * k + 1)!) / 2

Tactic:
add_zero,

Goal state after:
case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦ ((z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! + (-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) / 2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
⊢ (z * I) ^ (2 * k) / ↑(2 * k)! =
    ((z * I) ^ (2 * k) / ↑(2 * k)! + (-z * I) ^ (2 * k) / ↑(2 * k)!) / 2 +
      ((z * I) ^ (2 * k + 1) / ↑(2 * k + 1)! + (-z * I) ^ (2 * k + 1) / ↑(2 * k + 1)!) / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series

Goal state before:
pp: case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦ ((z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! + (-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) / 2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
⊢ (z ^ 2) ^ k * (I ^ 2) ^ k / ↑(2 * k)! = 2 * ((z ^ 2) ^ k * (I ^ 2) ^ k / ↑(2 * k)!) / 2 + 0

Tactic:
add_zero,

Goal state after:
case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦ ((z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! + (-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) / 2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
⊢ (z ^ 2) ^ k * (I ^ 2) ^ k / ↑(2 * k)! = 2 * ((z ^ 2) ^ k * (I ^ 2) ^ k / ↑(2 * k)!) / 2
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case inr
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) Set.univ z
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hM : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
H : ∀ (z : ℂ), ‖x - (algebraMap ℂ F) z‖ ≠ 0
key : ‖x‖ + M + 1 - ‖x‖ ≤ M
⊢ False

Tactic:
linarith only [key]

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

Goal state before:
pp: case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦
      ((-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! - (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) * I / 2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
k : ℕ
⊢ (z * I) ^ (2 * k + 1) / ↑(2 * k + 1)! / I =
    ((-z * I) ^ (2 * k + 0) / ↑(2 * k + 0)! - (z * I) ^ (2 * k + 0) / ↑(2 * k + 0)!) * I / 2 +
      ((-z * I) ^ (2 * k + 1) / ↑(2 * k + 1)! - (z * I) ^ (2 * k + 1) / ↑(2 * k + 1)!) * I / 2

Tactic:
add_zero,

Goal state after:
case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦
      ((-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! - (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) * I / 2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
k : ℕ
⊢ (z * I) ^ (2 * k + 1) / ↑(2 * k + 1)! / I =
    ((-z * I) ^ (2 * k) / ↑(2 * k)! - (z * I) ^ (2 * k) / ↑(2 * k)!) * I / 2 +
      ((-z * I) ^ (2 * k + 1) / ↑(2 * k + 1)! - (z * I) ^ (2 * k + 1) / ↑(2 * k + 1)!) * I / 2
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: q : ℍ
hq : q.re = 0
n : ℕ
⊢ ((expSeries ℝ ℍ (2 * n)) fun x ↦ q) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n)!)

Tactic:
rw [expSeries_apply_eq]
  have hq2 : q ^ 2 = -normSq q := sq_eq_neg_normSq.mpr hq
  let k : ℝ := ↑(2 * n)!
  calc
    k⁻¹ • q ^ (2 * n) = k⁻¹ • (-normSq q) ^ n := by rw [pow_mul, hq2]
    _ = k⁻¹ • ↑((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n)) := ?_
    _ = ↑((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n) / k) := ?_
  · congr 1
    rw [neg_pow, normSq_eq_norm_mul_self, pow_mul, sq]
    push_cast
    rfl
  · rw [← coe_mul_eq_smul, div_eq_mul_inv]
    norm_cast
    ring_nf

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

Goal state before:
pp: case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦
      ((-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! - (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) * I / 2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
k : ℕ
⊢ (z ^ 2) ^ k * (I ^ 2) ^ k * (z * I) / ↑(2 * k + 1)! / I =
    (-((z ^ 2) ^ k * (I ^ 2) ^ k * (z * I) / ↑(2 * k + 1)!) - (z ^ 2) ^ k * (I ^ 2) ^ k * (z * I) / ↑(2 * k + 1)!) * I /
      2

Tactic:
← neg_add',

Goal state after:
case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦
      ((-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! - (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) * I / 2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
k : ℕ
⊢ (z ^ 2) ^ k * (I ^ 2) ^ k * (z * I) / ↑(2 * k + 1)! / I =
    -((z ^ 2) ^ k * (I ^ 2) ^ k * (z * I) / ↑(2 * k + 1)! + (z ^ 2) ^ k * (I ^ 2) ^ k * (z * I) / ↑(2 * k + 1)!) * I / 2
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‖) ^ 2 * normSq q.im + 0 =
    Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2

Tactic:
add_zero,

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

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
H : φ x z ≠ 0
M : ℝ := ‖φ x z‖
h' : ∀ (r : ℝ), √M ≤ ‖x - (algebraMap ℝ F) r‖
this : Filter.Tendsto (fun x_1 ↦ ‖φ x x_1‖) (Bornology.cobounded (ℝ × ℝ)) Filter.atTop
⊢ False

Tactic:
simp only [norm_φ_eq_norm_φ_of_isMinOn h (norm_ne_zero_iff.mpr H)] at this

Goal state after:
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
H : φ x z ≠ 0
M : ℝ := ‖φ x z‖
h' : ∀ (r : ℝ), √M ≤ ‖x - (algebraMap ℝ F) r‖
this : Filter.Tendsto (fun x_1 ↦ ‖φ x z‖) (Bornology.cobounded (ℝ × ℝ)) Filter.atTop
⊢ False
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
⊢ ∀ (m : ℕ), p (x ^ s (ψ m)) ^ (1 / ↑(ψ m)) ≤ p x ^ (↑(s (ψ m)) / ↑(ψ m))

Tactic:
intro m

Goal state after:
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
m : ℕ
⊢ p (x ^ s (ψ m)) ^ (1 / ↑(ψ m)) ≤ p x ^ (↑(s (ψ m)) / ↑(ψ m))
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: case inl.refine_1
ι : 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
inst✝ : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) ⊥ f
x : R
hx : ∀ (a : R), x ≥ a
⊢ BddBelow Set.univ

pp: case inl.refine_2
ι : 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
inst✝ : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) ⊥ f
x : R
hx : ∀ (a : R), x ≥ a
⊢ BddAbove Set.univ

Tactic:
· refine ⟨x - x, mem_lowerBounds.2 fun y ↦ ?_⟩
      simp only [Set.mem_univ, true_implies]
      exact tsub_le_iff_tsub_le.1 (hx (x - y))

Goal state after:
case inl.refine_2
ι : 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
inst✝ : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) ⊥ f
x : R
hx : ∀ (a : R), x ≥ a
⊢ BddAbove Set.univ
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
⊢ ∃ m, ∀ n ≥ m, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))

Tactic:
have hε2 : 0 < ε / 2 := half_pos hε

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
hε2 : 0 < ε / 2
⊢ ∃ m, ∀ n ≥ m, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ Antitone (seminormFromConst_seq c f x)

Tactic:
intro m

Goal state after:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
m : ℕ
⊢ ∀ ⦃b : ℕ⦄, m ≤ b → seminormFromConst_seq c f x b ≤ seminormFromConst_seq c f x m
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
x✝ : ℝ
hx : x✝ < ‖r‖
⊢ x✝ < if 0 = 0 then ‖r‖ else 0

Tactic:
by simp only [if_true, hx]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
⊢ ∃ x, eval x f = 0

Tactic:
have norm_sub_le : ∀ a' : F, IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖ := by
    intro a' conj ne
    by_cases hS : S.Nonempty <;> simp only [hS, ↓reduceDIte, δ]
    · apply Finset.min'_le (S.image fun x => ‖a - x‖) (‖a - a'‖)
      apply Finset.mem_image_of_mem
      simp only [minpoly.eq_of_irreducible_of_monic firr fa0 fmon, Finset.mem_filter,
        Set.mem_toFinset, S]
      rw [← (isConjRoot_iff_mem_minpoly_rootSet ⟨f, fmon, fa0⟩)]
      exact ⟨conj, ne.symm⟩
    · simp only [ne_eq, Finset.not_nonempty_iff_eq_empty, Finset.filter_eq_empty_iff,
      Set.mem_toFinset, not_not, S] at hS
      rw [isConjRoot_iff_mem_minpoly_rootSet ⟨f, fmon, fa0⟩,
          ← minpoly.eq_of_irreducible_of_monic firr fa0 fmon] at conj
      exact (ne (hS conj).symm).elim

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
⊢ ∃ x, eval x f = 0
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
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
h : 0 < ↑p.natDegree - ↑m
hps : s.card = p.natDegree
⊢ f ((algebraMap K L) (p.coeff m)) = f ((Polynomial.map (algebraMap K L) p).coeff m)

Tactic:
coeff_map

Goal state after:
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
h : 0 < ↑p.natDegree - ↑m
hps : s.card = p.natDegree
⊢ f ((algebraMap K L) (p.coeff m)) = f ((algebraMap K L) (p.coeff m))
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : μ x < 1
⊢ c ≤ 1

Tactic:
apply hc_bd (1 : ℝ) 0

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : μ x < 1
⊢ ∀ (b : ℕ), 0 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ 1
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
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := ⋯
nu : ℕ → ℕ := ⋯
hnu : nu = fun n ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := ⋯
hb : b = 1 - a
⊢ ∀ (b : ℕ), 1 ≤ b → 1 - ↑(mu (ψ b)) / ↑(ψ b) = ↑(nu (ψ b)) / ↑(ψ b)

Tactic:
intro m

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := fun n ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun n ↦ n - mu n
hnu : nu = fun n ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
m : ℕ
⊢ 1 ≤ m → 1 - ↑(mu (ψ m)) / ↑(ψ m) = ↑(nu (ψ m)) / ↑(ψ m)
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
inst✝ : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
x : L
n : ℕ
hn : 1 ≤ n
E : IntermediateField K L := K⟮x⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
g : ↥K⟮x⟯ := AdjoinSimple.gen K x
hg : g = AdjoinSimple.gen K x
h_map : (algebraMap (↥E) L) g ^ n = x ^ n
⊢ spectralNorm K L (x ^ n) =
    spectralNorm K (↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
        ((algebraMap ↥K⟮x⟯ ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯))) (AdjoinSimple.gen K x)) ^
      n

Tactic:
← spectralNorm.eq_of_normalClosure (g ^ n) h_map,

Goal state after:
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
x : L
n : ℕ
hn : 1 ≤ n
E : IntermediateField K L := K⟮x⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
g : ↥K⟮x⟯ := AdjoinSimple.gen K x
hg : g = AdjoinSimple.gen K x
h_map : (algebraMap (↥E) L) g ^ n = x ^ n
⊢ spectralNorm K (↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
      ((algebraMap ↥K⟮x⟯ ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯))) (g ^ n)) =
    spectralNorm K (↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
        ((algebraMap ↥K⟮x⟯ ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯))) (AdjoinSimple.gen K x)) ^
      n
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁹ : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
f : E →L[R] F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
g : F →L[R] G
finv : F →L[R] E
hfinv : RightInverse ⇑finv ⇑f
ginv : G →L[R] F
hginv : RightInverse ⇑ginv ⇑g
x : G
⊢ g (ginv x) = x

Tactic:
hginv

Goal state after:
R : Type u_1
inst✝⁹ : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
f : E →L[R] F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
g : F →L[R] G
finv : F →L[R] E
hfinv : RightInverse ⇑finv ⇑f
ginv : G →L[R] F
hginv : RightInverse ⇑ginv ⇑g
x : G
⊢ x = x
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ ≤ ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖

Tactic:
have :=
              add_le_add_left (norm_le_insert' (R • x) (R • P • R • x)) (2 • ‖(1 - R) • P • R • x‖)

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
this : ‖R • x‖ + 2 • ‖(1 - R) • P • R • x‖ ≤ ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖
⊢ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ ≤ ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: case refine_2
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ ≤ ‖x‖

Tactic:
calc
      ‖x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖) := by
        rw [h₂.Lnorm x, h₁.Lnorm (Q • x), sub_smul, one_smul, sub_smul, one_smul, add_assoc]
      _ ≥ ‖P • Q • x‖ + ‖Q • x - P • Q • x + (x - Q • x)‖ :=
        ((add_le_add_iff_left ‖P • Q • x‖).mpr (norm_add_le (Q • x - P • Q • x) (x - Q • x)))
      _ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ := by
        rw [sub_add_sub_cancel', sub_smul, one_smul, mul_smul]

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

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P * ↑P + 0 + ↑Pᶜ * (↑Q * (↑R * ↑R) * ↑Pᶜ) = ↑P + ↑Pᶜ * (↑Q * ↑R)

Tactic:
add_zero,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P * ↑P + ↑Pᶜ * (↑Q * (↑R * ↑R) * ↑Pᶜ) = ↑P + ↑Pᶜ * (↑Q * ↑R)
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P * ↑P + 0 + ↑Q * ↑Pᶜ * (↑Pᶜ * ↑R) = ↑P + ↑Q * ↑R * ↑Pᶜ

Tactic:
add_zero,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P * ↑P + ↑Q * ↑Pᶜ * (↑Pᶜ * ↑R) = ↑P + ↑Q * ↑R * ↑Pᶜ
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : NormOneClass R
f : ι → R
inst✝ : CompleteSpace R
hf : Summable fun i ↦ ‖f i‖
ε : ℝ
hε : ε > 0
r₁ : ℝ
hr₁ : r₁ > 0
s₁ : Finset ι
hs₁ : ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, ‖1 + f i‖ ≤ r₁
s₂ : Finset ι
hs₂ : ∀ (t : Finset ι), Disjoint t s₂ → ‖∏ i ∈ t, (1 + f i) - 1‖ < ε / (2 * r₁)
s : Finset ι := s₁ ∪ s₂
x : R
hx : x ∈ Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2)
y : R
hy : y ∈ Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2)
⊢ dist x y < ε

Tactic:
exact (dist_triangle_right _ _ (∏ i ∈ s, (1 + f i))).trans_lt (add_halves ε ▸ add_lt_add hx hy)

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
⊢ (tprodL 𝕜).toMultilinearMap = tprod 𝕜

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → SeminormedAddCommGroup (E i)
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
⊢ (liftIsometry 𝕜 E (⨂[𝕜] (i : ι), E i)) (tprodL 𝕜) = ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i)

Tactic:
by
  ext; simp

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
s : Set ℝ
h : IsIntegralCurveOn γ v s
s' : Set ℝ
h₁ : s' ⊆ s
h₂ : IsOpen s'
h₃ : t₀ ∈ s'
t : ℝ
ht : t ∈ s'
⊢ HasDerivAt γ (v t (γ t)) t

Tactic:
apply (h t (h₁ ht)).hasDerivAt

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
s : Set ℝ
h : IsIntegralCurveOn γ v s
s' : Set ℝ
h₁ : s' ⊆ s
h₂ : IsOpen s'
h₃ : t₀ ∈ s'
t : ℝ
ht : t ∈ s'
⊢ s ∈ 𝓝 t
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
e : V ≃L[𝕜] W
α α' : 𝕜
hα : α ≠ 0
hα2 : α' * α' = α⁻¹
he : adjoint ↑e ∘SL ↑e = α • ContinuousLinearMap.id 𝕜 V
he' : ↑e ∘SL adjoint ↑e = α • ContinuousLinearMap.id 𝕜 W
hαa : (starRingEnd 𝕜) α' = α'
⊢ α⁻¹ • adjoint ↑e ∘SL ↑e = 1

Tactic:
simp [he, smul_smul, hα, one_def]

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
e : V ≃L[𝕜] W
α α' : 𝕜
hα : α ≠ 0
hα2 : α' * α' = α⁻¹
he : adjoint ↑e ∘SL ↑e = α • ContinuousLinearMap.id 𝕜 V
he' : ↑e ∘SL adjoint ↑e = α • ContinuousLinearMap.id 𝕜 W
hαa : (starRingEnd 𝕜) α' = α'
⊢ ↑(↑(auxIsometry e hα hα2 he he' hαa)).symm = α'⁻¹ • ↑e.symm

Tactic:
by
  ext y
  apply (auxIsometry e hα hα2 he he' hαa).toContinuousLinearEquiv.injective
  simp [smul_smul, inv_mul_cancel₀ (a := α') (by grind)]

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

Goal state before:
pp: δ K x : ℝ
⊢ gronwallBound δ K 0 x = δ * rexp (K * x)

Tactic:
by
  by_cases hK : K = 0
  · simp only [gronwallBound_K0, hK, zero_mul, exp_zero, add_zero, mul_one]
  · simp only [gronwallBound_of_K_ne_0 hK, zero_div, zero_mul, add_zero]

Goal state after: