mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
h : a * b = 0
⊢ False

Tactic:
rw [h] at hab

Goal state after:
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = 0
h : a * b = 0
⊢ False
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: case e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
this :
  succNthVal p n a₁ a₂ (fun i ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) +
        a₁.coeff (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun v ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p) (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun i ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
        a₂.coeff (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
      nthRemainder p n (fun i ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑i) (truncateFun (n + 1) a₂)
⊢ truncateFun (n + 1) (frobenius (mk p (frobeniusRotationCoeff p ha₁ ha₂))) = fun v ↦
    frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p

Tactic:
clear this

Goal state after:
case e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
⊢ truncateFun (n + 1) (frobenius (mk p (frobeniusRotationCoeff p ha₁ ha₂))) = fun v ↦
    frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := fun t ↦ Nat.rec a (fun x IH ↦ sSup (range fun x ↦ f x IH)) t
⊢ BddAbove (range g)

Tactic:
refine .of_not_isCofinal fun hg ↦ (cof_le hg).not_gt (hα.trans_le' ?_)

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := fun t ↦ Nat.rec a (fun x IH ↦ sSup (range fun x ↦ f x IH)) t
hg : IsCofinal (range g)
⊢ #↑(range g) ≤ ℵ₀
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k
hf :
  ∀ (x y : 𝕎 k),
    f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
x y : 𝕎 k
⊢ (x * y).coeff (n + 1) =
    x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
      f (truncateFun (n + 1) x) (truncateFun (n + 1) y)

Tactic:
rw [hf x y]

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k
hf :
  ∀ (x y : 𝕎 k),
    f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
x y : 𝕎 k
⊢ (x * y).coeff (n + 1) =
    x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
      ((x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1))
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
⊢ Monotone lfpApprox

Tactic:
by
  intro f g h x a
  induction a using WellFoundedLT.induction with | ind i IH
  rw [lfpApprox, lfpApprox]
  exact sup_le_sup_left (iSup₂_mono fun j hj ↦ (f.mono (IH j hj)).trans (h _)) _

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
ha : a ∈ fixedPoints ⇑f
hxa : x ≤ a
i : Ordinal.{u}
⊢ lfpApprox f x i ≤ a

Tactic:
induction i using WellFoundedLT.induction with | ind i IH
   =>  _ 

Goal state after:
case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
ha : a ∈ fixedPoints ⇑f
hxa : x ≤ a
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ a
⊢ lfpApprox f x i ≤ a
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inl
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ (coeff b (b ^ e * x + y)) e = (single e x) e + (coeff b y) e

Tactic:
single_eq_same,

Goal state after:
case inl
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ (coeff b (b ^ e * x + y)) e = x + (coeff b y) e
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: 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}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ (single e' x) e' + f e' = x

Tactic:
single_eq_same,

Goal state after:
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}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ x + f e' = x
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
| o

Tactic:
← CNF.foldr b o

Goal state after:
b o : Ordinal.{u_1}
| foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b o)
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
⊢ (single e x) e + f e = x

Tactic:
single_eq_same,

Goal state after:
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
⊢ x + f e = x
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : o ≠ 0
⊢ IsNormal (veblenWith f o)

Tactic:
veblenWith_of_ne_zero f h

Goal state after:
o : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : o ≠ 0
⊢ IsNormal (derivFamily fun x ↦ veblenWith f ↑x)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o x : Ordinal.{u}
h : x.invVeblen₁ < o
z : Ordinal.{u}
hz : veblen o z = ω ^ x
⊢ False

Tactic:
have hz' := hz

Goal state after:
o x : Ordinal.{u}
h : x.invVeblen₁ < o
z : Ordinal.{u}
hz hz' : veblen o z = ω ^ x
⊢ False
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: ⊢ ε_ 0 = nfp (fun a ↦ ω ^ a) 0

Tactic:
by
  rw [epsilon_eq_deriv, deriv_zero_right]

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

Goal state before:
pp: x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x.rank ≤ y.rank ↔ x ⊆ y

Tactic:
← notMem_iff_subset hy hx,

Goal state after:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x.rank ≤ y.rank ↔ y ∉ x
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
e0 : e = 0
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

Tactic:
simp_rw [scale_eq_mul]
      simp [Mul.mul, mul, e0, h.zero_of_zero,
        show x + 0 = x from repr_inj.1 (by simp)]

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

Goal state before:
pp: left right : Basis
f : ℝ → ℝ
h : WellFormedBasis (left ++ right)
hf_tendsto : Tendsto f atTop atTop
hf_comp_left : ∀ (g : ℝ → ℝ), List.getLast? left = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ WellFormedBasis (left ++ f :: right)

Tactic:
by
  have : WellFormedBasis (f :: right) := cons (h.of_sublist (by simp)) hf_tendsto
    (compare_right_aux (h.of_sublist (by simp)) hf_comp_right)
  apply compare_left_aux (h.of_sublist (by simp)) at hf_comp_left
  apply append (h.of_sublist (by simp)) this
  exact fun g hg ↦ compare_right_aux this (by grind)

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
⊢ Option.map
      ((fun x ↦
          match x with
          | ((exp, coef), tl) => (exp, coef, tl)) ∘
        fun x ↦ (x.1, ↑x.2 (Seq.tail ms)))
      (Seq.FriendlyOperation.unfold h (Seq.head ms)) =
    Option.map ((fun x ↦ (x.1, x.2.1, ↑x.2.2 ms.tail)) ∘ fun x ↦ (x.1.1, x.1.2, x.2))
      (Seq.FriendlyOperation.unfold h (Seq.head ms))

Tactic:
cases Seq.FriendlyOperation.unfold h (Seq.head ms) <;> rfl

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

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

Tactic:
obtain ⟨T, hT⟩ := h_step _ h_op

Goal state after:
case h_step
α : Type u_1
op✝ : Stream'.Seq α → Stream'.Seq α
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_base : motive op✝
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = opf ∘ op' ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
        (T s.head)
⊢ ∃ T,
    ∀ (s : Stream'.Seq α),
      ((opf ∘ op) s).destruct =
        Option.map
          (fun x ↦
            match x with
            | (hd, op') => (hd, ↑op' s.tail))
          (T s.head)
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
h_equiv : log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd
h_log : Tendsto (log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop

Tactic:
apply Filter.Tendsto.congr' _ (Real.tendsto_exp_atTop.comp h_log)

Goal state after:
exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : 0 < exps_hd
h_equiv : log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd
h_log : Tendsto (log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop
⊢ rexp ∘ log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) =ᶠ[atTop]
    toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

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

Tactic:
obtain ⟨T, hT⟩ := h_step _ h_op

Goal state after:
case h_step
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = op' ∘ opf ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
        (T s.head)
⊢ ∃ T,
    ∀ (s : Stream'.Seq α),
      ((op ∘ opf) s).destruct =
        Option.map
          (fun x ↦
            match x with
            | (hd, op') => (hd, ↑op' s.tail))
          (T s.head)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
h : ms.Sorted
⊢ ms.tail.Sorted

Tactic:
by
  cases ms with
  | nil => simp
  | cons exp coef tl => simpa using h.elim_cons.right.right

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

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

Tactic:
rw [jacobiSymNat, jacobiSym.zero_right]

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

Goal state before:
pp: case h.none
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup a A.dedupKeys).getD 0 = 0
haA : List.dlookup a A.dedupKeys = none
⊢ none = some (none.getD 0) ∧ decide True = true

pp: case h.some
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup a A.dedupKeys).getD 0 = 0
val✝ : β
haA : List.dlookup a A.dedupKeys = some val✝
⊢ some val✝ = some ((some val✝).getD 0) ∧ decide True = true

Tactic:
· simp [haA] at h

Goal state after:
case h.some
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup a A.dedupKeys).getD 0 = 0
val✝ : β
haA : List.dlookup a A.dedupKeys = some val✝
⊢ some val✝ = some ((some val✝).getD 0) ∧ decide True = true
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: case mpr
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
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
h : Equicontinuous fun x ↦ ⇑↑x
f : X →* Y
hf : f ∈ S1
⊢ ⇑f ∈ S4

Tactic:
exact ⟨⟨f, h.continuous ⟨f, hf⟩⟩, ⟨⟨f, h.continuous ⟨f, hf⟩⟩, hf, rfl⟩, rfl⟩

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 ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_ind : IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F)
F_cl : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q
⊢ IsInducing ((⋃₀ 𝔖).domRestrict ∘ F)

Tactic:
rwa [EquicontinuousOn.inducing_uniformOnFun_iff_pi' 𝔖_compact F_eqcont] at F_ind

Goal state after:
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
a : Ordinal.{u}
ha : sᵈ[a] ∈ fixedPoints ⇑relDerivedSet
⊢ sᵈ[a] ⊆ perfectKernel s

Tactic:
refine Set.subset_iInter fun i => ?_

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
a : Ordinal.{u}
ha : sᵈ[a] ∈ fixedPoints ⇑relDerivedSet
i : Ordinal.{u}
⊢ sᵈ[a] ⊆ sᵈ[i]
Module: Mathlib.Topology.CantorBendixson

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

Tactic:
refine Set.subset_iInter fun i => ?_

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s P : Set X
hP : Perfect P
hPs : P ⊆ s
i : Ordinal.{u}
⊢ P ⊆ sᵈ[i]
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
j : cell C 0
⊢ cellFrontier 0 j = ∅

Tactic:
by
  simp [cellFrontier, sphere_eq_empty_of_subsingleton]

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
inst✝ : T2Space X
A : Set X
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
hD : IsClosed[t] (A ∩ D)
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier (n + 1) j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell m j
⊢ IsClosed[t] (A ∩ (D ∪ ⋃ m, ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell m j) ∩ cellFrontier (n + 1) j)

Tactic:
refine IsClosed.inter ?_ isClosed_cellFrontier

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
hD : IsClosed[t] (A ∩ D)
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier (n + 1) j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell m j
⊢ IsClosed[t] (A ∩ (D ∪ ⋃ m, ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell m j))
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
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)
n : ℕ
j : cell C n
⊢ IsClosed[t] (A ∩ closedCell n j)

Tactic:
induction n using Nat.case_strong_induction_on with
  | hz =>
    rw [closedCell_zero_eq_singleton]
    exact isClosed_inter_singleton
  | hi n hn =>
    specialize h n.succ n.zero_lt_succ j
    rcases h with h1 | h2
    · rw [← cellFrontier_union_openCell_eq_closedCell, inter_union_distrib_left]
      exact (isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell hn j hDA).union h1
    · exact h2

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

Goal state before:
pp: I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x ↦ false} ℤ
a✝ : f ∈ ⊤
⊢ f ∈ ℤ ∙ eval {fun x ↦ false} nil

Tactic:
Submodule.mem_span_singleton

Goal state after:
I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x ↦ false} ℤ
a✝ : f ∈ ⊤
⊢ ∃ a, a • eval {fun x ↦ false} nil = f
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ LinearIndependent ℤ (eval (π C fun x ↦ ord I x < o)) ↔ LinearIndependent ℤ fun (p : ↑(smaller C o)) ↦ ↑p

Tactic:
rw [GoodProducts.linearIndependent_iff_range,
    ← LinearMap.linearIndependent_iff (πs C o)
    (LinearMap.ker_eq_bot_of_injective (injective_πs _ _)), ← smaller_factorization C o]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ LinearIndependent (ι := ↑(range (π C fun x ↦ ord I x < o))) ℤ ((fun p ↦ ↑p) ∘ (range_equiv_smaller C o).toFun) ↔
    LinearIndependent ℤ fun (p : ↑(smaller C o)) ↦ ↑p
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
⊢ ∃ I, cellFrontier n i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, openCell m j

Tactic:
induction n using Nat.case_strong_induction_on with
  | hz => simp [cellFrontier_zero_eq_empty]
  | hi n hn =>
    -- We apply `cellFrontier_subset_base_union_finite_closedCell` once and then apply
    -- the induction hypothesis to the finitely many cells that
    -- `cellFrontier_subset_base_union_finite_closedCell` gives us.
    classical
    obtain ⟨J, hJ⟩ := cellFrontier_subset_base_union_finite_closedCell n.succ i
    choose p hp using hn
    let I m := J m ∪ ((Finset.range n.succ).biUnion
      (fun l ↦ (J l).biUnion (fun y ↦ if h : l ≤ n then p l h y m else ∅)))
    use I
    intro x hx
    specialize hJ hx
    simp only [mem_union, mem_iUnion, exists_prop] at hJ ⊢
    rcases hJ with hJ | hJ
    · exact .inl hJ
    obtain ⟨l, hln, j, hj, hxj⟩ := hJ
    rw [← cellFrontier_union_openCell_eq_closedCell] at hxj
    rcases hxj with hxj | hxj
    · specialize hp l (Nat.le_of_lt_succ hln) j hxj
      simp_rw [mem_union, mem_iUnion, exists_prop] at hp
      refine .imp_right (fun ⟨k, hkl, i, hi, hxi⟩ ↦ ⟨k, lt_trans hkl hln, i, ?_, hxi⟩) hp
      simp only [Nat.succ_eq_add_one, Finset.mem_union, Finset.mem_biUnion, Finset.mem_range, I]
      exact .inr ⟨l, hln, j, hj, by simp [Nat.le_of_lt_succ hln, hi]⟩
    · right
      use l, hln, j
      simp only [Nat.succ_eq_add_one, Finset.mem_union, I]
      exact ⟨Or.intro_left _ hj, hxj⟩

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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ GoodProducts C = GoodProducts (π C fun x ↦ ord I x < o) ∪ MaxProducts C ho

Tactic:
ext l

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
l : Products I
⊢ l ∈ GoodProducts C ↔ l ∈ GoodProducts (π C fun x ↦ ord I x < o) ∪ MaxProducts C ho