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

Goal state before:
pp: case oadd.inl.none.inr.zero
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
⊢ IsSuccLimit (ω ^ a.repr) ∧
    (∀ (i : ℕ), (f i).repr < (f (i + 1)).repr ∧ (f i).repr < a.repr ∧ ((a.oadd 1 0).NF → ((f i).oadd 1 0).NF)) ∧
      ∀ a_1 < ω ^ a.repr, ∃ i, a_1 < ω ^ (f i).repr

Tactic:
refine ⟨isSuccLimit_opow one_lt_omega0 h1, fun i => ?_,
        exists_lt_omega0_opow' one_lt_omega0 h1 h3⟩

Goal state after:
case oadd.inl.none.inr.zero
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
i : ℕ
⊢ (f i).repr < (f (i + 1)).repr ∧ (f i).repr < a.repr ∧ ((a.oadd 1 0).NF → ((f i).oadd 1 0).NF)
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ ¬(IsSquare (↑n / ↑d).num ∧ IsSquare (↑n / ↑d).den)

Tactic:
← Int.cast_natCast n,

Goal state after:
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ ¬(IsSquare (↑↑n / ↑d).num ∧ IsSquare (↑↑n / ↑d).den)
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ ¬(IsSquare (↑n / ↑d).num ∧ IsSquare (↑n / ↑d).den)

Tactic:
← Int.cast_natCast n,

Goal state after:
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ ¬(IsSquare (↑↑n / ↑d).num ∧ IsSquare (↑↑n / ↑d).den)
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case neg
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : ↑a * ↑y ^ d = ↑x ^ d * ↑b
⊢ False

Tactic:
replace h : a * y ^ d = x ^ d * b := by
    qify
    assumption

Goal state after:
case neg
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : a * y ^ d = x ^ d * b
⊢ False
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case neg.inl
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
h_even : Even d
⊢ ↑a / ↑b ≠ q ^ d

pp: case neg.inr
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
h_odd : Odd d
⊢ ↑a / ↑b ≠ q ^ d

Tactic:
· have := not_power_rat_of_num_aux h_coprime (q := -q) ha (by linarith)
    rwa [h_even.neg_pow] at this

Goal state after:
case neg.inr
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
h_odd : Odd d
⊢ ↑a / ↑b ≠ q ^ d
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x : ℝ
num den den_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hd1 : den_k ^ 2 < den
hd2 : den < (den_k + 1) ^ 2
⊢ Irrational √x

Tactic:
rw [Real.sqrt_eq_rpow]
  apply irrational_rpow_rat_rat_of_den hx_isNNRat (y_num := 1) (y_den := 2) _ hx_coprime (by simp)
    hd1 hd2
  exact ⟨Invertible.mk (1/2) (by simp) (by simp), by simp⟩

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

Goal state before:
pp: case out
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ √(↑n * ⅟↑d) = ↑sn * ⅟↑sd

Tactic:
· simp [← hn, ← hd, Real.sqrt_mul (mul_self_nonneg ↑sn)]

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

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : ⟨a, od⟩ ∈ A.dedupKeys
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup a A.dedupKeys
⊢ ¬(some od).getD 0 = 0

pp: α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : ⟨a, od⟩ ∈ A.dedupKeys
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup a A.dedupKeys
⊢ List.dlookup a A = some od

Tactic:
· simpa using hod

Goal state after:
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : ⟨a, od⟩ ∈ A.dedupKeys
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup a A.dedupKeys
⊢ List.dlookup a A = some od
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : x' = x
h₃ : some y = some val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs

Tactic:
rw [Option.some_inj] at h₃

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : x' = x
h₃ : y = val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
h : Equicontinuous (DFunLike.coe ∘ Subtype.val)
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
⊢ LocallyCompactSpace (X →ₜ* Y)

Tactic:
let S1 : Set (X →* Y) := {f | Set.MapsTo f U W}

Goal state after:
X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
h : Equicontinuous (DFunLike.coe ∘ Subtype.val)
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
⊢ LocallyCompactSpace (X →ₜ* Y)
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:
by
    rw [isCompact_iff_compactSpace] at hS1 ⊢
    exact (Equiv.toHomeomorphOfIsInducing _ h).symm.compactSpace

Goal state after:
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
⊢ ∀ (x_1 : G), 𝓝 (x_1 • x) ≤ Filter.map (fun g ↦ g • x) (𝓝 x_1)

Tactic:
Filter.le_map_iff

Goal state after:
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
⊢ ∀ (x_1 : G), ∀ s ∈ 𝓝 x_1, (fun g ↦ g • x) '' s ∈ 𝓝 (x_1 • x)
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : E →ₗ[S] F →ₗ[S] F
e : E
f : M → F
hL : ∀ (y : F), (L e) y = y
⊢ ({1}.indicator fun x ↦ e) ⋆[L] f = f

Tactic:
ext x; simp only [convolution, Set.indicator_apply]
  rw [tsum_eq_single (⟨(1, x), by grind⟩ : mulFiber x) (by grind [LinearMap.zero_apply])]
  simp [hL]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
hB_inj : Function.Injective ⇑B
⊢ IsEmbedding fun x1 x2 ↦ (B x1) x2

Tactic:
by
  convert! (LinearMap.coe_injective.comp hB_inj |>.isEmbedding_induced)
  exact hB.eq_induced

Goal state after:
Module: Mathlib.Topology.Algebra.Ring.Compact

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : IsTopologicalRing R
inst✝² : CompactSpace R
inst✝¹ : T2Space R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
⊢ (Submodule.toAddSubgroup (∏ i ∈ Set.Finite.toFinset ⋯, i.maxPowDividing I)).FiniteIndex

Tactic:
refine @AddSubgroup.finiteIndex_of_finite_quotient _ _ _ ?_

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : IsTopologicalRing R
inst✝² : CompactSpace R
inst✝¹ : T2Space R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
⊢ Finite (R ⧸ Submodule.toAddSubgroup (∏ i ∈ Set.Finite.toFinset ⋯, i.maxPowDividing I))
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
⊢ ⨆ i, ⨆ f, coinduced (⇑f) inferInstance = coinduced (fun x ↦ x.fst.snd x.snd) inferInstance

Tactic:
instTopologicalSpaceSigma,

Goal state after:
ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
⊢ ⨆ i, ⨆ f, coinduced (⇑f) inferInstance = coinduced (fun x ↦ x.fst.snd x.snd) inferInstance
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
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 ∈ T2, S.Nonempty

Tactic:
suffices ∀ S ∈ T2, S ∈ T0 ∨ ∃ Q ∈ T0, S = AA ∩ Q by
      intro S hS
      rcases this _ hS with h | h
      · exact claim5 S h
      · rcases h with ⟨Q, hQ, rfl⟩
        exact claim4 Q hQ

Goal state after:
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
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 ∈ T2, S ∈ T0 ∨ ∃ Q ∈ T0, S = AA ∩ Q
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
⊢ ⊤ ≤ Submodule.span ℤ (Set.range (spanFinBasis C s))

Tactic:
intro f _
  rw [Finsupp.mem_span_range_iff_exists_finsupp]
  use Finsupp.onFinset (Finset.univ) f.toFun (fun _ _ ↦ Finset.mem_univ _)
  ext x
  change LocallyConstant.evalₗ ℤ x _ = _
  simp only [zsmul_eq_mul, map_finsuppSum, LocallyConstant.evalₗ_apply,
    LocallyConstant.coe_mul, Pi.mul_apply, spanFinBasis, LocallyConstant.coe_mk, mul_ite, mul_one,
    mul_zero, Finsupp.sum_ite_eq, Finsupp.mem_support_iff, ne_eq, ite_not]
  split_ifs with h <;> [exact h.symm; rfl]

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

Goal state before:
pp: case pos
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y = x
b : I
left✝ : b ∈ s.sort fun x1 x2 ↦ x1 ≥ x2
hh : ↑x b = true
⊢ (e (π C fun x ↦ x ∈ s) b) x = 1

Tactic:
rw [e, LocallyConstant.coe_mk, if_pos hh]

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

Goal state before:
pp: case h
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
f : (m : ℕ) → Finset (cell C m)
u : cell C 0
hu : u ∈ f 0
hun1 : ↑(map 1 e) (-1) = ↑(map 0 u) ![]
v : cell C 0
hv : v ∈ f 0
hv1 : ↑(map 1 e) 1 = ↑(map 0 v) ![]
⊢ cellFrontier 1 e = closedCell 0 u ∪ closedCell 0 v

Tactic:
simp [RelCWComplex.cellFrontier_one_eq, image_pair, RelCWComplex.closedCell_zero_eq_singleton,
    hun1, hv1, pair_comm]

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

Goal state before:
pp: case true
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ ↑x a
hx : ↑x a = true
⊢ ∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0

Tactic:
refine ⟨e (π C (· ∈ s)) a, ⟨e_mem_of_eq_true _ _ hx, ?_⟩⟩

Goal state after:
case true
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ ↑x a
hx : ↑x a = true
⊢ (LocallyConstant.evalMonoidHom y) (e (π C fun x ↦ x ∈ s) a) = 0
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
⊢ (factors C s x).prod y = 0

Tactic:
by
  rw [list_prod_apply (π C (· ∈ s)) y _]
  apply List.prod_eq_zero
  simp only [List.mem_map]
  obtain ⟨a, ha⟩ : ∃ a, y.val a ≠ x.val a := by contrapose! h; ext; apply h
  cases hx : x.val a
  · rw [hx, ne_eq, Bool.not_eq_false] at ha
    refine ⟨1 - (e (π C (· ∈ s)) a), ⟨one_sub_e_mem_of_false _ _ ha hx, ?_⟩⟩
    rw [e, LocallyConstant.evalMonoidHom_apply, LocallyConstant.sub_apply,
      LocallyConstant.coe_one, Pi.one_apply, LocallyConstant.coe_mk, if_pos ha, sub_self]
  · refine ⟨e (π C (· ∈ s)) a, ⟨e_mem_of_eq_true _ _ hx, ?_⟩⟩
    rw [hx] at ha
    rw [LocallyConstant.evalMonoidHom_apply, e, LocallyConstant.coe_mk, if_neg ha]

Goal state after:
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)
⊢ 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:
have hmas : m.val ≤ as := by
    apply hc
    simpa only [Finset.mem_coe, Finsupp.mem_support_iff] using hm

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
⊢ 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}
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
⊢ Disjoint D (⋃ n, ⋃ j, openCell n j)

Tactic:
simp_rw [disjoint_iff_inter_eq_empty, inter_iUnion, iUnion_eq_empty]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
⊢ ∀ (i : ℕ) (i_1 : cell C i), D ∩ openCell i i_1 = ∅
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_2.refine_2
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a : ↑(IndexFunctor.obj C J)
i : { i // J i }
⊢ ↑((iso_map C J) ⟨fun i ↦ if hi : J i then ↑a ⟨i, hi⟩ else false, ⋯⟩) i = ↑a i

Tactic:
exact dif_pos i.prop

Goal state after:
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}
hc' :
  (c.sum fun i a ↦ a • Products.eval (π C fun x ↦ x ∈ s) i) =
    (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) as).prod
⊢ (if ↑x a = true then e (π C fun x ↦ x ∈ s) a else 1 - e (π C fun x ↦ x ∈ s) a) *
      (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) as).prod ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
rw [← hc']

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}
hc' :
  (c.sum fun i a ↦ a • Products.eval (π C fun x ↦ x ∈ s) i) =
    (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) as).prod
⊢ ((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)
J K L : I → Prop
inst✝³ : (i : I) → Decidable (J i)
inst✝² : (i : I) → Decidable (K i)
inst✝¹ : (i : I) → Decidable (L i)
inst✝ : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
s t : Finset I
f : unop (op t) ⊆ unop (op s)
x : ↑((spanFunctor hC).obj (op s)).toTop
x✝ : ↑(π C (Membership.mem (unop (op s))))
i : ↥t
⊢ ↑((⇑(iso_map C fun x ↦ x ∈ t) ∘ ProjRestricts C f) x✝) i =
    ↑((⇑(IndexFunctor.map C f) ∘ ⇑(iso_map C fun x ↦ x ∈ s)) x✝) i

Tactic:
exact dif_pos i.prop

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝³ : (i : I) → Decidable (J i)
inst✝² : (i : I) → Decidable (K i)
inst✝¹ : (i : I) → Decidable (L i)
inst✝ : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
x✝¹ : (Finset I)ᵒᵖ
s : Finset I
a✝ : ↑(((Functor.const (Finset I)ᵒᵖ).obj (indexCone hC).pt).obj (op s)).toTop
x✝ : ↑C
i : ↥s
⊢ ↑((⇑(iso_map C fun x ↦ x ∈ s) ∘ ProjRestrict C fun x ↦ x ∈ s) x✝) i = ↑((IndexFunctor.π_app C fun x ↦ x ∈ s) x✝) i

Tactic:
exact dif_pos i.prop

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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : term I ho = i
⊢ true = g i

Tactic:
simpa only [← h] using hg.2.symm

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}
⊢ Function.Injective ⇑(ConcreteCategory.hom (ModuleCat.ofHom (πs C o)))

Tactic:
exact injective_πs _ _

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
inst✝ : RelCWComplex C D
n : ℕ∞
x : X
this : ∀ (m : ℕ), ↑m < n + 1 ↔ ↑m ≤ n
⊢ (x ∈ D ∨ ∃ m, ∃ (_ : ↑m < n + 1), ∃ j, x ∈ openCell m j) ↔ x ∈ D ∨ ∃ m, ∃ (_ : ↑m ≤ n), ∃ j, x ∈ openCell m j

Tactic:
simp_rw [this]

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case refine_2
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : ∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : ⋂ n, ⋂ m, ⋂ (_ : m ≤ n), C m = ∅
n : ℕ
⊢ dissipate C n ∈ S ∨ dissipate C n = ∅

Tactic:
by_cases g : (dissipate C n).Nonempty

Goal state after:
case pos
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : ∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : ⋂ n, ⋂ m, ⋂ (_ : m ≤ n), C m = ∅
n : ℕ
g : (dissipate C n).Nonempty
⊢ dissipate C n ∈ S ∨ dissipate C n = ∅

case neg
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : ∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : ⋂ n, ⋂ m, ⋂ (_ : m ≤ n), C m = ∅
n : ℕ
g : ¬(dissipate C n).Nonempty
⊢ dissipate C n ∈ S ∨ dissipate C n = ∅
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : ¬(tsupport ⇑f).Nonempty
⊢ f = 0

Tactic:
rwa [not_nonempty_iff_eq_empty, tsupport_eq_empty_iff, ← coe_zero, ← DFunLike.ext'_iff] at hs

Goal state after:
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case a
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
⊢ ∀ (i : Set X), IsCompact i → ∀ (i_2 : Set Y), IsOpen[inst✝] i_2 → MapsTo (⇑f) i i_2 → {g | MapsTo (⇑g) i i_2} ∈ 𝓝 f

Tactic:
intro K (hK : IsCompact K) U (hU : IsOpen U) hfKU

Goal state after:
case a
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
⊢ {g | MapsTo (⇑g) K U} ∈ 𝓝 f
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 j : ℕ
hij : i ≠ j
⊢ Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)

Tactic:
wlog! h : i < j generalizing i j
  · exact Disjoint.symm <| this hij.symm <| (ne_iff_lt_iff_le.mpr h).mp hij.symm
  apply Finset.disjoint_of_subset_right
  · exact (Finset.filter_subset _ _).trans (antitone_logSizeBallSeq_add_one_subset hJ h)
  simp [finset_logSizeBallSeq_add_one, Finset.disjoint_sdiff]

Goal state after: