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

Goal state before:
pp: case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ (e✝.oadd n✝ a✝²).repr < ω ^ b✝

Tactic:
| oadd' _ _ h₃ _ IH =>

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

Goal state before:
pp: case single_add.hxb
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : (∀ (e : Ordinal.{u_1}), f e < b) → coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ e ∉ f.support

Tactic:
exact fun h ↦ (hf' _ h).false

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

Goal state before:
pp: x y : ZFSet.{u}
h : x ∉ y
⊢ lift.{u + 1, u} (insert x y).card = lift.{u + 1, u} (y.card + 1)

Tactic:
simpa [← cardinalMk_coe_sort] using! mk_insert (SetLike.mem_coe.not.2 h)

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

Goal state before:
pp: case refine_1
x y z : ZFSet.{u_1}
h : {x, y} = {z}
⊢ x ∈ {z} ∧ y ∈ {z}

Tactic:
simp [← h]

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

Goal state before:
pp: case a.inr
x y y✝ : PSet.{u_1}
h : y✝ ∈ y
⊢ y✝.rank < max (succ x.rank) y.rank

Tactic:
· simp [rank_lt_of_mem h]

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

Goal state before:
pp: case mp
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : x ⊆ V_ o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ (V_ o).rank ≤ o

Tactic:
simp_rw [rank_le_iff, mem_vonNeumann']

Goal state after:
case mp
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : x ⊆ V_ o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ ∀ ⦃y : ZFSet.{u_1}⦄, (∃ a < o, y ⊆ V_ a) → y.rank < o
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f b : ℝ → ℝ
exp1 exp2 : ℝ
h_lt : exp1 ≤ exp2
h : Majorized f b exp1
⊢ Majorized f b exp2

Tactic:
by
  simp only [Majorized] at *
  exact fun exp' h_exp ↦ h _ (by linarith)

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

Goal state before:
pp: case cons
f g basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h : WellFormedBasis (basis_hd :: basis_tl)
h_comp : (Real.log ∘ basis_hd) =o[atTop] (Real.log ∘ f)
hg : g ∈ basis_hd :: basis_tl
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ f)

Tactic:
simp only [List.mem_cons] at hg

Goal state after:
case cons
f g basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h : WellFormedBasis (basis_hd :: basis_tl)
h_comp : (Real.log ∘ basis_hd) =o[atTop] (Real.log ∘ f)
hg : g = basis_hd ∨ g ∈ basis_tl
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
No : (a0.oadd n a').NF
⊢ (k ≠ 0 → R' < (ω ^ a0.repr) ^ succ ↑k) ∧
    (ω ^ a0.repr) ^ ↑k * (ω ^ a0.repr * ↑↑n + a'.repr) + R' = (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ succ ↑k

Tactic:
induction k with

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

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : 2⁻¹ * dist (op (Seq.cons hd x)).tail (op (Seq.cons hd y)).tail ≤ 2⁻¹ * dist x y
⊢ 0 < 2⁻¹

Tactic:
by norm_num

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 : 0 < exps_hd
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop

Tactic:
by
  have h_equiv : Real.log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop]
      exps_hd • Real.log ∘ basis_hd :=
    (toLogFun_isEquivalent_of_nonzero_head h_basis h_nonzero.ne').congr_left
      (log_toFun_eq_toLogFun h_basis).symm
  suffices h_log : Tendsto (Real.log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl))
      atTop atTop by
    apply Filter.Tendsto.congr' _ (Real.tendsto_exp_atTop.comp h_log)
    apply (toFun_pos (m := (exps_hd :: exps_tl)) h_basis).mono
    intro x hx
    simp only [Function.comp_apply]
    exact Real.exp_log hx
  apply IsEquivalent.tendsto_atTop h_equiv.symm
  apply Filter.Tendsto.const_mul_atTop h_nonzero
  apply Tendsto.comp Real.tendsto_log_atTop
  exact h_basis.tendsto_atTop (by simp)

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

Goal state before:
pp: case seq.right.cons.left
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
tl_tl : Multiseries basis_hd basis_tl
h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq, x.2.Sorted
h_Pairwise✝ :
  Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq
h_all : ∀ x ∈ Multiseries.cons tl_exp tl_coef tl_tl, (exp, coef) > x
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (Multiseries.cons tl_exp tl_coef tl_tl)
⊢ (Multiseries.cons tl_exp tl_coef tl_tl).leadingExp < ↑exp

Tactic:
simp only [leadingExp_cons, WithBot.coe_lt_coe]

Goal state after:
case seq.right.cons.left
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
tl_tl : Multiseries basis_hd basis_tl
h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq, x.2.Sorted
h_Pairwise✝ :
  Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq
h_all : ∀ x ∈ Multiseries.cons tl_exp tl_coef tl_tl, (exp, coef) > x
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (Multiseries.cons tl_exp tl_coef tl_tl)
⊢ tl_exp < exp
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f : ℝ → ℝ
h_coef : coef.Sorted
h_comp : tl.leadingExp < ↑exp
h_tl : tl.Sorted
⊢ (mk (Multiseries.cons exp coef tl) f).Sorted

Tactic:
by
  simp [Multiseries.Sorted.cons h_coef h_comp h_tl]

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

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

Tactic:
intro t
  eta_expand
  simp only [toFun, Pi.smul_apply, smul_eq_mul]
  convert Filter.Tendsto.const_mul _ (UnitMonomial.toFun_tendsto_one_of_allZero h_exps)
  simp [t]

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

Goal state before:
pp: case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
exp✝ : ℝ
coef✝ : MultiseriesExpansion basis_tl
h_trimmed : coef✝.Trimmed
h_ne_zero : ¬coef✝.IsZero
tl✝ : Multiseries basis_hd basis_tl
h_ms : Multiseries.cons exp coef tl = Multiseries.cons exp✝ coef✝ tl✝
⊢ coef.Trimmed ∧ ¬coef.IsZero

Tactic:
| cons h_trimmed h_ne_zero =>

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f
h_approx : ms.Approximates
⊢ (ms.replaceFun f).Approximates

Tactic:
let motive (ms : MultiseriesExpansion (basis_hd :: basis_tl)) : Prop :=
      ∃ (ms' : MultiseriesExpansion (basis_hd :: basis_tl)) (f' : ℝ → ℝ),
      ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f
h_approx : ms.Approximates
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop :=
  fun ms ↦ ∃ ms' f', ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
⊢ (ms.replaceFun f).Approximates
Module: Mathlib.Tactic.ModCases

Goal state before:
pp: p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ 0 ≤ (a % ↑n).toNat ∧ (a % ↑n).toNat < n ∧ a ≡ ↑(a % ↑n).toNat [ZMOD ↑n]

Tactic:
have := natCast_pos.2 <| Nat.le_of_ble_eq_true hn
    have nonneg := emod_nonneg a <| Int.ne_of_gt this
    refine ⟨Nat.zero_le _, ?_, ?_⟩
    · rw [Int.toNat_lt nonneg]; exact Int.emod_lt_of_pos _ this
    · rw [Int.ModEq, Int.toNat_of_nonneg nonneg, emod_emod]

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

Goal state before:
pp: case inr
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
h : ∀ (m : ℕ), n ≠ m ^ q
m : ℕ
hn : n ≠ 0
⊢ n ^ p ≠ m ^ q

Tactic:
contrapose! h

Goal state after:
case inr
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
⊢ ∃ m, n = m ^ q
Module: Mathlib.Tactic.NormNum.PowMod

Goal state before:
pp: a m : ℕ
⊢ (a.pow 1).mod m = a.mod m

Tactic:
by rw [natPow_one]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℤ
s : Finset ℤ
hs : Icc m (n - 1) = s
⊢ Ico m n = s

Tactic:
rw [← hs, Icc_sub_one_right_eq_Ico]

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

Goal state before:
pp: case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
xs_ih : val ∈ ys ↔ x ∈ xs
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : ⟨x, val⟩ ∈ map Prod.toSigma (xs.zip ys)
h₅ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
⊢ val ∈ ys

pp: case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
xs_ih : val ∈ ys ↔ x ∈ xs
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : val ∈ dlookup x (map Prod.toSigma (xs.zip ys))
h₅ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
⊢ (map Prod.toSigma (xs.zip ys)).NodupKeys

Tactic:
· simp only [Prod.toSigma, List.mem_map, Prod.exists] at h₃
          rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩
          apply (List.of_mem_zip h₃).2

Goal state after:
case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
xs_ih : val ∈ ys ↔ x ∈ xs
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : val ∈ dlookup x (map Prod.toSigma (xs.zip ys))
h₅ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
⊢ (map Prod.toSigma (xs.zip ys)).NodupKeys
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 ↦ x ^ x_1
H : MapClusterPt (x ^ m) (atTop.curry atTop) ↿fun a b ↦ x ^ (m + b - a)
⊢ MapClusterPt (x ^ m) atTop fun x_1 ↦ x ^ x_1

Tactic:
suffices Tendsto ↿(fun a b ↦ m + b - a) (atTop.curry atTop) atTop from H.of_comp this

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 ↦ x ^ x_1
H : MapClusterPt (x ^ m) (atTop.curry atTop) ↿fun a b ↦ x ^ (m + b - a)
⊢ Tendsto (↿fun a b ↦ m + b - a) (atTop.curry atTop) atTop
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
⊢ ∀ ⦃X Y : OpenNormalSubgroup ↑P.toProfinite.toTop⦄ (f_1 : X ⟶ Y),
    ((Functor.const (OpenNormalSubgroup ↑P.toProfinite.toTop)).obj (limitCone (diagram G)).pt).map f_1 ≫
        (limitCone (diagram G)).π.app (preimage f Y) ≫ ofFiniteGrpHom (quotientMap f Y) =
      ((limitCone (diagram G)).π.app (preimage f X) ≫ ofFiniteGrpHom (quotientMap f X)) ≫ P.diagram.map f_1

Tactic:
by
      intro X Y g
      ext ⟨x, hx⟩
      -- TODO: `dsimp` should handle this `change`; investigate missing simp lemmas in the
      -- `ProfiniteGrp` / `CompHausLike` API.
      change quotientMap f Y (x <| preimage f Y) =
        P.diagram.map g (quotientMap _ _ <| x <| preimage f X)
      have := hx <| preimage_le (f := f) g.le |>.hom
      obtain ⟨t, ht⟩ : ∃ g : G, QuotientGroup.mk g = x (preimage f X) :=
        QuotientGroup.mk_surjective (x (preimage f X))
      rw [← this, ← ht]
      have := P.cone.π.naturality g
      apply_fun fun q => q (f t) at this
      exact this

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

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : TopologicalSpace ι
inst✝ : T2Space α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_clemb : IsClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)
s : Set ι
s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K
s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q
⊢ IsCompact (closure[inst✝¹] s)

Tactic:
by
  -- We apply `ArzelaAscoli.compactSpace_of_isClosedEmbedding` to the map
  -- `F ∘ (↑) : closure s → (X → α)`, for which all the hypotheses are easily verified.
  rw [isCompact_iff_compactSpace]
  have : ∀ K ∈ 𝔖, ∀ x ∈ K, Continuous (eval x ∘ F) := fun K hK x hx ↦
    UniformOnFun.uniformContinuous_eval_of_mem _ _ hx hK |>.continuous.comp F_clemb.continuous
  have cls_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ ((↑) : closure s → ι)) K :=
    fun K hK ↦ (s_eqcont K hK).closure' <| show Continuous (K.domRestrict ∘ F) from
      continuous_pi fun ⟨x, hx⟩ ↦ this K hK x hx
  have cls_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ closure s ⊆ {i | F i x ∈ Q} :=
    fun K hK x hx ↦ (s_pointwiseCompact K hK x hx).imp fun Q hQ ↦ ⟨hQ.1, closure_minimal hQ.2 <|
      hQ.1.isClosed.preimage (this K hK x hx)⟩
  exact ArzelaAscoli.compactSpace_of_isClosedEmbedding 𝔖_compact
    (F_clemb.comp isClosed_closure.isClosedEmbedding_subtypeVal) cls_eqcont
    fun K hK x hx ↦ (cls_pointwiseCompact K hK x hx).imp fun Q hQ ↦ ⟨hQ.1, by simpa using! hQ.2⟩

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst✝¹⁰ : Monoid M
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module S E
inst✝⁴ : Module S E'
inst✝³ : Module S F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : ContinuousAdd F
f : M → E
g g' : M → E'
x : M
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExistsAt L f g x
hfg' : ConvolutionExistsAt L f g' x
⊢ (f ⋆[L] (g + g')) x = (f ⋆[L] g) x + (f ⋆[L] g') x

Tactic:
simpa [convolution] using hfg.tsum_add hfg'

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst✝¹⁰ : Monoid M
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module S E
inst✝⁴ : Module S E'
inst✝³ : Module S F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : ContinuousAdd F
f f' : M → E
g : M → E'
x : M
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExistsAt L f g x
hfg' : ConvolutionExistsAt L f' g x
⊢ ((f + f') ⋆[L] g) x = (f ⋆[L] g) x + (f' ⋆[L] g) x

Tactic:
simpa [convolution] using hfg.tsum_add hfg'

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this :
  (𝓝 1 ×ˢ Filter.comap (⇑MulOpposite.opHomeomorph.symm) (𝓝 1)).HasBasis (fun i ↦ True ∧ True) fun i ↦
    ((fun y ↦ 1 + y) '' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun y ↦ 1 + y) '' ↑(I ^ i.2))
⊢ s ∈ 𝓝 1

Tactic:
simp only [Homeomorph.comap_nhds_eq, Homeomorph.symm_symm, MulOpposite.opHomeomorph_apply,
    MulOpposite.op_one, and_self, Set.image_add_left] at this

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
⊢ s ∈ 𝓝 1
Module: Mathlib.Topology.Algebra.IsOpenUnits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝² :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this✝¹ : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
x : R
hx : x ∈ ↑(I ^ n)
this✝ : IsUnit (1 + x)
this : -1 + ↑this✝.unit⁻¹ = -↑this✝.unit⁻¹ * x
⊢ -↑this✝.unit⁻¹ * x ∈ I ^ n

Tactic:
exact Ideal.mul_mem_left _ _ hx

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

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : Finite C
x✝ : ∀ (n : ℕ), _root_.Finite (cell C n)
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → IsEmpty (cell C b)
this : ∀ (m : ℕ) (j : cell C m), m < n
⊢ Function.LeftInverse
    (fun x ↦
      match x with
      | ⟨m, j⟩ => ⟨⟨m, ⋯⟩, j⟩)
    fun x ↦
    match x with
    | ⟨m, j⟩ => ⟨↑m, j⟩

Tactic:
simp [Function.LeftInverse]

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

Goal state before:
pp: case mpr
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ basic A ∩ basic B → G ∈ basic (A ∩ B)

Tactic:
rintro ⟨h1, h2⟩

Goal state after:
case mpr
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
h1 : G ∈ basic A
h2 : G ∈ basic B
⊢ G ∈ basic (A ∩ B)
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
⊢ ∃ a, ↑y a ≠ ↑x a

Tactic:
contrapose! h

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : ∀ (a : I), ↑y a = ↑x a
⊢ y = x
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case a.sr.hz
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
hm : ↑0 < n
j : cell C 0
⊢ cellFrontier 0 j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j

Tactic:
| hz =>

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
m : ℕ
i : cell C m
h : ¬Disjoint (openCell n j) (openCell m i)
⊢ ⟨n, j⟩ = ⟨m, i⟩

Tactic:
contrapose! h

Goal state after:
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 : ⟨n, j⟩ ≠ ⟨m, i⟩
⊢ Disjoint (openCell n j) (openCell m i)
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst✝²] U → U ∈ F
c3 : ↑(Ultrafilter.map Ultrafilter.lim FF) ≤ 𝓝 x
U : Set X
hx : x ∈ U
hU : IsOpen[inst✝²] U
this : Ultrafilter.lim ⁻¹' U ∈ FF
⊢ {G | U ∈ G} ∈ FF

Tactic:
apply mem_of_superset this

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := ⋯
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst✝²] U → U ∈ F
c3 : ↑(Ultrafilter.map Ultrafilter.lim FF) ≤ 𝓝 x
U : Set X
hx : x ∈ U
hU : IsOpen[inst✝²] U
this : Ultrafilter.lim ⁻¹' U ∈ FF
⊢ Ultrafilter.lim ⁻¹' U ⊆ {G | U ∈ G}
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case hz
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
j : cell C 0
⊢ IsClosed[t] (A ∩ closedCell 0 j)

Tactic:
| hz =>

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
hC : IsClosed C
f : LocallyConstant ↑C ℤ
⊢ ∃ s g, f = LocallyConstant.comap { toFun := ProjRestrict C fun x ↦ x ∈ s, continuous_toFun := ⋯ } g

Tactic:
by
  obtain ⟨J, g, h⟩ := @Profinite.exists_locallyConstant (Finset I)ᵒᵖ _ _ _
    (spanCone hC.isCompact) ℤ
    (spanCone_isLimit hC.isCompact) f
  exact ⟨(Opposite.unop J), g, h⟩

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

Goal state before:
pp: case hz
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
i : cell C 0
⊢ ∃ I, cellFrontier 0 i ⊆ D ∪ ⋃ m, ⋃ (_ : m < 0), ⋃ j ∈ I m, openCell m j

Tactic:
| hz =>

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 : ℕ
j : cell C n
x : X
xmem : x ∈ closedCell n j
⊢ ↑n < ↑n + 1

Tactic:
by norm_cast; exact lt_add_one n

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
⊢ IsCompactSystem S ↔
    ∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅

Tactic:
rw [← isCompactSystem_insert_empty_iff]
  refine ⟨fun h ↦ fun C hdi hi ↦ ?_, fun h C h1 h2 ↦ ?_⟩
  · rw [← exists_dissipate_eq_empty_iff_of_directed hdi]
    exact h C (by simp [hi])
  rw [← biInter_le_eq_iInter] at h2
  suffices (∀ n, dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ (⋂ n, dissipate C n = ∅) by
    by_cases! f : ∀ n, dissipate C n ∈ S
    · exact h (dissipate C) directed_dissipate f this.2
    · obtain ⟨n, hn⟩ := f
      exact ⟨n, by simpa [hn] using this.1 n⟩
  refine ⟨fun n ↦ ?_, h2⟩
  by_cases g : (dissipate C n).Nonempty
  · simpa [or_comm] using hpi.insert_empty.dissipate_mem h1 n g
  · exact .inr (Set.not_nonempty_iff_eq_empty.mp g)

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : IsTopologicalSemiring Y
r : R
⊢ ↑((algebraMap R (LocallyConstant X Y)) r) = (algebraMap R C(X, Y)) r

Tactic:
ext x
    simp [Algebra.smul_def]

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

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
s : Set (Option α)
so : IsOpen[inst✝] s
x : Option α
xs : none ∈ s
⊢ 1 > 0

Tactic:
by norm_num

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

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

Tactic:
by norm_num

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

Goal state before:
pp: n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ (fun x ↦ (2 + x) / 3) (1 / 4) = 3 / 4

Tactic:
by norm_num

Goal state after: