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

Goal state before:
pp: case pos
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
x : ℕ
xe : ↑n₂ = x.succ
⊢ ω ^ e₁.repr * (↑↑n₁ * ↑x.succ) + a₁.repr = (ω ^ e₁.repr * ↑↑n₁ + a₁.repr) * ↑x.succ

Tactic:
Nat.cast_add_one x,

Goal state after:
case pos
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
x : ℕ
xe : ↑n₂ = x.succ
⊢ ω ^ e₁.repr * (↑↑n₁ * (↑x + 1)) + a₁.repr = (ω ^ e₁.repr * ↑↑n₁ + a₁.repr) * (↑x + 1)
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 : R
b : ℕ
h : r ^ b = s
⊢ (algebraMap R A) r ^ b = (algebraMap R A) s

Tactic:
← map_pow,

Goal state after:
R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s : R
b : ℕ
h : r ^ b = s
⊢ (algebraMap R A) (r ^ b) = (algebraMap R A) s
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
⊢ (match (scale 1 b', k + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) => (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑m) k m).NF

Tactic:
cases k <;> cases m

Goal state after:
case oadd.succ.zero.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
na : (a0.oadd n a').NF
this : a0.NF
e₂ : o₂.split' = (b', 0 + 1)
e₁ : o₁.split = (a0.oadd n a', 0)
⊢ (match (scale 1 b', 0 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) => (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑0) k 0).NF

case oadd.succ.zero.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
na : (a0.oadd n a').NF
this : a0.NF
e₂ : o₂.split' = (b', 0 + 1)
n✝ : ℕ
e₁ : o₁.split = (a0.oadd n a', n✝ + 1)
⊢ (match (scale 1 b', 0 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑(n✝ + 1)) k (n✝ + 1)).NF

case oadd.succ.succ.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
na : (a0.oadd n a').NF
this : a0.NF
n✝ : ℕ
e₂ : o₂.split' = (b', n✝ + 1 + 1)
e₁ : o₁.split = (a0.oadd n a', 0)
⊢ (match (scale 1 b', n✝ + 1 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) => (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑0) k 0).NF

case oadd.succ.succ.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
na : (a0.oadd n a').NF
this : a0.NF
n✝¹ : ℕ
e₂ : o₂.split' = (b', n✝¹ + 1 + 1)
n✝ : ℕ
e₁ : o₁.split = (a0.oadd n a', n✝ + 1)
⊢ (match (scale 1 b', n✝¹ + 1 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑(n✝ + 1)) k (n✝ + 1)).NF
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case neg
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
h_if : ¬some x :: ↑s = some x :: ↑t
⊢ Nat.find ⋯ = Nat.find ⋯ + 1

Tactic:
convert! Nat.find_comp_succ _ _ _

Goal state after:
case neg.convert_5
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
h_if : ¬some x :: ↑s = some x :: ↑t
⊢ ¬¬(some x :: ↑s) 0 = (some x :: ↑t) 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
x : α
s t : Stream'.Seq α
⊢ dist (Seq.cons x s) (Seq.cons x t) = 2⁻¹ * dist s t

Tactic:
by
  by_cases! h : s = t
  · simp [h]
  have h' : cons x s ≠ cons x t := by
    simpa
  rw [Subtype.dist_eq, Subtype.dist_eq, PiNat.dist_eq_of_ne (Subtype.coe_ne_coe.mpr h),
    PiNat.dist_eq_of_ne (Subtype.coe_ne_coe.mpr h')]
  simp only [show (1 / 2 : ℝ) = 2⁻¹ by simp, ← pow_succ']
  congr
  simp only [val_cons, PiNat.firstDiff, ne_eq, Classical.dite_not, Subtype.coe_ne_coe.mpr h,
    not_false_eq_true, ↓reduceDIte, val_eq_get]
  split_ifs with h_if
  · contrapose! h'
    apply_fun Subtype.val using Subtype.val_injective
    simpa
  · convert! Nat.find_comp_succ _ _ _
    simp [Stream'.cons]

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

Goal state before:
pp: case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + ↑0
hzero : 0 = zero
h : ¬o₂ = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
· have h' := mt repr_inj.1 h
        have hne : o₂ ≠ zero := fun he => h (he ▸ rfl)
        simp [-zero_def, opow_def, opowAux2, e₁, r₁, hne, hzero]
        exact (zero_opow h').symm

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

Goal state before:
pp: exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : exps_hd < 0
h_equiv : log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd
h_log_atTop : Tendsto (log ∘ basis_hd) atTop atTop
⊢ Tendsto (exps_hd • log ∘ basis_hd) atTop atBot

Tactic:
exact Filter.Tendsto.const_mul_atTop_of_neg h_nonzero h_log_atTop

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

Goal state before:
pp: t1 t2 : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length t1.unit = List.length t2.unit
⊢ (t1.mul t2).toFun basis =ᶠ[atTop] t1.toFun basis * t2.toFun basis

Tactic:
by
  simp only [toFun, mul, Algebra.mul_smul_comm, Algebra.smul_mul_assoc]
  grw [UnitMonomial.mul_toFun h_basis h_length]
  filter_upwards [] with t
  simp [Pi.smul_apply, Pi.mul_apply]
  ring

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

Goal state before:
pp: case h₂
basis : Basis
t1 t2 : Monomial
h_basis : WellFormedBasis basis
h1 : List.length t1.unit = List.length basis
h2 : List.length t2.unit = List.length basis
h_coef2 : t2.coef ≠ 0
h_lt : t1.unit < t2.unit
⊢ t1.unit.toFun basis =o[atTop] t2.unit.toFun basis

Tactic:
apply UnitMonomial.isLittleO_of_lt h_basis h1 h2 h_lt

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

Goal state before:
pp: a : ℕ
⊢ jacobiSymNat a 0 = 1

Tactic:
by
  rw [jacobiSymNat, jacobiSym.zero_right]

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type
inst✝ : DecidableEq α
xs✝ : List ((_ : α) × α)
h₀✝ : map Sigma.fst xs✝ ~ map Sigma.snd xs✝
h₁✝ : (map Sigma.snd xs✝).Nodup
xs' ys' : List α
h₀ : xs' ~ ys'
h₁ : ys'.Nodup
h₃ : xs'.length ≤ ys'.length
h₄ : ys'.length ≤ xs'.length
⊢ (map Sigma.snd (map Prod.toSigma (xs'.zip ys'))).Nodup

Tactic:
simp only [comp_def, List.map_snd_zip, *, Prod.snd_toSigma, List.map_map]

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

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

Tactic:
refine forall_congr' fun g ↦ imp_congr_left ?_

Goal state after:
G : GrpCat
g : ↑G
⊢ (ConcreteCategory.hom (eta G)) g = 1 ↔ ∀ (H : FiniteIndexNormalSubgroup ↑G), g ∈ H
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
h : IsInducing ⇑(Equiv.Set.image DFunLike.coe S ⋯)
⊢ IsCompact S

Tactic:
rw [isCompact_iff_compactSpace] at hS1 ⊢

Goal state after:
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : CompactSpace ↑(ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
h : IsInducing ⇑(Equiv.Set.image DFunLike.coe S ⋯)
⊢ CompactSpace ↑S
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f g : completion G ⟶ P
h : eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map f = eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map g
⊢ f = g

Tactic:
by
  ext x
  apply congrFun
  refine (denseRange (G := G)).equalizer f.hom.continuous_toFun g.hom.continuous_toFun ?_
  funext y
  simpa [GrpCat.comp_apply] using! (ConcreteCategory.congr_hom h y)

Goal state after:
Module: Mathlib.Topology.Baire.BaireMeasurable

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
h : MeasurableSet s
⊢ BaireMeasurableSet s

Tactic:
by
  borelize α
  exact h.eventuallyMeasurableSet

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : MulArchimedean Γ₀
inst✝ : Valued R Γ₀
x : R
hx : Valued.v x < 1
y : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
v : Valuation R Γ₀ := Valued.v
n : ℕ
hn : Valued.v x ^ n < ↑((Units.map ↑MonoidWithZeroHom.ValueGroup₀.embedding) y)
m : ℕ
hm : n ≤ m
⊢ Valued.v.restrict x ^ m < ↑y

Tactic:
← map_pow,

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : MulArchimedean Γ₀
inst✝ : Valued R Γ₀
x : R
hx : Valued.v x < 1
y : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
v : Valuation R Γ₀ := Valued.v
n : ℕ
hn : Valued.v x ^ n < ↑((Units.map ↑MonoidWithZeroHom.ValueGroup₀.embedding) y)
m : ℕ
hm : n ≤ m
⊢ Valued.v.restrict (x ^ m) < ↑y
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 D : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
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
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
isClosedBase : IsClosed[inst✝] D
union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h : (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) ∧ IsClosed[inst✝] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty (cell b)
this : IsClosed[inst✝] (A ∩ (D ∪ ⋃ n, ⋃ j, ↑(map (↑n) j) '' closedBall 0 1))
n : ℕ
⊢ ⋃ j, ↑(map n j) '' closedBall 0 1 ⊆ ⋃ (hx : n < N), ⋃ j, ↑(map (↑⟨n, hx⟩) j) '' closedBall 0 1

Tactic:
apply iUnion_subset

Goal state after:
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D✝ : Set X✝
inst✝¹ : RelCWComplex C✝ D✝
X : Type u
inst✝ : TopologicalSpace X
C D : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
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
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
isClosedBase : IsClosed[inst✝] D
union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h : (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) ∧ IsClosed[inst✝] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty (cell b)
this : IsClosed[inst✝] (A ∩ (D ∪ ⋃ n, ⋃ j, ↑(map (↑n) j) '' closedBall 0 1))
n : ℕ
⊢ ∀ (i : cell n), ↑(map n i) '' closedBall 0 1 ⊆ ⋃ (hx : n < N), ⋃ j, ↑(map (↑⟨n, hx⟩) j) '' closedBall 0 1
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: case h
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)
J : (m : ℕ) → Finset (cell C m)
x : X
hJ : x ∈ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ J m, openCell m j
hx : x ∈ ↑(map n ↑i) '' sphere 0 1
⊢ x ∈ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ (fun m ↦ (J m).preimage Subtype.val ⋯) m, ↑(map m ↑j) '' closedBall 0 1

Tactic:
simp_rw [iUnion_coe_set, mem_union, mem_iUnion, Finset.mem_preimage, exists_prop,
      Decidable.or_iff_not_imp_left] at hJ ⊢

Goal state after:
case h
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)
J : (m : ℕ) → Finset (cell C m)
x : X
hx : x ∈ ↑(map n ↑i) '' sphere 0 1
hJ : x ∉ D → ∃ i < n, ∃ i_1 ∈ J i, x ∈ openCell i i_1
⊢ x ∉ D → ∃ i < n, ∃ i_1 ∈ E.I i, i_1 ∈ J i ∧ x ∈ (fun a ↦ ↑(map i i_1) a) '' closedBall 0 1
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: case h
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)
J : (m : ℕ) → Finset (cell C m)
x : X
hx : x ∈ ↑(map n ↑i) '' sphere 0 1
hJ : x ∉ D → ∃ i < n, ∃ i_1 ∈ J i, x ∈ openCell i i_1
h : x ∉ D
⊢ ∃ i < n, ∃ i_1 ∈ E.I i, i_1 ∈ J i ∧ x ∈ (fun a ↦ ↑(map i i_1) a) '' closedBall 0 1

Tactic:
specialize hJ h

Goal state after:
case h
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)
J : (m : ℕ) → Finset (cell C m)
x : X
hx : x ∈ ↑(map n ↑i) '' sphere 0 1
hJ : ∃ i < n, ∃ i_1 ∈ J i, x ∈ openCell i i_1
h : x ∉ D
⊢ ∃ i < n, ∃ i_1 ∈ E.I i, i_1 ∈ J i ∧ x ∈ (fun a ↦ ↑(map i i_1) a) '' closedBall 0 1
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
hg : ContinuousGeneratedBy X g
T : Type u_1
inst✝ : TopologicalSpace T
f : T → Y
hf : ContinuousGeneratedBy X f
⊢ ContinuousGeneratedBy X (g ∘ f)

Tactic:
rw [continuousGeneratedBy_iff]
  exact (hg.continuousMap.comp hf.continuousMap).continuous

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : ↑C
i : ι
h : ↑((π_app C fun x ↦ x ∈ {i}) a) = ↑((π_app C fun x ↦ x ∈ {i}) b)
⊢ ↑a i = ↑b i

Tactic:
simp only [π_app, ContinuousMap.precomp, ContinuousMap.coe_mk] at h

Goal state after:
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : ↑C
i : ι
h :
  ↑(Set.MapsTo.restrict (fun f j ↦ f ↑j) C (obj C fun x ↦ x ∈ {i}) ⋯ a) =
    ↑(Set.MapsTo.restrict (fun f j ↦ f ↑j) C (obj C fun x ↦ x ∈ {i}) ⋯ b)
⊢ ↑a i = ↑b i
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case e_s
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
e : cell C 1
f : Fin 1 → ℝ
⊢ const (Fin 1) (f default) 0 = 1 ∨ const (Fin 1) (f default) 0 = -1 ↔
    const (Fin 1) (f default) 0 = (-1) 0 ∨ const (Fin 1) (f default) = 1

Tactic:
simp [const_apply, or_comm]

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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩
h₁ : Continuous C₁C
x : I → Bool
hx : x ∈ C
hx₁ : x ∈ C1 C ho
⊢ ↑(ProjRestrict C (fun x ↦ ord I x < o) ⟨x, hx⟩) ∈ π (C1 C ho) fun x ↦ ord I x < o

Tactic:
simpa only [ProjRestrict, Set.MapsTo.val_restrict_apply] using! ⟨x, hx₁, rfl⟩

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
l : Products I
o : Ordinal.{u}
hl : ∀ i ∈ ↑l, ord I i < o
f : LocallyConstant ↑C ℤ
m : Products I
hm : m < l
⊢ eval C m = f ↔ (πs C o) (eval (π C fun x ↦ ord I x < o) m) = f

Tactic:
rw [eval_πs C (lt_ord_of_lt hm hl)]

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

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
h : ∀ o' < o, P I o'
hho : o ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ ∀ (C : Set (I → Bool)), IsClosed C → contained C o → LinearIndependent ℤ (eval C)

Tactic:
C

Goal state after:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
h : ∀ o' < o, P I o'
hho : o ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
⊢ IsClosed C → contained C o → LinearIndependent ℤ (eval C)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case h
S : Profinite
C : { C // IsClopen C }
⊢ Continuous fun a ↦ decide (a ∈ ↑C)

Tactic:
← IsLocallyConstant.iff_continuous

Goal state after:
case h
S : Profinite
C : { C // IsClopen C }
⊢ IsLocallyConstant fun a ↦ decide (a ∈ ↑C)
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X),
    (∀ (i : Fin n), IsClopen (U i)) →
      (∀ (i : Fin n), (U i).Nonempty) → Pairwise (Disjoint on U) → ⋃ i, U i = Set.univ → ↑n ≤ (f ⁻¹' {y}).encard
hy : Infinite (ConnectedComponents X)
⊢ ENat.card (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard

Tactic:
simp only [ENat.card_eq_top_of_infinite, top_le_iff, ENat.eq_top_iff_forall_ge]

Goal state after:
case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X),
    (∀ (i : Fin n), IsClopen (U i)) →
      (∀ (i : Fin n), (U i).Nonempty) → Pairwise (Disjoint on U) → ⋃ i, U i = Set.univ → ↑n ≤ (f ⁻¹' {y}).encard
hy : Infinite (ConnectedComponents X)
⊢ ∀ (m : ℕ), ↑m ≤ (f ⁻¹' {y}).encard
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
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
⊢ (Linear_CC' C hsC ho) (Products.eval C ↑l) =
    (Linear_CC' C hsC ho) (m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod)

Tactic:
rw [← hmsum]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
⊢ (m.sum fun i a ↦ a • Products.eval (C' C ho) i) =
    (Linear_CC' C hsC ho) (m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod)
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: case pos
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
⊢ C(↑(Icc a c), E)

pp: case neg
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : ¬f ⊤ = g ⊥
⊢ C(↑(Icc a c), E)

Tactic:
· let h (t : α) : E := if t ≤ b then IccExtendCM f t else IccExtendCM g t
    suffices Continuous h from ⟨fun t => h t, by fun_prop⟩
    apply Continuous.if_le (by fun_prop) (by fun_prop) continuous_id continuous_const
    rintro x rfl
    simpa [IccExtendCM, projIccCM]

Goal state after:
case neg
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : ¬f ⊤ = g ⊥
⊢ C(↑(Icc a c), E)
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: ι : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
A✝ B : Set E
inst✝¹ : SequentialSpace E
inst✝ : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ i, closure[inst✝³] {x i}
this✝ : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
this : ∀ (k : ℕ), ∃ n > k, a ∈ closure[inst✝³] {x n}
φ : ℕ → ℕ
hφ1 : StrictMono φ
hφ2 : ∀ (n : ℕ), a ∈ closure[inst✝³] {x (φ n)}
⊢ False

Tactic:
refine hx a φ hφ1 (tendsto_atTop_nhds.2 fun U ha hUo => ⟨0, fun n _ => ?_⟩)

Goal state after:
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
A✝ B : Set E
inst✝¹ : SequentialSpace E
inst✝ : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ i, closure[inst✝³] {x i}
this✝ : IsCountablyCompact A
a : E
ha✝ : a ∈ A ∧ MapClusterPt a atTop x
this : ∀ (k : ℕ), ∃ n > k, a ∈ closure[inst✝³] {x n}
φ : ℕ → ℕ
hφ1 : StrictMono φ
hφ2 : ∀ (n : ℕ), a ∈ closure[inst✝³] {x (φ n)}
U : Set E
ha : a ∈ U
hUo : IsOpen[inst✝³] U
n : ℕ
x✝ : 0 ≤ n
⊢ (x ∘ φ) n ∈ U
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
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
⊢ Function.Injective (MaxToGood C hC hsC ho h₁)

Tactic:
intro m n h

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
m n : ↑(MaxProducts C ho)
h : MaxToGood C hC hsC ho h₁ m = MaxToGood C hC hsC ho h₁ n
⊢ m = n
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
l : Filter α
⊢ closure {l} = Ici l

Tactic:
ext l'
  simp [Filter.mem_closure, Filter.le_def]

Goal state after: