mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case succ.some
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, op') => (hd, ↑op' s.tail))
              (T s.head)
n : ℕ
ih :
  ∀ {op : Stream'.Seq α → Stream'.Seq α},
    motive op → ∀ (s t : Stream'.Seq α), dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n
op : Stream'.Seq α → Stream'.Seq α
h_base : motive op
s t : Stream'.Seq α
hn : dist s t ≤ 2⁻¹ ^ (n + 1)
T : Option α → Option (α × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, op') => (hd, ↑op' s.tail))
        (T s.head)
h_head : s.head = t.head
hd : α
op' : Stream'.Seq α → Stream'.Seq α
h_next : motive op'
hT_head : T s.head = some (hd, ⟨op', h_next⟩)
hs : (op s).destruct = some (hd, op' s.tail)
ht : (op t).destruct = some (hd, op' t.tail)
⊢ dist s.tail t.tail ≤ 2⁻¹ ^ n

Tactic:
simpa [dist_eq_half_of_head h_head, pow_succ'] using hn

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : coef.Sorted
h_comp : tl.leadingExp < ↑exp
h_tl : tl.Sorted
⊢ (Multiseries.cons exp coef tl).Sorted

Tactic:
by
  cases h_tl with | seq _ h_tl_coef h_tl_tl =>
  constructor
  · simp at h_tl_coef ⊢
    grind
  · cases tl
    · exact Seq.Pairwise_cons_nil
    · exact h_tl_tl.cons_cons_of_trans (by simpa [lt_iff_lt] using h_comp)

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.IsZero
⊢ ms.seq = Multiseries.nil

Tactic:
cases h

Goal state after:
case nil
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
f✝ : ℝ → ℝ
⊢ (mk Multiseries.nil f✝).seq = Multiseries.nil
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.Trimmed
⊢ ms.seq.Trimmed

Tactic:
cases h

Goal state after:
case nil
basis_hd : ℝ → ℝ
basis_tl : Basis
f✝ : ℝ → ℝ
⊢ (mk Multiseries.nil f✝).seq.Trimmed

case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp✝ : ℝ
f✝ : ℝ → ℝ
coef✝ : MultiseriesExpansion basis_tl
h_trimmed✝ : coef✝.Trimmed
h_ne_zero✝ : ¬coef✝.IsZero
tl✝ : Multiseries basis_hd basis_tl
⊢ (mk (Multiseries.cons exp✝ coef✝ tl✝) f✝).seq.Trimmed
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.seq.Trimmed
⊢ ms.Trimmed

Tactic:
generalize hs : ms.seq = s at h

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
hs : ms.seq = s
h : s.Trimmed
⊢ ms.Trimmed
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: f basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : mk Multiseries.nil f = ms
h : ms.Approximates
⊢ f =ᶠ[atTop] 0

Tactic:
cases h

Goal state after:
case nil
f basis_hd : ℝ → ℝ
basis_tl : Basis
f✝ : ℝ → ℝ
hf✝ : f✝ =ᶠ[atTop] 0
h_ms : mk Multiseries.nil f = mk Multiseries.nil f✝
⊢ f =ᶠ[atTop] 0

case cons
f basis_hd : ℝ → ℝ
basis_tl : Basis
f✝ : ℝ → ℝ
exp✝ : ℝ
h_maj✝ : Majorized f✝ basis_hd exp✝
coef✝ : MultiseriesExpansion basis_tl
h_coef✝ : coef✝.Approximates
tl✝ : Multiseries basis_hd basis_tl
h_tl✝ : (mk tl✝ (f✝ - basis_hd ^ exp✝ * coef✝.toFun)).Approximates
h_ms : mk Multiseries.nil f = mk (Multiseries.cons exp✝ coef✝ tl✝) f✝
⊢ f =ᶠ[atTop] 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : mk (Multiseries.cons exp coef tl) f = ms
h : ms.Approximates
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates

Tactic:
cases h

Goal state after:
case nil
f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f✝ : ℝ → ℝ
hf✝ : f✝ =ᶠ[atTop] 0
h_ms : mk (Multiseries.cons exp coef tl) f = mk Multiseries.nil f✝
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates

case cons
f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f✝ : ℝ → ℝ
exp✝ : ℝ
h_maj✝ : Majorized f✝ basis_hd exp✝
coef✝ : MultiseriesExpansion basis_tl
h_coef✝ : coef✝.Approximates
tl✝ : Multiseries basis_hd basis_tl
h_tl✝ : (mk tl✝ (f✝ - basis_hd ^ exp✝ * coef✝.toFun)).Approximates
h_ms : mk (Multiseries.cons exp coef tl) f = mk (Multiseries.cons exp✝ coef✝ tl✝) f✝
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: x✝ : ONote
o : ONote := x✝
a : ONote
h : o.FundamentalSequenceProp (Sum.inl (some a))
⊢ a < o

Tactic:
rw [lt_def, h.1]

Goal state after:
x✝ : ONote
o : ONote := x✝
a : ONote
h : o.FundamentalSequenceProp (Sum.inl (some a))
⊢ a.repr < succ a.repr
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
h_even : Even d
⊢ 0 ≤ -q

Tactic:
linarith

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
xs_ih : val ∈ ys ↔ x ∈ xs
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = some val
h₅ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
this : val ∈ ys
⊢ val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs

Tactic:
tauto

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

Goal state before:
pp: case inr.mpr
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter ↑S := comap Subtype.val (map F ℱ)
hS : S.Equicontinuous
ind : IsInducing (⇑UniformFun.ofFun ∘ Subtype.val)
f_mem : f ∈ S
h𝒢ℱ : map Subtype.val 𝒢 = map F ℱ
H' : Tendsto id 𝒢 (𝓝 ⟨f, f_mem⟩)
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f))

Tactic:
rwa [ind.tendsto_nhds_iff, comp_id, ← tendsto_map'_iff, h𝒢ℱ] at H'

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

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)
H2 :
  UniformSpace.comap ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)
H3 :
  ∀ K ∈ 𝔖,
    UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α) =
      UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)
