mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
⊢ (Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹

Tactic:
rcases ne_or_eq s 0 with (h | rfl)
  · rw [Gamma_add_one s h, mul_inv, mul_inv_cancel_left₀ h]
  · rw [zero_add, Gamma_zero, inv_zero, zero_mul]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential

Goal state before:
pp: case inl
m : Type u_1
𝔸 : Type u_5
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
n : ℕ
⊢ exp (↑n • A) = exp A ^ ↑n

Tactic:
zpow_natCast,

Goal state after:
case inl
m : Type u_1
𝔸 : Type u_5
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
n : ℕ
⊢ exp (↑n • A) = exp A ^ n
Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential

Goal state before:
pp: case inr
m : Type u_1
𝔸 : Type u_5
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
n : ℕ
this : IsUnit (exp A).det
⊢ exp (-↑n • A) = (exp A ^ ↑n)⁻¹

Tactic:
zpow_natCast,

Goal state after:
case inr
m : Type u_1
𝔸 : Type u_5
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
n : ℕ
this : IsUnit (exp A).det
⊢ exp (-↑n • A) = (exp A ^ n)⁻¹
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case refine_2.inr.inr.inr.inl
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
i₂ : Fin 3
i j : Fin (2 + 1)
hij : i ≠ j
h₂₃ : i₂ ≠ i
h₁₂ : j ≠ i₂
h₁₃ : j ≠ i
h₁ : dist (t.points j) (t.points i₂) = dist (t.points j) (t.points i)
h₂ : dist (t.points j) (t.points i₂) = dist (t.points i₂) (t.points i)
⊢ dist (t.points i) (t.points j) = dist (t.points j) (t.points i₂)

Tactic:
h₁,

Goal state after:
case refine_2.inr.inr.inr.inl
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
i₂ : Fin 3
i j : Fin (2 + 1)
hij : i ≠ j
h₂₃ : i₂ ≠ i
h₁₂ : j ≠ i₂
h₁₃ : j ≠ i
h₁ : dist (t.points j) (t.points i₂) = dist (t.points j) (t.points i)
h₂ : dist (t.points j) (t.points i₂) = dist (t.points i₂) (t.points i)
⊢ dist (t.points i) (t.points j) = dist (t.points j) (t.points i)
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: q : ℍ
⊢ exp q.re ^ 2 * (Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2) = exp q.re ^ 2

Tactic:
Real.cos_sq_add_sin_sq,

Goal state after:
q : ℍ
⊢ exp q.re ^ 2 * 1 = exp q.re ^ 2
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
⊢ Tendsto (fun x_1 ↦ x ^ 2 - x_1.1 • x + (algebraMap ℝ F) x_1.2) (cobounded (ℝ × ℝ)) (cobounded F)

Tactic:
sub_add

Goal state after:
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
⊢ Tendsto (fun x_1 ↦ x ^ 2 - (x_1.1 • x - (algebraMap ℝ F) x_1.2)) (cobounded (ℝ × ℝ)) (cobounded F)
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
⊢ Tendsto (fun x_1 ↦ ‖x_1.1 • x - (algebraMap ℝ F) x_1.2‖) (cobounded (ℝ × ℝ)) atTop

Tactic:
refine Tendsto.coprod_of_prod_top_right (α := ℝ) (fun s hs ↦ ?_) ?_

Goal state after:
case refine_1
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
s : Set ℝ
hs : s ∈ cobounded ℝ
⊢ Tendsto (fun x_1 ↦ ‖x_1.1 • x - (algebraMap ℝ F) x_1.2‖) (𝓟 sᶜ ×ˢ cobounded ℝ) atTop

case refine_2
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
⊢ Tendsto (fun x_1 ↦ ‖x_1.1 • x - (algebraMap ℝ F) x_1.2‖) (cobounded ℝ ×ˢ ⊤) atTop
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
h1 : f 1 ≠ 0
hxn : f (x ^ n) = 0
⊢ False

Tactic:
have : f 1 ≤ 0 := by simpa [← mul_pow, hxn] using f_mul (x ^ n) (hx.unit⁻¹ ^ n)

Goal state after:
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
h1 : f 1 ≠ 0
hxn : f (x ^ n) = 0
this : f 1 ≤ 0
⊢ False
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x = 0 x
⊢ 0 ≤ c * f x

pp: case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : 0 x < f x
⊢ 0 ≤ c * f x

Tactic:
· simp [hx]

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : 0 x < f x
⊢ 0 ≤ c * f x
Module: Mathlib.Analysis.Normed.Field.Approximation

Goal state before:
pp: K : Type u_1
inst✝ : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this✝ : (Multiset.map (fun x ↦ ‖a - x‖) g.roots).prod < (↑f.natDegree + 1) * ε * max ‖a‖ 1 ^ ↑f.natDegree
h : ∀ b ∈ g.roots, ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this : (↑f.natDegree + 1) * ε * max ‖a‖ 1 ^ ↑f.natDegree ≤ (Multiset.map (fun b ↦ ‖a - b‖) g.roots).prod
⊢ False

pp: K : Type u_1
inst✝ : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this✝ : (Multiset.map (fun x ↦ ‖a - x‖) g.roots).prod < (↑f.natDegree + 1) * ε * max ‖a‖ 1 ^ ↑f.natDegree
h : ∀ b ∈ g.roots, ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this :
  ((↑f.natDegree + 1) * ε) ^ ((↑f.natDegree)⁻¹ * ↑f.natDegree) * max ‖a‖ 1 ^ ↑f.natDegree ≤
    (Multiset.map (fun b ↦ ‖a - b‖) g.roots).prod
⊢ ↑f.natDegree ≠ 0

Tactic:
· linarith

Goal state after:
K : Type u_1
inst✝ : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this✝ : (Multiset.map (fun x ↦ ‖a - x‖) g.roots).prod < (↑f.natDegree + 1) * ε * max ‖a‖ 1 ^ ↑f.natDegree
h : ∀ b ∈ g.roots, ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this :
  ((↑f.natDegree + 1) * ε) ^ ((↑f.natDegree)⁻¹ * ↑f.natDegree) * max ‖a‖ 1 ^ ↑f.natDegree ≤
    (Multiset.map (fun b ↦ ‖a - b‖) g.roots).prod
⊢ ↑f.natDegree ≠ 0
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

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

Tactic:
exact le_of_eq (seminormFromBounded_one f_ne_zero f_nonneg f_mul)

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
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
⊢ ⨆ y, f x * f y / f y = f x

Tactic:
← mul_div_assoc'

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
⊢ ⨆ y, f x * (f y / f y) = f x
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 : μ 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
hL2 : ∀ ε_1 > 0, ∃ N, ∀ n ≥ N, dist ((L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n)) 1 < ε_1
δ : ℝ := ε / (2 * (L + ε / 2))
hδ_def : δ = ε / (2 * (L + ε / 2))
hδ : 0 < δ
N n : ℕ
hN : dist ((L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n)) 1 < δ
hn : n ≥ N
⊢ (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ δ

Tactic:
rw [Real.dist_eq, abs_lt] at hN

Goal state after:
case h
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
hL2 : ∀ ε_1 > 0, ∃ N, ∀ n ≥ N, dist ((L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n)) 1 < ε_1
δ : ℝ := ε / (2 * (L + ε / 2))
hδ_def : δ = ε / (2 * (L + ε / 2))
hδ : 0 < δ
N n : ℕ
hN :
  -δ < (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ∧
    (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 < δ
hn : n ≥ N
⊢ (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ δ
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: case inr
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 n : ℕ
hmn : m ≤ n
hc_pos : 0 < f c
hlt : m < n
h1 : 1 ≤ n - m
⊢ f (x * c ^ m) * f (c ^ (n - m)) / f c ^ n ≤ f (x * c ^ m) / f c ^ m

Tactic:
rw [hpm c h1, mul_div_assoc, div_eq_mul_inv, pow_sub₀ _ hc hmn, mul_assoc, mul_comm (f c ^ m)⁻¹,
      ← mul_assoc (f c ^ n), mul_inv_cancel₀ (pow_ne_zero n hc), one_mul, div_eq_mul_inv]

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.IsConjRoot

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R S
r : R
x : S
h : IsConjRoot R ((algebraMap R S) r) x
hf : Function.Injective ⇑(algebraMap R S)
⊢ x = (algebraMap R S) r

Tactic:
rw [IsConjRoot, minpoly.eq_X_sub_C_of_algebraMap_inj _ hf] at h
  have : x ∈ (X - C r).aroots S := by
    rw [mem_aroots]
    simp [X_sub_C_ne_zero, h ▸ minpoly.aeval R x]
  simpa [aroots_X_sub_C] using this

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
n m : ℕ
hmn : m < n
⊢ 0 = 0 ∧ ¬↑n - ↑m = 0

Tactic:
← cast_sub (le_of_lt hmn),

Goal state after:
case pos
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
n m : ℕ
hmn : m < n
⊢ 0 = 0 ∧ ¬↑(n - m) = 0
Module: Mathlib.Analysis.Normed.Group.Completeness

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
⊢ ∃ f, StrictMono f ∧ Summable fun i ↦ dist (u (f (i + 1))) (u (f i))

Tactic:
by
  obtain ⟨f, hf₁, hf₂⟩ := Metric.exists_subseq_bounded_of_cauchySeq u hu
    (fun n => (1 / (2 : ℝ)) ^ n) (fun n => by positivity)
  refine ⟨f, hf₁, ?_⟩
  refine Summable.of_nonneg_of_le (fun n => by positivity) ?_ summable_geometric_two
  exact fun n => le_of_lt <| hf₂ n (f (n + 1)) <| hf₁.monotone (Nat.le_add_right n 1)

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

Goal state before:
pp: case neg
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'‖
hS : ¬S.Nonempty
⊢ 1 > 0

Tactic:
· linarith

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
hn0 : ¬n = 0
⊢ ↑(mu μ hn n) / ↑n ≤ 1

Tactic:
· rw [div_le_one (cast_pos.mpr (Nat.pos_of_ne_zero hn0)), cast_le]
    exact mu_le _ _ _

Goal state after:
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
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : μ x ≤ 1
n : ℕ
⊢ (μ x ^ s (ψ n)) ^ (1 / ↑(ψ n)) ≤ 1

Tactic:
rw [← rpow_natCast, ← rpow_mul (apply_nonneg _ _), mul_one_div]

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : μ x ≤ 1
n : ℕ
⊢ μ x ^ (↑(s (ψ n)) / ↑(ψ n)) ≤ 1
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case pos
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
x : L
hx : x ∈ s
⊢ (if x ∈ s then f x else 0) ≤ spectralValue p

Tactic:
have hx0 : aeval x p = 0 := aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C s hx hp

Goal state after:
case pos
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
x : L
hx : x ∈ s
hx0 : (aeval x) p = 0
⊢ (if x ∈ s then f x else 0) ≤ spectralValue p
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
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : 1 < μ x
n : ℕ
⊢ (μ x ^ s (ψ n)) ^ (1 / ↑(ψ n)) ≤ μ x

Tactic:
rw [← rpow_natCast, ← rpow_mul (apply_nonneg _ _), mul_one_div]

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : 1 < μ x
n : ℕ
⊢ μ x ^ (↑(s (ψ n)) / ↑(ψ n)) ≤ μ x
Module: Mathlib.Analysis.Normed.Group.HomCompletion

Goal state before:
pp: G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in : f.completion hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑g‖ < δ
g' : G
hgg' : f g' = f g
hfg : ‖g'‖ ≤ C' * ‖f g‖
mem_ker : g - g' ∈ f.ker
this : ‖f g‖ ≤ ‖f‖ * δ
⊢ ‖hatg - (↑g - ↑g')‖ = ‖hatg - ↑g + ↑g'‖

Tactic:
sub_add

Goal state after:
G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in : f.completion hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑g‖ < δ
g' : G
hgg' : f g' = f g
hfg : ‖g'‖ ≤ C' * ‖f g‖
mem_ker : g - g' ∈ f.ker
this : ‖f g‖ ≤ ‖f‖ * δ
⊢ ‖hatg - (↑g - ↑g')‖ = ‖hatg - (↑g - ↑g')‖
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y : SemiNormedGrp₁
f : X ⟶ Y
s : CokernelCofork f
⊢ (cokernelCocone f).pt ⟶ s.pt

Tactic:
fconstructor
  -- The lift itself:
  · apply NormedAddGroupHom.lift _ s.π.1
    rintro _ ⟨b, rfl⟩
    change (f ≫ s.π) b = 0
    simp
  -- The lift has norm at most one:
  exact NormedAddGroupHom.lift_normNoninc _ _ _ s.π.2

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
inst✝ : IsUltrametricDist K
k : K
y : L
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
g : ↥K⟮y⟯ := AdjoinSimple.gen K y
hgy : k • y = (algebraMap (↥K⟮y⟯) L) (k • g)
h :
  (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) (k • g) =
    k • (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g
⊢ spectralNorm K L (k • y) =
    ↑‖k‖₊ *
      spectralNorm K (↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
        ((algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g)

Tactic:
hgy,

Goal state after:
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsUltrametricDist K
k : K
y : L
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
g : ↥K⟮y⟯ := AdjoinSimple.gen K y
hgy : k • y = (algebraMap (↥K⟮y⟯) L) (k • g)
h :
  (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) (k • g) =
    k • (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g
⊢ spectralNorm K L ((algebraMap (↥K⟮y⟯) L) (k • g)) =
    ↑‖k‖₊ *
      spectralNorm K (↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
        ((algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g)
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:

Tactic:
f.hasLeftInverse.leftInverse y
    _ = f.hasLeftInverse.leftInverse (f (f.symm y)) := by simp
    _ = f.symm y := f.hasLeftInverse.leftInverse_leftInverse (f.symm y)

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set ↑(sphere 0 r)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U • Subtype.val '' V)

Tactic:
rw [isOpen_iff_mem_nhds]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set ↑(sphere 0 r)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
⊢ ∀ x ∈ U • Subtype.val '' V, U • Subtype.val '' V ∈ 𝓝 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 R : { P // IsLprojection X P }
h₁ : ↑P = ↑P * ↑Q
h₂ : ↑Q = ↑Q * ↑R
⊢ ↑P = ↑P * ↑R

Tactic:
h₁,

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 }
h₁ : ↑P = ↑P * ↑Q
h₂ : ↑Q = ↑Q * ↑R
⊢ ↑P * ↑Q = ↑P * ↑Q * ↑R
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
v : ι → ℝ
hv : Multipliable v
r₁ : ℝ
hr₁ : 0 < r₁ ∧ ∏' (i : ι), v i < r₁
this : ∀ᶠ (a : Finset ι) in (unconditional ι).filter, ∏ b ∈ a, v b ≤ r₁
⊢ ∃ r₁ > 0, ∃ s₁, ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁

Tactic:
unconditional,

Goal state after:
ι : Type u_1
v : ι → ℝ
hv : Multipliable v
r₁ : ℝ
hr₁ : 0 < r₁ ∧ ∏' (i : ι), v i < r₁
this : ∀ᶠ (a : Finset ι) in { filter := atTop }.filter, ∏ b ∈ a, v b ≤ r₁
⊢ ∃ r₁ > 0, ∃ s₁, ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁
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)
r : ℝ≥0∞
inst✝² : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
inst✝¹ : Fact (1 ≤ ∞)
f : ↥(lp F ∞)
inst✝ : Fact (1 ≤ r)
e : ↥(lp E r)
hp : 1 ≤ r.toReal
hpqr : r.HolderTriple ∞ r
s : Finset ι
⊢ ∑ i ∈ s, ‖↑(((holderₗ r B hBK) e) f) i‖ ^ r.toReal ≤ (↑K * ‖e‖ * ‖f‖) ^ r.toReal

Tactic:
mul_right_comm,

Goal state after:
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)
r : ℝ≥0∞
inst✝² : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
inst✝¹ : Fact (1 ≤ ∞)
f : ↥(lp F ∞)
inst✝ : Fact (1 ≤ r)
e : ↥(lp E r)
hp : 1 ≤ r.toReal
hpqr : r.HolderTriple ∞ r
s : Finset ι
⊢ ∑ i ∈ s, ‖↑(((holderₗ r B hBK) e) f) i‖ ^ r.toReal ≤ (↑K * ‖f‖ * ‖e‖) ^ r.toReal
Module: Mathlib.Analysis.Normed.Operator.Fredholm.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace F
u : E →L[𝕜] F
pkg : u.FredholmPackage
⊢ (↑pkg.quasiInverse).IsQuasiInverse ↑(pkg.decCodom.X₁.subtypeL ∘SL ↑pkg.equiv ∘SL pkg.decDom.proj)

Tactic:
have hdom : IsQuasiInverse pkg.decDom.X₁.subtype pkg.decDom.proj :=
    have := pkg.decDom.finite_X₀
    isQuasiInverse_subtype_projectionOnto _

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace F
u : E →L[𝕜] F
pkg : u.FredholmPackage
hdom : pkg.decDom.X₁.subtype.IsQuasiInverse ↑pkg.decDom.proj
⊢ (↑pkg.quasiInverse).IsQuasiInverse ↑(pkg.decCodom.X₁.subtypeL ∘SL ↑pkg.equiv ∘SL pkg.decDom.proj)
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Iic y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Iic y
hy : y₁ ≤ y₂
i : ι
x✝ : i ∈ Finset.univ
⊢ Real.nnabs (y i - y₂ i) ≤ nndist (y₁ i) (y i)

Tactic:
Real.nnabs_of_nonneg (sub_nonneg_of_le (‹_ ≤ y› i : y₂ i ≤ y i)),

Goal state after:
ι : Type u_2
inst✝ : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Iic y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Iic y
hy : y₁ ≤ y₂
i : ι
x✝ : i ∈ Finset.univ
⊢ (y i - y₂ i).toNNReal ≤ nndist (y₁ i) (y i)
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ ∃ y, closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior s

Tactic:
by
  refine ⟨x + const _ (3 / 4 * δ), closedBall_subset_closedBall' ?_, ?_⟩
  · grw [dist_self_add_left, ← const_def, pi_norm_const_le]
    apply le_of_eq
    simp [abs_of_nonneg, hδ.le]
    ring
  obtain ⟨y, hy, hxy⟩ := Metric.mem_closure_iff.1 hx _ (div_pos hδ zero_lt_four)
  refine fun z hz => hs.mem_interior_of_forall_lt (subset_closure hy) fun i => ?_
  rw [mem_closedBall, dist_eq_norm'] at hz
  rw [dist_eq_norm] at hxy
  replace hxy := (norm_le_pi_norm _ i).trans hxy.le
  replace hz := (norm_le_pi_norm _ i).trans hz
  dsimp at hxy hz
  rw [abs_sub_le_iff] at hxy hz
  linarith

Goal state after: