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

Goal state before:
pp: 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 = ∑ j ∈ fs'', w'' j

Tactic:
exact Finset.sum_indicator_subset _ (by simp)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
k : ℤ
⊢ ↑π * s ≠ ↑k * ↑π

Tactic:
apply_fun im

Goal state after:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
k : ℤ
⊢ (↑π * s).im ≠ (↑k * ↑π).im
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
k : ℤ
⊢ π * s.im ≠ (↑k * ↑π).im

Tactic:
← ofReal_intCast,

Goal state after:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
k : ℤ
⊢ π * s.im ≠ (↑↑k * ↑π).im
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : AddCommGroup M
inst✝¹³ : Algebra ℚ R
inst✝¹² : Module ℚ M
inst✝¹¹ : Module R M
inst✝¹⁰ : Module Rᵐᵒᵖ M
inst✝⁹ : IsCentralScalar R M
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : IsTopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : T2Space R
inst✝¹ : T2Space M
x : tsze R M
inst✝ : Invertible x.fst
⊢ x = x.fst • inl 1 + x.fst • inr (⅟x.fst • x.snd)

Tactic:
← inl_smul,

Goal state after:
R : Type u_3
M : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : AddCommGroup M
inst✝¹³ : Algebra ℚ R
inst✝¹² : Module ℚ M
inst✝¹¹ : Module R M
inst✝¹⁰ : Module Rᵐᵒᵖ M
inst✝⁹ : IsCentralScalar R M
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : IsTopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : T2Space R
inst✝¹ : T2Space M
x : tsze R M
inst✝ : Invertible x.fst
⊢ x = inl (x.fst • 1) + x.fst • inr (⅟x.fst • x.snd)
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 w : X
hw : w ∈ {y | ‖f y‖ = M}
u : X
hu : u ∈ f ⁻¹' Metric.ball (f w) M
⊢ ‖f u‖ = M

Tactic:
simp only [mem_preimage, Metric.mem_ball, dist_eq_norm, ← div_lt_one₀ hM] at hu

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}
u : X
hu : ‖f u - f w‖ / M < 1
⊢ ‖f u‖ = M
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
x y : R
h : ¬x * y = 0
⊢ AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y

Tactic:
· change ite _ _ _ ≤ ite _ _ _ * ite _ _ _
          simp only [if_false, h, left_ne_zero_of_mul h, right_ne_zero_of_mul h, mul_one,
            le_refl]

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

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

Tactic:
map_mul_zero_of_map_zero f_nonneg f_mul hy (x * z),

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy : f y = 0
z : R
⊢ 0 / f z ≤ seminormFromBounded' f x * seminormFromBounded' f y
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

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

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 y : R
hy : ¬seminormFromBounded' f y = 0
⊢ ∀ (x_1 : R), f (x * y * x_1) / f x_1 ≤ seminormFromBounded' f x * seminormFromBounded' f y

Tactic:
· rw [seminormFromBounded_eq_zero_iff f_nonneg f_mul] at hy
    intro z
    rw [mul_comm x y, mul_assoc, map_mul_zero_of_map_zero f_nonneg f_mul hy (x * z), zero_div]
    exact mul_nonneg (seminormFromBounded_nonneg f_nonneg f_mul x)
      (seminormFromBounded_nonneg f_nonneg f_mul y)

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 y : R
hy : ¬seminormFromBounded' f y = 0
⊢ ∀ (x_1 : R), f (x * y * x_1) / f x_1 ≤ seminormFromBounded' f x * seminormFromBounded' f y
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

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

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
⊢ ⨆ y, f y / f y ≤ 1

case a
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
⊢ 1 ≤ ⨆ y, f y / f y
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
i : ι
hBi : B i = 1
x : K
⊢ (univ.sup' ⋯ fun x_1 ↦ ‖if i = x_1 then x else 0‖) = ‖x‖

Tactic:
apply le_antisymm

Goal state after:
case a
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
i : ι
hBi : B i = 1
x : K
⊢ (univ.sup' ⋯ fun x_1 ↦ ‖if i = x_1 then x else 0‖) ≤ ‖x‖

case a
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
i : ι
hBi : B i = 1
x : K
⊢ ‖x‖ ≤ univ.sup' ⋯ fun x_1 ↦ ‖if i = x_1 then x else 0‖
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

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

Tactic:
apply le_antisymm

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

case a
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 x ≤ ⨆ y, f x * (f y / f y)
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
y : R
hy0 : f y = 0
⊢ (fun y ↦ f x * (f y / f y)) y ≤ f x

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
y : R
hy0 : ¬f y = 0
⊢ (fun y ↦ f x * (f y / f y)) y ≤ f x

Tactic:
· simp only [hy0, div_zero, mul_zero]; exact f_nonneg _

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
y : R
hy0 : ¬f y = 0
⊢ (fun y ↦ f x * (f y / f y)) y ≤ f x
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
⊢ ⨆ y, f (x * y) / f y = f x

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
⊢ ⨆ y, f (x * y) / f y ≤ f x

case a
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
⊢ f x ≤ ⨆ y, f (x * y) / f y
Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension

Goal state before:
pp: K : Type u_1
inst✝² : NormedField K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
x : L
n : ℕ
hn : 1 ≤ n
⊢ (invariantExtension K L) (x ^ n) = (invariantExtension K L) x ^ n

Tactic:
rw [invariantExtension_apply, invariantExtension_apply, Real.iSup_pow
    (fun σ ↦ apply_nonneg (algNormOfAlgEquiv σ) x)]

Goal state after:
K : Type u_1
inst✝² : NormedField K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
x : L
n : ℕ
hn : 1 ≤ n
⊢ ⨆ σ, (algNormOfAlgEquiv σ) (x ^ n) = ⨆ i, (algNormOfAlgEquiv i) x ^ n
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
x : R
⊢ BddBelow (Set.range (seminormFromConst_seq c f x))

Tactic:
use 0
  rintro r ⟨n, rfl⟩
  exact seminormFromConst_seq_nonneg c f x n

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✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
⊢ (⨆ x, if x ∈ s then f x else 0) = spectralValue p

Tactic:
apply le_antisymm

Goal state after:
case a
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
⊢ (⨆ x, if x ∈ s then f x else 0) ≤ spectralValue p

case a
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
⊢ spectralValue p ≤ ⨆ x, if x ∈ s then f x else 0
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 : 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)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
⊢ ∑ k ∈ range n, C * b (k + 1) + (C * b 0 + C * ‖h‖) = ∑ k ∈ range (n + 1), C * b k + C * ‖h‖

Tactic:
by rw [← add_assoc, sum_range_succ']

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

Goal state before:
pp: case refine_1
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : V ⟶ X
x : V.carrier
⊢ (Hom.hom f) x = (Hom.hom default) x

Tactic:
have : x = 0 := Subsingleton.elim _ _

Goal state after:
case refine_1
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : V ⟶ X
x : V.carrier
this : x = 0
⊢ (Hom.hom f) x = (Hom.hom default) x
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: case refine_1
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : V ⟶ X
x : V.carrier
⊢ ↑(Hom.hom f) x = ↑(Hom.hom default) x

Tactic:
have : x = 0 := Subsingleton.elim _ _

Goal state after:
case refine_1
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : V ⟶ X
x : V.carrier
this : x = 0
⊢ ↑(Hom.hom f) x = ↑(Hom.hom default) x
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
⊢ spectralNorm K L 0 = 0

Tactic:
by
  unfold spectralNorm
  rw [minpoly.zero, ← pow_one X, spectralValue_X_pow 1]

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

Goal state before:
pp: case pos
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
x : L
hf1 : f 1 = 1
p : K[X] := minpoly K x
hp_sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
s : Multiset L
hs : Polynomial.map (algebraMap K L) (minpoly K x) = (Multiset.map (fun x ↦ X - C x) s).prod
h_lc : (algebraMap K L) (minpoly K x).leadingCoeff = 1
y : L
h : y ∈ s
⊢ f y ≤ ⨆ σ, f (σ x)

Tactic:
obtain ⟨σ, hσ⟩ : ∃ σ : Gal(L/K), σ x = y := minpoly.exists_algEquiv_of_root'
        (Algebra.IsAlgebraic.isAlgebraic x) (aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C s h hs)

Goal state after:
case pos
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
x : L
hf1 : f 1 = 1
p : K[X] := minpoly K x
hp_sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
s : Multiset L
hs : Polynomial.map (algebraMap K L) (minpoly K x) = (Multiset.map (fun x ↦ X - C x) s).prod
h_lc : (algebraMap K L) (minpoly K x).leadingCoeff = 1
y : L
h : y ∈ s
σ : Gal(L/K)
hσ : σ x = y
⊢ f y ≤ ⨆ σ, f (σ x)
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: A B C D B' D' : SemiNormedGrp
fab : A ⟶ B
fbd : B ⟶ D
fac : A ⟶ C
fcd : C ⟶ D
h : fab ≫ fbd = fac ≫ fcd
fbb' : B ⟶ B'
fdd' : D ⟶ D'
condb : fab ≫ fbb' = 0
condd : fcd ≫ fdd' = 0
g : B' ⟶ D'
h' : fbb' ≫ g = fbd ≫ fdd'
⊢ explicitCokernelDesc condb ≫ g = explicitCokernel.map h ≫ explicitCokernelDesc condd

Tactic:
by
  delta explicitCokernel.map
  simp only [← Category.assoc, ← cancel_epi (explicitCokernelπ fab)]
  simp [Category.assoc, explicitCokernelπ_desc, h']

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
x y : L
⊢ spectralNorm K L (-(y - x)) = spectralNorm K L (y - x)

Tactic:
spectralNorm_neg (Algebra.IsAlgebraic.isAlgebraic _)

Goal state after:
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
x y : L
⊢ spectralNorm K L (y - x) = spectralNorm K L (y - x)
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_7
E : Type u_8
F : Type u_9
inst✝⁶ : NontriviallyNormedField R
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace R E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : CompleteSpace F
f : E →L[R] F
hf : Injective ⇑f
hf' : IsClosed (range ⇑f)
hf'' : (↑f).range.ClosedComplemented
⊢ (↑f.rangeRestrict).ker = ⊥

Tactic:
ker_codRestrict

Goal state after:
R : Type u_7
E : Type u_8
F : Type u_9
inst✝⁶ : NontriviallyNormedField R
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace R E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : CompleteSpace F
f : E →L[R] F
hf : Injective ⇑f
hf' : IsClosed (range ⇑f)
hf'' : (↑f).range.ClosedComplemented
⊢ (↑f).ker = ⊥
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: case inr.inr
ι : 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
⊢ ‖((holderₗ r B hBK) e) f‖ ≤ ↑K * ‖e‖ * ‖f‖

Tactic:
· have hpqr := hpqr.toReal r (zero_lt_one.trans_le hp) (zero_lt_one.trans_le hq)
      have hp := hpqr.pos
      have hq := hpqr.symm.pos
      refine norm_le_of_forall_sum_le hpqr.pos' (by positivity) fun s ↦ ?_
      simp only [holderₗ_apply_apply_coe]
      calc
        _ ≤ K ^ r.toReal * (‖e‖ ^ p.toReal) ^ (r.toReal / p.toReal) *
          (‖f‖ ^ q.toReal) ^ (r.toReal / q.toReal) :=
          Memℓp.holder_gen_bound r hp hq B hBK (by positivity) (by positivity)
            (sum_rpow_le_norm_rpow hp e) (sum_rpow_le_norm_rpow hq f) s
        _ ≤ _ := 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:
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
⊢ [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 1 → 4 := IsFredholm.nonempty_fredholmPackage
  tfae_have 4 → 2 := by
    rintro ⟨dec⟩
    exact ⟨dec.quasiInverse, dec.isQuasiInverse⟩
  tfae_have 2 → 3 := by
    rintro ⟨v, huv⟩
    exact exists_restrict_isInvertible_of_isQuasiInverse huv
  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
  tfae_finish

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Int

Goal state before:
pp: n : ℤ
⊢ ↑n.toNat + ↑(-n).toNat = ‖n‖₊

Tactic:
rw [← Nat.cast_add, toNat_add_toNat_neg_eq_natAbs, NNReal.natCast_natAbs]

Goal state after:
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
inst✝¹ : T2Space F
u : E →L[𝕜] F
A : Submodule 𝕜 F
inst✝ : FiniteDimensional 𝕜 ↥A
A_compl : A.ClosedComplemented
S : Submodule 𝕜 F
A_compl_S : IsTopCompl A S
Φ : (F ⧸ A) ≃L[𝕜] ↥S := A.quotientEquivOfIsTopCompl S A_compl_S
i : ↥S →L[𝕜] F := S.subtypeL
i_clemb : IsClosedEmbedding ⇑i
p : F →L[𝕜] F := S.projectionL A ⋯
p_def : p = S.projectionL A ⋯
eq : ⇑i ∘ ⇑Φ ∘ ⇑A.mkQ = ⇑p
this : ↑u ≈ ↑(p ∘SL u)
⊢ IsStrictMap ((⇑i ∘ ⇑Φ ∘ ⇑A.mkQ) ∘ ⇑u) ∧ IsClosed[inst✝⁴] (range ((⇑i ∘ ⇑Φ ∘ ⇑A.mkQ) ∘ ⇑u)) ↔
    IsStrictMap (⇑i ∘ ⇑Φ ∘ ⇑A.mkQ ∘ ⇑u) ∧ IsClosed[inst✝⁴] (range (⇑i ∘ ⇑Φ ∘ ⇑A.mkQ ∘ ⇑u))

Tactic:
Function.comp_assoc

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
t' : ℝ
ht'✝ : t' ∈ Ioc (min ↑t₀ ↑t) (max ↑t₀ ↑t)
ht' : t' ∈ Icc tmin tmax
⊢ dist (f t' (((next hf hx)^[n] α).toFun ⟨t', ?m.549⟩)) (f t' (((next hf hx)^[n] β).toFun ⟨t', ?m.561⟩)) ≤
    ↑K ^ (n + 1) * |t' - ↑t₀| ^ n / ↑n ! * dist α β

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
t' : ℝ
ht'✝ : t' ∈ Ioc (min ↑t₀ ↑t) (max ↑t₀ ↑t)
ht' : t' ∈ Icc tmin tmax
⊢ t' ∈ Icc tmin tmax

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
t' : ℝ
ht'✝ : t' ∈ Ioc (min ↑t₀ ↑t) (max ↑t₀ ↑t)
ht' : t' ∈ Icc tmin tmax
⊢ t' ∈ Icc tmin tmax

Tactic:
exact dist_comp_iterate_next_le hf hx _ ⟨t', ht'⟩ (hn _)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case neg
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
⊢ ⨆ i, v (p.coeff i) * c ^ i = p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i

Tactic:
apply le_antisymm

Goal state after:
case neg.a
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
⊢ ⨆ i, v (p.coeff i) * c ^ i ≤ p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i

case a
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
hp : ¬p = 0
⊢ (p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i) ≤ ⨆ i, v (p.coeff i) * c ^ i