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

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Ring k
inst✝⁶ : PartialOrder k
inst✝⁵ : IsOrderedRing k
inst✝⁴ : AddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module k E
inst✝ : IsStrictOrderedModule k E
a a' b b' : E
r : k
ha : a < a'
hb : b < b'
h₀ : 0 ≤ r
h₁ : r ≤ 1
⊢ (lineMap a b) r < (lineMap a' b') r

Tactic:
rcases h₀.eq_or_lt with (rfl | h₀); · simpa
  exact (lineMap_mono_left ha.le h₁).trans_lt (lineMap_strict_mono_right hb h₀)

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case zero
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
⊢ approx 0 c x ≤ approx (0 + 1) c x

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case zero
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
c : CU P
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case refine_2
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
φ : ↑(characterSpace 𝕜 C(X, 𝕜))
x : X
hx : idealOfSet 𝕜 {x}ᶜ = RingHom.ker φ
⊢ ∃ a, (continuousMapEval X 𝕜) a = φ

Tactic:
refine ⟨x, CharacterSpace.ext_ker <| Ideal.ext fun f => ?_⟩

Goal state after:
case refine_2
X : Type u_1
𝕜 : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : RCLike 𝕜
φ : ↑(characterSpace 𝕜 C(X, 𝕜))
x : X
hx : idealOfSet 𝕜 {x}ᶜ = RingHom.ker φ
f : C(X, 𝕜)
⊢ f ∈ RingHom.ker ((continuousMapEval X 𝕜) x) ↔ f ∈ RingHom.ker φ
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
ha : ¬IsUnit a
⊢ ∃ f, f a = 0

Tactic:
obtain ⟨M, hM, haM⟩ := (span {a}).exists_le_maximal (span_singleton_ne_top ha)
  exact
    ⟨M.toCharacterSpace,
      M.toCharacterSpace_apply_eq_zero_of_mem
        (haM (mem_span_singleton.mpr ⟨1, (mul_one a).symm⟩))⟩

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

Goal state before:
pp: case zero
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ ∀ x ∈ spectrum ℝ 0, 0 ≤ x

Tactic:
| zero =>

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x y z : A
hxy : IsSelfAdjoint (y - x) ∧ QuasispectrumRestricts (y - x) ⇑ContinuousMap.realToNNReal
hyz : IsSelfAdjoint (z - y) ∧ QuasispectrumRestricts (z - y) ⇑ContinuousMap.realToNNReal
⊢ IsSelfAdjoint (z - x) ∧ QuasispectrumRestricts (z - x) ⇑ContinuousMap.realToNNReal

Tactic:
by
    simp +singlePass only [← Unitization.isSelfAdjoint_inr (R := ℂ),
      quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ] at hxy hyz ⊢
    exact ⟨by simpa using hyz.1.add hxy.1, by simpa using hyz.2.nnreal_add hyz.1 hxy.1 hxy.2⟩

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

Goal state before:
pp: case mpr.zero
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x p : A
⊢ IsSelfAdjoint 0 ∧ QuasispectrumRestricts 0 ⇑ContinuousMap.realToNNReal

Tactic:
| zero =>

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

Goal state before:
pp: case neg.inl
A : Type u_1
inst✝¹³ : NonUnitalCStarAlgebra A
R : Type u_2
inst✝¹² : Semifield R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : Algebra R ℂ
inst✝³ : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R A p
inst✝¹ : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst✝ : ContinuousMapZero.UniqueHom R (Unitization ℂ A)
hp : ∀ {a : A}, p' ↑a ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
hf : ¬ContinuousOn f (σₙ R a)
⊢ ↑0 = cfc f ↑a

Tactic:
inr_zero,

Goal state after:
case neg.inl
A : Type u_1
inst✝¹³ : NonUnitalCStarAlgebra A
R : Type u_2
inst✝¹² : Semifield R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : Algebra R ℂ
inst✝³ : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R A p
inst✝¹ : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst✝ : ContinuousMapZero.UniqueHom R (Unitization ℂ A)
hp : ∀ {a : A}, p' ↑a ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
hf : ¬ContinuousOn f (σₙ R a)
⊢ 0 = cfc f ↑a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: case neg.inr
A : Type u_1
inst✝¹³ : NonUnitalCStarAlgebra A
R : Type u_2
inst✝¹² : Semifield R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : Algebra R ℂ
inst✝³ : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R A p
inst✝¹ : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst✝ : ContinuousMapZero.UniqueHom R (Unitization ℂ A)
hp : ∀ {a : A}, p' ↑a ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
ha : ¬p a
⊢ ↑0 = cfc f ↑a

Tactic:
inr_zero,

Goal state after:
case neg.inr
A : Type u_1
inst✝¹³ : NonUnitalCStarAlgebra A
R : Type u_2
inst✝¹² : Semifield R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : Algebra R ℂ
inst✝³ : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R A p
inst✝¹ : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst✝ : ContinuousMapZero.UniqueHom R (Unitization ℂ A)
hp : ∀ {a : A}, p' ↑a ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
ha : ¬p a
⊢ 0 = cfc f ↑a
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
ha : 0 ≤ a
⊢ sqrt a = cfcₙ Real.sqrt a

Tactic:
by
  suffices cfcₙ (fun x : ℝ ↦ √x * √x) a = cfcₙ (fun x : ℝ ↦ x) a by
    rwa [cfcₙ_mul .., cfcₙ_id' ..,
      ← sqrt_eq_iff _ (hb := cfcₙ_nonneg (fun x _ ↦ Real.sqrt_nonneg x))] at this
  exact cfcₙ_congr fun x hx ↦ Real.mul_self_sqrt <| quasispectrum_nonneg_of_nonneg a ha x hx

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
⊢ Set.EqOn (fun a ↦ a ^ 0) (fun x ↦ 1) (Set.Ici 0)

Tactic:
intro a

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
⊢ a ∈ Set.Ici 0 → (fun a ↦ a ^ 0) a = (fun x ↦ 1) 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 : A
r : ℝ≥0
ha : 0 ≤ a
⊢ ‖a‖₊ ≤ r ↔ a ≤ (algebraMap ℝ≥0 A) r

Tactic:
by
  rw [← NNReal.coe_le_coe]
  exact norm_le_iff_le_algebraMap a r.2

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
⊢ AntitoneOn Ring.inverse {a | IsStrictlyPositive a}

Tactic:
intro a

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ a ∈ {a | IsStrictlyPositive a} → ∀ ⦃b : A⦄, b ∈ {a | IsStrictlyPositive a} → a ≤ b → Ring.inverse b ≤ Ring.inverse a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
ha : 0 ≤ a
hab : a ≤ b
⊢ ∀ (a b : Unitization ℂ A), 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖

Tactic:
intro a

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b : A
ha : 0 ≤ a✝
hab : a✝ ≤ b
a : Unitization ℂ A
⊢ ∀ (b : Unitization ℂ A), 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : IsSelfAdjoint b
⊢ ∀ (a b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)

Tactic:
intro a

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b : A
hb : IsSelfAdjoint b
a : Unitization ℂ A
⊢ ∀ (b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)
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
⊢ ‖⟪x, y⟫_A‖ ^ 2 = ‖⟪x, y⟫_A * ⟪y, x⟫_A‖

Tactic:
by
                rw [← star_inner x, CStarRing.norm_self_mul_star, pow_two]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a e : A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ ∀ (a e : Unitization ℂ A), IsStarProjection e → 0 ≤ a → a ≤ e → a * e = a

Tactic:
intro a

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ e : A
he : IsStarProjection e
ha : 0 ≤ a✝
hae : a✝ ≤ e
a : Unitization ℂ A
⊢ ∀ (e : Unitization ℂ A), IsStarProjection e → 0 ≤ a → a ≤ e → a * e = a
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ MonotoneOn (cfcₙ fun x ↦ 1 - (1 + x)⁻¹) (Set.Ici 0)

Tactic:
intro a

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ a ∈ Set.Ici 0 → ∀ ⦃b : A⦄, b ∈ Set.Ici 0 → a ≤ b → cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) a ≤ cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) b
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:
pp: A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul A (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
x✝ : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
⊢ ‖x i‖ ^ 2 ≤ ‖∑ i, ⟪x i, x i⟫_A‖

Tactic:
norm_sq_eq A

Goal state after:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul A (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
x✝ : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
⊢ ‖⟪x i, x i⟫_A‖ ≤ ‖∑ i, ⟪x i, x i⟫_A‖
Module: Mathlib.Topology.UniformSpace.Matrix

Goal state before:
pp: case mp
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
⊢ (∀ (i : m) (i_1 : n), Filter.Tendsto ((fun a ↦ (a.1 i i_1, a.2 i i_1)) ∘ fun x ↦ (f x.1, f x.2)) (𝓤 β) (𝓤 𝕜)) →
    ∀ (i : m) (j : n), Filter.Tendsto (fun x ↦ (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)

Tactic:
intro a

Goal state after:
case mp
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
a : ∀ (i : m) (i_1 : n), Filter.Tendsto ((fun a ↦ (a.1 i i_1, a.2 i i_1)) ∘ fun x ↦ (f x.1, f x.2)) (𝓤 β) (𝓤 𝕜)
⊢ ∀ (i : m) (j : n), Filter.Tendsto (fun x ↦ (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)
Module: Mathlib.Topology.UniformSpace.Matrix

Goal state before:
pp: case mpr
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
⊢ (∀ (i : m) (j : n), Filter.Tendsto (fun x ↦ (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)) →
    ∀ (i : m) (i_1 : n), Filter.Tendsto ((fun a ↦ (a.1 i i_1, a.2 i i_1)) ∘ fun x ↦ (f x.1, f x.2)) (𝓤 β) (𝓤 𝕜)

Tactic:
intro a

Goal state after:
case mpr
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
a : ∀ (i : m) (j : n), Filter.Tendsto (fun x ↦ (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)
⊢ ∀ (i : m) (i_1 : n), Filter.Tendsto ((fun a ↦ (a.1 i i_1, a.2 i i_1)) ∘ fun x ↦ (f x.1, f x.2)) (𝓤 β) (𝓤 𝕜)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case zero
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 : Set 𝕜
hs : IsCompact s
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace ↑s
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcₙHomSuperset ⋯ ⋯) 0

Tactic:
| zero =>

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

Goal state before:
pp: case neg
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
h : ¬a = 0
⊢ ‖‖a‖ • a⁻¹‖₊ = 1

Tactic:
· rw [← nnnorm_eq_zero] at h
    rw [nnnorm_smul, nnnorm_inv, nnnorm_norm, mul_inv_cancel₀ h]

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

Goal state before:
pp: case h
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✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
i : l
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ ‖∑ j_1, A i j_1 * B j_1 j‖₊ ^ 1 ≤ ((∑ j, ‖A i j‖₊ ^ 2) * ∑ x, ‖B x j‖₊ ^ 2) ^ (1 / 2)

Tactic:
NNReal.rpow_one,

Goal state after:
case h
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✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
i : l
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ ‖∑ j_1, A i j_1 * B j_1 j‖₊ ≤ ((∑ j, ‖A i j‖₊ ^ 2) * ∑ x, ‖B x j‖₊ ^ 2) ^ (1 / 2)
Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap

Goal state before:
pp: F : Type u_1
A₁ : Type u_2
A₂ : Type u_3
inst✝⁷ : NonUnitalCStarAlgebra A₁
inst✝⁶ : NonUnitalCStarAlgebra A₂
inst✝⁵ : PartialOrder A₁
inst✝⁴ : PartialOrder A₂
inst✝³ : StarOrderedRing A₁
inst✝² : StarOrderedRing A₂
inst✝¹ : FunLike F A₁ A₂
inst✝ : LinearMapClass F ℂ A₁ A₂
h : ∀ (φ : F) (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑φ
⊢ ∀ (f : F) (x : A₁), 0 ≤ x → 0 ≤ f x

Tactic:
intro φ

Goal state after:
F : Type u_1
A₁ : Type u_2
A₂ : Type u_3
inst✝⁷ : NonUnitalCStarAlgebra A₁
inst✝⁶ : NonUnitalCStarAlgebra A₂
inst✝⁵ : PartialOrder A₁
inst✝⁴ : PartialOrder A₂
inst✝³ : StarOrderedRing A₁
inst✝² : StarOrderedRing A₂
inst✝¹ : FunLike F A₁ A₂
inst✝ : LinearMapClass F ℂ A₁ A₂
h : ∀ (φ : F) (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑φ
φ : F
⊢ ∀ (x : A₁), 0 ≤ x → 0 ≤ φ x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: case zero
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
⊢ Commute ((cfcₙHom ha) 0) b

Tactic:
| zero =>

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

Goal state before:
pp: A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ A IsStarNormal
u : A
⊢ u ∈ unitary A ↔ IsStarNormal u ∧ spectrum ℂ u ⊆ ↑(unitary ℂ)

Tactic:
by
  rw [← and_iff_right_of_imp isStarNormal_of_mem_unitary]
  refine and_congr_right fun hu ↦ ?_
  nth_rw 1 [← cfc_id ℂ u]
  rw [cfc_unitary_iff id u, Set.subset_def]
  simp only [id_eq, RCLike.star_def, SetLike.mem_coe, Unitary.mem_iff_star_mul_self]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
htriv : Y = ⊤
⊢ ∃ a, (toDualMap 𝕜 E) a = ℓ

pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
htriv : ¬Y = ⊤
⊢ ∃ a, (toDualMap 𝕜 E) a = ℓ

Tactic:
· have hℓ : ℓ = 0 := by
          have h' := LinearMap.ker_eq_top.mp htriv
          norm_cast at h'
        exact ⟨0, by simp [hℓ]⟩

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

Goal state before:
pp: case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
h_x : x ∈ Multiset.map (fun x ↦ ‖U i x‖ ^ 2) Finset.univ.val
⊢ 0 ≤ x

Tactic:
Multiset.mem_map

Goal state after:
case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
h_x : ∃ a ∈ Finset.univ.val, ‖U i a‖ ^ 2 = x
⊢ 0 ≤ x
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
⊢ ‖U i j‖ ^ 2 ∈ Multiset.map (fun x ↦ ‖U i x‖ ^ 2) Finset.univ.val

Tactic:
Multiset.mem_map

Goal state after:
case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
⊢ ∃ a ∈ Finset.univ.val, ‖U i a‖ ^ 2 = ‖U i j‖ ^ 2
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ (↑U).domRestrict (↑e) (↑(e.subtypeRestr hU).symm y) = y

Tactic:
rw [← e.subtypeRestr_coe hU, (e.subtypeRestr hU).right_inv hy]

Goal state after:
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
e : Pretrivialization F proj
x : B × F
⊢ x ∈ e.baseSet ×ˢ univ ↔ x.1 ∈ e.baseSet

Tactic:
prod_univ,

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : B × F
⊢ x ∈ Prod.fst ⁻¹' e.baseSet ↔ x.1 ∈ e.baseSet
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case pos
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)

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_true]
    refine (tendsto_congr' ?_).and Iff.rfl
    exact hl.mono fun x ↦ e.coe_fst

Goal state after:
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)
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ (∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U) ↔
    ∀ (a b : X) (b_1 : f a = f b),
      ⟨(a, b), b_1⟩ ∈ Function.pullbackDiagonal f → Function.pullbackDiagonal f ∈ Filter.comap Subtype.val (𝓝 a ×ˢ 𝓝 b)

Tactic:
Filter.mem_comap

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ (∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U) ↔
    ∀ (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
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: case zero
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
x y : A
⊢ (a.toProd ^ 0).2 x * y = x * (a.toProd ^ 0).1 y

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
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 ⟨U, hU, emb⟩ := h x hx
    have : IsOpenEmbedding ((interior U).domRestrict f) := by
      refine emb.comp ⟨.inclusion interior_subset, ?_⟩
      rw [Set.range_inclusion]; exact isOpen_induced isOpen_interior
    obtain ⟨cont, inj, openMap⟩ := isOpenEmbedding_iff_continuous_injective_isOpenMap.mp this
    have : Nonempty X := ⟨x⟩
    exact ⟨OpenPartialHomeomorph.ofContinuousOpenRestrict
      (Set.injOn_iff_injective.mpr inj).toPartialEquiv
      (continuousOn_iff_continuous_domRestrict.mpr cont) openMap isOpen_interior,
      mem_interior_iff_mem_nhds.mpr hU, rfl⟩

Goal state after: