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

Goal state before:
pp: case add
𝕜 : 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 g : C(↑(spectrum 𝕜 a), 𝕜)
hf : Commute ((cfcHom ha) f) b
hg : Commute ((cfcHom ha) g) b
⊢ Commute ((cfcHom ha) (f + g)) b

Tactic:
| add f g hf hg =>

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

Goal state before:
pp: case add
𝕜 : 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 g : C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf : Commute ((cfcₙHom ha) f) b
hg : Commute ((cfcₙHom ha) g) b
⊢ Commute ((cfcₙHom ha) (f + g)) b

Tactic:
| add f g hf hg =>

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompactSpace Y
inst✝³ : Zero Y
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(Y, E)
f : X → Y → E
g : C(Y, E)₀
f_cont : Continuous (Function.uncurry f)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
x : X
zero_x : f x 0 = 0
⊢ ContinuousMap.mkD (f x) ↑g = ↑(mkD (f x) g)

Tactic:
mkD_eq_mkD_of_map_zero _ _ zero_x

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompactSpace Y
inst✝³ : Zero Y
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(Y, E)
f : X → Y → E
g : C(Y, E)₀
f_cont : Continuous (Function.uncurry f)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
x : X
zero_x : f x 0 = 0
⊢ ContinuousMap.mkD (f x) ↑g = ContinuousMap.mkD (f x) ↑g
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompactSpace Y
inst✝³ : Zero Y
s : Set X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(Y, E)
hs : MeasurableSet s
f : X → Y → E
g : C(Y, E)₀
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ univ)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
x : X
zero_x : f x 0 = 0
⊢ ContinuousMap.mkD (f x) ↑g = ↑(mkD (f x) g)

Tactic:
mkD_eq_mkD_of_map_zero _ _ zero_x

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompactSpace Y
inst✝³ : Zero Y
s : Set X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(Y, E)
hs : MeasurableSet s
f : X → Y → E
g : C(Y, E)₀
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ univ)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
x : X
zero_x : f x 0 = 0
⊢ ContinuousMap.mkD (f x) ↑g = ContinuousMap.mkD (f x) ↑g
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
t : Set Y
inst✝⁴ : CompactSpace ↑t
inst✝³ : Zero ↑t
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(↑t, E)
f : X → Y → E
g : C(↑t, E)₀
f_cont : ContinuousOn (Function.uncurry f) (univ ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ, f x ↑0 = 0
x : X
zero_x : f x ↑0 = 0
⊢ ContinuousMap.mkD (t.domRestrict (f x)) ↑g = ↑(mkD (t.domRestrict (f x)) g)

Tactic:
mkD_eq_mkD_of_map_zero _ _ zero_x

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
t : Set Y
inst✝⁴ : CompactSpace ↑t
inst✝³ : Zero ↑t
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(↑t, E)
f : X → Y → E
g : C(↑t, E)₀
f_cont : ContinuousOn (Function.uncurry f) (univ ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ, f x ↑0 = 0
x : X
zero_x : f x ↑0 = 0
⊢ ContinuousMap.mkD (t.domRestrict (f x)) ↑g = ContinuousMap.mkD (t.domRestrict (f x)) ↑g
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
s : Set X
t : Set Y
inst✝⁴ : CompactSpace ↑t
inst✝³ : Zero ↑t
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(↑t, E)
hs : MeasurableSet s
f : X → Y → E
g : C(↑t, E)₀
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x ↑0 = 0
x : X
zero_x : f x ↑0 = 0
⊢ ContinuousMap.mkD (t.domRestrict (f x)) ↑g = ↑(mkD (t.domRestrict (f x)) g)

Tactic:
mkD_eq_mkD_of_map_zero _ _ zero_x

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
s : Set X
t : Set Y
inst✝⁴ : CompactSpace ↑t
inst✝³ : Zero ↑t
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(↑t, E)
hs : MeasurableSet s
f : X → Y → E
g : C(↑t, E)₀
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x ↑0 = 0
x : X
zero_x : f x ↑0 = 0
⊢ ContinuousMap.mkD (t.domRestrict (f x)) ↑g = ContinuousMap.mkD (t.domRestrict (f x)) ↑g
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: A : Type u_1
inst✝¹⁴ : NonUnitalRing A
inst✝¹³ : StarRing A
inst✝¹² : Module ℝ A
inst✝¹¹ : IsScalarTower ℝ A A
inst✝¹⁰ : SMulCommClass ℝ A A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : IsTopologicalRing A
inst✝⁷ : T2Space A
inst✝⁶ : PartialOrder A
inst✝⁵ : NonnegSpectrumClass ℝ A
inst✝⁴ : StarOrderedRing A
inst✝³ : StarModule ℝ A
inst✝² : ContinuousStar A
inst✝¹ : ContinuousConstSMul ℝ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ (fun x ↦ cfcₙ x a) '' {f | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x} ⊆ ↑(NonUnitalStarAlgebra.elemental ℝ a) ∩ {a | 0 ≤ a}

Tactic:
← range_cfcₙ_subset _ ha.isSelfAdjoint,

Goal state after:
A : Type u_1
inst✝¹⁴ : NonUnitalRing A
inst✝¹³ : StarRing A
inst✝¹² : Module ℝ A
inst✝¹¹ : IsScalarTower ℝ A A
inst✝¹⁰ : SMulCommClass ℝ A A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : IsTopologicalRing A
inst✝⁷ : T2Space A
inst✝⁶ : PartialOrder A
inst✝⁵ : NonnegSpectrumClass ℝ A
inst✝⁴ : StarOrderedRing A
inst✝³ : StarModule ℝ A
inst✝² : ContinuousStar A
inst✝¹ : ContinuousConstSMul ℝ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ (fun x ↦ cfcₙ x a) '' {f | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x} ⊆ (Set.range fun x ↦ cfcₙ x a) ∩ {a | 0 ≤ a}
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ (x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) → x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x

pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ (x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x

Tactic:
· rw [← insert_endpoints_openSegment]
    rintro H (rfl | rfl | hx)
    exacts [Or.inl rfl, Or.inr rfl, Or.inl <| (H hx).1]

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ (x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : 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
⊢ ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2

Tactic:
apply Multiset.single_le_sum

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 ∈ Multiset.map (fun x ↦ ‖U i x‖ ^ 2) Finset.univ.val, 0 ≤ x

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
⊢ ‖U i j‖ ^ 2 ∈ Multiset.map (fun x ↦ ‖U i x‖ ^ 2) Finset.univ.val
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : 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
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x, ‖U i x‖ ^ 2)
re_diag_eq_norm_sum : RCLike.re ((U * Uᴴ) i i) = ∑ x, ‖U i x‖ ^ 2
⊢ ‖U i j‖ ≤ 1

Tactic:
have mul_eq_one : U * Uᴴ = 1 := Unitary.mul_star_self_of_mem hU

Goal state after:
𝕜 : 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
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x, ‖U i x‖ ^ 2)
re_diag_eq_norm_sum : RCLike.re ((U * Uᴴ) i i) = ∑ x, ‖U i x‖ ^ 2
mul_eq_one : U * Uᴴ = 1
⊢ ‖U i j‖ ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ‖Aᴴ * A‖ = ‖A‖ * ‖A‖

Tactic:
rw [l2_opNorm_def, toEuclideanLin_eq_toLin_orthonormal, LinearEquiv.trans_apply,
    Matrix.toLin_mul (v₂ := (EuclideanSpace.basisFun m 𝕜).toBasis), toLin_conjTranspose]
  exact ContinuousLinearMap.norm_adjoint_comp_self _

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
Z' : Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : X ≃ₜ Y
f : OpenPartialHomeomorph Y Z
f' : OpenPartialHomeomorph Z Z'
⊢ (e.transOpenPartialHomeomorph f).trans f' = e.transOpenPartialHomeomorph (f.trans f')

Tactic:
simp only [transOpenPartialHomeomorph_eq_trans, OpenPartialHomeomorph.trans_assoc]

Goal state after:
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
⊢ (f ∘ e.invFun) (extend f (↑e) (fun x ↦ Classical.arbitrary Z) (f x₀)) = f x₀

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
⊢ (f ∘ e.invFun) (↑e x₀) = f 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
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
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ extend f (↑e) (fun x ↦ Classical.arbitrary Z) (f x₀) =
    (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f x₀)

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
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
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ ↑e x₀ = (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f x₀)
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case h
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)
x' : X'
x : X
hx : x ∈ e.source
hx'x : f x = x'
⊢ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm x' ∈ e.source

Tactic:
← hx'x,

Goal state after:
case h
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)
x' : X'
x : X
hx : x ∈ e.source
hx'x : f x = x'
⊢ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm (f x) ∈ e.source
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
⊢ e'.symm.trans e.symm.symm = e'.symm.trans e.toPartialEquiv

Tactic:
PartialEquiv.symm_symm

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
⊢ e'.symm.trans e.toPartialEquiv = e'.symm.trans e.toPartialEquiv
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e e' : Trivialization F proj
h : (fun e ↦ e.toPretrivialization) e = (fun e ↦ e.toPretrivialization) e'
⊢ e = e'

Tactic:
by
  ext1
  exacts [OpenPartialHomeomorph.toPartialEquiv_injective congr(Pretrivialization.toPartialEquiv $h),
    congr(Pretrivialization.baseSet $h)]

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
G : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G E
hf : IsQuotientCoveringMap f G
x : X
this : MulAction G ↑(f ⁻¹' {x}) := hf.mulActionFiber x
e e' : ↑(f ⁻¹' {x})
⊢ ∃ g, g • e = e'

Tactic:
obtain ⟨g, hg⟩ := hf.apply_eq_iff_mem_orbit.mp (e'.2.trans e.2.symm)

Goal state after:
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 : IsQuotientCoveringMap f G
x : X
this : MulAction G ↑(f ⁻¹' {x}) := hf.mulActionFiber x
e e' : ↑(f ⁻¹' {x})
g : G
hg : (fun m ↦ m • ↑e) g = ↑e'
⊢ ∃ g, g • e = e'
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
h : IsQuotientCoveringMap f G
this : ContinuousConstSMul G E
e : E
U : Set E
hU : U ∈ 𝓝 e
hGU : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
g : G
hg : ((fun x ↦ g • x) '' U ∩ U).Nonempty
⊢ g • e = e

Tactic:
rw [hGU g hg, one_smul]

Goal state after:
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
⊢ cfc exp a = exp a

Tactic:
conv_rhs => rw [← cfc_id 𝕜 a ha, cfc_apply id a ha]
  have h := cfcHom_continuous (R := 𝕜) ha
  have _ : ContinuousOn exp (spectrum 𝕜 a) := exp_continuous.continuousOn
  let +nondep : Algebra ℚ A := .restrictScalars ℚ 𝕜 A
  simp_rw [← map_exp _ h, cfc_apply exp a ha]
  congr 1
  ext
  simp [exp_continuousMap_eq]

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

Goal state before:
pp: r : ℝ
hr : r ≤ π
⊢ BijOn (⇑exp) (Ioo (-r) r) (centeredArc r)

Tactic:
simp_rw [centeredArc, abs_lt, Set.Ioo_def]

Goal state after:
r : ℝ
hr : r ≤ π
⊢ BijOn (⇑exp) (Ioo (-r) r) (⇑exp '' Ioo (-r) r)
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h✝ : Nontrivial A
h_eqOn : Set.EqOn (fun z ↦ ‖z - 1‖ ^ 2) (fun z ↦ 2 * (1 - z.re)) (spectrum ℂ u)
h₂ : IsGreatest ((fun z ↦ 2 * (1 - z.re)) '' spectrum ℂ u) (2 * (1 - x))
⊢ IsGreatest ((fun x ↦ ‖x - 1‖ ^ 2) '' spectrum ℂ u) (‖cfc (fun x ↦ x - 1) u‖ ^ 2)

Tactic:
have := pow_left_monotoneOn (n := 2) |>.mono (s₂ := ((‖· - 1‖) '' spectrum ℂ u)) (by simp)

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h✝ : Nontrivial A
h_eqOn : Set.EqOn (fun z ↦ ‖z - 1‖ ^ 2) (fun z ↦ 2 * (1 - z.re)) (spectrum ℂ u)
h₂ : IsGreatest ((fun z ↦ 2 * (1 - z.re)) '' spectrum ℂ u) (2 * (1 - x))
this : MonotoneOn (fun a ↦ a ^ 2) ((fun x ↦ ‖x - 1‖) '' spectrum ℂ u)
⊢ IsGreatest ((fun x ↦ ‖x - 1‖ ^ 2) '' spectrum ℂ u) (‖cfc (fun x ↦ x - 1) u‖ ^ 2)
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ a + I • cfc Real.sqrt (1 - a ^ 2) = a + I • cfc (fun x ↦ √x) (cfc (fun x ↦ 1 - x ^ 2) a)

Tactic:
cfc_sub ..,

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ a + I • cfc Real.sqrt (1 - a ^ 2) = a + I • cfc (fun x ↦ √x) (cfc (fun x ↦ 1) a - cfc (fun x ↦ x ^ 2) a)
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ‖A x‖ ^ 2 = re ⟪x, (adjoint A ∘SL A) x⟫_𝕜

Tactic:
by
  have h : ⟪x, (A† ∘L A) x⟫ = ⟪A x, A x⟫ := by rw [← adjoint_inner_right]; rfl
  rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]

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‖ < δ
t : ↑unitInterval
⊢ (path 1 u ⋯) t ∈ ball 1 δ

Tactic:
simpa [Subtype.dist_eq, dist_eq_norm] using
    norm_expUnitary_smul_argSelfAdjoint_sub_one_le u t.2 (hu.trans hδ₂) |>.trans_lt hu

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] F
⊢ (↑(adjoint T ∘SL T)).ker = (↑T).ker

Tactic:
by
  refine le_antisymm (fun _ _ ↦ ?_) fun _ _ ↦ by simp_all
  rw [LinearMap.mem_ker, ← inner_self_eq_zero (𝕜 := 𝕜), coe_coe, ← adjoint_inner_left]
  simp_all

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
A : E →L[𝕜] E
hA : (↑A).IsSymmetric
⊢ IsSelfAdjoint A

Tactic:
← ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
A : E →L[𝕜] E
hA : IsSelfAdjoint A
⊢ IsSelfAdjoint A
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
this : (↑(adjoint T * T) - ↑(T * adjoint T)).IsSymmetric
⊢ (∀ (x : E), ↑‖T x‖ ^ 2 - ⟪T ((adjoint T) x), x⟫_𝕜 = 0) ↔ ∀ (v : E), ‖T v‖ = ‖(adjoint T) v‖

Tactic:
← adjoint_inner_right T,

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
this : (↑(adjoint T * T) - ↑(T * adjoint T)).IsSymmetric
⊢ (∀ (x : E), ↑‖T x‖ ^ 2 - ⟪(adjoint T) x, (adjoint T) x⟫_𝕜 = 0) ↔ ∀ (v : E), ‖T v‖ = ‖(adjoint T) v‖
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
⊢ T - T * T = 0 ↔ IsIdempotentElem T

Tactic:
by simp only [sub_eq_zero, IsIdempotentElem, eq_comm]

Goal state after: