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

Goal state before:
pp: case refine_3
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
v : E
instNACG : NormedAddCommGroup E := NormedAddCommGroup.ofCore ⋯
instNS : NormedSpace ℂ E := NormedSpace.ofCore ⋯
⊢ ‖v‖ ∈ upperBounds {x | ∃ w, ∃ (_ : ‖w‖ ≤ 1), ‖⟪w, v⟫_A‖ = x}

Tactic:
rintro - ⟨w, hw, rfl⟩
    calc _ ≤ ‖w‖ * ‖v‖ := norm_inner_le E
      _ ≤ 1 * ‖v‖ := by gcongr
      _ = ‖v‖ := by simp

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 < ↑ε
⊢ ∃ ia, (0 ≤ ia ∧ ‖ia‖ < 1) ∧ ∀ x ∈ {x | ia ≤ x} ∩ closedBall 0 1, x * m ∈ closedBall m ↑ε

Tactic:
coe_pos

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 < ε
⊢ ∃ ia, (0 ≤ ia ∧ ‖ia‖ < 1) ∧ ∀ x ∈ {x | ia ≤ x} ∩ closedBall 0 1, x * m ∈ closedBall m ↑ε
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap

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
f : X → Y → E
g : C(Y, E)
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
⊢ ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖(mkD (f x) g) y‖ ≤ bound x

Tactic:
filter_upwards [bound_ge, f_ae_cont] with x bound_ge_x cont_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
f : X → Y → E
g : C(Y, E)
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
x : X
bound_ge_x : ∀ (y : Y), ‖f x y‖ ≤ bound x
cont_x : Continuous (f x)
⊢ ∀ (y : Y), ‖(mkD (f x) g) y‖ ≤ bound x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

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

Tactic:
exact hf.smul_left r

Goal state after:
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 m
inst✝¹ : NonUnitalCStarAlgebra A
inst✝ : Fintype n
⊢ ∀ (x y : CStarMatrix n n A),
    (↑(MulOpposite.opLinearEquiv ℂ) ∘ₗ toCLM).toFun (x * y) =
      (↑(MulOpposite.opLinearEquiv ℂ) ∘ₗ toCLM).toFun x * (↑(MulOpposite.opLinearEquiv ℂ) ∘ₗ toCLM).toFun y

Tactic:
by
      intros
      simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.coe_comp,
        LinearEquiv.coe_coe, MulOpposite.coe_opLinearEquiv, Function.comp_apply,
        ← MulOpposite.op_mul, MulOpposite.op_inj]
      ext
      simp [toCLM]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_5
inst✝¹ : Fintype m
inst✝ : NonUnitalCStarAlgebra A
M : CStarMatrix m n A
⊢ toCLM M = 0 → M = 0

Tactic:
h

Goal state after:
m : Type u_1
n : Type u_2
A : Type u_5
inst✝¹ : Fintype m
inst✝ : NonUnitalCStarAlgebra A
M : CStarMatrix m n A
h : toCLM M = 0
⊢ M = 0
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ LipschitzWith 1 ⇑ofMatrixₗ.symm

Tactic:
by
  refine AddMonoidHomClass.lipschitz_of_bound_nnnorm _ _ fun M => ?_
  rw [one_mul, ← NNReal.coe_le_coe, coe_nnnorm, coe_nnnorm, Matrix.norm_le_iff (norm_nonneg _)]
  exact fun _ _ ↦ CStarMatrix.norm_entry_le_norm

Goal state after:
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✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ (Set.range fun x ↦ cfcₙ x a) = (fun x ↦ cfcₙ x a) '' {f | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x}

Tactic:
ext
  constructor
  · rintro ⟨f, rfl⟩
    simp only [cfcₙ_nnreal_eq_real f a]
    exact ⟨_, fun _ _ ↦ by positivity, rfl⟩
  · rintro ⟨f, hf, rfl⟩
    simp only [cfcₙ_real_eq_nnreal a hf]
    exact ⟨_, rfl⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
L : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : IsOrderedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : EquivLike L E F
inst✝ : LinearEquivClass L 𝕜 E F
f : L
s : Set E
a : E
this : ∀ (x y : E), ⇑f '' openSegment 𝕜 x y = openSegment 𝕜 (f x) (f y)
⊢ f a ∈ ⇑f '' extremePoints 𝕜 s ↔ f a ∈ extremePoints 𝕜 (⇑f '' s)

Tactic:
simp only [mem_extremePoints, (EquivLike.surjective f).forall,
    (EquivLike.injective f).mem_set_image, (EquivLike.injective f).eq_iff, ← this]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a : A
x : f.PreGNS
⊢ ‖(↑f.toPreGNS ∘ₗ ↑((ContinuousLinearMap.mul ℂ A) a) ∘ₗ ↑f.ofPreGNS) x‖ ^ 2 ≤ (‖a‖ * ‖x‖) ^ 2

Tactic:
mul_pow,

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a : A
x : f.PreGNS
⊢ ‖(↑f.toPreGNS ∘ₗ ↑((ContinuousLinearMap.mul ℂ A) a) ∘ₗ ↑f.ofPreGNS) x‖ ^ 2 ≤ ‖a‖ ^ 2 * ‖x‖ ^ 2
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: z : Circle
⊢ (starRingEnd ℂ) ↑z * ↑1⁻¹ = (starRingEnd ℂ) ↑z

Tactic:
inv_one,

Goal state after:
z : Circle
⊢ (starRingEnd ℂ) ↑z * ↑1 = (starRingEnd ℂ) ↑z
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)
x : EuclideanSpace 𝕜 n
i : n
x✝ : i ∈ Finset.univ
⊢ (‖v i‖ * ‖x.ofLp i‖) ^ 2 ≤ ?m.78 i

Tactic:
mul_pow,

Goal state after:
𝕜 : 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)
x : EuclideanSpace 𝕜 n
i : n
x✝ : i ∈ Finset.univ
⊢ ‖v i‖ ^ 2 * ‖x.ofLp i‖ ^ 2 ≤ ?m.78 i
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)
x : EuclideanSpace 𝕜 n
⊢ ∑ i, ‖v‖ ^ 2 * ‖x.ofLp i‖ ^ 2 = (‖v‖ * ‖x‖) ^ 2

Tactic:
by simp [mul_pow, EuclideanSpace.norm_sq_eq x, Finset.mul_sum]

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
hy : y ∈ e.source
⊢ ↑e x = ↑e y → x = y

Tactic:
h

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
h : ↑e x = ↑e y
⊢ x = y
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
hy : y ∈ e.source
h : ↑e x = ↑e y
⊢ ↑e.symm (↑e x) = ↑e.symm (↑e y)

Tactic:
h

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
h : ↑e x = ↑e y
⊢ ↑e.symm (↑e y) = ↑e.symm (↑e y)
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
p : B × F
hp : p ∈ (Z.baseSet i ∩ Z.baseSet j) ×ˢ univ
⊢ (p.1, Z.coordChange i j p.1 p.2) ∈ (Z.baseSet i ∩ Z.baseSet j) ×ˢ univ

Tactic:
simpa using hp

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

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
p : B × F
hp : p ∈ (Z.baseSet i ∩ Z.baseSet j) ×ˢ univ
⊢ (p.1, Z.coordChange j i p.1 p.2) ∈ (Z.baseSet i ∩ Z.baseSet j) ×ˢ univ

Tactic:
simpa using hp

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

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
Z' : Type u_5
inst✝ : TopologicalSpace Z'
h : Z' ≃ₜ Z
p : Z'
hp : p ∈ (h.transOpenPartialHomeomorph e.toOpenPartialHomeomorph).source
⊢ h p ∈ e.source

Tactic:
simpa using hp

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

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst✝³] s
hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
⊢ ContinuousWithinAt f (TotalSpace.proj ⁻¹' s) z

Tactic:
let e : Trivialization F (π F E) :=
    a.trivializationOfMemPretrivializationAtlas (a.pretrivialization_mem_atlas z.proj)

Goal state after:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst✝³] s
hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯
⊢ ContinuousWithinAt f (TotalSpace.proj ⁻¹' s) z
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case refine_3
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
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ ∀ (x : F), ↑e₁.symm (b, x) ∈ e₂.source

Tactic:
· intro x
    rwa [e₂.mem_source, e₁.proj_symm_apply' h₁]

Goal state after:
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: case refine_2
X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
x₁ x₂ : X
x✝² : f x₁ = f x₂
x✝¹ : x₁ ≠ x₂
x✝ : (Function.pullbackDiagonal f)ᶜ ∈ comap Subtype.val (𝓝 x₁ ×ˢ 𝓝 x₂)
t : Set (X × X)
ht : t ∈ 𝓝 x₁ ×ˢ 𝓝 x₂
t_sub : Subtype.val ⁻¹' t ⊆ (Function.pullbackDiagonal f)ᶜ
⊢ ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂

Tactic:
obtain ⟨s₁, h₁, s₂, h₂, s_sub⟩ := mem_prod_iff.mp ht

Goal state after:
case refine_2
X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
x₁ x₂ : X
x✝² : f x₁ = f x₂
x✝¹ : x₁ ≠ x₂
x✝ : (Function.pullbackDiagonal f)ᶜ ∈ comap Subtype.val (𝓝 x₁ ×ˢ 𝓝 x₂)
t : Set (X × X)
ht : t ∈ 𝓝 x₁ ×ˢ 𝓝 x₂
t_sub : Subtype.val ⁻¹' t ⊆ (Function.pullbackDiagonal f)ᶜ
s₁ : Set X
h₁ : s₁ ∈ 𝓝 x₁
s₂ : Set X
h₂ : s₂ ∈ 𝓝 x₂
s_sub : s₁ ×ˢ s₂ ⊆ t
⊢ ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
x : ↑s
e : OpenPartialHomeomorph X Y
hx : ↑x ∈ e.source
h : IsLocalHomeomorphOn (↑e) s
inst✝ : DiscreteTopology ↑(↑e '' s)
U : Set Y
hU : IsOpen[inst✝¹] U
eq : Subtype.val ⁻¹' U = {⟨↑e ↑x, ⋯⟩}
⊢ {x} ⊆ Subtype.val ⁻¹' (e.source ∩ ↑e ⁻¹' U)

Tactic:
rintro x rfl; exact ⟨hx, eq.superset rfl⟩

Goal state after:
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)
f : A →L[𝕜] A
C : ℝ≥0
⊢ (∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C

Tactic:
h

Goal state after:
𝕜 : 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)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊
⊢ ‖f‖₊ ≤ C
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
g : Y → Z
f : X → Y
s : Set X
t : Set Y
hg : IsLocalHomeomorphOn g t
hf : IsLocalHomeomorphOn f s
h : Set.MapsTo f s t
⊢ IsLocalHomeomorphOn (g ∘ f) s

Tactic:
by
  intro x hx
  obtain ⟨eg, hxg, rfl⟩ := hg (f x) (h hx)
  obtain ⟨ef, hxf, rfl⟩ := hf x hx
  exact ⟨ef.trans eg, ⟨hxf, hxg⟩, rfl⟩

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
hf : IsLocalHomeomorph f
x : X
⊢ f x ∈ (hf.localInverseAt x).source

Tactic:
← congrFun (hf.localInverseAt_symm x)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
⊢ ↑(hf.localInverseAt x).symm x ∈ (hf.localInverseAt x).source
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
hf : IsLocalHomeomorph f
x : X
y : Y
hx : y ∈ (hf.localInverseAt x).source
⊢ f (↑(hf.localInverseAt x) y) = y

Tactic:
← congrFun (hf.localInverseAt_symm x)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
y : Y
hx : y ∈ (hf.localInverseAt x).source
⊢ ↑(hf.localInverseAt x).symm (↑(hf.localInverseAt x) y) = y
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 : IsQuotientMap f
inst✝ : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this✝ : TopologicalSpace G := ⊥
this : DiscreteTopology G
e : E
he : e ∈ {e | MulAction.stabilizer G e = ⊥}
U : Set E
heU : U ∈ 𝓝 e
hU : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
g : G
hg : ((fun x ↦ g • x) '' interior U ∩ interior U).Nonempty
⊢ g ∈ MulAction.stabilizer G e

Tactic:
exact hU _ (hg.mono (by grw [interior_subset]))

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

Goal state before:
pp: s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
⊢ exp t₁ = exp t₂ → t₁ = t₂

Tactic:
heq

Goal state after:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
heq : exp t₁ = exp t₂
⊢ t₁ = t₂
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

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

Tactic:
have h : Disjoint ((x.path y) '' Ioo 0 1) ((y.path x) '' Ioo 0 1) := by
    refine (disjoint_path_image_Ioc h).mono ?_ ?_ <;> exact image_mono Ioo_subset_Ioc_self

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

Goal state before:
pp: case h.h
x✝¹ x✝ : ℝ
⊢ (↑x✝¹ + ↑x✝).toCircle = (↑x✝¹).toCircle * (↑x✝).toCircle

Tactic:
exact Circle.exp_add _ _

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

Goal state before:
pp: case h
x✝ : ℝ
⊢ ↑(↑(Real.cos x✝) + Complex.sin ↑x✝ * I).arg = ↑x✝

Tactic:
← ofReal_sin,

Goal state after:
case h
x✝ : ℝ
⊢ ↑(↑(Real.cos x✝) + ↑(Real.sin x✝) * I).arg = ↑x✝
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: case refine_2
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
a✝ : Nontrivial A
⊢ Real.cos ‖x‖ ∈ lowerBounds ((fun a ↦ Real.cos a) '' spectrum ℝ ↑x)

Tactic:
rintro - ⟨y, hy, rfl⟩
    exact Real.cos_abs y ▸ Real.cos_le_cos_of_nonneg_of_le_pi (by positivity) hx <|
      spectrum.norm_le_norm_of_mem hy

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

Goal state before:
pp: T : ℝ
hT : T ≠ 0
a b : AddCircle T
⊢ a.toCircle = b.toCircle → a = b

Tactic:
h

Goal state after:
T : ℝ
hT : T ≠ 0
a b : AddCircle T
h : a.toCircle = b.toCircle
⊢ a = b
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
⊢ Real.arccos (1 - ‖↑u - 1‖ ^ 2 / 2) < Real.arccos (1 - 2 ^ 2 / 2)

Tactic:
apply Real.arccos_lt_arccos (by norm_num) (by gcongr)

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
⊢ 1 - ‖↑u - 1‖ ^ 2 / 2 ≤ 1
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 : IsSelfAdjoint T
⊢ Commute (star T) T

Tactic:
h

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
hT : IsIdempotentElem T
h : IsSelfAdjoint T
⊢ Commute T T
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
⊢ adjoint (adjoint A) = A

Tactic:
ext v
  refine ext_inner_left 𝕜 fun w => ?_
  rw [adjoint_inner_right, adjoint_inner_left]

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✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ (A ∘ₗ adjoint A).ker = (adjoint A).ker

Tactic:
by
  simpa using A.adjoint.ker_adjoint_comp_self

Goal state after:
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
⊢ (∃ y, y • 1 = ↑(↑g).symm ∘SL ↑↑f) ↔ ∃ α, ∀ (x : H), f x = (α • g) x

Tactic:
refine ⟨fun ⟨y, h⟩ ↦ ?_, fun ⟨y, h⟩ ↦ ⟨(y : 𝕜), by ext; simp [h]⟩⟩

Goal state after:
𝕜 : 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
⊢ ∃ α, ∀ (x : H), f x = (α • g) x
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 : Fin (n + 1)
h : s.centroid = (↑n * (1 / (↑n + 1))) • (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i
⊢ s.centroid ∈ line[k, s.points i, s.faceOppositeCentroid i]

Tactic:
h

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 : Fin (n + 1)
h : s.centroid = (↑n * (1 / (↑n + 1))) • (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i
⊢ (↑n * (1 / (↑n + 1))) • (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i ∈
    line[k, s.points i, s.faceOppositeCentroid i]
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
h : (↑n)⁻¹ • (s.centroid -ᵥ s.points i) = (-1 / ↑n) • (s.points i -ᵥ s.centroid)
⊢ (↑n)⁻¹ • (s.centroid -ᵥ s.points i) +ᵥ s.centroid ∈ line[k, s.points i, s.centroid]

Tactic:
h

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 : Fin (n + 1)
h : (↑n)⁻¹ • (s.centroid -ᵥ s.points i) = (-1 / ↑n) • (s.points i -ᵥ s.centroid)
⊢ (-1 / ↑n) • (s.points i -ᵥ s.centroid) +ᵥ s.centroid ∈ line[k, s.points i, s.centroid]
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
h_span : ∀ (i : ↥s'), p -ᵥ s.centroid ∈ k ∙ u i
hi : LinearIndependent k u
i j : ↥s'
hij : i ≠ j
h_ij : Disjoint {i} {j}
h_disjoint : Disjoint (k ∙ u i) (k ∙ u j)
⊢ p -ᵥ s.centroid = 0

Tactic:
exact Submodule.disjoint_def.1 h_disjoint _ (h_span i) (h_span j)

Goal state after: