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

Goal state before:
pp: case refine_1
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsStarNormal a
⊢ Continuous ⇑((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))

Tactic:
exact continuous_subtype_val.comp <|
      (StarAlgEquiv.isometry (continuousFunctionalCalculus a)).continuous

Goal state after:
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:
← IsSelfAdjoint.spectralRadius_eq_nnnorm,

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)
⊢ 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.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: case mp
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := ⋯
x y : A
⊢ x ≤ y → ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), y = x + p

Tactic:
intro h
        obtain ⟨s, hs₁, _, hs₂⟩ :=
          CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts h.1 h.2
        refine ⟨s * s, ?_, by rwa [eq_sub_iff_add_eq', eq_comm] at hs₂⟩
        exact AddSubmonoid.subset_closure ⟨s, by simp [hs₁.star_eq]⟩

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
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
⊢ (a ^ x)⁻¹ʳ = a ^ (-x)

Tactic:
have : a ^ (-x) = (a ^ x) ^ (-1 : ℝ) := by
    rw [rpow_rpow (hx := hx) (ha := by grind)]
    simp
  rw [← inverse_eq_rpow_neg_one (by grind)] at this
  rw [this]

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

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NontriviallyNormedField α
inst✝¹ : NormedAlgebra ℝ α
inst✝ : DecidableEq n
f : (n → α) →L[α] m → α
⊢ ‖LinearMap.toMatrix' ↑f‖₊ = ‖f‖₊

Tactic:
rw [linfty_opNNNorm_eq_opNNNorm]

Goal state after:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NontriviallyNormedField α
inst✝¹ : NormedAlgebra ℝ α
inst✝ : DecidableEq n
f : (n → α) →L[α] m → α
⊢ ‖{ toLinearMap := (LinearMap.toMatrix' ↑f).mulVecLin, cont := ⋯ }‖₊ = ‖f‖₊
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖A‖₊ = (∑ i, ∑ j, ‖A i j‖₊ ^ 2) ^ (1 / 2)

Tactic:
change ‖toLp 2 fun i => toLp 2 fun j => A i j‖₊ = _

Goal state after:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖toLp 2 fun i ↦ toLp 2 fun j ↦ A i j‖₊ = (∑ i, ∑ j, ‖A i j‖₊ ^ 2) ^ (1 / 2)
Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap

Goal state before:
pp: A₁ : Type u_1
A₂ : Type u_2
inst✝⁵ : NonUnitalCStarAlgebra A₁
inst✝⁴ : NonUnitalCStarAlgebra A₂
inst✝³ : PartialOrder A₁
inst✝² : StarOrderedRing A₁
inst✝¹ : PartialOrder A₂
inst✝ : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
C : ℝ≥0
hmain : ∀ (a : A₁), 0 ≤ a → ‖f a‖ ≤ ↑C * ‖a‖
x : A₁
y : Fin 4 → A₁
hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i
hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖x‖
hy : x = ∑ i, I ^ ↑i • y i
⊢ ∑ i, ‖I ^ ↑i • f (y i)‖ ≤ ↑(4 * C) * ‖x‖

Tactic:
simp only [norm_smul, norm_pow, norm_I, one_pow, one_mul]

Goal state after:
A₁ : Type u_1
A₂ : Type u_2
inst✝⁵ : NonUnitalCStarAlgebra A₁
inst✝⁴ : NonUnitalCStarAlgebra A₂
inst✝³ : PartialOrder A₁
inst✝² : StarOrderedRing A₁
inst✝¹ : PartialOrder A₂
inst✝ : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
C : ℝ≥0
hmain : ∀ (a : A₁), 0 ≤ a → ‖f a‖ ≤ ↑C * ‖a‖
x : A₁
y : Fin 4 → A₁
hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i
hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖x‖
hy : x = ∑ i, I ^ ↑i • y i
⊢ ∑ x, ‖f (y x)‖ ≤ ↑(4 * C) * ‖x‖
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✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ i ∈ t, s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a i))
x : ↑t
⊢ ∃ S, IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a ↑x), quasispectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s

Tactic:
obtain ⟨S, ⟨hS₁, hS₂⟩, hS₃⟩ :=
      quasispectrum.isCompact_nnreal (a x) |>.nhdsSet_basis_isCompact.mem_iff.mp (hs' x x.2)

Goal state after:
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✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ i ∈ t, s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a i))
x : ↑t
S : Set ℝ≥0
hS₃ : id S ⊆ s
hS₁ : S ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a ↑x))
hS₂ : IsCompact S
⊢ ∃ S, IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a ↑x), quasispectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s
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
⊢ ∀ (a : CStarMatrix m n A), toCLM a = 0 → a = 0

Tactic:
intro M h

Goal state after:
m : Type u_1
n : Type u_2
A : Type u_5
inst✝¹ : Fintype m
inst✝ : NonUnitalCStarAlgebra A
M : CStarMatrix m n A
h : toCLM M = 0
⊢ M = 0
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
⊢ Function.Bijective fun y ↦ { toLinearMap := (innerₗ E).flip y, cont := ⋯ }

Tactic:
convert! (toDual ℝ E).bijective

Goal state after:
𝕜 : 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✝
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
⊢ (f.leftMulMapPreGNS 0).completion = 0

Tactic:
simpa using f.completion_leftMulMapPreGNS_map_smul 0 0

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

Goal state before:
pp: 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
⊢ ↑e * (2 - ↑e) = ↑(2 • e - e * e)

Tactic:
by simp [mul_sub, two_smul, mul_two]

Goal state after:
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsSeparatedMap f ↔ IsClosedEmbedding (toPullbackDiag f)

Tactic:
by
  rw [isSeparatedMap_iff_isClosed_diagonal, ← range_toPullbackDiag]
  exact ⟨fun h ↦ ⟨.toPullbackDiag f, h⟩, fun h ↦ h.isClosed_range⟩

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
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
⊢ Disjoint (e.baseSet ×ˢ univ) (e'.baseSet ×ˢ univ)

Tactic:
disjoint_iff_inf_le

Goal state after:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
⊢ e.baseSet ×ˢ univ ⊓ e'.baseSet ×ˢ univ ⊆ ⊥
Module: Mathlib.Topology.IsLocalHomeomorph

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

Tactic:
discreteTopology_iff_isOpen_singleton

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
h : IsLocalHomeomorphOn f s
hs : IsOpen[inst✝¹] s
⊢ (∀ (a : ↑s), IsOpen[instTopologicalSpaceSubtype] {a}) → ∀ (a : ↑(f '' s)), IsOpen[instTopologicalSpaceSubtype] {a}
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
inst✝ : Nonempty I
h✝ : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝²] U
hfU : IsOpen[inst✝³] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
e : E
he : f e ∈ U
⊢ (↑{ toFun := fun e ↦ if he : f e ∈ U then (↑(H ⟨e, he⟩).1, (H ⟨e, he⟩).2) else (x, Classical.arbitrary I),
            invFun := fun xi ↦ ↑(H.symm (if hx : xi.1 ∈ U then ⟨xi.1, hx⟩ else ⟨x, hxU⟩, xi.2)), source := f ⁻¹' U,
            target := U ×ˢ Set.univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯,
            continuousOn_toFun := ⋯, continuousOn_invFun := ⋯, open_source := hfU, open_target := ⋯ }
        e).1 =
    f e

Tactic:
simp [he, hH]

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
I : Type u_3
inst✝ : TopologicalSpace I
hs : IsOpen[inst✝¹] s
hfs : IsOpen[inst✝²] (f ⁻¹' s)
x✝¹ : X
hx : x✝¹ ∈ s
h : IsEvenlyCovered (fun e ↦ f ↑e) x✝¹ I
inst : DiscreteTopology I
U : Set X
hxU : x✝¹ ∈ U
hU : IsOpen[inst✝¹] U
hfU : IsOpen[instTopologicalSpaceSubtype] ((fun e ↦ f ↑e) ⁻¹' U)
H : ↑((fun e ↦ f ↑e) ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑((fun e ↦ f ↑e) ⁻¹' U)), ↑(H x).1 = (fun e ↦ f ↑e) ↑x
x✝ : Nonempty I
hUs : U ⊆ s
this : Subtype.val '' (fun e ↦ f ↑e) ⁻¹' U = f ⁻¹' U
x : ↑(f ⁻¹' U)
⊢ ↑((((⋯.homeomorphImage ((fun e ↦ f ↑e) ⁻¹' U)).trans (Homeomorph.setCongr this)).symm.trans H) x).1 = f ↑x

Tactic:
by
    dsimp; convert! hH ⟨⟨x, hUs x.2⟩, x.2⟩ using 4; rw [Homeomorph.symm_apply_eq]; rfl

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

Goal state before:
pp: case refine_3
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
e₁ : E
h₁ : e₁ ∈ (fun x ↦ g • x) ⁻¹' U
e₂ : E
h₂ : e₂ ∈ (fun x ↦ g • x) ⁻¹' U
he✝ : f (g • e₁) = f (g • e₂)
g' : G
he : (fun m ↦ m • g • e₂) g' = g • e₁
⊢ (fun m ↦ m • g • e₂) g' = g • e₂

Tactic:
disjoint g' ⟨_, ⟨_, h₂, he⟩, h₁⟩

Goal state after:
case refine_3
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
e₁ : E
h₁ : e₁ ∈ (fun x ↦ g • x) ⁻¹' U
e₂ : E
h₂ : e₂ ∈ (fun x ↦ g • x) ⁻¹' U
he✝ : f (g • e₁) = f (g • e₂)
g' : G
he : (fun m ↦ m • g • e₂) g' = g • e₁
⊢ (fun m ↦ m • g • e₂) 1 = g • e₂
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: case refine_4
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)
⊢ ∀ (i : G), Set.SurjOn f ((fun x ↦ i • x) ⁻¹' U) (f '' U)

Tactic:
rintro g x ⟨e, hU, rfl⟩

Goal state after:
case refine_4
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
e : E
hU : e ∈ U
⊢ f e ∈ f '' (fun x ↦ g • x) ⁻¹' U
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

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

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

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

Goal state before:
pp: case refine_3
x y : Circle
hxy : x ≠ y
⊢ {x, y}ᶜ ∩ (range ⇑(x.path y) ∩ range ⇑(y.path x)) = ∅

Tactic:
(Tactic.tacticSeq1Indented
 [(Tactic.rwSeq
   "rw"
   (Tactic.optConfig [])
   (Tactic.rwRuleSeq "[" [(Tactic.rwRule [] (Term.app `range_path_inter_range_path [`hxy]))] "]")
   [])
  []
  (Tactic.exact
   "exact"
   (Term.app
    `compl_inter_self
    [(choice
      («term{_}» "{" [`x "," `y] "}")
      (Term.structInst
       "{"
       []
       (Term.structInstFields
        [(Term.structInstField (Term.structInstLVal `x []) [])
         ","
         (Term.structInstField (Term.structInstLVal `y []) [])])
       (Term.optEllipsis [])
       []
       "}"))]))])

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

Goal state before:
pp: n : ℤ
inst✝ : NeZero n
⊢ IsUnit ↑n

Tactic:
simpa using NeZero.ne n

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

Goal state before:
pp: case refine_1
𝕜 : 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
⊢ ‖adjointAux A‖ ≤ ‖A‖

Tactic:
refine ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fun x => ?_
    rw [adjointAux_apply, LinearIsometryEquiv.norm_map]
    exact toSesqForm_apply_norm_le

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
⊢ ContinuousOn argSelfAdjoint (ball 1 2)

Tactic:
rw [Topology.IsInducing.subtypeVal.continuousOn_iff]
  simp only [Function.comp_def, argSelfAdjoint_coe]
  rw [isOpen_ball.continuousOn_iff]
  intro u (hu : dist u 1 < 2)
  obtain ⟨ε, huε, hε2⟩ := exists_between (sq_lt_sq₀ (by positivity) (by positivity) |>.mpr hu)
  have hε : 0 < ε := lt_of_le_of_lt (by positivity) huε
  have huε' : dist u 1 < √ε := Real.lt_sqrt_of_sq_lt huε
  apply ContinuousOn.continuousAt ?_ (closedBall_mem_nhds_of_mem huε')
  apply ContinuousOn.image_comp_continuous ?_ continuous_subtype_val
  apply continuousOn_cfc A (s := sphere 0 1 ∩ {z | 2 * (1 - z.re) ≤ ε}) ?_ _ ?_ |>.mono
  · rintro - ⟨v, hv, rfl⟩
    simp only [Set.subset_inter_iff, Set.mem_ofPred_eq]
    refine ⟨inferInstance, spectrum_subset_circle v, ?_⟩
    intro z hz
    simp only [Set.mem_ofPred_eq]
    trans ‖(v - 1 : A)‖ ^ 2
    · exact two_mul_one_sub_le_norm_sub_one_sq v.2 hz
    · refine Real.le_sqrt (by positivity) (by positivity) |>.mp ?_
      simpa [Subtype.dist_eq, dist_eq_norm] using hv
  · exact isCompact_sphere 0 1 |>.inter_right <| isClosed_le (by fun_prop) (by fun_prop)
  · refine continuous_ofReal.comp_continuousOn <| continuousOn_arg.mono ?_
    apply subset_slitPlane_iff_of_subset_sphere Set.inter_subset_left |>.mpr
    norm_num at hε2 ⊢
    exact hε2

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u✝ : ↥(unitary A)
δ : ℝ
hδ₀ : 0 < δ
hδ₂ : δ < 2
u : ↥(unitary A)
hu✝ : u ∈ ball 1 δ
hu : ‖↑u - 1‖ < δ
⊢ JoinedIn (ball 1 δ) 1 u

Tactic:
refine ⟨path 1 u (hu.trans hδ₂), fun t ↦ ?_⟩

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u✝ : ↥(unitary A)
δ : ℝ
hδ₀ : 0 < δ
hδ₂ : δ < 2
u : ↥(unitary A)
hu✝ : u ∈ ball 1 δ
hu : ‖↑u - 1‖ < δ
t : ↑unitInterval
⊢ (path 1 u ⋯) t ∈ ball 1 δ
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : 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
u : H →L[𝕜] K
⊢ (∀ (x : H), ‖u x‖ = ‖x‖) ↔ adjoint u ∘SL u = 1

Tactic:
rw [LinearMap.norm_map_iff_inner_map_map u, u.inner_map_map_iff_adjoint_comp_self]

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
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
i : ↥s'
⊢ p -ᵥ s.centroid ∈ k ∙ u i

Tactic:
have hi := h i

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
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
i : ↥s'
hi : p ∈ s.median ↑i
⊢ p -ᵥ s.centroid ∈ k ∙ u 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
h : LinearIndependent k fun i ↦ s.points ↑i -ᵥ s.points 0
x✝ : { x // x ≠ 0 }
⊢ (-↑n)⁻¹ ≠ 0

Tactic:
simpa using NeZero.ne n

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

Goal state before:
pp: case h
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
p₁ : P
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ p_1 ∈ s, ∃ r, p_1 = r • v +ᵥ p
p₂ : P
hp₂ : p₂ ∈ s
⊢ ∃ r, p₂ = r • v +ᵥ p₁

Tactic:
rcases hv p₂ hp₂ with ⟨r, rfl⟩

Goal state after:
case h
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
p₁ : P
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ p_1 ∈ s, ∃ r, p_1 = r • v +ᵥ p
r : k
hp₂ : r • v +ᵥ p ∈ s
⊢ ∃ r_1, r • v +ᵥ p = r_1 • v +ᵥ p₁
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: case hr
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)
this : Set.range s.medial.points -ᵥ Set.range s.medial.points = (-↑n)⁻¹ • (Set.range s.points -ᵥ Set.range s.points)
⊢ IsUnit (-↑n)⁻¹

Tactic:
simpa using NeZero.ne n

Goal state after:
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
⊢ ∫ (x : G), f (g * x) ∂μ = ∫ (x : G), f x ∂μ

Tactic:
by
  have h_mul : MeasurableEmbedding fun x => g * x := (MeasurableEquiv.mulLeft g).measurableEmbedding
  rw [← h_mul.integral_map, map_mul_left_eq_self]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f ∞
hg : Memℓp g ∞
⊢ Memℓp (f + g) ∞

Tactic:
apply memℓp_infty
    obtain ⟨A, hA⟩ := hf.bddAbove
    obtain ⟨B, hB⟩ := hg.bddAbove
    refine ⟨A + B, ?_⟩
    rintro a ⟨i, rfl⟩
    exact le_trans (norm_add_le _ _) (add_le_add (hA ⟨i, rfl⟩) (hB ⟨i, rfl⟩))

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : HasSum (fun i ↦ ‖↑f i‖ ^ p.toReal) 0
⊢ f = 0

Tactic:
have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i ↦ by positivity

Goal state after:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : HasSum (fun i ↦ ‖↑f i‖ ^ p.toReal) 0
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
⊢ f = 0
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : (fun i ↦ ‖↑f i‖ ^ p.toReal) = 0
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
i : α
⊢ ↑f i = ↑0 i

Tactic:
have : f i = 0 ∧ p.toReal ≠ 0 := by
      simpa [Real.rpow_eq_zero_iff_of_nonneg (norm_nonneg (f i))] using! congr_fun hf i

Goal state after:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : (fun i ↦ ‖↑f i‖ ^ p.toReal) = 0
this✝ : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
i : α
this : ↑f i = 0 ∧ p.toReal ≠ 0
⊢ ↑f i = ↑0 i