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

Goal state before:
pp: b : Ordinal.{u_1}
hb : 1 < b
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ (e : Ordinal.{u_1}), f e < b
⊢ coeff b (eval b f) = f

Tactic:
induction f using Finsupp.induction_on_max with
  | zero => simp
  | single_add e x f hf' hx IH =>
    have IH' (e') : f e' < b := by
      by_cases he' : e' ∈ f.support
      · apply (hf e').trans_eq'
        rw [add_apply, single_eq_of_ne, zero_add]
        exact (hf' _ he').ne
      · rw [notMem_support_iff.1 he']
        exact hb.pos
    rw [eval_single_add' _ hf', coeff_opow_mul_add hb hx, IH IH']
    · apply (hf e).trans_eq'
      rw [add_apply, single_eq_same, notMem_support_iff.1, add_zero]
      exact fun h ↦ (hf' _ h).false
    · exact eval_lt IH' hf'

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

Goal state before:
pp: α : Type u
A : α → PSet.{u}
y : PSet.{u}
x✝ : ∃ z ∈ mk α A, y ∈ z
β : Type u
B : β → PSet.{u}
a : (mk α A).Type
e : (mk β B).Equiv (A a)
b : (mk β B).Type
yb : y.Equiv ((mk β B).Func b)
⊢ y ∈ ⋃₀ mk α A

Tactic:
by
      rw [← eta (A a)] at e
      exact
        let ⟨βt, _⟩ := e
        let ⟨c, bc⟩ := βt b
        ⟨⟨a, c⟩, yb.trans bc⟩

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

Goal state before:
pp: α : Type u
inst✝ : Small.{v, u} α
f : α → ZFSet.{v}
⊢ lift.{max u (v + 1), max u v} (lift.{u, v} (range f).card) ≤ lift.{max u (v + 1), max u v} (lift.{v, u} #α)

Tactic:
lift_lift.{v},

Goal state after:
α : Type u
inst✝ : Small.{v, u} α
f : α → ZFSet.{v}
⊢ lift.{max u (v + 1), max u v} (lift.{u, v} (range f).card) ≤ lift.{max v u (v + 1), u} #α
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
hb : (A a).Equiv (B b)
x✝ : PSet.{u}
ea : A a = x✝
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)

Tactic:
induction ea : A a with

Goal state after:
case mk
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
hb : (A a).Equiv (B b)
γ : Type u
Γ : γ → PSet.{u}
A_ih✝ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f 1 = deriv f

Tactic:
simpa using veblenWith_add_one hf 0

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

Goal state before:
pp: x : ZFSet.{u}
h : x.IsOrdinal
⊢ ∀ {a b : ↥x},
    Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) a b ∨ a = b ∨ Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) b a

Tactic:
by
    intro ⟨a, ha⟩ ⟨b, hb⟩
    simpa using mem_trichotomous (h.mem ha) (h.mem hb)

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

Goal state before:
pp: case neg.e_a.e_a
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : ¬e₂ = 0
this✝¹ : e₁.NF
this✝ : e₂.NF
this : ¬e₂.repr = repr 0
⊢ ω ∣ ω ^ e₂.repr

Tactic:
simpa using! opow_dvd_opow ω (one_le_iff_ne_zero.2 this)

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

Goal state before:
pp: e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
⊢ o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + ↑m

Tactic:
by
    by_cases e0 : e = 0 <;>
      simp only [split', e0, ↓reduceIte, Prod.mk.injEq, repr, repr_zero, opow_zero, one_mul] at p ⊢
    · rcases p with ⟨rfl, rfl⟩
      simp [h.zero_of_zero e0, NF.zero]
    · revert p
      rcases h' : split' a with ⟨a', m'⟩
      have := h.fst
      have := h.snd
      obtain ⟨IH₁, IH₂⟩ := nf_repr_split' h'
      simp only [IH₂, and_imp]
      intros
      subst o' m
      have : (ω : Ordinal.{0}) ^ repr e = ω ^ (1 : Ordinal.{0}) * ω ^ (repr e - 1) := by
        have := mt repr_inj.1 e0
        rw [← opow_add, Ordinal.add_sub_cancel_of_le (one_le_iff_ne_zero.2 this)]
      refine ⟨NF.oadd (by infer_instance) _ ?_, ?_⟩
      · simp only [opow_one, repr_sub, repr_one, Nat.cast_one] at this ⊢
        refine IH₁.below_of_lt' <| (mul_lt_mul_iff_right₀ omega0_pos).1 <|
          (le_self_add (α := Ordinal) (b := m')).trans_lt ?_
        rw [← this, ← IH₂]
        exact h.snd'.repr_lt
      · rw [this]
        simp [mul_add, mul_assoc, add_assoc]

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s t : R
h : r + s = t
⊢ (algebraMap R A) r + (algebraMap R A) s = (algebraMap R A) t

Tactic:
by
  rw [← map_add, h]

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

Goal state before:
pp: case hbc
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0✝ : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
x✝ : k + 1 ≠ 0
e0 : 0 < a0.repr
rr0 : 0 < a0.repr + a0.repr
⊢ α' * ↑m < ω ^ (a0.repr + a0.repr)

Tactic:
have : _ < ω ^ (repr a0 + repr a0) := (No.below_of_lt ?_).repr_lt

Goal state after:
case hbc.refine_2
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0✝ : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
x✝ : k + 1 ≠ 0
e0 : 0 < a0.repr
rr0 : 0 < a0.repr + a0.repr
this : (a0.oadd n a').repr < ω ^ (a0.repr + a0.repr)
⊢ α' * ↑m < ω ^ (a0.repr + a0.repr)

case hbc.refine_1
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0✝ : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
x✝ : k + 1 ≠ 0
e0 : 0 < a0.repr
rr0 : 0 < a0.repr + a0.repr
⊢ a0.repr < a0.repr + a0.repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : Majorized f b f_exp
hg : Majorized g b g_exp
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
⊢ Majorized (f * g) b (f_exp + g_exp)

Tactic:
simp only [Majorized] at *
  intro exp h_exp
  let ε := (exp - f_exp - g_exp) / 2
  specialize hf (f_exp + ε) (by dsimp [ε]; linarith)
  specialize hg (g_exp + ε) (by dsimp [ε]; linarith)
  apply (hf.mul hg).trans_eventuallyEq (g₁ := fun t ↦ b t ^ (f_exp + ε) * b t ^ (g_exp + ε))
  apply h_pos.mono
  intro t hx
  simp only [Pi.pow_apply]
  conv_rhs => rw [show exp = (f_exp + ε) + (g_exp + ε) by dsimp [ε]; ring_nf, Real.rpow_add hx]

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

Goal state before:
pp: case succ.refine_2.e_a.zero
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
h : a'.repr + ↑0 < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) (k + 1) 0).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) k 0).repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑0) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑0) + R
Rl : R < ω ^ (a0.repr * succ ↑k)
⊢ ω0 ^ ↑k * α' * ↑0 + R = (ω0 ^ ↑k * α' + R) * ↑0

Tactic:
have : R = 0 := by cases k <;> simp [R, opowAux]
      simp [this]

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ WellFormedBasis (basis_hd :: basis_tl ++ [Real.log ∘ (basis_hd :: basis_tl).getLast ⋯])

Tactic:
apply h_basis.push
  · simp [Real.tendsto_log_atTop.comp, h_basis.right]
  · intro g hg
    simpa [List.getLast_of_getLast?_eq_some hg] using Real.isLittleO_log_id_atTop.comp_tendsto <|
      Real.tendsto_log_atTop.comp <| h_basis.tendsto_atTop <| List.mem_of_getLast? hg

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

Goal state before:
pp: c : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ Majorized (fun x ↦ c) basis_hd 0

Tactic:
exact Majorized.const <| h_basis.tendsto_atTop (by simp)

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

Goal state before:
pp: basis : Basis
n : Fin (List.length basis)
r : ℝ
⊢ (monomialRpow basis (↑n) r).toFun = basis[n] ^ r

Tactic:
by
  cases basis with
  | nil => grind
  | cons basis_hd basis_tl => cases n using Fin.cases <;> simp [monomialRpow]

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

Goal state before:
pp: hd : ℝ
tl : UnitMonomial
⊢ FirstNonzeroIsPos (hd :: tl) ↔ 0 < hd ∨ hd = 0 ∧ tl.FirstNonzeroIsPos

Tactic:
grind [FirstNonzeroIsPos, sign]

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

Goal state before:
pp: b₁ b₂ b₃ : ℝ → ℝ
bs₁ bs₂ bs₃ : Basis
f₁ : ℝ → ℝ
g₁ : MultiseriesExpansion bs₁ → MultiseriesExpansion bs₂
f₂ : ℝ → ℝ
g₂ : MultiseriesExpansion bs₂ → MultiseriesExpansion bs₃
ms : Multiseries b₁ bs₁
⊢ map (f₂ ∘ f₁) (g₂ ∘ g₁) ms = map f₂ g₂ (map f₁ g₁ ms)

Tactic:
simp [map, ← Stream'.Seq.map_comp]
  rfl

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

Goal state before:
pp: coef exp : ℝ
m : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ { coef := coef, unit := exp :: m }.toFun (basis_hd :: basis_tl) =
    basis_hd ^ exp * { coef := coef, unit := m }.toFun basis_tl

Tactic:
ext x
  simp [toFun]
  ring

Goal state after:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case a
a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
⊢ a ∣ y

Tactic:
exact eq_of_mul_eq_mul_of_coprime_aux hab h

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: n : ℕ
s : Finset ℕ
hs : Icc 0 n = s
⊢ Iio (n + 1) = s

Tactic:
Iio_eq_Ico,

Goal state after:
n : ℕ
s : Finset ℕ
hs : Icc 0 n = s
⊢ Ico ⊥ (n + 1) = s
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: A : Type u_2
B : Type u_3
inst✝⁵ : Monoid A
inst✝⁴ : Monoid B
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
⊢ IsClosed (Set.range toContinuousMap)

Tactic:
simp only [range_toContinuousMap, Set.ofPred_and, Set.ofPred_forall]
    refine .inter (isClosed_singleton.preimage (continuous_eval_const 1)) <|
      isClosed_iInter fun x ↦ isClosed_iInter fun y ↦ ?_
    exact isClosed_eq (continuous_eval_const (x * y)) <|
      .mul (continuous_eval_const x) (continuous_eval_const y)

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, (OneSkeletonGraph C).IsLoopAt e x) ↔ ∃ x, cellFrontier 1 e = closedCell 0 x

Tactic:
refine exists_congr fun x ↦ ?_

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
x : cell C 0
⊢ (OneSkeletonGraph C).IsLoopAt e x ↔ cellFrontier 1 e = closedCell 0 x
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
a : Ordinal.{u}
ha : sᵈ[a] ∈ fixedPoints ⇑relDerivedSet
i : Ordinal.{u}
⊢ sᵈ[a] ⊆ sᵈ[i]

Tactic:
rcases lt_or_ge i a with hi | hi

Goal state after:
case inl
X : Type u
inst✝ : TopologicalSpace X
s : Set X
a : Ordinal.{u}
ha : sᵈ[a] ∈ fixedPoints ⇑relDerivedSet
i : Ordinal.{u}
hi : i < a
⊢ sᵈ[a] ⊆ sᵈ[i]

case inr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
a : Ordinal.{u}
ha : sᵈ[a] ∈ fixedPoints ⇑relDerivedSet
i : Ordinal.{u}
hi : a ≤ i
⊢ sᵈ[a] ⊆ sᵈ[i]
Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : Y → Z
⊢ ContinuousGeneratedBy X g ↔ Continuous (⇑WithGeneratedByTopology.equiv.symm ∘ g ∘ ⇑WithGeneratedByTopology.equiv)

Tactic:
IsGeneratedBy.equiv_symm_comp_continuous_iff,

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : Y → Z
⊢ ContinuousGeneratedBy X g ↔ Continuous[_, inst✝] (g ∘ ⇑WithGeneratedByTopology.equiv)
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}
hC : IsClosed C
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ IsClosed (C1 C ho)

Tactic:
refine hC.inter ?_
  have h : Continuous (fun (f : I → Bool) ↦ f (term I ho)) := continuous_apply (term I ho)
  exact IsClosed.preimage h (t := {true}) (isClosed_discrete _)

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
⊢ smaller C o₁ ⊆ smaller C o₂

Tactic:
rintro f ⟨g, hg, rfl⟩

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
g : LocallyConstant ↑(π C fun x ↦ ord I x < o₁) ℤ
hg : g ∈ range (π C fun x ↦ ord I x < o₁)
⊢ (πs C o₁) g ∈ smaller C o₂
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
x : X
xmem : ∃ i < n, ∃ i_1 ∈ I i, x ∈ closedCell i i_1
⊢ ∃ i, ↑i < ↑n ∧ ∃ i_1, x ∈ closedCell i i_1

Tactic:
obtain ⟨i, iltn, j, _, xmem⟩ := xmem

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j✝ : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j✝ ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
x : X
i : ℕ
iltn : i < n
j : cell C i
left✝ : j ∈ I i
xmem : x ∈ closedCell i j
⊢ ∃ i, ↑i < ↑n ∧ ∃ i_1, x ∈ closedCell i i_1
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case pos
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)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₂ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
⊢ ((if SwapTrue o (↑x) (term I ho) = true then 1 else 0) - if ↑x (term I ho) = true then 1 else 0) = 1

Tactic:
rw [if_pos (swapTrue_eq_true _ _), if_neg]
    · rfl
    · simp [mem_C'_eq_false C ho x x.prop]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
s : Set (Set X)
hsS : s ⊆ S
hsf : s.Finite
hKs : K ⊆ ⋃₀ s
hst : MapsTo (⇑f) (⋃₀ s) (⋃₀ t)
⊢ {x | MapsTo (⇑x) (⋃₀ s) (⋃₀ t)} ⊆ {g | MapsTo (⇑g) K U}

Tactic:
exact fun g hg ↦ hg.mono hKs (sUnion_subset hTU)

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
x : X
hxV : x ∈ ⇑f ⁻¹' V
⊢ ∃ U ∈ countableBasis X, x ∈ U ∧ U ⊆ ⇑f ⁻¹' V

Tactic:
by
      rw [← (isBasis_countableBasis _).mem_nhds_iff]
      exact (hVo.preimage (map_continuous f)).mem_nhds hxV

Goal state after:
Module: Mathlib.Topology.Convenient.Localization

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
⊢ (morphismPropertyWithGeneratedByTopologyEquiv X).IsInvertedBy (toContinuousGeneratedByCat X)

Tactic:
rintro _ _ _ ⟨Z⟩; infer_instance

Goal state after:
Module: Mathlib.Topology.Convenient.Localization

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
⊢ (morphismPropertyWithGeneratedByTopologyEquiv X).IsInvertedBy toGeneratedByTopCat

Tactic:
rintro _ _ _ ⟨Z⟩; infer_instance

Goal state after:
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: case refine_2
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h :
  ∀ (i₁ : ι) (f₁ : C(X i₁, Z)) (i₂ : ι) (f₂ : C(X i₂, Y)),
    Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
      match x with
      | (x₁, x₂) => g (f₂ x₂, f₁ x₁)
⊢ ContinuousGeneratedBy X g

Tactic:
· rw [continuousGeneratedBy_def]
    intro i f
    exact (h i (ContinuousMap.snd.comp f) i (ContinuousMap.fst.comp f)).comp
      (Continuous.prodMk continuous_id continuous_id)

Goal state after:
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
θ : ↑I
γ : Path x y
⊢ γ 1 = y

Tactic:
γ.target

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x y : X
θ : ↑I
γ : Path x y
⊢ y = y
Module: Mathlib.Topology.Instances.PNat

Goal state before:
pp: ⊢ (Filter.cocompact ℕ+).NeBot

Tactic:
by simp only [Filter.cocompact_eq_cofinite, Filter.cofinite_neBot]

Goal state after:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case mpr
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
⊢ y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N → y ∈ Cube.boundary (M ⊕ N)

Tactic:
· rintro (⟨m, hm⟩ | ⟨n, hn⟩)
    · exact ⟨Sum.inl m, hm⟩
    · exact ⟨Sum.inr n, hn⟩

Goal state after:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case inl
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
y : N → ↑I
j : N
Hj : y j = 0 ∨ y j = 1
p : Ω (↑(Ω^ { j_1 // j_1 ≠ j } X x)) const
⊢ (↑(p.toContinuousMap (y j)) fun j_1 ↦ y ↑j_1) = x

Tactic:
rcases Hj with Hj | Hj

Goal state after:
case inl.inl
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
y : N → ↑I
j : N
p : Ω (↑(Ω^ { j_1 // j_1 ≠ j } X x)) const
Hj : y j = 0
⊢ (↑(p.toContinuousMap (y j)) fun j_1 ↦ y ↑j_1) = x

case inl.inr
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
y : N → ↑I
j : N
p : Ω (↑(Ω^ { j_1 // j_1 ≠ j } X x)) const
Hj : y j = 1
⊢ (↑(p.toContinuousMap (y j)) fun j_1 ↦ y ↑j_1) = x
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
f : ↑(Ω^ N X x)
⊢ ⟦symmAt i f⟧ = ⟦symmAt j f⟧

Tactic:
simp_rw [← fromLoop_symm_toLoop]

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
f : ↑(Ω^ N X x)
⊢ ⟦fromLoop i (Path.symm (toLoop i f))⟧ = ⟦fromLoop j (Path.symm (toLoop j f))⟧
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C : Set Y
hC_subset : C ⊆ f '' A
hC_cover : IsCover ε (f '' A) C
x : ↑C
⊢ ∃ y ∈ A, f y = ↑x

Tactic:
simpa using hC_subset x.2

Goal state after:
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C' : Set X
hC'_subset : C' ⊆ A
hC_subset : f '' C' ⊆ f '' A
hC_cover : IsCover ε A C'
⊢ C'.encard ≤ (f '' C').encard

Tactic:
rw [InjOn.encard_image]

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C' : Set X
hC'_subset : C' ⊆ A
hC_subset : f '' C' ⊆ f '' A
hC_cover : IsCover ε A C'
⊢ InjOn f C'
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
hs : 0 < s.infsep
⊢ s.Nontrivial

Tactic:
contrapose hs

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
hs : ¬s.Nontrivial
⊢ ¬0 < s.infsep
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ closure[instTopologicalSpace] {toUpperSet b} ⊆ closure[instTopologicalSpace] {toUpperSet a} ↔ b ≤ a

Tactic:
IsUpperSet.closure_singleton,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Iic (toUpperSet b) ⊆ Iic (toUpperSet a) ↔ b ≤ a
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: h : Set Prop
hs : h ∈ {∅, {True}}
⊢ h ∈ {s | ∃ a, (Iic a)ᶜ = s}

Tactic:
simp only [compl_Iic, mem_ofPred_eq]
        rw [← Ioi_True, ← Ioi_False] at hs
        rcases hs with (rfl | rfl)
        · use True
        · use False

Goal state after:
Module: Mathlib.Topology.OmegaCompletePartialOrder

Goal state before:
pp: case h
α : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α (range fun c ↦ range ⇑c)
f : α → Prop
a b : α
hab : a ≤ b
⊢ (fun c ↦ range ⇑c) (Chain.pair a b hab) = {a, b}

Tactic:
exact OmegaCompletePartialOrder.Chain.range_pair a b hab

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
⊢ x = y

Tactic:
have : range Φ = range Ψ := by
      have hΦ : IsCompact (range Φ) := isCompact_range Φisom.continuous
      have hΨ : IsCompact (range Ψ) := isCompact_range Ψisom.continuous
      apply (IsClosed.hausdorffDist_zero_iff_eq _ _ _).1 DΦΨ.symm
      · exact hΦ.isClosed
      · exact hΨ.isClosed
      · exact hausdorffEDist_ne_top_of_nonempty_of_bounded (range_nonempty _) (range_nonempty _)
          hΦ.isBounded hΨ.isBounded

Goal state after:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
this : range Φ = range Ψ
⊢ x = y