mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
E✝ : Type u_2
inst✝ : PseudoEMetricSpace E✝
f : α → E✝
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  (∀ (i : ℕ), 0 < i → i < n → E i ∈ s) →
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
⊢ ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E (n + 1)))

Tactic:
rw [← Icc_add_Icc (b := E n)]

Goal state after:
case neg
α : Type u_1
inst✝¹ : LinearOrder α
E✝ : Type u_2
inst✝ : PseudoEMetricSpace E✝
f : α → E✝
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  (∀ (i : ℕ), 0 < i → i < n → E i ∈ s) →
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
⊢ ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) =
    eVariationOn f (s ∩ Icc (E 0) (E n)) + eVariationOn f (s ∩ Icc (E n) (E (n + 1)))

case neg.hab
α : Type u_1
inst✝¹ : LinearOrder α
E✝ : Type u_2
inst✝ : PseudoEMetricSpace E✝
f : α → E✝
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  (∀ (i : ℕ), 0 < i → i < n → E i ∈ s) →
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
⊢ E 0 ≤ E n

case neg.hbc
α : Type u_1
inst✝¹ : LinearOrder α
E✝ : Type u_2
inst✝ : PseudoEMetricSpace E✝
f : α → E✝
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  (∀ (i : ℕ), 0 < i → i < n → E i ∈ s) →
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
⊢ E n ≤ E (n + 1)

case neg.hb
α : Type u_1
inst✝¹ : LinearOrder α
E✝ : Type u_2
inst✝ : PseudoEMetricSpace E✝
f : α → E✝
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  (∀ (i : ℕ), 0 < i → i < n → E i ∈ s) →
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
⊢ E n ∈ s
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
x y : α
hs : IsGreatest s x
ht : IsLeast t y
hxy : x ≤ y
⊢ s ∪ t = s ∪ {x, y} ∪ t

Tactic:
by grind [hs.1, ht.1]

Goal state after:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
⊢ LocallyBoundedVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s)

Tactic:
intro x y hx hy
  rw [← toDual_ofDual x, ← toDual_ofDual y, Icc_toDual, ← preimage_inter]
  apply BoundedVariationOn.ofDual (hf (ofDual y) (ofDual x) hy hx)

Goal state after:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
⊢ eVariationOn f (s ∩ Iic a) ≤ eVariationOn f (s ∩ Iio a) + edist (f a) l

Tactic:
rw [eVariationOn_eq_strictMonoOn]

Goal state after:
case refine_1
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
⊢ ⨆ p, ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i)) ≤ eVariationOn f (s ∩ Iio a) + edist (f a) l
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case h₁
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this✝¹ : u (n + 1) ≤ a
hn : u (n + 1) = a
this✝ :
  Tendsto (fun y ↦ eVariationOn f (s ∩ Iio a) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (eVariationOn f (s ∩ Iio a) + edist (f a) l))
this : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
y : α
hy : y ∈ s ∩ Ioo (u n) a
v : ℕ → α := ⋯
A :
  ∑ i ∈ Finset.range (n + 1), edist (f (u (i + 1))) (f (u i)) ≤
    ∑ i ∈ Finset.range (n + 2), edist (f (v (i + 1))) (f (v i))
⊢ ∑ x ∈ Finset.range (n + 1), edist (f (v (x + 1))) (f (v x)) ≤ eVariationOn f (s ∩ Iio a)

Tactic:
apply sum_le_of_monotoneOn_Iic

Goal state after:
case h₁.hu
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this✝¹ : u (n + 1) ≤ a
hn : u (n + 1) = a
this✝ :
  Tendsto (fun y ↦ eVariationOn f (s ∩ Iio a) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (eVariationOn f (s ∩ Iio a) + edist (f a) l))
this : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
y : α
hy : y ∈ s ∩ Ioo (u n) a
v : ℕ → α := ⋯
A :
  ∑ i ∈ Finset.range (n + 1), edist (f (u (i + 1))) (f (u i)) ≤
    ∑ i ∈ Finset.range (n + 2), edist (f (v (i + 1))) (f (v i))
⊢ MonotoneOn v (Iic (n + 1))

case us
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this✝¹ : u (n + 1) ≤ a
hn : u (n + 1) = a
this✝ :
  Tendsto (fun y ↦ eVariationOn f (s ∩ Iio a) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (eVariationOn f (s ∩ Iio a) + edist (f a) l))
this : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
y : α
hy : y ∈ s ∩ Ioo (u n) a
v : ℕ → α := ⋯
A :
  ∑ i ∈ Finset.range (n + 1), edist (f (u (i + 1))) (f (u i)) ≤
    ∑ i ∈ Finset.range (n + 2), edist (f (v (i + 1))) (f (v i))
⊢ ∀ i ≤ n + 1, v i ∈ s ∩ Iio a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

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✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (fun x ↦ (f x)⁻¹) a = (cfc f a)⁻¹ʳ

Tactic:
rw [← val_inv_cfcUnits f a hf', ← val_cfcUnits f a hf', Ring.inverse_unit]

Goal state after:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
⊢ eVariationOn g s ≤ eVariationOn f s

Tactic:
rw [eVariationOn_eq_strictMonoOn]

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
⊢ ⨆ p, ∑ i ∈ Finset.range p.fst, edist (g (↑p.snd (i + 1))) (g (↑p.snd i)) ≤ eVariationOn f s
Module: Mathlib.Topology.Algebra.StarSubalgebra

Goal state before:
pp: case mem.inr
R : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Semiring A
inst✝⁴ : StarRing A
inst✝³ : IsSemitopologicalSemiring A
inst✝² : ContinuousStar A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
x y✝ : A
hy✝ : y✝ ∈ elemental R x
P : (u : A) → u ∈ elemental R x → Prop
self : P x ⋯
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R A) r) ⋯
add : ∀ (u : A) (hu : u ∈ elemental R x) (v : A) (hv : v ∈ elemental R x), P u hu → P v hv → P (u + v) ⋯
mul : ∀ (u : A) (hu : u ∈ elemental R x) (v : A) (hv : v ∈ elemental R x), P u hu → P v hv → P (u * v) ⋯
closure :
  ∀ (s : Set A) (hs : s ⊆ ↑(elemental R x)),
    (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure[inst✝⁶] s), P v ⋯
y u : A
hu✝ : u ∈ {x} ∪ star {x}
hy : u ∈ ↑(adjoin R {x})
hu : star u = x
star_self : P u ⋯
⊢ P u ⋯

Tactic:
exact star_self

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν = 0
⊢ Polynomial.eval 0 (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) = 0

Tactic:
simp [zero_pow h]

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

Goal state before:
pp: case mp.refine_2
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((b - a)⁻¹ • X + Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
⊢ Polynomial.eval ((b - a)⁻¹ * ↑x + -(a * (b - a)⁻¹)) p = f x

Tactic:
convert! w ⟨_, _⟩

Goal state after:
case e'_3
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((b - a)⁻¹ • X + Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
⊢ x = (iccHomeoI a b h).symm ⟨(b - a)⁻¹ * ↑x + -(a * (b - a)⁻¹), ?mp.refine_2.convert_2⟩

case mp.refine_2.convert_2
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((b - a)⁻¹ • X + Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
⊢ (b - a)⁻¹ * ↑x + -(a * (b - a)⁻¹) ∈ I
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
⊢ cfcₙ (fun x ↦ -f x) a = -cfcₙ f a

Tactic:
by
  by_cases h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0
  · obtain ⟨ha, hf, h0⟩ := h
    rw [cfcₙ_apply f a, ← map_neg, cfcₙ_apply ..]
    congr
  · simp only [not_and_or] at h
    obtain (ha | hf | h0) := h
    · simp [cfcₙ_apply_of_not_predicate a ha]
    · rw [cfcₙ_apply_of_not_continuousOn a hf, cfcₙ_apply_of_not_continuousOn, neg_zero]
      exact fun hf_neg ↦ hf <| by simpa using hf_neg.fun_neg
    · rw [cfcₙ_apply_of_not_map_zero a h0, cfcₙ_apply_of_not_map_zero, neg_zero]
      exact (h0 <| neg_eq_zero.mp ·)

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
a✝ : Nontrivial A
⊢ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1‖ + ‖(mul 𝕜 A) x.toProd.2‖ = ‖x.toProd.1‖ + ‖x.toProd.2‖

Tactic:
norm_algebraMap',

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
a✝ : Nontrivial A
⊢ ‖x.toProd.1‖ + ‖(mul 𝕜 A) x.toProd.2‖ = ‖x.toProd.1‖ + ‖x.toProd.2‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
⊢ Continuous (ContinuousMap.toNNReal ∘ _root_.toContinuousMap)

Tactic:
exact ContinuousMap.continuous_postcomp _ |>.comp continuous_induced_dom

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
h0' : 0 ∈ s
⊢ _root_.toContinuousMap ⁻¹' closure (_root_.toContinuousMap '' ↑(adjoin 𝕜 {ContinuousMapZero.id s})) = Set.univ

Tactic:
← coe_toContinuousMapHom,

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
h0' : 0 ∈ s
⊢ ⇑toContinuousMapHom ⁻¹' closure (⇑toContinuousMapHom '' ↑(adjoin 𝕜 {ContinuousMapZero.id s})) = Set.univ
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ ∀ s ∈ 𝓤 α, (hausdorffEntourage s).IsRefl

Tactic:
intro (U : SetRel α α) hU

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ (hausdorffEntourage U).IsRefl
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
⊢ IsUniformInducing closure[inst✝.toTopologicalSpace]

Tactic:
by
  refine ⟨le_antisymm ?_ <| Filter.map_le_iff_le_comap.mp uniformContinuous_closure⟩
  rw [(𝓤 α).basis_sets.uniformity_hausdorff.comap _ |>.le_basis_iff
    (𝓤 α).basis_sets.uniformity_hausdorff, Function.comp_id]
  intro U hU
  obtain ⟨V : SetRel α α, hV, hVU⟩ := comp_mem_uniformity_sets hU
  refine ⟨V, hV, fun ⟨s, t⟩ ⟨hst, hts⟩ => ?_⟩
  simp only [mem_hausdorffEntourage] at *
  constructor
  · grw [subset_closure (s := s), hst, closure_subset_preimage hV t, ← hVU, SetRel.preimage_comp]
  · grw [subset_closure (s := t), hts, closure_subset_image hV s, ← hVU, SetRel.image_comp]

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

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
t : Set α
ht : TotallyBounded t
⊢ ∀ i ∈ 𝓤 α, ∃ t_1, t_1.Finite ∧ ∀ x ⊆ t, ∃ i_1, ∃ (_ : i_1 ∈ t_1), x ∈ {x | (x, i_1) ∈ hausdorffEntourage i}

Tactic:
intro (U : SetRel α α) hU

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
t : Set α
ht : TotallyBounded t
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ t_1, t_1.Finite ∧ ∀ x ⊆ t, ∃ i, ∃ (_ : i ∈ t_1), x ∈ {x | (x, i) ∈ hausdorffEntourage U}
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F₁ F₂ : Closeds α
h : Inseparable F₁ F₂
x : α
hx₁ : x ∈ F₁
⊢ ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∃ x_1 ∈ U, ∃ a, (x, a) = x_1 ∧ a ∈ ↑F₂

Tactic:
intro (U : SetRel α α) hU

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F₁ F₂ : Closeds α
h : Inseparable F₁ F₂
x : α
hx₁ : x ∈ F₁
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ x_1 ∈ U, ∃ a, (x, a) = x_1 ∧ a ∈ ↑F₂
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
⊢ ¬CompactSpace (Closeds α) ↔ ¬CompactSpace α

Tactic:
compactSpace_iff

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : NormOneClass A
φ : A →ₐ[𝕜] 𝕜
x✝¹ : ℝ
x✝ : x✝¹ ≥ 0
h : ∀ (x : A), ‖φ.toContinuousLinearMap x‖ ≤ x✝¹ * ‖x‖
⊢ 1 ≤ x✝¹

Tactic:
simpa only [coe_toContinuousLinearMap, map_one, norm_one, mul_one] using h 1

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ Dense {K | (↑K).Finite}

Tactic:
by
  simpa [dense_iff_closure_eq] using closure_finite_subsets univ

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
this : IsConnected ((σ ℂ a)ᶜ ∩ ({z | 0 ≤ z.im} ∪ {z | z.im ≤ 0}))
⊢ IsConnected (σ ℂ a)ᶜ

Tactic:
← Set.ofPred_or

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
this : IsConnected ((σ ℂ a)ᶜ ∩ {a | 0 ≤ a.im ∨ a.im ≤ 0})
⊢ IsConnected (σ ℂ a)ᶜ
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ ¬CompactSpace (Compacts α) ↔ ¬CompactSpace α

Tactic:
compactSpace_iff

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z✝ : ℂ
hf : Differentiable ℂ (expMulMulExp a b x)
z : ℂ
⊢ ‖↑(expUnitary (2 • ℑ (z • star b))) * x‖ = ‖x‖

Tactic:
CStarRing.norm_coe_unitary_mul

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z✝ : ℂ
hf : Differentiable ℂ (expMulMulExp a b x)
z : ℂ
⊢ ‖x‖ = ‖x‖
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: case e'_3
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
x : ℝ
u : ↥(unitary A) := ⟨NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a), ⋯⟩
⊢ NormedSpace.exp (x • star a) * NormedSpace.exp (-x • a) = ↑u⁻¹

Tactic:
simp_rw [u, ← Unitary.val_inv_toUnits_apply, neg_smul, ← Units.mul_eq_one_iff_eq_inv,
          Unitary.val_toUnits_apply]

Goal state after:
case e'_3
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
x : ℝ
u : ↥(unitary A) := ⟨NormedSpace.exp (x • a) * NormedSpace.exp (-x • star a), ⋯⟩
⊢ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a)) *
      (NormedSpace.exp (x • a) * NormedSpace.exp (-(x • star a))) =
    1
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: case refine_2
𝕜 : 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
⊢ ∀ (i' : ℕ), True → ∃ i, True ∧ u i ⊆ v i'

Tactic:
intro n _
      obtain ⟨m, hm⟩ := hu_basis.mem_iff.mp (isOpen_interior.mem_nhds (hu_zero n))
      exact ⟨m, trivial, hm.trans subset_absConvexHull⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ ¬CompactSpace (NonemptyCompacts α) ↔ ¬CompactSpace α

Tactic:
compactSpace_iff

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

Goal state before:
pp: case mpr
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝⁵ : Finite ι
inst✝⁴ : Field 𝕜
t𝕜 : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : T0Space 𝕜
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
x✝ : TopologicalSpace E := ⋯
⊢ Continuous[⨅ i, induced (⇑(f i)) t𝕜, t𝕜] ⇑φ → φ ∈ Submodule.span 𝕜 (Set.range f)

Tactic:
intro φ_cont
    refine mem_span_of_iInf_ker_le_ker fun x hx ↦ ?_
    simp_rw [Submodule.mem_iInf, LinearMap.mem_ker] at hx ⊢
    have : Inseparable x 0 := by
      -- Maybe missing lemmas about `Inseparable`?
      simp_rw [Inseparable, nhds_iInf, nhds_induced, hx, map_zero]
    simpa only [map_zero] using (this.map φ_cont).eq

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

Goal state before:
pp: case refine_2
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
hhomothety : ∀ (c : 𝕜), ‖(LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) c‖ = ‖x‖ * ‖c‖
coord : ↥(𝕜 ∙ x) →L[𝕜] 𝕜 := ↑(ofHomothety (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) ‖x‖ ⋯ hhomothety).symm
g : StrongDual 𝕜 E
hg : (∀ (x_1 : ↥(𝕜 ∙ x)), g ↑x_1 = (↑‖x‖ • coord) x_1) ∧ ‖g‖ = ‖↑‖x‖ • coord‖
hval : g x = ↑‖x‖
hle : ‖g x‖ ≤ ‖g‖ * ‖x‖
⊢ 1 ≤ ‖g‖

Tactic:
simp only [hval, norm_algebraMap', norm_norm] at hle

Goal state after:
case refine_2
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
hhomothety : ∀ (c : 𝕜), ‖(LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) c‖ = ‖x‖ * ‖c‖
coord : ↥(𝕜 ∙ x) →L[𝕜] 𝕜 := ↑(ofHomothety (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) ‖x‖ ⋯ hhomothety).symm
g : StrongDual 𝕜 E
hg : (∀ (x_1 : ↥(𝕜 ∙ x)), g ↑x_1 = (↑‖x‖ • coord) x_1) ∧ ‖g‖ = ‖↑‖x‖ • coord‖
hval : g x = ↑‖x‖
hle : ‖x‖ ≤ ‖g‖ * ‖x‖
⊢ 1 ≤ ‖g‖
Module: Mathlib.Analysis.LocallyConvex.Barrelled

Goal state before:
pp: ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous[inst✝¹, _] ⇑(p i)
bdd : BddAbove (range p)
⊢ LowerSemicontinuous ⇑(⨆ i, p i)

Tactic:
rw [Seminorm.coe_iSup_eq bdd]

Goal state after:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous[inst✝¹, _] ⇑(p i)
bdd : BddAbove (range p)
⊢ LowerSemicontinuous (⨆ i, ⇑(p i))
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g' : C(X, ℝ≥0)
hI' : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I
hgt' : ∀ x ∈ t, 0 < g' x
ht' : t = ∅
y : X
hy : y ∈ t
⊢ False

Tactic:
ht'

Goal state after:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g' : C(X, ℝ≥0)
hI' : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I
hgt' : ∀ x ∈ t, 0 < g' x
ht' : t = ∅
y : X
hy : y ∈ ∅
⊢ False
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCommCStarAlgebra A
ι : Type u_2
f : ι → A
s : Finset ι
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

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

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

Goal state before:
pp: 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✝¹ : T2Space A
inst✝ : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
⊢ -r • (-a)⁺ = -r • a⁻

Tactic:
posPart_neg

Goal state after:
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✝¹ : T2Space A
inst✝ : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
⊢ -r • a⁻ = -r • a⁻