⊢ ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α) =
    UniformSpace.comap ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)

Tactic:
H2,

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)
H2 :
  UniformSpace.comap ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)
H3 :
  ∀ K ∈ 𝔖,
    UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α) =
      UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)
⊢ ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
⊢ Injective (mapToSelf xs hperm hnodup).apply

Tactic:
generalize h₀ : List.map Sigma.fst xs = xs₀

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
⊢ Injective (mapToSelf xs hperm hnodup).apply
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
⊢ xs = List.toFinmap' ((map Sigma.fst xs).zip (map Sigma.snd xs))

Tactic:
List.toFinmap'

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
⊢ xs =
    map
      (fun x ↦
        match x with
        | (a, b) => ⟨a, b⟩)
      ((map Sigma.fst xs).zip (map Sigma.snd xs))
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons
α : Type u
inst✝ : DecidableEq α
xs_hd : (_ : α) × α
xs_tl : List ((_ : α) × α)
xs_ih :
  xs_tl =
    map
      (fun x ↦
        match x with
        | (a, b) => ⟨a, b⟩)
      ((map Sigma.fst xs_tl).zip (map Sigma.snd xs_tl))
⊢ xs_tl = map (fun x ↦ ⟨x.1, x.2⟩) ((map Sigma.fst xs_tl).zip (map Sigma.snd xs_tl))

Tactic:
exact xs_ih

Goal state after:
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : CompactSpace A
V : Set (PontryaginDual A) := {ψ | Set.MapsTo (⇑ψ) Set.univ (Circle.centeredArc (π / 2))}
⊢ IsOpen {ψ | Set.MapsTo (⇑ψ) Set.univ (Circle.centeredArc (π / 2))}

Tactic:
exact isOpen_induced (ContinuousMap.isOpen_setOfPred_mapsTo isCompact_univ
      (Circle.isOpen_centeredArc (π / 2)))

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Sphere

Goal state before:
pp: n : ℕ
t : Set (ULift.{?u.17, 0} ↑(Metric.closedBall 0 1))
x✝ : IsOpen t
s : Set ↑(Metric.closedBall 0 1)
r : Set (EuclideanSpace ℝ (Fin n))
hro : IsOpen r
hrs : Subtype.val ⁻¹' r = s
hst : ULift.down ⁻¹' s = t
⊢ ∃ t,
    IsOpen t ∧
      ULift.down ⁻¹' t =
        (fun x ↦
            match x with
            | { down := ⟨p, hp⟩ } => { down := ⟨p, ⋯⟩ }) ⁻¹'
          ULift.down ⁻¹' Subtype.val ⁻¹' r

Tactic:
tauto

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Graph

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
x y z w : cell C 0
h1 : cellFrontier 1 e = {↑(map 0 x) ![]} ∪ {↑(map 0 y) ![]}
h2 : y = w ∧ x = z ∨ y = z ∧ x = w
⊢ x = z ∨ x = w

