mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
h : l.reduceOption = l' ++ [a]
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []

Tactic:
reduceOption_eq_append_iff

Goal state after:
case mp
α : Type u_1
l : List (Option α)
l' : List α
a : α
h : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = [a]
⊢ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case lt
a b : PosNum
this : ↑a < ↑b
⊢ ↑a + ↑a + 1 < ↑b + ↑b + 1

Tactic:
exact Nat.succ_lt_succ (Nat.add_lt_add this this)

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b + 1 < ↑a + ↑a + 1

Tactic:
exact Nat.succ_lt_succ (Nat.add_lt_add this this)

Goal state after:
Module: Mathlib.Computability.MyhillNerode

Goal state before:
pp: α : Type u
σ : Type v
L : Language α
s : ↑(Set.range L.leftQuotient)
a : α
⊢ (↑s).leftQuotient [a] ∈ Set.range L.leftQuotient

Tactic:
obtain ⟨y, hy⟩ := s.prop

Goal state after:
α : Type u
σ : Type v
L : Language α
s : ↑(Set.range L.leftQuotient)
a : α
y : List α
hy : L.leftQuotient y = ↑s
⊢ (↑s).leftQuotient [a] ∈ Set.range L.leftQuotient
Module: Mathlib.Computability.RE

Goal state before:
pp: case inr
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this✝ : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cg n = Option.some x
⊢ ∃ n_1 a, a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)

Tactic:
refine ⟨k, ?_⟩

Goal state after:
case inr
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this✝ : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cg n = Option.some x
⊢ ∃ a, a ∈ (Code.evaln k cf n <|> Code.evaln k cg n)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
⊢ (∀ (i_1 : ℕ), L₁.nth i_1 = L₂.nth i_1) → L₁ = L₂

Tactic:
refine ListBlank.induction_on L₁ fun l₁ ↦ ListBlank.induction_on L₂ fun l₂ H ↦ ?_

Goal state after:
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
⊢ mk l₁ = mk l₂
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
l₃ : ListBlank Γ
⊢ append (l₁ ++ l₂) l₃ = append l₁ (append l₂ l₃)

Tactic:
by
  refine l₃.induction_on fun l ↦ ?_
  simp only [ListBlank.append_mk, List.append_assoc]

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

Goal state before:
pp: case zero
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
⊢ T.right₀.nth 0 = T.nth ↑0

Tactic:
simp only [Tape.nth, Tape.right₀, ListBlank.nth_zero,
    ListBlank.nth_succ, ListBlank.head_cons, ListBlank.tail_cons]

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

Goal state before:
pp: case succ
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
n✝ : ℕ
⊢ T.right₀.nth (n✝ + 1) = T.nth ↑(n✝ + 1)

Tactic:
simp only [Tape.nth, Tape.right₀, ListBlank.nth_zero,
    ListBlank.nth_succ, ListBlank.head_cons, ListBlank.tail_cons]

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a✝¹ a✝ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝¹, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝¹ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝¹ v T).var),
        Tape := (TM1.stepAux a✝¹ v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
e : p T.head v = false
⊢ TM0.step (tr M) { q := (some (TM1.Stmt.branch p a✝¹ a✝), v), Tape := T } =
    TM0.step (tr M) { q := (some a✝, v), Tape := T }

Tactic:
simp only [TM0.step, tr, trAux, e]

Goal state after:
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a✝¹ a✝ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝¹, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝¹ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝¹ v T).var),
        Tape := (TM1.stepAux a✝¹ v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
e : p T.head v = false
⊢ Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | move d => Tape.move d T
            | write a => Tape.write a T })
      (some (bif false then trAux M T.head a✝¹ v else trAux M T.head a✝ v)) =
    Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | move d => Tape.move d T
            | write a => Tape.write a T })
      (some (trAux M T.head a✝ v))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a✝¹ a✝ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝¹, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝¹ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝¹ v T).var),
        Tape := (TM1.stepAux a✝¹ v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
e : p T.head v = true
⊢ TM0.step (tr M) { q := (some (TM1.Stmt.branch p a✝¹ a✝), v), Tape := T } =
    TM0.step (tr M) { q := (some a✝¹, v), Tape := T }

Tactic:
simp only [TM0.step, tr, trAux, e]

Goal state after:
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a✝¹ a✝ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝¹, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝¹ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝¹ v T).var),
        Tape := (TM1.stepAux a✝¹ v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
e : p T.head v = true
⊢ Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | move d => Tape.move d T
            | write a => Tape.write a T })
      (some (bif true then trAux M T.head a✝¹ v else trAux M T.head a✝ v)) =
    Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | move d => Tape.move d T
            | write a => Tape.write a T })
      (some (trAux M T.head a✝¹ v))
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case epsilon
α : Type u_1
inst✝ : DecidableEq α
x : List α
⊢ rmatch 1 x = true ↔ x ∈ matches' 1

Tactic:
one_rmatch_iff,

Goal state after:
case epsilon
α : Type u_1
inst✝ : DecidableEq α
x : List α
⊢ x = [] ↔ x ∈ matches' 1
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some.move
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
d : Dir
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.move d q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.move d q) v (Tape.mk' L R)))

Tactic:
| move d q IH =>

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: ⊢ ∀ (m n : Num), ↑(m ^^^ n) = ↑m ^^^ ↑n

Tactic:
apply castNum_eq_bitwise PosNum.lxor <;> intros <;> (try cases_type* Bool) <;> rfl

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

Goal state before:
pp: case move
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q✝ : Λ' Γ Λ σ
h : q✝ ∈ trSupp M S
d : Dir
q : Stmt Γ Λ σ
IH :
  SupportsStmt S q →
    (∀ q' ∈ writes q, q' ∈ trSupp M S) →
      SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
hs : SupportsStmt S (Stmt.move d q)
hw : ∀ q' ∈ writes (Stmt.move d q), q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q)) ∧
    ∀ q' ∈ writes (Stmt.move d q), SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
| move d q IH =>

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m : Num
n : ℕ
⊢ ↑(m >>> n) = ↑m >>> n

Tactic:
obtain - | m := m <;> dsimp only [← shiftr_eq_shiftRight, shiftr]

Goal state after:
case zero
n : ℕ
⊢ ↑0 = ↑zero >>> n

case pos
n : ℕ
m : PosNum
⊢ ↑(m >>> n) = ↑(pos m) >>> n
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case neg.inr
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
h : (S k).length < i
⊢ (List.map some (S k)).reverse.getI i = ((List.map some (S k)).reverse ++ [some (f v)]).getI i

Tactic:
rw [List.getI_eq_default, List.getI_eq_default] <;>
          simp only [Nat.add_one_le_iff, h, List.length, le_of_lt, List.length_reverse,
            List.length_append, List.length_map]

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

Goal state before:
pp: n✝² : ℕ
f✝¹ : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
f : List.Vector ℕ n✝ → ℕ
g : List.Vector ℕ (n✝ + 2) → ℕ
a✝² : Nat.Primrec' f
a✝¹ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n✝ + 1)
hf : cf.eval (↑v).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
a✝ :
  (cf.prec cg).eval (n :: (↑v).tail) =
    pure (pure (Nat.rec (f (n ::ᵥ v.tail).tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ (n ::ᵥ v.tail).tail)) (n ::ᵥ v.tail).head))
