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

Goal state before:
pp: case pos
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x | ContinuousOn (F x) (spectrum R a)}
⊢ Tendsto (fun x ↦ (cfcHom ha) { toFun := (spectrum R a).domRestrict (F ↑x), continuous_toFun := ⋯ })
    (comap Subtype.val l) (𝓝 ((cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ }))

Tactic:
apply cfcHom_continuous _ |>.tendsto _ |>.comp

Goal state after:
case pos
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := ⋯
⊢ Tendsto (fun x ↦ { toFun := (spectrum R a).domRestrict (F ↑x), continuous_toFun := ⋯ }) (comap Subtype.val l)
    (𝓝 { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })
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
B : Type u_2
inst✝¹² : PartialOrder B
inst✝¹¹ : Ring B
inst✝¹⁰ : StarRing B
inst✝⁹ : TopologicalSpace B
inst✝⁸ : StarOrderedRing B
inst✝⁷ : Algebra ℝ B
inst✝⁶ : ContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst✝⁵ : ContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst✝⁴ : IsSemitopologicalRing B
inst✝³ : T2Space B
inst✝² : StarOrderedRing (A × B)
inst✝¹ : NonnegSpectrumClass ℝ B
inst✝ : NonnegSpectrumClass ℝ (A × B)
a : A
b : B
x : ℝ
ha : IsUnit a
hb : IsUnit b
ha' : 0 ≤ a
hb' : 0 ≤ b
ha'' : 0 ∉ spectrum ℝ≥0 a
hb'' : 0 ∉ spectrum ℝ≥0 b
⊢ 0 ≤ (a, b)

Tactic:
Prod.le_def

Goal state after:
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
B : Type u_2
inst✝¹² : PartialOrder B
inst✝¹¹ : Ring B
inst✝¹⁰ : StarRing B
inst✝⁹ : TopologicalSpace B
inst✝⁸ : StarOrderedRing B
inst✝⁷ : Algebra ℝ B
inst✝⁶ : ContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst✝⁵ : ContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst✝⁴ : IsSemitopologicalRing B
inst✝³ : T2Space B
inst✝² : StarOrderedRing (A × B)
inst✝¹ : NonnegSpectrumClass ℝ B
inst✝ : NonnegSpectrumClass ℝ (A × B)
a : A
b : B
x : ℝ
ha : IsUnit a
hb : IsUnit b
ha' : 0 ≤ a
hb' : 0 ≤ b
ha'' : 0 ∉ spectrum ℝ≥0 a
hb'' : 0 ∉ spectrum ℝ≥0 b
⊢ 0.1 ≤ (a, b).1 ∧ 0.2 ≤ (a, b).2
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
x : ℝ≥0
ha : 0 ≤ a
hx : ¬x = 0
h₁ : 0 ≤ ↑x
⊢ a ^ (1 / 2 * ↑x) = a ^ (↑x / 2)

Tactic:
one_div_mul_eq_div

Goal state after:
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
x : ℝ≥0
ha : 0 ≤ a
hx : ¬x = 0
h₁ : 0 ≤ ↑x
⊢ a ^ (↑x / 2) = a ^ (↑x / 2)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ : inr ∘ cfcₙ f = fun x ↦ ↑(cfcₙ f x)
x✝ : A
⊢ ↑(cfcₙ f x✝) = cfc f ↑x✝

Tactic:
real_cfcₙ_eq_cfc_inr ..

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ : inr ∘ cfcₙ f = fun x ↦ ↑(cfcₙ f x)
x✝ : A
⊢ cfc f ↑x✝ = cfc f ↑x✝
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
⊢ ∀ {z : ℂ} {x y : C⋆ᵐᵒᵈ(A, (i : ι) → E i)}, ∑ i, ⟪x i, (z • y) i⟫_A = z • ∑ i, ⟪x i, y i⟫_A

Tactic:
by simp [smul_sum]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
⊢ cfc (fun x ↦ 1 - (1 + x)⁻¹) ↑a ≤ cfc (fun x ↦ 1 - (1 + x)⁻¹) ↑b

Tactic:
have h_cfc_one_sub (c : A⁺¹) (hc : 0 ≤ c := by cfc_tac) :
      cfc (fun x : ℝ≥0 ↦ 1 - (1 + x)⁻¹) c = 1 - cfc (·⁻¹ : ℝ≥0 → ℝ≥0) (1 + c) := by
    rw [cfc_tsub _ _ _ (fun x _ ↦ by simp) (hg := by fun_prop (disch := intro _ _; positivity)),
      cfc_const_one ℝ≥0 c, cfc_comp' (·⁻¹) (1 + ·) c ?_, cfc_add .., cfc_const_one ℝ≥0 c,
      cfc_id' ℝ≥0 c]
    exact continuousOn_id.inv₀ (Set.forall_mem_image.mpr fun x _ ↦ by dsimp only [id]; positivity)

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
h_cfc_one_sub :
  ∀ (c : Unitization ℂ A),
    autoParam (0 ≤ c) monotoneOn_one_sub_one_add_inv._auto_1_6 →
      cfc (fun x ↦ 1 - (1 + x)⁻¹) c = 1 - cfc (fun x ↦ x⁻¹) (1 + c)
⊢ cfc (fun x ↦ 1 - (1 + x)⁻¹) ↑a ≤ cfc (fun x ↦ 1 - (1 + x)⁻¹) ↑b
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‖ ^ 2 ≤ ‖x‖ ^ 2

Tactic:
pi_norm_sq,

Goal state after:
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‖ ^ 2 ≤ ‖∑ i, ⟪x i, x i⟫_A‖
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x ↦ x * m) l (𝓝 m)
n : ℕ
c : Fin n → ℂ
x : Fin n → ↑({x | 0 ≤ x} ∩ ball 0 1)
this : ∑ i, c i • ↑(x i) ∈ span ℂ ({x | 0 ≤ x} ∩ ball 0 1)
i : Fin n
x✝ : i ∈ Finset.univ
⊢ Tendsto (fun x_1 ↦ c i • (x_1 * ↑(x i))) l (𝓝 (c i • ↑(x i)))

Tactic:
exact tendsto_const_nhds.smul <| h (x i) (x i).2.1 <| by simpa using (x i).2.2

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✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
⊢ (∑ i, ∑ j, ‖∑ j_1, A i j_1 * B j_1 j‖₊ ^ 2) ^ (1 / 2) ≤
    (∑ i, ∑ j, ‖A i j‖₊ ^ 2) ^ (1 / 2) * (∑ i, ∑ j, ‖B i j‖₊ ^ 2) ^ (1 / 2)

Tactic:
← NNReal.mul_rpow,

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✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
⊢ (∑ i, ∑ j, ‖∑ j_1, A i j_1 * B j_1 j‖₊ ^ 2) ^ (1 / 2) ≤ ((∑ i, ∑ j, ‖A i j‖₊ ^ 2) * ∑ i, ∑ j, ‖B i j‖₊ ^ 2) ^ (1 / 2)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: 𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : IsScalarTower 𝕜 A A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : ContinuousStar A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ ContinuousOn (fun x ↦ cfcₙ f x) {a | p a ∧ quasispectrum 𝕜 a ⊆ s}

Tactic:
by_cases hs0 : 0 ∈ s

Goal state after:
case pos
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : IsScalarTower 𝕜 A A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : ContinuousStar A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∈ s
⊢ ContinuousOn (fun x ↦ cfcₙ f x) {a | p a ∧ quasispectrum 𝕜 a ⊆ s}

case neg
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : IsScalarTower 𝕜 A A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : ContinuousStar A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∉ s
⊢ ContinuousOn (fun x ↦ cfcₙ f x) {a | p a ∧ quasispectrum 𝕜 a ⊆ s}
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, ∀ (a : A₁), ‖f a‖ ≤ ↑C * ‖a‖

Tactic:
suffices h_nonneg : ∃ C : ℝ≥0, ∀ a, 0 ≤ a → ‖f a‖ ≤ C * ‖a‖ by
    obtain ⟨C, hmain⟩ := h_nonneg
    refine ⟨4 * C, fun x ↦ ?_⟩
    obtain ⟨y, hy_nonneg, hy_norm, hy⟩ := CStarAlgebra.exists_sum_four_nonneg x
    conv_lhs => rw [hy]
    simp only [map_sum, map_smul]
    apply norm_sum_le _ _ |>.trans
    simp only [norm_smul, norm_pow, norm_I, one_pow, one_mul]
    apply Finset.sum_le_sum (g := fun _ ↦ C * ‖x‖) (fun i _ ↦ ?_) |>.trans <| by simp [mul_assoc]
    apply hmain _ (hy_nonneg i) |>.trans
    gcongr
    exact hy_norm i

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, ∀ (a : A₁), 0 ≤ a → ‖f a‖ ≤ ↑C * ‖a‖
Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap

Goal state before:
pp: F : Type u_1
A₁ : Type u_2
A₂ : Type u_3
inst✝⁷ : NonUnitalCStarAlgebra A₁
inst✝⁶ : NonUnitalCStarAlgebra A₂
inst✝⁵ : PartialOrder A₁
inst✝⁴ : PartialOrder A₂
inst✝³ : StarOrderedRing A₁
inst✝² : StarOrderedRing A₂
inst✝¹ : FunLike F A₁ A₂
inst✝ : LinearMapClass F ℂ A₁ A₂
h : ∀ (φ : F) (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑φ
⊢ ∀ (f : F) (x : A₁), 0 ≤ x → 0 ≤ f x

Tactic:
intro φ a ha

Goal state after:
F : Type u_1
A₁ : Type u_2
A₂ : Type u_3
inst✝⁷ : NonUnitalCStarAlgebra A₁
inst✝⁶ : NonUnitalCStarAlgebra A₂
inst✝⁵ : PartialOrder A₁
inst✝⁴ : PartialOrder A₂
inst✝³ : StarOrderedRing A₁
inst✝² : StarOrderedRing A₂
inst✝¹ : FunLike F A₁ A₂
inst✝ : LinearMapClass F ℂ A₁ A₂
h : ∀ (φ : F) (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑φ
φ : F
a : A₁
ha : 0 ≤ a
⊢ 0 ≤ φ a
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_5
M : CStarMatrix m n A
⊢ M.map id = M

Tactic:
by
  ext
  rfl

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✝⁵ : Unique n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Star A
inst✝ : Module R A
x✝ : A
⊢ (fun x y ↦ star x✝) = star fun x y ↦ x✝

Tactic:
ext; simp [star_eq_conjTranspose]

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

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
b : OrthonormalBasis ι ℝ E
L : StrongDual ℝ E
⊢ ‖L‖ ^ 2 = ∑ i, L (b i) ^ 2

Tactic:
have := b.toBasis.finiteDimensional_of_finite
  simp_rw [← (InnerProductSpace.toDual ℝ E).symm.norm_map, ← b.sum_sq_inner_left,
    InnerProductSpace.toDual_symm_apply]

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
hx : (x, y) ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y)
x₁ : E
hx₁ : x₁ ∈ s
x₂ : E
hx₂ : x₂ ∈ s
hx_fst : (x, y).1 ∈ openSegment 𝕜 x₁ x₂
⊢ (x, y) ∈ (fun x_1 ↦ (x_1, (x, y).2)) '' openSegment 𝕜 x₁ x₂

Tactic:
exact mem_image_of_mem _ hx_fst

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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CStarAlgebra A
inst✝³ : CStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective ⇑φ
h_spec : spectrum ℝ ((StarAlgHom.restrictScalars ℝ ↑φ) a) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum ℝ (φ a)
f : C(ℝ, ℝ)
h_eqOn : Set.EqOn (⇑f) 0 (spectrum ℝ (φ a))
h_eqOn_x : Set.EqOn (⇑f) 1 {x}
⊢ False

Tactic:
suffices φ (cfc f a) = 0 by
    rw [map_eq_zero_iff φ hφ, ← cfc_zero ℝ a, cfc_eq_cfc_iff_eqOn] at this
    exact zero_ne_one <| calc
      0 = f x := (this hx).symm
      _ = 1 := h_eqOn_x <| Set.mem_singleton x

Goal state after:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CStarAlgebra A
inst✝³ : CStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective ⇑φ
h_spec : spectrum ℝ ((StarAlgHom.restrictScalars ℝ ↑φ) a) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum ℝ (φ a)
f : C(ℝ, ℝ)
h_eqOn : Set.EqOn (⇑f) 0 (spectrum ℝ (φ a))
h_eqOn_x : Set.EqOn (⇑f) 1 {x}
⊢ φ (cfc (⇑f) a) = 0
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✝ e e' : OpenPartialHomeomorph X Y
inst✝¹ : (x : X) → Decidable (x ∈ e.source)
inst✝ : (y : Y) → Decidable (y ∈ e.target)
Hs : Disjoint e.source e'.source
Ht : Disjoint e.target e'.target
⊢ EqOn (↑e) (↑e') (e.source ∩ frontier e.source)

Tactic:
by
          rw [e.open_source.inter_frontier_eq]
          exact eqOn_empty _ _

Goal state after:
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
⊢ EqOn (↑(e.subtypeRestr hV).symm) (inclusion hUV ∘ ↑(e.subtypeRestr hU).symm) (e.subtypeRestr hU).target

Tactic:
by
  set i := Set.inclusion hUV
  intro y hy
  dsimp [OpenPartialHomeomorph.subtypeRestr_def] at hy ⊢
  have hyV : e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target := by
    rw [Opens.openPartialHomeomorphSubtypeCoe_target] at hy ⊢
    exact hUV hy.2
  refine (V.openPartialHomeomorphSubtypeCoe hV).injOn ?_ trivial ?_
  · simp
  · rw [(V.openPartialHomeomorphSubtypeCoe hV).right_inv hyV]
    change _ = U.openPartialHomeomorphSubtypeCoe hU _
    rw [(U.openPartialHomeomorphSubtypeCoe hU).right_inv hy.2]

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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
x : ↑s × F
hx : (↑x.1, x.2) ∈ e.target
⊢ (if h : (↑x.1, x.2) ∈ e.target then ⟨e.invFun (↑x.1, x.2), ⋯⟩
    else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) x.1 x.2) ∈
    Subtype.val ⁻¹' e.source

Tactic:
rw [dif_pos hx]

Goal state after:
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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
x : ↑s × F
hx : (↑x.1, x.2) ∈ e.target
⊢ ⟨e.invFun (↑x.1, x.2), ⋯⟩ ∈ Subtype.val ⁻¹' e.source
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 : ι
p : B × F
⊢ p ∈ (Z.localTrivAsPartialEquiv i).target ↔ p.1 ∈ Z.baseSet i

Tactic:
rw [localTrivAsPartialEquiv, 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 : ι
p : B × F
⊢ p.1 ∈ Z.baseSet i ∧ p.2 ∈ univ ↔ p.1 ∈ Z.baseSet i
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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
x : ↑s × F
hx : (↑x.1, x.2) ∈ e.target
⊢ (proj
        ↑(if h : (↑x.1, x.2) ∈ e.target then ⟨e.invFun (↑x.1, x.2), ⋯⟩
          else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) x.1 x.2),
      id
        (↑e
            ↑(if h : (↑x.1, x.2) ∈ e.target then ⟨e.invFun (↑x.1, x.2), ⋯⟩
              else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) x.1 x.2)).2) =
    Prod.map Subtype.val id x

Tactic:
rw [dif_pos hx]

Goal state after:
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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
x : ↑s × F
hx : (↑x.1, x.2) ∈ e.target
⊢ (proj ↑⟨e.invFun (↑x.1, x.2), ⋯⟩, id (↑e ↑⟨e.invFun (↑x.1, x.2), ⋯⟩).2) = Prod.map Subtype.val id x
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
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
⊢ ∀ p ∈ (e.disjointUnion e'.toOpenPartialHomeomorph ⋯ ⋯).source,
    (↑(e.disjointUnion e'.toOpenPartialHomeomorph ⋯ ⋯) p).1 = proj p

Tactic:
rintro p (hp | hp')
    · change (e.source.piecewise e e' p).1 = proj p
      rw [piecewise_eq_of_mem, e.coe_fst] <;> exact hp
    · change (e.source.piecewise e e' p).1 = proj p
      rw [piecewise_eq_of_notMem, e'.coe_fst hp']
      simp only [source_eq] at hp' ⊢
      exact fun h => H.le_bot ⟨h, hp'⟩

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
T : Trivialization F proj
ι : Type u_5
inst✝¹ : TopologicalSpace ι
inst✝ : LocallyCompactPair ι ↑T.baseSet
γ : C(ι, ↑T.baseSet)
i : ι
e : ↑T.source
h : proj ↑e = ↑(γ i)
this : proj ↑e ∈ T.baseSet
⊢ (T.clift (e, γ)) i = e

Tactic:
simp [clift, liftCM, ← h, lift_self, this]

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

Goal state before:
pp: case refine_1
𝕜 : 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 : F
⊢ ‖(adjointAux A) x‖ ≤ ‖A‖ * ‖x‖

Tactic:
rw [adjointAux_apply, LinearIsometryEquiv.norm_map]

Goal state after:
case refine_1
𝕜 : 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 : F
⊢ ‖(toSesqForm A) x‖ ≤ ‖A‖ * ‖x‖
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: case refine_2
𝕜 : 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
⊢ ‖(adjointAux (adjointAux A)) x‖ ≤ ‖adjointAux A‖ * ‖x‖

Tactic:
rw [adjointAux_apply, LinearIsometryEquiv.norm_map]

Goal state after:
case refine_2
𝕜 : 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
⊢ ‖(toSesqForm (adjointAux A)) x‖ ≤ ‖adjointAux A‖ * ‖x‖
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : Fin 4 → ↥(unitary A)
c : Fin 4 → ℂ
h : ∀ (i : Fin 4), ‖c i‖ ≤ ‖∑ i, c i • ↑(u i)‖ / 2
⊢ ∑ i, c i • ↑(u i) ∈ span ℂ ↑(unitary A)

Tactic:
exact sum_mem fun i _ ↦ smul_mem _ _ (subset_span (u i).2)

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

Goal state before:
pp: f : ℝ → ℝ
s : Set ℝ
hs : UniqueDiffOn ℝ s
n : ℕ
x : ℝ
hx : x ∈ s
p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hp : HasFTaylorSeriesUpToOn ∞ f p s
hp_nn : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → 0 ≤ (p x n) fun x ↦ 1
⊢ 0 ≤ iteratedDerivWithin n f s x

Tactic:
have heq : p x n = iteratedFDerivWithin ℝ n f s x :=
    hp.eq_iteratedFDerivWithin_of_uniqueDiffOn (mod_cast le_top) hs hx

Goal state after:
f : ℝ → ℝ
s : Set ℝ
hs : UniqueDiffOn ℝ s
n : ℕ
x : ℝ
hx : x ∈ s
p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hp : HasFTaylorSeriesUpToOn ∞ f p s
hp_nn : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → 0 ≤ (p x n) fun x ↦ 1
heq : p x n = iteratedFDerivWithin ℝ n f s x
⊢ 0 ≤ iteratedDerivWithin n f s x
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
s₁ s₂ : AffineSubspace k P
inst✝¹ : FiniteDimensional k ↥s₁.direction
inst✝ : FiniteDimensional k ↥s₂.direction
⊢ FiniteDimensional k ↥(s₁ ⊔ s₂).direction

Tactic:
by
  rcases eq_bot_or_nonempty s₁ with rfl | ⟨p₁, hp₁⟩
  · rwa [bot_sup_eq]
  rcases eq_bot_or_nonempty s₂ with rfl | ⟨p₂, hp₂⟩
  · rwa [sup_bot_eq]
  rw [AffineSubspace.direction_sup hp₁ hp₂]
  infer_instance

Goal state after: