mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace

Goal state before:
pp: case inl
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
h₁ : φ 1 * (1 - φ 1) = 0
h₂ : φ 1 = 0
⊢ φ 1 = 1

Tactic:
have : ∀ a, φ (a * 1) = 0 := fun a => by simp only [map_mul φ, h₂, mul_zero]

Goal state after:
case inl
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
h₁ : φ 1 * (1 - φ 1) = 0
h₂ : φ 1 = 0
this : ∀ (a : A), φ (a * 1) = 0
⊢ φ 1 = 1
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
s : Set α
hf : UpperHemicontinuousOn f s
hg : UpperHemicontinuousOn g s
⊢ UpperHemicontinuousOn (fun x ↦ f x ∪ g x) s

Tactic:
by
  rw [upperHemicontinuousOn_iff] at hf hg ⊢
  exact fun x hx ↦ (hf x hx).union (hg x hx)

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
ι : Type u_5
inst✝ : RegularSpace β
x₀ : α
l : Filter ι
hf : UpperHemicontinuousAt f x₀
hf_closed : IsClosed[inst✝¹] (f x₀)
x : ι → α
hx : Tendsto x l (𝓝 x₀)
y : ι → β
hy : ∃ᶠ (n : ι) in l, y n ∈ f (x n)
y₀ : β
hy₀ : Tendsto y l (𝓝 y₀)
this✝ : y₀ ∉ f x₀
s : Set β
hs : s ∈ 𝓝ˢ (f x₀)
t : Set β
ht : t ∈ 𝓝 y₀
hst : Disjoint s t
this : ∃ᶠ (n : ι) in l, y n ∈ s
⊢ False

Tactic:
apply this
    filter_upwards [hy₀ ht] with n hn hyn
    exact hst.notMem_of_mem_left hyn hn

Goal state after:
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
U : SetRel α α
s₁ s₂ t₁ t₂ : Set α
h₁ : (s₁, t₁) ∈ hausdorffEntourage U
h₂ : (s₂, t₂) ∈ hausdorffEntourage U
⊢ (s₁ ∪ s₂, t₁ ∪ t₂) ∈ hausdorffEntourage U

Tactic:
grind [mem_hausdorffEntourage, preimage_union, image_union]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NormedField 𝕜
B : Type u_3
inst✝⁵ : NonUnitalNormedRing B
inst✝⁴ : NormedSpace 𝕜 B
inst✝³ : CompleteSpace B
inst✝² : IsScalarTower 𝕜 B B
inst✝¹ : SMulCommClass 𝕜 B B
inst✝ : ProperSpace 𝕜
a : B
⊢ IsCompact (quasispectrum 𝕜 a)

Tactic:
rw [Unitization.quasispectrum_eq_spectrum_inr' 𝕜 𝕜,
    ← AlgEquiv.spectrum_eq (WithLp.unitizationAlgEquiv 𝕜).symm (a : Unitization 𝕜 B)]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NormedField 𝕜
B : Type u_3
inst✝⁵ : NonUnitalNormedRing B
inst✝⁴ : NormedSpace 𝕜 B
inst✝³ : CompleteSpace B
inst✝² : IsScalarTower 𝕜 B B
inst✝¹ : SMulCommClass 𝕜 B B
inst✝ : ProperSpace 𝕜
a : B
⊢ IsCompact (σ ((WithLp.unitizationAlgEquiv 𝕜).symm ↑a))
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsOpen[instTopologicalSpaceProd] U
this✝ : U.IsRefl
this : TopologicalSpace (Set α) := TopologicalSpace.vietoris α
V : SetRel α α
hV₁ : V ∈ 𝓤 α
hV₂ : IsOpen[instTopologicalSpaceProd] V
left✝ : V.IsSymm
hVU : V.comp V ⊆ U
t : Finset α
ht₁ : (↑t, s).1 ⊆ V.preimage (↑t, s).2
ht₂ : (↑t, s).2 ⊆ V.image (↑t, s).1
⊢ {a | s ⊆ U.preimage a} ∈ 𝓝 s

Tactic:
dsimp only at ht₁ ht₂

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsOpen[instTopologicalSpaceProd] U
this✝ : U.IsRefl
this : TopologicalSpace (Set α) := TopologicalSpace.vietoris α
V : SetRel α α
hV₁ : V ∈ 𝓤 α
hV₂ : IsOpen[instTopologicalSpaceProd] V
left✝ : V.IsSymm
hVU : V.comp V ⊆ U
t : Finset α
ht₁ : ↑t ⊆ V.preimage s
ht₂ : s ⊆ V.image ↑t
⊢ {a | s ⊆ U.preimage a} ∈ 𝓝 s
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case neg.inr
α : Type u_1
inst✝ : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS : S ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
hKS : {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U | IsOpen[inst✝] U ∧ {s | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ L ∈ s, (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : U ∈ {V | IsOpen[inst✝] V}
hUS : (fun V ↦ {s | (s ∩ V).Nonempty}) U ∈ S
hUu : K \ ⋃₀ u ∈ (fun V ↦ {s | (s ∩ V).Nonempty}) U
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q

Tactic:
obtain ⟨x, hxu, hxU⟩ := hUu
      cases hxu.2 <| mem_sUnion_of_mem hxU ⟨hU, hUS⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst✝⁶ : NormedField 𝕜₁
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜₁ A
inst✝² : NormedAlgebra 𝕜₂ A
inst✝¹ : NormedAlgebra 𝕜₁ 𝕜₂
inst✝ : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), ‖(algebraMap 𝕜₁ 𝕜₂) x‖₊ = ‖x‖₊
x : 𝕜₁
hx : x ∈ spectrum 𝕜₁ a
⊢ ↑‖x‖₊ ≤ ⨆ k ∈ spectrum 𝕜₂ a, ↑‖k‖₊

Tactic:
refine congr_arg ((↑) : ℝ≥0 → ℝ≥0∞) (this x) |>.symm.trans_le <| le_iSup₂ (α := ℝ≥0∞) _ ?_
    exact (spectrum.algebraMap_mem_iff _).mpr hx

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
y : ℝ≥0
hy : ↑y ∈ spectrum ℝ a
hx : ↑t - ↑y ∈ {↑t} - spectrum ℝ a
hty : -↑t ≤ ↑y
hyt : ↑y ≤ ↑t
⊢ y ≤ t

Tactic:
exact_mod_cast hyt

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: A : Type u_2
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : CompleteSpace A
⊢ UpperHemicontinuous (quasispectrum ℝ≥0)

Tactic:
obtain ⟨⟨h₁, -⟩, h₂⟩ := NNReal.isClosedEmbedding_coe
  simpa [← NNReal.algebraMap_eq_coe] using
    upperHemicontinuous_quasispectrum ℝ A |>.isInducing_comp h₁ h₂

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
⊢ √(spectralRadius ℂ (a⋆ * a)).toReal = ‖a‖

Tactic:
by
  simp [toReal_spectralRadius_star_mul_self_eq_norm_sq]

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {U | IsOpen[instTopologicalSpaceProd] U}
K : Compacts α
L : Compacts β
hKL : ↑K ×ˢ ↑L ⊆ U
⊢ ∃ t ⊆ (SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' 𝒫 U, IsOpen t ∧ (K, L) ∈ t

Tactic:
obtain ⟨V, W, hV, hW, hK, hL, hVW⟩ := generalized_tube_lemma K.isCompact L.isCompact hU hKL

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {U | IsOpen[instTopologicalSpaceProd] U}
K : Compacts α
L : Compacts β
hKL : ↑K ×ˢ ↑L ⊆ U
V : Set α
W : Set β
hV : IsOpen[inst✝¹] V
hW : IsOpen[inst✝] W
hK : ↑K ⊆ V
hL : ↑L ⊆ W
hVW : V ×ˢ W ⊆ U
⊢ ∃ t ⊆ (SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' 𝒫 U, IsOpen t ∧ (K, L) ∈ t
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : ↑K ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : Set α → Set α
hM : ∀ U ∈ u, IsCompact (M U)
hML : ∀ U ∈ u, M U ⊆ L
hMU : ∀ U ∈ u, M U ⊆ U
hMK : ∀ U ∈ u, (↑K ∩ interior (M U)).Nonempty
⊢ IsCompact {K' | ↑K' ⊆ L ∧ ∀ U ∈ u, (↑K' ∩ M U).Nonempty}

Tactic:
rw [isEmbedding_coe.isCompact_iff]
    refine vietoris.isCompact_aux hL (s := M '' u) (by grind) (by grind)
      |>.of_subset_of_specializes (by grind) (fun s ⟨hsL, hsu⟩ => ?_)
    /- The set `s` is not necessarily compact, but it specializes to the compact set
    `L ∩ closure s`. -/
    rw [forall_mem_image] at hsu
    let s' : Compacts α := ⟨L ∩ closure s, hL.inter_right isClosed_closure⟩
    refine ⟨s', mem_image_of_mem _ ⟨inter_subset_left, fun U hU => (hsu hU).mono ?_⟩,
      vietoris.specializes_of_subset_closure ?_ ?_⟩ <;>
      grind [coe_mk, subset_closure]

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
hK : K ≠ ⊥
hL : IsPreconnected ↑L
⊢ IsPreconnected (Icc K L)

Tactic:
wlog hKL : K ≤ L

Goal state after:
case inr
α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
hK : K ≠ ⊥
hL : IsPreconnected ↑L
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] {K L : Compacts α},
    K ≠ ⊥ → IsPreconnected ↑L → K ≤ L → IsPreconnected (Icc K L)
hKL : ¬K ≤ L
⊢ IsPreconnected (Icc K L)

α✝ : Type u_1
inst✝¹ : TopologicalSpace α✝
α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
hK : K ≠ ⊥
hL : IsPreconnected ↑L
hKL : K ≤ L
⊢ IsPreconnected (Icc K L)
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : PartialOrder 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : LocallyConvexSpace 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : FirstCountableTopology E
u : ℕ → Set E
hu_basis : (𝓝 0).HasAntitoneBasis u
hu_zero : ∀ (n : ℕ), 0 ∈ interior (u n)
v : ℕ → Set E := fun n ↦ (absConvexHull 𝕜) (interior (u n))
hv_open : ∀ (n : ℕ), IsOpen[inst✝⁵] (v n)
hv_nhds : ∀ (n : ℕ), v n ∈ 𝓝 0
hv_basis : (𝓝 0).HasAntitoneBasis v
m : ℕ
⊢ ∀ᶠ (n : ℕ) in Filter.atTop, v n + v n ⊆ v m

Tactic:
obtain ⟨W, hW_open, hW_zero, hW_add⟩ := exists_open_nhds_zero_add_subset (hv_nhds m)
      obtain ⟨N, hN⟩ := hv_basis.mem_iff.mp (hW_open.mem_nhds hW_zero)
      filter_upwards [Filter.eventually_ge_atTop N] with M hM
      exact (add_subset_add ((hv_basis.antitone hM).trans hN)
        ((hv_basis.antitone hM).trans hN)).trans hW_add

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : PartialOrder 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : LocallyConvexSpace 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : FirstCountableTopology E
⊢ ∃ x,
    (𝓝 0).HasAntitoneBasis x ∧
      ∀ (n : ℕ),
        IsOpen[inst✝⁵] (x n) ∧ AbsConvex 𝕜 (x n) ∧ x (n + 1) + x (n + 1) ⊆ x n ∧ closure[inst✝⁵] (x (n + 1)) ⊆ x n

Tactic:
by
  obtain ⟨u, hu_basis, -⟩ := IsTopologicalAddGroup.exists_antitone_basis_nhds_zero E
  have hu_zero (n : ℕ) : 0 ∈ interior (u n) :=
    mem_interior_iff_mem_nhds.mpr (hu_basis.mem_of_mem trivial)
  let v (n : ℕ) := absConvexHull 𝕜 (interior (u n))
  have hv_open (n : ℕ) : IsOpen (v n) := isOpen_interior.absConvexHull 𝕜 (hu_zero n)
  have hv_nhds (n : ℕ) : v n ∈ 𝓝 0 := (hv_open n).mem_nhds (subset_absConvexHull (hu_zero n))
  have hv_basis : (𝓝 0).HasAntitoneBasis v := by
    refine ⟨hu_basis.to_hasBasis ?_ ?_,
      fun _ _ hij ↦ absConvexHull_mono (interior_mono (hu_basis.antitone hij))⟩
    · intro n _
      obtain ⟨W, ⟨hW_nhds, hW_abs⟩, hWn⟩ :=
        (nhds_hasBasis_absConvex 𝕜 E).mem_iff.mp (hu_basis.mem_of_mem trivial)
      obtain ⟨m, hm⟩ := hu_basis.mem_iff.mp hW_nhds
      exact ⟨m, trivial, (absConvexHull_min (interior_subset.trans hm) hW_abs).trans hWn⟩
    · intro n _
      obtain ⟨m, hm⟩ := hu_basis.mem_iff.mp (isOpen_interior.mem_nhds (hu_zero n))
      exact ⟨m, trivial, hm.trans subset_absConvexHull⟩
  obtain ⟨φ, -, hφ_add, hφ_basis⟩ := hv_basis.subbasis_with_rel
    (r := fun i j ↦ v j + v j ⊆ v i) fun m ↦ by
      obtain ⟨W, hW_open, hW_zero, hW_add⟩ := exists_open_nhds_zero_add_subset (hv_nhds m)
      obtain ⟨N, hN⟩ := hv_basis.mem_iff.mp (hW_open.mem_nhds hW_zero)
      filter_upwards [Filter.eventually_ge_atTop N] with M hM
      exact (add_subset_add ((hv_basis.antitone hM).trans hN)
        ((hv_basis.antitone hM).trans hN)).trans hW_add
  exact ⟨v ∘ φ, hφ_basis, fun n ↦ ⟨hv_open (φ n), absConvex_absConvexHull, hφ_add (by simp),
    (closure_subset_add_self_of_mem_nhds_zero (hv_nhds (φ (n + 1)))).trans
        (hφ_add n.lt_succ_self)⟩⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.AddTorsor

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor V P
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 V
p₁ p₂ : P
c₁ c₂ : 𝕜
⊢ dist ((lineMap p₁ p₂) c₁) ((lineMap p₁ p₂) c₂) = dist c₁ c₂ * dist p₁ p₂

Tactic:
rw [dist_comm p₁ p₂]
  simp only [lineMap_apply, dist_eq_norm_vsub, vadd_vsub_vadd_cancel_right,
    ← sub_smul, norm_smul, vsub_eq_sub]

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
hx : x ∉ c.U
⊢ approx n c x = 1

Tactic:
induction n generalizing c with
  | zero =>
    rw [← mem_compl_iff] at hx
    exact indicator_of_mem hx _
  | succ n ihn =>
    simp only [approx]
    rw [ihn, ihn, midpoint_self]
    exacts [hx, fun hU => hx <| c.left_U_subset hU]

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
x : X
h : x ∈ c.C
⊢ c.lim x = 0

Tactic:
by
  simp only [CU.lim, approx_of_mem_C, h, ciSup_const]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r' : k
h : 0 < r' * (b - a)
⊢ f (r' * (a - b) + b) ≤ r' • (f a - f b) + f b ↔
    (b - a)⁻¹ • (f b - f a) ≤ (r' * (b - a))⁻¹ • (f b - f (r' * (a - b) + b))

Tactic:
le_inv_smul_iff_of_pos h,

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r' : k
h : 0 < r' * (b - a)
⊢ f (r' * (a - b) + b) ≤ r' • (f a - f b) + f b ↔ (r' * (b - a)) • (b - a)⁻¹ • (f b - f a) ≤ f b - f (r' * (a - b) + b)
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set X
f : C(X, R)
⊢ f ∉ idealOfSet R s ↔ ∃ x ∈ sᶜ, f x ≠ 0

Tactic:
by
  simp_rw [mem_idealOfSet]; push Not; rfl

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

Goal state before:
pp: A : Type u_1
inst✝ : CommCStarAlgebra A
⊢ ∀ {a : C(↑(characterSpace ℂ A), ℂ)},
    a ∈ (gelfandTransform ℂ A).range.carrier → star a ∈ (gelfandTransform ℂ A).range.carrier

Tactic:
rintro - ⟨a, rfl⟩
        use star a
        ext1 φ
        dsimp
        simp only [map_star, RCLike.star_def]

Goal state after:
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst✝¹ : PseudoEMetricSpace β
inst✝ : Finite ↑𝔖
f : γ → α →ᵤ[𝔖] β
K : ℝ≥0
⊢ LipschitzWith K f ↔ ∀ c ∈ ⋃₀ 𝔖, LipschitzWith K fun x ↦ (toFun 𝔖) (f x) c

Tactic:
by
  simp [LipschitzWith, edist_le]
  tauto

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric

Goal state before:
pp: case pos.inl
A : Type u_1
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace ℝ A
inst✝³ : SMulCommClass ℝ A A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : StarRing A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
h : x ≤ 0
⊢ ‖x⁺‖ ≤ ‖a‖

pp: case pos.inr
A : Type u_1
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace ℝ A
inst✝³ : SMulCommClass ℝ A A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : StarRing A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
h : 0 < x
⊢ ‖x⁺‖ ≤ ‖a‖

Tactic:
· simp [posPart_def, max_eq_right h]

Goal state after:
case pos.inr
A : Type u_1
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace ℝ A
inst✝³ : SMulCommClass ℝ A A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : StarRing A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
h : 0 < x
⊢ ‖x⁺‖ ≤ ‖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 b : A
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ^ 2 = b ^ 2 ↔ a = b

Tactic:
by
  simp_rw [sq, mul_self_eq_mul_self_iff a b]

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
⊢ -(algebraMap ℝ A) ‖a‖ ≤ a

Tactic:
rw [neg_le, ← norm_neg]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
⊢ -a ≤ (algebraMap ℝ A) ‖-a‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
r : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ ‖a‖ ≤ r ↔ a ≤ (algebraMap ℝ A) r

Tactic:
le_algebraMap_iff_spectrum_le

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
r : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ ‖a‖ ≤ r ↔ ∀ x ∈ spectrum ℝ a, x ≤ r
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: case neg.inl
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
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
H : ¬0 ≤ a
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ

Tactic:
rw [sqrt_of_not_nonneg H, inverse_zero]
      by_cases hunit : IsUnit a
      · have h₂ : ¬0 ≤ inverse a := by grind [CFC.ringInverse_nonneg_iff_nonneg_of_isUnit]
        rw [sqrt_of_not_nonneg h₂]
      · simp [inverse_non_unit _ hunit]

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
h : IsStrictlyPositive a
⊢ IsUnit b

Tactic:
nontriviality A
  rw [← spectrum.zero_notMem_iff ℝ]
  obtain ⟨r, hr, hr_le⟩ : ∃ r > 0, (algebraMap ℝ A) r ≤ a :=
    (exists_pos_algebraMap_le_iff h.isSelfAdjoint).2 fun x hx ↦ h.spectrum_pos hx
  exact fun h0 ↦ not_le_of_gt hr <| (algebraMap_le_iff_le_spectrum <| .of_nonneg <|
    h.nonneg.trans hab).1 (hr_le.trans hab) 0 h0

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

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℂ A
inst✝⁵ : Module ℂ E
inst✝⁴ : PartialOrder A
inst✝³ : SMul A E
inst✝² : Norm A
inst✝¹ : Norm E
inst✝ : CStarModule A E
x y z : E
⊢ ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫

Tactic:
by
  rw [← star_star (r := ⟪x + y, z⟫)]
  simp only [inner_add_right, star_add, star_inner]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Matrix

Goal state before:
pp: m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ ⨅ i, Filter.comap (fun a ↦ (a.1 i, a.2 i)) (𝓤 (n → 𝕜)) = ⨅ i, ⨅ j, Filter.comap (fun a ↦ (a.1 i j, a.2 i j)) (𝓤 𝕜)

Tactic:
simp_rw [Pi.uniformity, Filter.comap_iInf, Filter.comap_comap]

Goal state after:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ ⨅ i, ⨅ i_1, Filter.comap ((fun a ↦ (a.1 i_1, a.2 i_1)) ∘ fun a ↦ (a.1 i, a.2 i)) (𝓤 𝕜) =
    ⨅ i, ⨅ j, Filter.comap (fun a ↦ (a.1 i j, a.2 i j)) (𝓤 𝕜)
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: case inr
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j ↦ unitOf (A i j)
hN : ∀ b ∈ Finset.univ, ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x b‖₊ ≤ N
hxn : ‖x‖₊ = 1
⊢ ∑ j, ‖A i j‖₊ ≤ N

Tactic:
replace hN := hN i (Finset.mem_univ _)

Goal state after:
case inr
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j ↦ unitOf (A i j)
hxn : ‖x‖₊ = 1
hN : ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x i‖₊ ≤ N
⊢ ∑ j, ‖A i j‖₊ ≤ N
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
𝕜 : 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
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ i ∈ t, s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
S : ↑t → Set 𝕜
hS₁ : ∀ (x : ↑t), IsCompact (S x)
hS₂ : ∀ (x : ↑t), ∀ᶠ (x' : A) in 𝓝 (a ↑x), quasispectrum 𝕜 x' ⊆ S x
hS₃ : ∀ (x : ↑t), S x ⊆ s
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) t

Tactic:
refine ha_cont.cfcₙ (s := fun x : X ↦ if hx : x ∈ t then S ⟨x, hx⟩ else ∅) f
    (by simpa +contextual using hS₁) ?_ ha' ?_

Goal state after:
case refine_1
X : Type u_1
𝕜 : 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
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ i ∈ t, s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
S : ↑t → Set 𝕜
hS₁ : ∀ (x : ↑t), IsCompact (S x)
hS₂ : ∀ (x : ↑t), ∀ᶠ (x' : A) in 𝓝 (a ↑x), quasispectrum 𝕜 x' ⊆ S x
hS₃ : ∀ (x : ↑t), S x ⊆ s
⊢ ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ if hx : x₀ ∈ t then S ⟨x₀, hx⟩ else ∅

case refine_2
X : Type u_1
𝕜 : 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
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ i ∈ t, s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
S : ↑t → Set 𝕜
hS₁ : ∀ (x : ↑t), IsCompact (S x)
hS₂ : ∀ (x : ↑t), ∀ᶠ (x' : A) in 𝓝 (a ↑x), quasispectrum 𝕜 x' ⊆ S x
hS₃ : ∀ (x : ↑t), S x ⊆ s
⊢ ∀ x ∈ t, ContinuousOn f (if hx : x ∈ t then S ⟨x, hx⟩ else ∅)