mathlib-initiative/mathlib-tactics huggingface dataset:
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]

Goal state after:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
⊢ cfc (fun x ↦ x⁺) 1 = 1
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]

Goal state after:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
r : ℝ
⊢ cfc (fun x ↦ x⁺) ((algebraMap ℝ A) r) = (algebraMap ℝ A) r⁺
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✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : ContinuousStar A
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
a₀ : A
l : Filter X
ha_tendsto : Tendsto a l (𝓝 a₀)
ha : ∀ᶠ (x : X) in l, spectrum 𝕜 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, p (a x)
ha₀ : spectrum 𝕜 a₀ ⊆ s
ha₀' : p a₀
hf : ContinuousOn f s
⊢ Tendsto (fun x ↦ cfc f (a x)) l (𝓝 (cfc f a₀))

Tactic:
by
  apply continuousOn_cfc A hs f |>.continuousWithinAt ⟨ha₀', ha₀⟩ |>.tendsto.comp
  rw [tendsto_nhdsWithin_iff]
  exact ⟨ha_tendsto, ha'.and 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
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⁻¹

Tactic:
← CStarRing.norm_star_mul_self

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⁻¹
⊢ ↑b⁻¹ ≤ ↑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 : A
ha : 0 ≤ a
x : ℂ
hx : x ∈ σₙ ℂ a
⊢ 0 ≤ x

Tactic:
by
    rw [Unitization.quasispectrum_eq_spectrum_inr' ℂ ℂ a] at hx
    exact spectrum_nonneg_of_nonneg (Unitization.inr_nonneg_iff.mpr ha) hx

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
x : A
⊢ 0 ≤ ↑x → (‖↑x‖ ≤ 1 ↔ ↑x ≤ 1)

Tactic:
exact (norm_le_one_iff_of_nonneg _ ·)

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalCStarAlgebra A
inst✝⁸ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : Module ℂ E
inst✝⁵ : SMul A E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : Module ℂ F
inst✝² : SMul A F
inst✝¹ : CStarModule A E
inst✝ : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖x‖ ≤ ‖x.1‖ + ‖x.2‖

Tactic:
refine abs_le_of_sq_le_sq' ?_ (by positivity) |>.2
  calc ‖x‖ ^ 2 ≤ ‖⟪x.1, x.1⟫_A‖ + ‖⟪x.2, x.2⟫_A‖ := prod_norm_sq x ▸ norm_add_le _ _
    _ = ‖x.1‖ ^ 2 + 0 + ‖x.2‖ ^ 2 := by simp [norm_sq_eq A]
    _ ≤ ‖x.1‖ ^ 2 + 2 * ‖x.1‖ * ‖x.2‖ + ‖x.2‖ ^ 2 := by gcongr; positivity
    _ = (‖x.1‖ + ‖x.2‖) ^ 2 := by ring

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
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
⊢ cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) b = cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) b

Tactic:
by
          rw [cfcₙ_nnreal_eq_real _ _ hb]
          refine cfcₙ_congr ?_
          intro x hx
          have hx' : 0 ≤ x := by grind
          simp [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
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ : cfc (fun y ↦ 1 - (1 + y)⁻¹) (ε⁻¹ ^ 2 • ↑m) ≤ ↑x
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
⊢ ‖m - x * m‖₊ ≤ ε

Tactic:
← norm_inr (𝕜 := ℂ)

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
hx₀ : 0 ≤ x
⊢ ‖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
hx₀ : 0 ≤ ↑x
⊢ ‖m - x * m‖₊ ≤ ε

Tactic:
← nnnorm_inr (𝕜 := ℂ),

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
hx₀ : 0 ≤ ↑x
⊢ ‖↑(m - x * m)‖₊ ≤ ε
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : One α
⊢ ‖1‖₊ = NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊

Tactic:
by
  calc
    ‖(diagonal 1 : Matrix n n α)‖₊
    _ = ‖toLp 2 (Function.const _ 1)‖₊ := frobenius_nnnorm_diagonal _
    _ = .sqrt (Fintype.card n) * ‖(1 : α)‖₊ := by
      rw [PiLp.nnnorm_toLp_const (ENNReal.ofNat_ne_top (n := 2))]
      simp [NNReal.sqrt_eq_rpow]

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
R : Type ?u.14
A : Type ?u.16
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Module R A
inst✝ : Star A
e : m ≃ n
M : CStarMatrix m m A
⊢ (↑(reindexₗ R A e e)).toFun (star M) = star ((↑(reindexₗ R A e e)).toFun M)

Tactic:
ext
      unfold reindexₗ
      dsimp only [Equiv.toFun_as_coe, Equiv.invFun_as_coe, Matrix.reindex_symm, AddHom.toFun_eq_coe,
        AddHom.coe_mk, Matrix.reindex_apply, Matrix.submatrix_apply]
      rw [star_apply, star_apply]
      simp [Matrix.submatrix_apply]

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
R : Type ?u.14
A : Type ?u.16
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Module R A
inst✝ : Star A
e : m ≃ n
M : CStarMatrix m m A
⊢ (↑(reindexₗ R A e e)).toFun (star M) = star ((↑(reindexₗ R A e e)).toFun M)

Tactic:
by
      ext
      unfold reindexₗ
      dsimp only [Equiv.toFun_as_coe, Equiv.invFun_as_coe, Matrix.reindex_symm, AddHom.toFun_eq_coe,
        AddHom.coe_mk, Matrix.reindex_apply, Matrix.submatrix_apply]
      rw [star_apply, star_apply]
      simp [Matrix.submatrix_apply]

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

Goal state before:
pp: A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℂ A
inst✝³ : StarModule ℂ A
inst✝² : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMap.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (spectrum ℝ ↑(ℜ a))
ha : IsStarNormal a
⊢ ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.re) '' spectrum ℂ a)

Tactic:
rw [spectrum_realPart' a] at hf

Goal state after:
A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℂ A
inst✝³ : StarModule ℂ A
inst✝² : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMap.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (re '' spectrum ℂ a)
ha : IsStarNormal a
⊢ ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.re) '' spectrum ℂ a)
Module: Mathlib.Analysis.CStarAlgebra.Extreme

Goal state before:
pp: case refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
x✝ :
  (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
⊢ IsStarProjection e

Tactic:
· /- Now suppose `e` is an extreme point of the nonnegative closed unit ball.
    So then it is self-adjoint, and so we only need to show `e * e = e`.
    Note that since `0 ≤ e ≤ 1` in the unitization, we also get `0 ≤ e * (2 - e) = 2 • e - e * e`,
    and `0 ≤ star (1 - e) * (1 - e) = 1 - 2 • e - e * e` which means `2 • e - e * e` is in the
    closed unit ball. So `2 • e - e * e` is in the nonnegative closed unit ball.
    Then using the extremity of `e`, we get `e * e = e` since `e * e` is obviously in the
    nonnegative closed unit ball, and `e = 2⁻¹ • e * e + 2⁻¹ • (2 • e - e * e)`. -/
    have := calc
      0 ≤ (e : A⁺¹) * (2 - e) := by
        have : (e : A⁺¹) ≤ 1 := norm_le_one_iff_of_nonneg _ (by simpa) |>.mp (by simpa [norm_inr])
        apply Commute.mul_nonneg (by simpa) (by grw [sub_nonneg, this, one_le_two])
        simp [commute_iff_eq, mul_sub, sub_mul, mul_two, two_mul]
      _ = (((2 : ℝ) • e - e * e : A) : A⁺¹) := by simp [mul_sub, two_smul, mul_two]
    refine ⟨h3 _ (Commute.mul_nonneg h1 h1 rfl) ?_ ((2 : ℝ) • e - e * e) this.of_inr ?_
      ⟨2⁻¹, 2⁻¹, by simp [smul_sub, ← one_div, smul_smul]⟩, h1.isSelfAdjoint⟩
    · grw [norm_mul_le, h2, h2, one_mul]
    · rw [← norm_inr (𝕜 := ℂ), norm_le_one_iff_of_nonneg _ this, ← sub_nonneg]
      calc 0 ≤ star (1 - e : A⁺¹) * (1 - e) := star_mul_self_nonneg _
        _ = _ := by simp [LE.le.star_eq, h1, mul_sub, sub_mul, two_smul, sub_sub, add_sub]

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case hs
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e e' : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
z : Z
⊢ z ∈ ((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)).source ↔ z ∈ (e.symm.trans e').source

Tactic:
simp_rw [OpenPartialHomeomorph.trans_source, e.lift_openEmbedding_symm_source, e.symm_source,
      e.lift_openEmbedding_symm, e'.lift_openEmbedding_source]

Goal state after:
case hs
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e e' : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
z : Z
⊢ z ∈ e.target ∩ f ∘ ↑e.symm ⁻¹' f '' e'.source ↔ z ∈ e.target ∩ ↑e.symm ⁻¹' e'.source
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case h₁.hs
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), ↑e x = ↑e' x
h₂ : ∀ (x : B × F), ↑e.symm x = ↑e'.symm x
h₃ : e.baseSet = e'.baseSet
⊢ e.source = e'.source

Tactic:
rw [e.source_eq, e'.source_eq, h₃]

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: 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
e✝ : Pretrivialization F proj✝
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
z : Z
hz : z ∈ e.source
⊢ (↑(↑e z).1, (↑e z).2) ∈ Prod.map Subtype.val id '' e.target

Tactic:
simpa using e.map_source hz

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
f : E → X
s : Set X
F : ↑s → Type u_3
inst✝ : (x : ↑s) → TopologicalSpace (F x)
hF : ∀ (x : ↑s), DiscreteTopology (F x)
t : (x : ↑s) → ↑x ∈ Set.range f → { t // ↑x ∈ t.baseSet }
h : ∀ (x : ↑s), ↑x ∉ Set.range f → ∃ U ∈ 𝓝 ↑x, f ⁻¹' U = ∅
x : X
hx : x ∈ s
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})

Tactic:
lift x to s using hx
  by_cases hxf : x.1 ∈ Set.range f
  · exact .to_isEvenlyCovered_preimage (.of_trivialization (t x hxf).2)
  · have ⟨U, hUx, hfU⟩ := h x hxf
    exact .to_isEvenlyCovered_preimage (.of_preimage_eq_empty Empty hUx hfU)

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
f : E → X
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
surj : ∀ (i : ι), Set.SurjOn f (U i) V
disjoint : Pairwise (Disjoint on U)
exhaustive exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
⊢ Trivialization ι f

Tactic:
simp_rw [Set.subset_def, Set.mem_iUnion] at exhaustive

Goal state after:
E : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace X
f : E → X
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
surj : ∀ (i : ι), Set.SurjOn f (U i) V
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
exhaustive : ∀ x ∈ f ⁻¹' V, ∃ i, x ∈ U i
⊢ Trivialization ι f
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₁ : IsSelfAdjoint a
⊢ log (a ^ n) = n • log a

Tactic:
have ha₂' : ContinuousOn Real.log (spectrum ℝ a) := by fun_prop
  have ha₂'' : ContinuousOn Real.log ((· ^ n) '' spectrum ℝ a) := by fun_prop (disch := aesop)
  rw [log, ← cfc_pow_id (R := ℝ) a n ha₁, ← cfc_comp' Real.log (· ^ n) a ha₂'', log]
  simp_rw [Real.log_pow, ← Nat.cast_smul_eq_nsmul ℝ n, cfc_const_mul (n : ℝ) Real.log a ha₂']

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

Goal state before:
pp: A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ exp (log a) = a

Tactic:
← real_exp_eq_normedSpace_exp .log,

Goal state after:
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ cfc Real.exp (log a) = a
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ ⇑(x.path y) '' Ioc 0 1 = ⇑exp '' Ioc (↑x).arg (x.angleDiff y + (↑x).arg)

Tactic:
by
  rw [coe_path, image_comp, segment_image_Ioc (by simp [angleDiff_pos h])]

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

Goal state before:
pp: x : Circle
⊢ IsPathConnected {x}ᶜ

Tactic:
by
  refine ⟨-x, neg_ne_self x, fun y (hyx : y ≠ x) ↦ ?_⟩
  obtain hxP | hxP := (em (x ∈ range (path (-x) y))).symm
  · exact ⟨(path (-x) y), fun t ↦ by grind⟩
  refine ⟨(path y (-x)).symm, ?_⟩
  have hne : -x ≠ y := by
    rintro rfl
    simp [(neg_ne_self x).symm] at hxP
  have hP₂ : x ∉ range (path y (-x)) := by
    rintro hP₂
    have h : x ∈ range _ ∩ _ := ⟨hxP, hP₂⟩
    rw [range_path_inter_range_path hne] at h
    simp [(neg_ne_self x).symm, hyx.symm] at h
  grind

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
a✝ : Nontrivial A
⊢ ‖↑(expUnitary x) - 1‖ ^ 2 = 2 * (1 - Real.cos ‖x‖)

Tactic:
apply norm_sub_one_sq_eq (expUnitary x).2

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
a✝ : Nontrivial A
⊢ IsLeast (re '' spectrum ℂ ↑(expUnitary x)) (Real.cos ‖x‖)
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: case inr
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
key : a + I • CFC.sqrt (1 - a ^ 2) = cfc (fun x ↦ ↑x.re + I * ↑√(1 - x.re ^ 2)) a
x : ℂ
hx : x ∈ spectrum ℂ a
⊢ star (↑x.re + I * ↑√(1 - x.re ^ 2)) * (↑x.re + I * ↑√(1 - x.re ^ 2)) = 1

Tactic:
← starRingEnd_apply,

Goal state after:
case inr
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
key : a + I • CFC.sqrt (1 - a ^ 2) = cfc (fun x ↦ ↑x.re + I * ↑√(1 - x.re ^ 2)) a
x : ℂ
hx : x ∈ spectrum ℂ a
⊢ (starRingEnd ℂ) (↑x.re + I * ↑√(1 - x.re ^ 2)) * (↑x.re + I * ↑√(1 - x.re ^ 2)) = 1
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‖) ≤ 2 * (1 - Real.cos ‖argSelfAdjoint u‖)

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 ‖argSelfAdjoint u‖) ≤ ‖↑u - 1‖ ^ 2

Tactic:
· gcongr
    exact Real.cos_le_cos_of_nonneg_of_le_pi (by positivity) (norm_argSelfAdjoint_le_pi u) key

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 ‖argSelfAdjoint u‖) ≤ ‖↑u - 1‖ ^ 2
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ‖(adjoint A ∘SL A) x‖ * ‖x‖ ≤ ‖adjoint A ∘SL A‖ * ‖x‖ * ‖x‖

Tactic:
gcongr; exact le_opNorm _ _

Goal state after:
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
hT : IsIdempotentElem T
h : IsStarNormal T
⊢ (∀ (x : E), ‖(T - star T * T) x‖ = 0) ↔ ∀ (x : E), ‖(adjoint (1 - T)) (T x)‖ = 0

Tactic:
simp [star_eq_adjoint, one_def]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : CharZero k
s : Simplex k P n
p : P
⊢ p = s.centroid ↔ ∑ i, (s.points i -ᵥ p) = 0

Tactic:
by
  constructor
  · intro h
    rw [h, centroid_weighted_vsub_eq_zero]
  · intro h
    rw [← vsub_eq_zero_iff_eq]
    have : ∑ i, (s.points i -ᵥ p) = ∑ i, ((s.points i -ᵥ s.centroid) - (p -ᵥ s.centroid)) := by
      apply sum_congr rfl
      intro x hx
      rw [vsub_sub_vsub_cancel_right _ _ s.centroid]
    rw [this, sum_sub_distrib, centroid_weighted_vsub_eq_zero] at h
    simp only [sum_const, card_univ, Fintype.card_fin, zero_sub, neg_eq_zero] at h
    have h' : ((n : k) + 1) • (p -ᵥ s.centroid) = 0 := by norm_cast
    rw [smul_eq_zero_iff_right (by norm_cast)] at h'
    exact h'

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
x✝ : ∃ y, y • 1 = ↑(↑g).symm ∘SL ↑↑f
y : 𝕜
h : y • 1 = ↑(↑g).symm ∘SL ↑↑f
hy : y ≠ 0
hfg : ↑↑f = y • ↑↑g
hgf : ↑↑g = star y • ↑↑f
this : 1 • ↑↑g = ((starRingEnd 𝕜) y * y) • ↑↑g
⊢ ∃ α, ∀ (x : H), f x = (α • g) x

Tactic:
rw [← sub_eq_zero, ← sub_smul, smul_eq_zero, sub_eq_zero, eq_comm] at this

Goal state after:
case neg
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
x✝ : ∃ y, y • 1 = ↑(↑g).symm ∘SL ↑↑f
y : 𝕜
h : y • 1 = ↑(↑g).symm ∘SL ↑↑f
hy : y ≠ 0
hfg : ↑↑f = y • ↑↑g
hgf : ↑↑g = star y • ↑↑f
this : (starRingEnd 𝕜) y * y = 1 ∨ ↑↑g = 0
⊢ ∃ α, ∀ (x : H), f x = (α • g) x
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : InnerProductSpace 𝕜 F
m : Type u_5
n : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
v₁ : OrthonormalBasis n 𝕜 E
v₂ : OrthonormalBasis m 𝕜 F
f : E →ₗ[𝕜] F
⊢ (toLin v₂.toBasis v₁.toBasis) ((toMatrix v₂.toBasis v₁.toBasis) (adjoint f)) =
    (toLin v₂.toBasis v₁.toBasis) ((toMatrix v₁.toBasis v₂.toBasis) f)ᴴ

Tactic:
simp [toLin_conjTranspose]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case inr
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : FiniteDimensional k ↥s.direction
p p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ FiniteDimensional k ↥(affineSpan k (insert p ↑s)).direction

Tactic:
direction_affineSpan_insert hp₀

Goal state after:
case inr
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : AffineSubspace k P
inst✝ : FiniteDimensional k ↥s.direction
p p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ FiniteDimensional k ↥(k ∙ (p -ᵥ p₀) ⊔ s.direction)
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case neg
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)
i : α
F : Fin 2 → ℝ≥0 := ![‖f i‖₊, ‖g i‖₊]
h : 1 ≤ p.toReal
⊢ (‖f i‖ + ‖g i‖) ^ p.toReal ≤ 2 ^ (p.toReal - 1) * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)

Tactic:
simpa [Fin.sum_univ_succ] using!
        Real.rpow_sum_le_const_mul_sum_rpow_of_nonneg Finset.univ h fun i _ => (F i).coe_nonneg

Goal state after: