mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
c : k
v p : V
hs₁ : StarConvex k p s
hs₂ : IsClosed[inst✝²] s
hc : 0 ≤ c
hv : ∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.1 • a.2 +ᵥ p ∈ s
t : k
u : V
ht : c ≤ t
⊢ (t, u).1 • (t, u).2 +ᵥ p ∈ s → c • (t, u).2 +ᵥ p ∈ s

Tactic:
(h : t • u +ᵥ p ∈ s)

Goal state after:
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
c : k
v p : V
hs₁ : StarConvex k p s
hs₂ : IsClosed[inst✝²] s
hc : 0 ≤ c
hv : ∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.1 • a.2 +ᵥ p ∈ s
t : k
u : V
ht : c ≤ t
h : t • u +ᵥ p ∈ s
⊢ c • (t, u).2 +ᵥ p ∈ s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case inl
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : ↑n < x
⊢ ‖0‖ ≤ rexp (-x) * x ^ (s.re - 1)

Tactic:
norm_zero,

Goal state after:
case inl
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : ↑n < x
⊢ 0 ≤ rexp (-x) * x ^ (s.re - 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this✝ : ↑n ^ z * ↑n ^ (1 - z) = ↑n
this : ∀ (j : ℕ), (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)
⊢ ↑n * ↑n ! ^ 2 / ((↑(n ! ^ 2) * ∏ x ∈ Finset.range n, (1 - z ^ 2 / (↑x + 1) ^ 2)) * (z * (↑n + 1 - z))) =
    ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))

Tactic:
Nat.cast_pow,

Goal state after:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this✝ : ↑n ^ z * ↑n ^ (1 - z) = ↑n
this : ∀ (j : ℕ), (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)
⊢ ↑n * ↑n ! ^ 2 / ((↑n ! ^ 2 * ∏ x ∈ Finset.range n, (1 - z ^ 2 / (↑x + 1) ^ 2)) * (z * (↑n + 1 - z))) =
    ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: 𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst✝¹² : SeminormedCommRing S
inst✝¹¹ : SeminormedRing R
inst✝¹⁰ : SeminormedAddCommGroup M
inst✝⁹ : Algebra S R
inst✝⁸ : Module S M
inst✝⁷ : IsBoundedSMul S R
inst✝⁶ : IsBoundedSMul S M
inst✝⁵ : Module R M
inst✝⁴ : IsBoundedSMul R M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : IsBoundedSMul Rᵐᵒᵖ M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝ : NormOneClass R
⊢ ‖1‖ + ‖0‖ = 1

Tactic:
norm_zero,

Goal state after:
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst✝¹² : SeminormedCommRing S
inst✝¹¹ : SeminormedRing R
inst✝¹⁰ : SeminormedAddCommGroup M
inst✝⁹ : Algebra S R
inst✝⁸ : Module S M
inst✝⁷ : IsBoundedSMul S R
inst✝⁶ : IsBoundedSMul S M
inst✝⁵ : Module R M
inst✝⁴ : IsBoundedSMul R M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : IsBoundedSMul Rᵐᵒᵖ M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝ : NormOneClass R
⊢ ‖1‖ + 0 = 1
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: ⊢ ‖1‖ = 1

Tactic:
norm_eq_sqrt_real_inner,

Goal state after:
⊢ √⟪1, 1⟫ = 1
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: a : ℝ
⊢ ‖↑a‖ = ‖a‖

Tactic:
norm_eq_sqrt_real_inner,

Goal state after:
a : ℝ
⊢ √⟪↑a, ↑a⟫ = ‖a‖
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: a : ℍ
⊢ ‖star a‖ = ‖a‖

Tactic:
norm_eq_sqrt_real_inner,

Goal state after:
a : ℍ
⊢ √⟪star a, star a⟫ = √⟪a, a⟫
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: x✝¹ x✝ : ℍ
⊢ ‖x✝¹ * x✝‖ = ‖x✝¹‖ * ‖x✝‖

Tactic:
norm_eq_sqrt_real_inner,

Goal state after:
x✝¹ x✝ : ℍ
⊢ √⟪x✝¹ * x✝, x✝¹ * x✝⟫ = √⟪x✝¹, x✝¹⟫ * √⟪x✝, x✝⟫
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: x : ℍ
⊢ ‖WithLp.toLp 2 ((equivTuple ℝ) x)‖ = ‖x‖

Tactic:
norm_eq_sqrt_real_inner,

Goal state after:
x : ℍ
⊢ √⟪WithLp.toLp 2 ((equivTuple ℝ) x), WithLp.toLp 2 ((equivTuple ℝ) x)⟫ = ‖x‖
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: x : ℍ
⊢ √⟪WithLp.toLp 2 ((equivTuple ℝ) x), WithLp.toLp 2 ((equivTuple ℝ) x)⟫ = ‖x‖

Tactic:
norm_eq_sqrt_real_inner,

Goal state after:
x : ℍ
⊢ √⟪WithLp.toLp 2 ((equivTuple ℝ) x), WithLp.toLp 2 ((equivTuple ℝ) x)⟫ = √⟪x, x⟫
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: q : ℍ
hq : q.re = 0
⊢ HasSum (fun n ↦ (expSeries ℝ ℍ n) fun x ↦ q) (↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q)

Tactic:
exact hasSum_expSeries_of_imaginary hq (Real.hasSum_cos _) (Real.hasSum_sin _)

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

Goal state before:
pp: R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
⊢ ∃ m, ↑(m + 1) < (a / max 1 ‖x‖) ^ m

Tactic:
apply_mod_cast Real.exists_natCast_add_one_lt_pow_of_one_lt

Goal state after:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
⊢ 1 < a / max 1 ‖x‖
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: q : ℍ
⊢ ‖exp q‖ = ‖exp q.re‖

Tactic:
by
  rw [norm_eq_sqrt_real_inner (exp q), inner_self, normSq_exp, Real.sqrt_sq_eq_abs,
    Real.norm_eq_abs]

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

Goal state before:
pp: A : Type u_2
inst✝ : Ring A
f : MulRingNorm A
x : A
n : ℕ
hn : 1 ≤ n
⊢ f (x ^ n) = f x ^ n

Tactic:
cases n
  · lia
  · rw [map_pow]

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

Tactic:
simp [hx]

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean Norm.norm
x y : L
ixy : ι
left✝ : ixy ∈ univ
hixy : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x + y)) i‖) = ‖(B.repr (x + y)) ixy‖
⊢ ‖(B.repr x) ixy + (B.repr y) ixy‖ ≤ max ‖(B.repr x) ixy‖ ‖(B.repr y) ixy‖

Tactic:
exact hna _ _

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

Goal state before:
pp: case neg
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
hna : IsNonarchimedean f
x y z : R
hz : ¬f z = 0
⊢ f (x * z + y * z) ≤ max (f (x * z)) (f (y * z))

Tactic:
exact hna _ _

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

Goal state before:
pp: K : Type u_2
S : Type u_4
inst✝³ : CommRing S
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : IsDomain S
x y : S
h : IsIntegral K x
⊢ (Polynomial.aeval y) (minpoly K x) = 0 ↔ minpoly K x ≠ 0 ∧ (Polynomial.aeval y) (minpoly K x) = 0

Tactic:
simp only [iff_and_self]

Goal state after:
K : Type u_2
S : Type u_4
inst✝³ : CommRing S
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : IsDomain S
x y : S
h : IsIntegral K x
⊢ (Polynomial.aeval y) (minpoly K x) = 0 → minpoly K x ≠ 0
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 ∧ 1 / (↑n - ↑m) ≠ 0

Tactic:
norm_zero,

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

Goal state before:
pp: case h
E : Type u_2
F : Type u_3
𝓕 : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : 𝓕
inst✝² : ProperSpace F
inst✝¹ : FunLike 𝓕 E F
inst✝ : CocompactMapClass 𝓕 E F
ε : ℝ
h : ⇑f ⁻¹' (closedBall 0 ε)ᶜ ∈ cocompact E
r : ℝ
hr : (closedBall 0 r)ᶜ ⊆ ⇑f ⁻¹' (closedBall 0 ε)ᶜ
x : E
hx : r < ‖x‖
⊢ x ∈ (closedBall 0 r)ᶜ

Tactic:
simp [hx]

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x ↦ ‖u x‖) → ∃ a, Tendsto (fun n ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i ↦ ‖u (f (i + 1)) - u (f i)‖
v : ℕ → E := fun n ↦ u (f (n + 1)) - u (f n)
hv_sum : (fun n ↦ ∑ i ∈ range n, v i) = fun n ↦ u (f n) - u (f 0)
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
obtain ⟨a, ha⟩ := h v hf₂

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x ↦ ‖u x‖) → ∃ a, Tendsto (fun n ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable fun i ↦ ‖u (f (i + 1)) - u (f i)‖
v : ℕ → E := fun n ↦ u (f (n + 1)) - u (f n)
hv_sum : (fun n ↦ ∑ i ∈ range n, v i) = fun n ↦ u (f n) - u (f 0)
a : E
ha : Tendsto (fun n ↦ ∑ i ∈ range n, v i) atTop (𝓝 a)
⊢ ∃ a, Tendsto u atTop (𝓝 a)
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
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
h_ge : ¬f x ≤ spectralValue p
hn_lt : ∀ n < p.natDegree, ‖p.coeff n‖ < f x ^ (p.natDegree - n)
h_deg : 0 < p.natDegree
n : ℕ
hn : n < p.natDegree
hn0 : ¬n = 0
⊢ p.natDegree = p.natDegree - n + n

Tactic:
Nat.sub_add_cancel (le_of_lt hn)

Goal state after:
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
h_ge : ¬f x ≤ spectralValue p
hn_lt : ∀ n < p.natDegree, ‖p.coeff n‖ < f x ^ (p.natDegree - n)
h_deg : 0 < p.natDegree
n : ℕ
hn : n < p.natDegree
hn0 : ¬n = 0
⊢ p.natDegree = p.natDegree
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
E : Type u_4
inst✝³ : Field E
inst✝² : Algebra K E
inst✝¹ : Algebra E L
inst✝ : IsScalarTower K E L
x : E
hx : minpoly K ((algebraMap E L) x) = minpoly K x
⊢ spectralNorm K E x = spectralNorm K L ((algebraMap E L) x)

Tactic:
simp only [spectralNorm, hx]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
cond2 : g ≫ h = 0
⊢ explicitCokernelπ f ≫ explicitCokernelDesc cond ≫ h = explicitCokernelπ f ≫ 0

Tactic:
← Category.assoc,

Goal state after:
X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
cond2 : g ≫ h = 0
⊢ (explicitCokernelπ f ≫ explicitCokernelDesc cond) ≫ h = explicitCokernelπ 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✝ : IsUltrametricDist K
x y : L
hx : IsAlgebraic K x
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮x, y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
gx : ↥K⟮x, y⟯ := AdjoinPair.gen₁ K x y
gy : ↥K⟮x, y⟯ := AdjoinPair.gen₂ K x y
hxy : x * y = (algebraMap (↥K⟮x, y⟯) L) (gx * gy)
⊢ spectralNorm K L (x * y) ≤ spectralNorm K L x * spectralNorm K L y

Tactic:
hxy,

Goal state after:
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsUltrametricDist K
x y : L
hx : IsAlgebraic K x
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮x, y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
gx : ↥K⟮x, y⟯ := AdjoinPair.gen₁ K x y
gy : ↥K⟮x, y⟯ := AdjoinPair.gen₂ K x y
hxy : x * y = (algebraMap (↥K⟮x, y⟯) L) (gx * gy)
⊢ spectralNorm K L ((algebraMap (↥K⟮x, y⟯) L) (gx * gy)) ≤ spectralNorm K L x * spectralNorm K L y
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

Goal state before:
pp: M : Type u_1
N✝ : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_3
inst✝ : SeminormedAddCommGroup N
g : NormedAddGroupHom (SeparationQuotient M) N
x : M
hx : mk x = 0
⊢ (g.comp normedMk) x = 0

Tactic:
simp [hx]

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
h_alg : Algebra.IsAlgebraic K L
x y : L
E : IntermediateField K L := K⟮x, y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
gx : ↥K⟮x, y⟯ := AdjoinPair.gen₁ K x y
gy : ↥K⟮x, y⟯ := AdjoinPair.gen₂ K x y
hxy : x + y = (algebraMap (↥K⟮x, y⟯) L) (gx + gy)
⊢ spectralNorm K L (x + y) ≤ max (spectralNorm K L x) (spectralNorm K L y)

Tactic:
hxy,

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 y : L
E : IntermediateField K L := K⟮x, y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
gx : ↥K⟮x, y⟯ := AdjoinPair.gen₁ K x y
gy : ↥K⟮x, y⟯ := AdjoinPair.gen₂ K x y
hxy : x + y = (algebraMap (↥K⟮x, y⟯) L) (gx + gy)
⊢ spectralNorm K L ((algebraMap (↥K⟮x, y⟯) L) (gx + gy)) ≤ max (spectralNorm K L x) (spectralNorm K L y)
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
n : ℕ
hn : 0 ≤ 1 / ↑n
⊢ μ ((x * y) ^ n) ^ (1 / ↑n) ≤ μ (x ^ n) ^ (1 / ↑n) * μ (y ^ n) ^ (1 / ↑n)

Tactic:
← mul_rpow (apply_nonneg μ _) (apply_nonneg μ _),

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
n : ℕ
hn : 0 ≤ 1 / ↑n
⊢ μ ((x * y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ n) * μ (y ^ n)) ^ (1 / ↑n)
Module: Mathlib.Analysis.Normed.Lp.Finsupp

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : PseudoEMetricSpace X
f g h : WithLp (↑p) (ι →₀ X)
this : 0 < p
s : Finset ι := f.ofLp.support ∪ g.ofLp.support ∪ h.ofLp.support
⊢ (∑ x ∈ s, (zipWith edist ⋯ f.ofLp h.ofLp) x ^ ↑p) ^ (↑p)⁻¹ ≤
    (∑ x ∈ s, (zipWith edist ⋯ f.ofLp g.ofLp) x ^ ↑p) ^ (↑p)⁻¹ +
      (∑ x ∈ s, (zipWith edist ⋯ g.ofLp h.ofLp) x ^ ↑p) ^ (↑p)⁻¹

Tactic:
simp only [zipWith_apply, ← one_div]

Goal state after:
ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : PseudoEMetricSpace X
f g h : WithLp (↑p) (ι →₀ X)
this : 0 < p
s : Finset ι := f.ofLp.support ∪ g.ofLp.support ∪ h.ofLp.support
⊢ (∑ x ∈ s, edist (f.ofLp x) (h.ofLp x) ^ ↑p) ^ (1 / ↑p) ≤
    (∑ x ∈ s, edist (f.ofLp x) (g.ofLp x) ^ ↑p) ^ (1 / ↑p) + (∑ x ∈ s, edist (g.ofLp x) (h.ofLp x) ^ ↑p) ^ (1 / ↑p)
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
hu : IsUltrametricDist K
inst✝⁵ : CompleteSpace K
x : L
E : Type u_2
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : Algebra L E
inst✝¹ : IsScalarTower K L E
inst✝ : Algebra.IsAlgebraic K E
a : E
ha : (mapAlg K E) (minpoly K x) ≠ 0 ∧ eval a ((mapAlg K E) (minpoly K x)) = 0
⊢ (aeval a) (minpoly K ((algebraMap L E) x)) = 0

Tactic:
rw [← ha.2, mapAlg_eq_map, minpoly.algebraMap_eq (algebraMap L E).injective, aeval_def,
      eval_map]

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 + ↑P * (↑Pᶜ * ↑(Q ⊓ R)) + (↑R * ↑Pᶜ * ↑P + ↑Pᶜ * (↑(Q ⊓ R) * ↑R * ↑Pᶜ)) = ↑P + ↑Pᶜ * ↑(Q ⊓ R)

Tactic:
coe_inf Q,

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 * (↑Pᶜ * (↑Q * ↑R)) + (↑R * ↑Pᶜ * ↑P + ↑Pᶜ * (↑Q * ↑R * ↑R * ↑Pᶜ)) = ↑P + ↑Pᶜ * (↑Q * ↑R)
Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn

Goal state before:
pp: α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
R : Type u_3
inst✝⁴ : NormedCommRing R
inst✝³ : NormOneClass R
inst✝² : CompleteSpace R
inst✝¹ : TopologicalSpace α
f : ι → α → R
inst✝ : LocallyCompactSpace α
hK : IsOpen[inst✝¹] K
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
hcts : ∀ (i : ι), ContinuousOn (f i) K
S : Set α
hS : S ⊆ K
hC : IsCompact S
⊢ ∀ᶠ (i : ι) in cofinite, ∀ x ∈ S, ‖f i x‖ ≤ u i

Tactic:
filter_upwards [h] with i hi a ha using hi a (hS ha)

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : α → Type u_3
F : α → Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
inst✝³ : (i : α) → NormedSpace 𝕜 (E i)
inst✝² : (i : α) → NormedAddCommGroup (F i)
inst✝¹ : (i : α) → NormedSpace 𝕜 (F i)
p✝ q r p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
T : (i : α) → E i →L[𝕜] F i
K : ℝ
hK : 0 ≤ K
hTK : ∀ (i : α), ‖T i‖ ≤ K
key : ∀ (i : α) (x : E i), ‖(T i) x‖ ≤ K * ‖x‖
x : ↥(lp E p)
⊢ ‖{ toFun := fun x ↦ ⟨fun i ↦ (T i) (↑x i), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } x‖ ≤ K * ‖x‖

Tactic:
rw [← norm_toNorm]

Goal state after:
α : Type u_1
𝕜 : Type u_2
E : α → Type u_3
F : α → Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
inst✝³ : (i : α) → NormedSpace 𝕜 (E i)
inst✝² : (i : α) → NormedAddCommGroup (F i)
inst✝¹ : (i : α) → NormedSpace 𝕜 (F i)
p✝ q r p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
T : (i : α) → E i →L[𝕜] F i
K : ℝ
hK : 0 ≤ K
hTK : ∀ (i : α), ‖T i‖ ≤ K
key : ∀ (i : α) (x : E i), ‖(T i) x‖ ≤ K * ‖x‖
x : ↥(lp E p)
⊢ ‖toNorm ({ toFun := fun x ↦ ⟨fun i ↦ (T i) (↑x i), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } x)‖ ≤ K * ‖x‖
Module: Mathlib.Topology.Maps.Strict.Group

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁴ : Group G
inst✝³ : Group H
f : G →* H
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup G
⊢ IsStrictMap ⇑f ↔ IsOpenQuotientMap ⇑f.rangeRestrict

Tactic:
by
  rw [isOpenQuotientMap_iff_isQuotientMap]
  rfl

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

Goal state before:
pp: case h₁
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁷ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (F i)
p q : ℝ≥0∞
H : Type u_6
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : NormedSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fact (1 ≤ q)
inst✝ : p.HolderConjugate q
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] H
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
⊢ ‖ContinuousLinearMap.postcomp (↥(lp F q)) (tsumCLM 𝕜 ι H)‖ ≤ 1

