mathlib-initiative/mathlib-tactics huggingface dataset:
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
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
h_pr : f t.prod ≤ (Multiset.map (⇑f) t).prod
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, f z ≤ f y
⊢ (Multiset.map (⇑f) t).prod ≤ f y ^ (p.natDegree - m)

Tactic:
set g : L → NNReal := fun x ↦ ⟨f x, apply_nonneg f x⟩

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
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
h_pr : f t.prod ≤ (Multiset.map (⇑f) t).prod
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, f z ≤ f y
g : L → NNReal := fun x ↦ ⟨f x, ⋯⟩
⊢ (Multiset.map (⇑f) t).prod ≤ f y ^ (p.natDegree - m)
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case h
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
h_pr : f t.prod ≤ (Multiset.map (⇑f) t).prod
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, f z ≤ f y
this : (Multiset.map (⇑f) t).prod ≤ f y ^ (p.natDegree - m)
r : ℝ
hr : r ∈ Set.range fun x ↦ if x ∈ s then f x else 0
z : L
hz : (fun x ↦ if x ∈ s then f x else 0) z = r
⊢ r ≤ f y

Tactic:
simp only at hz

Goal state after:
case h
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
h_pr : f t.prod ≤ (Multiset.map (⇑f) t).prod
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, f z ≤ f y
this : (Multiset.map (⇑f) t).prod ≤ f y ^ (p.natDegree - m)
r : ℝ
hr : r ∈ Set.range fun x ↦ if x ∈ s then f x else 0
z : L
hz : (if z ∈ s then f z else 0) = r
⊢ r ≤ f y
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y : SemiNormedGrp
f : X ⟶ Y
⊢ ∀ {Z : SemiNormedGrp} (g h : explicitCokernel f ⟶ Z), explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h → g = h

Tactic:
intro Z g h H

Goal state after:
X Y : SemiNormedGrp
f : X ⟶ Y
Z : SemiNormedGrp
g h : explicitCokernel f ⟶ Z
H : explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h
⊢ g = h
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

Goal state before:
pp: case mp
M : Type u_1
inst✝ : SeminormedAddCommGroup M
⊢ normedMk = 0 → ∀ (x : M), ‖x‖ = 0

pp: case mpr
M : Type u_1
inst✝ : SeminormedAddCommGroup M
⊢ (∀ (x : M), ‖x‖ = 0) → normedMk = 0

Tactic:
· intro h x
    rw [SeparationQuotient.mk_eq_zero_iff.mp]
    have : normedMk x = 0 := by
      rw [h]
      simp only [NormedAddGroupHom.zero_apply]
    rw [← this]
    simp

Goal state after:
case mpr
M : Type u_1
inst✝ : SeminormedAddCommGroup M
⊢ (∀ (x : M), ‖x‖ = 0) → normedMk = 0
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : SeminormedAddCommGroup M
⊢ (∀ (x : M), ‖x‖ = 0) → normedMk = 0

Tactic:
intro h
    ext x
    simpa [← norm_eq_zero] using h x

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : x ∈ {0}ᶜ
⊢ (fun x ↦ ⟨↑x.2 • ↑x.1, ⋯⟩)
      ((fun x ↦
          have this := ⋯;
          (⟨r • ‖↑x‖⁻¹ • ↑x, ⋯⟩, ⟨‖↑x‖ / r, ⋯⟩))
        ⟨x, hx⟩) =
    ⟨x, hx⟩

Tactic:
have : 0 < ‖x‖ := by simpa using hx

Goal state after:
E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : x ∈ {0}ᶜ
this : 0 < ‖x‖
⊢ (fun x ↦ ⟨↑x.2 • ↑x.1, ⋯⟩)
      ((fun x ↦
          have this := ⋯;
          (⟨r • ‖↑x‖⁻¹ • ↑x, ⋯⟩, ⟨‖↑x‖ / r, ⋯⟩))
        ⟨x, hx⟩) =
    ⟨x, hx⟩
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
hf : Summable fun i ↦ ‖f i‖
i : ι
| ‖1 + f i‖

Tactic:
← sub_add_cancel ‖1 + f i‖ 1,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
hf : Summable fun i ↦ ‖f i‖
i : ι
| ‖1 + f i‖ - 1 + 1
Module: Mathlib.Topology.Maps.Strict.Group

Goal state before:
pp: G : Type u_1
H : Type u_2
G' : Type u_3
H' : Type u_4
inst✝⁹ : Group G'
inst✝⁸ : Group H'
inst✝⁷ : Group G
inst✝⁶ : Group H
f : G →* H
g : G' →* H'
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalGroup G
inst✝² : TopologicalSpace G'
inst✝¹ : IsTopologicalGroup G'
inst✝ : TopologicalSpace H'
Φ : ↥(f.prodMap g).range ≃ₜ ↥f.range × ↥g.range := (Homeomorph.setCongr ⋯).trans (Homeomorph.Set.prod ↑f.range ↑g.range)
eq : ⇑Φ ∘ ⇑(f.prodMap g).rangeRestrict = ⇑(f.rangeRestrict.prodMap g.rangeRestrict)
⊢ IsOpenQuotientMap (Prod.map ⇑f.rangeRestrict ⇑g.rangeRestrict) ↔
    IsOpenQuotientMap ⇑f.rangeRestrict ∧ IsOpenQuotientMap ⇑g.rangeRestrict

Tactic:
isOpenQuotientMap_prodMap_iff

Goal state after:
G : Type u_1
H : Type u_2
G' : Type u_3
H' : Type u_4
inst✝⁹ : Group G'
inst✝⁸ : Group H'
inst✝⁷ : Group G
inst✝⁶ : Group H
f : G →* H
g : G' →* H'
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalGroup G
inst✝² : TopologicalSpace G'
inst✝¹ : IsTopologicalGroup G'
inst✝ : TopologicalSpace H'
Φ : ↥(f.prodMap g).range ≃ₜ ↥f.range × ↥g.range := (Homeomorph.setCongr ⋯).trans (Homeomorph.Set.prod ↑f.range ↑g.range)
eq : ⇑Φ ∘ ⇑(f.prodMap g).rangeRestrict = ⇑(f.rangeRestrict.prodMap g.rangeRestrict)
⊢ IsOpenQuotientMap ⇑f.rangeRestrict ∧ IsOpenQuotientMap ⇑g.rangeRestrict ↔
    IsOpenQuotientMap ⇑f.rangeRestrict ∧ IsOpenQuotientMap ⇑g.rangeRestrict
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: case refine_2
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
⊢ ∀
    b ∈
      {p |
        ∃ G x x_1,
          p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)},
    b ≤ projectiveSeminorm

Tactic:
intro p hp
    simp only [Set.mem_ofPred_eq] at hp
    obtain ⟨G, _, _, h⟩ := hp
    rw [h]; intro x; simp only [Seminorm.comp_apply, coe_normSeminorm]
    exact toDualContinuousMultilinearMap_le_projectiveSeminorm _

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
u : E →L[𝕜] F
E₁ : Submodule 𝕜 E
E₁_closed : IsClosed[inst✝⁶] ↑E₁
E₁_coFG : E₁.CoFG
F₁ : Submodule 𝕜 F
F₁_closed : IsClosed[inst✝⁵] ↑F₁
F₁_coFG : F₁.CoFG
h_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
e : ↥E₁ ≃L[𝕜] ↥F₁
he : ↑e = u.restrict h_mapsto
eqL : u.domRestrict E₁ = F₁.subtypeL ∘SL ↑e
eqₗ : (↑u).domRestrict E₁ = F₁.subtype ∘ₗ ↑↑e
h : IsStrictMap ⇑u ∧ IsClosed[inst✝⁵] ↑(↑u).range
⊢ Disjoint E₁ (↑u).ker

Tactic:
disjoint_iff_comap_eq_bot,

Goal state after:
𝕜 : 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
u : E →L[𝕜] F
E₁ : Submodule 𝕜 E
E₁_closed : IsClosed[inst✝⁶] ↑E₁
E₁_coFG : E₁.CoFG
F₁ : Submodule 𝕜 F
F₁_closed : IsClosed[inst✝⁵] ↑F₁
F₁_coFG : F₁.CoFG
h_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
e : ↥E₁ ≃L[𝕜] ↥F₁
he : ↑e = u.restrict h_mapsto
eqL : u.domRestrict E₁ = F₁.subtypeL ∘SL ↑e
eqₗ : (↑u).domRestrict E₁ = F₁.subtype ∘ₗ ↑↑e
h : IsStrictMap ⇑u ∧ IsClosed[inst✝⁵] ↑(↑u).range
⊢ comap E₁.subtype (↑u).ker = ⊥
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
F' : Submodule 𝕜 F := (↑u).range
h_range : IsClosed[inst✝³] ↑F'
i : ↥F' →L[𝕜] F := F'.subtypeL
i_clemb : IsClosedEmbedding ⇑i
u' : E →L[𝕜] ↥F' := u.rangeRestrict
⊢ IsStrictMap ⇑u ↔ IsStrictMap ⇑(u.domRestrict A) ∧ IsClosed[inst✝³] ↑(↑(u.domRestrict A)).range

