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

Goal state before:
pp: case frequently
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
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace ↑s
f : C(↑s, 𝕜)
hf :
  ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) g
ε : ℝ
hε : 0 < ε
g : C(↑s, 𝕜)
g_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) g
hg : ‖f - g‖ ≤ ε
x : X
⊢ ‖(cfcHomSuperset ⋯ ⋯) (f - g)‖ ≤ ε

Tactic:
cfcHomSuperset_apply

Goal state after:
case frequently
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
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace ↑s
f : C(↑s, 𝕜)
hf :
  ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) g
ε : ℝ
hε : 0 < ε
g : C(↑s, 𝕜)
g_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) g
hg : ‖f - g‖ ≤ ε
x : X
⊢ ‖(cfcHom ⋯) ((f - g).comp { toFun := Subtype.map id ⋯, continuous_toFun := ⋯ })‖ ≤ ε
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
ha : 0 ≤ a
⊢ sqrt a = 1 ↔ a = 1

Tactic:
by
  rw [sqrt_eq_iff a _, mul_one, eq_comm]

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x ↦ ↑(f x.toNNReal - g x.toNNReal)) (fun x ↦ ↑(f x.toNNReal) - ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ cfc (fun x ↦ ↑(f x.toNNReal) - ↑(g x.toNNReal)) a = cfc (fun x ↦ ↑(f x.toNNReal)) a - cfc (fun x ↦ ↑(g x.toNNReal)) a

Tactic:
refine cfc_sub _ _ a ?_ ?_

Goal state after:
case refine_1
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x ↦ ↑(f x.toNNReal - g x.toNNReal)) (fun x ↦ ↑(f x.toNNReal) - ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ ContinuousOn (fun x ↦ ↑(f x.toNNReal)) (spectrum ℝ a)

case refine_2
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x ↦ ↑(f x.toNNReal - g x.toNNReal)) (fun x ↦ ↑(f x.toNNReal) - ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ ContinuousOn (fun x ↦ ↑(g x.toNNReal)) (spectrum ℝ a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: case pos
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
ha' : 0 ≤ ↑a
⊢ ↑(CFC.sqrt a) * ↑(CFC.sqrt a) = ↑a

Tactic:
← inr_mul,

Goal state after:
case pos
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
ha' : 0 ≤ ↑a
⊢ ↑(CFC.sqrt a * CFC.sqrt a) = ↑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
ha : 0 ≤ a
b : Aˣ
hb : IsStrictlyPositive ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
h : ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2)) ≤ 1
⊢ sqrt ↑b * ↑b ^ (-(1 / 2)) * a * (↑b ^ (-(1 / 2)) * sqrt ↑b) =
    sqrt ↑b * (↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))) * sqrt ↑b

Tactic:
simp only [mul_assoc]

Goal state after:
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)
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ ∑ i, ‖⟪x i, x i⟫_A‖ = ∑ i, ‖x i‖ ^ 2

Tactic:
by simp only [norm_sq_eq A]

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 b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
c : Unitization ℂ A
hc : 0 ≤ c
x : ℝ≥0
x✝ : x ∈ σ ℝ≥0 c
⊢ id (1 + x) ≠ 0

Tactic:
by dsimp only [id]; positivity

Goal state after:
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
inst✝ : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
⊢ ⟪Pi.single i y i, x i⟫_A = ⟪y, x i⟫_A

pp: case h₀
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
inst✝ : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
⊢ ∀ b ∈ Finset.univ, b ≠ i → ⟪Pi.single i y b, x b⟫_A = 0

pp: case h₁
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
inst✝ : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
⊢ i ∉ Finset.univ → ⟪Pi.single i y i, x i⟫_A = 0

Tactic:
all_goals simp_all

Goal state after:
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
inst✝ : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
⊢ ⟪x i, Pi.single i y i⟫_A = ⟪x i, y⟫_A

pp: case h₀
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
inst✝ : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
⊢ ∀ b ∈ Finset.univ, b ≠ i → ⟪x b, Pi.single i y b⟫_A = 0

pp: case h₁
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
inst✝ : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
⊢ i ∉ Finset.univ → ⟪x i, Pi.single i y i⟫_A = 0

Tactic:
all_goals simp_all

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
f : ℝ≥0 → ℝ≥0 := fun x ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x ↦ x * (1 - x)⁻¹
this : ∀ (a b : A), 0 ≤ a → 0 ≤ b → ‖a‖ < 1 → ‖b‖ < 1 → a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) ({x | 0 ≤ x} ∩ Metric.ball 0 1)

Tactic:
rintro a ⟨(ha₁ : 0 ≤ a), ha₂⟩ b ⟨(hb₁ : 0 ≤ b), hb₂⟩
    simp only [Metric.mem_ball, dist_zero_right] at ha₂ hb₂
    refine ⟨cfcₙ f (cfcₙ g a + cfcₙ g b), ⟨by simp, ?_⟩, ?_, ?_⟩
    · simpa only [Metric.mem_ball, dist_zero_right] using norm_cfcₙ_one_sub_one_add_inv_lt_one _
    · exact this a b ha₁ hb₁ ha₂ hb₂
    · exact add_comm (cfcₙ g a) (cfcₙ g b) ▸ this b a hb₁ ha₁ hb₂ ha₂

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
⊢ ∀ (x y : CStarMatrix n n A), (mapₗ ↑f) (x + y) = (mapₗ ↑f) x + (mapₗ ↑f) y

Tactic:
by simp [map_add]

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

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : MeasurableSpace X
μ : Measure X
inst✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra 𝕜 A
inst✝⁴ : ContinuousFunctionalCalculus 𝕜 A p
inst✝³ : CompleteSpace A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf : ContinuousOn (Function.uncurry f) (univ ×ˢ spectrum 𝕜 a)
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
⊢ Integrable (fun x ↦ cfc (f x) a) μ

Tactic:
by
  refine integrable_cfc' _ _ ⟨?_, ?_⟩ ha
  · exact aeStronglyMeasurable_mkD_restrict_of_uncurry _ _ hf
  · refine hasFiniteIntegral_mkD_restrict_of_bound f _ ?_ bound bound_int bound_ge
    exact .of_forall fun x ↦
      hf.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨Set.mem_univ _, hz⟩

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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CStarAlgebra A
inst✝³ : CStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective ⇑φ
⊢ spectrum ℝ (φ a) = spectrum ℝ a

Tactic:
have h_spec := AlgHom.spectrum_apply_subset ((φ : A →⋆ₐ[ℂ] B).restrictScalars ℝ) a
  refine Set.eq_of_subset_of_subset h_spec fun x hx ↦ ?_
  /- we prove the reverse inclusion by contradiction, so assume that `x ∈ spectrum ℝ a`, but
  `x ∉ spectrum ℝ (φ a)`. Then by Urysohn's lemma we can get a function for which `f x = 1`, but
  `f = 0` on `spectrum ℝ a`. -/
  by_contra hx'
  obtain ⟨f, h_eqOn, h_eqOn_x, -⟩ := exists_continuous_zero_one_of_isClosed
    (spectrum.isClosed (𝕜 := ℝ) (φ a)) (isClosed_singleton (x := x)) <| by simpa
  /- it suffices to show that `φ (f a) = 0`, for if so, then `f a = 0` by injectivity of `φ`, and
  hence `f = 0` on `spectrum ℝ a`, contradicting the fact that `f x = 1`. -/
  suffices φ (cfc f a) = 0 by
    rw [map_eq_zero_iff φ hφ, ← cfc_zero ℝ a, cfc_eq_cfc_iff_eqOn] at this
    exact zero_ne_one <| calc
      0 = f x := (this hx).symm
      _ = 1 := h_eqOn_x <| Set.mem_singleton x
  /- Finally, `φ (f a) = f (φ a) = 0`, where the last equality follows since `f = 0` on
  `spectrum ℝ (φ a)`. -/
  calc φ (cfc f a) = cfc f (φ a) := StarAlgHomClass.map_cfc φ f a
    _ = cfc (0 : ℝ → ℝ) (φ a) := cfc_congr h_eqOn
    _ = 0 := by simp

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
inst✝ : TopologicalSpace Z
e : Trivialization F proj
x : Z
ex : x ∈ e.source
⊢ map proj (𝓝 x) = 𝓝 (proj x)

Tactic:
rw [← e.coe_fst ex, ← map_congr (e.coe_fst_eventuallyEq_proj ex), ← map_map, ← e.coe_coe,
    e.map_nhds_eq ex, map_fst_nhds]

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
n : ℤ
x y : A
⊢ ↑n x * y = x * ↑n y

Tactic:
simp only [← Int.smul_one_eq_cast, smul_apply, one_apply_eq_self, mul_smul_comm,
        smul_mul_assoc]

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
⊢ log 0 = 0

Tactic:
by simp [log]

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
⊢ log 1 = 0

Tactic:
by simp [log]

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

Goal state before:
pp: z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : z ∈ centeredArc (π / ↑n)
h2 : z ^ n ∈ centeredArc s
hs0 : 0 < s
⊢ n ≠ 0

Tactic:
contrapose! h1

Goal state after:
z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h2 : z ^ n ∈ centeredArc s
hs0 : 0 < s
h1 : n = 0
⊢ z ∉ centeredArc (π / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : |(↑z).arg| < π / ↑n
h2 : |(n • ↑(↑z).arg).toReal| < s
hs0 : 0 < s
hn0 : n ≠ 0
hn : 1 ≤ ↑n
⊢ (↑(↑z).arg).toReal ∈ Ioo (-π / ↑n) (π / ↑n)

Tactic:
rwa [neg_div, mem_Ioo, ← abs_lt, arg_coe_angle_toReal_eq_arg]

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

Goal state before:
pp: x y : Circle
⊢ 0 ≤ x.angleDiff y

Tactic:
grind [neg_pi_lt_arg y.val, arg_le_pi x.val]

Goal state after:
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
⊢ a + I • CFC.sqrt (1 - a ^ 2) ∈ unitary A

Tactic:
rw [key, cfc_unitary_iff ..]

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 ∈ spectrum ℂ a, star (↑x.re + I * ↑√(1 - x.re ^ 2)) * (↑x.re + I * ↑√(1 - x.re ^ 2)) = 1
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: case inl
A : Type u_1
inst✝ : CStarAlgebra A
x✝¹ : (A : Type ?u.39) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
x✝ : ∀ (A : Type ?u.41) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
⊢ ∃ u c, 0 = ∑ i, c i • ↑(u i) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ ‖0‖ / 2

Tactic:
exact ⟨![1, -1, 1, -1], 0, by simp⟩

Goal state after:
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
y : F
x : E
⊢ ‖y - A x‖ = ⨅ z, ‖y - ↑z‖ ↔ (adjoint A) (y - A x) = 0

Tactic:
rw [A.range.norm_eq_iInf_iff_inner_eq_zero (by simp),
    ← Submodule.mem_orthogonal', A.orthogonal_range, LinearMap.mem_ker, coe_coe]

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
S : E →L[𝕜] E
hS : IsStarProjection S
hT : IsStarProjection T
⊢ S = T ↔ (↑S).range = (↑T).range

Tactic:
by
  simpa using hS.isSymmetricProjection.ext_iff hT.isSymmetricProjection

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 : ℕ
s₁ s₂ : Simplex k P n
h : Set.range s₁.points = Set.range s₂.points
⊢ Finset.centroid k univ s₁.points = Finset.centroid k univ s₂.points

Tactic:
rw [← Set.image_univ, ← Set.image_univ, ← Finset.coe_univ] at h
  exact
    Finset.univ.centroid_eq_of_inj_on_of_image_eq k _
      (fun _ _ _ _ he => AffineIndependent.injective s₁.independent he)
      (fun _ _ _ _ he => AffineIndependent.injective s₂.independent he) h

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✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i j : Fin (n + 1)
h1 : ∀ (i : Fin (n + 1)), ∑ x, (s.points x -ᵥ s.points i) = ∑ x, (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0))
⊢ (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0)) -
        (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points 0 - (s.points j -ᵥ s.points 0)) +
      (s.points i -ᵥ s.points j) =
    (↑n)⁻¹ • (s.points j -ᵥ s.points i)

Tactic:
sum_sub_distrib

Goal state after:
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✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i j : Fin (n + 1)
h1 : ∀ (i : Fin (n + 1)), ∑ x, (s.points x -ᵥ s.points i) = ∑ x, (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0))
⊢ (↑n)⁻¹ • (∑ x, (s.points x -ᵥ s.points 0) - ∑ x, (s.points i -ᵥ s.points 0)) -
        (↑n)⁻¹ • (∑ x, (s.points x -ᵥ s.points 0) - ∑ x, (s.points j -ᵥ s.points 0)) +
      (s.points i -ᵥ s.points j) =
    (↑n)⁻¹ • (s.points j -ᵥ s.points i)
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✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i) =
    (↑n + 1) • ((↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i) - (↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ s.points i))

Tactic:
← sub_smul,

Goal state after:
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✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i) = (↑n + 1) • ((↑n)⁻¹ - (↑n + 1)⁻¹) • ∑ x, (s.points x -ᵥ s.points i)
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✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ ↑n • ((↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ s.points i) - (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i)) =
    -((↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ s.points i))

Tactic:
← sub_smul,

Goal state after:
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✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ ↑n • ((↑n + 1)⁻¹ - (↑n)⁻¹) • ∑ x, (s.points x -ᵥ s.points i) = -((↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ s.points i))
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 = 0
⊢ ∃ α, ∀ (x : H), f x = (α • g) x

Tactic:
← sub_smul,

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 : (1 - (starRingEnd 𝕜) y * y) • ↑↑g = 0
⊢ ∃ α, ∀ (x : H), f x = (α • g) x
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✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hmem1 : s.medial.points 0 ∈ affineSpan k (Set.range s.medial.points)
hmem2 : s.medial.points 0 ∈ affineSpan k (Set.range s.points)
⊢ (affineSpan k (Set.range s.medial.points)).direction = (affineSpan k (Set.range s.points)).direction

Tactic:
simp_rw [direction_affineSpan, vectorSpan_def]

Goal state after:
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✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hmem1 : s.medial.points 0 ∈ affineSpan k (Set.range s.medial.points)
hmem2 : s.medial.points 0 ∈ affineSpan k (Set.range s.points)
⊢ Submodule.span k (Set.range s.medial.points -ᵥ Set.range s.medial.points) =
    Submodule.span k (Set.range s.points -ᵥ Set.range s.points)
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulLeftInvariant
f : G → E
g : G
h_mul : MeasurableEmbedding fun x ↦ g * x
⊢ ∫ (x : G), f (g * x) ∂μ = ∫ (x : G), f x ∂μ

Tactic:
← h_mul.integral_map,

Goal state after:
G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulLeftInvariant
f : G → E
g : G
h_mul : MeasurableEmbedding fun x ↦ g * x
⊢ ∫ (y : G), f y ∂map (fun x ↦ g * x) μ = ∫ (x : G), f x ∂μ