mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case bit.bit
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
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
yb : Bool
y : ℕ
hyb : bit yb y ≠ 0
a✝ :
  bitwise f (bit xb x) y =
    binaryRec (bif f true false then bit xb x else 0)
      (fun b n x_1 ↦
        bit (f xb b)
          (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 n))
      y
⊢ bit (f (bit xb x).bodd (bit yb y).bodd) (bitwise f (bit xb x / 2) (bit yb y / 2)) =
    ⋯ ▸
      bit (f xb (bit yb y).bodd)
        (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
          (bit yb y).div2)

Tactic:
bodd_bit,

Goal state after:
case bit.bit
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
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
yb : Bool
y : ℕ
hyb : bit yb y ≠ 0
a✝ :
  bitwise f (bit xb x) y =
    binaryRec (bif f true false then bit xb x else 0)
      (fun b n x_1 ↦
        bit (f xb b)
          (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 n))
      y
⊢ bit (f xb yb) (bitwise f (bit xb x / 2) (bit yb y / 2)) =
    ⋯ ▸
      bit (f xb yb)
        (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
          (bit yb y).div2)
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case neg
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
⊢ bit b n < bit b' m

Tactic:
have := hn' _ hn hm fun j hj => by
          convert! hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_bit_succ]

Goal state after:
case neg
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), n.testBit i = false → m.testBit i = true → (∀ (j : ℕ), i < j → n.testBit j = m.testBit j) → n < m
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    (bit b n).testBit i = false →
      m.testBit i = true → (∀ (j : ℕ), i < j → (bit b n).testBit j = m.testBit j) → bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), i'.succ < j → (bit b n).testBit j = (bit b' m).testBit j
hi : ¬i'.succ = 0
hn : n.testBit i' = false
hm : m.testBit i' = true
this : n < m
⊢ bit b n < bit b' m
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: f : Bool → Bool → Bool
hf : ∀ (b b' : Bool), f b b' = f b' b
n m : ℕ
this : bitwise f = swap (bitwise f)
| bitwise f n m

Tactic:
rw [this]

Goal state after:
f : Bool → Bool → Bool
hf : ∀ (b b' : Bool), f b b' = f b' b
n m : ℕ
this : bitwise f = swap (bitwise f)
| swap (bitwise f) n m
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : α
⊢ (fun x ↦ a :: x) ⁻¹' M.acceptsFrom S = M.acceptsFrom (M.stepSet S a)

Tactic:
ext x; simp [cons_mem_acceptsFrom M]

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

Goal state before:
pp: case eq
a b : PosNum
this : a = b
⊢ a.bit0 = b.bit0

Tactic:
rw [this]

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

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

Tactic:
rw [this]

Goal state after:
case eq
a b : PosNum
this : a = b
⊢ ↑b + ↑b < ↑b + ↑b + 1
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
rw [this]

Goal state after:
case eq
a b : PosNum
this : a = b
⊢ ↑b + ↑b < ↑b + ↑b + 1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case eq
a b : PosNum
this : a = b
⊢ a.bit1 = b.bit1

Tactic:
rw [this]

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

Goal state before:
pp: n : Num
⊢ ↑n.succ'.pred' = ↑n

Tactic:
pred'_to_nat,

Goal state after:
n : Num
⊢ (↑n.succ').pred = ↑n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : PosNum
⊢ ↑n.pred' + 1 = ↑n

Tactic:
pred'_to_nat,

Goal state after:
n : PosNum
⊢ (↑n).pred + 1 = ↑n
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
start : Set σ
this : M.toεNFA.stepSet = M.stepSet
⊢ List.foldl M.toεNFA.stepSet start = List.foldl M.stepSet start

Tactic:
rw [this]

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

Goal state before:
pp: f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
this : f = g + (f - g)
⊢ GrowsPolynomially f

Tactic:
rw [this]

Goal state after:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
this : f = g + (f - g)
⊢ GrowsPolynomially (g + (f - g))
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
i : ℤ
⊢ (move Dir.right T).nth i = (move Dir.left (move Dir.right T)).nth (i + 1)

Tactic:
rw [Tape.move_left_nth, add_sub_cancel_right]

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

Goal state before:
pp: case right
Γ : 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
⊢ ∀ {q : Λ' M} {a : Γ} {q' : Λ' M} {s : TM0.Stmt Γ}, (q', s) ∈ tr M q a → q ∈ ↑(trStmts M S) → q' ∈ ↑(trStmts M S)

Tactic:
intro q

Goal state after:
case right
Γ : 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
q : Λ' M
⊢ ∀ {a : Γ} {q' : Λ' M} {s : TM0.Stmt Γ}, (q', s) ∈ tr M q a → q ∈ ↑(trStmts M S) → q' ∈ ↑(trStmts M S)
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

Tactic:
List.cons_eq_cons

Goal state after:
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 = b ∧ x = t ++ u
hP : P.rmatch (b :: t) = true
⊢ ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case neg.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

Tactic:
List.cons_eq_cons

Goal state after:
case neg.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 = b ∧ x = t ++ u
hP : P.rmatch (b :: t) = true
⊢ ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₂ : Stmt Γ Λ σ
h₁₂ : q₁ ∈ stmts₁ q₂
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
⊢ q₀ ∈ stmts₁ q₂

Tactic:
induction q₂ with (
    simp only [stmts₁] at h₁₂ ⊢
    simp only [Finset.mem_insert, Finset.mem_singleton, Finset.mem_union] at h₁₂)
  | branch f q₁ q₂ IH₁ IH₂ =>
    rcases h₁₂ with (rfl | h₁₂ | h₁₂)
    · unfold stmts₁ at h₀₁
      exact h₀₁
    · exact Finset.mem_insert_of_mem (Finset.mem_union_left _ (IH₁ h₁₂))
    · exact Finset.mem_insert_of_mem (Finset.mem_union_right _ (IH₂ h₁₂))
  | goto l => subst h₁₂; exact h₀₁
  | halt => subst h₁₂; exact h₀₁
  | load _ q IH | _ _ _ q IH =>
    rcases h₁₂ with (rfl | h₁₂)
    · unfold stmts₁ at h₀₁
      exact h₀₁
    · exact Finset.mem_insert_of_mem (IH h₁₂)

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.land

Goal state after:
case gff
⊢ (false && false) = false

case f00
⊢ 0 &&& 0 = 0

case f0n
⊢ ∀ (n : PosNum), 0 &&& pos n = bif false && true then pos n else 0

case fn0
⊢ ∀ (n : PosNum), pos n &&& 0 = bif true && false then pos n else 0

case fnn
⊢ ∀ (m n : PosNum), pos m &&& pos n = m.land n

case p11
⊢ PosNum.land 1 1 = bif true && true then 1 else 0

case p1b
⊢ ∀ (b : Bool) (n : PosNum), PosNum.land 1 (PosNum.bit b n) = bit (true && b) (bif false && true then pos n else 0)

case pb1
⊢ ∀ (a : Bool) (m : PosNum), (PosNum.bit a m).land 1 = bit (a && true) (bif true && false then pos m else 0)

case pbb
⊢ ∀ (a b : Bool) (m n : PosNum), (PosNum.bit a m).land (PosNum.bit b n) = bit (a && b) (m.land n)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some
Γ : 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 Γ Λ σ
v : σ
L : ListBlank Γ
⊢ ∀ (q : Stmt Γ Λ σ) (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)))

Tactic:
intro q

Goal state after:
case some
Γ : 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 Γ Λ σ
v : σ
L : ListBlank Γ
q : Stmt Γ Λ σ
⊢ ∀ (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)))
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
apply castNum_eq_bitwise PosNum.lxor <;> intros

Goal state after:
case gff
⊢ (false != false) = false

case f00
⊢ 0 ^^^ 0 = 0

case f0n
n✝ : PosNum
⊢ 0 ^^^ pos n✝ = bif false != true then pos n✝ else 0

case fn0
n✝ : PosNum
⊢ pos n✝ ^^^ 0 = bif true != false then pos n✝ else 0

case fnn
m✝ n✝ : PosNum
⊢ pos m✝ ^^^ pos n✝ = m✝.lxor n✝

case p11
⊢ PosNum.lxor 1 1 = bif true != true then 1 else 0

case p1b
b✝ : Bool
n✝ : PosNum
⊢ PosNum.lxor 1 (PosNum.bit b✝ n✝) = bit (true != b✝) (bif false != true then pos n✝ else 0)

case pb1
a✝ : Bool
m✝ : PosNum
⊢ (PosNum.bit a✝ m✝).lxor 1 = bit (a✝ != true) (bif true != false then pos m✝ else 0)

case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).lxor (PosNum.bit b✝ n✝) = bit (a✝ != b✝) (m✝.lxor n✝)
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 → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
⊢ ∀ (q : Stmt Γ Λ σ),
    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')

Tactic:
intro q

Goal state after:
Γ : 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
q : Stmt Γ Λ σ
⊢ 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')
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case write.inr
Γ : 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
f : Γ → σ → Γ
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.write f q)
hw : ∀ (q' : Λ' Γ Λ σ), (∃ a, Λ'.write a q = q') ∨ q' ∈ writes q → q' ∈ trSupp M S
IH : SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
q' : Λ' Γ Λ σ
hq : q' ∈ writes q
⊢ SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
· exact IH.2 _ hq

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

Goal state before:
pp: case pos.zero.bit0
m : PosNum
⊢ false = (↑m.bit0).testBit 0

Tactic:
rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_zero]

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P✝¹ : TopCat → Prop
α : Type w
inst✝³ : Finite α
X : α → CompHausLike P✝¹
inst✝² : HasExplicitFiniteCoproduct X
P✝ : TopCat → Prop
inst✝¹ : HasExplicitFiniteCoproducts P✝
P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
n : ℕ
F : Discrete (Fin n) ⥤ CompHausLike P
⊢ PreservesColimit F (compHausLikeToTop P)

Tactic:
suffices PreservesColimit (Discrete.functor (F.obj ∘ Discrete.mk)) (compHausLikeToTop P) from
    preservesColimit_of_iso_diagram _ Discrete.natIsoFunctor.symm

Goal state after:
P✝¹ : TopCat → Prop
α : Type w
inst✝³ : Finite α
X : α → CompHausLike P✝¹
inst✝² : HasExplicitFiniteCoproduct X
P✝ : TopCat → Prop
inst✝¹ : HasExplicitFiniteCoproducts P✝
P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
n : ℕ
F : Discrete (Fin n) ⥤ CompHausLike P
⊢ PreservesColimit (Discrete.functor (F.obj ∘ Discrete.mk)) (compHausLikeToTop P)
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
X Y B : CompHausLike P
f : X ⟶ B
g : Y ⟶ B
inst✝ : HasExplicitPullback f g
Z : CompHausLike P
a b : Z ⟶ pullback f g
hfst : a ≫ fst f g = b ≫ fst f g
hsnd : a ≫ snd f g = b ≫ snd f g
⊢ a = b

Tactic:
ext z
  apply_fun (fun q ↦ q z) at hfst hsnd
  apply Subtype.ext
  apply Prod.ext
  · exact hfst
  · exact hsnd

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

Goal state before:
pp: case succ
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
IH :
  Reaches₀ (TM1.step (tr M))
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
    { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
⊢ some (TM1.stepAux (tr M (ret q)) v ((Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)))) =
    some { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }

Tactic:
rw [Option.some_inj, tr, TM1.stepAux, Tape.move_right_n_head, Tape.mk'_nth_nat,
      addBottom_nth_succ_fst, TM1.stepAux, iterate_succ', Function.comp_apply, Tape.move_right_left]

Goal state after:
case succ
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
IH :
  Reaches₀ (TM1.step (tr M))
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
    { l := some (ret q), var := v, Tape := Tape.mk' ∅ (addBottom L) }
⊢ (bif false then
      TM1.stepAux (trNormal q) v (Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))))
    else TM1.stepAux (goto fun x x_1 ↦ ret q) v ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)))) =
    { l := some (ret q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
x✝ : Epi (Sigma.desc π)
e : Function.Surjective ⇑(ConcreteCategory.hom (Sigma.desc π))
i : ∐ X ≅ finiteCoproduct X :=
  (colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X)
t : ↑(∐ X).toTop
q : (fun X ↦ ↑X.toTop) (finiteCoproduct X) := (ConcreteCategory.hom i.hom) t
this : t = (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) t)
⊢ (ConcreteCategory.hom (π q.fst)) q.snd = (ConcreteCategory.hom (Sigma.desc π)) t

Tactic:
rw [this]

Goal state after:
α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
x✝ : Epi (Sigma.desc π)
e : Function.Surjective ⇑(ConcreteCategory.hom (Sigma.desc π))
i : ∐ X ≅ finiteCoproduct X :=
  (colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X)
t : ↑(∐ X).toTop
q : (fun X ↦ ↑X.toTop) (finiteCoproduct X) := (ConcreteCategory.hom i.hom) t
this : t = (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) t)
⊢ (ConcreteCategory.hom (π q.fst)) q.snd =
    (ConcreteCategory.hom (Sigma.desc π)) ((ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) t))
Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
x✝ : Epi (Sigma.desc π)
e : Function.Surjective ⇑(ConcreteCategory.hom (Sigma.desc π))
i : ∐ X ≅ finiteCoproduct X :=
  (colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X)
t : ↑(∐ X).toTop
q : (fun X ↦ ↑X.toTop) (finiteCoproduct X) := (ConcreteCategory.hom i.hom) t
this✝ : t = (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) t)
this : i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π
⊢ (ConcreteCategory.hom (π q.fst)) q.snd =
    (ConcreteCategory.hom (i.inv ≫ Sigma.desc π)) ((ConcreteCategory.hom i.hom) t)

Tactic:
rw [this]

Goal state after:
α : Type
inst✝ : Finite α
B : CompHaus
X : α → CompHaus
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_3_to_2 : (∀ (b : ↑B.toTop), ∃ a x, (ConcreteCategory.hom (π a)) x = b) → Epi (Sigma.desc π)
x✝ : Epi (Sigma.desc π)
e : Function.Surjective ⇑(ConcreteCategory.hom (Sigma.desc π))
i : ∐ X ≅ finiteCoproduct X :=
  (colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X)
t : ↑(∐ X).toTop
q : (fun X ↦ ↑X.toTop) (finiteCoproduct X) := (ConcreteCategory.hom i.hom) t
this✝ : t = (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) t)
this : i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π
⊢ (ConcreteCategory.hom (π q.fst)) q.snd =
    (ConcreteCategory.hom (finiteCoproduct.desc X π)) ((ConcreteCategory.hom i.hom) t)
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
hxU : x ∈ U
⊢ IsOpen[inst✝³] U → ∃ v ∈ fun U ↦ IsClosed[inst✝³] U ∧ IsOpen[inst✝³] U, x ∈ v ∧ v ⊆ U

Tactic:
U_op

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hxU : x ∈ U
U_op : IsOpen[inst✝³] U
⊢ ∃ v ∈ fun U ↦ IsClosed[inst✝³] U ∧ IsOpen[inst✝³] U, x ∈ v ∧ v ⊆ U
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: 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)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
⊢ stepRet k₀ v₀ ∈ step (stepNormal f Cont.halt v'.tail)

Tactic:
rw [e₀]

Goal state after:
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)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
⊢ stepRet k₀ v₀ ∈ step (Cfg.ret k₀ v₀)
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✝³] (range fun x ↦ ↑↑x)

Tactic:
rw [this]

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
this : (range fun x ↦ ↑↑x) = interior s
⊢ IsOpen[inst✝³] (interior s)