mathlib-initiative/mathlib-tactics huggingface dataset:
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
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
hc : ‖p.coeff m‖ = f (((mapAlg K L) p).coeff m)
h : f ((-1) ^ (s.card - m) * s.esymm (s.card - m)) = f (s.esymm (s.card - m))
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge : f (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤ f t.prod
⊢ f (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤ (⨆ x, if x ∈ s then f x else 0) ^ (p.natDegree - m)

Tactic:
apply le_trans ht_ge

Goal state after:
case pos
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
hc : ‖p.coeff m‖ = f (((mapAlg K L) p).coeff m)
h : f ((-1) ^ (s.card - m) * s.esymm (s.card - m)) = f (s.esymm (s.card - m))
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge : f (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤ f t.prod
⊢ f t.prod ≤ (⨆ x, if x ∈ s then f x else 0) ^ (p.natDegree - m)
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 : ℕ
⊢ ‖h‖ + ‖v 0 - h‖ ≤ ‖h‖ + b 0

Tactic:
rw [← norm_neg_add]; gcongr

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

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 : 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, C * b (k + 1) + C * b 0 + C * ‖h‖
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

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

Tactic:
refine explicitCokernelDesc_unique _ _ ?_
  rw [← CategoryTheory.Category.assoc, explicitCokernelπ_desc]

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
⊢ Tendsto (fun x ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))

Tactic:
rcases isEmpty_or_nonempty β

Goal state after:
case inl
α : 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✝ : IsEmpty β
⊢ Tendsto (fun x ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))

case inr
α : 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 β
⊢ Tendsto (fun x ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
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
E : Type u_2
L : Type u_3
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra.IsAlgebraic K L
inst✝³ : NormedField E
inst✝² : NormedAlgebra K E
inst✝¹ : Algebra E L
inst✝ : IsScalarTower K E L
x✝⁴ : NormedField L := normedField K L
x✝³ : NormedAlgebra K L := normedAlgebra K L
x✝² : Algebra.IsAlgebraic K E := Algebra.IsAlgebraic.tower_bot K E L
x✝¹ : E
x✝ : L
⊢ ‖x✝¹ • x✝‖ ≤ ‖x✝¹‖ * ‖x✝‖

Tactic:
apply le_of_eq

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
E : Type u_2
L : Type u_3
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra.IsAlgebraic K L
inst✝³ : NormedField E
inst✝² : NormedAlgebra K E
inst✝¹ : Algebra E L
inst✝ : IsScalarTower K E L
x✝⁴ : NormedField L := ⋯
x✝³ : NormedAlgebra K L := ⋯
x✝² : Algebra.IsAlgebraic K E := ⋯
x✝¹ : E
x✝ : L
⊢ ‖x✝¹ • x✝‖ = ‖x✝¹‖ * ‖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✝ : Algebra.IsAlgebraic K E
a : E
ha : (mapAlg K E) (minpoly K x) ≠ 0 ∧ eval a ((mapAlg K E) (minpoly K x)) = 0
⊢ eval₂ (algebraMap K E) a (minpoly K x) = eval a (Polynomial.map (algebraMap K E) (minpoly K x))

Tactic:
eval_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
⊢ eval₂ (algebraMap K E) a (minpoly K x) = eval₂ (algebraMap K E) a (minpoly K x)
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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖

Tactic:
abel

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

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P = ↑P * ↑R → ↑Q = ↑Q * ↑R → ↑P + (↑Q - ↑P * ↑Q) = ↑P * ↑R + (↑Q * ↑R - ↑P * (↑Q * ↑R))

Tactic:
intro h₁

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 }
h₁ : ↑P = ↑P * ↑R
⊢ ↑Q = ↑Q * ↑R → ↑P + (↑Q - ↑P * ↑Q) = ↑P * ↑R + (↑Q * ↑R - ↑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 * ↑Q → ↑P = ↑P * ↑R → ↑P = ↑P * ↑Q * ↑R

Tactic:
intro h₁

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 }
h₁ : ↑P = ↑P * ↑Q
⊢ ↑P = ↑P * ↑R → ↑P = ↑P * ↑Q * ↑R
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : NormedCommRing R
inst✝² : NormOneClass R
f : ι → R
inst✝¹ : CompleteSpace R
inst✝ : NormMulClass R
hf : ∀ (i : ι), 1 + f i ≠ 0
hu : Summable fun x ↦ ‖f x‖
⊢ ∏' (i : ι), (1 + f i) ≠ 0

Tactic:
rw [← norm_ne_zero_iff, Multipliable.norm_tprod]
  · rw [← Real.rexp_tsum_eq_tprod (fun i ↦ norm_pos_iff.mpr <| hf i) hu.summable_log_norm_one_add]
    apply Real.exp_ne_zero
  · exact multipliable_one_add_of_summable hu

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
K : Set α
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
hf : TendstoUniformlyOn f g p K
hg : BddAbove ((fun x ↦ (g x).re) '' K)
⊢ TendstoUniformlyOn (fun x ↦ cexp ∘ f x) (cexp ∘ g) p K

Tactic:
obtain ⟨v, hv⟩ : ∃ v, ∀ x ∈ K, (g x).re ≤ v := hg.imp <| by simp [mem_upperBounds]

Goal state after:
α : Type u_1
ι : Type u_2
K : Set α
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
hf : TendstoUniformlyOn f g p K
hg : BddAbove ((fun x ↦ (g x).re) '' K)
v : ℝ
hv : ∀ x ∈ K, (g x).re ≤ v
⊢ TendstoUniformlyOn (fun x ↦ cexp ∘ f x) (cexp ∘ g) p K
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: case inl
ι : 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)
q : ℝ≥0∞
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
e : (i : ι) → E i
f : (i : ι) → F i
he : Memℓp e ∞
hf : Memℓp f q
h : IsEmpty ι
⊢ Memℓp (fun i ↦ ((B i) (e i)) (f i)) q

