mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
⊢ Monotone (lfpApprox f x)

Tactic:
intro a b h
  rw [lfpApprox, lfpApprox]
  apply sup_le_sup_left (iSup₂_mono' _)
  grind

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
h : cons a l₁ ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
generalize h' : Lists'.cons a l₁ = l₁' at h

Goal state after:
α : Type u_1
a : Lists α
l₁ l₂ l₁' : Lists' α true
h' : cons a l₁ = l₁'
h : l₁' ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
Module: Mathlib.Topology.Order.IsNormal

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
⊢ IsClosed (f ⁻¹' Iic b)

Tactic:
· have : Nonempty α := ⟨a⟩
      have : Nonempty β := ⟨b⟩
      rw [hf.preimage_Iic h (ha ▸ bddAbove_Iio)]
      exact isClosed_Iic

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : IsMax a
⊢ {a} = Ioi b

Tactic:
hb.Ioi_eq

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : IsMax a
⊢ {a} = Ici a
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case inl
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nh : ↑n₁ < ↑n₂ ∧ Ordering.lt = Ordering.lt
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
exact oadd_lt_oadd_2 h₁ nh.left

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case single_add
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : (∀ (e : Ordinal.{u_1}), f e < b) → coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f) e_1 < b
⊢ coeff b (eval b (single e x + f)) = single e x + f

Tactic:
| single_add e x f hf' hx IH =>

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝¹ : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
⊢ (match e.cmp e' with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')).repr =
    ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)

Tactic:
have ee := cmp_compares e e'

Goal state after:
case oadd
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝¹ : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
ee : (e.cmp e').Compares e e'
⊢ (match e.cmp e' with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')).repr =
    ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: n : ℕ
⊢ (fun a ↦ veblen a 0)^[n] 0 < nfp (fun x ↦ veblen x 0) 0

Tactic:
apply iterate_lt_nfp veblen_zero_strictMono

Goal state after:
n : ℕ
⊢ 0 < veblen 0 0
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (range f).rank ≤ ⨆ i, succ (f i).rank

pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ∀ (i : α), succ (f i).rank ≤ (range f).rank

Tactic:
· simpa [rank_le_iff, ← add_one_le_iff] using Ordinal.le_iSup _

Goal state after:
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ∀ (i : α), succ (f i).rank ≤ (range f).rank
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
z : ZFSet.{u}
hz : z ∈ x ∩ y
w : ZFSet.{u}
hw : w ∈ z
⊢ w ∈ x ∩ y

Tactic:
by
  rw [mem_inter] at hz ⊢
  exact ⟨hx.mem_trans hw hz.1, hy.mem_trans hw hz.2⟩

Goal state after:
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ⨆ a, Order.succ (↑a.toOrd).toPSet.rank = ⨆ a, Order.succ ↑a

Tactic:
convert! ToType.mk.symm.iSup_comp (g := fun x ↦ Order.succ x.1.toPSet.rank)

Goal state after:
case e'_3
o : Ordinal.{u_1}
x✝ : ↑(Iio o)
⊢ ↑x✝ = (↑x✝).toPSet.rank
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f g : β →ᵤ Stream'.Seq α
b : β
a : α
c : γ
b' : β
⊢ dist (f b') (g b') ≤ dist f g

Tactic:
simp only [UniformFun.dist_def]
          apply le_ciSup (f := fun b ↦ dist (f b) (g b))
          have : ∃ C, ∀ (a b : Seq α), dist a b ≤ C := by
            rw [← Metric.boundedSpace_iff]
            infer_instance
          obtain ⟨C, hC⟩ := this
          use C
          simp [upperBounds]
          grind

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 : Seq.cons (exp, coef) tl = Seq.nil
⊢ False

Tactic:
apply Seq.cons_ne_nil h

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_nonzero : exps_hd ≠ 0
hlo : ∀ b ∈ basis_tl, (log ∘ b) =o[atTop] (log ∘ basis_hd)
⊢ exps_tl.toLogFun basis_tl =o[atTop] (log ∘ basis_hd)

Tactic:
induction exps_tl generalizing basis_tl with

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f : ℝ → ℝ
h : (mk (Multiseries.cons exp coef tl) f).Trimmed
⊢ coef.Trimmed ∧ ¬coef.IsZero

Tactic:
simp only [trimmed_iff_seq_trimmed, mk_seq] at h

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f : ℝ → ℝ
h : (Multiseries.cons exp coef tl).Trimmed
⊢ coef.Trimmed ∧ ¬coef.IsZero
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: case inl
a b : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
ha' : legendreSym 2 ↑a = 1
hc : b / 2 = 0
hr : jacobiSymNat a 0 = r
⊢ jacobiSymNat a b = r

pp: case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
⊢ jacobiSymNat a b = r

Tactic:
· rw [← hr, Nat.eq_zero_of_dvd_of_div_eq_zero (Nat.dvd_of_mod_eq_zero hb) hc]

Goal state after:
case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
⊢ jacobiSymNat a b = r
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case h
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup a A.dedupKeys).getD 0 = 0
⊢ ⟨a, (List.dlookup a A.dedupKeys).getD 0⟩ ∈ A.dedupKeys ∧ (decide ¬(List.dlookup a A.dedupKeys).getD 0 = 0) = true

Tactic:
simp only [h, ← List.mem_dlookup_iff A.nodupKeys_dedupKeys, not_false_iff, Option.mem_def]

Goal state after:
case h
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup a A.dedupKeys).getD 0 = 0
⊢ List.dlookup a A.dedupKeys = some ((List.dlookup a A.dedupKeys).getD 0) ∧ decide True = true
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons.zero.nil
α : Type u
inst✝ : DecidableEq α
y x' : α
xs : List α
h₀ : (x' :: xs).Nodup
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x' → (applyId (xs.zip ys) x' = y ↔ ys[i]? = some y)
h₁ : (x' :: xs).length = [].length
⊢ applyId ((x' :: xs).zip []) x' = y ↔ [][0]? = some y

pp: case cons.zero.cons
α : Type u
inst✝ : DecidableEq α
y x' : α
xs : List α
h₀ : (x' :: xs).Nodup
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x' → (applyId (xs.zip ys) x' = y ↔ ys[i]? = some y)
head✝ : α
tail✝ : List α
h₁ : (x' :: xs).length = (head✝ :: tail✝).length
⊢ applyId ((x' :: xs).zip (head✝ :: tail✝)) x' = y ↔ (head✝ :: tail✝)[0]? = some y

Tactic:
· cases h₁

Goal state after:
case cons.zero.cons
α : Type u
inst✝ : DecidableEq α
y x' : α
xs : List α
h₀ : (x' :: xs).Nodup
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x' → (applyId (xs.zip ys) x' = y ↔ ys[i]? = some y)
head✝ : α
tail✝ : List α
h₁ : (x' :: xs).length = (head✝ :: tail✝).length
⊢ applyId ((x' :: xs).zip (head✝ :: tail✝)) x' = y ↔ (head✝ :: tail✝)[0]? = some y
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons.succ.nil
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
h₀ : (x' :: xs).Nodup
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
h₁ : (x' :: xs).length = [].length
⊢ applyId ((x' :: xs).zip []) x = y ↔ [][n✝ + 1]? = some y

pp: case cons.succ.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
h₀ : (x' :: xs).Nodup
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
head✝ : α
tail✝ : List α
h₁ : (x' :: xs).length = (head✝ :: tail✝).length
⊢ applyId ((x' :: xs).zip (head✝ :: tail✝)) x = y ↔ (head✝ :: tail✝)[n✝ + 1]? = some y

Tactic:
· cases h₁

Goal state after:
case cons.succ.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
h₀ : (x' :: xs).Nodup
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
head✝ : α
tail✝ : List α
h₁ : (x' :: xs).length = (head✝ :: tail✝).length
⊢ applyId ((x' :: xs).zip (head✝ :: tail✝)) x = y ↔ (head✝ :: tail✝)[n✝ + 1]? = some y
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
g : ↑G
⊢ (ConcreteCategory.hom (eta G)) g = 1 ↔ ∀ (H : FiniteIndexNormalSubgroup ↑G), g ∈ H

Tactic:
Subtype.ext_iff,

Goal state after:
G : GrpCat
g : ↑G
⊢ ↑((ConcreteCategory.hom (eta G)) g) = ↑1 ↔ ∀ (H : FiniteIndexNormalSubgroup ↑G), g ∈ H
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
⊢ IsOpenMap fun g ↦ g • x

Tactic:
by
  /- We have already proved the theorem around the basepoint of the orbit, in
  `smul_singleton_mem_nhds_of_sigmaCompact`. The general statement follows around an arbitrary
  point by changing basepoints. -/
  simp_rw [isOpenMap_iff_nhds_le, Filter.le_map_iff]
  intro g U hU
  have : (· • x) = (· • (g • x)) ∘ (· * g⁻¹) := by
    ext g
    simp [smul_smul]
  rw [this, image_comp, ← smul_singleton]
  apply smul_singleton_mem_nhds_of_sigmaCompact
  simpa using isOpenMap_mul_right g⁻¹ |>.image_mem_nhds hU

Goal state after:
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous[inst✝⁸, inst✝³] ⇑f
⊢ IsOpenMap ⇑f

Tactic:
let A : MulAction G H := MulAction.compHom _ f

Goal state after:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous[inst✝⁸, inst✝³] ⇑f
A : MulAction G H := MulAction.compHom H f
⊢ IsOpenMap ⇑f
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousStar E
inst✝ : ContinuousStar F
f : WithConv (E →L[R] F)
⊢ IsSelfAdjoint f ↔ ∀ (x : E), f.ofConv (star x) = star (f.ofConv x)

Tactic:
by
  simp [IsSelfAdjoint, WithConv.ext_iff, ContinuousLinearMap.ext_iff, star_eq_iff_star_eq,
    eq_comm (a := f _)]

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

Goal state before:
pp: case neg
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
A : Set X
hA : A ⊆ ↑E
h : (∀ (n : ℕ) (j : ↑(E.I n)), IsClosed[t] (A ∩ ↑(map n ↑j) '' closedBall 0 1)) ∧ IsClosed[t] (A ∩ D)
n : ℕ
x✝ : 0 < n
j : cell C n
hj : j ∉ E.I n
⊢ Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)

Tactic:
exact Or.intro_left _ ((disjoint_openCell_subcomplex_of_not_mem E hj).symm.mono_left hA)

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x z : cell C 0
h : (fun x ↦ ↑(map 0 x) ![]) x = (fun x ↦ ↑(map 0 x) ![]) z
hne : ¬x = z
⊢ ↑(map 0 x) ![] ∈ openCell 0 x ∧ ↑(map 0 x) ![] ∈ openCell 0 z

Tactic:
simp [openCell_zero_eq_singleton, h]

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

Goal state before:
pp: case refine_1
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
z : I → Bool
hz : z ∈ C
⊢ Proj J (Proj K z) ∈ π C J

Tactic:
refine ⟨z, hz, (?_ : _ = (Proj J ∘ Proj K) z)⟩

Goal state after:
case refine_1
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
z : I → Bool
hz : z ∈ C
⊢ Proj J z = (Proj J ∘ Proj K) z
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝² : (i : I) → Decidable (J i)
inst✝¹ : (i : I) → Decidable (K i)
inst✝ : (i : I) → Decidable (L i)
i : { i // J i }
⊢ Continuous fun a ↦ ↑a ↑i

Tactic:
exact (continuous_apply i.val).comp continuous_subtype_val

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

Goal state before:
pp: case inr
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne : ⟨a, ha⟩ ≠ ⟨b, hb⟩
h' : ⟨b, hb⟩ < ⟨a, ha⟩
⊢ False

Tactic:
| inr h' =>

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

Goal state before:
pp: case neg.h₁
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 := ⋯
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c.sum g = c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
⊢ (c.sum fun i a ↦ a • Products.eval (π C fun x ↦ x ∈ s) i) ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})

pp: case neg.h₂
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 := ⋯
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c.sum g = c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
⊢ (-1 • c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * b • Products.eval (π C fun x ↦ x ∈ s) a_1) ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
· apply Submodule.finsuppSum_mem
        intro m hm
        apply Submodule.smul_mem
        apply Submodule.subset_span
        refine ⟨m, ⟨?_, rfl⟩⟩
        simp only [Set.mem_ofPred_eq]
        have hmas : m.val ≤ as :=
          hc (by simpa only [Finset.mem_coe, Finsupp.mem_support_iff] using hm)
        refine le_trans hmas ?_
        cases as with
        | nil => exact (List.nil_lt_cons a []).le
        | cons b bs =>
          apply le_of_lt
          rw [List.isChain_cons_cons] at ha
          exact (List.lt_iff_lex_lt _ _).mp (List.Lex.rel ha.1)

Goal state after:
case neg.h₂
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 := ⋯
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c.sum g = c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
⊢ (-1 • c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * b • Products.eval (π C fun x ↦ x ∈ s) a_1) ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})
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
x : I → Bool
hx : x ∈ C0 C ho
⊢ Proj (fun x ↦ ord I x < o) x = x

Tactic:
ext i
  simp only [Proj, ite_eq_left_iff, not_lt]
  intro hi
  rcases hi.lt_or_eq with hi | hi
  · specialize hsC x hx.1 i
    rw [← not_imp_not] at hsC
    simp only [not_lt, Bool.not_eq_true, Order.succ_le_iff] at hsC
    exact (hsC hi).symm
  · simp only [C0, Set.mem_inter_iff, Set.mem_ofPred_eq] at hx
    rw [eq_comm, ord_term ho] at hi
    rw [← hx.2, hi]

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

Goal state before:
pp: case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun x ↦ ord I x < o) l
hslt : ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o
he :
  eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
hlt : ∀ i ∈ ↑l, ord I i < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)
⊢ (πs' C ⋯) (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l) ∈
    Submodule.span ℤ
      (⇑(πs' C ⋯) '' eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})

Tactic:
Submodule.apply_mem_span_image_iff_mem_span (injective_πs' C _)

Goal state after:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun x ↦ ord I x < o) l
hslt : ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o
he :
  eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
hlt : ∀ i ∈ ↑l, ord I i < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)
⊢ eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case neg
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
l : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
he :
  Products.eval (π C fun x ↦ ord I x < o) l ∈ Submodule.span ℤ (Products.eval (π C fun x ↦ ord I x < o) '' {m | m < l})
h' : ∀ i ∈ ↑l, ord I i ≤ o
hh' : ∀ a ∈ ↑l, ord I a < o
⊢ Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})

Tactic:
rwa [Products.eval_πs_image C hh', ← Products.eval_πs C hh',
        Submodule.apply_mem_span_image_iff_mem_span (injective_πs _ _)]

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

Goal state before:
pp: case refine_2
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
l : Products I
h : Products.isGood (π C fun x ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l
hh : Products.isGood (π C fun x ↦ ord I x < o) l
⊢ Products.isGood C l

Tactic:
have := Products.isGood_mono C (Order.lt_succ o).le hh

Goal state after:
case refine_2
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
l : Products I
h : Products.isGood (π C fun x ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l
hh : Products.isGood (π C fun x ↦ ord I x < o) l
this : Products.isGood (π C fun x ↦ ord I x < Order.succ o) l
⊢ Products.isGood C l
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
x : X
xD : x ∈ D
⊢ ∃ i x_1,
    ‖x_1‖ ≤ 1 ∧
      ↑(match 0, i with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          x_1 =
        x

Tactic:
simpa [-Matrix.zero_empty]

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

Goal state before:
pp: case neg
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
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this✝ : Inhabited I
a : I
ha : a ∈ ↑q
hM : ¬↑(↑l).Tail = []
this : List.IsChain (fun x1 x2 ↦ x1 > x2) ↑↑l
⊢ (↑(↑l).Tail).head! < term I ho

Tactic:
max_eq_o_cons_tail C hsC ho l,

Goal state after:
case neg
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
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this✝ : Inhabited I
a : I
ha : a ∈ ↑q
hM : ¬↑(↑l).Tail = []
this : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑(↑l).Tail)
⊢ (↑(↑l).Tail).head! < term I ho
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: case refine_1
E : Type u_2
inst✝ : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hBA : B ⊆ A
hB : B.Infinite
f : ℕ ↪ ↑B := Set.Infinite.natEmbedding B hB
x : ℕ → E := Subtype.val ∘ ⇑f
hx_inj : Function.Injective x
a : E
haA : a ∈ A
hac : MapClusterPt a atTop x
⊢ map x atTop ≤ 𝓟 {a}ᶜ

Tactic:
exact tendsto_principal.mpr <| Nat.cofinite_eq_atTop ▸
      ((Set.finite_singleton a).preimage hx_inj.injOn).compl_mem_cofinite

Goal state after: