mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
⊢ ↑(mk (PSet.mk (Shrink.{u, u + 1} ↑s) fun x ↦ Quotient.out ↑((equivShrink ↑s).symm x))) = s

Tactic:
by
  ext x
  rw [SetLike.mem_coe, ← mk_out x, mk_mem_iff, mk_out]
  refine ⟨?_, fun xs ↦ ⟨equivShrink s (Subtype.mk x xs), ?_⟩⟩
  · rintro ⟨b, h2⟩
    rw [← ZFSet.eq, ZFSet.mk_out] at h2
    simp [h2]
  · simp [PSet.Equiv.refl]

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

Goal state before:
pp: x a₁✝ : ZFSet.{u}
⊢ ∀ ⦃a₂ : ZFSet.{u}⦄, (fun x ↦ ⟨↑x, ⋯⟩) a₁✝ = (fun x ↦ ⟨↑x, ⋯⟩) a₂ → a₁✝ = a₂

Tactic:
_

Goal state after:
x a₁✝ a₂✝ : ZFSet.{u}
⊢ (fun x ↦ ⟨↑x, ⋯⟩) a₁✝ = (fun x ↦ ⟨↑x, ⋯⟩) a₂✝ → a₁✝ = a₂✝
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
o : Ordinal.{u}
h : o < x.rank
⊢ lift.{u + 1, u} o < ⨆ i, succ (lift.{u + 1, u} (↑i).rank)

Tactic:
simpa [Ordinal.lt_iSup_iff] using lt_rank_iff.1 h

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

Goal state before:
pp: case refine_1.inl
y : ZFSet.{u_1}
h : y.IsOrdinal
hy : y ∈ insert y y
⊢ y ⊆ insert y y

Tactic:
simp_all [subset_def]

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

Goal state before:
pp: case refine_1.inr
x : ZFSet.{u_1}
h : x.IsOrdinal
y : ZFSet.{u_1}
hy✝ : y ∈ insert x x
hy : y ∈ x
⊢ x ⊆ insert x x

Tactic:
simp_all [subset_def]

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

Goal state before:
pp: case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m
⊢ e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m

Tactic:
· revert p
      rcases h' : split' a with ⟨a', m'⟩
      have := h.fst
      have := h.snd
      simp only [split_eq_scale_split' h', and_imp]
      have : 1 + (e - 1) = e := by
        refine repr_inj.1 ?_
        simp only [repr_add, repr_one, Nat.cast_one, repr_sub]
        have := mt repr_inj.1 e0
        exact Ordinal.add_sub_cancel_of_le <| one_le_iff_ne_zero.2 this
      intros
      subst o' m
      simp [scale, this]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
a : A
lit : ℕ
h : IsInt a (Int.negOfNat lit)
⊢ a = (algebraMap R A) ((Int.negOfNat lit).rawCast + 0) + 0

Tactic:
simp [h.out]

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
a : A
lit : ℕ
h : IsNat a lit
⊢ a = (algebraMap R A) (↑lit + 0) + 0

Tactic:
simp [h.out]

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

Goal state before:
pp: case succ.zero
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
m : ℕ
⊢ (match 0, m + 1 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m).NF

Tactic:
exact NF.oadd_zero _ _

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

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

Tactic:
simp [R', opowAux]

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

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

Tactic:
simp [R', opowAux]

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

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹
⊢ (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head

Tactic:
obtain (⟨hx, hy⟩ | ⟨_, _, _, hx, hy⟩) := dist_le_half_iff.mp h

Goal state after:
case inl
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹
hx : op (Seq.cons hd x) = nil
hy : op (Seq.cons hd y) = nil
⊢ (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head

case inr
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹
w✝² : α
w✝¹ w✝ : Stream'.Seq α
hx : op (Seq.cons hd x) = Seq.cons w✝² w✝¹
hy : op (Seq.cons hd y) = Seq.cons w✝² w✝
⊢ (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons.nil
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
h1 : (exp1 :: m1).length = (basis_hd :: basis_tl).length
h2 : [].length = (basis_hd :: basis_tl).length
h_lt : exp1 :: m1 < []
⊢ toFun (exp1 :: m1) (basis_hd :: basis_tl) =o[atTop] toFun [] (basis_hd :: basis_tl)

Tactic:
simp at h2

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

Goal state before:
pp: x y r : ℕ
hr : y * y + r = x
hle : r.ble (2 * y) = true
⊢ x.sqrt = y

Tactic:
rw [← hr, ← pow_two]

Goal state after:
x y r : ℕ
hr : y * y + r = x
hle : r.ble (2 * y) = true
⊢ (y ^ 2 + r).sqrt = y
Module: Mathlib.Tactic.Sat.FromLRAT

Goal state before:
pp: case inl
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
h : c ∈ f₁
⊢ False

pp: case inr
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
h : c ∈ f₂
⊢ False

Tactic:
· exact hn <| Or.inl <| h₁.1 fun Hc ↦ hn' <| Hc.1 _ h

Goal state after:
case inr
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
h : c ∈ f₂
⊢ False
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hs : Icc (m + 1) (n - 1) = s
⊢ Ioo m n = s

Tactic:
by
  rw [← hs, ← Icc_add_one_sub_one_eq_Ioo]

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

Goal state before:
pp: m n : ℤ
s : Finset ℤ
hs : Icc (m + 1) (n - 1) = s
⊢ Ioo m n = s

Tactic:
by
  rw [← hs, ← Icc_add_one_sub_one_eq_Ioo]

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 → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : X → Set X := fun x ↦ {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
⊢ Prod.map F F ⁻¹' UniformFun.gen X α U ∈ ⨅ i, comap (fun x ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α)

Tactic:
have : (⋂ a ∈ A, {ij : ι × ι | (F ij.1 a, F ij.2 a) ∈ V}) ⊆
      (Prod.map F F) ⁻¹' UniformFun.gen X α U := by
    -- Given `(i, j) ∈ ⋂ a ∈ A, 𝐒(V, a)` and `x : X`, we have to prove that `(F i x, F j x) ∈ U`.
    rintro ⟨i, j⟩ hij x
    rw [mem_iInter₂] at hij
    -- We know that `x ∈ Ω a` for some `a ∈ A`, so that both `(F i x, F i a)` and `(F j a, F j x)`
    -- are in `V`.
    rcases mem_iUnion₂.mp (Acover.symm.subset <| mem_univ x) with ⟨a, ha, hax⟩
    -- Since `(i, j) ∈ 𝐒(V, a)` we also have `(F i a, F j a) ∈ V`, and finally we get
    -- `(F i x, F j x) ∈ V ○ V ○ V ⊆ U`.
    exact hVU <| SetRel.prodMk_mem_comp (SetRel.prodMk_mem_comp (SetRel.symm V <| hax i) (hij a ha))
      (hax j)

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : X → Set X := fun x ↦ {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
this : ⋂ a ∈ A, {ij | (F ij.1 a, F ij.2 a) ∈ V} ⊆ Prod.map F F ⁻¹' UniformFun.gen X α U
⊢ Prod.map F F ⁻¹' UniformFun.gen X α U ∈ ⨅ i, comap (fun x ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α)
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
⊢ eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map (lift f) = f

Tactic:
let e := isoLimittoFiniteQuotientFunctor P

Goal state after:
G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
e : P ≅ limit P.diagram := P.isoLimittoFiniteQuotientFunctor
⊢ eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map (lift f) = f
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst✝⁸ : Monoid M
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid E'
inst✝⁴ : AddCommMonoid F
inst✝³ : Module S E
inst✝² : Module S E'
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : E →ₗ[S] E' →ₗ[S] F
f : M → E'
⊢ 0 ⋆[L] f = 0

Tactic:
by
  ext; simp [convolution]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst✝⁸ : Monoid M
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid E'
inst✝⁴ : AddCommMonoid F
inst✝³ : Module S E
inst✝² : Module S E'
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : E →ₗ[S] E' →ₗ[S] F
f : M → E
⊢ f ⋆[L] 0 = 0

Tactic:
by
  ext; simp [convolution]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
inst✝⁴ : CommMonoid M
inst✝³ : CommSemiring S
inst✝² : AddCommMonoid E
inst✝¹ : Module S E
inst✝ : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL : ∀ (x y : E), (L x) y = (L y) x
x : M
⊢ ∑' (ab : ↑(mulFiber x)), (L (f (↑ab).1)) (g (↑ab).2) = ∑' (ab : ↑(mulFiber x)), (L (g (↑ab).1)) (f (↑ab).2)

Tactic:
rw [← (mulFiber_swapEquiv x).tsum_eq]

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
inst✝⁴ : CommMonoid M
inst✝³ : CommSemiring S
inst✝² : AddCommMonoid E
inst✝¹ : Module S E
inst✝ : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL : ∀ (x y : E), (L x) y = (L y) x
x : M
⊢ ∑' (c : ↑(mulFiber x)), (L (f (↑((mulFiber_swapEquiv x) c)).1)) (g (↑((mulFiber_swapEquiv x) c)).2) =
    ∑' (ab : ↑(mulFiber x)), (L (g (↑ab).1)) (f (↑ab).2)
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
c : 𝕜₁
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
c_ne : c ≠ 0
cV_mem : c • V ∈ 𝓕₂ ⊓ 𝓟 V
basis_𝓕₂ : 𝓕₂.HasBasis (fun s ↦ s ∈ 𝓕₂ ∧ Balanced 𝕜₁ s) id
W : Set E
hW : id W ∩ V ⊆ c • V
W_mem_𝓕₂ : W ∈ 𝓕₂
W_bal : Balanced 𝕜₁ W
w : E
w_in_W : w ∈ W
n : ℕ
hn : c ^ n • w ∈ V
k : ℕ
⊢ k < n → c ^ (k + 1) • w ∈ V → c ^ k • w ∈ V

Tactic:
_

Goal state after:
𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
c : 𝕜₁
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
c_ne : c ≠ 0
cV_mem : c • V ∈ 𝓕₂ ⊓ 𝓟 V
basis_𝓕₂ : 𝓕₂.HasBasis (fun s ↦ s ∈ 𝓕₂ ∧ Balanced 𝕜₁ s) id
W : Set E
hW : id W ∩ V ⊆ c • V
W_mem_𝓕₂ : W ∈ 𝓕₂
W_bal : Balanced 𝕜₁ W
w : E
w_in_W : w ∈ W
n : ℕ
hn : c ^ n • w ∈ V
k : ℕ
h✝ : k < n
⊢ c ^ (k + 1) • w ∈ V → c ^ k • w ∈ V
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : cell C n
hi : i ∈ E.I n
⊢ openCell n i ⊆ ↑E

Tactic:
← E.union

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : cell C n
hi : i ∈ E.I n
⊢ openCell n i ⊆ D ∪ ⋃ n, ⋃ j, openCell n ↑j
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: case a
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ ↑E ⊆ D ∪ ⋃ n, ⋃ j, closedCell n ↑j

Tactic:
← E.union

Goal state after:
case a
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ D ∪ ⋃ n, ⋃ j, openCell n ↑j ⊆ D ∪ ⋃ n, ⋃ j, closedCell n ↑j
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
⊢ ⟨n, i⟩ ∈ univ →
    ∀ ⦃y : (n : ℕ) × ↑(E.I n)⦄,
      y ∈ univ → ⟨n, i⟩ ≠ y → Function.onFun Disjoint (fun ni ↦ ↑(map ni.fst ↑ni.snd) '' ball 0 1) ⟨n, i⟩ y

Tactic:
_

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
a✝ : ⟨n, i⟩ ∈ univ
⊢ ∀ ⦃y : (n : ℕ) × ↑(E.I n)⦄,
    y ∈ univ → ⟨n, i⟩ ≠ y → Function.onFun Disjoint (fun ni ↦ ↑(map ni.fst ↑ni.snd) '' ball 0 1) ⟨n, i⟩ y
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
a✝ : ⟨n, i⟩ ∈ univ
m : ℕ
j : ↑(E.I m)
⊢ ⟨m, j⟩ ∈ univ → ⟨n, i⟩ ≠ ⟨m, j⟩ → Function.onFun Disjoint (fun ni ↦ ↑(map ni.fst ↑ni.snd) '' ball 0 1) ⟨n, i⟩ ⟨m, j⟩

Tactic:
_

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
a✝¹ : ⟨n, i⟩ ∈ univ
m : ℕ
j : ↑(E.I m)
a✝ : ⟨m, j⟩ ∈ univ
⊢ ⟨n, i⟩ ≠ ⟨m, j⟩ → Function.onFun Disjoint (fun ni ↦ ↑(map ni.fst ↑ni.snd) '' ball 0 1) ⟨n, i⟩ ⟨m, j⟩
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: 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 : ℕ
⊢ 0 < n → ∀ (j : cell C n), Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)

Tactic:
_

Goal state after:
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), Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: case h
X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : _root_.Finite ((n : ℕ) × cell C n)
h✝ : Nonempty ((n : ℕ) × cell C n)
x✝ : Fintype ((n : ℕ) × cell C n)
A : Finset ℕ := Finset.image Sigma.fst Finset.univ
m : ℕ
⊢ A.max' ⋯ + 1 ≤ m → IsEmpty (cell C m)

Tactic:
_

Goal state after:
case h
X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : _root_.Finite ((n : ℕ) × cell C n)
h✝ : Nonempty ((n : ℕ) × cell C n)
x✝ : Fintype ((n : ℕ) × cell C n)
A : Finset ℕ := Finset.image Sigma.fst Finset.univ
m : ℕ
a✝ : A.max' ⋯ + 1 ≤ m
⊢ IsEmpty (cell C m)
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
⊢ ↑F ≤ 𝓟 Set.univ → ∃ x ∈ Set.univ, ↑F ≤ 𝓝 x

Tactic:
_

Goal state after:
X : Compactum
F : Ultrafilter X.A
a✝ : ↑F ≤ 𝓟 Set.univ
⊢ ∃ x ∈ Set.univ, ↑F ≤ 𝓝 x
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : IsGeneratedBy X Y
f : Y → Z
x✝ : TopologicalSpace Z := TopologicalSpace.coinduced f tY
⊢ IsGeneratedBy X Z

Tactic:
refine iff_le_generatedBy.2 ?_

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : IsGeneratedBy X Y
f : Y → Z
x✝ : TopologicalSpace Z := TopologicalSpace.coinduced f tY
⊢ TopologicalSpace.coinduced f tY ≤ TopologicalSpace.generatedBy X
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ
⊢ f ∈ ⊤ → f ∈ Submodule.span ℤ (Set.range (spanFinBasis C s))

Tactic:
_

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ
a✝ : f ∈ ⊤
⊢ f ∈ Submodule.span ℤ (Set.range (spanFinBasis C s))
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case cond.inter_mem
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := ⋯
ssu : Type u_1 := ⋯
ι : fsu → ssu := ⋯
T0 : ssu := ⋯
AA : Set (Ultrafilter X.A) := ⋯
T1 : ssu := ⋯
T2 : Set (Set (Ultrafilter X.A)) := ⋯
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
⊢ ∀ ⦃s : Set (Ultrafilter X.A)⦄, s ∈ T0 → ∀ ⦃t : Set (Ultrafilter X.A)⦄, t ∈ T0 → s ∩ t ∈ T0

Tactic:
· exact claim3

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

Goal state before:
pp: case false
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ 1 y - { toFun := fun f ↦ if ↑f a = true then 1 else 0, isLocallyConstant := ⋯ } y = 0

Tactic:
Pi.one_apply,

Goal state after:
case false
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ 1 - { toFun := fun f ↦ if ↑f a = true then 1 else 0, isLocallyConstant := ⋯ } y = 0
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
x✝ : X.A
⊢ ∀ {y : X.A} (f : Ultrafilter X.A), ↑f ≤ 𝓝 x✝ → ↑f ≤ 𝓝 y → x✝ = y

Tactic:
_

Goal state after:
X : Compactum
x✝ y✝ : X.A
⊢ ∀ (f : Ultrafilter X.A), ↑f ≤ 𝓝 x✝ → ↑f ≤ 𝓝 y✝ → x✝ = y✝
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext FF

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
FF : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X✝ : Compactum
⊢ ∀ {Y : Compactum}, Function.Injective compactumToCompHaus.map

Tactic:
_

Goal state after:
X✝ Y✝ : Compactum
⊢ Function.Injective compactumToCompHaus.map
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X✝ Y✝ : Compactum
⊢ Function.Injective compactumToCompHaus.map

Tactic:
_

Goal state after:
X✝ Y✝ : Compactum
a₁✝ : X✝ ⟶ Y✝
⊢ ∀ ⦃a₂ : X✝ ⟶ Y✝⦄, compactumToCompHaus.map a₁✝ = compactumToCompHaus.map a₂ → a₁✝ = a₂
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X✝ Y✝ : Compactum
a₁✝ : X✝ ⟶ Y✝
⊢ ∀ ⦃a₂ : X✝ ⟶ Y✝⦄, compactumToCompHaus.map a₁✝ = compactumToCompHaus.map a₂ → a₁✝ = a₂

Tactic:
_

Goal state after:
X✝ Y✝ : Compactum
a₁✝ a₂✝ : X✝ ⟶ Y✝
⊢ compactumToCompHaus.map a₁✝ = compactumToCompHaus.map a₂✝ → a₁✝ = a₂✝
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝¹ : (j : I) → Decidable (J j)
inst✝ : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
x✝ : ↑(π (π C K) J)
⊢ (⇑(eval (π C J) l) ∘ ⇑(Homeomorph.setCongr ⋯)) x✝ = (eval (π (π C K) J) l) x✝

Tactic:
simp [Homeomorph.setCongr, Products.eval_eq]

Goal state after:
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
i : I
⊢ o ≤ ord I i → false = x i

Tactic:
intro hi

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
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi : o ≤ ord I i
⊢ false = x i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
hC : IsClosed C
f : LocallyConstant ↑C ℤ
⊢ f ∈ ⊤ → f ∈ Submodule.span ℤ (Set.range (Products.eval C))

Tactic:
_

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
hC : IsClosed C
f : LocallyConstant ↑C ℤ
a✝ : f ∈ ⊤
⊢ f ∈ Submodule.span ℤ (Set.range (Products.eval C))
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x ↦ false} ℤ
⊢ f ∈ ⊤ → f ∈ ℤ ∙ eval {fun x ↦ false} nil

Tactic:
_

Goal state after:
I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x ↦ false} ℤ
a✝ : f ∈ ⊤
⊢ f ∈ ℤ ∙ eval {fun x ↦ false} nil
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
c : I → Bool
hc : c ∈ C
⊢ c ∈ {fun x ↦ false}

Tactic:
by
    ext x; exact Bool.eq_false_iff.mpr (fun ht ↦ not_lt_zero (hsC c hc x ht))

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

Goal state before:
pp: case h
X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
hEC : E ⊆ C
n : ℕ
⊢ 0 < n → ∀ (j : cell C n), Disjoint E (openCell n j) ∨ IsClosed[t] (E ∩ closedCell n j)

Tactic:
_

Goal state after:
case h
X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
hEC : E ⊆ C
n : ℕ
x✝ : 0 < n
⊢ ∀ (j : cell C n), Disjoint E (openCell n j) ∨ IsClosed[t] (E ∩ closedCell n j)