Tactic:
exact all _

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝⁹ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_4
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E' : ι → Type u_5
E'' : ι → Type u_6
inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)
g : (i : ι) → E' i →L[𝕜] E'' i
f✝ f : (i : ι) → E i →L[𝕜] E' i
⊢ ‖{ toFun := mapL, map_update_add' := ⋯, map_update_smul' := ⋯ } f‖ ≤ 1 * ∏ i, ‖f i‖

Tactic:
by rw [one_mul]; exact opNorm_mapL f

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

Goal state before:
pp: case inl
ι : 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
e : (i : ι) → E i
f : (i : ι) → F i
he : Memℓp e p
hf : Memℓp f q
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
h : IsEmpty ι
⊢ Memℓp (fun i ↦ ((B i) (e i)) (f i)) r

Tactic:
exact all _

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
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁵] ↑A
A_cofg : A.CoFG
h_ker : Disjoint (↑u).ker A
range_u : (↑u).range = ⊤
range_u_restr : IsClosed[inst✝²] ↑(↑(u.domRestrict A)).range
S : Submodule 𝕜 E
ker_le_S : (↑u).ker ≤ S
this✝ : FiniteDimensional 𝕜 ↥S
S_compl_A : IsTopCompl S A
uS_compl_uA : IsTopCompl (map (↑u) S) (map (↑u) A)
this : T2Space ↥(map (↑u) S)
uₛ : ↥S →L[𝕜] ↥(map (↑u) S) := u.restrict ⋯
uₐ : ↥A →L[𝕜] ↥(map (↑u) A) := u.restrict ⋯
Φ : (↥S × ↥A) ≃L[𝕜] E := S.prodEquivOfIsTopCompl A S_compl_A
Ψ : (↥(map (↑u) S) × ↥(map (↑u) A)) ≃L[𝕜] F := (map (↑u) S).prodEquivOfIsTopCompl (map (↑u) A) uS_compl_uA
u_eq : ⇑u = ⇑Ψ ∘ ⇑(uₛ.prodMap uₐ) ∘ ⇑Φ.symm
u_restr_eq : ⇑(u.domRestrict A) = ⇑(map (↑u) A).subtypeL ∘ ⇑uₐ
⊢ IsStrictMap ⇑(uₛ.prodMap uₐ) ↔ IsStrictMap ⇑uₐ