Tactic:
have range_u' : u'.range = ⊤ := u.range_rangeRestrict

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
F' : Submodule 𝕜 F := (↑u).range
h_range : IsClosed[inst✝³] ↑F'
i : ↥F' →L[𝕜] F := F'.subtypeL
i_clemb : IsClosedEmbedding ⇑i
u' : E →L[𝕜] ↥F' := u.rangeRestrict
range_u' : (↑u').range = ⊤
⊢ IsStrictMap ⇑u ↔ IsStrictMap ⇑(u.domRestrict A) ∧ IsClosed[inst✝³] ↑(↑(u.domRestrict A)).range
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
⊢ ∀ (i : ι), z i < y i

Tactic:
refine fun i => (hxy _).trans_le' (sub_le_iff_le_add'.1 <| (le_abs_self _).trans ?_)

Goal state after:
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
i : ι
⊢ |z i - x i| ≤ ε
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
hxy : dist x y < δ / 4
z : ι → ℝ
hz : ‖x + const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
⊢ y i < z i

Tactic:
rw [dist_eq_norm] at hxy

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
hxy : ‖x - y‖ < δ / 4
z : ι → ℝ
hz : ‖x + const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
⊢ 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
hxy : dist x y < δ / 4
z : ι → ℝ
hz : ‖x - const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
⊢ z i < y i

Tactic:
rw [dist_eq_norm] at hxy

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
hxy : ‖x - y‖ < δ / 4
z : ι → ℝ
hz : ‖x - const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
⊢ z i < y i
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: case neg
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
⊢ ∃ U, ∀ (x : V →L[𝕜] V), f x ∘SL ↑U = ↑U ∘SL x

Tactic:
set T := apply' _ (.id 𝕜) z ∘L f.toContinuousAlgHom.toContinuousLinearMap ∘L smulRightL 𝕜 _ _ v

Goal state after:
case neg
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →L[𝕜] W := (apply' W (RingHom.id 𝕜)) z ∘SL (↑f).toContinuousLinearMap ∘SL (smulRightL 𝕜 V V) v
⊢ ∃ U, ∀ (x : V →L[𝕜] V), f x ∘SL ↑U = ↑U ∘SL x
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: case neg
δ K ε x : ℝ
hK : ¬K = 0
⊢ HasDerivAt (fun x ↦ δ * rexp (K * x) + ε / K * (rexp (K * x) - 1))
    (K * (δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)) + ε) x

Tactic:
convert!
      (((hasDerivAt_id x).const_mul K).exp.const_mul δ).add
        ((((hasDerivAt_id x).const_mul K).exp.sub_const 1).const_mul (ε / K)) using 1

Goal state after:
case e'_9
δ K ε x : ℝ
hK : ¬K = 0
⊢ K * (δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)) + ε =
    δ * (rexp (K * id x) * (K * 1)) + ε / K * (rexp (K * id x) * (K * 1))
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
ε : ℝ
hε : ε > 0
h : IsIntegralCurveOn γ v (Metric.ball t₀ ε)
t : ℝ
⊢ t ∈ Metric.ball (t₀ / a) (ε / |a|) ↔ t ∈ {t | t * a ∈ Metric.ball t₀ ε}

Tactic:
rw [mem_ofPred_eq, Metric.mem_ball, Metric.mem_ball, Real.dist_eq, Real.dist_eq,
    lt_div_iff₀ (abs_pos.mpr ha), ← abs_mul, sub_mul, div_mul_cancel₀ _ ha]

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

Goal state before:
pp: case mpr
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
h : ∀ (t : ↑(Icc tmin tmax)), α.toFun t = picard f (↑t₀) x α.compProj ↑t
t : ↑(Icc tmin tmax)
⊢ (next hf hx α).toFun t = α.toFun t

Tactic:
rw [h, next_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.degree = Q.degree
⊢ Tendsto (fun x ↦ eval x P / eval x Q) atBot (𝓝 (P.leadingCoeff / Q.leadingCoeff))

Tactic:
by
  refine (isEquivalent_atBot_div P Q).symm.tendsto_nhds ?_
  simp [natDegree_eq_natDegree hdeg]

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

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedRing A
p : A[X]
⊢ p.supNorm ∈ upperBounds (Set.range fun x ↦ ‖p.coeff x‖)

Tactic:
simpa [mem_upperBounds] using le_supNorm p

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

Goal state before:
pp: P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
h : Odd P.natDegree
hlc' : 0 ≤ -1 * (P.comp (-X)).leadingCoeff
⊢ 0 < -1 * eval x P

Tactic:
neg_one_mul

Goal state after:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
h : Odd P.natDegree
hlc' : 0 ≤ -(P.comp (-X)).leadingCoeff
⊢ 0 < -eval x P
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: case inr
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑b ≤ ↑a
⊢ a =ᶠ[↑φ] fun x ↦ max (a x) (b x)

Tactic:
exact h.mono fun i hi => (max_eq_left hi).symm

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

Goal state before:
pp: n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
⊢ ∏ z ∈ x.toFinset, max 1 ‖z‖ ^ count z x ≤ ∏ z ∈ p.roots.toFinset, max 1 ‖z‖ ^ count z x

Tactic:
simp_rw [← coe_nnnorm]

Goal state after:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
⊢ ∏ z ∈ x.toFinset, max 1 ↑‖z‖₊ ^ count z x ≤ ∏ z ∈ p.roots.toFinset, max 1 ↑‖z‖₊ ^ count z x
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case hbc
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this : ∀ x ∈ S.toFinset, ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots
x : Multiset ℂ
hx : x ∈ S.toFinset
⊢ ‖x.prod‖ ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots

Tactic:
Finset.prod_multiset_count,

Goal state after:
case hbc
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this : ∀ x ∈ S.toFinset, ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots
x : Multiset ℂ
hx : x ∈ S.toFinset
⊢ ‖∏ m ∈ x.toFinset, m ^ count m x‖ ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: ⊢ round π = 3

Tactic:
refine round_eq _ |>.trans <| Int.floor_eq_iff.mpr ⟨by grind [pi_gt_three], ?_⟩
  grw [pi_lt_d2]
  norm_num

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
let v₁ (x : ℝ) : ℝ := sin (x * θ)

Goal state after:
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case h₀
x : ℝ
⊢ ¬Real.arctan x = π / 2

Tactic:
rw [← ne_eq]; exact (Real.arctan_lt_pi_div_two _).ne

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case a
x : ℝ≥0
⊢ x ≤ x.agm x

Tactic:
nth_rw 1 [← min_self x]
    exact min_le_agm

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ qaryEntropy 2 = binEntropy

Tactic:
by ext; simp [qaryEntropy]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt

Goal state before:
pp: A : Type u_1
inst✝⁸ : PartialOrder A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : SeparatelyContinuousMul A
c a b : A
⊢ a ≤ b → (conjSqrt c) a ≤ (conjSqrt c) b

Tactic:
hab

Goal state after:
A : Type u_1
inst✝⁸ : PartialOrder A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : SeparatelyContinuousMul A
c a b : A
hab : a ≤ b
⊢ (conjSqrt c) a ≤ (conjSqrt c) b
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hp : p ∈ Icc 0 1
a b : A
⊢ a ≤ b → (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b

Tactic:
hab

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hp : p ∈ Icc 0 1
a b : A
hab : a ≤ b
⊢ (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
⊢ a ≤ b → sqrt a ≤ sqrt b

Tactic:
hab

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
⊢ sqrt a ≤ sqrt b
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case inl
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : q = 0
a b : A
⊢ a ≤ b → (fun a ↦ a ^ ↑0) a ≤ (fun a ↦ a ^ ↑0) b

Tactic:
hab

Goal state after:
case inl
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : q = 0
a b : A
hab : a ≤ b
⊢ (fun a ↦ a ^ ↑0) a ≤ (fun a ↦ a ^ ↑0) b
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a + b = 1 → (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ

Tactic:
hab

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = p.rpowIntegrand₀₁ t 1 * x ^ (p - 1)

Tactic:
rpowIntegrand₀₁_eq_pow_div hp ht zero_le_one

Goal state after:
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)