mathlib-initiative/mathlib-tactics huggingface dataset:
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‖₊ < ε

Tactic:
· refine lt_of_le_of_lt ?_ (half_lt_self hε)
      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
      calc
        ‖f x - f x * (algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g x‖₊ =
            ‖f x * (1 - (algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g) x‖₊ := by
          simp only [mul_sub, coe_sub, coe_one, Pi.sub_apply, Pi.one_apply, mul_one]
        _ ≤ ε / 2 * ‖(1 - (algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g) x‖₊ :=
          ((nnnorm_mul_le _ _).trans
            (mul_le_mul_left (not_le.mp <| show ¬ε / 2 ≤ ‖f x‖₊ from hx).le _))
        _ ≤ ε / 2 := by simpa only [mul_one] using! mul_le_mul_right this _

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case refine_4
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ᶜ
f : ℕ → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s
fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)
f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : ∑' (i : ℕ), u i = 1
g : X → ℝ := fun x ↦ ∑' (n : ℕ), u n * (f n) x
hgmc : EqOn g 0 mᶜ
I : ∀ (n : ℕ) (x : X), u n * (f n) x ≤ u n
S : ∀ (x : X), Summable fun n ↦ u n * (f n) x
x : X
⊢ 0 ≤ { toFun := g, continuous_toFun := ⋯ } x

pp: case refine_5
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ᶜ
f : ℕ → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s
fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)
f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : ∑' (i : ℕ), u i = 1
g : X → ℝ := fun x ↦ ∑' (n : ℕ), u n * (f n) x
hgmc : EqOn g 0 mᶜ
I : ∀ (n : ℕ) (x : X), u n * (f n) x ≤ u n
S : ∀ (x : X), Summable fun n ↦ u n * (f n) x
x : X
⊢ { toFun := g, continuous_toFun := ⋯ } x ≤ 1

Tactic:
· exact tsum_nonneg (fun n ↦ mul_nonneg (u_pos n).le (f_range n x).1)

Goal state after:
case refine_5
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ᶜ
f : ℕ → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s
fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)
f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : ∑' (i : ℕ), u i = 1
g : X → ℝ := fun x ↦ ∑' (n : ℕ), u n * (f n) x
hgmc : EqOn g 0 mᶜ
I : ∀ (n : ℕ) (x : X), u n * (f n) x ≤ u n
S : ∀ (x : X), Summable fun n ↦ u n * (f n) x
x : X
⊢ { toFun := g, continuous_toFun := ⋯ } x ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: case refine_1
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 ⋯
x✝ : NonUnitalCommCStarAlgebra ↥S :=
  { toNonUnitalNormedRing := (nonUnitalCStarAlgebra S).toNonUnitalNormedRing, mul_comm := ⋯,
    toStarRing := (nonUnitalCStarAlgebra S).toStarRing, toCompleteSpace := ⋯, toCStarRing := ⋯,
    toNormedSpace := (nonUnitalCStarAlgebra S).toNormedSpace, toIsScalarTower := ⋯, toSMulCommClass := ⋯,
    toStarModule := ⋯ }
⊢ a ∈ S

pp: case refine_2
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 ⋯
x✝ : NonUnitalCommCStarAlgebra ↥S :=
  { toNonUnitalNormedRing := (nonUnitalCStarAlgebra S).toNonUnitalNormedRing, mul_comm := ⋯,
    toStarRing := (nonUnitalCStarAlgebra S).toStarRing, toCompleteSpace := ⋯, toCStarRing := ⋯,
    toNormedSpace := (nonUnitalCStarAlgebra S).toNormedSpace, toIsScalarTower := ⋯, toSMulCommClass := ⋯,
    toStarModule := ⋯ }
⊢ b ∈ S

Tactic:
all_goals apply le_topologicalClosure; aesop

Goal state after:
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✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace ↑s
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
mul₁ : ∀ (f g : C(↑s, ℝ)₀), (cfcₙHomSuperset hb' hbs) f * (cfcₙHomSuperset hc' hcs) g = 0
f g : C(↑s, ℝ)₀
⊢ (cfcₙHomSuperset hc' hcs) f * (cfcₙHomSuperset hb' hbs) g = 0

Tactic:
simpa only [star_mul, star_zero, ← map_star, star_trivial] using congr(star $(mul₁ g f))

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
ha₂ : ∀ x ∈ spectrum ℝ (-a), 0 ≤ x
⊢ spectrum ℝ a ⊆ {0}

Tactic:
rw [Set.subset_singleton_iff]

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
ha₂ : ∀ x ∈ spectrum ℝ (-a), 0 ≤ x
⊢ ∀ y ∈ spectrum ℝ a, y = 0
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
⊢ 1⁺ = 1

Tactic:
rw [CFC.posPart_def, cfcₙ_eq_cfc]
  simp

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Tactic:
have h_c_spec₀ : SpectrumRestricts (-(star c * c)) (ContinuousMap.realToNNReal ·) := by
    simp only [SpectrumRestricts.nnreal_iff, h_eq_negPart_a, CFC.negPart_def]
    rw [cfcₙ_eq_cfc (hf0 := by simp), ← cfc_pow (ha := ha) .., cfc_map_spectrum (ha := ha) ..]
    rintro - ⟨x, -, rfl⟩
    positivity

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x ↦ ContinuousMap.realToNNReal x
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
r : ℝ
⊢ ((algebraMap ℝ A) r)⁺ = (algebraMap ℝ A) r⁺

Tactic:
rw [CFC.posPart_def, cfcₙ_eq_cfc]
  simp

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
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
⊢ (a ^ x⁻¹) ^ x = a

Tactic:
simpa using rpow_rpow_inv a x⁻¹ (inv_ne_zero hx)

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

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
h : x ≠ 0
a : A
⊢ 0 ≤
    ‖x‖ ^ 2 •> (a * star a) - ‖x‖ ^ 2 •> (a * ⟪y, x⟫_A) - ‖x‖ ^ 2 •> (⟪x, y⟫_A * star a) +
      ‖x‖ ^ 2 •> ‖x‖ ^ 2 •> ⟪y, y⟫_A

Tactic:
by
      calc (0 : A) ≤ ⟪a • x - ‖x‖ ^ 2 • y, a • x - ‖x‖ ^ 2 • y⟫_A := by
                      exact inner_self_nonneg
            _ = a * ⟪x, x⟫ * star a - ‖x‖ ^ 2 • (a * ⟪y, x⟫)
                  - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := by
                      simp only [inner_sub_right, inner_op_smul_right, inner_sub_left,
                        inner_op_smul_left, inner_smul_left_real, mul_sub, mul_smul_comm,
                        inner_smul_right_real, smul_sub, mul_assoc]
                      abel
            _ ≤ ‖x‖ ^ 2 • (a * star a) - ‖x‖ ^ 2 • (a * ⟪y, x⟫)
                  - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := by
                      gcongr
                      calc _ ≤ ‖⟪x, x⟫_A‖ • (a * star a) :=
                          CStarAlgebra.star_right_conjugate_le_norm_smul
                        _ = (√‖⟪x, x⟫_A‖) ^ 2 • (a * star a) := by
                          rw [Real.sq_sqrt]
                          positivity
                        _ = ‖x‖ ^ 2 • (a * star a) := by rw [← norm_eq_sqrt_norm_inner_self]

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

Goal state before:
pp: case refine_1
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
⊢ ‖‖v‖⁻¹ •> v‖ ≤ 1

pp: case refine_2
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
⊢ ‖⟪‖v‖⁻¹ •> v, v⟫_A‖ = ‖v‖

pp: case refine_3
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
⊢ ‖v‖ ∈ upperBounds {x | ∃ w, ∃ (_ : ‖w‖ ≤ 1), ‖⟪w, v⟫_A‖ = x}

Tactic:
· simpa only [norm_smul, norm_inv, norm_norm] using inv_mul_le_one_of_le₀ le_rfl (by positivity)

Goal state after:
case refine_2
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
⊢ ‖⟪‖v‖⁻¹ •> v, v⟫_A‖ = ‖v‖

case refine_3
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
⊢ ‖v‖ ∈ upperBounds {x | ∃ w, ∃ (_ : ‖w‖ ≤ 1), ‖⟪w, v⟫_A‖ = x}
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
c : Unitization ℂ A
hc : 0 ≤ c
⊢ 1 - cfc (fun x ↦ x⁻¹) (1 + cfc (fun x ↦ x) c) = 1 - cfc (fun x ↦ x⁻¹) (1 + c)

pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
c : Unitization ℂ A
hc : 0 ≤ c
⊢ ContinuousOn (fun x ↦ x⁻¹) ((fun x ↦ 1 + x) '' σ ℝ≥0 c)

Tactic:
cfc_id' ℝ≥0 c

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
c : Unitization ℂ A
hc : 0 ≤ c
⊢ 1 - cfc (fun x ↦ x⁻¹) (1 + c) = 1 - cfc (fun x ↦ x⁻¹) (1 + c)

A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
c : Unitization ℂ A
hc : 0 ≤ c
⊢ ContinuousOn (fun x ↦ x⁻¹) ((fun x ↦ 1 + x) '' σ ℝ≥0 c)
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
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ : cfcₙ (fun y ↦ 1 - (1 + y)⁻¹) (ε⁻¹ ^ 2 • m) ≤ x
hx₂ : x ∈ closedBall 0 1
⊢ x * m ∈ closedBall m ↑ε

Tactic:
simp only [mem_closedBall, dist_eq_norm', zero_sub, norm_neg] at hx₂ ⊢

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝ m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ : cfcₙ (fun y ↦ 1 - (1 + y)⁻¹) (ε⁻¹ ^ 2 • m) ≤ x
hx₂ : ‖x‖ ≤ 1
⊢ ‖m - x * m‖ ≤ ↑ε
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
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ : cfcₙ (fun y ↦ 1 - (1 + y)⁻¹) (ε⁻¹ ^ 2 • m) ≤ x
hx₂ : ‖x‖ ≤ 1
⊢ ↑‖m - x * m‖₊ ≤ ↑ε

Tactic:
coe_le_coe

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝ m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ : cfcₙ (fun y ↦ 1 - (1 + y)⁻¹) (ε⁻¹ ^ 2 • m) ≤ x
hx₂ : ‖x‖ ≤ 1
⊢ ‖m - x * m‖₊ ≤ ε
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero

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
t : Set Y
inst✝⁴ : CompactSpace ↑t
inst✝³ : Zero ↑t
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(↑t, E)
f : X → Y → E
g : C(↑t, E)₀
f_cont : ContinuousOn (Function.uncurry f) (univ ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ, f x ↑0 = 0
⊢ AEStronglyMeasurable (fun x ↦ mkD (t.domRestrict (f x)) g) μ

Tactic:
rw [← ContinuousMapZero.isEmbedding_toContinuousMap.aestronglyMeasurable_comp_iff]
  refine aestronglyMeasurable_congr ?_ |>.mp <|
    ContinuousMap.aeStronglyMeasurable_mkD_restrict_of_uncurry f g f_cont
  filter_upwards [f_zero] with x zero_x
  rw [mkD_eq_mkD_of_map_zero _ _ zero_x]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁷ : Fintype n
inst✝⁶ : Semiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : Module R A
inst✝³ : Star A
inst✝² : NonUnitalNonAssocSemiring B
inst✝¹ : Module R B
inst✝ : Star B
f : A →⋆ₙₐ[R] B
M : CStarMatrix n n A
⊢ (mapₗ ↑f) (star M) = star ((mapₗ ↑f) M)

Tactic:
by ext; simp [map, star_apply, map_star]

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
x y : M
hx : ‖x‖ = 0
hy : ‖y‖ = 0
⊢ ‖x‖ + ‖y‖ = 0

Tactic:
hx,

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
x y : M
hx : ‖x‖ = 0
hy : ‖y‖ = 0
⊢ 0 + ‖y‖ = 0
Module: Mathlib.Analysis.Normed.Group.NullSubmodule

Goal state before:
pp: M : Type u_1
inst✝⁴ : SeminormedCommGroup M
𝕜 : Type u_2
E : Type u_3
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
c : 𝕜
x : E
hx : ‖x‖ = 0
⊢ ‖c‖ * ‖x‖ = 0

Tactic:
hx,

Goal state after:
M : Type u_1
inst✝⁴ : SeminormedCommGroup M
𝕜 : Type u_2
E : Type u_3
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
c : 𝕜
x : E
hx : ‖x‖ = 0
⊢ ‖c‖ * 0 = 0
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x

Tactic:
mem_extremePoints

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
⊢ (x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) ↔
    x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b✝ : B
a : F
b : B
x : Z.Fiber b
⊢ 𝓝 x = 𝓝 x ⊓ ⊤

Tactic:
inf_top_eq

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b✝ : B
a : F
b : B
x : Z.Fiber b
⊢ 𝓝 x = 𝓝 x
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case neg
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
hl : ¬∀ᶠ (x : α) in l, f x ∈ e.source
⊢ ((Tendsto (fun n ↦ ((↑e ∘ f) n).1) l (𝓝 (proj z)) ∧ Tendsto (fun n ↦ ((↑e ∘ f) n).2) l (𝓝 (↑e z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x ↦ (↑e (f x)).2) l (𝓝 (↑e z).2)

Tactic:
· simp only [hl, and_false, false_iff, not_and]
    rw [e.source_eq] at hl hz
    exact fun h _ ↦ hl <| h <| e.open_baseSet.mem_nhds hz

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

Goal state before:
pp: case snd
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ (↑𝕜 x).toProd.2 = ((algebraMap 𝕜 𝓜(𝕜, 𝕜)) x).toProd.2

Tactic:
· refine ContinuousLinearMap.ext fun y => ?_
    exact mul_comm y x

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CStarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : (Metric.closedBall 0 1).Nonempty
key : ∀ (x y : A), ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖a.toProd.2 (star (a.toProd.1 (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
x : A
hx : x ∈ Metric.closedBall 0 1
y : A
hy : y ∈ Metric.closedBall 0 1
⊢ (fun x_1 ↦ ‖a.toProd.2 (star (a.toProd.1 (star x))) * x_1‖₊) y ≤ ‖a‖₊ * ‖a‖₊

Tactic:
exact key x y (mem_closedBall_zero_iff.1 hx) (mem_closedBall_zero_iff.1 hy)

Goal state after:
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: case refine_1
E : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G E
hf : IsQuotientMap f
inst✝² : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst✝¹ : TopologicalSpace G
inst✝ : DiscreteTopology G
U : Set E
open_U : IsOpen[inst✝⁶] U
disjoint : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ g, (fun x ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst✝⁶] (f ⁻¹' W ∩ (fun x ↦ g • x) ⁻¹' U)
e : E
hW : e ∈ f ⁻¹' W
⊢ e ∈ ⋃ i, (fun x ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun x ↦ g • x) ⁻¹' U)

Tactic:
have ⟨e', he', hfe⟩ := hWU hW
      obtain ⟨g', rfl⟩ := hfG.mp hfe
      refine ⟨_, ⟨g⁻¹ * g', rfl⟩, ?_, ?_⟩
      · apply Set.mem_of_eq_of_mem (pGE _ e) hW
      · apply Set.mem_of_eq_of_mem _ he'; simp_rw [mul_smul, smul_inv_smul]

Goal state after:
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: case refine_5
E : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G E
hf : IsQuotientMap f
inst✝² : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst✝¹ : TopologicalSpace G
inst✝ : DiscreteTopology G
U : Set E
open_U : IsOpen[inst✝⁶] U
disjoint : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ g, (fun x ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g₁ g₂ : G
hne : g₁ ≠ g₂
e : E
x✝ : e ∈ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₁ ⊓ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₂
h₁ : e ∈ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₁
h₂ : e ∈ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₂
⊢ (fun x ↦ (g₁ * g₂⁻¹) • x) ((fun x ↦ g₂ • x) e) = (fun x ↦ g₁ • x) e

Tactic:
· simp_rw [mul_smul, inv_smul_smul]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: n : ℤ
inst✝ : NeZero n
hn : IsUnit ↑n
e : AddCircle 1 ≃ₜ Circle := homeomorphCircle ⋯
x✝ : ℝ
⊢ ∀ ⦃a₂ : ℝ⦄, (fun x ↦ n • x) x✝ = (fun x ↦ n • x) a₂ → x✝ = a₂

Tactic:
simp [NeZero.ne]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : t ∈ Set.Icc 0 1
hu : ‖↑u - 1‖ < 2
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
⊢ 2 * (1 - Real.cos ‖t • argSelfAdjoint u‖) ≤ ‖↑u - 1‖ ^ 2

Tactic:
trans 2 * (1 - Real.cos ‖argSelfAdjoint u‖)

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : t ∈ Set.Icc 0 1
hu : ‖↑u - 1‖ < 2
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
⊢ 2 * (1 - Real.cos ‖t • argSelfAdjoint u‖) ≤ 2 * (1 - Real.cos ‖argSelfAdjoint u‖)

A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : t ∈ Set.Icc 0 1
hu : ‖↑u - 1‖ < 2
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
⊢ 2 * (1 - Real.cos ‖argSelfAdjoint u‖) ≤ ‖↑u - 1‖ ^ 2