b : ℕ
IH :
  ∀ (a : ℕ),
    a + b = n →
      n.succ :: 0 :: g (n ::ᵥ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) :: (↑v).tail ∈
        PFun.fix
          (fun v ↦
            (cg.eval (v.headI :: v.tail.tail)).bind fun x ↦
              Part.some
                (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
                else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
          (a :: b :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail)
a : ℕ
e : a + (b + 1) = n
⊢ a + 1 + b = n

Tactic:
by rwa [add_right_comm]

Goal state after:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hx : ⋂ s, ↑s = {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s // IsClopen s ∧ x ∈ s }
this : Nonempty N
⊢ ∃ s, ↑s ⊆ U

Tactic:
have hNcl : ∀ s : N, IsClosed s.val := fun s => s.property.1.1

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hx : ⋂ s, ↑s = {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s // IsClopen s ∧ x ∈ s }
this : Nonempty N
hNcl : ∀ (s : N), IsClosed[inst✝³] ↑s
⊢ ∃ s, ↑s ⊆ U
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case neg
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
a✝ : IsOpen U
j : ι
ij : ¬i = j
⊢ IsOpen (Sigma.mk j ⁻¹' Sigma.mk i '' U)

Tactic:
· rw [sigma_mk_preimage_image' ij]
      exact isOpen_empty

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.EffectiveEpi

Goal state before:
pp: ⊢ Preregular LightProfinite

Tactic:
apply CompHausLike.preregular

Goal state after:
⊢ ∀ ⦃X Y : CompHausLike fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X⦄ (f : X ⟶ Y),
    EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case fix
f : Code
k : Cont
IH :
  ∀ (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₂
v : List ℕ
s : Option Γ'
this :
  if v.headI = 0 then natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
  else
    natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
⊢ ∃ b₂,
    TrCfg (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (Λ'.ret (trCont (Cont.fix f k))), var := s,
          stk := elim (trList v) [] [] (trContStack (Cont.fix f k)) }
        b₂

Tactic:
by_cases h : v.headI = 0

Goal state after:
case pos
f : Code
k : Cont
IH :
  ∀ (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₂
v : List ℕ
s : Option Γ'
this :
  if v.headI = 0 then natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
  else
    natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
h : v.headI = 0
⊢ ∃ b₂,
    TrCfg (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (Λ'.ret (trCont (Cont.fix f k))), var := s,
          stk := elim (trList v) [] [] (trContStack (Cont.fix f k)) }
        b₂

case neg
f : Code
k : Cont
IH :
  ∀ (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₂
v : List ℕ
s : Option Γ'
this :
  if v.headI = 0 then natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
  else
    natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
h : ¬v.headI = 0
⊢ ∃ b₂,
    TrCfg (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (Λ'.ret (trCont (Cont.fix f k))), var := s,
          stk := elim (trList v) [] [] (trContStack (Cont.fix f k)) }
        b₂
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: S : LightProfinite
⊢ Countable (Clopens ↑S.toTop)

Tactic:
rw [TopologicalSpace.Clopens.countable_iff_secondCountable]
  infer_instance

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.AsLimit

Goal state before:
pp: S : LightProfinite
n m : ℕ
h : n ≤ m
⊢ ⇑(ConcreteCategory.hom (S.transitionMapLE h)) ∘ ⇑(ConcreteCategory.hom (S.proj m)) =
    ⇑(ConcreteCategory.hom (S.proj n))

Tactic:
← S.proj_comp_transitionMapLE h

Goal state after:
S : LightProfinite
n m : ℕ
h : n ≤ m
⊢ ⇑(ConcreteCategory.hom (S.transitionMapLE h)) ∘ ⇑(ConcreteCategory.hom (S.proj m)) =
    ⇑(ConcreteCategory.hom (S.proj m ≫ S.diagram.map (Opposite.op (homOfLE h))))
Module: Mathlib.Topology.Category.LightProfinite.Extend

Goal state before:
pp: F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
this : ∀ (i : ℕᵒᵖ), Epi ((lightToProfinite.mapCone c).π.app i)
⊢ (functor c ⋙ StructuredArrow.post c.pt toLightProfinite lightToProfinite).Initial

Tactic:
exact Profinite.Extend.functor_initial _ (isLimitOfPreserves lightToProfinite hc)

Goal state after:
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
⊢ (unit P hs).app
        (((sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj (op (of P PUnit.{u + 1}))).obj X) ≫
      ((sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj (op (of P PUnit.{u + 1}))).map
        ((counit P hs).app X) =
    𝟙 (((sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj (op (of P PUnit.{u + 1}))).obj X)

Tactic:
ext (x : X.obj.obj _)
    dsimp
    have := CompHausLike.preregular hs
    let : PreservesFiniteProducts ((sheafToPresheaf (coherentTopology _) _).obj X) :=
      inferInstanceAs (PreservesFiniteProducts X.obj)
    apply presheaf_ext ((unit P hs).app _ x)
    intro a
    erw [incl_of_counitAppApp]
    simp only [counitAppAppImage]
    erw [← map_eq_image _ a ⟨PUnit.unit, by simp [mem_iff_eq_image, ← map_preimage_eq_image]⟩]
    rfl

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ ∀ (i j : ℕᵒᵖᵒᵖ) (xi : (fun X ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj i))
    (xj : (fun X ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj j)),
    (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app i)) xi =
        (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map f)) xi =
          (ConcreteCategory.hom (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map g)) xj

Tactic:
· intro ⟨i⟩ ⟨j⟩ (fi : LocallyConstant _ _) (fj : LocallyConstant _ _)
      (h : fi.comap (c.π.app i).hom.hom = fj.comap (c.π.app j).hom.hom)
    obtain ⟨k, ki, kj, _⟩ := IsCofilteredOrEmpty.cone_objs i j
    refine ⟨⟨k⟩, ki.op, kj.op, ?_⟩
    dsimp
    ext x
    obtain ⟨x, hx⟩ := ((LightProfinite.epi_iff_surjective (c.π.app k)).mp inferInstance) x
    rw [← hx]
    change fi ((c.π.app k ≫ (F ⋙ toLightProfinite).map _) x) =
      fj ((c.π.app k ≫ (F ⋙ toLightProfinite).map _) x)
    have h := LocallyConstant.congr_fun h x
    dsimp [- CompHausLike.coe_comp] -- `coe_comp` prevents rewriting with `c.w`
    rwa [dsimp% c.w, dsimp% c.w]

Goal state after:
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
P : LightCondSet
h :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite)
    (g : (free R).obj S.toCondensed ⊗ (free R).obj P ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', (lightProfiniteToLightCondSet ⋙ free R).map π ▷ (free R).obj P ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj (S.toCondensed ⊗ P) ⟶ B
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (lightProfiniteToLightCondSet.map π ▷ P) ≫ g = g' ≫ e

Tactic:
specialize h e S ((μIso (free R) _ _).hom ≫ g)
    obtain ⟨S', π, hπ, g', hh⟩ := h
    refine ⟨S', π, hπ, (μIso (free R) _ _).inv ≫ g', ?_⟩
    rw [assoc, ← hh]
    -- Generated by `simp?`. Leaving it unsqueezed is too slow
    simp only [μIso_inv, comp_obj, Functor.comp_map, μIso_hom, μ_natural_left_assoc, δ_μ_assoc]

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
⊢ LiftR' (α.RelLast' rr) x y ↔ LiftR (α.RelLast rr) x y

Tactic:
by
  dsimp only [LiftR, LiftR']
  apply exists_iff_exists_of_mono F (f' rr _ _) (g' rr _ _)
  · ext i ⟨x, _⟩ : 2
    cases i <;> rfl
  · intros
    simp +unfoldPartialApp only [map_map, TypeVec.comp]
    apply iff_of_eq -- Switch to `eq` so we can use `ext`
    congr <;> ext i ⟨x, _⟩ <;> cases i <;> rfl

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: z : ℤ
w : ℕ
⊢ (↑(z % 2 ^ (w + 1)).toNat).bmod (2 ^ (w + 1)) = (↑z).toInt

Tactic:
Int.ofNat_toNat,

Goal state after:
z : ℤ
w : ℕ
⊢ (max (z % 2 ^ (w + 1)) 0).bmod (2 ^ (w + 1)) = (↑z).toInt