pp: case h₂
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁷ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (F i)
p q : ℝ≥0∞
H : Type u_6
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : NormedSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fact (1 ≤ q)
inst✝ : p.HolderConjugate q
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] H
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
⊢ ‖holderL 1 B hBK‖ ≤ ↑K

Tactic:
· exact ContinuousLinearMap.norm_postcomp_le _ |>.trans norm_tsumCLM_le

Goal state after:
case h₂
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁷ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (F i)
p q : ℝ≥0∞
H : Type u_6
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : NormedSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fact (1 ≤ q)
inst✝ : p.HolderConjugate q
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] H
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
⊢ ‖holderL 1 B hBK‖ ≤ ↑K
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
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space E
inst✝ : T2Space F
u : E →L[𝕜] F
tfae_1_to_4 : u.IsFredholm → Nonempty u.FredholmPackage
tfae_4_to_2 : Nonempty u.FredholmPackage → ∃ v, (↑v).IsQuasiInverse ↑u
tfae_2_to_3 :
  (∃ v, (↑v).IsQuasiInverse ↑u) →
    ∃ E₁ F₁,
      IsClosed[inst✝⁸] ↑E₁ ∧
        IsClosed[inst✝⁷] ↑F₁ ∧ E₁.CoFG ∧ F₁.CoFG ∧ ∃ (h : MapsTo ⇑u ↑E₁ ↑F₁), (u.restrict h).IsInvertible
⊢ [u.IsFredholm, ∃ v, (↑v).IsQuasiInverse ↑u,
      ∃ E₁ F₁,
        IsClosed[inst✝⁸] ↑E₁ ∧
          IsClosed[inst✝⁷] ↑F₁ ∧ E₁.CoFG ∧ F₁.CoFG ∧ ∃ (h : MapsTo ⇑u ↑E₁ ↑F₁), (u.restrict h).IsInvertible,
      Nonempty u.FredholmPackage].TFAE

Tactic:
tfae_have 3 → 1 := by
    rintro ⟨E₁, F₁, E₁_closed, F₁_closed, E₁_coFG, F₁_coFG, u_mapsto, u_invertible⟩
    exact .of_isInvertible_restrict E₁_closed F₁_closed u_mapsto u_invertible

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
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space E
inst✝ : T2Space F
u : E →L[𝕜] F
tfae_1_to_4 : u.IsFredholm → Nonempty u.FredholmPackage
tfae_4_to_2 : Nonempty u.FredholmPackage → ∃ v, (↑v).IsQuasiInverse ↑u
tfae_2_to_3 :
  (∃ v, (↑v).IsQuasiInverse ↑u) →
    ∃ E₁ F₁,
      IsClosed[inst✝⁸] ↑E₁ ∧
        IsClosed[inst✝⁷] ↑F₁ ∧ E₁.CoFG ∧ F₁.CoFG ∧ ∃ (h : MapsTo ⇑u ↑E₁ ↑F₁), (u.restrict h).IsInvertible
tfae_3_to_1 :
  (∃ E₁ F₁,
      IsClosed[inst✝⁸] ↑E₁ ∧
        IsClosed[inst✝⁷] ↑F₁ ∧ E₁.CoFG ∧ F₁.CoFG ∧ ∃ (h : MapsTo ⇑u ↑E₁ ↑F₁), (u.restrict h).IsInvertible) →
    u.IsFredholm
⊢ [u.IsFredholm, ∃ v, (↑v).IsQuasiInverse ↑u,
      ∃ E₁ F₁,
        IsClosed[inst✝⁸] ↑E₁ ∧
          IsClosed[inst✝⁷] ↑F₁ ∧ E₁.CoFG ∧ F₁.CoFG ∧ ∃ (h : MapsTo ⇑u ↑E₁ ↑F₁), (u.restrict h).IsInvertible,
      Nonempty u.FredholmPackage].TFAE
Module: Mathlib.Analysis.Normed.Ring.InfiniteProd

Goal state before:
pp: α : Type u_1
R : Type u_2
β : Type u_3
inst✝² : NormedCommRing R
inst✝¹ : NormOneClass R
inst✝ : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ Tendsto (fun n ↦ ∏' (k : β), (1 + f n k)) 𝓕 (𝓝 (∏' (k : β), (1 + g k)))

Tactic:
rcases eq_or_neBot 𝓕 with rfl | _

Goal state after:
case inl
α : Type u_1
R : Type u_2
β : Type u_3
inst✝² : NormedCommRing R
inst✝¹ : NormOneClass R
inst✝ : CompleteSpace R
g : β → R
bound : β → ℝ
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) ⊥ (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in ⊥, ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ Tendsto (fun n ↦ ∏' (k : β), (1 + f n k)) ⊥ (𝓝 (∏' (k : β), (1 + g k)))

case inr
α : Type u_1
R : Type u_2
β : Type u_3
inst✝² : NormedCommRing R
inst✝¹ : NormOneClass R
inst✝ : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝ : 𝓕.NeBot
⊢ Tendsto (fun n ↦ ∏' (k : β), (1 + f n k)) 𝓕 (𝓝 (∏' (k : β), (1 + g k)))