mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Affine.MazurUlam

Goal state before:
pp: E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  ((f.trans (pointReflection ℝ (midpoint ℝ (f x) (f y))).toIsometryEquiv).trans f.symm).trans
    (pointReflection ℝ (midpoint ℝ x y)).toIsometryEquiv
hx : e x = x
hy : e y = y
hm :
  (pointReflection ℝ (midpoint ℝ x y)).toIsometryEquiv
      (f.symm ((pointReflection ℝ (midpoint ℝ (f x) (f y))).toIsometryEquiv (f (midpoint ℝ x y)))) =
    midpoint ℝ x y
⊢ f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)

Tactic:
← eq_symm_apply,

Goal state after:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  ((f.trans (pointReflection ℝ (midpoint ℝ (f x) (f y))).toIsometryEquiv).trans f.symm).trans
    (pointReflection ℝ (midpoint ℝ x y)).toIsometryEquiv
hx : e x = x
hy : e y = y
hm :
  f.symm ((pointReflection ℝ (midpoint ℝ (f x) (f y))).toIsometryEquiv (f (midpoint ℝ x y))) =
    (pointReflection ℝ (midpoint ℝ x y)).toIsometryEquiv.symm (midpoint ℝ x y)
⊢ f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k Finset.univ p) (w i)]
w'' : ι → k
fs'' : Finset ι
hw'' : ∑ j ∈ fs'', w'' j = 1
hw''p' : (Finset.affineCombination k fs'' p) w'' = p'
hi : ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑Finset.univ \ {↑i}).indicator (w i) j = (↑fs'' \ {↑i}).indicator w'' j
⊢ ∃ w',
    ∑ j, w' j = 1 ∧
      (Finset.affineCombination k Finset.univ p) w' = p' ∧
        ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * {↑i}ᶜ.indicator (w i) j = {↑i}ᶜ.indicator w' j

Tactic:
refine ⟨Set.indicator fs'' w'', ?_, ?_, ?_⟩

Goal state after:
case refine_1
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k Finset.univ p) (w i)]
w'' : ι → k
fs'' : Finset ι
hw'' : ∑ j ∈ fs'', w'' j = 1
hw''p' : (Finset.affineCombination k fs'' p) w'' = p'
hi : ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑Finset.univ \ {↑i}).indicator (w i) j = (↑fs'' \ {↑i}).indicator w'' j
⊢ ∑ j, (↑fs'').indicator w'' j = 1

case refine_2
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k Finset.univ p) (w i)]
w'' : ι → k
fs'' : Finset ι
hw'' : ∑ j ∈ fs'', w'' j = 1
hw''p' : (Finset.affineCombination k fs'' p) w'' = p'
hi : ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑Finset.univ \ {↑i}).indicator (w i) j = (↑fs'' \ {↑i}).indicator w'' j
⊢ (Finset.affineCombination k Finset.univ p) ((↑fs'').indicator w'') = p'

case refine_3
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k Finset.univ p) (w i)]
w'' : ι → k
fs'' : Finset ι
hw'' : ∑ j ∈ fs'', w'' j = 1
hw''p' : (Finset.affineCombination k fs'' p) w'' = p'
hi : ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑Finset.univ \ {↑i}).indicator (w i) j = (↑fs'' \ {↑i}).indicator w'' j
⊢ ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * {↑i}ᶜ.indicator (w i) j = {↑i}ᶜ.indicator ((↑fs'').indicator w'') j
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁶ : Field 𝕜
inst✝¹⁵ : CharZero 𝕜
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Algebra 𝕜 R
inst✝¹¹ : Module 𝕜 M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower 𝕜 R M
inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : IsTopologicalRing R
inst✝² : IsTopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
e : R
h : HasSum (fun n ↦ (expSeries 𝕜 R n) fun x_1 ↦ x.fst) e
⊢ HasSum (fun n ↦ (expSeries 𝕜 (tsze R M) n) fun x_1 ↦ x) (inl e + inr (e • x.snd))

Tactic:
have : HasSum (fun n => fst (expSeries 𝕜 (tsze R M) n fun _ => x)) e := by
    simpa [fst_expSeries] using h
  simpa only [inl_fst_add_inr_snd_eq] using
    (hasSum_inl _ <| this).add (hasSum_inr _ <| hasSum_snd_expSeries_of_smul_comm 𝕜 x hx h)

Goal state after:
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
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ ‖(r₁, m₁) * (r₂, m₂)‖ ≤ ‖(r₁, m₁)‖ * ‖(r₂, m₂)‖

Tactic:
simp_rw [norm_def]
    calc ‖r₁ * r₂‖ + ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖
    _ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) := by
      gcongr
      · apply norm_mul_le
      · refine norm_add_le_of_le ?_ ?_ <;>
        apply norm_smul_le
    _ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) + (‖m₁‖ * ‖m₂‖) := by
      apply le_add_of_nonneg_right
      positivity
    _ = (‖r₁‖ + ‖m₁‖) * (‖r₂‖ + ‖m₂‖) := by ring

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

Goal state before:
pp: 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‖) univ z
H : ∀ (z' : ℂ), ‖x - (algebraMap ℂ F) z'‖ ≠ 0
c : ℂ
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hMdef : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
y w : ℂ
hy : ‖x - (algebraMap ℂ F) y‖ = M
n : ℕ
hn : n > 0
p : ℂ[X]
hp : p.IsMonicOfDegree (n - 1)
hrel : X ^ n = p * (X - C (w - y)) + C (w - y) ^ n
⊢ ‖x - (algebraMap ℂ F) w‖ * ‖(aeval (x - (algebraMap ℂ F) y)) p‖ ≤ M ^ n + ‖w - y‖ ^ n

Tactic:
eq_comm,

Goal state after:
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‖) univ z
H : ∀ (z' : ℂ), ‖x - (algebraMap ℂ F) z'‖ ≠ 0
c : ℂ
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hMdef : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
y w : ℂ
hy : ‖x - (algebraMap ℂ F) y‖ = M
n : ℕ
hn : n > 0
p : ℂ[X]
hp : p.IsMonicOfDegree (n - 1)
hrel : p * (X - C (w - y)) + C (w - y) ^ n = X ^ n
⊢ ‖x - (algebraMap ℂ F) w‖ * ‖(aeval (x - (algebraMap ℂ F) y)) p‖ ≤ M ^ n + ‖w - y‖ ^ n
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝⁴ : NormedRing F
inst✝³ : NormOneClass F
inst✝² : NormMulClass F
inst✝¹ : NormedAlgebra ℂ F
inst✝ : Nontrivial F
x : F
z : ℂ
hz : x = (algebraMap ℂ F) z
⊢ (ofId ℂ F) z = x

Tactic:
eq_comm,

Goal state after:
F : Type u_1
inst✝⁴ : NormedRing F
inst✝³ : NormOneClass F
inst✝² : NormMulClass F
inst✝¹ : NormedAlgebra ℂ F
inst✝ : Nontrivial F
x : F
z : ℂ
hz : (algebraMap ℂ F) z = x
⊢ (ofId ℂ F) z = x
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
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * (n - 1))
hrel : q w ^ n - (q w - q u) ^ n = p * q u
⊢ ‖φ x u‖ * ‖(aeval x) p‖ ≤ M ^ n + ‖φ x u - φ x w‖ ^ n

Tactic:
eq_comm,

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
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * (n - 1))
hrel : p * q u = q w ^ n - (q w - q u) ^ n
⊢ ‖φ x u‖ * ‖(aeval x) p‖ ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
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
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * (n - 1))
hrel : ‖(aeval x) (q u * p)‖ = ‖(aeval x) (q w ^ n - (q w - q u) ^ n)‖
⊢ ‖φ x u‖ * ‖(aeval x) p‖ ≤ M ^ n + ‖φ x u - φ x w‖ ^ n

Tactic:
rw [map_mul, norm_mul, map_sub, aeval_eq_φ x u] at hrel

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
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * (n - 1))
hrel : ‖φ x u‖ * ‖(aeval x) p‖ = ‖(aeval x) (q w ^ n) - (aeval x) ((q w - q u) ^ n)‖
⊢ ‖φ x u‖ * ‖(aeval x) p‖ ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case inl
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
u : ℝ
hu : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℝ F) x_1‖) univ u
hc₀ : 0 = ‖x - (algebraMap ℝ F) u‖
⊢ ∃ z, IsMinOn (fun x_1 ↦ ‖φ x x_1‖) univ z

Tactic:
eq_comm,

Goal state after:
case inl
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
u : ℝ
hu : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℝ F) x_1‖) univ u
hc₀ : ‖x - (algebraMap ℝ F) u‖ = 0
⊢ ∃ z, IsMinOn (fun x_1 ↦ ‖φ x x_1‖) univ z
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
⊢ f x ≤ f 1 * seminormFromBounded' f x

Tactic:
by
  by_cases h1 : f 1 = 0
  · specialize f_mul x 1
    rw [mul_one, h1, mul_zero] at f_mul
    have hx0 : f x = 0 := f_mul.antisymm (f_nonneg _)
    rw [hx0, h1, zero_mul]
  · rw [mul_comm, ← div_le_iff₀ (lt_of_le_of_ne' (f_nonneg _) h1)]
    conv_lhs => rw [← mul_one x]
    exact le_ciSup (seminormFromBounded_bddAbove_range f_nonneg f_mul x) (1 : R)

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

Goal state before:
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
y : R
⊢ y ∈ Set.univ → y ≤ x

Tactic:
simp only [Set.mem_univ, hx y, implies_true]

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

Goal state before:
pp: ι : 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
a x : R
hx : ∀ (a : R), x ≤ a
y : R
⊢ y ∈ Set.univ → x ≤ y

Tactic:
simp only [Set.mem_univ, hx y, implies_true]

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
⊢ seminormFromBounded' f 1 ≤ 1

Tactic:
by
  by_cases! f_ne_zero : f ≠ 0
  · exact le_of_eq (seminormFromBounded_one f_ne_zero f_nonneg f_mul)
  · simp_rw [seminormFromBounded', one_mul]
    refine ciSup_le (fun _ ↦ ?_)
    simp only [f_ne_zero, Pi.zero_apply, div_zero, zero_le_one]

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
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
x y z : R
hz : ¬f z = 0
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z

Tactic:
rw [← add_div, div_le_div_iff_of_pos_right (lt_of_le_of_ne' (f_nonneg _) hz), add_mul]
    exact f_add _ _

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✝¹ : Field L
inst✝ : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean norm
h1 : LinearIndepOn K id {1}
ι : Type u_2 := { x // x ∈ h1.extend ⋯ }
B : Basis ι K L := Basis.extend h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex B
hem : Nonempty ι
h1L : 1 ∈ h1.extend ⋯
hB1 : B ⟨1, h1L⟩ = 1
g : L → ℝ := B.norm
hg0 : g 0 = 0
x : L
⊢ 0 ≤ g x

Tactic:
simp only [g, Basis.norm]

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : NormedField K
inst✝¹ : Field L
inst✝ : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean norm
h1 : LinearIndepOn K id {1}
ι : Type u_2 := { x // x ∈ h1.extend ⋯ }
B : Basis ι K L := Basis.extend h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex B
hem : Nonempty ι
h1L : 1 ∈ h1.extend ⋯
hB1 : B ⟨1, h1L⟩ = 1
g : L → ℝ := B.norm
hg0 : g 0 = 0
x : L
⊢ 0 ≤ univ.sup' ⋯ fun i ↦ ‖(B.repr x) i‖
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
⊢ Tendsto (seminormFromConst_seq c f 0) atTop (𝓝 0)

Tactic:
simpa [seminormFromConst_seq_zero c (map_zero _)] using! tendsto_const_nhds

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✝¹ : Field L
inst✝ : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean norm
h1 : LinearIndepOn K id {1}
ι : Type u_2 := { x // x ∈ h1.extend ⋯ }
B : Basis ι K L := Basis.extend h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex B
hem : Nonempty ι
h1L : 1 ∈ h1.extend ⋯
hB1 : B ⟨1, h1L⟩ = 1
g : L → ℝ := B.norm
hg0 : g 0 = 0
hg_nonneg : ∀ (x : L), 0 ≤ g x
hg_ext : ∀ (x : K), g ((algebraMap K L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g b
hg_neg : ∀ (a : L), g (-a) = g a
w✝¹ : ℝ
w✝ : 0 < w✝¹
hg_bdd : ∀ (x y : L), B.norm (x * y) ≤ w✝¹ * B.norm x * B.norm y
hg_mul : ∀ (k : K) (y : L), g ((algebraMap K L) k * y) = g ((algebraMap K L) k) * g y
f : RingSeminorm L := seminormFromBounded hg0 hg_nonneg hg_bdd hg_add hg_neg
hf_na : IsNonarchimedean ⇑f
hf_1 : f 1 ≤ 1
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
F' : RingSeminorm L := smoothingSeminorm f hf_1 hf_na
hF' : F' = smoothingSeminorm f hf_1 hf_na
hF'_ext : ∀ (k : K), F' ((algebraMap K L) k) = ‖k‖
hF'_1 : F' 1 = 1
hF'_0 : F' ≠ 0
k : K
y : L
hk : ∀ (y : L), f ((algebraMap K L) k * y) = f ((algebraMap K L) k) * f y
⊢ f ((algebraMap K L) k) = (smoothingSeminorm f hf_1 hf_na) ((algebraMap K L) k)

Tactic:
eq_comm,

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : NormedField K
inst✝¹ : Field L
inst✝ : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean norm
h1 : LinearIndepOn K id {1}
ι : Type u_2 := { x // x ∈ h1.extend ⋯ }
B : Basis ι K L := Basis.extend h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex B
hem : Nonempty ι
h1L : 1 ∈ h1.extend ⋯
hB1 : B ⟨1, h1L⟩ = 1
g : L → ℝ := B.norm
hg0 : g 0 = 0
hg_nonneg : ∀ (x : L), 0 ≤ g x
hg_ext : ∀ (x : K), g ((algebraMap K L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g b
hg_neg : ∀ (a : L), g (-a) = g a
w✝¹ : ℝ
w✝ : 0 < w✝¹
hg_bdd : ∀ (x y : L), B.norm (x * y) ≤ w✝¹ * B.norm x * B.norm y
hg_mul : ∀ (k : K) (y : L), g ((algebraMap K L) k * y) = g ((algebraMap K L) k) * g y
f : RingSeminorm L := seminormFromBounded hg0 hg_nonneg hg_bdd hg_add hg_neg
hf_na : IsNonarchimedean ⇑f
hf_1 : f 1 ≤ 1
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
F' : RingSeminorm L := smoothingSeminorm f hf_1 hf_na
hF' : F' = smoothingSeminorm f hf_1 hf_na
hF'_ext : ∀ (k : K), F' ((algebraMap K L) k) = ‖k‖
hF'_1 : F' 1 = 1
hF'_0 : F' ≠ 0
k : K
y : L
hk : ∀ (y : L), f ((algebraMap K L) k * y) = f ((algebraMap K L) k) * f y
⊢ (smoothingSeminorm f hf_1 hf_na) ((algebraMap K L) k) = f ((algebraMap K L) k)
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
⊢ ‖x - y‖ < ‖x - (z' + y)‖

Tactic:
apply kr (z' + y)
          · apply IsConjRoot.of_isScalarTower (L := K⟮y⟯) xsep.isIntegral
            simpa [z, y'] using IsConjRoot.add_algebraMap y' h1
          · simpa [z, sub_eq_iff_eq_add] using hne

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1
n : ℕ
hn : ¬n < P.natDegree
⊢ 0 ≤ 1

Tactic:
· exact zero_le_one

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

Goal state before:
pp: case neg.refine_1
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)
this : ⇑f ∘ s = fun n ↦ ∑ k ∈ range (n + 1), v k
⊢ f g = h

Tactic:
rw [← this] at lim_v

Goal state after:
case neg.refine_1
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
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
lim_v : Tendsto (⇑f ∘ s) atTop (𝓝 h)
this✝ : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
this : ⇑f ∘ s = fun n ↦ ∑ k ∈ range (n + 1), v k
⊢ f g = h
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 = spectralValue (minpoly K y)

Tactic:
eq_comm,

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
⊢ ¬spectralValue (minpoly K y) = 0
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
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
x : L
E : Type v := id ↥K⟮x⟯
this✝ : Field E :=
  id
    (have this := inferInstance;
    this)
this : Module K E :=
  id
    (have this := inferInstance;
    this)
id1 : ↥K⟮x⟯ →ₗ[K] E := LinearMap.id
id2 : E →ₗ[K] ↥K⟮x⟯ := LinearMap.id
hs_norm : RingNorm E :=
  { toFun := fun y ↦ spectralNorm K L ↑(id2 y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯,
    eq_zero_of_map_eq_zero' := ⋯ }
n1 : NormedRing E := hs_norm.toNormedRing
N1 : NormedSpace K E :=
  { toSMul := DistribMulAction.toDistribSMul.toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯, norm_smul_le := ⋯ }
a : ↥K⟮x⟯
ha : f ((algebraMap (↥K⟮x⟯) L) a) = 0
⊢ a = 0

Tactic:
simpa [map_eq_zero_iff_eq_zero, map_eq_zero] using! ha

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
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✝¹ : Nonempty β
h✝ : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable fun x ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
⊢ ∃ T, dist (∑ b ∈ T, bound b) S < ε / 3

Tactic:
rw [HasSum, Metric.tendsto_nhds] at hS

Goal state after:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
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✝¹ : Nonempty β
h✝ : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable fun x ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : ∀ ε > 0, ∀ᶠ (x : Finset β) in (SummationFilter.unconditional β).filter, dist (∑ b ∈ x, bound b) S < ε
⊢ ∃ T, dist (∑ b ∈ T, bound b) S < ε / 3
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
f : AbsoluteValue L ℝ
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
x : L
g : AlgebraNorm K L :=
  let __src := MulRingNorm.mulRingNormEquivAbsoluteValue.invFun f;
  { toAddGroupSeminorm := __src.toAddGroupSeminorm, mul_le' := ⋯, eq_zero_of_map_eq_zero' := ⋯, smul' := ⋯ }
hg_pow : IsPowMul ⇑g
hgx : f x = g x
⊢ f x = spectralNorm K L x

Tactic:
rw [hgx, spectralNorm_unique hg_pow, spectralAlgNorm_def]

Goal state after: