mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: case neg
A : Type u_2
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
a✝ : Nontrivial A
x : ℝ
r : ℝˣ
hr : 0 ≤ ↑r
hx : r⁻¹ • x ∈ spectrum ℝ a
hr' : ¬↑r = 0
⊢ (↑r)⁻¹ • 0 ≤ (↑r)⁻¹ • x

Tactic:
simpa [Units.smul_def] using ha _ hx

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : CStarRing A
inst✝⁵ : NormedSpace ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
⊢ ‖star b * a * b‖ = ‖sqrt a * b‖ ^ 2

Tactic:
sq,

Goal state after:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : CStarRing A
inst✝⁵ : NormedSpace ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
⊢ ‖star b * a * b‖ = ‖sqrt a * b‖ * ‖sqrt a * b‖
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
⊢ (a ^ (1 / 2)) ^ x = a ^ (x / 2)

Tactic:
nnrpow_nnrpow,

Goal state after:
A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
⊢ a ^ (1 / 2 * x) = a ^ (x / 2)
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 b : A
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ^ 2 = b ^ 2 ↔ a = b

Tactic:
sq,

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✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a * a = b * b ↔ a = b
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 : 0 ≤ a
b : Aˣ
hb : IsStrictlyPositive ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
| ‖sqrt a * ↑b ^ (-(1 / 2))‖ ^ 2 ≤ 1

Tactic:
sq,

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : IsStrictlyPositive ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
| ‖sqrt a * ↑b ^ (-(1 / 2))‖ * ‖sqrt a * ↑b ^ (-(1 / 2))‖ ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖sqrt ↑a * sqrt ↑b⁻¹‖ ^ 2 ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ↑b⁻¹ ≤ ↑a⁻¹

Tactic:
sq,

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖sqrt ↑a * sqrt ↑b⁻¹‖ * ‖sqrt ↑a * sqrt ↑b⁻¹‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ↑b⁻¹ ≤ ↑a⁻¹
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖star (sqrt ↑a * sqrt ↑b⁻¹) * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ‖sqrt ↑b⁻¹ * sqrt ↑a‖ ^ 2 ≤ 1

Tactic:
sq,

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖star (sqrt ↑a * sqrt ↑b⁻¹) * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ‖sqrt ↑b⁻¹ * sqrt ↑a‖ * ‖sqrt ↑b⁻¹ * sqrt ↑a‖ ≤ 1
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) ≤ 1

Tactic:
by
  lift a to Aˣ using isUnit_of_le 1 ha
  rw [rpow_neg_one_eq_inv a (zero_le_one.trans ha)]
  exact inv_le_one ha

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

Goal state before:
pp: A : Type u_2
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ c ^ 2
⊢ ‖(1 - y) * z‖₊ ^ 2 ≤ c ^ 2

Tactic:
sq,

Goal state after:
A : Type u_2
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ c ^ 2
⊢ ‖(1 - y) * z‖₊ * ‖(1 - y) * z‖₊ ≤ c ^ 2
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: case e_f.refine_1
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i j : n
hj : j ∈ Finset.univ
⊢ ‖diagonal v i j‖₊ ≤ ‖v i‖₊

Tactic:
obtain rfl | hij := eq_or_ne i j

Goal state after:
case e_f.refine_1.inl
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i : n
hj : i ∈ Finset.univ
⊢ ‖diagonal v i i‖₊ ≤ ‖v i‖₊

case e_f.refine_1.inr
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i j : n
hj : j ∈ Finset.univ
hij : i ≠ j
⊢ ‖diagonal v i j‖₊ ≤ ‖v i‖₊
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✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ NNReal.sqrt (∑ x, NNReal.sqrt (∑ x_1, ‖A x x_1‖₊ ^ 2) ^ 2) = (∑ i, ∑ j, ‖A i j‖₊ ^ 2) ^ (1 / 2)

Tactic:
NNReal.sq_sqrt,

Goal state after:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ NNReal.sqrt (∑ x, ∑ x_1, ‖A x x_1‖₊ ^ 2) = (∑ i, ∑ j, ‖A i j‖₊ ^ 2) ^ (1 / 2)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: case frequently
𝕜 : 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✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C(↑(spectrum 𝕜 a), 𝕜)
hf : ∃ᶠ (g : C(↑(spectrum 𝕜 a), 𝕜)) in nhds f, Commute ((cfcHom ha) g) b
⊢ Filter.Tendsto (⇑(cfcHom ha)) (nhds f) (nhds ((cfcHom ha) f))

Tactic:
exact cfcHom_continuous ha |>.tendsto _

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

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
ha_cont : ContinuousOn a Set.univ
hs : ∀ (x : X), IsCompact (s x)
ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
hf : ∀ (x : X), ContinuousOn f (s x)
hf0 : f 0 = 0
ha' : ∀ (x : X), p (a x)
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) Set.univ

Tactic:
exact ha_cont.cfcₙ f (fun x _ ↦ hs x) (fun x _ ↦ by simpa using ha x) (fun x _ ↦ ha' x)

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

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_5
inst✝¹ : Fintype m
inst✝ : NonUnitalCStarAlgebra A
M : CStarMatrix m n A
h : toCLM M = 0
i : m
j : n
⊢ ‖M i j‖ ^ 2 = 0

Tactic:
sq,

Goal state after:
m : Type u_1
n : Type u_2
A : Type u_5
inst✝¹ : Fintype m
inst✝ : NonUnitalCStarAlgebra A
M : CStarMatrix m n A
h : toCLM M = 0
i : m
j : n
⊢ ‖M i j‖ * ‖M i j‖ = 0
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: case inr
m : Type u_1
n : Type u_2
A : Type u_5
inst✝⁴ : Fintype m
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype n
M : CStarMatrix m n A
C : ℝ≥0
h : ∀ (v : C⋆ᵐᵒᵈ(A, m → A)) (w : C⋆ᵐᵒᵈ(A, n → A)), ‖⟪w, (toCLM M) v⟫_A‖ ≤ ↑C * ‖v‖ * ‖w‖
v : C⋆ᵐᵒᵈ(A, m → A)
h₀ : 0 < ‖(toCLM M) v‖
⊢ ‖(toCLM M) v‖ * ‖(toCLM M) v‖ ≤ ↑C * ‖v‖ * ‖(toCLM M) v‖

Tactic:
simpa [← sq, norm_sq_eq A] using h ..

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

Goal state before:
pp: A : Type u_1
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
M : CStarMatrix n n A
v : C⋆ᵐᵒᵈ(A, n → A)
⊢ ‖v‖ * ‖(toCLM Mᴴ) ((toCLM M) v)‖ ≤ ‖v‖ * ‖toCLM Mᴴ ∘SL toCLM M‖ * ‖v‖

Tactic:
rw [mul_assoc]

Goal state after:
A : Type u_1
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
M : CStarMatrix n n A
v : C⋆ᵐᵒᵈ(A, n → A)
⊢ ‖v‖ * ‖(toCLM Mᴴ) ((toCLM M) v)‖ ≤ ‖v‖ * (‖toCLM Mᴴ ∘SL toCLM M‖ * ‖v‖)
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: case refine_1.a
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module 𝕜 (M i)
s : (i : ι) → Set (M i)
x : (i : ι) → M i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → M i),
    (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x
i : ι
x₁ : M i
hx₁ : x₁ ∈ s i
x₂ : M i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
⊢ ∀ (i_1 : ι), update x i x₂ i_1 ∈ s i_1

Tactic:
rintro j
      obtain rfl | hji := eq_or_ne j i <;> simp [*]

Goal state after:
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module 𝕜 (M i)
s : (i : ι) → Set (M i)
x : (i : ι) → M i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → M i),
    (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x
i : ι
x₁ : M i
hx₁ : x₁ ∈ s i
x₂ : M i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
⊢ ∀ (i_1 : ι), update x i x₁ i_1 ∈ s i_1

Tactic:
rintro j
      obtain rfl | hji := eq_or_ne j i <;> simp [*]

Goal state after:
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
hA : Convex 𝕜 A
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A \ (convexHull 𝕜) (A \ {x})

Tactic:
rw [hA.mem_extremePoints_iff_convex_sdiff, hA.convex_remove_iff_notMem_convexHull_remove,
    mem_sdiff]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a : A
x : f.PreGNS
⊢ star (f.ofPreGNS x) * (star a * a) * f.ofPreGNS x ≤ ‖a‖ ^ 2 • star (f.ofPreGNS x) * f.ofPreGNS x

Tactic:
sq,

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a : A
x : f.PreGNS
⊢ star (f.ofPreGNS x) * (star a * a) * f.ofPreGNS x ≤ (‖a‖ * ‖a‖) • star (f.ofPreGNS x) * f.ofPreGNS x
Module: Mathlib.Analysis.Normed.Field.UnitBall

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
x y : ↑(sphere 0 1)
⊢ ‖↑x‖ / ‖↑y‖ = 1

Tactic:
mem_sphere_zero_iff_norm.1 x.2,

Goal state after:
𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
x y : ↑(sphere 0 1)
⊢ 1 / ‖↑y‖ = 1
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set Y
hs : IsOpen[inst✝] s
⊢ e.source ∩ ↑e ⁻¹' (ofSet s hs).source = (e.restr (↑e ⁻¹' s)).source

Tactic:
restr_source,

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set Y
hs : IsOpen[inst✝] s
⊢ e.source ∩ ↑e ⁻¹' (ofSet s hs).source = e.source ∩ interior (↑e ⁻¹' s)
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‖ ≤ ‖v‖ * ‖x‖

Tactic:
refine (sq_le_sq₀ (by positivity) (by positivity)).mp ?_

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
⊢ ‖T x‖ ^ 2 ≤ (‖v‖ * ‖x‖) ^ 2
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 : ι
p : B × F
hp : p ∈ Z.baseSet i ×ˢ univ
⊢ { proj := p.1, snd := Z.coordChange i (Z.indexAt p.1) p.1 p.2 } ∈ Z.proj ⁻¹' Z.baseSet i

Tactic:
simpa only [Set.mem_preimage, and_true, Set.mem_univ, Set.mem_prod] using hp

Goal state after:
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h :
  ∀ (a b : X) (b_1 : f a = f b),
    ⟨(a, b), b_1⟩ ∈ Function.pullbackDiagonal f → ∃ t ∈ 𝓝 a ×ˢ 𝓝 b, Subtype.val ⁻¹' t ⊆ Function.pullbackDiagonal f
x : X
t : Set (X × X)
ht : t ∈ 𝓝 x ×ˢ 𝓝 x
t_sub : Subtype.val ⁻¹' t ⊆ Function.pullbackDiagonal f
t₁ : Set X
h₁ : t₁ ∈ 𝓝 x
t₂ : Set X
h₂ : t₂ ∈ 𝓝 x
prod_sub : t₁ ×ˢ t₂ ⊆ t
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
exact ⟨t₁ ∩ t₂, Filter.inter_mem h₁ h₂,
      fun x₁ h₁ x₂ h₂ he ↦ @t_sub ⟨(x₁, x₂), he⟩ (prod_sub ⟨h₁.1, h₂.2⟩)⟩

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : IsLocalHomeomorphOn f s
x : X
hx : x ∈ s
⊢ ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.domRestrict f)

pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.domRestrict f)
x : X
hx : x ∈ s
⊢ ∃ e, x ∈ e.source ∧ f = ↑e

Tactic:
· obtain ⟨e, hxe, rfl⟩ := h x hx
    exact ⟨e.source, e.open_source.mem_nhds hxe, e.isOpenEmbedding_restrict⟩

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.domRestrict f)
x : X
hx : x ∈ s
⊢ ∃ e, x ∈ e.source ∧ f = ↑e
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case fst
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace F
proj : Z → B
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
inst✝¹ : LinearOrder B
inst✝ : OrderTopology B
e e' : Trivialization F proj
p : Z
He : proj p ∈ e.baseSet
He' : proj p ∈ e'.baseSet
⊢ (↑e p).1 = (↑(e'.transFiberHomeomorph (e'.coordChangeHomeomorph e He' He)) p).1

pp: case snd
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace F
proj : Z → B
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
inst✝¹ : LinearOrder B
inst✝ : OrderTopology B
e e' : Trivialization F proj
p : Z
He : proj p ∈ e.baseSet
He' : proj p ∈ e'.baseSet
⊢ (↑e p).2 = (↑(e'.transFiberHomeomorph (e'.coordChangeHomeomorph e He' He)) p).2

Tactic:
· simp [*]

Goal state after:
case snd
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace F
proj : Z → B
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
inst✝¹ : LinearOrder B
inst✝ : OrderTopology B
e e' : Trivialization F proj
p : Z
He : proj p ∈ e.baseSet
He' : proj p ∈ e'.baseSet
⊢ (↑e p).2 = (↑(e'.transFiberHomeomorph (e'.coordChangeHomeomorph e He' He)) p).2
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case snd
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace F
proj : Z → B
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
inst✝¹ : LinearOrder B
inst✝ : OrderTopology B
e e' : Trivialization F proj
p : Z
He : proj p ∈ e.baseSet
He' : proj p ∈ e'.baseSet
⊢ (↑e p).2 = (↑(e'.transFiberHomeomorph (e'.coordChangeHomeomorph e He' He)) p).2

Tactic:
· simp [*]

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
h : IsLocalHomeomorphOn f s
hs : IsOpen[inst✝¹] s
⊢ (∀ (a : ↑s), IsOpen[instTopologicalSpaceSubtype] {a}) → ∀ (a : ↑(f '' s)), IsOpen[instTopologicalSpaceSubtype] {a}

Tactic:
rintro hX ⟨_, x, hx, rfl⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
h : IsLocalHomeomorphOn f s
hs : IsOpen[inst✝¹] s
hX : ∀ (a : ↑s), IsOpen[instTopologicalSpaceSubtype] {a}
x : X
hx : x ∈ s
⊢ IsOpen[instTopologicalSpaceSubtype] {⟨f x, ⋯⟩}
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case inr
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp' : p ∈ e'.source
⊢ (e.source.piecewise (↑e) (↑e') p).1 = proj p

Tactic:
piecewise_eq_of_notMem,

Goal state after:
case inr
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp' : p ∈ e'.source
⊢ (↑e' p).1 = proj p

case inr.hi
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp' : p ∈ e'.source
⊢ p ∉ e.source
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
inst✝ : Nonempty I
h✝ : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝²] U
hfU : IsOpen[inst✝³] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
xi : X × I
⊢ xi ∈ U ×ˢ Set.univ →
    (if he : f ↑(H.symm (if hx : xi.1 ∈ U then ⟨xi.1, hx⟩ else ⟨x, hxU⟩, xi.2)) ∈ U then
        (↑(H ⟨↑(H.symm (if hx : xi.1 ∈ U then ⟨xi.1, hx⟩ else ⟨x, hxU⟩, xi.2)), he⟩).1,
          (H ⟨↑(H.symm (if hx : xi.1 ∈ U then ⟨xi.1, hx⟩ else ⟨x, hxU⟩, xi.2)), he⟩).2)
      else (x, Classical.arbitrary I)) =
      xi

Tactic:
rintro ⟨hx, -⟩; simpa [hx] using fun h ↦ (h (H.symm _).2).elim

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : IsTopologicalRing 𝕜
p : 𝕜
inst✝² : T0Space (AddCircle p)
inst✝¹ : Algebra ℚ 𝕜
n : ℕ
inst✝ : NeZero n
⊢ IsUnit ↑n

Tactic:
by
    convert! (Nat.cast_ne_zero.mpr <| NeZero.ne n).isUnit.map (algebraMap ℚ 𝕜); simp

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
f : E → X
h : ∀ (x : E), f x ∈ s
hf : IsCoveringMap fun x ↦ ⟨f x, ⋯⟩
⊢ f ⁻¹' s = Set.univ

Tactic:
by simpa [Set.range, Set.subset_def] using h

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ ‖a ^ 2‖ ≤ 1

Tactic:
sq,

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ ‖a * a‖ ≤ 1
Module: Mathlib.Analysis.Calculus.AddTorsor.AffineMap

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace 𝕜 W
n : WithTop ℕ∞
f : V →ᴬ[𝕜] W
⊢ ContDiff 𝕜 n ⇑f

Tactic:
f.decomp

Goal state after:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace 𝕜 W
n : WithTop ℕ∞
f : V →ᴬ[𝕜] W
⊢ ContDiff 𝕜 n (⇑f.contLinear + Function.const V (f 0))
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
⊢ star T * T - T * star T = 0 ↔ ∀ (v : E), ‖T v‖ = ‖(adjoint T) v‖

Tactic:
simp_rw [ContinuousLinearMap.ext_iff, ← coe_coe, toLinearMap_sub, ← LinearMap.ext_iff,
    toLinearMap_zero]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
⊢ ↑(star T * T) - ↑(T * star T) = 0 ↔ ∀ (v : E), ‖↑T v‖ = ‖↑(adjoint T) v‖
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
⊢ have this := ⋯;
  IsStarProjection (toContinuousLinearMap T) ↔ IsStarProjection T

Tactic:
simp [isStarProjection_iff, isSelfAdjoint_toContinuousLinearMap_iff,
    ← ContinuousLinearMap.isIdempotentElem_toLinearMap_iff]

Goal state after: