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

Goal state before:
pp: case insert
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
h0 : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : (∀ i ∈ s, IsSelfAdjoint (f i)) → ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊
h : ∀ i ∈ insert j s, IsSelfAdjoint (f i)
⊢ ‖∑ i ∈ insert j s, f i‖₊ = (insert j s).sup fun x ↦ ‖f x‖₊

Tactic:
suffices f j * ∑ i ∈ s, f i = 0 by
      simp_all [(h j (by simp)).nnnorm_add_eq_max (by cfc_tac) this]
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind)

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
x : X
⊢ ∃ f, HasCompactSupport ⇑f ∧ 0 ≤ ⇑f ∧ f x ≠ 0

Tactic:
by
  rcases exists_compact_mem_nhds x with ⟨k, hk, k_mem⟩
  rcases exists_continuous_one_zero_of_isCompact hk isClosed_empty (disjoint_empty k)
    with ⟨f, fk, -, f_comp, hf⟩
  refine ⟨f, f_comp, fun x ↦ (hf x).1, ?_⟩
  have := fk (mem_of_mem_nhds k_mem)
  simp only [Pi.one_apply] at this
  simp [this]

Goal state after:
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst✝² : Finite ↑𝔖
inst✝¹ : PseudoMetricSpace β
inst✝ : BoundedSpace β
⊢ Set.univ = ⇑(ofFun 𝔖) ∘ ⇑UniformFun.toFun '' Set.univ

Tactic:
ext f

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst✝² : Finite ↑𝔖
inst✝¹ : PseudoMetricSpace β
inst✝ : BoundedSpace β
f : α →ᵤ[𝔖] β
⊢ f ∈ Set.univ ↔ f ∈ ⇑(ofFun 𝔖) ∘ ⇑UniformFun.toFun '' Set.univ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsStarNormal a
this : Isometry ⇑((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))
f : C(↑(spectrum ℂ a), ℂ)
⊢ spectrum ℂ f = Set.range ⇑f

Tactic:
ContinuousMap.spectrum_eq_range

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsStarNormal a
this : Isometry ⇑((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))
f : C(↑(spectrum ℂ a), ℂ)
⊢ Set.range ⇑f = Set.range ⇑f
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
f : C(↑(σₙ ℂ a), ℂ)₀
⊢ ‖(((↑(cfcHom ⋯)).comp ↑(Homeomorph.compStarAlgEquiv' ℂ ℂ (Homeomorph.setCongr ⋯))).comp toContinuousMapHom) f‖ = ‖f‖

Tactic:
simp only [NonUnitalStarAlgHom.comp_assoc, NonUnitalStarAlgHom.comp_apply,
      NonUnitalStarAlgHom.coe_coe]

Goal state after:
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
f : C(↑(σₙ ℂ a), ℂ)₀
⊢ ‖(cfcHom ⋯) ((Homeomorph.compStarAlgEquiv' ℂ ℂ (Homeomorph.setCongr ⋯)) (toContinuousMapHom f))‖ = ‖f‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : ‖a‖₊ ≤ t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ‖(algebraMap ℝ A) ↑t - a‖₊ ≤ t

Tactic:
rw [← ENNReal.coe_le_coe, ← IsSelfAdjoint.spectralRadius_eq_nnnorm,
    ← SpectrumRestricts.spectralRadius_eq (f := Complex.reCLM)] at ht ⊢

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℝ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t

A : Type u_1
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℝ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ SpectrumRestricts ((algebraMap ℝ A) ↑t - a) ⇑Complex.reCLM

A : Type u_1
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℂ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ SpectrumRestricts a ⇑Complex.reCLM

A : Type u_1
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℂ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)

A : Type u_1
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : ↑‖a‖₊ ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ IsSelfAdjoint a
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
⊢ ∀ {z : ℂ} {x y : C⋆ᵐᵒᵈ(A, (i : ι) → E i)}, ∑ i, ⟪x i, (z • y) i⟫_A = z • ∑ i, ⟪x i, y i⟫_A

Tactic:
simp [smul_sum]

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

Goal state before:
pp: case refine_1
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h : ‖star ↑z * (1 - ↑x) * ↑z‖ ≤ c ^ 2
⊢ 0 ≤ ↑x

Tactic:
inr_nonneg_iff

Goal state after:
case refine_1
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h : ‖star ↑z * (1 - ↑x) * ↑z‖ ≤ c ^ 2
⊢ 0 ≤ x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: 𝕜 : 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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ ContinuousOn (fun x ↦ cfcₙ f x) {a | p a ∧ quasispectrum 𝕜 a ⊆ s}

Tactic:
by
  by_cases hs0 : 0 ∈ s
  · rw [continuousOn_iff_continuous_domRestrict]
    convert!
      continuous_cfcₙHomSuperset_left hs (hs0 := ⟨hs0⟩) ⟨⟨_, hf.domRestrict⟩, hf0⟩ (X :=
        {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}) continuous_subtype_val (fun x ↦ x.2.2) with
      x
    rw [cfcₙHomSuperset_apply, Set.domRestrict_apply, cfcₙ_apply _ _ (hf.mono x.2.2) hf0 x.2.1]
    congr!
  · convert! continuousOn_empty _
    rw [Set.eq_empty_iff_forall_notMem]
    exact fun a ha ↦ hs0 <| ha.2 <| quasispectrum.zero_mem 𝕜 a

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

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
ha_cont : ContinuousOn a Set.univ
hs : ∀ (x : X), IsCompact (s x)
ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
hf : ∀ (x : X), ContinuousOn f (s x)
hf0 : f 0 = 0
ha' : ∀ (x : X), 0 ≤ a x
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) Set.univ

Tactic:
exact ha_cont.cfcₙ_nnreal 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
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 N : CStarMatrix m m A
⊢ (↑(reindexₗ R A e e)).toFun (M * N) = (↑(reindexₗ R A e e)).toFun M * (↑(reindexₗ R A e e)).toFun N

Tactic:
by
      ext i j
      simp only [mul_apply]
      refine Fintype.sum_equiv e _ _ ?_
      intro k
      simp

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
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‖
⊢ ‖M‖ ≤ ↑C

Tactic:
refine (toCLM M).opNorm_le_bound (by simp) fun v ↦ ?_

Goal state after:
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)
⊢ ‖(toCLM M) v‖ ≤ ↑C * ‖v‖
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
x✝ : E
⊢ { toLinearMap := (innerₗ E).flip x✝, cont := ⋯ } = (toDual ℝ E) x✝

Tactic:
ext y

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
x✝ y : E
⊢ { toLinearMap := (innerₗ E).flip x✝, cont := ⋯ } y = ((toDual ℝ E) x✝) y
Module: Mathlib.Analysis.CStarAlgebra.Projection

Goal state before:
pp: A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
p : A
hp : IsIdempotentElem p
h : IsStarNormal p
x : ℂ
hx : x ∈ quasispectrum ℂ p
⊢ x = ↑x.re

Tactic:
rcases hp.quasispectrum_subset _ hx with (hx | hx)

Goal state after:
case inl
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
p : A
hp : IsIdempotentElem p
h : IsStarNormal p
x : ℂ
hx✝ : x ∈ quasispectrum ℂ p
hx : x = 0
⊢ x = ↑x.re

case inr
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
p : A
hp : IsIdempotentElem p
h : IsStarNormal p
x : ℂ
hx✝ : x ∈ quasispectrum ℂ p
hx : x ∈ {1}
⊢ x = ↑x.re
Module: Mathlib.Analysis.Normed.Field.UnitBall

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝ : NonUnitalSeminormedRing 𝕜
a✝ b✝ : 𝕜
hx : a✝ ∈ closedBall 0 1
hy : b✝ ∈ closedBall 0 1
⊢ a✝ * b✝ ∈ closedBall 0 1

Tactic:
rw [mem_closedBall_zero_iff] at *

Goal state after:
𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝ : NonUnitalSeminormedRing 𝕜
a✝ b✝ : 𝕜
hx : ‖a✝‖ ≤ 1
hy : ‖b✝‖ ≤ 1
⊢ ‖a✝ * b✝‖ ≤ 1
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: x : ℝ
z : ℤ
⊢ exp (z • x) = exp x ^ z

Tactic:
exp_zsmul

Goal state after:
x : ℝ
z : ℤ
⊢ exp x ^ z = exp x ^ z
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: E : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℂ E
u : Circle
v : E
⊢ ‖u • v‖ = ‖v‖

Tactic:
smul_def,

Goal state after:
E : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℂ E
u : Circle
v : E
⊢ ‖↑u • v‖ = ‖v‖
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
A : Matrix m n 𝕜
B : Matrix n l 𝕜
this :
  ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) A ∘SL (toEuclideanLin ≪≫ₗ toContinuousLinearMap) B‖ ≤
    ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) A‖ * ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) B‖
x : EuclideanSpace 𝕜 l
⊢ ((toEuclideanLin ≪≫ₗ toContinuousLinearMap) (A * B)) x =
    ((toEuclideanLin ≪≫ₗ toContinuousLinearMap) A ∘SL (toEuclideanLin ≪≫ₗ toContinuousLinearMap) B) x

Tactic:
exact congr(toLp 2 ($(Matrix.toLin'_mul A B) x))

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
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e' : Trivialization F TotalSpace.proj
b : B
y : E b
F' : Type u_5
inst✝ : TopologicalSpace F'
e : Trivialization F proj
h : F ≃ₜ F'
⊢ (e.transHomeomorph ((Homeomorph.refl B).prodCongr h)).target = e.baseSet ×ˢ univ

Tactic:
by simp [target_eq, prod_univ, preimage_preimage]

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
inst✝ : DiscreteTopology ↑(f '' s)
x : ↑s
⊢ IsOpen[instTopologicalSpaceSubtype] {x}

Tactic:
obtain ⟨e, hx, rfl⟩ := h x x.2

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
x : ↑s
e : OpenPartialHomeomorph X Y
hx : ↑x ∈ e.source
h : IsLocalHomeomorphOn (↑e) s
inst✝ : DiscreteTopology ↑(↑e '' s)
⊢ IsOpen[instTopologicalSpaceSubtype] {x}
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: case refine_2.refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst✝¹] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph ↑f
⊢ ↑f ∘ ⇑{ toFun := (f.target ∩ ↑f.symm ⁻¹' U).domRestrict f.invFun, continuous_toFun := ⋯ } = Subtype.val

Tactic:
ext y

Goal state after:
case refine_2.refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst✝¹] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph ↑f
y : ↑(f.target ∩ ↑f.symm ⁻¹' U)
⊢ (↑f ∘ ⇑{ toFun := (f.target ∩ ↑f.symm ⁻¹' U).domRestrict f.invFun, continuous_toFun := ⋯ }) y = ↑y
Module: Mathlib.Topology.Covering.Quotient

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

Tactic:
simp_rw [mul_smul, smul_inv_smul]

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
hf : IsQuotientMap f
inst✝¹ : Group E
inst✝ : IsTopologicalGroup E
G : Subgroup E
hG : IsDiscrete ↑G
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁⁻¹ * e₂ ∈ G
e : E
U : Set E
hU : U ∈ 𝓝 1
left✝ : U⁻¹ = U
disj : ∀ g ∈ G, ((fun x ↦ x * g) '' U ∩ U).Nonempty → g = 1
x✝ : ↥G.op
s : E
hS : { unop' := s } ∈ G.op
hs : ((fun x ↦ ⟨{ unop' := s }, hS⟩ • x) '' ({e} * U) ∩ ({e} * U)).Nonempty
⊢ ((fun x ↦ x * MulOpposite.unop ↑⟨{ unop' := s }, hS⟩) '' U ∩ U).Nonempty

Tactic:
obtain ⟨_, ⟨_, ⟨_, rfl, x, hx, rfl⟩, rfl⟩, g, rfl, y, hy, he⟩ := hs

Goal state after:
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
hf : IsQuotientMap f
inst✝¹ : Group E
inst✝ : IsTopologicalGroup E
G : Subgroup E
hG : IsDiscrete ↑G
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁⁻¹ * e₂ ∈ G
U : Set E
hU : U ∈ 𝓝 1
left✝ : U⁻¹ = U
disj : ∀ g ∈ G, ((fun x ↦ x * g) '' U ∩ U).Nonempty → g = 1
x✝ : ↥G.op
s : E
hS : { unop' := s } ∈ G.op
x : E
hx : x ∈ U
g y : E
hy : y ∈ U
he : (fun x1 x2 ↦ x1 * x2) g y = (fun x ↦ ⟨{ unop' := s }, hS⟩ • x) ((fun x1 x2 ↦ x1 * x2) g x)
⊢ ((fun x ↦ x * MulOpposite.unop ↑⟨{ unop' := s }, hS⟩) '' U ∩ U).Nonempty
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : RCLike 𝕜
p : A → Prop
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : ContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
h : Continuous ⇑(cfcHom ha)
x✝ : ContinuousOn exp (spectrum 𝕜 a)
this : Algebra ℚ A
⊢ cfc exp a = (cfcHom ha) (exp { toFun := (spectrum 𝕜 a).domRestrict id, continuous_toFun := ⋯ })

Tactic:
cfc_apply exp a ha

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : RCLike 𝕜
p : A → Prop
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : ContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
h : Continuous ⇑(cfcHom ha)
x✝ : ContinuousOn exp (spectrum 𝕜 a)
this : Algebra ℚ A
⊢ (cfcHom ha) { toFun := (spectrum 𝕜 a).domRestrict exp, continuous_toFun := ⋯ } =
    (cfcHom ha) (exp { toFun := (spectrum 𝕜 a).domRestrict id, continuous_toFun := ⋯ })
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
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this✝¹ : DiscreteTopology ↑(f ⁻¹' {x})
φ : ↑(f ⁻¹' {x}) → OpenPartialHomeomorph E X
hφ : ∀ (e : ↑(f ⁻¹' {x})), ↑e ∈ (φ e).source ∧ ↑(φ e) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst✝²] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : ↑(f ⁻¹' {x}) → Set E := fun e ↦ V ↑e ∩ (φ e).source
hV' : ∀ (e : ↑(f ⁻¹' {x})), IsOpen[inst✝²] (V' e)
this✝ : ⋃ e, V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ e, V' e
h✝ : Nonempty ↑(f ⁻¹' {x})
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst✝¹] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ e, f '' V' e
this : Finite ↑(f ⁻¹' {x})
e : ↑(f ⁻¹' {x})
⊢ IsOpen[inst✝¹] (f '' V' e)

Tactic:
convert! ← (φ e).isOpen_image_of_subset_source (hV' _) inter_subset_right; exact (hφ e).2

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
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h✝² : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this✝³ : DiscreteTopology ↑(f ⁻¹' {x})
φ : ↑(f ⁻¹' {x}) → OpenPartialHomeomorph E X
hφ : ∀ (e : ↑(f ⁻¹' {x})), ↑e ∈ (φ e).source ∧ ↑(φ e) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst✝²] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : ↑(f ⁻¹' {x}) → Set E := fun e ↦ V ↑e ∩ (φ e).source
hV' : ∀ (e : ↑(f ⁻¹' {x})), IsOpen[inst✝²] (V' e)
this✝² : ⋃ e, V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ e, V' e
h✝¹ : Nonempty ↑(f ⁻¹' {x})
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst✝¹] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ e, f '' V' e
this✝¹ : Finite ↑(f ⁻¹' {x})
hU' : IsOpen[inst✝¹] U'
hUV : ∀ (e : ↑(f ⁻¹' {x})), U' ⊆ f '' V' e
this✝ : Nonempty E
e : ↑(f ⁻¹' {x})
s : Set X
hs : s ⊆ U'
h✝ : IsOpen[inst✝²] (f ⁻¹' s ∩ V' e)
this : s ⊆ (φ e).target
e' : E
h : e' ∈ f ⁻¹' s ∩ (φ e).source
e'' : E
left✝ : e'' ∈ V ↑e
mem : e'' ∈ (φ e).source
eq : f e'' = f e'
⊢ ↑(φ e) e'' = ↑(φ e) e'

Tactic:
rwa [(hφ e).2]

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
this : spectrum ℂ ↑(expUnitary x) ⊆ slitPlane
⊢ cfc (fun x ↦ ↑(NormedSpace.exp (I • x)).arg) ↑x = ↑x

Tactic:
conv_rhs => rw [← cfc_id' ℂ (x : A)]

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
this : spectrum ℂ ↑(expUnitary x) ⊆ slitPlane
⊢ cfc (fun x ↦ ↑(NormedSpace.exp (I • x)).arg) ↑x = cfc (fun x ↦ x) ↑x
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:

Tactic:
Real.arccos (1 - ‖(u - 1 : A)‖ ^ 2 / 2) < Real.arccos (1 - 2 ^ 2 / 2) := by
        apply Real.arccos_lt_arccos (by norm_num) (by gcongr)
        linarith [(by positivity : 0 ≤ ‖(u - 1 : A)‖ ^ 2 / 2)]
      _ = π := by norm_num

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✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
⊢ ⟪(adjoint A) y, x⟫_𝕜 = ⟪y, A x⟫_𝕜

Tactic:
by
  have := FiniteDimensional.complete 𝕜 E
  have := FiniteDimensional.complete 𝕜 F
  rw [← coe_toContinuousLinearMap A, adjoint_eq_toCLM_adjoint]
  exact ContinuousLinearMap.adjoint_inner_left _ x y

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
⊢ ∑ i, centroidWeights k univ i • (s.points i -ᵥ p) = (↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ p)

Tactic:
simp [smul_sum]

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
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
ha : ∀ (x : Fin (n + 1)), centroidWeightsIndicator k fs₁ x = centroidWeightsIndicator k fs₂ x
⊢ fs₁ = fs₂

Tactic:
Finset.centroidWeightsIndicator_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
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
ha : ∀ (x : Fin (n + 1)), (↑fs₁).indicator (centroidWeights k fs₁) x = (↑fs₂).indicator (centroidWeights k fs₂) x
⊢ fs₁ = fs₂
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
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).faceOppositeCentroid = s.faceOppositeCentroid ∘ ⇑e.symm

Tactic:
ext i
  rw [faceOppositeCentroid]
  obtain rfl : m = n := by simpa using Fintype.card_eq.2 ⟨e⟩
  exact centroid_eq_of_range_eq <| Affine.Simplex.range_faceOpposite_reindex s e i

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

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
s : Set P
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
h : Collinear k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 1
⊢ Collinear k s ↔ finrank k ↥(vectorSpan k s) ≤ 1

Tactic:
← finrank_eq_rank

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
s : Set P
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
h : Collinear k s ↔ ↑(finrank k ↥(vectorSpan k s)) ≤ 1
⊢ Collinear k s ↔ finrank k ↥(vectorSpan k s) ≤ 1