mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : CommRing k
inst✝³ : NoZeroDivisors k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h✝ : Nontrivial k
w : ↑Set.univ → Fin 3 → k := fun i ↦ Finset.affineCombinationLineMapWeights (↑i + 1) (↑i + 2) (r ↑i)
hw : ∀ (i : ↑Set.univ), ∑ j, w i j = 1
w' : Fin (2 + 1) → k
hw' : ∑ j, w' j = 1
h : ∀ (i : ↑Set.univ), ∃ r, ∀ (j : Fin (2 + 1)), r * {↑i}ᶜ.indicator (w i) j = {↑i}ᶜ.indicator w' j
hp' :
  ∀ (i : Fin 3),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
hp'w :
  ∀ (i : ↑Set.univ),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points ↑i, (Finset.affineCombination k Finset.univ t.points) (w i)]
h' :
  ∀ (i : Fin 3), ∃ c, ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k := fun i ↦ ⋯.choose
hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
hc2 : ∀ (i : Fin 3), c i * r i = w' (i + 2)
hcr : (∏ i, c i) * ∏ i, r i = (∏ i, c i) * ∏ i, (1 - r i)
i : Fin 3
hi : c i = 0
hw'i1 : w' (i + 1) = 0
hw'i2 : w' (i + 2) = 0
hw'i0 : w' i = 1
hi1 : c (i + 1) * r (i + 1) = 1
hi1' : c (i + 1) * (1 - r (i + 1)) = 0
⊢ c (i + 1) = 1

Tactic:
suffices c (i + 1) * (r (i + 1) + (1 - r (i + 1))) = 1 + 0 by simpa using this

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : CommRing k
inst✝³ : NoZeroDivisors k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h✝ : Nontrivial k
w : ↑Set.univ → Fin 3 → k := fun i ↦ Finset.affineCombinationLineMapWeights (↑i + 1) (↑i + 2) (r ↑i)
hw : ∀ (i : ↑Set.univ), ∑ j, w i j = 1
w' : Fin (2 + 1) → k
hw' : ∑ j, w' j = 1
h : ∀ (i : ↑Set.univ), ∃ r, ∀ (j : Fin (2 + 1)), r * {↑i}ᶜ.indicator (w i) j = {↑i}ᶜ.indicator w' j
hp' :
  ∀ (i : Fin 3),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
hp'w :
  ∀ (i : ↑Set.univ),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points ↑i, (Finset.affineCombination k Finset.univ t.points) (w i)]
h' :
  ∀ (i : Fin 3), ∃ c, ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k := fun i ↦ ⋯.choose
hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
hc2 : ∀ (i : Fin 3), c i * r i = w' (i + 2)
hcr : (∏ i, c i) * ∏ i, r i = (∏ i, c i) * ∏ i, (1 - r i)
i : Fin 3
hi : c i = 0
hw'i1 : w' (i + 1) = 0
hw'i2 : w' (i + 2) = 0
hw'i0 : w' i = 1
hi1 : c (i + 1) * r (i + 1) = 1
hi1' : c (i + 1) * (1 - r (i + 1)) = 0
⊢ c (i + 1) * (r (i + 1) + (1 - r (i + 1))) = 1 + 0
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: z w : ℂ
⊢ ↑(z + w) = ↑z + ↑w

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: z w : ℂ
⊢ ↑(z * w) = ↑z * ↑w

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: r : ℝ
z : ℂ
⊢ r • ↑z = ↑r * ↑z

Tactic:
ext <;> simp

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 =
    0 * I / 2 +
      ((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:
zero_mul,

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 =
    0 / 2 +
      ((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.Unbundled.AlgebraNorm

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

Tactic:
lia

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_zero : f 0 = 0
⊢ ⨆ y, f (0 * y) / f y = 0

Tactic:
zero_mul,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_zero : f 0 = 0
⊢ ⨆ y, f 0 / f y = 0
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
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f = 0
⊢ 0 ≤ ⨆ y, 0 * 0

Tactic:
zero_mul,

Goal state after:
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
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f = 0
⊢ 0 ≤ ⨆ y, 0
Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful

Goal state before:
pp: case h
F : Type u_1
α : Type u_2
inst✝³ : Ring α
inst✝² : FunLike F α ℝ
inst✝¹ : RingSeminormClass F α ℝ
β : Type u_3
inst✝ : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ (f x) ≤ C * nα x
hlim : Tendsto (fun n ↦ C ^ (1 / ↑n) * nα x) atTop (𝓝 (nα x))
n : ℕ
hn : 1 ≤ n
h : (C ^ (1 / ↑n)) ^ n = C
⊢ C * nα (x ^ n) ≤ C * nα x ^ n

Tactic:
mul_le_mul_iff_right₀ hC0

Goal state after:
case h
F : Type u_1
α : Type u_2
inst✝³ : Ring α
inst✝² : FunLike F α ℝ
inst✝¹ : RingSeminormClass F α ℝ
β : Type u_3
inst✝ : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ (f x) ≤ C * nα x
hlim : Tendsto (fun n ↦ C ^ (1 / ↑n) * nα x) atTop (𝓝 (nα x))
n : ℕ
hn : 1 ≤ n
h : (C ^ (1 / ↑n)) ^ n = C
⊢ nα (x ^ n) ≤ nα x ^ n
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf : f 0 = 0
n : ℕ
⊢ f (0 * c ^ n) / f c ^ n = 0 n

Tactic:
zero_mul,

Goal state after:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf : f 0 = 0
n : ℕ
⊢ f 0 / f c ^ n = 0 n
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x y : R
n : ℕ
⊢ n ≤ 2 * n

Tactic:
lia

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

Goal state before:
pp: case h
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
n : ℕ
⊢ n ≤ n + 1

Tactic:
lia

Goal state after:
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✝ : Algebra.IsAlgebraic 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'‖
C : Type u_1 := AlgebraicClosure K
this✝² : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this✝¹ : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst✝ : Algebra L C := iL.toAlgebra
this✝ : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := of_completeSpace_of_normal K C
⊢ x ∈ K⟮y⟯

Tactic:
have norm_iL (x : L) : ‖iL x‖ = ‖x‖ := norm_algebraMap' _ _

Goal state after:
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✝ : Algebra.IsAlgebraic 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'‖
C : Type u_1 := AlgebraicClosure K
this✝² : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this✝¹ : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst✝ : Algebra L C := iL.toAlgebra
this✝ : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := of_completeSpace_of_normal K C
norm_iL : ∀ (x : L), ‖iL x‖ = ‖x‖
⊢ x ∈ K⟮y⟯
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case pos
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
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬μ (x ^ (n % ↑m1)) = 0
hxn' : 0 < μ (x ^ (n % ↑m1))
h : μ (x ^ (↑m1 * (n / ↑m1))) ^ (1 / ↑n) ≤ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n)
hL0' : 0 < L + ε / 2
h1 : (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))
hnm1 : n % ↑m1 = 0
⊢ μ (x ^ (n % ↑m1)) ^ (1 / ↑n) ≤ (μ x ^ (n % ↑m1)) ^ (1 / ↑n)

Tactic:
simpa [hnm1, pow_zero] using rpow_le_rpow (apply_nonneg μ _) hμ1 (one_div_cast_nonneg _)

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

Goal state before:
pp: R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
⊢ spectralValue P ≤ 1 ↔ ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1

Tactic:
rw [spectralValue]
  refine ⟨fun h n ↦ ?_, fun h ↦ ?_⟩
  · obtain hPn | hPn | hPn := lt_trichotomy P.natDegree n
    · simp [coeff_eq_zero_of_natDegree_lt hPn]
    · rw [← hPn, hP.coeff_natDegree, norm_one]
    · have : spectralValueTerms P n ≤ 1 := le_ciSup (spectralValueTerms_bddAbove P) n |>.trans h
      contrapose! this
      simp only [spectralValueTerms_of_lt_natDegree _ hPn]
      exact Real.one_lt_rpow this (by simp [hPn])
  · apply ciSup_le (fun n ↦ ?_)
    rw [spectralValueTerms]
    split_ifs with hn
    · apply Real.rpow_le_one (norm_nonneg _) (h n)
      rw [one_div_nonneg, sub_nonneg, Nat.cast_le]
      exact le_of_lt hn
    · exact zero_le_one

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
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
n : ℕ
hn : n < p.natDegree
hexp : (‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n))) ^ (p.natDegree - n) = ‖p.coeff n‖
h_base : ‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n)) < f x
⊢ ‖p.coeff n‖ < f x ^ (p.natDegree - n)

Tactic:
← hexp,

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
n : ℕ
hn : n < p.natDegree
hexp : (‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n))) ^ (p.natDegree - n) = ‖p.coeff n‖
h_base : ‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n)) < f x
⊢ (‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n))) ^ (p.natDegree - n) < f x ^ (p.natDegree - n)
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
n : ℕ
hn : 1 ≤ n
⊢ μ 1 ^ (1 / ↑n) ≤ 1

Tactic:
conv_rhs => rw [← one_rpow (1 / n : ℝ)]

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
n : ℕ
hn : 1 ≤ n
⊢ μ 1 ^ (1 / ↑n) ≤ 1 ^ (1 / ↑n)
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 (((mapAlg K L) p).coeff m)

Tactic:
mapAlg_eq_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 ((Polynomial.map (algebraMap K L) p).coeff m)
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
h : (fun n ↦ 1 / ↑(s (ψ n)) * ↑(s (ψ n))) =ᶠ[atTop] 1
⊢ (fun n ↦ (μ (x ^ s (ψ n)) ^ (1 / ↑(s (ψ n)))) ^ (↑(s (ψ n)) / ↑(ψ n))) =ᶠ[atTop] fun n ↦
    μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))

Tactic:
simp_rw [← rpow_mul (apply_nonneg μ _), mul_div]

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 a)
ha : ¬a = 0
ha_pos : 0 < a
h : (fun n ↦ 1 / ↑(s (ψ n)) * ↑(s (ψ n))) =ᶠ[atTop] 1
⊢ (fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(s (ψ n)) * ↑(s (ψ n)) / ↑(ψ n))) =ᶠ[atTop] fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))
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
x : L
hx_alg : IsAlgebraic K x
⊢ (aeval x) (minpoly K x) = 0

Tactic:
by rw [minpoly.aeval]

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

Goal state before:
pp: K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
x y : L
⊢ (spectralAlgNorm K L) (x * y) = (spectralAlgNorm K L) x * (spectralAlgNorm K L) y

Tactic:
by_cases hx : x = 0
  · simp [hx, zero_mul, map_zero]
  · have hx' : spectralAlgNorm K L x ≠ 0 :=
      ne_of_gt (spectralNorm_zero_lt hx (Algebra.IsAlgebraic.isAlgebraic x))
    have hf1 : (spectralAlgNorm K L) 1 ≤ 1 := le_of_eq spectralAlgNorm_one
    set f : AlgebraNorm K L := algNormFromConst hf1 hx with hf
    have hf_pow : IsPowMul f := seminormFromConst_isPowMul hf1 hx' isPowMul_spectralNorm
    rw [← spectralNorm_unique hf_pow, hf]
    exact seminormFromConst_const_mul hf1 hx' isPowMul_spectralNorm _

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

Goal state before:
pp: K : Type u
inst✝⁸ : NontriviallyNormedField K
L : Type v
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
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)) = eval a ((mapAlg K E) (minpoly K x))

Tactic:
mapAlg_eq_map,

Goal state after:
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)) = eval a (Polynomial.map (algebraMap K E) (minpoly K x))
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✝¹ : IsSplittingField L E ((mapAlg K L) (minpoly K x))
inst✝ : Algebra.IsAlgebraic K E
⊢ (minpoly K x).natDegree = ((mapAlg K E) (minpoly K x)).natDegree

Tactic:
mapAlg_eq_map,

Goal state after:
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✝¹ : IsSplittingField L E ((mapAlg K L) (minpoly K x))
inst✝ : Algebra.IsAlgebraic K E
⊢ (minpoly K x).natDegree = (Polynomial.map (algebraMap K E) (minpoly K x)).natDegree
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 * ↑R) + (↑R * 0 + ↑Pᶜ * (↑Q * (↑R * ↑R) * ↑Pᶜ)) = ↑P + ↑Pᶜ * (↑Q * ↑R)

Tactic:
zero_mul,

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

Tactic:
zero_mul,

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁶] ↑A
inst✝ : A.CoFG
h_ker : Disjoint (↑u).ker A
h_range : (↑u).range = ⊤
⊢ IsStrictMap ⇑u → IsClosed[inst✝³] ↑(↑(u.domRestrict A)).range

Tactic:
intro u_strict

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁶] ↑A
inst✝ : A.CoFG
h_ker : Disjoint (↑u).ker A
h_range : (↑u).range = ⊤
u_strict : IsStrictMap ⇑u
⊢ IsClosed[inst✝³] ↑(↑(u.domRestrict A)).range
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: case refine_2
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
z : ι → ℝ
hz : ‖x + const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
hxy : ‖(x - y) i‖ ≤ δ / 4
⊢ y i < z i

Tactic:
replace hz := (norm_le_pi_norm _ i).trans hz

Goal state after:
case refine_2
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
z : ι → ℝ
i : ι
hxy : ‖(x - y) i‖ ≤ δ / 4
hz : ‖(x + const ι (3 / 4 * δ) - z) i‖ ≤ δ / 4
⊢ y i < z i
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: case refine_2
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
z : ι → ℝ
hz : ‖x - const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
hxy : ‖(x - y) i‖ ≤ δ / 4
⊢ z i < y i

Tactic:
replace hz := (norm_le_pi_norm _ i).trans hz

Goal state after:
case refine_2
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
z : ι → ℝ
i : ι
hxy : ‖(x - y) i‖ ≤ δ / 4
hz : ‖(x - const ι (3 / 4 * δ) - z) i‖ ≤ δ / 4
⊢ z i < y i
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'
⊢ s ∈ 𝓝 t

Tactic:
rw [mem_nhds_iff]

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'
⊢ ∃ t_1 ⊆ s, IsOpen t_1 ∧ t ∈ t_1
Module: Mathlib.Analysis.ODE.Gronwall

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

pp: case neg
δ K x : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K 0 x = δ * rexp (K * x)

Tactic:
· simp only [gronwallBound_K0, hK, zero_mul, exp_zero, add_zero, mul_one]

Goal state after:
case neg
δ K x : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K 0 x = δ * rexp (K * x)
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : dist (f a) (g a) ≤ δ
⊢ ∀ t ∈ Icc a b, dist (f t) (g t) ≤ δ * rexp (↑K * (t - a))

Tactic:
have f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0 := by intros; rw [dist_self]
  have g_bound : ∀ t ∈ Ico a b, dist (v t (g t)) (v t (g t)) ≤ 0 := by intros; rw [dist_self]
  intro t ht
  have :=
    dist_le_of_approx_trajectories_ODE_of_mem hv hf hf' f_bound hfs hg hg' g_bound hgs ha t ht
  rwa [zero_add, gronwallBound_ε0] at this

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : f a = g a
t : ℝ
ht : t ∈ Icc a b
this : dist (f t) (g t) ≤ 0 * Real.exp (↑K * (t - a))
⊢ f t = g t

Tactic:
zero_mul,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : f a = g a
t : ℝ
ht : t ∈ Icc a b
this : dist (f t) (g t) ≤ 0
⊢ f t = g t