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
⊢ c ≤ (t, u).1 → (t, u).1 • (t, u).2 +ᵥ p ∈ s → c • (t, u).2 +ᵥ p ∈ s

Tactic:
(ht : c ≤ t)

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
⊢ (t, u).1 • (t, u).2 +ᵥ p ∈ s → c • (t, u).2 +ᵥ p ∈ s
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: 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
p : ι → P
hp : AffineIndependent k p
s : Set ι
fs : ↑s → Finset ι
hfs : ∀ (i : ↑s), ↑i ∈ fs i
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
hp'' : ∀ (i : ↑s), ∃ r, (Finset.affineCombination k (fs i) p) ((AffineMap.lineMap (Pi.single (↑i) 1) (w i)) r) = p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs ⟨i', hi'⟩) p) ((AffineMap.lineMap (Pi.single (↑⟨i', hi'⟩) 1) (w ⟨i', hi'⟩)) ri') = p'
w' : ι → k := (AffineMap.lineMap (Pi.single i' 1) (w ⟨i', hi'⟩)) ri'
i : ↑s
r : k
hr : (Finset.affineCombination k (fs i) p) ((AffineMap.lineMap (Pi.single (↑i) 1) (w i)) r) = p'
⊢ ∀ (j : ι), r * (↑(fs i) \ {↑i}).indicator (w i) j = (↑(fs ⟨i', hi'⟩) \ {↑i}).indicator w' j

Tactic:
← hri'

Goal state after:
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
p : ι → P
hp : AffineIndependent k p
s : Set ι
fs : ↑s → Finset ι
hfs : ∀ (i : ↑s), ↑i ∈ fs i
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
hp'' : ∀ (i : ↑s), ∃ r, (Finset.affineCombination k (fs i) p) ((AffineMap.lineMap (Pi.single (↑i) 1) (w i)) r) = p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs ⟨i', hi'⟩) p) ((AffineMap.lineMap (Pi.single (↑⟨i', hi'⟩) 1) (w ⟨i', hi'⟩)) ri') = p'
w' : ι → k := (AffineMap.lineMap (Pi.single i' 1) (w ⟨i', hi'⟩)) ri'
i : ↑s
r : k
hr :
  (Finset.affineCombination k (fs i) p) ((AffineMap.lineMap (Pi.single (↑i) 1) (w i)) r) =
    (Finset.affineCombination k (fs ⟨i', hi'⟩) p) ((AffineMap.lineMap (Pi.single (↑⟨i', hi'⟩) 1) (w ⟨i', hi'⟩)) ri')
⊢ ∀ (j : ι), r * (↑(fs i) \ {↑i}).indicator (w i) j = (↑(fs ⟨i', hi'⟩) \ {↑i}).indicator w' j
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case inr
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✝ s : Set V
hs : Convex k s
hs' : IsClosed[inst✝²] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
⊢ 0 ≤ a → 0 ≤ b → a + b = 1 → a • v + b • u ∈ asymptoticCone k s

Tactic:
ha

Goal state after:
case inr
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✝ s : Set V
hs : Convex k s
hs' : IsClosed[inst✝²] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
⊢ 0 ≤ b → a + b = 1 → a • v + b • u ∈ asymptoticCone k s
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case inl.inr
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₄₃lt : i₄ < i₃
⊢ ⟨(i₁, i₂), h₁₂lt⟩ ≠ ⟨(i₄, i₃), h₄₃lt⟩

Tactic:
cases h₁₂₄₃ <;> simp [*]

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case 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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₃₄lt : i₃ < i₄
⊢ ⟨(i₂, i₁), h₂₁lt⟩ ≠ ⟨(i₃, i₄), h₃₄lt⟩

Tactic:
cases h₁₂₄₃ <;> simp [*]

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

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (fun x ↦ ‖f x‖) univ x
hf : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y : X
⊢ ∀ x ∈ {y | ‖f y‖ = M}, ∀ᶠ (y : X) in 𝓝 x, y ∈ {y | ‖f y‖ = M}

Tactic:
intro w hw

Goal state after:
X : Type u_1
E : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (fun x ↦ ‖f x‖) univ x
hf : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y w : X
hw : w ∈ {y | ‖f y‖ = M}
⊢ ∀ᶠ (y : X) in 𝓝 w, y ∈ {y | ‖f y‖ = M}
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 x_1) (cobounded (ℝ × ℝ)) (cobounded F)

Tactic:
φ,

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.Field.Ultra

Goal state before:
pp: case h.inr
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm✝ : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
hm : m ≠ 0
⊢ ‖x‖ ^ i ≤ 1

Tactic:
pow_le_one_iff_of_nonneg (norm_nonneg _) hm

Goal state after:
case h.inr
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm✝ : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
hm : m ≠ 0
⊢ ‖x‖ ^ i ≤ 1
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‖
this : Tendsto (fun y ↦ ‖y.1‖ * c) (cobounded ℝ ×ˢ ⊤) atTop
y : ℝ × ℝ
hy : y ∈ {0}ᶜ ×ˢ Set.univ
⊢ ‖y.1‖ * c ≤ ‖y.1 • x - (algebraMap ℝ F) y.2‖

Tactic:
calc ‖y.1‖ * c
        _ ≤ ‖y.1‖ * ‖x - algebraMap ℝ F (y.1⁻¹ * y.2)‖ := by gcongr; exact hbd _
        _ = ‖y.1 • x - algebraMap ℝ F y.2‖ := by
          simp only [← norm_smul, smul_sub, smul_smul, Algebra.algebraMap_eq_smul_one]
          simp_all

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

Goal state before:
pp: R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f✝ f f' : AlgebraNorm R S
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) f'
⊢ f = f'

Tactic:
simp only [AddGroupSeminorm.toFun_eq_coe, RingSeminorm.toFun_eq_coe] at h
    cases f; cases f'; congr
    simp only at h
    ext s
    erw [h]
    rfl

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : SeminormedCommRing R
S : Type u_2
inst✝⁵ : Ring S
inst✝⁴ : Algebra R S
f✝ : AlgebraNorm R S
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra A S
inst✝ : IsScalarTower R A S
hinj : Function.Injective ⇑(algebraMap A S)
f : AlgebraNorm R S
x : A
hx : f ((algebraMap A S) x) = 0
⊢ x = 0

Tactic:
rw [← map_eq_zero_iff (algebraMap A S) hinj]

Goal state after:
R : Type u_1
inst✝⁶ : SeminormedCommRing R
S : Type u_2
inst✝⁵ : Ring S
inst✝⁴ : Algebra R S
f✝ : AlgebraNorm R S
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra A S
inst✝ : IsScalarTower R A S
hinj : Function.Injective ⇑(algebraMap A S)
f : AlgebraNorm R S
x : A
hx : f ((algebraMap A S) x) = 0
⊢ (algebraMap A S) x = 0
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

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

Tactic:
obtain ⟨N, hN⟩ := hL2 δ hδ

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
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
f_neg : ∀ (x : R), f (-x) = f x
h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0
x : R
⊢ seminormFromBounded' f x = 0 ↔ x = 0

Tactic:
exact ⟨fun h ↦ h0 x h, fun h ↦ by rw [h]; exact seminormFromBounded_zero f_zero⟩

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

Goal state before:
pp: case a
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 := ⋯
this✝¹ : FiniteDimensional K ↥K⟮y⟯
this✝ : IsUltrametricDist L
y' : ↥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
⊢ IsConjRoot K x (z' + y)

Tactic:
apply IsConjRoot.of_isScalarTower (L := K⟮y⟯) xsep.isIntegral

Goal state after:
case a
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 := ⋯
this✝¹ : FiniteDimensional K ↥K⟮y⟯
this✝ : IsUltrametricDist L
y' : ↥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
⊢ IsConjRoot (↥K⟮y⟯) x (z' + y)
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'‖
⊢ x ∈ K⟮y⟯

Tactic:
by
    -- Reduce to the case `L = algebraic closure of K` to apply the previous lemma.
    let C := AlgebraicClosure K
    let : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
    let : NormedAlgebra K C := spectralNorm.normedAlgebra K C
    let iL : L →ₐ[K] C := IsAlgClosed.lift
    algebraize [iL.toRingHom]
    let : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
    let := IsKrasner.of_completeSpace_of_normal K C
    -- The norm on `L` is compatible with the norm on the algebraic closure of `K`,
    -- this gives the result.
    have norm_iL (x : L) : ‖iL x‖ = ‖x‖ := norm_algebraMap' _ _
    suffices this : iL x ∈ K⟮iL y⟯ by
      simpa [← Set.image_singleton, ← IntermediateField.adjoin_map] using! this
    refine IsKrasner.krasner ((xsep.map _ iL.injective).of_dvd dvd_rfl) ?_ (yint.map iL) ?_
    · exact Polynomial.Splits.of_dvd (sp.of_isScalarTower C)
        (Polynomial.map_ne_zero (minpoly.ne_zero xsep.isIntegral))
        (Polynomial.map_dvd _ (by simpa using! minpoly.dvd_map_of_isScalarTower' K K C x))
    · intros xC' hx' hne
      have : xC' ∈ (minpoly K x).rootSet C := by
        rwa [isConjRoot_iff_mem_minpoly_rootSet (xsep.isIntegral.map _),
          minpoly.algHom_eq iL iL.injective x] at hx'
      simp only [← sp.image_rootSet iL, Set.mem_image] at this
      obtain ⟨c, hc, rfl⟩ := this
      rw [← isConjRoot_iff_mem_minpoly_rootSet xsep.isIntegral] at hc
      simpa [norm_iL, ← map_sub] using! kr c hc (fun h ↦ (iff_false_intro hne).mp (congrArg iL h))

Goal state after:
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
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
⊢ limsup (fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a

Tactic:
ha

Goal state after:
case pos
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 (𝓝 0)
ha : a = 0
⊢ limsup (fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a
Module: Mathlib.Analysis.Normed.Group.ControlledClosure

Goal state before:
pp: G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : CompleteSpace G
H : Type u_2
inst✝¹ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), ‖j x‖ = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ g, f g = j k ∧ ‖g‖ ≤ C * ‖k‖
h : H
h_in : h ∈ j.range
⊢ ∃ g, f g = h ∧ ‖g‖ ≤ C * ‖h‖

Tactic:
rcases (j.mem_range _).mp h_in with ⟨k, rfl⟩

Goal state after:
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : CompleteSpace G
H : Type u_2
inst✝¹ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), ‖j x‖ = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ g, f g = j k ∧ ‖g‖ ≤ C * ‖k‖
k : K
h_in : j k ∈ j.range
⊢ ∃ g, f g = j k ∧ ‖g‖ ≤ C * ‖j k‖
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
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := fun n ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun n ↦ n - mu n
hnu : nu = fun n ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun n ↦ ↑(nu n) / ↑n) ∘ ψ) atTop (𝓝 b)
b_in : b ∈ Set.Icc 0 1
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx : limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a
hy : limsup (fun n ↦ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ y ^ b
hxy' :
  limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n)) * μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤
    limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n))) atTop * limsup (fun n ↦ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop
h_bdd : IsBoundedUnder LE.le atTop fun n ↦ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))
⊢ limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n)) * μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b

Tactic:
apply le_trans hxy' (mul_le_mul hx hy (le_limsup_of_frequently_le (Frequently.of_forall
      (fun n ↦ by positivity)) h_bdd) (rpow_nonneg (smoothingFun_nonneg μ hμ1 x) _))

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

Goal state before:
pp: R : Type u_1
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
⊢ SeminormedRing L

Tactic:
letI : NormedField L := normedField K L
  infer_instance

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

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

Tactic:
refine ⟨finv.comp ginv, fun x ↦ ?_⟩

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

Goal state before:
pp: R : Type u_7
E : Type u_8
F : Type u_10
inst✝⁸ : Ring R
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup F
inst✝² : Module R F
f : E →L[R] F
inst✝¹ : T1Space F
hf : f.HasLeftInverse
inst✝ : IsTopologicalAddGroup F
⊢ IsClosed (range ⇑↑f)

Tactic:
← f.coe_range,

Goal state after:
R : Type u_7
E : Type u_8
F : Type u_10
inst✝⁸ : Ring R
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup F
inst✝² : Module R F
f : E →L[R] F
inst✝¹ : T1Space F
hf : f.HasLeftInverse
inst✝ : IsTopologicalAddGroup F
⊢ IsClosed ↑(↑f).range
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

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

Tactic:
refine ⟨finv.comp ginv, fun x ↦ ?_⟩

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

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

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

Goal state after:
Module: Mathlib.Analysis.Normed.Module.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 : ι
hi : ∀ x ∈ K, ‖f i x‖ ≤ u i
a : α
⊢ a ∈ S → ‖f i a‖ ≤ u i

Tactic:
ha

Goal state after:
α : 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 : ι
hi : ∀ x ∈ K, ‖f i x‖ ≤ u i
a : α
ha : a ∈ S
⊢ ‖f i a‖ ≤ u i
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : 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)
p q r : ℝ≥0∞
hpqr✝ : p.HolderTriple q r
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fact (1 ≤ q)
inst✝ : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
e : ↥(lp E p)
f : ↥(lp F q)
hp✝ : 1 ≤ p.toReal
hq✝ : 1 ≤ q.toReal
hpqr : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p.toReal
hq : 0 < q.toReal
s : Finset ι
⊢ ↑K ^ r.toReal * (‖e‖ ^ p.toReal) ^ (r.toReal / p.toReal) * (‖f‖ ^ q.toReal) ^ (r.toReal / q.toReal) ≤
    (↑K * ‖e‖ * ‖f‖) ^ r.toReal

Tactic:
by
          rw [← Real.rpow_mul, ← Real.rpow_mul]
          · simp only [← mul_div_assoc, ne_eq, hp.ne', not_false_eq_true, mul_div_cancel_left₀,
            hq.ne', fieldLe]
            rw [Real.mul_rpow, Real.mul_rpow]
            all_goals positivity
          all_goals positivity

Goal state after: