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

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f (r • (b -ᵥ a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔
    ((r • (b -ᵥ a) +ᵥ a) - a)⁻¹ • (f (r • (b -ᵥ a) +ᵥ a) -ᵥ f a) ≤ (b - a)⁻¹ • (f b -ᵥ f a)

Tactic:
vsub_eq_sub,

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f (r • (b - a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔
    ((r • (b - a) +ᵥ a) - a)⁻¹ • (f (r • (b - a) +ᵥ a) -ᵥ f a) ≤ (b - a)⁻¹ • (f b -ᵥ f a)
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f (r • (b - a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔
    ((r • (b - a) +ᵥ a) - a)⁻¹ • (f (r • (b - a) +ᵥ a) -ᵥ f a) ≤ (b - a)⁻¹ • (f b -ᵥ f a)

Tactic:
vsub_eq_sub,

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f (r • (b - a) +ᵥ a) ≤ r • (f b - f a) +ᵥ f a ↔
    ((r • (b - a) +ᵥ a) - a)⁻¹ • (f (r • (b - a) +ᵥ a) -ᵥ f a) ≤ (b - a)⁻¹ • (f b - f a)
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f (r • (b - a) +ᵥ a) ≤ r • (f b - f a) +ᵥ f a ↔
    ((r • (b - a) +ᵥ a) - a)⁻¹ • (f (r • (b - a) +ᵥ a) -ᵥ f a) ≤ (b - a)⁻¹ • (f b - f a)

Tactic:
vsub_eq_sub,

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f (r • (b - a) +ᵥ a) ≤ r • (f b - f a) +ᵥ f a ↔
    ((r • (b - a) +ᵥ a) - a)⁻¹ • (f (r • (b - a) +ᵥ a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r' : k
h : 0 < r' * (b - a)
⊢ f (r' • (a -ᵥ b) +ᵥ b) ≤ r' • (f a -ᵥ f b) +ᵥ f b ↔
    (b - a)⁻¹ • (f b -ᵥ f a) ≤ (b - (r' • (a -ᵥ b) +ᵥ b))⁻¹ • (f b -ᵥ f (r' • (a -ᵥ b) +ᵥ b))

Tactic:
vsub_eq_sub,

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r' : k
h : 0 < r' * (b - a)
⊢ f (r' • (a - b) +ᵥ b) ≤ r' • (f a - f b) +ᵥ f b ↔
    (b - a)⁻¹ • (f b - f a) ≤ (b - (r' • (a - b) +ᵥ b))⁻¹ • (f b - f (r' • (a - b) +ᵥ b))
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: case refine_2
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : I ≤ idealOfSet R s
x : X
hx : x ∈ setOfIdeal I
⊢ x ∈ s

Tactic:
obtain ⟨f, hf, hfx⟩ := mem_setOfIdeal.mp hx
    by_contra hx'
    exact notMem_idealOfSet.mpr ⟨x, hx', hfx⟩ (h hf)

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: case neg
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g : C(X, ℝ≥0)
hgI : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I
hg : ∀ (x : X), g x ≤ 1
hgt : Set.EqOn (⇑g) 1 t
x : X
hx : x ∉ t
⊢ ‖f x - f x * ((↑(algebraMapCLM ℝ≥0 𝕜)).comp g) x‖₊ ≤ ε / 2

Tactic:
have :=
        calc
          ‖((1 - (algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g) x : 𝕜)‖₊ =
              ‖1 - algebraMap ℝ≥0 𝕜 (g x)‖₊ := by
            simp only [coe_sub, coe_one, coe_comp, ContinuousMap.coe_coe, Pi.sub_apply,
              Pi.one_apply, Function.comp_apply, algebraMapCLM_apply]
          _ = ‖algebraMap ℝ≥0 𝕜 (1 - g x)‖₊ := by
            simp only [Algebra.algebraMap_eq_smul_one, NNReal.smul_def, NNReal.coe_sub (hg x),
              NNReal.coe_one, sub_smul, one_smul]
          _ ≤ 1 := (nnnorm_algebraMap_nnreal 𝕜 (1 - g x)).trans_le tsub_le_self

Goal state after:
case neg
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g : C(X, ℝ≥0)
hgI : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I
hg : ∀ (x : X), g x ≤ 1
hgt : Set.EqOn (⇑g) 1 t
x : X
hx : x ∉ t
this : ‖(1 - (↑(algebraMapCLM ℝ≥0 𝕜)).comp g) x‖₊ ≤ 1
⊢ ‖f x - f x * ((↑(algebraMapCLM ℝ≥0 𝕜)).comp g) x‖₊ ≤ ε / 2
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hU : s = ⋂ n, U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
n : ℕ
⊢ ∃ f, EqOn (⇑f) 1 s ∧ EqOn (⇑f) 0 (U n ∩ interior m)ᶜ ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
apply exists_continuous_one_zero_of_isCompact hs
      ((U_open n).inter isOpen_interior).isClosed_compl

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hU : s = ⋂ n, U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
n : ℕ
⊢ Disjoint s (U n ∩ interior m)ᶜ
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: case refine_4
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
hx : x ∈ setOfIdeal I
⊢ ∃ t_1 ∈ nhdsWithin x t, ∃ g', (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I ∧ ∀ x ∈ t_1, 0 < g' x

Tactic:
mem_setOfIdeal

Goal state after:
case refine_4
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
x : X
hx : ∃ f ∈ I, f x ≠ 0
⊢ ∃ t_1 ∈ nhdsWithin x t, ∃ g', (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I ∧ ∀ x ∈ t_1, 0 < g' x
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g' : C(X, ℝ≥0)
hI' : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I
hgt' : ∀ x ∈ t, 0 < g' x
c : ℝ≥0
hc : c > 0
hgc' : t ⊆ {y | c ≤ g' y}
g : C(X, ℝ≥0)
hg : ∀ (x : X), (g * g') x ≤ 1
hgc : Set.EqOn (⇑(g * g')) 1 {x | c ≤ g' x}
⊢ ∃ g, (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I ∧ (∀ (x : X), g x ≤ 1) ∧ Set.EqOn (⇑g) 1 t

Tactic:
refine ⟨g * g', ?_, hg, hgc.mono hgc'⟩

Goal state after:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g' : C(X, ℝ≥0)
hI' : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I
hgt' : ∀ x ∈ t, 0 < g' x
c : ℝ≥0
hc : c > 0
hgc' : t ⊆ {y | c ≤ g' y}
g : C(X, ℝ≥0)
hg : ∀ (x : X), (g * g') x ≤ 1
hgc : Set.EqOn (⇑(g * g')) 1 {x | c ≤ g' x}
⊢ (↑(algebraMapCLM ℝ≥0 𝕜)).comp (g * g') ∈ I
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure
hS : IsClosed ↑S
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative ↥(adjoin ℂ {a, b})
⊢ ‖a + b‖ = max ‖a‖ ‖b‖

Tactic:
let _ : NonUnitalCommRing S := (adjoin ℂ {a, b}).nonUnitalCommRingTopologicalClosure mul_comm

Goal state after:
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsStarNormal a
hb : IsStarNormal b
hcomm : Commute a b
hab : a * b = 0
S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure
hS : IsClosed ↑S
hcomm₁ : Commute (star a) b
hcomm₂ : Commute a (star b)
this : IsMulCommutative ↥(adjoin ℂ {a, b})
x✝ : NonUnitalCommRing ↥S := (adjoin ℂ {a, b}).nonUnitalCommRingTopologicalClosure ⋯
⊢ ‖a + b‖ = max ‖a‖ ‖b‖
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : T2Space A
inst✝ : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
⊢ (r • a)⁻ = -r • a⁺

Tactic:
conv_lhs => rw [← neg_neg r, neg_smul, negPart_neg, posPart_smul_of_nonneg (by simpa)]

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

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
a : A
n : ℕ
ha : 0 ≤ a
⊢ a ^ ↑n = a ^ n

Tactic:
← cfc_pow_id (R := ℝ≥0) a n,

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
a : A
n : ℕ
ha : 0 ≤ a
⊢ a ^ ↑n = cfc (fun x ↦ x ^ n) a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarRing A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ ℝ≥0 a)
hg0 : g 0 = 0
⊢ cfcₙ (fun x ↦ f x - g x) a = cfcₙ f a - cfcₙ g a

Tactic:
have ha' := QuasispectrumRestricts.nnreal_of_nonneg ha

Goal state after:
A : Type u_1
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarRing A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ ℝ≥0 a)
hg0 : g 0 = 0
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ cfcₙ (fun x ↦ f x - g x) a = cfcₙ f a - cfcₙ g a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : Nontrivial A
a : A
ha : IsSelfAdjoint a
⊢ ‖a‖ ∈ spectrum ℝ a ∨ -‖a‖ ∈ spectrum ℝ a

Tactic:
have ha' : SpectrumRestricts a Complex.reCLM := ha.spectrumRestricts
  rw [← ha.toReal_spectralRadius_eq_norm]
  exact Real.spectralRadius_mem_spectrum_or (ha'.image ▸ (spectrum.nonempty a).image _)

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : 1 ≤ ↑a⁻¹
⊢ ↑a ≤ 1

Tactic:
by
  simpa using CStarAlgebra.inv_le_one ha

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
b a : Aˣ
ha : IsStrictlyPositive ↑a
hab : ↑a ≤ ↑b
⊢ ↑b ^ (-1) ≤ ↑a⁻¹

Tactic:
rpow_neg_one_eq_inv b (ha.nonneg.trans hab)

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
b a : Aˣ
ha : IsStrictlyPositive ↑a
hab : ↑a ≤ ↑b
⊢ ↑b⁻¹ ≤ ↑a⁻¹
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:

Tactic:
_ ≤ ‖w‖ * ‖v‖ := norm_inner_le E
      _ ≤ 1 * ‖v‖ := by gcongr
      _ = ‖v‖ := by simp

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

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.univ.sup fun i ↦ ∑ k, ∑ j, ‖A i j‖₊ * ‖B j k‖₊) = Finset.univ.sup fun i ↦ ∑ j, ‖A i j‖₊ * ∑ k, ‖B j k‖₊

Tactic:
simp_rw [@Finset.sum_comm m, Finset.mul_sum]

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

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN : ∀ (x : n → α), ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N * ‖x‖₊
i : m
x✝ : i ∈ Finset.univ
⊢ ∑ j, ‖A i j‖₊ ≤ N

Tactic:
cases isEmpty_or_nonempty n

Goal state after:
case inl
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN : ∀ (x : n → α), ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N * ‖x‖₊
i : m
x✝ : i ∈ Finset.univ
h✝ : IsEmpty n
⊢ ∑ j, ‖A i j‖₊ ≤ N

case inr
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN : ∀ (x : n → α), ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N * ‖x‖₊
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
⊢ ∑ j, ‖A i j‖₊ ≤ N
Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap

Goal state before:
pp: case a
B₁ : Type u_3
B₂ : Type u_4
inst✝⁵ : CStarAlgebra B₁
inst✝⁴ : CStarAlgebra B₂
inst✝³ : PartialOrder B₁
inst✝² : PartialOrder B₂
inst✝¹ : StarOrderedRing B₁
inst✝ : StarOrderedRing B₂
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : 0 ≤ x
⊢ x ≤ (algebraMap ℂ B₁) ↑‖x‖

Tactic:
exact IsSelfAdjoint.le_algebraMap_norm_self <| .of_nonneg hx

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝¹ m✝ : A
ε : ℝ≥0
hε : 0 < ε
x✝ : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun y ↦ 1 - (1 + y)⁻¹
hx₁ : cfc g (ε⁻¹ ^ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) (σ ℝ≥0 m)
hx : x ∈ Set.Icc 0 1
hx' : x ∈ Set.Icc (cfc g (ε⁻¹ ^ 2 • m)) 1
⊢ ‖star m * (1 - cfc g (ε⁻¹ ^ 2 • m)) * m‖₊ ≤ ε ^ 2

Tactic:
suffices star m * (1 - cfc g (ε⁻¹ ^ 2 • m)) * m =
      cfc (fun y : ℝ≥0 ↦ y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y) m by
    rw [this]
    refine nnnorm_cfc_nnreal_le fun y hy ↦ ?_
    calc
      y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y = y * ε ^ 2 * (y / (ε ^ 2 + y)) := by simp [field]
      _ ≤ ε ^ 2 * 1 := by
        gcongr
        · apply mul_le_of_le_one_left'
          have hm' := hm₂.le
          rw [norm_le_one_iff_of_nonneg m hm₁, ← cfc_id' ℝ≥0 m, ← cfc_one (R := ℝ≥0) m,
            cfc_nnreal_le_iff _ _ _ (QuasispectrumRestricts.nnreal_of_nonneg hm₁)] at hm'
          exact hm' y hy
        · exact div_le_one (by positivity) |>.mpr le_add_self
      _ = ε ^ 2 := mul_one _

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝¹ m✝ : A
ε : ℝ≥0
hε : 0 < ε
x✝ : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun y ↦ 1 - (1 + y)⁻¹
hx₁ : cfc g (ε⁻¹ ^ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) (σ ℝ≥0 m)
hx : x ∈ Set.Icc 0 1
hx' : x ∈ Set.Icc (cfc g (ε⁻¹ ^ 2 • m)) 1
⊢ star m * (1 - cfc g (ε⁻¹ ^ 2 • m)) * m = cfc (fun y ↦ y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y) m
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : TopologicalSpace Y
E : Type u_3
inst✝¹ : NormedAddCommGroup E
s : Set Y
inst✝ : CompactSpace ↑s
f : X → Y → E
g : C(↑s, E)
f_ae_contOn : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) s
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ y ∈ s, ‖f x y‖ ≤ bound x
⊢ HasFiniteIntegral (fun x ↦ mkD (s.domRestrict (f x)) g) μ

Tactic:
refine hasFiniteIntegral_mkD_of_bound _ _ ?_ bound bound_int ?_
  · simpa [← continuousOn_iff_continuous_domRestrict]
  · simpa

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : Algebra 𝕜 A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarModule 𝕜 A
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : ContinuousStar A
a : A
ha : p a
⊢ StarSubalgebra.map (cfcHom ha)
      (adjoin 𝕜 {ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜)}).topologicalClosure =
    elemental 𝕜 a

Tactic:
← StarSubalgebra.topologicalClosure_map _ _ (cfcHom_isClosedEmbedding ha (R := 𝕜)).isClosedMap
      (cfcHom_continuous ha),

Goal state after:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : Algebra 𝕜 A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarModule 𝕜 A
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : ContinuousStar A
a : A
ha : p a
⊢ (StarSubalgebra.map (cfcHom ha)
        (adjoin 𝕜 {ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜)})).topologicalClosure =
    elemental 𝕜 a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module ℂ A
inst✝⁵ : IsScalarTower ℂ A A
inst✝⁴ : SMulCommClass ℂ A A
inst✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMapZero.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (quasispectrum ℝ ↑(ℑ a))
hf0 : f 0 = 0
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.im) '' quasispectrum ℂ a)
| cfcₙ f ↑(ℑ a)

Tactic:
rw [cfcₙ_real_eq_complex, ← cfcₙ_im_id a, ← cfcₙ_comp' ..]

Goal state after:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module ℂ A
inst✝⁵ : IsScalarTower ℂ A A
inst✝⁴ : SMulCommClass ℂ A A
inst✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMapZero.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (quasispectrum ℝ ↑(ℑ a))
hf0 : f 0 = 0
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.im) '' quasispectrum ℂ a)
| cfcₙ (fun x ↦ ↑(f (↑x.im).re)) a
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
⊢ ∃ a, (toDualMap 𝕜 E) a = ℓ

Tactic:
set Y := ℓ.ker

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
⊢ ∃ a, (toDualMap 𝕜 E) a = ℓ
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: case refine_1
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
x : EuclideanSpace 𝕜 n
⊢ ‖T x‖ ^ 2 ≤ (‖v‖ * ‖x‖) ^ 2

Tactic:
simp only [(T x).norm_sq_eq, ofLp_toEuclideanCLM, mulVec_diagonal, norm_mul, T]

Goal state after:
case refine_1
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
x : EuclideanSpace 𝕜 n
⊢ ∑ x_1, (‖v x_1‖ * ‖x.ofLp x_1‖) ^ 2 ≤ (‖v‖ * ‖x‖) ^ 2
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ ↑e.symm) (↑e z)
⊢ z ∈ e.symm.target

Tactic:
rw [PartialEquiv.symm_target, e.mem_source]

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ ↑e.symm) (↑e z)
⊢ proj z ∈ e.baseSet
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: case refine_3
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst✝³] s
hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯
⊢ z ∈ e.source

Tactic:
· rw [e.mem_source]
    exact a.mem_base_pretrivializationAt z.proj

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊
⊢ ‖f‖₊ ≤ C

Tactic:
have h1 b : C * ‖f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2 := by grw [f.le_opNNNorm b]; ring_nf; rfl

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊
h1 : ∀ (b : A), C * ‖f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
⊢ ‖f‖₊ ≤ C