mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := ⋯
y : MvPolynomial Bool R := ⋯
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := ⋯
⊢ ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν =
    (MvPolynomial.aeval e) ((pderiv true) ((pderiv true) ((x + y) ^ n))) * X ^ 2

pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := ⋯
y : MvPolynomial Bool R := ⋯
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := ⋯
⊢ (MvPolynomial.aeval e) ((pderiv true) ((pderiv true) ((x + y) ^ n))) * X ^ 2 = (n * (n - 1)) • X ^ 2

Tactic:
· -- We first prepare a tedious rewrite:
    have w : ∀ k : ℕ, (k * (k - 1)) • bernsteinPolynomial R n k =
        (n.choose k : R[X]) * ((1 - Polynomial.X) ^ (n - k) *
          ((k : R[X]) * ((↑(k - 1) : R[X]) * Polynomial.X ^ (k - 1 - 1)))) * Polynomial.X ^ 2 := by
      rintro (_ | _ | k)
      · simp
      · simp
      · rw [bernsteinPolynomial]
        simp only [← natCast_mul, Nat.add_succ_sub_one, add_zero, pow_succ]
        push_cast
        ring
    rw [add_pow, map_sum (pderiv true), map_sum (pderiv true), map_sum (MvPolynomial.aeval e),
      Finset.sum_mul]
    -- Step inside the sum:
    refine Finset.sum_congr rfl fun k _ => (w k).trans ?_
    simp only [x, y, e, pderiv_true_x, pderiv_true_y, smul_eq_mul, nsmul_eq_mul,
      Bool.cond_true, Bool.cond_false, add_zero, zero_add, mul_zero, mul_one,
      MvPolynomial.aeval_X,
      Derivation.leibniz_pow, Derivation.leibniz, Derivation.map_natCast, map_natCast, map_pow,
      map_mul]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := ⋯
y : MvPolynomial Bool R := ⋯
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := ⋯
⊢ (MvPolynomial.aeval e) ((pderiv true) ((pderiv true) ((x + y) ^ n))) * X ^ 2 = (n * (n - 1)) • X ^ 2
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield 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
a : A
⊢ CompactSpace ↑(σₙ R a)

Tactic:
by
    have h_cpct : CompactSpace (spectrum R a) := inferInstance
    simp only [← isCompact_iff_compactSpace, quasispectrum_eq_spectrum_union_zero] at h_cpct ⊢
    exact h_cpct |>.union isCompact_singleton

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖(x * y).ofLp.toProd.1‖ + ‖(x * y).ofLp.toProd.2‖ ≤
    ‖x.ofLp.toProd.1‖ * (‖y.ofLp.toProd.1‖ + ‖y.ofLp.toProd.2‖) +
      ‖x.ofLp.toProd.2‖ * (‖y.ofLp.toProd.1‖ + ‖y.ofLp.toProd.2‖)

Tactic:
mul_add,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖(x * y).ofLp.toProd.1‖ + ‖(x * y).ofLp.toProd.2‖ ≤
    ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.1‖ * ‖y.ofLp.toProd.2‖ +
      (‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖)
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

pp: case inr
𝕜 : 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 - φ 1 = 0
⊢ φ 1 = 1

Tactic:
· have : ∀ a, φ (a * 1) = 0 := fun a => by simp only [map_mul φ, h₂, mul_zero]
      exact False.elim (φ.prop.1 <| ContinuousLinearMap.ext <| by simpa only [mul_one] using! this)

Goal state after:
case inr
𝕜 : 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 - φ 1 = 0
⊢ φ 1 = 1
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x : α
γ : Type u_5
inst✝ : TopologicalSpace γ
i : γ → β
hf : UpperHemicontinuousAt f x
hi : IsInducing i
h_cl : IsClosed[inst✝¹] (range i)
⊢ UpperHemicontinuousAt (fun x ↦ i ⁻¹' f x) x

Tactic:
by
  simpa [upperHemicontinuousWithinAt_univ_iff] using
    hf.upperHemicontinuousWithinAt (s := Set.univ) |>.isInducing_comp hi h_cl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : α → Set β
⊢ HasOpenLowerSections f ↔ ∀ (b : β), IsOpen[inst✝] (f ⁻¹' Iic {b}ᶜ)ᶜ

Tactic:
have h (b : β) : (f ⁻¹' (Iic {b}ᶜ))ᶜ = {x | b ∈ f x} := by
    simp [Set.ext_iff, Iic, Set.mem_compl_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : α → Set β
h : ∀ (b : β), (f ⁻¹' Iic {b}ᶜ)ᶜ = {x | b ∈ f x}
⊢ HasOpenLowerSections f ↔ ∀ (b : β), IsOpen[inst✝] (f ⁻¹' Iic {b}ᶜ)ᶜ
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case e'_4
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊
hn : 0 < ↑(n + 1)
⊢ ↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1)) = (↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊) ^ (1 / ↑(n + 1))

Tactic:
Nat.cast_succ,

Goal state after:
case e'_4
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊
hn : 0 < ↑(n + 1)
⊢ ↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1)) = (↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊) ^ (1 / (↑n + 1))
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
l : Filter ↥S
a : ↥S
ha : IsUnit ↑a
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S)) l) (𝓝 ↑ha.unit⁻¹)
⊢ ∀ᶠ (a : ↥S) in l, Ring.inverse ((val S) a) ∈ ↑S

Tactic:
apply hl.mono fun x hx ↦ ?_

Goal state after:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
l : Filter ↥S
a : ↥S
ha : IsUnit ↑a
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S)) l) (𝓝 ↑ha.unit⁻¹)
x : ↥S
hx : IsUnit x
⊢ Ring.inverse ((val S) x) ∈ ↑S
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
x✝ : CompleteSpace (NonemptyCompacts α)
f : Filter α
hf : Cauchy f
K : NonemptyCompacts α
hK : Filter.map (fun x ↦ {x}) f ≤ 𝓝 K
x : α
hx : x ∈ ↑K
⊢ ∃ x, f ≤ 𝓝 x

Tactic:
exists x

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
x✝ : CompleteSpace (NonemptyCompacts α)
f : Filter α
hf : Cauchy f
K : NonemptyCompacts α
hK : Filter.map (fun x ↦ {x}) f ≤ 𝓝 K
x : α
hx : x ∈ ↑K
⊢ f ≤ 𝓝 x
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case neg
α : Type u_1
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : IsPreconnected s
t : Set α
hts : t ∈ s
ht : IsPreconnected t
hts' : t ⊆ ⋃₀ s
U V : Set α
hU : IsOpen[inst✝] U
hV : IsOpen[inst✝] V
hUV : ⋃₀ s ⊆ U ∪ V
ht' : ¬t ⊆ U ∧ ¬t ⊆ V
htU : ¬Disjoint t U
htV : ¬Disjoint t V
⊢ (⋃₀ s ∩ (U ∩ V)).Nonempty

Tactic:
not_disjoint_iff_nonempty_inter

Goal state after:
case neg
α : Type u_1
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : IsPreconnected s
t : Set α
hts : t ∈ s
ht : IsPreconnected t
hts' : t ⊆ ⋃₀ s
U V : Set α
hU : IsOpen[inst✝] U
hV : IsOpen[inst✝] V
hUV : ⋃₀ s ⊆ U ∪ V
ht' : ¬t ⊆ U ∧ ¬t ⊆ V
htU : (t ∩ U).Nonempty
htV : (t ∩ V).Nonempty
⊢ (⋃₀ s ∩ (U ∩ V)).Nonempty
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 ↑x)ᶜ

Tactic:
spectrum.subset_subalgebra

Goal state after:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁶ : NormedRing A
inst✝⁵ : CompleteSpace A
inst✝⁴ : SetLike SA A
inst✝³ : SubringClass SA A
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
⊢ σ 𝕜 x = σ 𝕜 ↑x

Tactic:
by
  suffices σ 𝕜 x \ σ 𝕜 (x : A) = ∅ by
    rw [spectrum_sUnion_connectedComponentIn, this]
    simp
  refine eq_empty_of_forall_notMem fun z hz ↦ NormedSpace.unbounded_univ 𝕜 𝕜 ?_
  obtain ⟨hz, hz'⟩ := mem_sdiff _ |>.mp hz
  have := (spectrum.isBounded (x : A)).union <|
    h.connectedComponentIn hz' ▸ spectrum_isBounded_connectedComponentIn S x hz
  simpa

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

Goal state before:
pp: r : ℝ
s : Set ℂ
hs₁ : {z | r < z.im} ⊆ s
hs₂ : s ⊆ {z | r ≤ z.im}
⊢ IsConnected s

Tactic:
by
  refine .subset_closure ?_ hs₁ (by simpa only [closure_setOfPred_lt_im] using hs₂)
  exact (convex_halfSpace_im_gt r).isConnected ⟨(r + 1) * I, by simp⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ Continuous fun p ↦ p.1 ×ˢ p.2

Tactic:
continuous_induced_rng,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ Continuous[_, TopologicalSpace.vietoris (α × β)] (SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
⊢ ∀ {ι : Type u_1} (U : ι → Set α),
    (∀ (i : ι), IsOpen[inst✝] (U i)) → ⋃ K ∈ S, ↑K ⊆ ⋃ i, U i → ∃ t, ⋃ K ∈ S, ↑K ⊆ ⋃ i ∈ t, U i

Tactic:
intro ι

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
ι : Type u_1
⊢ ∀ (U : ι → Set α), (∀ (i : ι), IsOpen[inst✝] (U i)) → ⋃ K ∈ S, ↑K ⊆ ⋃ i, U i → ∃ t, ⋃ K ∈ S, ↑K ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Analysis.LocallyConvex.Polar

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : E
hx : x ∈ s
y : F
hy : y ∈ B.polar s
⊢ ‖(B.flip y) x‖ ≤ 1

Tactic:
B.flip_apply

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : E
hx : x ∈ s
y : F
hy : y ∈ B.polar s
⊢ ‖(B x) y‖ ≤ 1
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‖ ≤ ‖(B x) y‖⁻¹

Tactic:
rw [← one_div, 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.LocallyConvex.AbsConvexOpen

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : ContinuousSMul ℝ E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s : Set E
hs : 0 ∈ s ∧ IsOpen[inst✝⁷] s ∧ AbsConvex 𝕜 s
⊢ s ∈ (gaugeSeminormFamily 𝕜 E).basisSets

Tactic:
convert! (gaugeSeminormFamily _ _).basisSets_singleton_mem ⟨s, hs⟩ one_pos

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : ContinuousSMul ℝ E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s : Set E
hs : 0 ∈ s ∧ IsOpen[inst✝⁷] s ∧ AbsConvex 𝕜 s
⊢ s = (gaugeSeminormFamily 𝕜 E ⟨s, hs⟩).ball 0 1
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a✝ : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a✝) * NormedSpace.exp (-x • star a✝) ∈ unitary A
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a✝) * NormedSpace.exp (x • star a✝) =
      NormedSpace.exp (x • star a✝) * NormedSpace.exp (-x • a✝)
a b c : A
y : ℝ
⊢ deriv (fun x ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
    NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)

Tactic:
mul_add,

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a✝ : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a✝) * NormedSpace.exp (-x • star a✝) ∈ unitary A
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a✝) * NormedSpace.exp (x • star a✝) =
      NormedSpace.exp (x • star a✝) * NormedSpace.exp (-x • a✝)
a b c : A
y : ℝ
⊢ deriv (fun x ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
    (NormedSpace.exp (y • a) * (a * c) + NormedSpace.exp (y • a) * (c * b)) * NormedSpace.exp (y • b)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ IsTopologicalBasis ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u.Nonempty ∧ u ⊆ B})

Tactic:
refine hB.compacts.isInducing isEmbedding_toCompacts.isInducing
    |>.isTopologicalBasis_of_exists_subset ?_ ?_ <;> simp_rw [forall_mem_image]
  · rintro u ⟨hu, -, huB⟩
    simp_rw [ofPred_and, ofPred_forall]
    exact .inter
      (isOpen_subsets_of_isOpen <| isOpen_sUnion fun U hU => hB.isOpen <| huB hU)
      (hu.isOpen_biInter fun U hU => isOpen_inter_nonempty_of_isOpen <| hB.isOpen <| huB hU)
  · intro u ⟨hu, huB⟩ K ⟨hK₁, hK₂⟩
    rcases eq_empty_or_nonempty u with rfl | hu'
    · absurd K.nonempty.mono hK₁; simp
    rw [exists_mem_image]
    exists u

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 : α → β
⊢ Continuous fun p ↦ p.1 ⊔ p.2

Tactic:
simp_rw [isEmbedding_toCompacts.continuous_iff, Function.comp_def, toCompacts_sup]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
⊢ Continuous fun x ↦ x.1.toCompacts ⊔ x.2.toCompacts
Module: Mathlib.Analysis.Normed.Module.RCLike.Extend

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
⊢ ‖fr.extendRCLike x‖ ≤ ‖fr‖ * ‖x‖

Tactic:
refine Module.Dual.norm_extendRCLike_le_seminorm (p := ‖fr‖₊ • normSeminorm 𝕜 F)
    fr.toLinearMap ?_ x

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
⊢ ∀ (x : F), |↑fr x| ≤ (‖fr‖₊ • normSeminorm 𝕜 F) x
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁸ : Ring k
inst✝⁷ : PartialOrder k
inst✝⁶ : IsOrderedRing k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
a b : E
r r' : k
inst✝ : PosSMulReflectLT k E
h : r < r'
⊢ (r' - r) • a < (r' - r) • b ↔ a < b

Tactic:
smul_lt_smul_iff_of_pos_left (sub_pos.2 h)

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁸ : Ring k
inst✝⁷ : PartialOrder k
inst✝⁶ : IsOrderedRing k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
a b : E
r r' : k
inst✝ : PosSMulReflectLT k E
h : r < r'
⊢ a < b ↔ a < b
Module: Mathlib.Analysis.Normed.Module.WeakDual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set (WeakDual 𝕜 E)
hb : Bornology.IsBounded s
⊢ Bornology.IsBounded (closure s)

Tactic:
obtain ⟨R, hR⟩ := (Metric.isBounded_iff_subset_closedBall (0 : StrongDual 𝕜 E)).mp hb
  exact (isBounded_closedBall 0 R).subset
    (closure_minimal (fun y hy ↦ hR (a := toStrongDual y) hy) (isClosed_closedBall 0 R))

Goal state after:
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
I : Ideal C(X, R)
x : X
⊢ x ∈ setOfIdeal I ↔ ∃ f ∈ I, f x ≠ 0

Tactic:
simp_rw [setOfIdeal, Set.mem_compl_iff, Set.mem_ofPred]; push Not; rfl

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ContinuousSqrt

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
x : 𝕜 × 𝕜
hx : 0 ≤ x.2 - x.1
hx' : ↑(re (x.2 - x.1)) = x.2 - x.1
⊢ x.2 = x.1 + ↑(√(re (x.2 - x.1)) * √(re (x.2 - x.1)))

Tactic:
Real.mul_self_sqrt,

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
x : 𝕜 × 𝕜
hx : 0 ≤ x.2 - x.1
hx' : ↑(re (x.2 - x.1)) = x.2 - x.1
⊢ x.2 = x.1 + ↑(re (x.2 - x.1))

𝕜 : Type u_1
inst✝ : RCLike 𝕜
x : 𝕜 × 𝕜
hx : 0 ≤ x.2 - x.1
hx' : ↑(re (x.2 - x.1)) = x.2 - x.1
⊢ 0 ≤ re (x.2 - x.1)
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: case h
A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
⊢ (gelfandTransform ℂ A).toRingHom (star a) = star ((gelfandTransform ℂ A).toRingHom a)

Tactic:
ext1 φ

Goal state after:
case h
A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
φ : ↑(characterSpace ℂ A)
⊢ ((gelfandTransform ℂ A).toRingHom (star a)) φ = (star ((gelfandTransform ℂ A).toRingHom a)) φ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst✝²³ : CommSemiring R
inst✝²² : StarRing R
inst✝²¹ : MetricSpace R
inst✝²⁰ : IsTopologicalSemiring R
inst✝¹⁹ : ContinuousStar R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
inst✝¹⁶ : Ring A
inst✝¹⁵ : Ring B
inst✝¹⁴ : Algebra S A
inst✝¹³ : Algebra S B
inst✝¹² : Algebra R A
inst✝¹¹ : Algebra R B
inst✝¹⁰ : IsScalarTower R S A
inst✝⁹ : IsScalarTower R S B
inst✝⁸ : StarRing A
inst✝⁷ : StarRing B
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst✝⁴ : ContinuousFunctionalCalculus R (A × B) pab
inst✝³ : ContinuousFunctionalCalculus R A pa
inst✝² : ContinuousFunctionalCalculus R B pb
inst✝¹ : ContinuousMap.UniqueHom R A
inst✝ : ContinuousMap.UniqueHom R B
f : R → R
a : A
b : B
hf : ContinuousOn f (spectrum R a ∪ spectrum R b)
hab : pab (a, b)
ha : pa a
hb : pb b
⊢ (cfc f (a, b)).2 = (cfc f a, cfc f b).2

Tactic:
let φ := StarAlgHom.snd S A B
    exact φ.map_cfc f (a, b) (by rwa [Prod.spectrum_eq]) continuous_snd hab hb

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

Goal state before:
pp: A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
r : ℝ
hr : 0 < r
ha : 0 ≤ a
⊢ ‖a ^ r‖₊ = ‖a‖₊ ^ r

Tactic:
by
  lift r to ℝ≥0 using hr.le
  rw [← nnrpow_eq_rpow, ← nnnorm_nnrpow a]
  all_goals simpa

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : CStarRing A
inst✝⁵ : NormedSpace ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a b : A
hb : IsSelfAdjoint b
ha : 0 ≤ a
⊢ ‖b * a * b‖ = ‖b * sqrt a‖ ^ 2

Tactic:
by
  simpa [hb.star_eq] using norm_mul_mul_star_self_of_nonneg b ha

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
⊢ 0 * 0 = a ↔ a = 0

Tactic:
mul_zero,

Goal state after:
A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
⊢ 0 = a ↔ a = 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝³ : CStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Nontrivial A
a : A
ha : 0 ≤ a
⊢ ‖a‖₊ ∈ spectrum ℝ≥0 a

Tactic:
have : IsSelfAdjoint a := .of_nonneg ha
  convert! NNReal.spectralRadius_mem_spectrum (a := a) ?_ (.nnreal_of_nonneg ha)
  · simp [this.spectrumRestricts.spectralRadius_eq, this.spectralRadius_eq_nnnorm]
  · exact this.spectrumRestricts.image ▸ (spectrum.nonempty a).image _

Goal state after: