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

Goal state before:
pp: case inl
m : Type u_1
n : Type u_2
A : Type u_5
inst✝⁴ : Fintype m
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype n
M : CStarMatrix m n A
i : m
j : n
this : ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
h : M i j = 0
⊢ ‖M i j‖ ≤ ‖M‖

pp: case inr
m : Type u_1
n : Type u_2
A : Type u_5
inst✝⁴ : Fintype m
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype n
M : CStarMatrix m n A
i : m
j : n
this : ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
h : 0 < ‖M i j‖
⊢ ‖M i j‖ ≤ ‖M‖

Tactic:
· simp [h, norm_def]

Goal state after:
case inr
m : Type u_1
n : Type u_2
A : Type u_5
inst✝⁴ : Fintype m
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype n
M : CStarMatrix m n A
i : m
j : n
this : ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
h : 0 < ‖M i j‖
⊢ ‖M i j‖ ≤ ‖M‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral

Goal state before:
pp: case refine_2
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : MeasurableSpace X
μ : Measure X
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace 𝕜 A
inst✝⁶ : IsScalarTower 𝕜 A A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝³ : CompleteSpace A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)
hf : ContinuousOn (uncurry f) (univ ×ˢ quasispectrum 𝕜 a)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
⊢ HasFiniteIntegral (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ

Tactic:
refine hasFiniteIntegral_mkD_restrict_of_bound f _ ?_ f_zero bound bound_int bound_ge

Goal state after:
case refine_2
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : MeasurableSpace X
μ : Measure X
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace 𝕜 A
inst✝⁶ : IsScalarTower 𝕜 A A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝³ : CompleteSpace A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)
hf : ContinuousOn (uncurry f) (univ ×ˢ quasispectrum 𝕜 a)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
⊢ ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral

Goal state before:
pp: case refine_2
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : MeasurableSpace X
μ : Measure X
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace 𝕜 A
inst✝⁶ : IsScalarTower 𝕜 A A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝³ : CompleteSpace A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)
hf : ContinuousOn (uncurry f) (s ×ˢ quasispectrum 𝕜 a)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound (μ.restrict s)
ha : p a
⊢ HasFiniteIntegral (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) (μ.restrict s)

Tactic:
refine hasFiniteIntegral_mkD_restrict_of_bound f _ ?_ f_zero bound bound_int bound_ge

Goal state after:
case refine_2
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : MeasurableSpace X
μ : Measure X
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace 𝕜 A
inst✝⁶ : IsScalarTower 𝕜 A A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝³ : CompleteSpace A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)
hf : ContinuousOn (uncurry f) (s ×ˢ quasispectrum 𝕜 a)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound (μ.restrict s)
ha : p a
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (quasispectrum 𝕜 a)
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
⊢ ∃ a, (toDualMap 𝕜 E) a = ℓ

Tactic:
by_cases htriv : Y = ⊤

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
htriv : Y = ⊤
⊢ ∃ a, (toDualMap 𝕜 E) a = ℓ

case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
htriv : ¬Y = ⊤
⊢ ∃ a, (toDualMap 𝕜 E) a = ℓ
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: case left_mem_of_mem_openSegment
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
hAB : IsExtreme 𝕜 A B
hAC : IsExtreme 𝕜 A C
⊢ ∀ ⦃x : E⦄, x ∈ A → ∀ ⦃y : E⦄, y ∈ A → ∀ ⦃z : E⦄, z ∈ B ∩ C → z ∈ openSegment 𝕜 x y → x ∈ B ∩ C

Tactic:
rintro x₁ hx₁A x₂ hx₂A x ⟨hxB, hxC⟩ hx

Goal state after:
case left_mem_of_mem_openSegment
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
hAB : IsExtreme 𝕜 A B
hAC : IsExtreme 𝕜 A C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxB : x ∈ B
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ B ∩ C
Module: Mathlib.Analysis.CStarAlgebra.Extreme

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
x✝ : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : ↑a ∈ Icc 0 1
hb01 : ↑b ∈ Icc 0 1
⊢ t • (↑e * (1 - ↑a) * ↑e) ≤ t • (↑e * (1 - ↑a) * ↑e) + s • (↑e * (1 - ↑b) * ↑e)

Tactic:
refine le_add_of_nonneg_right <| smul_nonneg h0s.le ?_
        simpa [mul_one_sub_mul] using he.inr.isSelfAdjoint.conjugate_le_conjugate <|
          norm_le_one_iff_of_nonneg (b : A⁺¹) (by simpa) |>.mp (by simpa [norm_inr])

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
i j : ι
p : B × F
⊢ p ∈ (Z.trivChange i j).source ↔ p.1 ∈ Z.baseSet i ∩ Z.baseSet j

Tactic:
rw [trivChange, mem_prod]

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
p : B × F
⊢ p.1 ∈ Z.baseSet i ∩ Z.baseSet j ∧ p.2 ∈ univ ↔ p.1 ∈ Z.baseSet i ∩ Z.baseSet j
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✝ : Z
h : x✝ ∈ e.source
⊢ (↑(↑e x✝).1, (↑e x✝).2).1 = (Subtype.val ∘ proj) x✝

Tactic:
simp [e.coe_fst h]

Goal state after:
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
⊢ (∀ (x : X), {x} ∈ 𝓝 x) ↔ IsLocallyInjective fun x ↦ y

Tactic:
isLocallyInjective_iff_nhds

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
⊢ (∀ (x : X), {x} ∈ 𝓝 x) ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn (fun x ↦ y) U
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
hf : IsLocallyInjective f
g : A → X
cont : Continuous[inst✝, inst✝¹] g
hg : Function.Injective g
⊢ IsLocallyInjective (f ∘ g)

Tactic:
rw [isLocallyInjective_iff_isOpen_diagonal] at hf ⊢

Goal state after:
X : Type u_1
Y : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
hf : IsOpen[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → X
cont : Continuous[inst✝, inst✝¹] g
hg : Function.Injective g
⊢ IsOpen[instTopologicalSpaceSubtype] (Function.pullbackDiagonal (f ∘ g))
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
⊢ 1 • e = e

Tactic:
one_smul

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
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
⊢ 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 :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left✝ : DiscreteTopology ↑(f ⁻¹' {f e})
U : Set X
heU : f e ∈ U
hU : IsOpen[inst✝²] U
hfU : IsOpen[inst✝³] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × ↑(f ⁻¹' {f e})
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
g : G
x : { x // x ∈ f ⁻¹' U }
hx : x ∈ Prod.snd ∘ ⇑H ⁻¹' {(H ⟨e, heU⟩).2}
y : { x // x ∈ f ⁻¹' U }
hy : y ∈ Prod.snd ∘ ⇑H ⁻¹' {(H ⟨e, heU⟩).2}
eq : ↑y = (fun x ↦ g • x) ↑x
this : IsCancelSMul G E
⊢ ↑y = 1 • ↑x

Tactic:
one_smul

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
h :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left✝ : DiscreteTopology ↑(f ⁻¹' {f e})
U : Set X
heU : f e ∈ U
hU : IsOpen[inst✝²] U
hfU : IsOpen[inst✝³] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × ↑(f ⁻¹' {f e})
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
g : G
x : { x // x ∈ f ⁻¹' U }
hx : x ∈ Prod.snd ∘ ⇑H ⁻¹' {(H ⟨e, heU⟩).2}
y : { x // x ∈ f ⁻¹' U }
hy : y ∈ Prod.snd ∘ ⇑H ⁻¹' {(H ⟨e, heU⟩).2}
eq : ↑y = (fun x ↦ g • x) ↑x
this : IsCancelSMul G E
⊢ ↑y = ↑x
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
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
heq : cexp (↑(t₁ - t₂) * I) = 1
⊢ (cexp (↑(t₁ - t₂) * I)).re = 1

Tactic:
Complex.ext_iff

Goal state after:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
heq : (cexp (↑(t₁ - t₂) * I)).re = re 1 ∧ (cexp (↑(t₁ - t₂) * I)).im = im 1
⊢ (cexp (↑(t₁ - t₂) * I)).re = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case left
a b : ℝ
h : b - a < 2 * π
x : ℝ
x✝¹ : x ∈ Icc a b
y : ℝ
x✝ : y ∈ Icc a b
hx1 : a ≤ x
hx2 : x ≤ b
hy1 : a ≤ y
hy2 : y ≤ b
⊢ -2 * π < x - y

Tactic:
linarith

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

Goal state before:
pp: case right
a b : ℝ
h : b - a < 2 * π
x : ℝ
x✝¹ : x ∈ Icc a b
y : ℝ
x✝ : y ∈ Icc a b
hx1 : a ≤ x
hx2 : x ≤ b
hy1 : a ≤ y
hy2 : y ≤ b
⊢ x - y < 2 * π

Tactic:
linarith

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

Goal state before:
pp: case left
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
x✝¹ : x ∈ Ico a b
y : ℝ
x✝ : y ∈ Ico a b
hx1 : a ≤ x
hx2 : x < b
hy1 : a ≤ y
hy2 : y < b
⊢ -2 * π < x - y

Tactic:
linarith

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

Goal state before:
pp: case right
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
x✝¹ : x ∈ Ico a b
y : ℝ
x✝ : y ∈ Ico a b
hx1 : a ≤ x
hx2 : x < b
hy1 : a ≤ y
hy2 : y < b
⊢ x - y < 2 * π

Tactic:
linarith

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

Goal state before:
pp: case left
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
x✝¹ : x ∈ Ioc a b
y : ℝ
x✝ : y ∈ Ioc a b
hx1 : a < x
hx2 : x ≤ b
hy1 : a < y
hy2 : y ≤ b
⊢ -2 * π < x - y

Tactic:
linarith

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

Goal state before:
pp: case right
a b : ℝ
h : b - a ≤ 2 * π
x : ℝ
x✝¹ : x ∈ Ioc a b
y : ℝ
x✝ : y ∈ Ioc a b
hx1 : a < x
hx2 : x ≤ b
hy1 : a < y
hy2 : y ≤ b
⊢ x - y < 2 * π

Tactic:
linarith

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

Goal state before:
pp: case refine_1
x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x).arg (x.angleDiff y + (↑x).arg)) (Ioc (↑y).arg (y.angleDiff x + (↑y).arg))
a : ℝ
ha : a ∈ Ioc (↑x).arg (x.angleDiff y + (↑x).arg)
b : ℝ
hb : b ∈ Ioc (↑y).arg (y.angleDiff x + (↑y).arg)
⊢ a ∈ Ioc (↑x).arg (x.angleDiff y + (↑x).arg) ∪ Ioc (↑y).arg (y.angleDiff x + (↑y).arg)

Tactic:
tauto

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

Goal state before:
pp: case refine_2
x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x).arg (x.angleDiff y + (↑x).arg)) (Ioc (↑y).arg (y.angleDiff x + (↑y).arg))
a : ℝ
ha : a ∈ Ioc (↑x).arg (x.angleDiff y + (↑x).arg)
b : ℝ
hb : b ∈ Ioc (↑y).arg (y.angleDiff x + (↑y).arg)
⊢ b ∈ Ioc (↑x).arg (x.angleDiff y + (↑x).arg) ∪ Ioc (↑y).arg (y.angleDiff x + (↑y).arg)

Tactic:
tauto

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

Goal state before:
pp: x y : Circle
hne : x ≠ y
⊢ 2⁻¹ ≤ 1

Tactic:
linarith

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

Goal state before:
pp: case h
x y : Circle
hne : x ≠ y
⊢ ↑⟨2⁻¹, ⋯⟩ < 1

Tactic:
linarith

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : 2 ^ 2 ≤ 2 * (1 - z.re)
⊢ z.re ≤ -1

Tactic:
linarith

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

Goal state before:
pp: case refine_4
x y : Circle
hxy : x ≠ y
⊢ ¬range ⇑(y.path x) = univ

Tactic:
exact (range_path_ssubset_univ y x).ne

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

Goal state before:
pp: case h
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : z✝ = z✝¹ + T * ↑m
⊢ ↑m * T = -z✝¹ + z✝

Tactic:
linarith

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
r : ℝ
hr : r < 0
x : V
⊢ 0 < -r

Tactic:
linarith

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

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
r : ℝ
x : V
h_pos : 0 < r
⊢ normalize (r • x) = ↑(SignType.sign r) • normalize x

Tactic:
simp [normalize_smul_of_pos, h_pos]

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
this : ContinuousOn arg (spectrum ℂ ↑u)
| ↑u

Tactic:
← cfc_id' ℂ (u : A)

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
this : ContinuousOn arg (spectrum ℂ ↑u)
| cfc (fun x ↦ x) ↑u
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
hx : x ≠ 0
u₁ : ↥(unitary A) := selfAdjoint.unitarySelfAddISMul (ℜ (‖x‖⁻¹ • x)) ⋯
u₂ : ↥(unitary A) := selfAdjoint.unitarySelfAddISMul (ℑ (‖x‖⁻¹ • x)) ⋯
⊢ x = ‖x‖ • (2⁻¹ • (↑u₁ + ↑(star u₁)) + 2⁻¹ • I • (↑u₂ + ↑(star u₂)))

Tactic:
smul_comm _ I,

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
hx : x ≠ 0
u₁ : ↥(unitary A) := selfAdjoint.unitarySelfAddISMul (ℜ (‖x‖⁻¹ • x)) ⋯
u₂ : ↥(unitary A) := selfAdjoint.unitarySelfAddISMul (ℑ (‖x‖⁻¹ • x)) ⋯
⊢ x = ‖x‖ • (2⁻¹ • (↑u₁ + ↑(star u₁)) + I • 2⁻¹ • (↑u₂ + ↑(star u₂)))
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : dist u 1 ^ 2 < ε
hε : 0 < ε
huε' : dist u 1 < √ε
hε2 : ε < 4
⊢ ε < 4

Tactic:
exact hε2

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
this : -1 < Real.cos ‖↑x‖
⊢ 2 - 2 * Real.cos ‖↑x‖ < 2 * 2

Tactic:
linarith

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

Goal state before:
pp: case a
𝕜 : 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
x : E
hx : x ∈ (↑T).ker
⊢ x ∈ (↑(adjoint T)).rangeᗮ

Tactic:
rintro _ ⟨y, rfl⟩
    simp_all [T.adjoint_inner_left]

Goal state after:
Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone

Goal state before:
pp: f g : ℝ → ℝ
s : Set ℝ
hf : AbsolutelyMonotoneOn f s
hg : AbsolutelyMonotoneOn g s
⊢ AbsolutelyMonotoneOn (f + g) s

Tactic:
by
  obtain ⟨p, hp, hp_nn⟩ := hf
  obtain ⟨q, hq, hq_nn⟩ := hg
  refine ⟨p + q, hp.add hq, fun n x hx => ?_⟩
  simp only [Pi.add_apply, FormalMultilinearSeries.add_apply, add_apply]
  exact add_nonneg (hp_nn n hx) (hq_nn n hx)

Goal state after:
Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone

Goal state before:
pp: f : ℝ → ℝ
s : Set ℝ
c : ℝ
hf : AbsolutelyMonotoneOn f s
hc : 0 ≤ c
⊢ AbsolutelyMonotoneOn (c • f) s

Tactic:
by
  obtain ⟨p, hp, hp_nn⟩ := hf
  -- Witness: post-composition by the CLM `y ↦ c * y`.
  set T : ℝ →L[ℝ] ℝ := c • ContinuousLinearMap.id ℝ ℝ with hT
  have hcomp : (T ∘ f) = c • f := by ext x; simp [hT, smul_eq_mul]
  refine ⟨_, hcomp ▸ hp.continuousLinearMap_comp T, fun n x hx => ?_⟩
  simp only [ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply, hT,
    smul_apply, ContinuousLinearMap.id_apply, smul_eq_mul]
  exact mul_nonneg hc (hp_nn n hx)

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
S : E →L[𝕜] E
hS : IsStarProjection S
hT : IsStarProjection T
⊢ S = T ↔ (↑S).range = (↑T).range

Tactic:
simpa using hS.isSymmetricProjection.ext_iff hT.isSymmetricProjection

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ 1 • ∑ x, (s.points x -ᵥ s.points i) = ∑ x, (s.points x -ᵥ s.points i)

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✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ ↑n + 1 ≠ 0

Tactic:
one_smul

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✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ ∑ x, (s.points x -ᵥ s.points i) = ∑ x, (s.points x -ᵥ s.points i)

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✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ ↑n + 1 ≠ 0
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i j : Fin (n + 1)
h1 : ∀ (i : Fin (n + 1)), ∑ x, (s.points x -ᵥ s.points i) = ∑ x, (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0))
this✝ : s.points i -ᵥ s.points j = -(s.points j -ᵥ s.points i)
this : (↑n)⁻¹ • n • (s.points j -ᵥ s.points i) = (↑n)⁻¹ • ↑n • (s.points j -ᵥ s.points i)
⊢ (1 / ↑n) • (s.points j -ᵥ s.points i) + 1 • (s.points j -ᵥ s.points i) =
    (1 / ↑n) • (s.points j -ᵥ s.points i) + (s.points j -ᵥ s.points i)

Tactic:
one_smul

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i j : Fin (n + 1)
h1 : ∀ (i : Fin (n + 1)), ∑ x, (s.points x -ᵥ s.points i) = ∑ x, (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0))
this✝ : s.points i -ᵥ s.points j = -(s.points j -ᵥ s.points i)
this : (↑n)⁻¹ • n • (s.points j -ᵥ s.points i) = (↑n)⁻¹ • ↑n • (s.points j -ᵥ s.points i)
⊢ (1 / ↑n) • (s.points j -ᵥ s.points i) + (s.points j -ᵥ s.points i) =
    (1 / ↑n) • (s.points j -ᵥ s.points i) + (s.points j -ᵥ s.points 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)
⊢ s.faceOppositeCentroid i -ᵥ s.centroid = 1 • (s.faceOppositeCentroid i -ᵥ s.centroid)

Tactic:
one_smul

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)
⊢ s.faceOppositeCentroid i -ᵥ s.centroid = s.faceOppositeCentroid 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
i : Fin (n + 1)
⊢ s.centroid -ᵥ s.faceOppositeCentroid i = 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)

Tactic:
one_smul

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)
⊢ s.centroid -ᵥ s.faceOppositeCentroid i = s.centroid -ᵥ s.faceOppositeCentroid i