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

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✝² : StarModule ℂ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝ : ContinuousMapZero.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf : ContinuousOn f (quasispectrum ℂ ↑(ℑ a))
hf0 : f 0 = 0
ha : IsStarNormal a
⊢ cfcₙ f ↑(ℑ a) = cfcₙ (fun x ↦ f ↑x.im) a

Tactic:
quasispectrum_imaginaryPart a

Goal state after:
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✝² : StarModule ℂ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝ : ContinuousMapZero.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf : ContinuousOn f ((fun x ↦ ↑x.im) '' quasispectrum ℂ a)
hf0 : f 0 = 0
ha : IsStarNormal a
⊢ cfcₙ f ↑(ℑ a) = cfcₙ (fun x ↦ f ↑x.im) a
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: case e_a
A : Type u_1
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
M : CStarMatrix n n A
v : C⋆ᵐᵒᵈ(A, n → A)
⊢ toCLM Mᴴ ∘SL toCLM M = toCLM (M * star M)

Tactic:
apply MulOpposite.op_injective

Goal state after:
case e_a
A : Type u_1
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
M : CStarMatrix n n A
v : C⋆ᵐᵒᵈ(A, n → A)
⊢ MulOpposite.op (toCLM Mᴴ ∘SL toCLM M) = MulOpposite.op (toCLM (M * star M))
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: case e_a
A : Type u_1
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
M : CStarMatrix n n A
v : C⋆ᵐᵒᵈ(A, n → A)
⊢ MulOpposite.op (toCLM Mᴴ ∘SL toCLM M) = MulOpposite.op (toCLM (M * star M))

Tactic:
simp only [← toCLMNonUnitalAlgHom_eq_toCLM, map_mul]

Goal state after:
case e_a
A : Type u_1
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
M : CStarMatrix n n A
v : C⋆ᵐᵒᵈ(A, n → A)
⊢ MulOpposite.op (toCLM Mᴴ ∘SL toCLM M) = toCLMNonUnitalAlgHom M * toCLMNonUnitalAlgHom (star M)
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✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : NormedSpace 𝕜 A
inst✝⁷ : IsScalarTower 𝕜 A A
inst✝⁶ : SMulCommClass 𝕜 A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝⁴ : CompleteSpace A
inst✝³ : NormedSpace ℝ A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)
hf : ContinuousOn (uncurry f) (univ ×ˢ quasispectrum 𝕜 a)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
⊢ cfcₙ (fun r ↦ ∫ (x : X), f x r ∂μ) a = ∫ (x : X), cfcₙ (f x) a ∂μ

Tactic:
by
  have : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a) := .of_forall fun x ↦
    hf.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨Set.mem_univ _, hz⟩
  refine cfcₙ_integral' _ _ this f_zero ⟨?_, ?_⟩ ha
  · exact aeStronglyMeasurable_mkD_restrict_of_uncurry _ _ hf f_zero
  · exact hasFiniteIntegral_mkD_restrict_of_bound f _ this f_zero bound bound_int bound_ge

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

Goal state before:
pp: case refine_1.snd
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
hx : (x, y) ∈ s ×ˢ t
h :
  (∀ ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1) ∧
    ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → (x, y).2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).2
x₁ : E × F
hx₁ : x₁ ∈ s ×ˢ t
x₂ : E × F
hx₂ : x₂ ∈ s ×ˢ t
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : a • x₁ + b • x₂ = (x, y)
⊢ x₁.2 = (x, y).2

Tactic:
exact h.2 hx₁.2 hx₂.2 ⟨a, b, ha, hb, hab, congrArg Prod.snd hx'⟩

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

Goal state before:
pp: case refine_3
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
hx : (x, y) ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y)
⊢ ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → (x, y).2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).2

Tactic:
· rintro x₁ hx₁ x₂ hx₂ hx_snd
    refine congrArg Prod.snd (h (mk_mem_prod hx.1 hx₁) (mk_mem_prod hx.1 hx₂) ?_)
    rw [← Prod.image_mk_openSegment_right]
    exact mem_image_of_mem _ hx_snd

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
i : n
⊢ ‖v i‖ = ‖T (toLp 2 (Pi.single i 1))‖

Tactic:
by
          rw [toEuclideanCLM_toLp (diagonal v) (Pi.single i (1 : 𝕜))]
          simp

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

Goal state before:
pp: case hf
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
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 : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : Nonempty X
F : X' → Z := extend f ↑e fun x ↦ Classical.arbitrary Z
F_eq : F = extend f ↑e fun x ↦ Classical.arbitrary Z
heq : EqOn F (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)
this : ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' univ)
⊢ ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)

Tactic:
exact this.mono <| image_mono <| subset_univ _

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.target ∩ ↑(e.lift_openEmbedding hf).symm ⁻¹' (e'.lift_openEmbedding hf).source ↔
    z ∈ e.target ∩ ↑e.symm ⁻¹' e'.source

Tactic:
e.lift_openEmbedding_symm,

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 ⁻¹' (e'.lift_openEmbedding hf).source ↔ z ∈ e.target ∩ ↑e.symm ⁻¹' e'.source
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace F
E : B → Type u_5
inst✝³ : TopologicalSpace (TotalSpace F E)
inst✝² : (b : B) → TopologicalSpace (E b)
inst✝¹ : FiberBundle F E
inst✝ : T1Space B
x : B
⊢ IsClosed[inst✝³] (range (TotalSpace.mk x))

Tactic:
by
    rw [TotalSpace.range_mk]
    exact isClosed_singleton.preimage <| continuous_proj F E

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
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : ∀ (x : B), Nonempty (E x)
e : Trivialization F TotalSpace.proj
⊢ ContinuousOn (fun z ↦ TotalSpace.mk' F z.1 (e.symm z.1 z.2)) (e.baseSet ×ˢ univ)

Tactic:
by
  have : ∀ z ∈ e.baseSet ×ˢ (univ : Set F),
      TotalSpace.mk z.1 (e.symm z.1 z.2) = e.toOpenPartialHomeomorph.symm z := by
    rintro x ⟨hx : x.1 ∈ e.baseSet, _⟩
    rw [e.mk_symm hx]
  refine ContinuousOn.congr ?_ this
  rw [← e.target_eq]
  exact e.toOpenPartialHomeomorph.continuousOn_symm

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
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.domRestrict f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.domRestrict f)
⊢ IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion ⋯))

Tactic:
Set.range_inclusion

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.domRestrict f)
x : X
hx : x ∈ s
U : Set X
hU : U ∈ 𝓝 x
emb : IsOpenEmbedding (U.domRestrict f)
⊢ IsOpen[instTopologicalSpaceSubtype] {x | ↑x ∈ interior U}
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: case refine_1
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CStarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : (Metric.closedBall 0 1).Nonempty
key : ∀ (x y : A), ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖a.toProd.2 (star (a.toProd.1 (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
⊢ ∀
    a_1 ∈
      (fun a_2 ↦ sSup ((fun x ↦ ‖a.toProd.2 (star (a.toProd.1 (star a_2))) * x‖₊) '' Metric.closedBall 0 1)) ''
        Metric.closedBall 0 1,
    a_1 ≤ ‖a‖₊ * ‖a‖₊

Tactic:
rintro - ⟨x, hx, rfl⟩
        refine csSup_le (hball.image _) ?_
        rintro - ⟨y, hy, rfl⟩
        exact key x y (mem_closedBall_zero_iff.1 hx) (mem_closedBall_zero_iff.1 hy)

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
x : X
hxs : x ∈ s
h : IsEvenlyCovered f x I
inst : 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 : ↑(s.restrictPreimage f ⁻¹' Subtype.val ⁻¹' U)
⊢ ⟨↑(H ⟨↑↑e, ⋯⟩).1, ⋯⟩ ∈ Subtype.val ⁻¹' U

Tactic:
by simpa only [hH] using! e.2

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

Goal state before:
pp: case refine_1
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
e : E
x✝ : e ∈ f ⁻¹' f '' U
e' : E
heU : e' ∈ U
he : f e' = f e
⊢ e ∈ ⋃ g, (fun x ↦ g • x) ⁻¹' U

Tactic:
obtain ⟨g, rfl⟩ := hfG.mp he; exact ⟨_, ⟨g, rfl⟩, heU⟩

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

Goal state before:
pp: case refine_3
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
e₁ : E
hf : IsEvenlyCovered f (f e₁) ↑(f ⁻¹' {f e₁})
e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this✝ : Nonempty ↑(f ⁻¹' {f e₁})
t : Trivialization (↑(f ⁻¹' {f e₁})) f := hf.toTrivialization
this : DiscreteTopology ↑(f ⁻¹' {f e₁})
he₁ : e₁ ∈ t.source
he₂ : e₂ ∈ t.source
x : E
h₁ : x ∈ t.source ∩ Prod.snd ∘ ↑t ⁻¹' {(↑t e₁).2}
h₂ : x ∈ t.source ∩ Prod.snd ∘ ↑t ⁻¹' {(↑t e₂).2}
⊢ f e₁ = (↑t.toOpenPartialHomeomorph e₂).1

Tactic:
t.proj_toFun e₂ he₂

Goal state after:
case refine_3
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
e₁ : E
hf : IsEvenlyCovered f (f e₁) ↑(f ⁻¹' {f e₁})
e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this✝ : Nonempty ↑(f ⁻¹' {f e₁})
t : Trivialization (↑(f ⁻¹' {f e₁})) f := hf.toTrivialization
this : DiscreteTopology ↑(f ⁻¹' {f e₁})
he₁ : e₁ ∈ t.source
he₂ : e₂ ∈ t.source
x : E
h₁ : x ∈ t.source ∩ Prod.snd ∘ ↑t ⁻¹' {(↑t e₁).2}
h₂ : x ∈ t.source ∩ Prod.snd ∘ ↑t ⁻¹' {(↑t e₂).2}
⊢ f e₁ = f e₂
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case refine_3
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)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
F : PartialEquiv E (X × ι) :=
  { toFun := fun e ↦ (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι),
    invFun := fun x ↦ if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1, source := f ⁻¹' V,
    target := V ×ˢ Set.univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }
open_preim : ∀ {W : Set X}, W ⊆ V → IsOpen[inst✝⁴] W → IsOpen[inst✝⁵] (f ⁻¹' W)
open_source : IsOpen[inst✝⁵] F.source
cont_f : ContinuousOn f F.source
i : ι
⊢ ContinuousOn (fun x ↦ if h : x ∈ V then inv i ⋯ else Classical.arbitrary (X → E) x) {a | (a, i) ∈ V ×ˢ Set.univ}

Tactic:
Set.prodMk_mem_set_prod_eq,

Goal state after:
case refine_3
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)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
F : PartialEquiv E (X × ι) :=
  { toFun := fun e ↦ (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι),
    invFun := fun x ↦ if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1, source := f ⁻¹' V,
    target := V ×ˢ Set.univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }
open_preim : ∀ {W : Set X}, W ⊆ V → IsOpen[inst✝⁴] W → IsOpen[inst✝⁵] (f ⁻¹' W)
open_source : IsOpen[inst✝⁵] F.source
cont_f : ContinuousOn f F.source
i : ι
⊢ ContinuousOn (fun x ↦ if h : x ∈ V then inv i ⋯ else Classical.arbitrary (X → E) x) {a | a ∈ V ∧ i ∈ Set.univ}
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
⊢ exp
      ((if (↑(exp (↑x).arg)).arg ≤ (↑y).arg then (↑y).arg - (↑(exp (↑x).arg)).arg
        else 2 * π + (↑y).arg - (↑(exp (↑x).arg)).arg) +
        (↑x).arg) =
    y

Tactic:
split_ifs with hxy

Goal state after:
case pos
x y : Circle
hxy : (↑(exp (↑x).arg)).arg ≤ (↑y).arg
⊢ exp ((↑y).arg - (↑(exp (↑x).arg)).arg + (↑x).arg) = y

case neg
x y : Circle
hxy : ¬(↑(exp (↑x).arg)).arg ≤ (↑y).arg
⊢ exp (2 * π + (↑y).arg - (↑(exp (↑x).arg)).arg + (↑x).arg) = y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

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

Tactic:
← path_image_Ioc_of_ne h,

Goal state after:
x y : Circle
h : x ≠ y
⊢ (insert (exp (↑x).arg) (⇑(x.path y) '' Ioc 0 1))ᶜ = ⇑(y.path x) '' Ioo 0 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: ⊢ Filter.Tendsto (fun i ↦ π / 2 ^ (i + 1)) Filter.atTop (nhds 0)

Tactic:
div_eq_mul_inv,

Goal state after:
⊢ Filter.Tendsto (fun i ↦ π * (2 ^ (i + 1))⁻¹) Filter.atTop (nhds 0)
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

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

Tactic:
obtain (rfl | hx) := eq_or_ne x 0

Goal state after:
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

case inr
A : Type u_1
inst✝ : CStarAlgebra A
x : A
x✝¹ : (A : Type ?u.39) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
x✝ : ∀ (A : Type ?u.41) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
⊢ ∃ u c, x = ∑ i, c i • ↑(u i) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ ‖x‖ / 2
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 - T * T) x‖ = 0) ↔ T - T * T = 0

Tactic:
by simp only [norm_eq_zero, ContinuousLinearMap.ext_iff, zero_apply]

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)⁻¹ • (n + 1) • (s.points j -ᵥ s.points i) + (s.points i -ᵥ s.points j) = (↑n)⁻¹ • (s.points j -ᵥ s.points i)

Tactic:
have : (s.points i -ᵥ s.points j) = -(s.points j -ᵥ s.points i) := by simp

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))
this : s.points i -ᵥ s.points j = -(s.points j -ᵥ s.points i)
⊢ (↑n)⁻¹ • (n + 1) • (s.points j -ᵥ s.points i) + (s.points i -ᵥ s.points j) = (↑n)⁻¹ • (s.points j -ᵥ s.points i)
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: case e_a
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)⁻¹ - (↑n + 1)⁻¹)

Tactic:
mul_sub,

Goal state after:
case e_a
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)⁻¹ - (↑n + 1) * (↑n + 1)⁻¹
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: case e_a
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)⁻¹) = -(↑n + 1)⁻¹

Tactic:
mul_sub,

Goal state after:
case e_a
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 * (↑n)⁻¹ = -(↑n + 1)⁻¹
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✝ : μ.IsMulRightInvariant
f : G → E
g : G
⊢ ∫ (x : G), f (x / g) ∂μ = ∫ (x : G), f x ∂μ

Tactic:
div_eq_mul_inv,

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✝ : μ.IsMulRightInvariant
f : G → E
g : G
⊢ ∫ (x : G), f (x * g⁻¹) ∂μ = ∫ (x : G), f x ∂μ
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
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → E
μ : Measure G
inst✝¹ : μ.IsInvInvariant
inst✝ : μ.IsMulLeftInvariant
x' : G
⊢ ∫ (x : G), f (x' / x) ∂μ = ∫ (x : G), f x ∂μ

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_4
E : Type u_5
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → E
μ : Measure G
inst✝¹ : μ.IsInvInvariant
inst✝ : μ.IsMulLeftInvariant
x' : G
⊢ ∫ (x : G), f (x' * x⁻¹) ∂μ = ∫ (x : G), f x ∂μ
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
⊢ ℝ

Tactic:
exact ((lp.memℓp f).finite_dsupport.toFinset.card : ℝ)

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

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
⊢ 0 ≤ ‖f‖

Tactic:
by
  rcases p.trichotomy with (rfl | rfl | hp)
  · simp [lp.norm_eq_card_dsupport f]
  · rcases isEmpty_or_nonempty α with _i | _i
    · rw [lp.norm_eq_ciSup]
      simp [Real.iSup_of_isEmpty]
    inhabit α
    exact (norm_nonneg (f default)).trans ((lp.isLUB_norm f).1 ⟨default, rfl⟩)
  · rw [lp.norm_eq_tsum_rpow hp f]
    exact Real.rpow_nonneg (tsum_nonneg fun i ↦ by positivity) _

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

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
h : ‖f‖ = 0
i : α
⊢ ↑f i = ↑0 i

Tactic:
have : { i : α | ¬f i = 0 } = ∅ := by simpa [lp.norm_eq_card_dsupport f] using! h

Goal state after:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
h : ‖f‖ = 0
i : α
this : {i | ¬↑f i = 0} = ∅
⊢ ↑f i = ↑0 i
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 : ↥(lp E ∞)
h : ‖f‖ = 0
⊢ f = 0

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

Tactic:
· rcases isEmpty_or_nonempty α with _i | _i
    · simp [eq_iff_true_of_subsingleton]
    have H : IsLUB (Set.range fun i => ‖f i‖) 0 := by simpa [h] using! lp.isLUB_norm f
    ext i
    have : ‖f i‖ = 0 := le_antisymm (H.1 ⟨i, rfl⟩) (norm_nonneg _)
    simpa using! this

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