Tactic:
tauto

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
a✝ : ↑F ≤ 𝓟 Set.univ
⊢ X.str F ∈ Set.univ

Tactic:
tauto

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
⊢ ∀ A ⊆ C,
    (∀ (n : ℕ) (j : CWComplex.cell C n), IsClosed[inst✝¹] (A ∩ ↑(CWComplex.map n j) '' closedBall 0 1)) ∧
        IsClosed[inst✝¹] (A ∩ ∅) →
      IsClosed[inst✝¹] A

Tactic:
by simpa only [inter_empty, isClosed_empty, and_true] using CWComplex.closed'

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
S : Set (Ultrafilter X.A)
hS : S ∈ T2
x✝ : Ultrafilter X.A
⊢ x✝ ∈ basic Set.univ → x✝ ∈ Set.univ

Tactic:
tauto

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
⊢ cellFrontier n i ∪ openCell n i = closedCell n i

Tactic:
by
  rw [cellFrontier, openCell, closedCell, ← image_union]
  congrm map n i '' ?_
  exact sphere_union_ball

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
z : I → Bool
hz : z ∈ C
hx : ↑⟨Proj (fun x ↦ x ∈ s) z, ⋯⟩ a = true
⊢ ∃ a_1 ∈ s,
    (if Proj (fun x ↦ x ∈ s) z a_1 = true then e (π C fun x ↦ x ∈ s) a_1 else 1 - e (π C fun x ↦ x ∈ s) a_1) =
      e (π C fun x ↦ x ∈ s) a

Tactic:
refine ⟨a, ?_, if_pos hx⟩

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
z : I → Bool
hz : z ∈ C
hx : ↑⟨Proj (fun x ↦ x ∈ s) z, ⋯⟩ a = true
⊢ a ∈ s
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
⊢ ∀ (s : Set X.A), X.str F ∈ s → IsOpen s → s ∈ ↑F

Tactic:
tauto

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case mpr
X : Compactum
A : Set X.A
x✝ : X.A
⊢ (∃ u, A ∈ u ∧ ↑u ≤ 𝓝 x✝) → x✝ ∈ cl A

Tactic:
rintro ⟨F, h1, h2⟩
    exact ⟨F, h1, str_eq_of_le_nhds _ _ h2⟩

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case cons
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := s.sort fun x1 x2 ↦ x1 ≥ x2
a : I
as : List I
ih :
  (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) as).prod ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ as})
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
⊢ (if ↑x a = true then e (π C fun x ↦ x ∈ s) a else 1 - e (π C fun x ↦ x ∈ s) a) *
      (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) as).prod ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
rw [Finsupp.mem_span_image_iff_linearCombination] at ih

Goal state after:
case cons
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := s.sort fun x1 x2 ↦ x1 ≥ x2
a : I
as : List I
ih :
  ∃ l ∈ Finsupp.supported ℤ ℤ {m | ↑m ≤ as},
    (Finsupp.linearCombination ℤ (Products.eval (π C fun x ↦ x ∈ s))) l =
      (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) as).prod
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
⊢ (if ↑x a = true then e (π C fun x ↦ x ∈ s) a else 1 - e (π C fun x ↦ x ∈ s) a) *
      (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) as).prod ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u_1
inst✝ : LinearOrder I
m : List I
hm : List.IsChain (fun x1 x2 ↦ x1 > x2) m
⊢ ⟨m, hm⟩ ∈ ∅ → ⟨m, hm⟩ ∈ {m | m < nil}

Tactic:
tauto

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o : Ordinal.{u}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ ↑l
h' : ¬ord I i < o
this : eval C l = 0
⊢ eval C l ∈ Submodule.span ℤ (eval C '' {m | m < l})

Tactic:
simp [this]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o : Ordinal.{u}
hl : ∀ i ∈ ↑l, ord I i < o
f : LocallyConstant ↑C ℤ
⊢ f ∈ eval C '' {m | m < l} ↔ f ∈ ⇑(πs C o) '' eval (π C fun x ↦ ord I x < o) '' {m | m < l}

Tactic:
simp only [Set.mem_image, Set.mem_ofPred_eq, exists_exists_and_eq_and]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o : Ordinal.{u}
hl : ∀ i ∈ ↑l, ord I i < o
f : LocallyConstant ↑C ℤ
⊢ (∃ x < l, eval C x = f) ↔ ∃ a < l, (πs C o) (eval (π C fun x ↦ ord I x < o) a) = f
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x ↦ ord I x < o₂) ℤ
⊢ f ∈ eval (π C fun x ↦ ord I x < o₂) '' {m | m < l} ↔ f ∈ ⇑(πs' C h) '' eval (π C fun x ↦ ord I x < o₁) '' {m | m < l}

Tactic:
simp only [Set.mem_image, Set.mem_ofPred_eq, exists_exists_and_eq_and]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x ↦ ord I x < o₂) ℤ
⊢ (∃ x < l, eval (π C fun x ↦ ord I x < o₂) x = f) ↔ ∃ a < l, (πs' C h) (eval (π C fun x ↦ ord I x < o₁) a) = f
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
⊢ ((Linear_CC' C hsC ho) (e C (term I ho) * eval C ⟨↑l.Tail, ⋯⟩)) x =
    (eval (C' C ho) (Tail ⟨term I ho :: ↑l.Tail, hlc⟩)) x

Tactic:
simp only [Linear_CC', Linear_CC'₁, LocallyConstant.comapₗ, Linear_CC'₀, Subtype.coe_eta,
    LinearMap.sub_apply, LinearMap.coe_mk, AddHom.coe_mk, LocallyConstant.sub_apply,
    LocallyConstant.coe_comap, LocallyConstant.coe_mul, ContinuousMap.coe_mk, Function.comp_apply,
    Pi.mul_apply]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
⊢ (e C (term I ho)) (CC'₁ C hsC ho x) * (eval C l.Tail) (CC'₁ C hsC ho x) -
      (e C (term I ho)) (CC'₀ C ho x) * (eval C l.Tail) (CC'₀ C ho x) =
    (eval (C' C ho) (Tail ⟨term I ho :: ↑l.Tail, hlc⟩)) x
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case succ.zero
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
n : ℕ
j :
  match n + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝¹ : ⟨n + 1, j⟩ ∈ univ
i :
  match 0 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝ : ⟨0, i⟩ ∈ univ
ne : ⟨n + 1, j⟩ ≠ ⟨0, i⟩
⊢ Disjoint
    ((fun a ↦
        ↑(match ⟨n + 1, j⟩.fst, ⟨n + 1, j⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)
    ((fun a ↦
        ↑(match ⟨0, i⟩.fst, ⟨0, i⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)

Tactic:
tauto

Goal state after:
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X),
    (∀ (i : Fin n), IsClopen (U i)) →
      (∀ (i : Fin n), (U i).Nonempty) → Pairwise (Disjoint on U) → ⋃ i, U i = Set.univ → ↑n ≤ (f ⁻¹' {y}).encard
hy : Finite (ConnectedComponents X)
⊢ ENat.card (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard

Tactic:
cases nonempty_fintype (ConnectedComponents X)
      simp only [ENat.card_eq_coe_fintype_card]
      refine h (fun i ↦ ConnectedComponents.mk ⁻¹' {(Fintype.equivFin _).symm i}) (fun i ↦ ?_)
          (fun i ↦ ?_) (fun i j hij ↦ Disjoint.preimage _ (by simp [hij])) ?_
      · exact (isClopen_discrete _).preimage continuous_coe
      · exact (Set.singleton_nonempty _).preimage surjective_coe
      · simp [← Set.preimage_iUnion]

Goal state after:
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
hU2 : ∀ (i : Fin n), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : ⋃ i, U i = Set.univ
heq : f ⁻¹' {y} = ⋃ i, U i ∩ f ⁻¹' {y}
⊢ ∑ i, 1 ≤ ∑ᶠ (i : Fin n), (U i ∩ f ⁻¹' {y}).encard

Tactic:
· rw [finsum_eq_sum_of_fintype]
    refine Fintype.sum_mono fun i ↦ Set.one_le_encard_iff_nonempty.mpr (show y ∈ f '' (U i) from ?_)
    convert! Set.mem_univ y
    exact IsClopen.eq_univ ⟨hf₂ _ (hU1 i).1, hf₁ _ (hU1 i).2⟩ ((hU2 i).image f)

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

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : ¬(tsupport ⇑f).Nonempty
this : f = 0
⊢ ∃ x, ‖f x‖ = ‖f‖

Tactic:
simp [this]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : IsTopologicalSemiring Y
r : R
x : X
⊢ ↑((algebraMap R (LocallyConstant X Y)) r) x = ((algebraMap R C(X, Y)) r) x

Tactic:
simp [Algebra.smul_def]

Goal state after: