mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op op' : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
h' : FriendlyOperation op'
⊢ FriendlyOperation (op ∘ op')

Tactic:
by
  rw [FriendlyOperation] at h h' ⊢
  convert! h.comp h'
  simp

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

Goal state before:
pp: case h.some
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
a : α
c : γ
b' : β
hb : F b = some (a, c, b')
⊢ match some (a, c, b') with
  | none =>
    (match some (a, c, b') with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b'))) =
      nil
  | some (a_1, c_1, b'_1) =>
    (match some (a, c, b') with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b'))) =
      Seq.cons a_1
        (op c_1
          (match F b'_1 with
          | none => nil
          | some (a, c, b') => Seq.cons a (op c (f b'))))

Tactic:
simp only [cons_eq_cons, true_and]

Goal state after:
case h.some
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
a : α
c : γ
b' : β
hb : F b = some (a, c, b')
⊢ op c (f b') =
    op c
      (match F b' with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b')))
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg.h
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ ↑m + 1 < ω

Tactic:
· rw [← Nat.cast_succ, lt_omega0]
        exact ⟨_, rfl⟩

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
h : FriendlyOperation op
ms : Multiseries basis_hd basis_tl
⊢ (op ms).destruct =
    Option.map
      (fun x ↦
        match x with
        | (exp, coef, op') => (exp, coef, ↑op' ms.tail))
      (h.unfold ms.head)

Tactic:
by
  unfold Multiseries.destruct
  simp [Seq.FriendlyOperation.destruct_apply_eq_unfold h, FriendlyOperation.unfold, head]
  cases Seq.FriendlyOperation.unfold h (Seq.head ms) <;> rfl

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

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

Tactic:
eta_expand

Goal state after:
m : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
⊢ (fun a ↦ m.inv.toFun basis a) =ᶠ[atTop] fun a ↦ (fun a ↦ m.toFun basis a)⁻¹ a
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.nil
exps_hd : ℝ
exps_tl : List ℝ
h_allZero : AllZero (exps_hd :: exps_tl)
⊢ Tendsto (toFun (exps_hd :: exps_tl) []) atTop (𝓝 1)

Tactic:
eta_expand

Goal state after:
case cons.nil
exps_hd : ℝ
exps_tl : List ℝ
h_allZero : AllZero (exps_hd :: exps_tl)
⊢ Tendsto (fun a ↦ toFun (exps_hd :: exps_tl) [] a) atTop (𝓝 1)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_exps : exps.FirstNonzeroIsNeg
t : Monomial := { coef := coef, unit := exps }
⊢ Tendsto (t.toFun basis) atTop (𝓝 0)

Tactic:
eta_expand

Goal state after:
coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_exps : exps.FirstNonzeroIsNeg
t : Monomial := { coef := coef, unit := exps }
⊢ Tendsto (fun a ↦ t.toFun basis a) atTop (𝓝 0)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_coef : 0 < coef
h_exps : exps.FirstNonzeroIsPos
t : Monomial := { coef := coef, unit := exps }
⊢ Tendsto (t.toFun basis) atTop atTop

Tactic:
eta_expand

Goal state after:
coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_coef : 0 < coef
h_exps : exps.FirstNonzeroIsPos
t : Monomial := { coef := coef, unit := exps }
⊢ Tendsto (fun a ↦ t.toFun basis a) atTop atTop
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_coef : coef < 0
h_exps : exps.FirstNonzeroIsPos
t : Monomial := { coef := coef, unit := exps }
⊢ Tendsto (t.toFun basis) atTop atBot

Tactic:
eta_expand

Goal state after:
coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_coef : coef < 0
h_exps : exps.FirstNonzeroIsPos
t : Monomial := { coef := coef, unit := exps }
⊢ Tendsto (fun a ↦ t.toFun basis a) atTop atBot
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_exps : exps.AllZero
t : Monomial := { coef := coef, unit := exps }
⊢ Tendsto (t.toFun basis) atTop (𝓝 coef)

Tactic:
eta_expand

Goal state after:
coef : ℝ
exps : UnitMonomial
basis : Basis
h_exps : exps.AllZero
t : Monomial := { coef := coef, unit := exps }
⊢ Tendsto (fun a ↦ t.toFun basis a) atTop (𝓝 coef)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

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

Tactic:
have : t2'.toFun (left ++ right) = Monomial.toFun ⟨coef2, exps2⟩ right :=
    Monomial.zeros_append_toFun _

Goal state after:
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_coef2 : { coef := coef2, unit := exps2 }.coef ≠ 0
h_lt : t1.unit < List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit
t2' : Monomial := { coef := coef2, unit := List.replicate (List.length left) 0 ++ exps2 }
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ t1.toFun (left ++ right) =o[atTop] { coef := coef2, unit := exps2 }.toFun right
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

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

Tactic:
have : t2'.toFun (left ++ right) = Monomial.toFun ⟨coef2, exps2⟩ right :=
    Monomial.zeros_append_toFun _

Goal state after:
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := { coef := coef2, unit := List.replicate (List.length left) 0 ++ exps2 }
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ { coef := coef2, unit := exps2 }.toFun right =o[atTop] t1.toFun (left ++ right)
Module: Mathlib.Tactic.DeriveEncodable

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

Tactic:
have := Nat.unpair_lt (by lia : 1 ≤ n' + 1)
          lia

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

Goal state before:
pp: i : ℕ
⊢ (fastGrowing 0)^[i] i = 2 * i

Tactic:
two_mul,

Goal state after:
i : ℕ
⊢ (fastGrowing 0)^[i] i = i + i
Module: Mathlib.Tactic.ModCases

Goal state before:
pp: case refine_2
p : Sort ?u.2
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ a ≡ a % n [MOD n]

Tactic:
· rw [Nat.ModEq, Nat.mod_mod]

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

Goal state before:
pp: a b m : ℕ
⊢ a ^ (2 * b) * a ^ 1 % m = a ^ b % m * (a ^ b % m * a % m) % m

Tactic:
two_mul,

Goal state after:
a b m : ℕ
⊢ a ^ (b + b) * a ^ 1 % m = a ^ b % m * (a ^ b % m * a % m) % m
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✝¹ : UniformSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ IsUniformInducing (⇑UniformFun.ofFun ∘ F) ↔ IsUniformInducing F

Tactic:
rw [isUniformInducing_iff_uniformSpace, isUniformInducing_iff_uniformSpace,
      ← F_eqcont.comap_uniformFun_eq]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : UniformSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ UniformSpace.comap (⇑UniformFun.ofFun ∘ F) (UniformFun.uniformSpace X α) = inst✝¹ ↔
    UniformSpace.comap F (UniformFun.uniformSpace X α) = inst✝¹
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
f : InjectiveFunction α
⊢ Injective f.apply

Tactic:
obtain ⟨xs, hperm, hnodup⟩ := f

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
⊢ Injective (mapToSelf xs hperm hnodup).apply
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✝ : UniformSpace ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
φ : (↑(⋃₀ 𝔖) → α) ≃ᵤ (X → α) := UniformEquiv.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)
⊢ IsUniformInducing (⇑φ.symm ∘ F) ↔ IsUniformInducing F

Tactic:
exact ⟨fun H ↦ φ.isUniformInducing.comp H, fun H ↦ φ.symm.isUniformInducing.comp H⟩

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)
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → Valued.v.restrict x ^ b < ↑y

Tactic:
refine ⟨n, fun m hm ↦ ?_⟩

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.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
A B : Set X
x : X
⊢ x ∈ derivedSet (A ∪ B) ↔ x ∈ derivedSet A ∪ derivedSet B

Tactic:
simp [derivedSet, ← sup_principal, accPt_sup]

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case h
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
Q : Set X.A
hQ : Q ∈ F
R : Set X.A
hR : R ∈ F
⊢ Q ∩ R ∈ F

Tactic:
exact inter_sets _ hQ hR

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case cond.univ_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
⊢ Set.univ ∈ T0

Tactic:
use Set.univ

Goal state after:
case h
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
⊢ Set.univ ∈ F ∧ Set.univ = basic Set.univ
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 : ℕ
i : cell C n
⊢ 0 ∈ ball 0 1

Tactic:
simp only [mem_ball, dist_self, zero_lt_one]

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✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ closedCell n j ⊆ C

Tactic:
simp_rw [← union]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ closedCell n j ⊆ D ∪ ⋃ n, ⋃ j, closedCell n 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
⊢ D ⊆ C

Tactic:
simp_rw [← union]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
⊢ D ⊆ D ∪ ⋃ n, ⋃ j, closedCell n j
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c • x = c • (e (π C fun x ↦ x ∈ s) a * x)
hmas : ↑m ≤ as
⊢ e (π C fun x ↦ x ∈ s) a * Products.eval (π C fun x ↦ x ∈ s) m ∈
    Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as}

Tactic:
refine ⟨⟨a :: m.val, ha.cons_of_le m.prop hmas⟩, ⟨List.cons_le_cons a hmas, ?_⟩⟩

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c • x = c • (e (π C fun x ↦ x ∈ s) a * x)
hmas : ↑m ≤ as
⊢ Products.eval (π C fun x ↦ x ∈ s) ⟨a :: ↑m, ⋯⟩ = e (π C fun x ↦ x ∈ s) a * Products.eval (π C fun x ↦ x ∈ s) m
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case cons
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) ℤ),
    (LinearMap.mulLeft ℤ (e (π C fun x ↦ x ∈ s) a)) (c.sum g) =
      c.sum fun a_1 b ↦ (LinearMap.mulLeft ℤ (e (π C fun x ↦ x ∈ s) a)) (g a_1 b)
⊢ ((if ↑x a = true then e (π C fun x ↦ x ∈ s) a else 1 - e (π C fun x ↦ x ∈ s) a) *
      c.sum fun i a ↦ a • Products.eval (π C fun x ↦ x ∈ s) i) ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
dsimp at hmap ⊢

Goal state after:
case cons
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
⊢ ((if ↑x a = true then e (π C fun x ↦ x ∈ s) a else 1 - e (π C fun x ↦ x ∈ s) a) *
      c.sum fun i a ↦ a • Products.eval (π C fun x ↦ x ∈ s) i) ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})
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}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ ↑l
⊢ ord I i < o

Tactic:
by
  by_contra h'
  apply h
  suffices eval C l = 0 by simp [this]
  ext x
  simp only [eval_eq, LocallyConstant.coe_zero, Pi.zero_apply, ite_eq_right_iff, one_ne_zero]
  contrapose! h'
  exact hsC x.val x.prop i (h'.1 i 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
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
⊢ eval (π C fun x ↦ ord I x < o₂) '' {m | m < l} = ⇑(πs' C h) '' eval (π C fun x ↦ ord I x < o₁) '' {m | m < l}

Tactic:
ext f
  simp only [Set.mem_image, Set.mem_ofPred_eq, exists_exists_and_eq_and]
  apply exists_congr; intro m
  apply and_congr_right; intro hm
  rw [eval_πs' C h (lt_ord_of_lt hm hl)]

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✝ : RelCWComplex C D
E : Subcomplex C
⊢ D ⊆ ↑E

Tactic:
simp_rw [← union]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ D ⊆ D ∪ ⋃ n, ⋃ j, openCell n ↑j
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
inst✝ : Inhabited I
l : ↑(MaxProducts C ho)
hm : term I ho ∈ ↑↑l
⊢ ord I (↑↑l).head! = o

Tactic:
have := Products.prop_of_isGood_of_contained C _ l.prop.1 hsC l.val.val.head!
    (List.head!_mem_self (List.ne_nil_of_mem hm))

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
inst✝ : Inhabited I
l : ↑(MaxProducts C ho)
hm : term I ho ∈ ↑↑l
this : ord I (↑↑l).head! < Order.succ o
⊢ ord I (↑↑l).head! = o
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ cellFrontier n j ⊆ ↑(skeletonLT C ↑n)

Tactic:
obtain ⟨I, hI⟩ := cellFrontier_subset_base_union_finite_closedCell n j

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
⊢ cellFrontier n j ⊆ ↑(skeletonLT C ↑n)
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
C : ℕ → Set α
hC_cc : ∀ (i : ℕ), C i ∈ {s | IsCompact s ∧ IsClosed s}
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
⊢ (⋂ i, C i).Nonempty

Tactic:
← iInter_dissipate

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
C : ℕ → Set α
hC_cc : ∀ (i : ℕ), C i ∈ {s | IsCompact s ∧ IsClosed s}
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
⊢ (⋂ x, dissipate C x).Nonempty
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: a b : ℝ≥0∞
⊢ edist a b = ∞ ↔ a ≠ b ∧ (a = ∞ ∨ b = ∞)

Tactic:
cases a <;> cases b

Goal state after:
case top.top
⊢ edist ∞ ∞ = ∞ ↔ ∞ ≠ ∞ ∧ (∞ = ∞ ∨ ∞ = ∞)

case top.coe
x✝ : ℝ≥0
⊢ edist ∞ ↑x✝ = ∞ ↔ ∞ ≠ ↑x✝ ∧ (∞ = ∞ ∨ ↑x✝ = ∞)

case coe.top
x✝ : ℝ≥0
⊢ edist ↑x✝ ∞ = ∞ ↔ ↑x✝ ≠ ∞ ∧ (↑x✝ = ∞ ∨ ∞ = ∞)

case coe.coe
x✝¹ x✝ : ℝ≥0
⊢ edist ↑x✝¹ ↑x✝ = ∞ ↔ ↑x✝¹ ≠ ↑x✝ ∧ (↑x✝¹ = ∞ ∨ ↑x✝ = ∞)
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight._proof_1 (2 * ↑t)) = 1

Tactic:
rw [(Set.projIcc_eq_right _).2]
    · linarith
    · exact zero_lt_one

Goal state after:
Module: Mathlib.Topology.EMetricSpace.PairReduction

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

Tactic:
rw [logSizeRadius, dif_pos ha]
  exact (Nat.find_spec (exists_radius_le t V ha c)).2

Goal state after:
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
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c 0).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c 0).point ∈ (logSizeBallSeq J hJ a c 0).finset

Tactic:
simp [point_logSizeBallSeq_zero, finset_logSizeBallSeq_zero, Exists.choose_spec]

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ M X x)
⊢ (fun p ↦ ⟨(↑p).comp { toFun := fun t n ↦ t (e.symm n), continuous_toFun := ⋯ }, ⋯⟩)
      ((fun p ↦ ⟨(↑p).comp { toFun := fun t m ↦ t (e m), continuous_toFun := ⋯ }, ⋯⟩) p) =
    p

Tactic:
ext t; simp

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ N X x)
⊢ (fun p ↦ ⟨(↑p).comp { toFun := fun t m ↦ t (e m), continuous_toFun := ⋯ }, ⋯⟩)
      ((fun p ↦ ⟨(↑p).comp { toFun := fun t n ↦ t (e.symm n), continuous_toFun := ⋯ }, ⋯⟩) p) =
    p

Tactic:
ext t; simp

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

Goal state before:
pp: n : ℕ
ih : 0 ∈ preCantorSet n
⊢ (fun x ↦ x / 3) 0 = 0

Tactic:
simp only [zero_div]

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

Goal state before:
pp: n : ℕ
⊢ preCantorSet n ⊆ preCantorSet 0

Tactic:
exact preCantorSet_antitone (by simp)

Goal state after: