mathlib-initiative/mathlib-tactics huggingface dataset:
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 : 1 ≤ a
⊢ a ^ (-1) ≤ 1

Tactic:
lift a to Aˣ using isUnit_of_le 1 ha
  rw [rpow_neg_one_eq_inv a (zero_le_one.trans ha)]
  exact inv_le_one ha

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha✝ : 0 ≤ a✝
hab✝ : a✝ ≤ b✝
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
hb : 0 ≤ b
⊢ ‖a‖ ≤ ‖b‖

Tactic:
exact (norm_le_iff_le_algebraMap a (norm_nonneg _) ha).2 <| hab.trans <|
    IsSelfAdjoint.le_algebraMap_norm_self (.of_nonneg hb)

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : IsSelfAdjoint b
this : ∀ (a b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)
⊢ star a * b * a ≤ ‖b‖ • (star a * a)

Tactic:
by
    rw [← Unitization.inr_le_iff _ _ (by aesop) ((IsSelfAdjoint.all _).smul (.star_mul_self a))]
    simpa [Unitization.norm_inr] using this a b <| hb.inr ℂ

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
⊢ cfc (fun x ↦ 1 - (1 + x)⁻¹) ↑a ≤ cfc (fun x ↦ 1 - (1 + x)⁻¹) ↑b

Tactic:
← inr_nonneg_iff

Goal state after:
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
⊢ cfc (fun x ↦ 1 - (1 + x)⁻¹) ↑a ≤ cfc (fun x ↦ 1 - (1 + x)⁻¹) ↑b
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
⊢ cfc (fun x ↦ 1 - (1 + x)⁻¹) c = 1 - cfc (fun x ↦ x⁻¹) (1 + c)

Tactic:
cfc_tsub _ _ _ (fun x _ ↦ by simp) (hg := by fun_prop (disch := intro _ _; positivity)),

Goal state after:
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
⊢ cfc (fun x ↦ 1) c - cfc (fun x ↦ (1 + x)⁻¹) c = 1 - cfc (fun x ↦ x⁻¹) (1 + c)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : TopologicalSpace X
f : X → R → R
a : A
s : Set X
h_cont : ContinuousOn (fun x ↦ (ofFun {quasispectrum R a}) (f x)) s
hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ x ∈ s, f x 0 = 0
⊢ ContinuousOn (fun x ↦ cfcₙ (f x) a) s

Tactic:
by
  rw [ContinuousOn] at h_cont ⊢
  simp only [ContinuousWithinAt, UniformOnFun.tendsto_iff_tendstoUniformlyOn, Set.mem_singleton_iff,
    Function.comp_def, toFun_ofFun, forall_eq] at h_cont
  refine fun x hx ↦ continuousWithinAt_cfcₙ_fun (h_cont x hx) ?_ ?_
  all_goals filter_upwards [self_mem_nhdsWithin] with x hx
  exacts [hf x hx, hf0 x hx]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝ m : A
hm₁ : 0 ≤ m
hm₂ : ‖↑m‖ < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ : cfc (fun y ↦ 1 - (1 + y)⁻¹) (ε⁻¹ ^ 2 • ↑m) ≤ ↑x
hx₂ : ‖↑x‖ ≤ 1
hx₀ : 0 ≤ x
⊢ ‖m - x * m‖₊ ≤ ε

Tactic:
← inr_nonneg_iff

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝ m : A
hm₁ : 0 ≤ ↑m
hm₂ : ‖↑m‖ < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ : cfc (fun y ↦ 1 - (1 + y)⁻¹) (ε⁻¹ ^ 2 • ↑m) ≤ ↑x
hx₂ : ‖↑x‖ ≤ 1
hx₀ : 0 ≤ ↑x
⊢ ‖m - x * m‖₊ ≤ ε
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: case frequently
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra 𝕜 A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C(↑(spectrum 𝕜 a), 𝕜)
hf : ∃ᶠ (g : C(↑(spectrum 𝕜 a), 𝕜)) in nhds f, Commute ((cfcHom ha) g) b
⊢ (cfcHom ha) f ∈ {x | x * b = b * x}

Tactic:
← (isClosed_eq (by fun_prop) (by fun_prop)).closure_eq

Goal state after:
case frequently
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra 𝕜 A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C(↑(spectrum 𝕜 a), 𝕜)
hf : ∃ᶠ (g : C(↑(spectrum 𝕜 a), 𝕜)) in nhds f, Commute ((cfcHom ha) g) b
⊢ (cfcHom ha) f ∈ closure {y | y * b = b * y}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: case frequently
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf : ∃ᶠ (g : C(↑(quasispectrum 𝕜 a), 𝕜)₀) in nhds f, Commute ((cfcₙHom ha) g) b
⊢ (cfcₙHom ha) f ∈ {x | x * b = b * x}

Tactic:
← (isClosed_eq (by fun_prop) (by fun_prop)).closure_eq

Goal state after:
case frequently
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf : ∃ᶠ (g : C(↑(quasispectrum 𝕜 a), 𝕜)₀) in nhds f, Commute ((cfcₙHom ha) g) b
⊢ (cfcₙHom ha) f ∈ closure {y | y * b = b * y}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : Module 𝕜 A
inst✝⁷ : IsScalarTower 𝕜 A A
inst✝⁶ : SMulCommClass 𝕜 A A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousConstSMul 𝕜 A
inst✝³ : StarModule 𝕜 A
inst✝² : IsTopologicalRing A
inst✝¹ : ContinuousStar A
inst✝ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
⊢ (adjoin 𝕜 (⇑(cfcₙHom ha) '' {ContinuousMapZero.id (quasispectrum 𝕜 a)})).topologicalClosure ≤ elemental 𝕜 a

Tactic:
simp [cfcₙHom_id ha, elemental]

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
this : 0 ≤ ↑(2 • e - e * e)
⊢ star (1 - ↑e) * (1 - ↑e) = 1 - ↑(2 • e - e * e)

Tactic:
simp [LE.le.star_eq, h1, mul_sub, sub_mul, two_smul, sub_sub, add_sub]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
h : p ≤ q
⊢ p * q = q * p

Tactic:
hp.le_iff_mul_eq_right hq |>.mp h,

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
h : p ≤ q
⊢ p * q = p
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
⊢ x ∈ Multiset.map (fun x ↦ ‖U i x‖ ^ 2) Finset.univ.val → 0 ≤ x

Tactic:
h_x

Goal state after:
case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
h_x : x ∈ Multiset.map (fun x ↦ ‖U i x‖ ^ 2) Finset.univ.val
⊢ 0 ≤ x
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: 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
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ extend f (↑e) (fun x ↦ Classical.arbitrary Z) (f x₀) ∈ e.target

Tactic:
hf.injective.extend_apply e

Goal state after:
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
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ ↑e x₀ ∈ e.target
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case fst
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x✝ : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
x : { x // x ∈ s } × F
hx : x ∈ e.target
⊢ (↑(↑e
              (if h : (Prod.map Subtype.val id x).1 ∈ s then
                e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
              else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).1,
        (↑e
            (if h : (Prod.map Subtype.val id x).1 ∈ s then
              e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
            else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).2).1 =
    (Prod.map Subtype.val id x).1

Tactic:
simp [e.apply_symm_apply hx]

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

Goal state before:
pp: case snd
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x✝ : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
x : { x // x ∈ s } × F
hx : x ∈ e.target
⊢ (↑(↑e
              (if h : (Prod.map Subtype.val id x).1 ∈ s then
                e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
              else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).1,
        (↑e
            (if h : (Prod.map Subtype.val id x).1 ∈ s then
              e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
            else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).2).2 =
    (Prod.map Subtype.val id x).2

Tactic:
simp [e.apply_symm_apply hx]

Goal state after:
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h :
  ∀ (a b : X) (b_1 : f a = f b),
    ⟨(a, b), b_1⟩ ∈ Function.pullbackDiagonal f → ∃ t ∈ 𝓝 a ×ˢ 𝓝 b, Subtype.val ⁻¹' t ⊆ Function.pullbackDiagonal f
x : X
t : Set (X × X)
ht : t ∈ 𝓝 x ×ˢ 𝓝 x
t_sub : Subtype.val ⁻¹' t ⊆ Function.pullbackDiagonal f
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
obtain ⟨t₁, h₁, t₂, h₂, prod_sub⟩ := Filter.mem_prod_iff.mp ht

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h :
  ∀ (a b : X) (b_1 : f a = f b),
    ⟨(a, b), b_1⟩ ∈ Function.pullbackDiagonal f → ∃ t ∈ 𝓝 a ×ˢ 𝓝 b, Subtype.val ⁻¹' t ⊆ Function.pullbackDiagonal f
x : X
t : Set (X × X)
ht : t ∈ 𝓝 x ×ˢ 𝓝 x
t_sub : Subtype.val ⁻¹' t ⊆ Function.pullbackDiagonal f
t₁ : Set X
h₁ : t₁ ∈ 𝓝 x
t₂ : Set X
h₂ : t₂ ∈ 𝓝 x
prod_sub : t₁ ×ˢ t₂ ⊆ t
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: case snd
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ (↑𝕜 x).toProd.2 = ((algebraMap 𝕜 𝓜(𝕜, 𝕜)) x).toProd.2

Tactic:
refine ContinuousLinearMap.ext fun y => ?_
    exact mul_comm y x

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
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
i : I
⊢ ↑(H.symm (⟨x, hxU⟩, i)) ∈ f ⁻¹' {x}

Tactic:
by simp [← 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
x : X
h : IsEvenlyCovered f x I
⊢ I ≃ₜ ↑(f ⁻¹' {x})

Tactic:
choose _ U hxU hU hfU H hH using h
  exact
  { toFun i := ⟨H.symm (⟨x, hxU⟩, i), by simp [← hH]⟩
    invFun e := (H ⟨e, by rwa [Set.mem_preimage, (e.2 : f e = x)]⟩).2
    left_inv _ := by simp
    right_inv e := Set.inclusion_injective (Set.preimage_mono (Set.singleton_subset_iff.mpr hxU)) <|
      H.injective <| Prod.ext (Subtype.ext <| by simpa [hH] using e.2.symm) (by simp)
    continuous_toFun := by fun_prop
    continuous_invFun := by fun_prop }

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
h : IsEvenlyCovered f x I
⊢ I ≃ₜ ↑(f ⁻¹' {x})

Tactic:
by
  choose _ U hxU hU hfU H hH using h
  exact
  { toFun i := ⟨H.symm (⟨x, hxU⟩, i), by simp [← hH]⟩
    invFun e := (H ⟨e, by rwa [Set.mem_preimage, (e.2 : f e = x)]⟩).2
    left_inv _ := by simp
    right_inv e := Set.inclusion_injective (Set.preimage_mono (Set.singleton_subset_iff.mpr hxU)) <|
      H.injective <| Prod.ext (Subtype.ext <| by simpa [hH] using e.2.symm) (by simp)
    continuous_toFun := by fun_prop
    continuous_invFun := by fun_prop }

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
x : ↑(Subtype.val ⁻¹' U) × I
⊢ ↑(H.symm (⟨↑↑x.1, ⋯⟩, x.2)) ∈ f ⁻¹' s

Tactic:
by simp [← 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
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
x : ↑(Subtype.val ⁻¹' U) × I
⊢ ⟨↑(H.symm (⟨↑↑x.1, ⋯⟩, x.2)), ⋯⟩ ∈ s.restrictPreimage f ⁻¹' Subtype.val ⁻¹' U

Tactic:
by simp [← 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
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✝ : IsEmpty ↑(f ⁻¹' {x})
⊢ f ⁻¹' W = ∅

Tactic:
by simpa using hWV

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

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ ⇑(x.path y) '' insert 0 (Ioc 0 1) ∩ ⇑(y.path x) '' insert 0 (Ioc 0 1) = {x, y}

Tactic:
← Ioo_insert_right (by simp)

Goal state after:
x y : Circle
h : x ≠ y
⊢ ⇑(x.path y) '' insert 0 (insert 1 (Ioo 0 1)) ∩ ⇑(y.path x) '' insert 0 (insert 1 (Ioo 0 1)) = {x, y}
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
⊢ spectrum ℂ u ⊆ slitPlane ↔ ‖u - 1‖ < 2

Tactic:
simp [subset_slitPlane_iff_of_subset_sphere (spectrum.subset_circle_of_unitary hu),
    norm_sub_one_lt_two_iff hu]

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
inst✝¹ : CompleteSpace E
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
⊢ adjoint (adjoint U.subtypeL) = U.subtypeL

Tactic:
adjoint_adjoint

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
⊢ U.subtypeL = U.subtypeL
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
⊢ IsSelfAdjoint (U.starProjection ∘SL T ∘SL U.starProjection)

Tactic:
by
  rw [← mul_def, ← mul_def, ← mul_assoc]
  exact hT.conjugate_self <| isSelfAdjoint_starProjection U

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
⊢ (∀ (x : E), (↑(star T * T) - ↑(T * star T)) x = ↑0 x) ↔ ∀ (v : E), ‖↑T v‖ = ‖↑(adjoint T) v‖

Tactic:
← LinearMap.ext_iff,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
⊢ ↑(star T * T) - ↑(T * star T) = ↑0 ↔ ∀ (v : E), ‖↑T v‖ = ‖↑(adjoint T) v‖
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
⊢ finrank 𝕜 ↥(adjoint A).ker + finrank 𝕜 ↥(adjoint (adjoint A)).range - finrank 𝕜 ↥(adjoint A).ker = finrank 𝕜 ↥A.range

Tactic:
adjoint_adjoint

Goal state after:
𝕜 : 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
⊢ finrank 𝕜 ↥(adjoint A).ker + finrank 𝕜 ↥A.range - finrank 𝕜 ↥(adjoint A).ker = finrank 𝕜 ↥A.range
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 : Set.univ.indicator (centroidWeightsIndicator k fs₁) = Set.univ.indicator (centroidWeightsIndicator k fs₂)
⊢ fs₁ = fs₂

Tactic:
Set.indicator_univ,

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 : centroidWeightsIndicator k fs₁ = centroidWeightsIndicator k fs₂
⊢ fs₁ = fs₂
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
f g : H ≃ₗᵢ[𝕜] K
x✝ : ∃ y, y • 1 = ↑(↑g).symm ∘SL ↑↑f
y : 𝕜
h : y • 1 = ↑(↑g).symm ∘SL ↑↑f
hy : y = 0
x : H
⊢ f x = (1 • g) x

Tactic:
simp [by simpa [hy] using congr($h x).symm]

Goal state after:
Module: Mathlib.Analysis.Calculus.BumpFunction.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
⊢ support ↑f = ball c f.rOut

Tactic:
simp only [toFun, support_comp_eq_preimage, ContDiffBumpBase.support _ _ f.one_lt_rOut_div_rIn]
  ext x
  simp only [mem_ball_iff_norm, sub_zero, norm_smul, mem_preimage, Real.norm_eq_abs, abs_inv,
    abs_of_pos f.rIn_pos, ← div_eq_inv_mul, div_lt_div_iff_of_pos_right f.rIn_pos]

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
inst✝² : Group G
inst✝¹ : MeasurableInv G
f : G → E
μ : Measure G
inst✝ : μ.IsInvInvariant
h : MeasurableEmbedding fun x ↦ x⁻¹
⊢ ∫ (x : G), f x⁻¹ ∂μ = ∫ (x : G), f x ∂μ

Tactic:
← h.integral_map,

Goal state after:
G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Group G
inst✝¹ : MeasurableInv G
f : G → E
μ : Measure G
inst✝ : μ.IsInvInvariant
h : MeasurableEmbedding fun x ↦ x⁻¹
⊢ ∫ (y : G), f y ∂map (fun x ↦ x⁻¹) μ = ∫ (x : G), f x ∂μ
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: α : Type u_3
E : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
G : Type u_7
inst✝⁴ : Group G
inst✝³ : MeasurableSpace α
inst✝² : MulAction G α
inst✝¹ : MeasurableConstSMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
f : α → E
g : G
h : MeasurableEmbedding fun x ↦ g • x
⊢ ∫ (x : α), f (g • x) ∂μ = ∫ (x : α), f x ∂μ

Tactic:
← h.integral_map,

Goal state after:
α : Type u_3
E : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
G : Type u_7
inst✝⁴ : Group G
inst✝³ : MeasurableSpace α
inst✝² : MulAction G α
inst✝¹ : MeasurableConstSMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
f : α → E
g : G
h : MeasurableEmbedding fun x ↦ g • x
⊢ ∫ (y : α), f y ∂map (fun x ↦ g • x) μ = ∫ (x : α), f x ∂μ