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

Goal state before:
pp: f g : ℝ → ℝ
hg✝ : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun x ↦ ‖g x‖) x) (c₄ * (fun x ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
hg_bound : ∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ b * x ≤ 1 * x

Tactic:
gcongr; exact le_of_lt hb.2

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

Goal state before:
pp: case mp
α : Type u_1
l : List (Option α)
⊢ (∀ (a : Option α), a ∈ l → id a = none) → ∃ n, l = replicate n none

pp: case mpr
α : Type u_1
l : List (Option α)
⊢ (∃ n, l = replicate n none) → ∀ (a : Option α), a ∈ l → id a = none

Tactic:
· intro h
    exact ⟨l.length, eq_replicate_of_mem h⟩

Goal state after:
case mpr
α : Type u_1
l : List (Option α)
⊢ (∃ n, l = replicate n none) → ∀ (a : Option α), a ∈ l → id a = none
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length = l.length ↔ ∀ (x : Option α), x ∈ l → x.isSome = true

Tactic:
rw [reduceOption_length_eq, List.length_filter_eq_length_iff]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case nil.mp
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h✝ : M.IsPath s₁ s₂ (List.replicate n none)
⊢ ∃ x', x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x'

Tactic:
use List.replicate n none

Goal state after:
case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h✝ : M.IsPath s₁ s₂ (List.replicate n none)
⊢ (List.replicate n none).reduceOption = [] ∧ M.IsPath s₁ s₂ (List.replicate n none)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : Num
⊢ ↑↑n = ↑n

Tactic:
← to_nat_to_int,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
n : Num
⊢ ↑↑↑n = ↑n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : ℕ
⊢ ↑↑(n + 1) = n + 1

Tactic:
Nat.cast_succ,

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

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : σ
⊢ a ∈ M.toεNFA.εClosure S ↔ a ∈ S

Tactic:
refine ⟨?_, εNFA.εClosure.base _⟩

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : σ
⊢ a ∈ M.toεNFA.εClosure S → a ∈ S
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: p : PosNum
⊢ ↑(pos p).pred = (↑(pos p)).pred

Tactic:
rw [pred, PosNum.pred'_to_nat]; rfl

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

Goal state before:
pp: Γ : Type ?u.5
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
⊢ { l // BlankExtends l₁ l ∧ BlankExtends l₂ l }

Tactic:
refine
    if hl : l₁.length ≤ l₂.length then ⟨l₂, Or.elim h id fun h' ↦ ?_, BlankExtends.refl _⟩
    else ⟨l₁, BlankExtends.refl _, Or.elim h (fun h' ↦ ?_) id⟩

Goal state after:
case refine_1
Γ : Type ?u.5
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
hl : l₁.length ≤ l₂.length
h' : BlankExtends l₂ l₁
⊢ BlankExtends l₁ l₂

case refine_2
Γ : Type ?u.5
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
hl : ¬l₁.length ≤ l₂.length
h' : BlankExtends l₁ l₂
⊢ BlankExtends l₂ l₁
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refine_1.none
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
e : f a = none
⊢ Reaches f a b ∧ f b = none

Tactic:
rw [Part.mem_unique h
          (PFun.mem_fix_iff.2 <| Or.inl <| Part.mem_some_iff.2 <| by rw [e]; rfl)]
      exact ⟨ReflTransGen.refl, e⟩

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ₁ σ₂ : Type u_1
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
H : Respects f₁ f₂ fun a b ↦ tr a = b
a₁ : σ₁
b₂ : σ₂
h✝ : b₂ ∈ tr <$> eval f₁ a₁
b₁ : σ₁
ab : b₁ ∈ eval f₁ a₁
bb : tr b₁ = b₂
h : tr b₁ ∈ eval f₂ (tr a₁)
⊢ b₂ ∈ eval f₂ (tr a₁)

Tactic:
bb

Goal state after:
σ₁ σ₂ : Type u_1
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
H : Respects f₁ f₂ fun a b ↦ tr a = b
a₁ : σ₁
b₂ : σ₂
h✝ : b₂ ∈ tr <$> eval f₁ a₁
b₁ : σ₁
ab : b₁ ∈ eval f₁ a₁
bb : tr b₁ = b₂
h : b₂ ∈ eval f₂ (tr a₁)
⊢ b₂ ∈ eval f₂ (tr a₁)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ (branch p q₁ q₂)
⊢ q₀ ∈ stmts₁ (branch p q₁ q₂)

Tactic:
(
    simp only [stmts₁] at h₁₂ ⊢
    simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂)

Goal state after:
case branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ = branch p q₁ q₂ ∨ q₁✝ ∈ stmts₁ q₁ ∨ q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
l : Γ → σ → Λ
h₁₂ : q₁ ∈ stmts₁ (goto l)
⊢ q₀ ∈ stmts₁ (goto l)

Tactic:
(
    simp only [stmts₁] at h₁₂ ⊢
    simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂)

Goal state after:
case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
l : Γ → σ → Λ
h₁₂ : q₁ = goto l
⊢ q₀ ∈ {goto l}
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

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

Tactic:
(
    simp only [stmts₁] at h₁₂ ⊢
    simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂)

Goal state after:
case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
h₁₂ : q₁ = halt
⊢ q₀ ∈ {halt}
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case move
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Dir
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ (move a✝ q)
⊢ q₀ ∈ stmts₁ (move a✝ q)

Tactic:
(
    simp only [stmts₁] at h₁₂ ⊢
    simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂)

Goal state after:
case move
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Dir
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ = move a✝ q ∨ q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (move a✝ q) (stmts₁ q)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ (write a✝ q)
⊢ q₀ ∈ stmts₁ (write a✝ q)

Tactic:
(
    simp only [stmts₁] at h₁₂ ⊢
    simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂)

Goal state after:
case write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ = write a✝ q ∨ q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (write a✝ q) (stmts₁ q)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case load
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Γ → σ → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ (load a✝ q)
⊢ q₀ ∈ stmts₁ (load a✝ q)

Tactic:
(
    simp only [stmts₁] at h₁₂ ⊢
    simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂)

Goal state after:
case load
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Γ → σ → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ = load a✝ q ∨ q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (load a✝ q) (stmts₁ q)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : Tape Γ
x✝ : Stmt Γ Λ σ
⊢ SupportsStmt S x✝ → (stepAux x✝ v T).l ∈ Finset.insertNone S

Tactic:
induction M l₁ generalizing v T with

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

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

Tactic:
induction M l₁ generalizing v T with

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

Goal state before:
pp: Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
n : ℕ
e : Γ ≃ Fin n
this : DecidableEq Γ := e.decidableEq
G : Fin n ↪ Fin n → Bool := { toFun := fun a b ↦ decide (a = b), inj' := ⋯ }
H : Γ ↪ List.Vector Bool n := (e.toEmbedding.trans G).trans (Equiv.vectorEquivFin Bool n).symm.toEmbedding
enc : Γ ↪ List.Vector Bool n := H.setValue default (List.Vector.replicate n false)
⊢ ∃ n enc dec, enc default = List.Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a

Tactic:
exact ⟨_, enc, Function.invFun enc, H.setValue_eq _ _, Function.leftInverse_invFun enc.2⟩

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

Goal state before:
pp: case branch
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₁' → (stepAux q₁' v T).l ∈ Finset.insertNone S
IH₂ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₂' → (stepAux q₂' v T).l ∈ Finset.insertNone S
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt S (branch p q₁' q₂')
⊢ (stepAux (branch p q₁' q₂') v T).l ∈ Finset.insertNone S

Tactic:
unfold stepAux; cases p v
      · exact IH₂ _ _ hs.2
      · exact IH₁ _ _ hs.1

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

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : (k : K) → List (Γ k)
x✝ : Stmt Γ Λ σ
⊢ SupportsStmt S x✝ → (stepAux x✝ v T).l ∈ Finset.insertNone S

Tactic:
induction M l₁ generalizing v T with

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case mpr.cons.cons.nil
α : 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)
U : List (List α)
hsum : a :: x = ([] :: U).flatten
helem : ([] ≠ [] ∧ P.rmatch [] = true) ∧ ∀ a ∈ U, a ≠ [] ∧ P.rmatch a = true
⊢ ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ P.star.rmatch u = true

Tactic:
simp only [not_true, Ne, false_and] at helem

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

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

Tactic:
apply castNum_eq_bitwise fun x y => pos (PosNum.lor x y) <;>
    (try rintro (_ | _)) <;> (try rintro (_ | _)) <;> intros <;> rfl

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

Goal state before:
pp: m n : ℕ
f : List.Vector ℕ n →. ℕ
g : Fin n → List.Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
cg : Code
hg : ∀ (v : List.Vector ℕ m), cg.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v
cf : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval ↑v = pure <$> f v
v : List.Vector ℕ m
⊢ (cf.comp cg).eval ↑v = pure <$> ((Vector.mOfFn fun i ↦ g i v) >>= f)

Tactic:
simp [hg, hf, map_bind]
        rfl

Goal state after:
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)
⊢ TrCfg (TM2.init k L) (TM1.init (trInit k L))

Tactic:
(_ : TM1.init _ = _)

Goal state after:
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)
⊢ TrCfg (TM2.init k L) ?m.33

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)
⊢ TM1.init (trInit k L) = ?m.33
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
⊢ IsOpen[inst✝³] (Subtype.val '' V)

Tactic:
have f1 : IsOpenEmbedding ((↑) : u → H) := by
      refine ⟨f0, ?_⟩
      · have : Set.range ((↑) : u → H) = interior s := by
          rw [this, Set.range_comp, Subtype.range_coe, Subtype.image_preimage_coe]
          apply Set.inter_eq_self_of_subset_right interior_subset
        rw [this]
        apply isOpen_interior

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
⊢ IsOpen[inst✝³] (Subtype.val '' V)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

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

pp: 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

Tactic:
· subst k'
      simp only [Function.update_self]
      rw [ListBlank.nth_mk, List.getI_eq_getElem?_getD, ← List.map_reverse, List.getElem?_map]

Goal state after:
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.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = (a :: L₁, o, L₂)
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (bif
        match (S k).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (S k).head?, stk := update S k (S k).tail }
    else { l := some (Λ'.clear p k q), var := (S k).head?, stk := update S k (S k).tail })
    { l := some q, var := o, stk := update S k L₂ }

Tactic:
rcases e₁ : S k with - | ⟨a', Sk⟩ <;> rw [e₁, splitAtPred] at e

Goal state after:
case cons.nil
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
e : ([], none, []) = (a :: L₁, o, L₂)
e₁ : S k = []
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (bif
        match [].head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := [].head?, stk := update S k [].tail }
    else { l := some (Λ'.clear p k q), var := [].head?, stk := update S k [].tail })
    { l := some q, var := o, stk := update S k L₂ }

case cons.cons
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := o, stk := update S k L₂ }
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e :
  (bif p a' then ([], some a', Sk)
    else
      match splitAtPred p Sk with
      | (l₁, o, l₂) => (a' :: l₁, o, l₂)) =
    (a :: L₁, o, L₂)
e₁ : S k = a' :: Sk
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail }
    else { l := some (Λ'.clear p k q), var := (a' :: Sk).head?, stk := update S k (a' :: Sk).tail })
    { l := some q, var := o, stk := update S k L₂ }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.succ
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₂
s : Option Γ'
tail✝ : List ℕ
n : ℕ
⊢ if n + 1 = 0 then
    natEnd ((trNum ↑(n + 1) ++ Γ'.cons :: trList tail✝).head?.getD default) = true ∧
      (trNum ↑(n + 1) ++ Γ'.cons :: trList tail✝).tail = trList ((n + 1) :: tail✝).tail
  else
    natEnd ((trNum ↑(n + 1) ++ Γ'.cons :: trList tail✝).head?.getD default) = false ∧
      (trNum ↑(n + 1) ++ Γ'.cons :: trList tail✝).tail =
        (trNum ↑(n + 1)).tail ++ Γ'.cons :: trList ((n + 1) :: tail✝).tail

Tactic:
Nat.cast_succ,

Goal state after:
case cons.succ
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₂
s : Option Γ'
tail✝ : List ℕ
n : ℕ
⊢ if n + 1 = 0 then
    natEnd ((trNum (↑n + 1) ++ Γ'.cons :: trList tail✝).head?.getD default) = true ∧
      (trNum (↑n + 1) ++ Γ'.cons :: trList tail✝).tail = trList ((n + 1) :: tail✝).tail
  else
    natEnd ((trNum (↑n + 1) ++ Γ'.cons :: trList tail✝).head?.getD default) = false ∧
      (trNum (↑n + 1) ++ Γ'.cons :: trList tail✝).tail =
        (trNum (↑n + 1)).tail ++ Γ'.cons :: trList ((n + 1) :: tail✝).tail
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: X Y : LightProfinite
f✝ : X ⟶ Y
A B : LightProfinite
f : A ⟶ B
hf : IsIso ((forget LightProfinite).map f)
⊢ IsIso f

Tactic:
rw [isIso_iff_bijective] at hf

Goal state after:
X Y : LightProfinite
f✝ : X ⟶ Y
A B : LightProfinite
f : A ⟶ B
hf : Function.Bijective ⇑(ConcreteCategory.hom ((forget LightProfinite).map f))
⊢ IsIso f
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
⊢ Supports (codeSupp' (f.cons fs) k) S

Tactic:
have H' := H

Goal state after:
case cons
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Supports (codeSupp' fs k) S
k : Cont'
H H' : codeSupp (f.cons fs) k ⊆ S
⊢ Supports (codeSupp' (f.cons fs) k) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case comp
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Supports (codeSupp' g k) S
k : Cont'
H : codeSupp (f.comp g) k ⊆ S
⊢ Supports (codeSupp' (f.comp g) k) S

Tactic:
have H' := H

Goal state after:
case comp
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Supports (codeSupp' g k) S
k : Cont'
H H' : codeSupp (f.comp g) k ⊆ S
⊢ Supports (codeSupp' (f.comp g) k) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case case
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Supports (codeSupp' g k) S
k : Cont'
H : codeSupp (f.case g) k ⊆ S
⊢ Supports (codeSupp' (f.case g) k) S

Tactic:
have H' := H

Goal state after:
case case
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Supports (codeSupp' g k) S
k : Cont'
H H' : codeSupp (f.case g) k ⊆ S
⊢ Supports (codeSupp' (f.case g) k) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case fix
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
⊢ Supports (codeSupp' f.fix k) S

Tactic:
have H' := H

Goal state after:
case fix
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
k : Cont'
H H' : codeSupp f.fix k ⊆ S
⊢ Supports (codeSupp' f.fix k) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons₂
S : Finset Λ'
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp k.cons₂ ⊆ S
⊢ Supports (contSupp k.cons₂) S

Tactic:
have H' := H

Goal state after:
case cons₂
S : Finset Λ'
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H H' : contSupp k.cons₂ ⊆ S
⊢ Supports (contSupp k.cons₂) S