Tactic:
← coe_coe,

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
A_cofg : A.CoFG
h_ker : Disjoint (↑u).ker A
range_u : (↑u).range = ⊤
range_u_restr : IsClosed[inst✝²] ↑(↑(u.domRestrict A)).range
S : Submodule 𝕜 E
ker_le_S : (↑u).ker ≤ S
this✝ : FiniteDimensional 𝕜 ↥S
S_compl_A : IsTopCompl S A
uS_compl_uA : IsTopCompl (map (↑u) S) (map (↑u) A)
this : T2Space ↥(map (↑u) S)
uₛ : ↥S →L[𝕜] ↥(map (↑u) S) := u.restrict ⋯
uₐ : ↥A →L[𝕜] ↥(map (↑u) A) := u.restrict ⋯
Φ : (↥S × ↥A) ≃L[𝕜] E := S.prodEquivOfIsTopCompl A S_compl_A
Ψ : (↥(map (↑u) S) × ↥(map (↑u) A)) ≃L[𝕜] F := (map (↑u) S).prodEquivOfIsTopCompl (map (↑u) A) uS_compl_uA
u_eq : ⇑u = ⇑Ψ ∘ ⇑(uₛ.prodMap uₐ) ∘ ⇑Φ.symm
u_restr_eq : ⇑(u.domRestrict A) = ⇑(map (↑u) A).subtypeL ∘ ⇑uₐ
⊢ IsStrictMap ⇑↑(uₛ.prodMap uₐ) ↔ IsStrictMap ⇑↑uₐ
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:
rw [← Real.rpow_mul, ← Real.rpow_mul]

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

case hx
ι : 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 ι
⊢ 0 ≤ ‖f‖

case hx
ι : 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 ι
⊢ 0 ≤ ‖e‖
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 = ⊤
u_strict : IsStrictMap ⇑u
u_quot : IsQuotientMap ⇑u
⊢ IsClosed[inst✝⁶] (⇑u ⁻¹' ↑(↑(u.domRestrict A)).range)

Tactic:
← coe_coe,

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
u_quot : IsQuotientMap ⇑u
⊢ IsClosed[inst✝⁶] (⇑↑u ⁻¹' ↑(↑(u.domRestrict A)).range)
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: case refine_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + ‖3 / 4 * δ‖ ≤ δ

Tactic:
apply le_of_eq

Goal state after:
case refine_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + ‖3 / 4 * δ‖ = δ
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: case refine_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + ‖3 / 4 * δ‖ ≤ δ

Tactic:
apply le_of_eq

Goal state after:
case refine_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + ‖3 / 4 * δ‖ = δ
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: case neg
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : { toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = y.conjContinuousAlgEquiv
this : ∀ (x : V →L[𝕜] V), adjoint (f x) = f (adjoint x)
⊢ ∃ U, f = U.conjStarAlgEquiv

Tactic:
rw [ContinuousAlgEquiv.ext_iff] at hy

Goal state after:
case neg
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this : ∀ (x : V →L[𝕜] V), adjoint (f x) = f (adjoint x)
⊢ ∃ U, f = U.conjStarAlgEquiv
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case succ
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)
⊢ dist (((next hf hx)^[n + 1] α).toFun t) (((next hf hx)^[n + 1] β).toFun t) ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β

Tactic:
| succ n hn =>

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
t₀ : ℝ
hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)
hf : ∀ (t : ℝ), HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ (t : ℝ), HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t A B : ℝ
Ht : t ∈ Ioo A B
Ht₀ : t₀ ∈ Ioo A B
⊢ f t = g t

Tactic:
exact ODE_solution_unique_of_mem_Ioo
    (fun t _ => hv t) Ht₀ (fun t _ => hf t) (fun t _ => hg t) heq Ht

Goal state after:
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
ha✝ : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
⊢ ‖a‖₊ - 1 + 1 = ‖a‖₊ ^ p.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1

Tactic:
by field

Goal state after: