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

Goal state before:
pp: 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')
e' : m.natPred = 0
this : 0 + 1 = ↑m
⊢ m = 1

Tactic:
exact PNat.coe_inj.1 this.symm

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

Goal state before:
pp: 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 : m' + 1 + 1 = ↑m
⊢ m = 1

Tactic:
exact PNat.coe_inj.1 this.symm

Goal state after:
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 : m' + 1 + 1 = ↑m
⊢ m = 1
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case h_step
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_base : motive op
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop := ⋯
⊢ ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive' op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, op') => (hd, ↑op' s.tail))
              (T s.head)

Tactic:
clear h_base op

Goal state after:
case h_step
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = op' ∘ opf ∧ FriendlyOperation opf ∧ motive op'
⊢ ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive' op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, op') => (hd, ↑op' s.tail))
              (T s.head)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
this : 0 + 1 = ↑m
⊢ m = 1

Tactic:
exact PNat.coe_inj.1 this.symm

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

Goal state before:
pp: case cons.cons.cons.cons
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
h1 : (exp1 :: m1).length = (basis_hd :: basis_tl).length
m2 : List ℝ
h2 : (exp1 :: m2).length = (basis_hd :: basis_tl).length
h : List.Lex (fun x1 x2 ↦ x1 < x2) m1 m2
⊢ toFun m1 basis_tl =o[atTop] toFun m2 basis_tl

Tactic:
exact isLittleO_of_lt h_basis.tail (by simpa using h1) (by simpa using h2) h

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

Goal state before:
pp: a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
this : m' + 1 + 1 = ↑m
⊢ m = 1

Tactic:
exact PNat.coe_inj.1 this.symm

Goal state after:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
this : m' + 1 + 1 = ↑m
⊢ m = 1
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
⊢ t.inv.toFun basis =ᶠ[atTop] (t.toFun basis)⁻¹

Tactic:
simp only [toFun, inv]

Goal state after:
t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
⊢ t.coef⁻¹ • t.unit.inv.toFun basis =ᶠ[atTop] (t.coef • t.unit.toFun basis)⁻¹
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case step.left
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
h_tl : (tl_exp, tl_coef) ∈ tl.head
⊢ (exp, coef) > (tl_exp, tl_coef)

Tactic:
rw [gt_iff_lt, lt_iff_lt]

Goal state after:
case step.left
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
h_tl : (tl_exp, tl_coef) ∈ tl.head
⊢ tl_exp < exp
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: case ind
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
⊢ (S.decode n).encode = n

Tactic:
unfold S.decode
    dsimp only
    split
    next h =>
      unfold S.encode
      rw [← h, Nat.pair_unpair]
    next h =>
      unfold S.encode
      rw [ih, ih, Nat.sub_add_cancel, Nat.pair_unpair]
      · rwa [Nat.one_le_iff_ne_zero]
      · exact nat_unpair_lt_2 h
      · obtain _ | n' := n
        · exact False.elim (h (by simp))
        · have := Nat.unpair_lt (by lia : 1 ≤ n' + 1)
          lia

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

Goal state before:
pp: b : ℕ
hb : (b / 2).beq 0 = false
⊢ jacobiSymNat 0 b = 0

Tactic:
rw [jacobiSymNat, Nat.cast_zero, jacobiSym.zero_left ?_]

Goal state after:
b : ℕ
hb : (b / 2).beq 0 = false
⊢ 1 < b
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
⊢ ⨅ i ∈ 𝔖,
      UniformSpace.comap
        ((⇑{ toFun := fun x ↦ x, invFun := fun x ↦ x, left_inv := ⋯, right_inv := ⋯ } ∘
            i.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘
          F)
        (UniformFun.uniformSpace (↑i) α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)

Tactic:
Equiv.coe_fn_mk,

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
⊢ ⨅ i ∈ 𝔖,
      UniformSpace.comap (((fun x ↦ x) ∘ i.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ F)
        (UniformFun.uniformSpace (↑i) α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)
Module: Mathlib.Testing.Plausible.Functions

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

Tactic:
simp only [Sigma.eta, List.zip_cons_cons,
        List.map, List.cons_inj_right]
      exact xs_ih

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

Goal state before:
pp: X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ IsInducing ⇑(Equiv.Set.image DFunLike.coe S ⋯)

Tactic:
← IsInducing.subtypeVal.of_comp_iff,

Goal state after:
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ IsInducing (Subtype.val ∘ ⇑(Equiv.Set.image DFunLike.coe S ⋯))
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:
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.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)
⊢ IsEmbedding ⇑f

Tactic:
refine ⟨isInducing_of_restrict_nhds_zero V_mem H.isInducing, ?_⟩

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)
⊢ Function.Injective ⇑f
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 : cell C 0
⊢ cellFrontier 1 e = closedCell 0 x ∪ closedCell 0 x ↔ cellFrontier 1 e = closedCell 0 x

Tactic:
rw [union_self]

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
⊢ D ∪ ⋃ n, ⋃ j, closedCell n ↑j = ↑E

Tactic:
apply subset_antisymm

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, closedCell n ↑j ⊆ ↑E

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
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : cell C n
h : i ∉ E.I n
⊢ Disjoint (openCell n i) D ∧ ∀ (i_1 : ℕ) (i_2 : ↑(E.I i_1)), Disjoint (openCell n i) (openCell i_1 ↑i_2)

Tactic:
exact ⟨disjointBase n i , fun _ _ ↦ disjoint_openCell_of_ne (by lia)⟩

Goal state after:
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ perfectKernel s ⊆ s

Tactic:
simpa [iteratedDerivedSet_zero] using perfectKernel_subset_iteratedDerivedSet s 0

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

Goal state before:
pp: X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D : Set X✝
inst✝¹ : RelCWComplex C✝ D
X : Type u
inst✝ : TopologicalSpace X
C : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
mapsTo_iff_image_subset :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
union' : ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
⊢ ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' ball 0 1) ∅

Tactic:
by simp only [disjoint_empty, implies_true]

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 y : cell C 0
h : closedCell 0 x = closedCell 0 y
⊢ x = y

Tactic:
rw [closedCell_zero_eq_singleton, closedCell_zero_eq_singleton, singleton_eq_singleton_iff] at h

Goal state after:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x y : cell C 0
h : ↑(map 0 x) ![] = ↑(map 0 y) ![]
⊢ x = y
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 : ℕ∞
⊢ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j = D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

Tactic:
apply subset_antisymm

Goal state after:
case a
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
⊢ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

case a
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
⊢ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j
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 : ℕ
j : cell C n
m : ℕ
i : cell C m
h : ¬Disjoint (openCell n j) (openCell m i)
⊢ ⟨n, j⟩ = ⟨m, i⟩

Tactic:
by
  contrapose! h
  exact disjoint_openCell_of_ne h

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

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : ↑((iso_map C J) a) = ↑((iso_map C J) b)
i : I
hi : ¬J i
⊢ ↑a i = ↑b i

Tactic:
· rcases a with ⟨_, c, hc, rfl⟩
      rcases b with ⟨_, d, hd, rfl⟩
      simp only [Proj, if_neg hi]

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
⊢ LinearIndependent ℤ (Subtype.val ∘ Set.rangeFactorization (eval C)) ↔ LinearIndependent ℤ fun (p : ↑(range C)) ↦ ↑p

Tactic:
← equiv_toFun_eq_eval C

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
⊢ LinearIndependent ℤ (Subtype.val ∘ (equiv_range C).toFun) ↔ LinearIndependent ℤ fun (p : ↑(range C)) ↦ ↑p
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
⊢ LinearIndependent ℤ (eval C) ↔ LinearIndependent ℤ (SumEval C ho)

Tactic:
rw [← linearIndependent_equiv (sum_equiv C hsC ho), SumEval,
    ← sum_equiv_comp_eval_eq_elim C hsC ho]

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
⊢ LinearIndependent ℤ (eval C ∘ ⇑(sum_equiv C hsC ho)) ↔ LinearIndependent ℤ (eval C ∘ (sum_equiv C hsC ho).toFun)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝¹ : T2Space X
inst✝ : CWComplex C
n : ℕ∞
⊢ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j = ↑(skeletonLT C n)

Tactic:
by
  rw [← RelCWComplex.iUnion_openCell_eq_skeletonLT, empty_union]

Goal state after:
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 i_1 x_1,
    ‖x_1‖ ≤ 1 ∧
      ↑(match i, i_1 with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          x_1 =
        x

Tactic:
refine ⟨0, ?_⟩

Goal state after:
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
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (⋂ k, ⋂ (_ : k < n), C k).Nonempty) → (⋂ i, C i).Nonempty
C : ℕ → Set α
hi : ∀ (i : ℕ), C i ∈ S
h' : ∀ (n : ℕ), dissipate C n ≠ ∅
n : ℕ
g : ⋂ k, ⋂ (_ : k < n), C k ⊆ ∅
x : α
⊢ x ∈ ⋂ y, ⋂ (_ : y ≤ n), C y → x ∈ ⋂ k, ⋂ (_ : k < n), C k

Tactic:
by simp; grind

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
⊢ IsCompact A

Tactic:
let F : (α →ᵇ s) → α →ᵇ β := comp (↑) M

Goal state after:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
⊢ IsCompact A
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
⊢ { toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ } ((e, e), e, e) = (e, e)

Tactic:
simp only [ContinuousMap.coe_mk, Prod.mk_inj]
    exact ⟨HSpace.hmul_e_e, HSpace.hmul_e_e⟩

Goal state after:
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: p : ℚ
s✝ s o : Set ℚ
hs : IsCompact (s, o).1
hpo : p ∈ (s, o).2
ho : IsOpen (s, o).2
⊢ ((s, o).1ᶜ ∩ (s, o).2).Nonempty

Tactic:
inter_comm

Goal state after:
p : ℚ
s✝ s o : Set ℚ
hs : IsCompact (s, o).1
hpo : p ∈ (s, o).2
ho : IsOpen (s, o).2
⊢ ((s, o).2 ∩ (s, o).1ᶜ).Nonempty
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case h
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
H : t₀ = 0 ∨ t₀ = 1
⊢ (if h : i = i then (t₀, t).1 else (t₀, t).2 ⟨i, ⋯⟩) = 0 ∨ (if h : i = i then (t₀, t).1 else (t₀, t).2 ⟨i, ⋯⟩) = 1

Tactic:
dif_pos rfl

Goal state after:
case h
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
H : t₀ = 0 ∨ t₀ = 1
⊢ (t₀, t).1 = 0 ∨ (t₀, t).1 = 1
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case h
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t y : ↑I
yH : y ∈ {0, 1}
y✝ : { j // j ≠ i } → ↑I
⊢ (if h : i = i then ((t, y).2, y✝).1 else ((t, y).2, y✝).2 ⟨i, ⋯⟩) = 0 ∨
    (if h : i = i then ((t, y).2, y✝).1 else ((t, y).2, y✝).2 ⟨i, ⋯⟩) = 1

Tactic:
dif_pos rfl

Goal state after:
case h
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t y : ↑I
yH : y ∈ {0, 1}
y✝ : { j // j ≠ i } → ↑I
⊢ ((t, y).2, y✝).1 = 0 ∨ ((t, y).2, y✝).1 = 1
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 (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
have hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c := by
    simp only [logSizeBallStruct.ball, Finset.mem_filter, hsV, true_and]
    grw [h, tsub_le_self]

Goal state after:
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
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case mp
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x✝ : X
inst✝¹ : DecidableEq N✝
N : Type ?u.16
x : X
inst✝ : IsEmpty N
a₁ a₂ : ↑(Ω^ N X x)
H : (↑a₁).HomotopyRel (↑a₂) (Cube.boundary N)
⊢ (pathSetoid X) ((genLoopHomeoOfIsEmpty N x).toEquiv a₁) ((genLoopHomeoOfIsEmpty N x).toEquiv a₂)

pp: case mpr
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x✝ : X
inst✝¹ : DecidableEq N✝
N : Type ?u.16
x : X
inst✝ : IsEmpty N
a₁ a₂ : ↑(Ω^ N X x)
H : Path ((genLoopHomeoOfIsEmpty N x).toEquiv a₁) ((genLoopHomeoOfIsEmpty N x).toEquiv a₂)
⊢ (Homotopic.setoid N x) a₁ a₂

Tactic:
exacts
        [⟨{ toFun := fun t ↦ H ⟨t, isEmptyElim⟩
            source' := (H.apply_zero _).trans (congr_arg a₁ <| Subsingleton.elim _ _)
            target' := (H.apply_one _).trans (congr_arg a₂ <| Subsingleton.elim _ _) }⟩,
        ⟨{  toFun := fun t0 ↦ H t0.fst
            map_zero_left := fun _ ↦ H.source.trans (congr_arg a₁ <| Subsingleton.elim _ _)
            map_one_left := fun _ ↦ H.target.trans (congr_arg a₂ <| Subsingleton.elim _ _)
            prop' := fun _ _ ⟨i, _⟩ ↦ isEmptyElim i }⟩]

Goal state after: