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

Goal state before:
pp: k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
⊢ n < k + 1

Tactic:
cases c <;> rw [evaln] at h

Goal state after:
case zero
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        pure 0)
      n
⊢ n < k + 1

case succ
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        pure n.succ)
      n
⊢ n < k + 1

case left
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        pure (unpair n).1)
      n
⊢ n < k + 1

case right
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        pure (unpair n).2)
      n
⊢ n < k + 1

case pair
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        Nat.pair <$> evaln (k + 1) a✝¹ n <*> evaln (k + 1) a✝ n)
      n
⊢ n < k + 1

case comp
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        let x ← evaln (k + 1) a✝ n
        evaln (k + 1) a✝¹ x)
      n
⊢ n < k + 1

case prec
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a n ↦
              Nat.casesOn n (evaln (k + 1) a✝¹ a) fun y ↦ do
                let i ← evaln k (a✝¹.prec a✝) (Nat.pair a y)
                evaln (k + 1) a✝ (Nat.pair a (Nat.pair y i)))
            n)
      n
⊢ n < k + 1

case rfind'
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝ : Code
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a m ↦ do
              let x ← evaln (k + 1) a✝ (Nat.pair a m)
              if x = 0 then pure m else evaln k a✝.rfind' (Nat.pair a (m + 1)))
            n)
      n
⊢ n < k + 1
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hf : GrowsPolynomially f
hfg : g =o[atTop] f
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun x ↦ f x + g x) u ∈ Set.Icc (c₁ * (fun x ↦ f x + g x) x) (c₂ * (fun x ↦ f x + g x) x)

Tactic:
isLittleO_iff

Goal state after:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hfg : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ c * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun x ↦ f x + g x) u ∈ Set.Icc (c₁ * (fun x ↦ f x + g x) x) (c₂ * (fun x ↦ f x + g x) x)
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ),
    Nat.rec (evaln (k + 1) cf (unpair n).1)
          (fun n_1 n_ih ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          m =
        some x →
      x ∈ Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i))) m
x : ℕ
⊢ ∀ (x_1 : ℕ),
    evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some x_1 →
      evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m x_1)) = some x →
        ∃
          a ∈
            Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
              m,
          x ∈ cg.eval (Nat.pair (unpair n).1 (Nat.pair m a))

Tactic:
refine fun y h₁ h₂ => ⟨y, IH _ ?_, ?_⟩
        · have := evaln_mono k.le_succ h₁
          simp [evaln, Option.bind_eq_some_iff] at this
          exact this.2
        · exact hg _ _ h₂

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
⊢ x ∈ c.eval n

Tactic:
induction c generalizing x n <;> simp [eval, evaln, Option.bind_eq_some_iff, Seq.seq] at h ⊢ <;>
      obtain ⟨_, h⟩ := h
    iterate 4 simpa [pure, PFun.pure, eq_comm] using h
    case pair cf cg hf hg _ =>
      rcases h with ⟨y, ef, z, eg, rfl⟩
      exact ⟨_, hf _ _ ef, _, hg _ _ eg, rfl⟩
    case comp cf cg hf hg _ =>
      rcases h with ⟨y, eg, ef⟩
      exact ⟨_, hg _ _ eg, hf _ _ ef⟩
    case prec cf cg hf hg _ =>
      revert h
      induction n.unpair.2 generalizing x with simp [Option.bind_eq_some_iff]
      | zero => apply hf
      | succ m IH =>
        refine fun y h₁ h₂ => ⟨y, IH _ ?_, ?_⟩
        · have := evaln_mono k.le_succ h₁
          simp [evaln, Option.bind_eq_some_iff] at this
          exact this.2
        · exact hg _ _ h₂
    case rfind' cf hf _ =>
      rcases h with ⟨m, h₁, h₂⟩
      by_cases m0 : m = 0 <;> simp [m0] at h₂
      · exact
          ⟨0, ⟨by simpa [m0] using hf _ _ h₁, fun {m} => (Nat.not_lt_zero _).elim⟩, by simp [h₂]⟩
      · have := evaln_sound h₂
        simp [eval] at this
        rcases this with ⟨y, ⟨hy₁, hy₂⟩, rfl⟩
        refine
          ⟨y + 1, ⟨by simpa [add_comm, add_left_comm] using hy₁, fun {i} im => ?_⟩, by
            simp [add_comm, add_left_comm]⟩
        rcases i with - | i
        · exact ⟨m, by simpa using hf _ _ h₁, m0⟩
        · rcases hy₂ (Nat.lt_of_succ_lt_succ im) with ⟨z, hz, z0⟩
          exact ⟨z, by simpa [add_comm, add_left_comm] using hz, z0⟩

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

Goal state before:
pp: case h₂
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
⊢ ‖g u‖ ≤ -(1 / 2 * f u)

Tactic:
rwa [← neg_mul, ← neg_div]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case f
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
cg : Primrec fun a ↦ a.2.2.1
| fun p ↦
    (fun a x ↦ do
        let y ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2
        some (Nat.pair x y))
      p.1 p.2

Tactic:
ext p

Goal state after:
case f
a : Primrec fun a ↦ ofNat (ℕ × Code) a.length
k✝¹ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.length).1
n✝¹ : Primrec Prod.snd
k✝ : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).1
n✝ : Primrec fun a ↦ a.1.2
k' : Primrec Prod.snd
c : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a ↦ a.1.1.1
k : Primrec fun a ↦ (ofNat (ℕ × Code) a.1.1.1.length).1
n : Primrec fun a ↦ a.1.1.2
cf : Primrec fun a ↦ a.2.1
cg : Primrec fun a ↦ a.2.2.1
p : (((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) × ℕ
| (fun a x ↦ do
      let y ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2
      some (Nat.pair x y))
    p.1 p.2
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
⊢ ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.accepts

Tactic:
use a, b, c, hx, hlen, hnil

Goal state after:
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
⊢ {a} * {b}∗ * {c} ≤ M.accepts
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Tendsto ((fun n ↦ 1 + ε n) ∘ Nat.cast) atTop (𝓝 1)

Tactic:
exact Tendsto.comp isEquivalent_one_add_smoothingFn_one.tendsto_const
        tendsto_natCast_atTop_atTop

Goal state after:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n x : ℕ
⊢ (x + x + 1) / 2 = x

Tactic:
rw [← two_mul, add_comm]

Goal state after:
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n x : ℕ
⊢ (1 + 2 * x) / 2 = x
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
⊢ bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n)

Tactic:
by
  conv_lhs => unfold bitwise
  simp only [bit, Bool.cond_eq_ite]
  have h4 x : (x + x + 1) / 2 = x := by rw [← two_mul, add_comm]; simp [add_mul_div_left]
  cases a <;> cases b <;> simp <;> split_ifs
    <;> simp_all +decide [two_mul]

Goal state after:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: f : Bool → Bool → Bool
⊢ bitwise (swap f) = swap (bitwise f)

Tactic:
funext m n

Goal state after:
f : Bool → Bool → Bool
m n : ℕ
⊢ bitwise (swap f) m n = swap (bitwise f) m n
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s u : σ
x y : List (Option α)
⊢ M.IsPath s u (x ++ y) → ∃ t, M.IsPath s t x ∧ M.IsPath t u y

Tactic:
induction x generalizing s with
    | nil =>
      rw [List.nil_append]
      tauto
    | cons x a ih =>
      rintro (_ | ⟨t, _, _, _, _, _, h⟩)
      apply ih at h
      tauto

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

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n : PosNum
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
rw [← not_lt]; exact not_congr cast_lt

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

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n : Num
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
rw [← not_lt]; exact not_congr cast_lt

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
⊢ ∃ k, Partrec k ∧ ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)

Tactic:
let k' (a : α) := (k (encode a)).bind fun n => (decode (α := σ) n : Part σ)

Goal state after:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a ↦ Part.map encode (g a)).Dom)
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
⊢ ∃ k, Partrec k ∧ ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case tail
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ c₁ d₁ : σ₁
a✝ : TransGen (fun a b ↦ b ∈ f₁ a) a₁ c₁
cd : d₁ ∈ f₁ c₁
c₂ : σ₂
cc : tr c₁ c₂
ac₂ : Reaches₁ f₂ a₂ c₂
this :
  match f₁ c₁ with
  | some b₁ => ∃ b₂, tr b₁ b₂ ∧ Reaches₁ f₂ c₂ b₂
  | none => f₂ c₂ = none
⊢ ∃ b₂, tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂

Tactic:
show f₁ c₁ = _ from cd

Goal state after:
case tail
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ c₁ d₁ : σ₁
a✝ : TransGen (fun a b ↦ b ∈ f₁ a) a₁ c₁
cd : d₁ ∈ f₁ c₁
c₂ : σ₂
cc : tr c₁ c₂
ac₂ : Reaches₁ f₂ a₂ c₂
this :
  match some d₁ with
  | some b₁ => ∃ b₂, tr b₁ b₂ ∧ Reaches₁ f₂ c₂ b₂
  | none => f₂ c₂ = none
⊢ ∃ b₂, tr d₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

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

Tactic:
exact TransGen.head rfl (IH _ _)

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

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

Tactic:
exact TransGen.head rfl (IH _ _)

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

Goal state before:
pp: case some.branch.true
Γ : 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
⊢ Reaches₁ (TM0.step (tr M)) { q := (some (TM1.Stmt.branch p a✝¹ a✝), v), Tape := T }
    {
      q :=
        (match (bif true then TM1.stepAux a✝¹ v T else TM1.stepAux a✝ v T).l with
          | some x => some (M x)
          | none => none,
          (bif true then TM1.stepAux a✝¹ v T else TM1.stepAux a✝ v T).var),
      Tape := (bif true then TM1.stepAux a✝¹ v T else TM1.stepAux a✝ v T).Tape }

Tactic:
· exact (reaches₁_eq (by simp only [TM0.step, tr, trAux, e]; rfl)).2 (IH₁ _ _)

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
l₁ l₂ l₂' : List Bool
e : l₂'.length = l₂.length
⊢ stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
    stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')

Tactic:
induction l₂ generalizing l₁ l₂' with
  | nil => cases List.length_eq_zero_iff.1 e; rfl
  | cons a l₂ IH =>
    rcases l₂' with - | ⟨b, l₂'⟩ <;>
      simp only [List.length_nil, List.length_cons, Nat.succ_inj, reduceCtorEq] at e
    rw [List.reverseAux, ← IH (a :: l₁) l₂' e]
    simp [stepAux, ListBlank.append, write]

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
f : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
⊢ ∀ (f : List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux n f) v
        (Tape.mk' (L.flatMap (fun x ↦ (enc x).toList.reverse) ⋯)
          (ListBlank.append (enc a).toList (R.flatMap (fun x ↦ (enc x).toList) ⋯))) =
      stepAux (f (enc a)) v
        (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.flatMap (fun x ↦ (enc x).toList.reverse) ⋯))
          (R.flatMap (fun x ↦ (enc x).toList) ⋯))

Tactic:
suffices ∀ i f L' R' l₁ l₂ h,
      stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, h⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R') by
    intro f
    exact this n f (L.flatMap (fun x => (enc x).1.reverse) _)
      (R.flatMap (fun x => (enc x).1) _) [] _ (enc a).2

Goal state after:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
f : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
⊢ ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ) (L' R' : ListBlank Bool) (l₁ l₂ : List Bool)
    (h : l₂.length = i),
    stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, h⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case comp
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, (a✝.then k').eval v = a✝.eval v >>= k'.eval
v : List ℕ
⊢ ((comp a✝¹ a✝).then k').eval v = (comp a✝¹ a✝).eval v >>= k'.eval

Tactic:
| comp _ _ k_ih =>

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

Goal state before:
pp: case pos
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
h✝ : v.headI = 0
⊢ (stepRet a✝ v.tail).then k' = (stepRet a✝ v.tail).then k'

pp: case neg
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
h✝ : ¬v.headI = 0
⊢ stepNormal a✝¹ (Cont.fix a✝¹ (a✝.then k')) v.tail = (stepNormal a✝¹ (Cont.fix a✝¹ a✝) v.tail).then k'

Tactic:
· rw [← k_ih]

Goal state after:
case neg
k' : Cont
a✝¹ : Code
a✝ : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a✝.then k') v = (stepRet a✝ v).then k'
v : List ℕ
h✝ : ¬v.headI = 0
⊢ stepNormal a✝¹ (Cont.fix a✝¹ (a✝.then k')) v.tail = (stepNormal a✝¹ (Cont.fix a✝¹ a✝) v.tail).then k'
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case mpr
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr✝ : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v)

Tactic:
refine PFun.fixInduction he fun v (he : v' ∈ f.fix.eval v) IH => ?_

Goal state after:
case mpr
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he✝ : v' ∈ f.fix.eval v✝
hr✝ : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v)
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: case mpr
X Y : Profinite
f : X ⟶ Y
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f

Tactic:
rw [← CategoryTheory.ofHom_epi_iff_surjective]
    apply (forget Profinite).epi_of_epi_map

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
S : DiscreteQuotient X
x : X
⊢ IsClopen (ofPred (S.toSetoid x))

Tactic:
rw [← fiber_eq]
  apply isClopen_preimage

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
A : DiscreteQuotient X
B B' : DiscreteQuotient Y
cond : LEComap f A B
h : B ≤ B'
a : Quotient A.toSetoid
⊢ ofLE h (map f cond a) = map f ⋯ a

Tactic:
rcases a with ⟨⟩
  rfl

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
H₁ : ∀ (Q₁ Q₂ : DiscreteQuotient X), Q₁ ≤ Q₂ → Q₁.proj ⁻¹' {Qs Q₁} ⊆ Q₂.proj ⁻¹' {Qs Q₂}
⊢ ∃ x, ∀ (Q : DiscreteQuotient X), Q.proj x = Qs Q

Tactic:
obtain ⟨x, hx⟩ : Set.Nonempty (⋂ Q, proj Q ⁻¹' {Qs Q}) :=
    IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
      (fun Q : DiscreteQuotient X => Q.proj ⁻¹' {Qs _}) (directed_of_isDirected_ge H₁)
      (fun Q => (singleton_nonempty _).preimage Q.proj_surjective)
      (fun Q => (Q.isClosed_preimage {Qs _}).isCompact) fun Q => Q.isClosed_preimage _

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
H₁ : ∀ (Q₁ Q₂ : DiscreteQuotient X), Q₁ ≤ Q₂ → Q₁.proj ⁻¹' {Qs Q₁} ⊆ Q₂.proj ⁻¹' {Qs Q₂}
x : X
hx : x ∈ ⋂ Q, Q.proj ⁻¹' {Qs Q}
⊢ ∃ x, ∀ (Q : DiscreteQuotient X), Q.proj x = Qs Q
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
⊢ ∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W

Tactic:
have hp : Continuous (fun y : Y ↦ (a.1, y)) := .prodMk_right _

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous[inst✝¹, instTopologicalSpaceProd] fun y ↦ (a.1, y)
⊢ ∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W