mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Algebra.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : NormedField L
inst✝ : NormedAlgebra K L
F : IntermediateField K L
k : K
hk : 1 < ‖k‖
⊢ ∃ x, 1 < ‖x‖

Tactic:
use algebraMap K F k

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : NormedField L
inst✝ : NormedAlgebra K L
F : IntermediateField K L
k : K
hk : 1 < ‖k‖
⊢ 1 < ‖(algebraMap K ↥F) k‖
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hU : s = ⋂ n, U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
n : ℕ
⊢ Disjoint s (U n ∩ interior m)ᶜ

Tactic:
disjoint_compl_right_iff_subset

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hU : s = ⋂ n, U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
n : ℕ
⊢ s ⊆ U n ∩ interior m
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
⊢ z ∈ Set.range ⇑((gelfandTransform ℂ A) a) ↔ ∃ f, f a = z

Tactic:
exact Iff.rfl

Goal state after:
Module: Mathlib.Order.CompleteLattice.Group

Goal state before:
pp: α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝³ : CompleteLattice α
inst✝² : Mul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
u v : (i : ι) → κ i → α
⊢ ⨆ i, ⨆ j, u i j * v i j ≤ (⨆ i, ⨆ j, u i j) * ⨆ i, ⨆ j, v i j

Tactic:
refine le_trans ?_ (iSup_mul_le ..)
  gcongr
  exact iSup_mul_le ..

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

Goal state before:
pp: case add
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a x y : A
x_mem : x ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
y_mem : y ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hx : ∀ x_1 ∈ spectrum ℝ x, 0 ≤ x_1
hy : ∀ x ∈ spectrum ℝ y, 0 ≤ x
⊢ ∀ x_1 ∈ spectrum ℝ (x + y), 0 ≤ x_1

Tactic:
rw [← SpectrumRestricts.nnreal_iff] at hx hy ⊢

Goal state after:
case add
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a x y : A
x_mem : x ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
y_mem : y ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hx : SpectrumRestricts x ⇑ContinuousMap.realToNNReal
hy : SpectrumRestricts y ⇑ContinuousMap.realToNNReal
⊢ SpectrumRestricts (x + y) ⇑ContinuousMap.realToNNReal
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric

Goal state before:
pp: A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
r : ℝ≥0
hr : 0 < ↑r
⊢ 0 < r

pp: A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
r : ℝ≥0
hr : 0 < ↑r
⊢ 0 < r

Tactic:
all_goals simpa

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
⊢ cfcₙ (fun z ↦ id z * (id z * id z)) a = a * a * a

Tactic:
cfcₙ_mul id _ a,

Goal state after:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
⊢ cfcₙ id a * cfcₙ (fun z ↦ id z * id z) a = a * a * a
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
⊢ cfcₙ id a * cfcₙ (fun z ↦ id z * id z) a = a * a * a

Tactic:
cfcₙ_mul id _ a,

Goal state after:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
⊢ cfcₙ id a * (cfcₙ id a * cfcₙ id a) = a * a * a
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
y : ℝ
f : ℝ → ℝ
hf₁ : ∀ x ∈ spectrum ℝ a, 0 < f x
hf₂ : ContinuousOn f (spectrum ℝ a)
ha : IsSelfAdjoint a
⊢ cfc f a ^ y = cfc (fun r ↦ f r ^ y) a

Tactic:
have hg : ContinuousOn (fun r => r ^ y) (f '' spectrum ℝ a) :=
    ContinuousOn.rpow_const (f := id) (by fun_prop) (by grind)
  rw [CFC.rpow_eq_cfc_real (by grind [cfc_nonneg]), ← cfc_comp _ _ a ha]
  rfl

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
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConvexOn ℝ s (inr ∘ f)
x : A
hx : x ∈ s
y : A
⊢ y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
hy

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConvexOn ℝ s (inr ∘ f)
x : A
hx : x ∈ s
y : A
hy : y ∈ s
⊢ ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConcaveOn ℝ s (inr ∘ f)
x : A
hx : x ∈ s
y : A
⊢ y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)

Tactic:
hy

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConcaveOn ℝ s (inr ∘ f)
x : A
hx : x ∈ s
y : A
hy : y ∈ s
⊢ ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:
pp: A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul A (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
x✝ : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
⊢ ⟪x i, x i⟫_A ≤ ∑ i, ⟪x i, x i⟫_A

Tactic:
exact Finset.single_le_sum (fun j _ ↦ inner_self_nonneg (A := A) (x := x j)) (Finset.mem_univ i)

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

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.univ.sup fun i ↦ (∑ i_1, ‖A i i_1‖₊) * Finset.univ.sup fun i ↦ ∑ j, ‖B i j‖₊) ≤
    (Finset.univ.sup fun i ↦ ∑ j, ‖A i j‖₊) * Finset.univ.sup fun i ↦ ∑ j, ‖B i j‖₊

Tactic:
← NNReal.finset_sup_mul

Goal state after:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ ((Finset.univ.sup fun a ↦ ∑ i, ‖A a i‖₊) * Finset.univ.sup fun i ↦ ∑ j, ‖B i j‖₊) ≤
    (Finset.univ.sup fun i ↦ ∑ j, ‖A i j‖₊) * Finset.univ.sup fun i ↦ ∑ j, ‖B i j‖₊
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
| ‖f x‖

Tactic:
hy

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
| ‖f (∑ i, I ^ ↑i • y i)‖
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁷ : Fintype n
inst✝⁶ : Semiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : Module R A
inst✝³ : Star A
inst✝² : NonUnitalNonAssocSemiring B
inst✝¹ : Module R B
inst✝ : Star B
f : A →⋆ₙₐ[R] B
⊢ (mapₗ ↑f) 0 = 0

Tactic:
by simp [map_zero]

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

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

Tactic:
rw [← continuousOn_univ] at ha_cont ⊢
  exact ha_cont.cfcₙ_nnreal_of_mem_nhdsSet f (by simpa) (by simpa)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f : R → R
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ Set.EqOn (fun x ↦ star (f x) * f x) 1 (spectrum R a) ↔ ∀ x ∈ spectrum R a, star (f x) * f x = 1

Tactic:
exact Iff.rfl

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

Goal state before:
pp: case refine_1.e_a
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
x : X
hx : x ∈ s
y : X
⊢ y ∈ e.source → ↑e x = ↑e y → x = y

Tactic:
hy

Goal state after:
case refine_1.e_a
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
x : X
hx : x ∈ s
y : X
hy : y ∈ e.source
⊢ ↑e x = ↑e y → x = y
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
⊢ y ∈ (e.subtypeRestr hU).target → ↑(e.subtypeRestr hV).symm y = (i ∘ ↑(e.subtypeRestr hU).symm) y

Tactic:
hy

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ ↑(e.subtypeRestr hV).symm y = (i ∘ ↑(e.subtypeRestr hU).symm) y
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) x ∈ e.target

Tactic:
← hxx₀,

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
⊢ extend f (↑e) (fun x ↦ Classical.arbitrary Z) (f x₀) ∈ e.target
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) x) = x

Tactic:
← hxx₀,

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) (extend f (↑e) (fun x ↦ Classical.arbitrary Z) (f 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
⊢ F x = (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) x

Tactic:
← hxx₀,

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
⊢ F (f x₀) = (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f x₀)
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: case inr
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✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
⊢ ∃ e, Icc a b ⊆ e.baseSet

Tactic:
have ha : a ∈ s := ⟨left_mem_Icc.2 hab, ea, by simp [hea]⟩

Goal state after:
case inr
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✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
⊢ ∃ e, Icc a b ⊆ e.baseSet
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
h₁ : e.toPartialEquiv = e'.toPartialEquiv
h₂ : e.baseSet = e'.baseSet
⊢ e = e'

Tactic:
cases e; cases e'; congr

Goal state after:
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 : Pretrivialization F proj
x : Z
ex : x ∈ e.source
⊢ ↑e.symm ((↑e.toPartialEquiv x).1, (↑e.toPartialEquiv x).2) = x

Tactic:
e.left_inv ex

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 : Pretrivialization F proj
x : Z
ex : x ∈ e.source
⊢ x = x
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 : Pretrivialization F proj
⊢ ↑e.symm ⁻¹' proj ⁻¹' e.baseSet ∩ e.target = e.target

Tactic:
by
  refine inter_eq_right.mpr fun x hx => ?_
  simp only [mem_preimage, e.proj_symm_apply hx]
  exact e.mem_target.mp hx

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

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
b : B
⊢ b ∈ (Z.localTrivAt b).baseSet

Tactic:
rw [localTrivAt, ← baseSet_at]
  exact Z.mem_baseSet_at b

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
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 : B × F
⊢ Z

Tactic:
by classical exact if h : x.1 ∈ s then e.invFun (⟨x.1, h⟩, x.2)
    else Classical.arbitrary (B → F → Z) x.1 x.2

Goal state after:
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₁ : e.toOpenPartialHomeomorph = e'.toOpenPartialHomeomorph
h₂ : e.baseSet = e'.baseSet
⊢ e = e'

Tactic:
cases e; cases e'; congr

Goal state after:
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U
x : X
⊢ ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ Set.InjOn f U

Tactic:
· obtain ⟨U, hn, hi⟩ := h x
    exact ⟨interior U, isOpen_interior, mem_interior_iff_mem_nhds.mpr hn, hi.mono interior_subset⟩

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

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

Tactic:
by
  refine ⟨fun _ ↦ h.discreteTopology_of_image, ?_⟩
  simp_rw [discreteTopology_iff_isOpen_singleton]
  rintro hX ⟨_, x, hx, rfl⟩
  obtain ⟨e, hxe, rfl⟩ := h x hx
  refine ⟨e '' {x}, e.isOpen_image_of_subset_source ?_ (Set.singleton_subset_iff.mpr hxe), ?_⟩
  · simpa using hs.isOpenMap_subtype_val _ (hX ⟨x, hx⟩)
  · ext; simp [Subtype.ext_iff]

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : ↑g ∘ f = ↑gf
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
⊢ f y = ↑g.symm (↑gf y)

Tactic:
have : f y ∈ g.source := by apply interior_subset hy.1.2

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : ↑g ∘ f = ↑gf
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
this : f y ∈ g.source
⊢ f y = ↑g.symm (↑gf y)
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
h1 : ∀ (b : A), ‖a.toProd.1 b‖₊ ^ 2 ≤ ‖a.toProd.2‖₊ * ‖a.toProd.1 b‖₊ * ‖b‖₊
h2 : ∀ (b : A), ‖a.toProd.2 b‖₊ ^ 2 ≤ ‖a.toProd.1‖₊ * ‖a.toProd.2 b‖₊ * ‖b‖₊
⊢ ‖a.toProd.1‖ = ‖a.toProd.2‖

Tactic:
exact le_antisymm (h0 _ _ h1) (h0 _ _ h2)

Goal state after: