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

Goal state before:
pp: case eq
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.eq
ee : Ordering.eq.Compares e₁ e₂
⊢ (match Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

pp: case gt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.gt
ee : Ordering.gt.Compares e₁ e₂
⊢ (match Ordering.gt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

Tactic:
· change e₁ = e₂ at ee
      subst e₂
      dsimp only
      cases mn : (n₁ : ℕ) - n₂ <;> dsimp only
      · by_cases en : n₁ = n₂
        · simpa [en]
        · simp only [en, ite_false]
          exact
            (Ordinal.sub_eq_zero_iff_le.2 <|
                le_of_lt <|
                  oadd_lt_oadd_2 h₁ <|
                    lt_of_le_of_ne (tsub_eq_zero_iff_le.1 mn) (mt PNat.eq en)).symm
      · simp only [Nat.succPNat, Nat.succ_eq_add_one, repr, PNat.mk_coe, ← succ_eq_add_one]
        rw [(tsub_eq_iff_eq_add_of_le <| le_of_lt <| Nat.lt_of_sub_eq_succ mn).1 mn, add_comm,
          Nat.cast_add, mul_add, add_assoc, add_sub_add_cancel]
        refine
          (Ordinal.sub_eq_of_add_eq <|
              add_of_omega0_opow_le h₂.snd'.repr_lt <| le_trans ?_ le_self_add).symm
        exact Ordinal.le_mul_left _ (Nat.cast_lt.2 <| Nat.succ_pos _)

Goal state after:
case gt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.gt
ee : Ordering.gt.Compares e₁ e₂
⊢ (match Ordering.gt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case e'_3
o : Ordinal.{u_1}
x✝ : ↑(Iio o)
⊢ ↑x✝ = (↑x✝).toPSet.rank

Tactic:
rw [rank_toPSet]

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

Goal state before:
pp: case neg
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
⊢ ((e₁ + e₂).oadd n₂ (e₁.oadd n₁ a₁ * a₂)).NFBelow (e₁.repr + b₂)

Tactic:
have := h₁.fst
      have := h₂.fst
      apply NFBelow.oadd
      · infer_instance
      · rwa [repr_add]
      · grw [repr_add, h₂.lt]

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

Goal state before:
pp: case a
o : Ordinal.{u_1}
a✝ : PSet.{u_1}
x✝ : Ordinal.{u_1}
⊢ a✝.Equiv x✝.toPSet ↔ mk x✝.toPSet = mk a✝

Tactic:
eq,

Goal state after:
case a
o : Ordinal.{u_1}
a✝ : PSet.{u_1}
x✝ : Ordinal.{u_1}
⊢ a✝.Equiv x✝.toPSet ↔ x✝.toPSet.Equiv a✝
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case limit.refine_2
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
h : ⨆ i, (V_ ↑i).card < o.card
⊢ False

Tactic:
refine (⨆ i : Set.Iio o, (V_ ↑i).card).card_ord.not_lt <|
        (Ordinal.card_le_card_vonNeumann _).trans_lt <| (cantor _).trans_le ?_

Goal state after:
case limit.refine_2
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
h : ⨆ i, (V_ ↑i).card < o.card
⊢ 2 ^ (V_ (⨆ i, (V_ ↑i).card).ord).card ≤ ⨆ i, (V_ ↑i).card
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
⊢ (match k, m 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:
cases m with

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

Goal state before:
pp: case oadd
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
· have := N₁.fst
    have := N₁.snd
    obtain ⟨a00, ad⟩ := N₁.of_dvd_omega0 (split_dvd e₁)
    have al := split_add_lt e₁
    have aa : repr (a' + ofNat m) = repr a' + m := by
      simp only [ONote.repr_ofNat, ONote.repr_add]
    rcases e₂ : split' o₂ with ⟨b', k⟩
    obtain ⟨_, r₂⟩ := nf_repr_split' e₂
    simp only [opow_def, e₁, r₁, split_eq_scale_split' e₂, opowAux2, repr]
    rcases k with - | k
    · simp [r₂, opow_mul, repr_opow_aux₁ a00 al aa, add_assoc]
    · simp [r₂, opow_add, opow_mul, mul_assoc, add_assoc, repr_one]
      rw [repr_opow_aux₁ a00 al aa, scale_opowAux]
      simp only [repr_mul, repr_scale, repr_one,
        Nat.cast_one, opow_one, opow_mul]
      rw [← mul_add, ← add_assoc ((ω : Ordinal.{0}) ^ repr a0 * (n : ℕ))]
      congr 1
      rw [← pow_succ, ← opow_natCast, ← opow_natCast]
      exact (repr_opow_aux₂ _ ad a00 al _ _).2

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

Goal state before:
pp: m : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length m = List.length basis
h_firstIsPos : m.FirstNonzeroIsPos
⊢ Tendsto (m.toFun basis) atTop atTop

Tactic:
cases m with

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

Goal state before:
pp: m : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length m = List.length basis
h_firstIsNeg : m.FirstNonzeroIsNeg
⊢ Tendsto (m.toFun basis) atTop (𝓝 0)

Tactic:
cases m with

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

Goal state before:
pp: m : UnitMonomial
basis : Basis
h_allZero : m.AllZero
⊢ Tendsto (m.toFun basis) atTop (𝓝 1)

Tactic:
cases m with

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

Goal state before:
pp: left right : Basis
t1 t2 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h2 : List.length t2.unit = List.length right
h_coef2 : t2.coef ≠ 0
h_lt : t1.unit < List.replicate (List.length left) 0 ++ t2.unit
⊢ t1.toFun (left ++ right) =o[atTop] t2.toFun right

Tactic:
by
  obtain ⟨coef2, exps2⟩ := t2
  let t2' : Monomial := ⟨coef2, List.replicate left.length 0 ++ exps2⟩
  have : t2'.toFun (left ++ right) = Monomial.toFun ⟨coef2, exps2⟩ right :=
    Monomial.zeros_append_toFun _
  rw [← this]
  apply isLittleO_of_lt_exps h_basis <;> simpa [t2']

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

Goal state before:
pp: left right : Basis
t1 t2 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h2 : List.length t2.unit = List.length right
h_coef1 : t1.coef ≠ 0
h_lt : List.replicate (List.length left) 0 ++ t2.unit < t1.unit
⊢ t2.toFun right =o[atTop] t1.toFun (left ++ right)

Tactic:
by
  obtain ⟨coef2, exps2⟩ := t2
  let t2' : Monomial := ⟨coef2, List.replicate left.length 0 ++ exps2⟩
  have : t2'.toFun (left ++ right) = Monomial.toFun ⟨coef2, exps2⟩ right :=
    Monomial.zeros_append_toFun _
  rw [← this]
  apply isLittleO_of_lt_exps h_basis <;> simpa [t2']

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: case a
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ (Nat.unpair n).1 - 1 < n

Tactic:
· obtain _ | n' := n
        · exact False.elim (h (by simp))
        · have := Nat.unpair_lt (by lia : 1 ≤ n' + 1)
          lia

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

Goal state before:
pp: case oadd.inl.none.inl.some.succ.refine_2
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
⊢ (a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat 0)).NF

Tactic:
refine fun H => H.fst.oadd _ (NF.below_of_lt' ?_ (@NF.oadd_zero _ _ (iha.2 H.fst)))

Goal state after:
case oadd.inl.none.inl.some.succ.refine_2
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ (a'.oadd i.succPNat 0).repr < ω ^ a.repr
Module: Mathlib.Tactic.NormNum.Irrational

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

Tactic:
rw [mul_comm, ← h, mul_comm]

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

Goal state before:
pp: case hb0
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ 0 < ↑d

pp: case h
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ (↑n).natAbs.Coprime (↑d).natAbs

Tactic:
· contrapose! hnd
    simp_all

Goal state after:
case h
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ (↑n).natAbs.Coprime (↑d).natAbs
Module: Mathlib.Tactic.Sat.FromLRAT

Goal state before:
pp: p : Prop
as ps as₁ : List Prop
⊢ as = as₁.reverseAux ps → (mk as).implies p ps as₁.length → p

Tactic:
induction ps generalizing as₁ with

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
ℱ : Filter ι
f : X → α
⊢ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔
    Tendsto ((⋃₀ 𝔖).domRestrict ∘ F) ℱ (𝓝 ((⋃₀ 𝔖).domRestrict f))

Tactic:
rw [← Filter.tendsto_comap_iff (g := (⋃₀ 𝔖).domRestrict), ← nhds_induced]

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
ℱ : Filter ι
f : X → α
⊢ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Tendsto F ℱ (𝓝 f)
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
⊢ (Subgroup.closure s).toSubmonoid ≤ (Submonoid.closure s).topologicalClosure

Tactic:
rw [Subgroup.closure_toSubmonoid, Submonoid.closure_le]

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
⊢ s ∪ s⁻¹ ⊆ ↑(Submonoid.closure s).topologicalClosure
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
f : E →ₛₗ[σ] F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : RingHomIsometric σ
V : Set E
V_mem : V ∈ 𝓝 0
H : IsEmbedding (V.domRestrict ⇑f)
f_injOn : InjOn (⇑f) V
x : E
hx : x ∈ f.ker
⊢ x = 0

Tactic:
obtain ⟨c, hc, c_ne : c ≠ 0⟩ := absorbent_nhds_zero (𝕜 := 𝕜₁) V_mem
    |>.eventually_nhdsNE_zero x |>.and eventually_mem_nhdsWithin |>.exists

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
f : E →ₛₗ[σ] F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : RingHomIsometric σ
V : Set E
V_mem : V ∈ 𝓝 0
H : IsEmbedding (V.domRestrict ⇑f)
f_injOn : InjOn (⇑f) V
x : E
hx : x ∈ f.ker
c : 𝕜₁
hc : c • x ∈ V
c_ne : c ≠ 0
⊢ x = 0
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
f : E →ₛₗ[σ] F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : RingHomIsometric σ
V : Set E
V_mem : V ∈ 𝓝 0
H : IsEmbedding (V.domRestrict ⇑f)
f_injOn : InjOn (⇑f) V
x : E
hx : x ∈ f.ker
c : 𝕜₁
hc : c • x ∈ V
c_ne : c ≠ 0
⊢ x = 0

Tactic:
rw [← smul_eq_zero_iff_right c_ne, ← f_injOn.eq_iff hc (mem_of_mem_nhds V_mem), map_zero,
    map_smulₛₗ, hx, smul_zero]

Goal state after:
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 ⊆ D ∪ ⋃ n, ⋃ j, openCell n ↑j

Tactic:
apply subset_union_of_subset_right

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 ⊆ ⋃ n, ⋃ j, openCell n ↑j
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty

Tactic:
apply isPreconnected_closed_iff.mp hs

Goal state after:
case pos.a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ IsClosed[inst✝¹] (derivedSet a)

case pos.a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ IsClosed[inst✝¹] (derivedSet b)

case pos.a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ U ⊆ derivedSet a ∪ derivedSet b

case pos.a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ (U ∩ derivedSet a).Nonempty

case pos.a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ (U ∩ derivedSet b).Nonempty
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 : ℕ∞
m : ℕ
hm : ↑m < n
j : cell C m
⊢ openCell m j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

Tactic:
apply subset_union_of_subset_right

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
hm : ↑m < n
j : cell C m
⊢ openCell m j ⊆ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
x✝ : x ∈ π C J
y : I → Bool
hy : y ∈ C
h : Proj J y = x
⊢ x ∈ C

Tactic:
rwa [← h, proj_eq_self]; exact (hh · y hy)

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

Goal state before:
pp: case tr
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
hm' : ∀ m_1 ≤ m, ↑m_1 < n → ∀ (j : cell C m_1), cellFrontier m_1 j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j
hm : ↑(m + 1) < n
j : cell C (m + 1)
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier (m + 1) j ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell m_1 j
l : ℕ
hl : l < m + 1
i : cell C l
x✝ : i ∈ I l
⊢ openCell l i ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j

Tactic:
apply subset_union_of_subset_right

Goal state after:
case tr
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
hm' : ∀ m_1 ≤ m, ↑m_1 < n → ∀ (j : cell C m_1), cellFrontier m_1 j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j
hm : ↑(m + 1) < n
j : cell C (m + 1)
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier (m + 1) j ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell m_1 j
l : ℕ
hl : l < m + 1
i : cell C l
x✝ : i ∈ I l
⊢ openCell l i ⊆ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j
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 := s.sort fun x1 x2 ↦ x1 ≥ x2
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
m : Products I
hm : c m ≠ 0
hmas : ↑m ≤ as
⊢ as ≤ a :: as

Tactic:
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:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ contained (π C fun x ↦ ord I x < o) o

Tactic:
intro x ⟨_, _, h⟩ j hj
  aesop (add simp Proj)

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

Tactic:
exact Or.inr ⟨h, hh⟩

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✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
l : ℕ
i : cell C l
hi : i ∈ {x | ↑l < n}
⊢ closedCell l ↑⟨i, hi⟩ ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

Tactic:
apply subset_union_of_subset_right

Goal state after:
X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
l : ℕ
i : cell C l
hi : i ∈ {x | ↑l < n}
⊢ closedCell l ↑⟨i, hi⟩ ⊆ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j
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
⊢ univ.PairwiseDisjoint fun ni ↦
    ↑(match ni.fst, ni.snd with
        | 0, i => PartialEquiv.single ![] ↑i
        | n.succ, i => PEmpty.elim i) ''
      ball 0 1

Tactic:
by
    simp_rw [PairwiseDisjoint, Set.Pairwise, Function.onFun]
    rintro ⟨_|n, j⟩ _ ⟨_|m, i⟩ _ ne
    · simp_all [Subtype.coe_injective.ne]
    · exact i.elim
    · tauto
    · exact i.elim

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Closeds (X a.fst) := ⋯
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑F := ⋯
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
this :
  ∀ (V : Set ↑F),
    (∀ (a : (i : ι) × C(X i, Y)), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsClosed[instTopologicalSpaceSubtype] V
⊢ Continuous[instTopologicalSpaceSubtype, _] ⇑WithGeneratedByTopology.equiv.symm

Tactic:
rw [continuous_iff_isClosed]

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Closeds (X a.fst) :=
  fun a ↦ { carrier := ⇑a.snd ⁻¹' F, isClosed' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑F := fun a ↦ F.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
this :
  ∀ (V : Set ↑F),
    (∀ (a : (i : ι) × C(X i, Y)), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsClosed[instTopologicalSpaceSubtype] V
⊢ ∀ (s : Set (WithGeneratedByTopology X ↑F)),
    IsClosed s → IsClosed[instTopologicalSpaceSubtype] (⇑WithGeneratedByTopology.equiv.symm ⁻¹' s)
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case pos
T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : logSizeRadius t V a c = 1
⊢ a ^ (logSizeRadius t V a c - 1) ≤ ↑(#({x ∈ V | edist t x ≤ (↑(logSizeRadius t V a c) - 1) * c}))

Tactic:
simp only [h_one, tsub_self, pow_zero, Nat.cast_one, zero_mul, nonpos_iff_eq_zero,
      Nat.one_le_cast, Finset.one_le_card]

Goal state after:
case pos
T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : logSizeRadius t V a c = 1
⊢ {x ∈ V | edist t x = 0}.Nonempty
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
⊢ edist (logSizeBallSeq J hJ a c l).point s ≤ ↑(logSizeBallSeq J hJ a c l).radius * c

Tactic:
grw [h, tsub_le_self]

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
x y : α
⊢ min (edist x y) (edist y x) ≤ {x, y}.einfsep

Tactic:
simp_rw [le_einfsep_iff, inf_le_iff, mem_insert_iff, mem_singleton_iff]

Goal state after:
α : Type u_1
inst✝ : EDist α
x y : α
⊢ ∀ (x_1 : α),
    x_1 = x ∨ x_1 = y →
      ∀ (y_1 : α), y_1 = x ∨ y_1 = y → x_1 ≠ y_1 → edist x y ≤ edist x_1 y_1 ∨ edist y x ≤ edist x_1 y_1