mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
m n : PosNum
⊢ ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)

Tactic:
have this b (n : PosNum) : (cond b (↑n) 0 : ℕ) = ↑(cond b (pos n) 0 : Num) := by
      cases b <;> rfl

Goal state after:
case pos.pos
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
m n : PosNum
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
⊢ ↑(p m n) = Nat.bitwise g ↑(pos m) ↑(pos n)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case h
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
h : l₁.length ≤ l₂.length
e : l₁.length + i = l₂.length + j
⊢ ?m.139 + j ≤ ?m.139 + i

pp: Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
h : l₁.length ≤ l₂.length
e : l₁.length + i = l₂.length + j
⊢ ℕ

Tactic:
e,

Goal state after:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
h : l₁.length ≤ l₂.length
e : l₁.length + i = l₂.length + j
⊢ l₁.length + j ≤ l₂.length + j
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case right.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
q' : Option (TM1.Stmt Γ Λ σ)
v' : σ
h₁ : ((q', v'), s) ∈ tr M (some q, v) a
h₂ : (some q, v) ∈ TM1.stmts M S ×ˢ Finset.univ
⊢ (q', v') ∈ TM1.stmts M S ×ˢ Finset.univ

Tactic:
Finset.mem_product

Goal state after:
case right.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
q' : Option (TM1.Stmt Γ Λ σ)
v' : σ
h₁ : ((q', v'), s) ∈ tr M (some q, v) a
h₂ : (some q, v).1 ∈ TM1.stmts M S ∧ (some q, v).2 ∈ Finset.univ
⊢ (q', v').1 ∈ TM1.stmts M S ∧ (q', v').2 ∈ Finset.univ
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case right.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
q' : Option (TM1.Stmt Γ Λ σ)
v' : σ
h₁ : ((q', v'), s) ∈ tr M (some q, v) a
h₂ : (some q, v) ∈ TM1.stmts M S ×ˢ Finset.univ
⊢ (q', v') ∈ TM1.stmts M S ×ˢ Finset.univ

Tactic:
rw [Finset.mem_product] at h₂ ⊢

Goal state after:
case right.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
q' : Option (TM1.Stmt Γ Λ σ)
v' : σ
h₁ : ((q', v'), s) ∈ tr M (some q, v) a
h₂ : (some q, v).1 ∈ TM1.stmts M S ∧ (some q, v).2 ∈ Finset.univ
⊢ (q', v').1 ∈ TM1.stmts M S ∧ (q', v').2 ∈ Finset.univ
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case comp
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
ih₁ : ∀ (x : List α), P.rmatch x = true ↔ x ∈ P.matches'
ih₂ : ∀ (x : List α), Q.rmatch x = true ↔ x ∈ Q.matches'
x : List α
⊢ (P.comp Q).rmatch x = true ↔ x ∈ (P.comp Q).matches'

Tactic:
simp only [comp_def, mul_rmatch_iff, matches'_mul, Language.mem_mul, *]

Goal state after:
case comp
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
ih₁ : ∀ (x : List α), P.rmatch x = true ↔ x ∈ P.matches'
ih₂ : ∀ (x : List α), Q.rmatch x = true ↔ x ∈ Q.matches'
x : List α
⊢ (∃ t u, x = t ++ u ∧ t ∈ P.matches' ∧ u ∈ Q.matches') ↔ ∃ a ∈ P.matches', ∃ b ∈ Q.matches', a ++ b = x
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
by
  cases m with dsimp only [testBit]
  | zero =>
    rw [show (Num.zero : Nat) = 0 from rfl, Nat.zero_testBit]
  | pos m =>
    rw [cast_pos]
    induction n generalizing m <;> obtain - | m | m := m
        <;> simp only [PosNum.testBit]
    · rfl
    · rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_zero]
    · rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_zero]
    · simp [Nat.testBit_add_one]
    case succ.bit1 n IH =>
      rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_succ, IH]
    case succ.bit0 n IH =>
      rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_succ, IH]

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

Goal state before:
pp: case right.e_a.e_a.cons
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 : σ → Option (Γ k) → σ
head✝ : Γ k
tail✝ : List (Γ k)
e : S k = head✝ :: tail✝
⊢ (S k).reverse[tail✝.length]? = (head✝ :: tail✝).head?

Tactic:
e,

Goal state after:
case right.e_a.e_a.cons
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 : σ → Option (Γ k) → σ
head✝ : Γ k
tail✝ : List (Γ k)
e : S k = head✝ :: tail✝
⊢ (head✝ :: tail✝).reverse[tail✝.length]? = (head✝ :: tail✝).head?
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: 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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
⊢ TM1.stepAux q (f v (S k).reverse[tl.length]?)
      ((Tape.move Dir.right)^[tl.length]
        (Tape.mk' ∅ (addBottom (ListBlank.modifyNth (fun a ↦ update a k none) tl.length L)))) =
    TM1.stepAux q (f v (hd :: tl).head?)
      ((Tape.move Dir.right)^[(hd :: tl).tail.length] (Tape.mk' ∅ (addBottom ?m.569)))

Tactic:
e,

Goal state after:
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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
⊢ TM1.stepAux q (f v (hd :: tl).reverse[tl.length]?)
      ((Tape.move Dir.right)^[tl.length]
        (Tape.mk' ∅ (addBottom (ListBlank.modifyNth (fun a ↦ update a k none) tl.length L)))) =
    TM1.stepAux q (f v (hd :: tl).head?)
      ((Tape.move Dir.right)^[(hd :: tl).tail.length] (Tape.mk' ∅ (addBottom ?m.569)))
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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : ¬i = tl.length
⊢ (List.map some (S k)).reverse.getI i = (List.map some tl).reverse.getI i

Tactic:
e,

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 : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
i : ℕ
h : ¬i = tl.length
⊢ (List.map some (hd :: tl)).reverse.getI i = (List.map some tl).reverse.getI i
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case mp.halt.refl
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
⊢ x ∈ eval step (if v'.headI = 0 then stepRet k v'.tail else stepNormal f (Cont.fix f k) v'.tail) →
    ∃ v₂ ∈ if v'.headI = 0 then pure v'.tail else f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
by_cases he : v'.headI = 0 <;> simp only [if_pos, if_false, he] <;> intro h

Goal state after:
case pos
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : v'.headI = 0
h : x ∈ eval step (stepRet k v'.tail)
⊢ ∃ v₂ ∈ pure v'.tail, x ∈ eval step (Cfg.ret k v₂)

case neg
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
⊢ ∃ v₂ ∈ f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this : ((proj k').f ∘ fun a ↦ update default k (some a)) = fun a ↦ (proj k').f (update default k (some a))
⊢ (Option.map (fun a ↦ update default k (some a) k') L.reverse[i]?).getD default =
    (ListBlank.mk (List.map some (update (fun x ↦ []) k L k')).reverse).nth i

Tactic:
by_cases h : k' = k

Goal state after:
case pos
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this : ((proj k').f ∘ fun a ↦ update default k (some a)) = fun a ↦ (proj k').f (update default k (some a))
h : k' = k
⊢ (Option.map (fun a ↦ update default k (some a) k') L.reverse[i]?).getD default =
    (ListBlank.mk (List.map some (update (fun x ↦ []) k L k')).reverse).nth i

case neg
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this : ((proj k').f ∘ fun a ↦ update default k (some a)) = fun a ↦ (proj k').f (update default k (some a))
h : ¬k' = k
⊢ (Option.map (fun a ↦ update default k (some a) k') L.reverse[i]?).getD default =
    (ListBlank.mk (List.map some (update (fun x ↦ []) k L k')).reverse).nth i
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝¹ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this✝ : (fun x ↦ ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x ↦ ↑↑x
this : (range fun x ↦ ↑↑x) = interior s
⊢ IsOpen[inst✝³] (interior s)

Tactic:
apply isOpen_interior

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

Goal state before:
pp: H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x ↦ ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x ↦ ↑↑x
f1 : IsOpenEmbedding fun x ↦ ↑↑x
f2 : IsOpen[instTopologicalSpaceSubtype] v
⊢ IsOpen[inst✝³] (Subtype.val '' V)

Tactic:
have f3 : ((↑) : s → H) '' V = ((↑) : u → H) '' v := by
      rw [this, image_comp, Subtype.image_preimage_coe, inter_eq_self_of_subset_right V_sub]

Goal state after:
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst✝³] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this✝ : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set ↑u := Subtype.val ⁻¹' V
this : (fun x ↦ ↑↑x) = Subtype.val ∘ Subtype.val
f0 : IsEmbedding fun x ↦ ↑↑x
f1 : IsOpenEmbedding fun x ↦ ↑↑x
f2 : IsOpen[instTopologicalSpaceSubtype] v
f3 : Subtype.val '' V = (fun x ↦ ↑↑x) '' v
⊢ IsOpen[inst✝³] (Subtype.val '' V)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ stepNormal f (Cont.cons₁ fs v k) v) k v) = do
    let v ← (f.cons fs).eval v
    eval step (Cfg.ret k v)

Tactic:
rw [Code.eval, IHf]
    simp only [bind_assoc, pure_bind]; congr; funext v
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [stepRet, IHfs]; congr; funext v'
    refine Eq.trans (b := eval step (stepRet (Cont.cons₂ v k) v')) ?_ (Eq.symm ?_) <;>
      exact reaches_eval (ReflTransGen.single rfl)

Goal state after:
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : Profinite
⊢ Epi (π X)

Tactic:
have := (profiniteToCompHaus.obj X).projectivePresentation.epi

Goal state after:
X : Profinite
this : Epi (profiniteToCompHaus.obj X).projectivePresentation.f
⊢ Epi (π X)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pos.bit1
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
IH :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m ++ [Γ'.cons]) l₁ c d }
          { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
s : Option Γ'
l₁ : List Γ'
⊢ ∃ l₁' l₂' s',
    l₁.reverseAux (trPosNum m.bit1.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m.bit1 ++ [Γ'.cons]) l₁ c d }
        { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }

Tactic:
obtain ⟨l₁', l₂', s', e, h⟩ := IH (Γ'.bit0 :: l₁)
    refine ⟨l₁', l₂', s', e, TransGen.head ?_ h⟩
    simp [trPosNum]
    rfl

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

Goal state before:
pp: case e'_4.e'_7
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn v none fun x x_1 ↦ some Γ'.cons
⊢ elim (trList v.tail) [] [] (trContStack k) = update (elim (trList v) [] [] (trContStack k)) main ?tail.convert_7

pp: case tail.convert_5
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := ⋯
⊢ List Γ'

pp: case tail.convert_7
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := ⋯
⊢ List Γ'

pp: case tail.convert_9
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn v none fun x x_1 ↦ some Γ'.cons
⊢ splitAtPred natEnd (elim (trList v) [] [] (trContStack k) main) = (?tail.convert_5, o, ?tail.convert_7)

Tactic:
· simp; rfl

Goal state after:
case tail.convert_5
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := ⋯
⊢ List Γ'

case tail.convert_9
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn v none fun x x_1 ↦ some Γ'.cons
⊢ splitAtPred natEnd (elim (trList v) [] [] (trContStack k) main) = (?tail.convert_5, o, trList v.tail)
Module: Mathlib.Topology.Category.LightProfinite.Limits

Goal state before:
pp: X Y Z : LightProfinite
f : X ⟶ Z
g : Y ⟶ Z
h : Epi g
⊢ Epi (CompHausLike.pullback.fst f g)

Tactic:
rw [LightProfinite.epi_iff_surjective] at h ⊢
  intro x
  obtain ⟨y, hy⟩ := h (f x)
  exact ⟨⟨⟨x, y⟩, hy.symm⟩, rfl⟩

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

Goal state before:
pp: 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 Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal f (trCont (Cont.fix f k))), var := some Γ'.cons,
      stk := elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) }
    s'
⊢ ∃ b₂,
    TrCfg (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:
refine ⟨_, h₁, TransGen.head rfl <| TransGen.trans ?_ h₂⟩

Goal state after:
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 Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal f (trCont (Cont.fix f k))), var := some Γ'.cons,
      stk := elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) }
    s'
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux (tr (Λ'.ret (trCont (Cont.fix f k)))) s (elim (trList v) [] [] (trContStack (Cont.fix f k))))
    { l := some (trNormal f (trCont (Cont.fix f k))), var := some Γ'.cons,
      stk := elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) }
Module: Mathlib.Topology.Category.LightProfinite.Basic

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

Tactic:
by
  rw [TopologicalSpace.Clopens.countable_iff_secondCountable]
  infer_instance

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

Goal state before:
pp: case fix
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : contSupp (Cont'.fix a✝¹ a✝) ⊆ S
⊢ TM2.SupportsStmt S (tr (Λ'.ret (Cont'.fix a✝¹ a✝)))

Tactic:
contSupp_fix

Goal state after:
case fix
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : codeSupp a✝¹ (Cont'.fix a✝¹ a✝) ⊆ S
⊢ TM2.SupportsStmt S (tr (Λ'.ret (Cont'.fix a✝¹ a✝)))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case fix
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : codeSupp a✝¹ (Cont'.fix a✝¹ a✝) ⊆ S
⊢ TM2.SupportsStmt S (tr (Λ'.ret (Cont'.fix a✝¹ a✝)))

Tactic:
have L := @Finset.mem_union_left

Goal state after:
case fix
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : codeSupp a✝¹ (Cont'.fix a✝¹ a✝) ⊆ S
L : ∀ {α : Type ?u.19} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α), a ∈ s → a ∈ s ∪ t
⊢ TM2.SupportsStmt S (tr (Λ'.ret (Cont'.fix a✝¹ a✝)))
Module: Mathlib.Topology.Category.Profinite.Extend

Goal state before:
pp: I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
this : DiscreteTopology ↑(toProfinite.obj X).toTop
f' : LocallyConstant ↑c.pt.toTop ↑(toProfinite.obj X).toTop :=
  { toFun := ⇑(ConcreteCategory.hom f), isLocallyConstant := ⋯ }
i : I
g : LocallyConstant ↑((F ⋙ toProfinite).obj i).toTop ↑(toProfinite.obj X).toTop
h : f' = LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) g
⊢ ∃ i g, f = c.π.app i ≫ toProfinite.map g

Tactic:
refine ⟨i, ⟨↾g⟩, ?_⟩

Goal state after:
I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
this : DiscreteTopology ↑(toProfinite.obj X).toTop
f' : LocallyConstant ↑c.pt.toTop ↑(toProfinite.obj X).toTop :=
  { toFun := ⇑(ConcreteCategory.hom f), isLocallyConstant := ⋯ }
i : I
g : LocallyConstant ↑((F ⋙ toProfinite).obj i).toTop ↑(toProfinite.obj X).toTop
h : f' = LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) g
⊢ f = c.π.app i ≫ toProfinite.map { hom := ↾⇑g }
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X Y : CondensedSet
f : X ⟶ Y
S : CompHaus
x : X.obj.obj (Opposite.op S)
⊢ Continuous fun a ↦
    (ConcreteCategory.hom (f.hom.app (Opposite.op (of PUnit.{u + 1}))))
      ((ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) a).op)) x)

Tactic:
rw [show (fun (a : S) ↦
          f.hom.app ⟨of PUnit⟩ (X.obj.map ((of PUnit.{u + 1}).const a).op x)) = _
        from funext fun a ↦ NatTrans.naturality_apply f.hom ((of PUnit.{u + 1}).const a).op x]

Goal state after:
X Y : CondensedSet
f : X ⟶ Y
S : CompHaus
x : X.obj.obj (Opposite.op S)
⊢ Continuous fun a ↦
    (ConcreteCategory.hom (Y.obj.map (CompHausLike.const (of PUnit.{u + 1}) a).op))
      ((ConcreteCategory.hom (f.hom.app (Opposite.op S))) x)
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
⊢ f = g

Tactic:
by
  refine funext (fun x => ?_)
  cases x
  · apply h₁
  · apply congr_fun h₀

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
β : TypeVec.{?u.4} 0 → Sort u_1
f : β Fin2.elim0
v : TypeVec.{?u.4} 0
⊢ β Fin2.elim0 = β v

Tactic:
by congr; funext i; cases i

Goal state after: