mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ 1 * l = l

Tactic:
simp [mul_def, one_def]

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ 1 * l = l

Tactic:
by simp [mul_def, one_def]

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ l * 1 = l

Tactic:
simp [mul_def, one_def]

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ l * 1 = l

Tactic:
by simp [mul_def, one_def]

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: case refine_2
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)
hle : ↑n ≤ ↑m
⊢ (List.take (↑n) (List.take (↑m) x)).length + (List.drop (↑n) (List.take (↑m) x)).length ≤ Fintype.card σ

Tactic:
simp only [List.length_drop, List.length_take]
    omega

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf✝ : GrowsPolynomially fun x ↦ |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ |f u|⁻¹ ∈ Set.Icc (c₂⁻¹ * |f x|⁻¹) (c₁⁻¹ * |f x|⁻¹)

Tactic:
have h₁ : 0 < |f u| := by rw [abs_pos]; exact hx'' u hu.1

Goal state after:
f : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf✝ : GrowsPolynomially fun x ↦ |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
⊢ |f u|⁻¹ ∈ Set.Icc (c₂⁻¹ * |f x|⁻¹) (c₁⁻¹ * |f x|⁻¹)
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case bit
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : x = 0 → xb = true
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun x ↦ ℕ → ℕ) (fun n ↦ bif f false true then n else 0)
        (fun a m Ia n ↦ binaryRec (bif f true false then bit a m else 0) (fun b n x ↦ bit (f a b) (Ia n)) n) x y
y : ℕ
⊢ bitwise f (bit xb x) y =
    binaryRec (motive := fun x ↦ ℕ → ℕ) (fun n ↦ bif f false true then n else 0)
      (fun a m Ia n ↦ binaryRec (bif f true false then bit a m else 0) (fun b n x ↦ bit (f a b) (Ia n)) n) (bit xb x) y

Tactic:
| bit xb x hxb ih =>

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case inr
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun x ↦ f x ^ p) x) (c₂ * (fun x ↦ f x ^ p) x)

Tactic:
match hf.eventually_atTop_zero_or_pos_or_neg with
    | .inl hzero => -- eventually zero
      refine ⟨1, by norm_num, 1, by norm_num, ?_⟩
      filter_upwards [hzero, hfnew] with x hx hx'
      intro u hu
      simp only [hx, zero_rpow (ne_of_lt hp), mul_zero,
        Set.Icc_self, Set.mem_singleton_iff]
      simp only [hx, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx'
      rw [hx' u hu, zero_rpow (ne_of_lt hp)]
    | .inr (.inl hpos) => -- eventually positive
      refine ⟨c₂^p, hc₂p, ?_⟩
      refine ⟨c₁^p, hc₁p, ?_⟩
      filter_upwards [eventually_gt_atTop 0, hfnew, hpos,
          (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hpos]
          with x _ hf₁ hf_pos hf_pos₂
      intro u hu
      refine ⟨?lb, ?ub⟩
      case lb => calc
        c₂ ^ p * (f x) ^ p = (c₂ * f x) ^ p := by rw [mul_rpow (le_of_lt hc₂_mem) (le_of_lt hf_pos)]
          _ ≤ _ := rpow_le_rpow_of_nonpos (hf_pos₂ u hu.1) (hf₁ u hu).2 (le_of_lt hp)
      case ub => calc
        (f u) ^ p ≤ (c₁ * f x) ^ p := by
              exact rpow_le_rpow_of_nonpos (by positivity) (hf₁ u hu).1 (le_of_lt hp)
          _ = _ := by rw [← mul_rpow (le_of_lt hc₁_mem) (le_of_lt hf_pos)]
    | .inr (.inr hneg) => -- eventually negative (which is impossible)
      have : ∀ᶠ (_ : ℝ) in atTop, False := by
        filter_upwards [hf_nonneg, hneg] with x hx hx'; linarith
      rw [Filter.eventually_false_iff_eq_bot] at this
      exact False.elim <| atTop_neBot.ne this

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length < l.length ↔ none ∈ l

Tactic:
rw [Nat.lt_iff_le_and_ne, and_iff_right (reduceOption_length_le l), Ne,
    reduceOption_length_eq_iff]

Goal state after:
α : Type u_1
l : List (Option α)
⊢ (¬∀ (x : Option α), x ∈ l → x.isSome = true) ↔ none ∈ l
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
⊢ {x | ∃ S ∈ M.toεNFA.accept, S ∈ M.toεNFA.eval x} = M.accepts

Tactic:
εNFA.eval,

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
⊢ {x | ∃ S ∈ M.toεNFA.accept, S ∈ M.toεNFA.evalFrom M.toεNFA.start x} = M.accepts
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
c : σ
left✝ : Reaches f a b
b0 : f b = none
b' : σ
h' : b' ∈ f b
⊢ False

Tactic:
by cases b0.symm.trans h'

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case tail
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b✝ c✝ : σ₂
a✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) a₂ b✝
cd : c✝ ∈ f₂ b✝
e₁ : σ₁
e₂ : σ₂
ce : Reaches f₂ b✝ e₂
ee : tr e₁ e₂
ae : Reaches f₁ a₁ e₁
⊢ ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
rcases ReflTransGen.cases_head ce with (rfl | ⟨d', cd', de⟩)

Goal state after:
case tail.inl
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b✝ c✝ : σ₂
a✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) a₂ b✝
cd : c✝ ∈ f₂ b✝
e₁ : σ₁
ae : Reaches f₁ a₁ e₁
ce : Reaches f₂ b✝ b✝
ee : tr e₁ b✝
⊢ ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

case tail.inr
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ b✝ c✝ : σ₂
a✝ : ReflTransGen (fun a b ↦ b ∈ f₂ a) a₂ b✝
cd : c✝ ∈ f₂ b✝
e₁ : σ₁
e₂ : σ₂
ce : Reaches f₂ b✝ e₂
ee : tr e₁ e₂
ae : Reaches f₁ a₁ e₁
d' : σ₂
cd' : d' ∈ f₂ b✝
de : ReflTransGen (fun a b ↦ b ∈ f₂ a) d' e₂
⊢ ∃ c₁ c₂, Reaches f₂ c✝ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: ι : Type u_1
Γ : ι → Type u_2
inst✝ : (i : ι) → Inhabited (Γ i)
i : ι
L : ListBlank ((i : ι) → Γ i)
n : ℕ
⊢ (ListBlank.map (proj i) L).nth n = L.nth n i

Tactic:
rw [ListBlank.nth_map]; rfl

Goal state after:
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
⊢ mk' T.left T.right₀ = T

Tactic:
simp only [Tape.right₀, Tape.mk', ListBlank.head_cons, ListBlank.tail_cons]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case pos.mpr.cons
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a :: x = b :: t ++ u
hP : P.rmatch (b :: t) = true
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) ∨ (Q.deriv a).rmatch x = true

Tactic:
left
          rw [List.cons_append, List.cons_eq_cons] at h
          refine ⟨t, u, h.2, ?_, hQ⟩
          rw [rmatch] at hP
          convert! hP
          exact h.1

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case neg.mpr
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
t u : List α
h : a :: x = t ++ u
hP : P.rmatch t = true
hQ : Q.rmatch u = true
⊢ ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true

Tactic:
rcases t with - | ⟨b, t⟩
        · contradiction
        · rw [List.cons_append, List.cons_eq_cons] at h
          refine ⟨t, u, h.2, ?_, hQ⟩
          rw [rmatch] at hP
          convert! hP
          exact h.1

Goal state after:
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
this :
  ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' (?m.157 i) (?m.158 i) σ) σ) (L' R' : ListBlank Bool)
    (l₁ l₂ : List Bool) (h : l₂.length = i),
    stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, h⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
f : List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ
⊢ stepAux (readAux n f) v
      (Tape.mk' (L.flatMap (fun x ↦ (enc x).toList.reverse) ⋯)
        (ListBlank.append (enc a).toList (R.flatMap (fun x ↦ (enc x).toList) ⋯))) =
    stepAux (f (enc a)) v
      (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.flatMap (fun x ↦ (enc x).toList.reverse) ⋯))
        (R.flatMap (fun x ↦ (enc x).toList) ⋯))

Tactic:
exact this n f (L.flatMap (fun x => (enc x).1.reverse) _)
      (R.flatMap (fun x => (enc x).1) _) [] _ (enc a).2

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case mpr.cons.cons
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
t' : List α
U : List (List α)
helem : ∀ t ∈ t' :: U, t ≠ [] ∧ P.rmatch t = true
hsum : a :: x = (t' :: U).flatten
⊢ ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true

Tactic:
· obtain - | ⟨b, t⟩ := t'
          · simp only [forall_eq_or_imp, List.mem_cons] at helem
            simp only [not_true, Ne, false_and] at helem
          simp only [List.flatten_cons, List.cons_append, List.cons_eq_cons] at hsum
          refine ⟨t, U.flatten, hsum.2, ?_, ?_⟩
          · specialize helem (b :: t) (by simp)
            rw [rmatch] at helem
            convert! helem.2
            exact hsum.1
          · grind

Goal state after:
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case neg
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h : ¬i = (S k).length
⊢ (ListBlank.mk (List.map some (S k)).reverse).nth i = ((List.map some (S k)).reverse ++ [some (f v)]).getI i

Tactic:
ListBlank.nth_mk

Goal state after:
case neg
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h : ¬i = (S k).length
⊢ (List.map some (S k)).reverse.getI i = ((List.map some (S k)).reverse ++ [some (f v)]).getI i
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case pos
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n✝
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
v' v₀ : List ℕ
n : ℕ
h2 :
  v' ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (n :: ↑v)
IH :
  ∀ (a'' : List ℕ),
    (Sum.inr a'' ∈
        (cf.eval (n :: ↑v)).bind fun y ↦
          Part.some
            (if y.headI = 0 then Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)
            else Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail))) →
      ∀ (n : ℕ),
        a'' = n :: ↑v →
          (∀ m < n, ¬f (m ::ᵥ v) = 0) →
            ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
hm : ∀ m < n, ¬f (m ::ᵥ v) = 0
h : [f (n ::ᵥ v)].headI = 0
this : v' = n.succ :: ↑v
⊢ ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]

Tactic:
subst this

Goal state after:
case pos
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n✝
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
v₀ : List ℕ
n : ℕ
hm : ∀ m < n, ¬f (m ::ᵥ v) = 0
h : [f (n ::ᵥ v)].headI = 0
h2 :
  n.succ :: ↑v ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (n :: ↑v)
IH :
  ∀ (a'' : List ℕ),
    (Sum.inr a'' ∈
        (cf.eval (n :: ↑v)).bind fun y ↦
          Part.some
            (if y.headI = 0 then Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)
            else Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail))) →
      ∀ (n_1 : ℕ),
        a'' = n_1 :: ↑v →
          (∀ m < n_1, ¬f (m ::ᵥ v) = 0) →
            ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [(n.succ :: ↑v).headI.pred]
⊢ ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [(n.succ :: ↑v).headI.pred]
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
inst✝¹ : HasExplicitFiniteCoproducts P
inst✝ : HasExplicitPullbacksOfInclusions P
⊢ ∀ {X Y Z : CompHausLike P} (f : Z ⟶ X ⨿ Y), PreservesLimit (cospan coprod.inl f) (compHausLikeToTop P)

Tactic:
intro X Y Z f

Goal state after:
P : TopCat → Prop
inst✝¹ : HasExplicitFiniteCoproducts P
inst✝ : HasExplicitPullbacksOfInclusions P
X Y Z : CompHausLike P
f : Z ⟶ X ⨿ Y
⊢ PreservesLimit (cospan coprod.inl f) (compHausLikeToTop P)
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case h_option
X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
Z'_disj : univ.PairwiseDisjoint (Z ∘ some)
U : Set X := D none \ ⋃ i, Z (some i)
U_open : IsOpen[inst✝⁵] U
Z0_subset_U : Z none ⊆ U
V : Set X
V_clopen : IsClopen V
Z0_subset_V : Z none ⊆ V
V_subset_U : V ⊆ U
V_subset_D0 : V ⊆ D none
D' : I → Set X := fun i ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
⊢ ∃ C,
    (∀ (i : Option I), IsClopen (C i)) ∧
      (∀ (i : Option I), Z i ⊆ C i) ∧ (∀ (i : Option I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C

Tactic:
have Z'_subset_D' (i : I) : Z' i ⊆ D' i := by
      rw [subset_sdiff]
      refine ⟨by grind, Disjoint.mono_right V_subset_U ?_⟩
      exact Disjoint.mono_left (subset_iUnion_of_subset i fun _ h ↦ h) (by grind)

Goal state after:
case h_option
X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
Z'_disj : univ.PairwiseDisjoint (Z ∘ some)
U : Set X := D none \ ⋃ i, Z (some i)
U_open : IsOpen[inst✝⁵] U
Z0_subset_U : Z none ⊆ U
V : Set X
V_clopen : IsClopen V
Z0_subset_V : Z none ⊆ V
V_subset_U : V ⊆ U
V_subset_D0 : V ⊆ D none
D' : I → Set X := fun i ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
⊢ ∃ C,
    (∀ (i : Option I), IsClopen (C i)) ∧
      (∀ (i : Option I), Z i ⊆ C i) ∧ (∀ (i : Option I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
f_sur : Surjective f
this✝ : CompactSpace ↑Z
g : X → ↑Z
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
this : closure U = φ ⁻¹' Z₂
⊢ (Z₁ ∪ Z₂) ∩ (Z₁ ∩ Z₂) = ∅

Tactic:
· rw [hZ₁₂.inter_eq, inter_empty]

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
this : ∀ C ⊆ S, IsChain (fun x1 x2 ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
⊢ ∃ E, CompactSpace ↑E ∧ X '' E = univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.domRestrict X '' E₀ ≠ univ

Tactic:
rcases zorn_superset S this with ⟨E, E_min⟩
    obtain ⟨E_closed, E_surj⟩ := E_min.prop
    refine ⟨E, isCompact_iff_compactSpace.mp E_closed.isCompact, E_surj, ?_⟩
    intro E₀ E₀_min E₀_closed
    contrapose E₀_min
    exact eq_univ_of_image_val_eq <|
      E_min.eq_of_subset ⟨E₀_closed.trans E_closed, image_image_val_eq_domRestrict_image ▸ E₀_min⟩
        image_val_subset

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A E : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
G₂_comp : IsCompact G₂ᶜ
G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ
G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ
disj' : Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ
disj'' : Disjoint (closure (ρ '' G₁ᶜ)ᶜ) (closure (ρ '' G₂ᶜ)ᶜ)
hx₁' : ρ x₁ ∈ closure (ρ '' G₁ᶜ)ᶜ
hx₂' : ρ x₂ ∈ closure (ρ '' G₂ᶜ)ᶜ
⊢ False

Tactic:
exact disj''.ne_of_mem hx₁' hx₂' hρx

Goal state after:
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: case refine_1
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : Countable (Clopens X)
⊢ {s | IsClopen s}.Countable

pp: case refine_2
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : Countable (Clopens X)
⊢ inst✝³ = generateFrom {s | IsClopen s}

pp: case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : SecondCountableTopology X
⊢ Countable (Clopens X)

Tactic:
· let f : {s : Set X | IsClopen s} → Clopens X := fun s ↦ ⟨s.1, s.2⟩
    exact Injective.of_eq_imp_le (f := f) (·.le) |>.countable

Goal state after:
case refine_2
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : Countable (Clopens X)
⊢ inst✝³ = generateFrom {s | IsClopen s}

case refine_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : SecondCountableTopology X
⊢ Countable (Clopens X)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg (stepRet k v) b₂ ∧
      Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
        b₂

Tactic:
induction k generalizing v s with

Goal state after: