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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁴ : CommRing R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : IsTopologicalRing R
inst✝⁹ : ContinuousStar R
inst✝⁸ : ContinuousSqrt R
inst✝⁷ : StarOrderedRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ 1 ≤ cfc f a ↔ ∀ x ∈ spectrum R a, 1 ≤ f x

Tactic:
by
  simpa using algebraMap_le_cfc_iff f 1 a

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁴ : CommRing R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : IsTopologicalRing R
inst✝⁹ : ContinuousStar R
inst✝⁸ : ContinuousSqrt R
inst✝⁷ : StarOrderedRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
⊢ 1 ≤ a ↔ ∀ x ∈ spectrum R a, 1 ≤ x

Tactic:
by
  simpa using algebraMap_le_iff_le_spectrum (r := (1 : R)) (a := a)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n ν : ℕ
⊢ Polynomial.map f (bernsteinPolynomial R n ν) = bernsteinPolynomial S n ν

Tactic:
by simp [bernsteinPolynomial]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝ : CommRing R
k : ℕ
ih : ∀ (n ν : ℕ), k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0
n ν : ℕ
h : k + 1 ≤ ν
⊢ Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R (n - 1) ν)) -
      Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R (n - 1) (ν + 1))) =
    0

Tactic:
ih _ _ (Nat.le_of_succ_le h),

Goal state after:
case succ.succ
R : Type u_1
inst✝ : CommRing R
k : ℕ
ih : ∀ (n ν : ℕ), k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0
n ν : ℕ
h : k + 1 ≤ ν
⊢ Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R (n - 1) ν)) - 0 = 0
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
⊢ ∑ ν ∈ Finset.range (n + 1), (n • X - ↑ν) ^ 2 * bernsteinPolynomial R n ν = n • X * (1 - X)

Tactic:
calc
    _ = _ := Finset.sum_congr rfl fun k m => ?_
    _ = _ := p
    _ = _ := ?_

Goal state after:
case calc_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
k : ℕ
m : k ∈ Finset.range (n + 1)
⊢ (n • X - ↑k) ^ 2 * bernsteinPolynomial R n k =
    (↑(k * (k - 1)) + (1 - ↑(2 * n) * X) * ↑k + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n k

case calc_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
⊢ ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1 = n • X * (1 - X)
Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace

Goal state before:
pp: 𝕜 : 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)
⊢ φ 1 = 1

Tactic:
have h₁ : φ 1 * (1 - φ 1) = 0 := by rw [mul_sub, sub_eq_zero, mul_one, ← map_mul φ, one_mul]

Goal state after:
𝕜 : 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
⊢ φ 1 = 1
Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
a b : A
⊢ { toFun := fun φ ↦ φ (a * b), continuous_toFun := ⋯ } =
    { toFun := fun φ ↦ φ a, continuous_toFun := ⋯ } * { toFun := fun φ ↦ φ b, continuous_toFun := ⋯ }

Tactic:
by ext; simp only [map_mul, coe_mk, coe_mul, Pi.mul_apply]

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

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → 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✝¹⁵ : Ring B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Algebra R B
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : ContinuousFunctionalCalculus R A p
inst✝⁴ : ContinuousFunctionalCalculus R B q
inst✝³ : ContinuousMap.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hφ : Continuous[inst✝¹⁷, inst✝¹³] ⇑φ
ha : p a
hφa : q (φ a)
ψ : A →⋆ₐ[R] B := StarAlgHom.restrictScalars R ↑φ
this✝ : Continuous[inst✝¹⁷, inst✝¹³] ⇑ψ
h_spec : spectrum R (ψ a) ⊆ spectrum R a
hψa : q (ψ a)
ι : C(↑(spectrum R (ψ a)), ↑(spectrum R a)) := { toFun := Set.inclusion h_spec, continuous_toFun := ⋯ }
this : ψ.comp (cfcHom ha) = (cfcHom hψa).comp (ContinuousMap.compStarAlgHom' R R ι)
⊢ φ (cfc f a) = cfc f (φ a)

Tactic:
have hf' : ContinuousOn f (spectrum R (ψ a)) := hf.mono h_spec

Goal state after:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → 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✝¹⁵ : Ring B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Algebra R B
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : ContinuousFunctionalCalculus R A p
inst✝⁴ : ContinuousFunctionalCalculus R B q
inst✝³ : ContinuousMap.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hφ : Continuous[inst✝¹⁷, inst✝¹³] ⇑φ
ha : p a
hφa : q (φ a)
ψ : A →⋆ₐ[R] B := StarAlgHom.restrictScalars R ↑φ
this✝ : Continuous[inst✝¹⁷, inst✝¹³] ⇑ψ
h_spec : spectrum R (ψ a) ⊆ spectrum R a
hψa : q (ψ a)
ι : C(↑(spectrum R (ψ a)), ↑(spectrum R a)) := { toFun := Set.inclusion h_spec, continuous_toFun := ⋯ }
this : ψ.comp (cfcHom ha) = (cfcHom hψa).comp (ContinuousMap.compStarAlgHom' R R ι)
hf' : ContinuousOn f (spectrum R (ψ a))
⊢ φ (cfc f a) = cfc f (φ a)
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
⊢ Dense ↑(adjoin 𝕜 {ContinuousMapZero.id s})

Tactic:
by
  have h0' : 0 ∈ s := Fact.out
  rw [dense_iff_closure_eq,
    ← isClosedEmbedding_toContinuousMap.injective.preimage_image (closure _),
    ← isClosedEmbedding_toContinuousMap.closure_image_eq, ← coe_toContinuousMapHom,
    ← NonUnitalStarSubalgebra.coe_map, NonUnitalStarAlgHom.map_adjoin_singleton,
    coe_toContinuousMapHom, toContinuousMap_id,
    ← ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id s h0']
  apply Set.eq_univ_of_forall fun f ↦ ?_
  simp only [Set.mem_preimage, SetLike.mem_coe, RingHom.mem_ker,
    ContinuousMap.evalStarAlgHom_apply, ContinuousMap.coe_coe]
  exact map_zero f

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
⊢ UpperHemicontinuousAt (fun x ↦ {f x}) x ↔ ContinuousAt f x

Tactic:
by
  simp [← upperHemicontinuousWithinAt_univ_iff, continuousWithinAt_univ]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
⊢ UpperHemicontinuousAt f x₀

Tactic:
by
  refine .of_frequently fun t ht hft ↦ ?_
  obtain ⟨x, hx, hfx⟩ := exists_seq_forall_of_frequently hft
  choose y hy using hfx
  obtain ⟨y₀, hy₀, φ, hφ, hyφ⟩ := hK.subseq_of_frequently_in (x := y) <| by
    refine Eventually.frequently ?_
    filter_upwards [hx hf] with n hn
    exact hn (hy n).1
  specialize h (x ∘ φ) (hx.comp hφ.tendsto_atTop) (y ∘ φ) (fun n ↦ (hy _).1) _ hyφ
  exact ⟨y₀, h, ht.closure_eq ▸ mem_closure_of_tendsto hyφ <| .of_forall fun n ↦ (hy _).2⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : Set α → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
t : Set α
x✝ : t ∈ {s | s ⊆ (⋃₀ u, f '' u).1 ∧ ∀ U ∈ (⋃₀ u, f '' u).2, (s ∩ U).Nonempty}
ht₁ : t ⊆ (⋃₀ u, f '' u).1
ht₂ : ∀ ⦃x : Set α⦄, x ∈ u → (t ∩ f x).Nonempty
U : Set α
hU : U ∈ u
⊢ (t ∩ U).Nonempty

Tactic:
← hfU U hU

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : Set α → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
t : Set α
x✝ : t ∈ {s | s ⊆ (⋃₀ u, f '' u).1 ∧ ∀ U ∈ (⋃₀ u, f '' u).2, (s ∩ U).Nonempty}
ht₁ : t ⊆ (⋃₀ u, f '' u).1
ht₂ : ∀ ⦃x : Set α⦄, x ∈ u → (t ∩ f x).Nonempty
U : Set α
hU : U ∈ u
⊢ (t ∩ f U).Nonempty
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ closure[TopologicalSpace.vietoris α] {t | t.Finite ∧ t ⊆ s} ⊆ 𝒫 closure[inst✝] s

Tactic:
rw [isClosed_closure.powerset_vietoris.closure_subset_iff]

Goal state after:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ {t | t.Finite ∧ t ⊆ s} ⊆ 𝒫 closure[inst✝] s
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s K : Set α
hKs : K ∈ 𝒫 closure[inst✝] s
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
ht₁ : K ⊆ ⋃₀ u
ht₂ : ∀ U ∈ u, (K ∩ U).Nonempty
U : ↑u
⊢ (↑U ∩ s).Nonempty

Tactic:
obtain ⟨x, hxK, hxV⟩ := ht₂ U U.prop

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s K : Set α
hKs : K ∈ 𝒫 closure[inst✝] s
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
ht₁ : K ⊆ ⋃₀ u
ht₂ : ∀ U ∈ u, (K ∩ U).Nonempty
U : ↑u
x : α
hxK : x ∈ K
hxV : x ∈ ↑U
⊢ (↑U ∩ s).Nonempty
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ¬ε = 0
| ⨆ i, (⨅ i_1, ↑‖a ^ (i_1 + i)‖₊ ^ (1 / ↑(i_1 + i))) * ε⁻¹

Tactic:
arg 1

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ¬ε = 0
| fun i ↦ (⨅ i_1, ↑‖a ^ (i_1 + i)‖₊ ^ (1 / ↑(i_1 + i))) * ε⁻¹
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
⊢ (∀ (U : Set β), IsOpen[inst✝] U → IsOpen[TopologicalSpace.vietoris α] {a | f '' a ⊆ U}) ∧
    ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[TopologicalSpace.vietoris α] {a | f '' a ⊆ F}

Tactic:
image_subset_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
⊢ (∀ (U : Set β), IsOpen[inst✝] U → IsOpen[TopologicalSpace.vietoris α] {a | a ⊆ f ⁻¹' U}) ∧
    ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[TopologicalSpace.vietoris α] {a | a ⊆ f ⁻¹' F}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
h : s ⤳ t
x : α
hx : x ∈ s
⊢ ∃ y ∈ t, x ⤳ y

pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x✝ : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst✝] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst✝] s
⊢ s ⤳ t

Tactic:
· obtain ⟨y, hyt, hxy⟩ := h.mem_closed (s := {u | (u ∩ closure {x}).Nonempty})
      (isClosed_inter_nonempty_of_isClosed isClosed_closure) ⟨x, hx, subset_closure rfl⟩
    exact ⟨y, hyt, specializes_iff_mem_closure.mpr hxy⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x✝ : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst✝] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst✝] s
⊢ s ⤳ t
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: F : Type u_1
A : Type u_2
inst✝¹ : CStarAlgebra A
inst✝ : FunLike F A ℂ
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
hsa : ∀ (s : ↥(selfAdjoint A)), (φ ↑s)⋆ = φ ↑s
⊢ φ a⋆ = (φ a)⋆

Tactic:
rw [← realPart_add_I_smul_imaginaryPart a]

Goal state after:
F : Type u_1
A : Type u_2
inst✝¹ : CStarAlgebra A
inst✝ : FunLike F A ℂ
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
hsa : ∀ (s : ↥(selfAdjoint A)), (φ ↑s)⋆ = φ ↑s
⊢ φ (↑(ℜ a) + I • ↑(ℑ a))⋆ = (φ (↑(ℜ a) + I • ↑(ℑ a)))⋆
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
x : α
hx₁ : x ∈ K₁
hx₂ : x ∉ K₂
U V : Set α
hU : IsOpen[inst✝³] U
hV : IsOpen[inst✝³] V
hU' : ↑K₂ ⊆ U
hV' : x ∈ V
hUV : Disjoint U V
⊢ Disjoint {K | (↑K ∩ V).Nonempty} {K | ↑K ⊆ U}

Tactic:
by grind [Set.Nonempty]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
U : Set α
hU : U ∈ {U | IsOpen[inst✝³] U}
K : Compacts α
hK : K ∈ (fun a ↦ {a_1 | ↑a_1 ⊆ a}) U
V W : Set α
hV : IsOpen[inst✝³] V
hW : IsOpen[inst✝³] W
hKV : ↑K ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ Disjoint {K | (↑K ∩ W).Nonempty} {K | ↑K ⊆ V}

Tactic:
by grind [Set.Nonempty]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : RegularSpace α
U : Set α
hU : U ∈ {U | IsOpen[inst✝³] U}
K : Compacts α
x : α
hx₁ : x ∈ ↑K
hx₂ : x ∈ U
V W : Set α
hV : IsOpen[inst✝³] V
hW : IsOpen[inst✝³] W
hxV : {x} ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ Disjoint {K | ↑K ⊆ W} {K | (↑K ∩ V).Nonempty}

Tactic:
by grind [Set.Nonempty]

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : F
hy : y ∈ B.polar ↑m
x : E
hx : x ∈ m
r : 𝕜
hr : (B x) y ≠ 0
⊢ ‖r‖ ≤ 1 / ‖(B x) y‖

Tactic:
le_div_iff₀ (norm_pos_iff.2 hr)

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : F
hy : y ∈ B.polar ↑m
x : E
hx : x ∈ m
r : 𝕜
hr : (B x) y ≠ 0
⊢ ‖r‖ * ‖(B x) y‖ ≤ 1
Module: Mathlib.Analysis.Normed.Module.HahnBanach

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual 𝕜 ↥p
⊢ ?m.28

Tactic:
refine Module.Dual.exists_continuous_extension_of_le_seminorm p f
      (show Continuous (‖f‖₊ • (normSeminorm 𝕜 E)) from ?_) fun x => f.le_opNorm x
    exact continuous_norm.const_smul ‖f‖₊

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

Goal state before:
pp: ι : Type u_2
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : IsUniformAddGroup E
inst✝³ : IsUniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst✝ : PolynormableSpace 𝕜₂ F
hp : WithSeminorms fun p ↦ ↑p
H : ∀ (x : E) (i : { p // Continuous[inst✝⁵.toTopologicalSpace, _] ⇑p }), BddAbove (range (⇑↑i ∘ fun i ↦ (𝓕 i) x))
⊢ ∀ (k : { p // Continuous[inst✝⁵.toTopologicalSpace, _] ⇑p }) (x : E), BddAbove (range fun i ↦ ↑k ((𝓕 i) x))

Tactic:
exact fun q x ↦ H x q

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst✝²] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst✝², _] f
hfs : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 0 s
hft : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 1 (interior k)ᶜ
h'f : ∀ (x : X), { toFun := f, continuous_toFun := hf } x ∈ Icc 0 1
A : t ⊆ (interior k)ᶜ
⊢ ∃ f, EqOn (⇑f) 1 s ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
refine ⟨⟨fun x ↦ 1 - f x, by fun_prop⟩, fun x hx ↦ by simpa using hfs hx,
    fun x hx ↦ by simpa [sub_eq_zero] using (hft (A hx)).symm, ?_, fun x ↦ ?_⟩

Goal state after:
case refine_1
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst✝²] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst✝², _] f
hfs : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 0 s
hft : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 1 (interior k)ᶜ
h'f : ∀ (x : X), { toFun := f, continuous_toFun := hf } x ∈ Icc 0 1
A : t ⊆ (interior k)ᶜ
⊢ HasCompactSupport ⇑{ toFun := fun x ↦ 1 - f x, continuous_toFun := ⋯ }

case refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst✝²] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst✝², _] f
hfs : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 0 s
hft : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 1 (interior k)ᶜ
h'f : ∀ (x : X), { toFun := f, continuous_toFun := hf } x ∈ Icc 0 1
A : t ⊆ (interior k)ᶜ
x : X
⊢ { toFun := fun x ↦ 1 - f x, continuous_toFun := ⋯ } x ∈ Icc 0 1
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
ha : ¬IsUnit a
⊢ ∃ f, f a = 0

Tactic:
by
  obtain ⟨M, hM, haM⟩ := (span {a}).exists_le_maximal (span_singleton_ne_top ha)
  exact
    ⟨M.toCharacterSpace,
      M.toCharacterSpace_apply_eq_zero_of_mem
        (haM (mem_span_singleton.mpr ⟨1, (mul_one a).symm⟩))⟩

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
s : Finset ι
h : ∀ i ∈ s, IsSelfAdjoint (f i)
h0 : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
⊢ ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert j s hj ih =>
    suffices f j * ∑ i ∈ s, f i = 0 by
      simp_all [(h j (by simp)).nnnorm_add_eq_max (by cfc_tac) this]
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind)

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 ↑𝔖
x✝ : Fintype ↑𝔖 := Fintype.ofFinite ↑𝔖
⊢ comap
      (fun x ↦
        (fun s ↦ UniformFun.ofFun ((↑s).domRestrict ((toFun 𝔖) x.1)), fun s ↦
          UniformFun.ofFun ((↑s).domRestrict ((toFun 𝔖) x.2))))
      (𝓤 ((s : ↑𝔖) → ↑↑s →ᵤ β)) =
    ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}

Tactic:
PseudoEMetricSpace.uniformity_edist,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst✝¹ : PseudoEMetricSpace β
inst✝ : Finite ↑𝔖
x✝ : Fintype ↑𝔖 := Fintype.ofFinite ↑𝔖
⊢ comap
      (fun x ↦
        (fun s ↦ UniformFun.ofFun ((↑s).domRestrict ((toFun 𝔖) x.1)), fun s ↦
          UniformFun.ofFun ((↑s).domRestrict ((toFun 𝔖) x.2))))
      (⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}) =
    ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: case star_id
A : Type u_1
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : Module ℝ A
inst✝⁹ : SMulCommClass ℝ A A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace ↑s
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
f g : C(↑s, ℝ)₀
⊢ (cfcₙHomSuperset hb' hbs) (ContinuousMapZero.id s) * (cfcₙHomSuperset hc' hcs) g = 0

pp: case id
A : Type u_1
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : Module ℝ A
inst✝⁹ : SMulCommClass ℝ A A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace ↑s
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
f g : C(↑s, ℝ)₀
⊢ (cfcₙHomSuperset hb' hbs) (ContinuousMapZero.id s) * (cfcₙHomSuperset hc' hcs) g = 0

Tactic:
all_goals
      refine g.mul_nonUnitalStarAlgHom_apply_eq_zero _ _ ?_ ?_
        (cfcₙHomSuperset_continuous hc' hcs)
      all_goals simp only [star_trivial, cfcₙHomSuperset_id hb' hbs,
        cfcₙHomSuperset_id hc' hcs, mul_neg, hbc, neg_zero]

Goal state after: