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

Goal state before:
pp: case succ.mpr
α : Type u_1
l : Language α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
x : List α
⊢ (∃ S, x = S.flatten ∧ S.length = n + 1 ∧ ∀ y ∈ S, y ∈ l) →
    ∃ a ∈ l, ∃ b, (∃ S, b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a ++ b = x

Tactic:
rintro ⟨_ | ⟨a, S⟩, rfl, hn, hS⟩ <;> cases hn
      rw [forall_mem_cons] at hS
      exact ⟨a, hS.1, _, ⟨S, rfl, rfl, hS.2⟩, rfl⟩

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
l : Language α
⊢ (map f) l∗ = ((map f) l)∗

Tactic:
by
  rw [kstar_eq_iSup_pow, kstar_eq_iSup_pow]
  simp_rw [← map_pow]
  exact image_iUnion

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l : Language α
⊢ 1 + l * l∗ = l∗

Tactic:
by
  simp only [kstar_eq_iSup_pow, mul_iSup, ← pow_succ', ← pow_zero l]
  exact sup_iSup_nat_succ _

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: case a.zero
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
⊢ m ^ 0 * n ≤ m * l + n

Tactic:
rw [pow_zero, one_mul, add_comm]
        exact le_self_add

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hvw : r.Rewrites u v
p : List (Symbol T N)
⊢ r.Rewrites (u ++ p) (v ++ p)

Tactic:
by
  rw [rewrites_iff] at *
  rcases hvw with ⟨x, y, hxy⟩
  use x, y ++ p
  simp_all

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

Goal state before:
pp: case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
⊢ GrowsPolynomially fun x ↦ (f x)⁻¹

Tactic:
| inr hf_pos_or_neg =>

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

Goal state before:
pp: case 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
y : ℕ
⊢ bitwise f (bit xb 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) (bit xb x) y

Tactic:
simp_rw [binaryRec_of_ne_zero _ _ hxb, bodd_bit, div2_bit, eq_rec_constant]

Goal state after:
case 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
y : ℕ
⊢ 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
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 1
⊢ (match 1 with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) ^^^
      n + 1 =
    match 1 + Fin.ofNat 4 1 with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0

Tactic:
Nat.xor_comm

Goal state after:
n : ℕ
ih :
  List.foldl (fun x1 x2 ↦ x1 ^^^ x2) 0 (List.range (n + 1)) =
    match Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0
h : Fin.ofNat 4 n = 1
⊢ (n + 1 ^^^
      match 1 with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) =
    match 1 + Fin.ofNat 4 1 with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0
Module: Mathlib.Computability.Encoding

Goal state before:
pp: case zero
⊢ decodeNum (encodeNum Num.zero) = Num.zero

Tactic:
unfold encodeNum decodeNum

Goal state after:
case zero
⊢ (if
        (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.zero
Module: Mathlib.Computability.Encoding

Goal state before:
pp: case pos
n : PosNum
⊢ decodeNum (encodeNum (Num.pos n)) = Num.pos n

Tactic:
unfold encodeNum decodeNum

Goal state after:
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.pos n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit true n + 1) = ofNat' (Nat.bit true n) + 1

Tactic:
show n.bit true + 1 = (n + 1).bit false by simp [Nat.bit, mul_add],

Goal state after:
case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit false (n + 1)) = ofNat' (Nat.bit true n) + 1
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
by rw [pred'_to_nat, succ'_to_nat, Nat.add_one, Nat.pred_succ]

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

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
m n : PosNum
⊢ ↑↑m + ↑↑n = ↑m + ↑n

Tactic:
cast_to_nat,

Goal state after:
α : Type u_1
inst✝ : AddMonoidWithOne α
m n : PosNum
⊢ ↑m + ↑↑n = ↑m + ↑n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
m n : PosNum
⊢ ↑↑m * ↑↑n = ↑m * ↑n

Tactic:
cast_to_nat,

Goal state after:
α : Type u_1
inst✝ : NonAssocSemiring α
m n : PosNum
⊢ ↑m * ↑↑n = ↑m * ↑n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
m n : Num
⊢ ↑↑m + ↑↑n = ↑m + ↑n

Tactic:
cast_to_nat,

Goal state after:
α : Type u_1
inst✝ : AddMonoidWithOne α
m n : Num
⊢ ↑m + ↑↑n = ↑m + ↑n
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: n m : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ n → List.Vector ℕ m
hf : Partrec' ↑f
hg : Vec g
i✝ : Fin m.succ
i : Fin m
⊢ Partrec' fun v ↦ ↑(some (((fun v ↦ f v ::ᵥ g v) v).get i.succ))

Tactic:
simp only [hg i, get_cons_succ]

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

Goal state before:
pp: case refine_1
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
h : l₁.length ≤ l₂.length
⊢ l₂.length = (l₁ ++ List.replicate (l₂.length - l₁.length) default).length

Tactic:
simp only [Nat.add_sub_cancel' h, List.length_append, List.length_replicate]

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ : σ₂
ab : Reaches f₂ a₂ b₂
⊢ ∃ c₁ c₂, Reaches f₂ b₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
induction ab with
  | refl => exact ⟨_, _, ReflTransGen.refl, aa, ReflTransGen.refl⟩
  | tail _ cd IH =>
    rcases IH with ⟨e₁, e₂, ce, ee, ae⟩
    rcases ReflTransGen.cases_head ce with (rfl | ⟨d', cd', de⟩)
    · have := H ee
      revert this
      rcases eg : f₁ e₁ with - | g₁ <;> simp only [and_imp, exists_imp]
      · intro c0
        cases cd.symm.trans c0
      · intro g₂ gg cg
        rcases TransGen.head'_iff.1 cg with ⟨d', cd', dg⟩
        cases Option.mem_unique cd cd'
        exact ⟨_, _, dg, gg, ae.tail eg⟩
    · cases Option.mem_unique cd cd'
      exact ⟨_, _, de, ee, ae⟩

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

Goal state before:
pp: case refine_2.inr
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), l₁.getI i = l₂.getI i
h✝ : l₁.length ≤ l₂.length
i : ℕ
h : i < l₂.length
h₂ : i < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length
h' : l₁.length ≤ i
⊢ default = l₂[i]

Tactic:
← List.getI_eq_default _ h',

Goal state after:
case refine_2.inr
Γ : Type u_1
i✝ : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i : ℕ), l₁.getI i = l₂.getI i
h✝ : l₁.length ≤ l₂.length
i : ℕ
h : i < l₂.length
h₂ : i < (l₁ ++ List.replicate (l₂.length - l₁.length) default).length
h' : l₁.length ≤ i
⊢ l₁.getI i = l₂[i]
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → Prop
f : α → β
c : Computable f
g : β → Bool
hg : Computable g
h₂ : ComputablePred fun a ↦ g a = true
hf : ∀ (a : α), p a ↔ (fun a ↦ g a = true) (f a)
⊢ Computable fun a ↦ decide ((fun a ↦ (fun a ↦ g a = true) (f a)) a)

Tactic:
simpa using hg.comp c

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

Goal state before:
pp: case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
i : ℕ
IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
T : Tape Bool
⊢ stepAux ((Stmt.move d)^[i] q) v (Tape.move d T) = stepAux q v ((Tape.move d)^[i] (Tape.move d T))

Tactic:
rw [IH]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case neg.mpr.nil
α : 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
h : a :: x = [] ++ u
hP : P.rmatch [] = true
⊢ ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true

Tactic:
contradiction

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case mp.cons
α : 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)
⊢ P.star.rmatch (a :: x) = true → ∃ S, a :: x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
· rw [rmatch, deriv, mul_rmatch_iff]
        rintro ⟨t, u, hs, ht, hu⟩
        have hwf : u.length < (List.cons a x).length := by
          rw [hs, List.length_cons, List.length_append]
          lia
        rw [IH _ hwf] at hu
        rcases hu with ⟨S', hsum, helem⟩
        use (a :: t) :: S'
        constructor
        · simp [hs, hsum]
        · intro t' ht'
          cases ht' with
          | head ht' =>
            simp only [ne_eq, not_false_iff, true_and, rmatch, reduceCtorEq]
            exact ht
          | tail _ ht' => exact helem t' ht'

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
x : List α
⊢ P.star.rmatch x = true ↔ ∃ S, x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
by
    have IH := fun t (_h : List.length t < List.length x) => star_rmatch_iff P t
    clear star_rmatch_iff
    constructor
    · rcases x with - | ⟨a, x⟩
      · intro _h
        use []; dsimp; tauto
      · rw [rmatch, deriv, mul_rmatch_iff]
        rintro ⟨t, u, hs, ht, hu⟩
        have hwf : u.length < (List.cons a x).length := by
          rw [hs, List.length_cons, List.length_append]
          lia
        rw [IH _ hwf] at hu
        rcases hu with ⟨S', hsum, helem⟩
        use (a :: t) :: S'
        constructor
        · simp [hs, hsum]
        · intro t' ht'
          cases ht' with
          | head ht' =>
            simp only [ne_eq, not_false_iff, true_and, rmatch, reduceCtorEq]
            exact ht
          | tail _ ht' => exact helem t' ht'
    · rintro ⟨S, hsum, helem⟩
      rcases x with - | ⟨a, x⟩
      · rfl
      · rw [rmatch, deriv, mul_rmatch_iff]
        rcases S with - | ⟨t', U⟩
        · exact ⟨[], [], by tauto⟩
        · obtain - | ⟨b, t⟩ := t'
          · simp only [forall_eq_or_imp, List.mem_cons] at helem
            simp only [not_true, Ne, false_and] at helem
          simp only [List.flatten_cons, List.cons_append, List.cons_eq_cons] at hsum
          refine ⟨t, U.flatten, hsum.2, ?_, ?_⟩
          · specialize helem (b :: t) (by simp)
            rw [rmatch] at helem
            convert! helem.2
            exact hsum.1
          · grind

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

Goal state before:
pp: case gff
⊢ (false && false) = false

Tactic:
(try cases_type* Bool)

Goal state after:
case gff
⊢ (false && false) = false
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f00
⊢ 0 &&& 0 = 0

Tactic:
(try cases_type* Bool)

Goal state after:
case f00
⊢ 0 &&& 0 = 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f0n
n✝ : PosNum
⊢ 0 &&& pos n✝ = bif false && true then pos n✝ else 0

Tactic:
(try cases_type* Bool)

Goal state after:
case f0n
n✝ : PosNum
⊢ 0 &&& pos n✝ = bif false && true then pos n✝ else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fn0
n✝ : PosNum
⊢ pos n✝ &&& 0 = bif true && false then pos n✝ else 0

Tactic:
(try cases_type* Bool)

Goal state after:
case fn0
n✝ : PosNum
⊢ pos n✝ &&& 0 = bif true && false then pos n✝ else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn
m✝ n✝ : PosNum
⊢ pos m✝ &&& pos n✝ = m✝.land n✝

Tactic:
(try cases_type* Bool)

Goal state after:
case fnn
m✝ n✝ : PosNum
⊢ pos m✝ &&& pos n✝ = m✝.land n✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p11
⊢ PosNum.land 1 1 = bif true && true then 1 else 0

Tactic:
(try cases_type* Bool)

Goal state after:
case p11
⊢ PosNum.land 1 1 = bif true && true then 1 else 0
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
R S : RegularExpression α
⊢ (map f (R * S)).matches' = (Language.map f) (R * S).matches'

Tactic:
by simp [matches'_map]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
R : RegularExpression α
⊢ (map f R.star).matches' = (Language.map f) R.star.matches'

Tactic:
by simp [matches'_map]

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

Goal state before:
pp: case p1b
b✝ : Bool
n✝ : PosNum
⊢ PosNum.land 1 (PosNum.bit b✝ n✝) = bit (true && b✝) (bif false && true then pos n✝ else 0)

Tactic:
(try cases_type* Bool)

Goal state after:
case p1b.false
n✝ : PosNum
⊢ PosNum.land 1 (PosNum.bit false n✝) = bit (true && false) (bif false && true then pos n✝ else 0)

case p1b.true
n✝ : PosNum
⊢ PosNum.land 1 (PosNum.bit true n✝) = bit (true && true) (bif false && true then pos n✝ else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1
a✝ : Bool
m✝ : PosNum
⊢ (PosNum.bit a✝ m✝).land 1 = bit (a✝ && true) (bif true && false then pos m✝ else 0)

Tactic:
(try cases_type* Bool)

Goal state after:
case pb1.false
m✝ : PosNum
⊢ (PosNum.bit false m✝).land 1 = bit (false && true) (bif true && false then pos m✝ else 0)

case pb1.true
m✝ : PosNum
⊢ (PosNum.bit true m✝).land 1 = bit (true && true) (bif true && false then pos m✝ else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).land (PosNum.bit b✝ n✝) = bit (a✝ && b✝) (m✝.land n✝)

Tactic:
(try cases_type* Bool)

Goal state after:
case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).land (PosNum.bit false n✝) = bit (false && false) (m✝.land n✝)

case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).land (PosNum.bit true n✝) = bit (false && true) (m✝.land n✝)

case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).land (PosNum.bit false n✝) = bit (true && false) (m✝.land n✝)

case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).land (PosNum.bit true n✝) = bit (true && true) (m✝.land n✝)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case gff
⊢ (false && !false) = false

Tactic:
(try cases_type* Bool)

Goal state after:
case gff
⊢ (false && !false) = false
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f00
⊢ ldiff 0 0 = 0

Tactic:
(try cases_type* Bool)

Goal state after:
case f00
⊢ ldiff 0 0 = 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f0n
n✝ : PosNum
⊢ ldiff 0 (pos n✝) = bif false && !true then pos n✝ else 0

Tactic:
(try cases_type* Bool)

Goal state after:
case f0n
n✝ : PosNum
⊢ ldiff 0 (pos n✝) = bif false && !true then pos n✝ else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fn0
n✝ : PosNum
⊢ (pos n✝).ldiff 0 = bif true && !false then pos n✝ else 0

Tactic:
(try cases_type* Bool)

Goal state after:
case fn0
n✝ : PosNum
⊢ (pos n✝).ldiff 0 = bif true && !false then pos n✝ else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn
m✝ n✝ : PosNum
⊢ (pos m✝).ldiff (pos n✝) = m✝.ldiff n✝

Tactic:
(try cases_type* Bool)

Goal state after:
case fnn
m✝ n✝ : PosNum
⊢ (pos m✝).ldiff (pos n✝) = m✝.ldiff n✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p11
⊢ PosNum.ldiff 1 1 = bif true && !true then 1 else 0

Tactic:
(try cases_type* Bool)

Goal state after:
case p11
⊢ PosNum.ldiff 1 1 = bif true && !true then 1 else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p1b
b✝ : Bool
n✝ : PosNum
⊢ PosNum.ldiff 1 (PosNum.bit b✝ n✝) = bit (true && !b✝) (bif false && !true then pos n✝ else 0)

Tactic:
(try cases_type* Bool)

Goal state after:
case p1b.false
n✝ : PosNum
⊢ PosNum.ldiff 1 (PosNum.bit false n✝) = bit (true && !false) (bif false && !true then pos n✝ else 0)

case p1b.true
n✝ : PosNum
⊢ PosNum.ldiff 1 (PosNum.bit true n✝) = bit (true && !true) (bif false && !true then pos n✝ else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pb1
a✝ : Bool
m✝ : PosNum
⊢ (PosNum.bit a✝ m✝).ldiff 1 = bit (a✝ && !true) (bif true && !false then pos m✝ else 0)

Tactic:
(try cases_type* Bool)

Goal state after:
case pb1.false
m✝ : PosNum
⊢ (PosNum.bit false m✝).ldiff 1 = bit (false && !true) (bif true && !false then pos m✝ else 0)

case pb1.true
m✝ : PosNum
⊢ (PosNum.bit true m✝).ldiff 1 = bit (true && !true) (bif true && !false then pos m✝ else 0)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case push
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
⊢ ∃ L',
    (∀ (k_1 : K), ListBlank.map (proj k_1) L' = ListBlank.mk (List.map some (update S k (f v :: S k) k_1)).reverse) ∧
      TM1.stepAux q v
          (Tape.move Dir.right
            (Tape.write
              (((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))).head.1,
                update ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))).head.2 k (some (f v)))
              ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))))) =
        TM1.stepAux q v ((Tape.move Dir.right)^[(f v :: S k).length] (Tape.mk' ∅ (addBottom L')))

Tactic:
refine
      ⟨_, fun k' ↦ ?_, by
        -- Porting note: `rw [...]` to `erw [...]; rfl`.
        -- https://github.com/leanprover-community/mathlib4/issues/5164
        rw [Tape.move_right_n_head, List.length, Tape.mk'_nth_nat, this]
        erw [addBottom_modifyNth fun a ↦ update a k (some (f v))]
        rw [Nat.add_one, iterate_succ']
        rfl⟩

Goal state after:
case push
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
k' : K
⊢ ListBlank.map (proj k') (ListBlank.modifyNth (fun a ↦ update a k (some (f v))) (S k).length L) =
    ListBlank.mk (List.map some (update S k (f v :: S k) k')).reverse
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).ldiff (PosNum.bit b✝ n✝) = bit (a✝ && !b✝) (m✝.ldiff n✝)

Tactic:
(try cases_type* Bool)

Goal state after:
case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).ldiff (PosNum.bit false n✝) = bit (false && !false) (m✝.ldiff n✝)

case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).ldiff (PosNum.bit true n✝) = bit (false && !true) (m✝.ldiff n✝)

case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).ldiff (PosNum.bit false n✝) = bit (true && !false) (m✝.ldiff n✝)

case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).ldiff (PosNum.bit true n✝) = bit (true && !true) (m✝.ldiff n✝)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case gff
⊢ (false != false) = false

Tactic:
(try cases_type* Bool)

Goal state after:
case gff
⊢ (false != false) = false
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case f00
⊢ 0 ^^^ 0 = 0

Tactic:
(try cases_type* Bool)

Goal state after:
case f00
⊢ 0 ^^^ 0 = 0
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
(try cases_type* Bool)

Goal state after:
case f0n
n✝ : PosNum
⊢ 0 ^^^ pos n✝ = bif false != true then pos n✝ else 0
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
(try cases_type* Bool)

Goal state after:
case fn0
n✝ : PosNum
⊢ pos n✝ ^^^ 0 = bif true != false then pos n✝ else 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case fnn
m✝ n✝ : PosNum
⊢ pos m✝ ^^^ pos n✝ = m✝.lxor n✝

Tactic:
(try cases_type* Bool)

Goal state after:
case fnn
m✝ n✝ : PosNum
⊢ pos m✝ ^^^ pos n✝ = m✝.lxor n✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case p11
⊢ PosNum.lxor 1 1 = bif true != true then 1 else 0

Tactic:
(try cases_type* Bool)

Goal state after:
case p11
⊢ PosNum.lxor 1 1 = bif true != true then 1 else 0
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
(try cases_type* Bool)

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

case p1b.true
n✝ : PosNum
⊢ PosNum.lxor 1 (PosNum.bit true n✝) = bit (true != true) (bif false != true then pos n✝ else 0)
Module: Mathlib.Data.Num.Lemmas

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

Tactic:
(try cases_type* Bool)

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

case pb1.true
m✝ : PosNum
⊢ (PosNum.bit true m✝).lxor 1 = bit (true != true) (bif true != false then pos m✝ else 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).lxor (PosNum.bit b✝ n✝) = bit (a✝ != b✝) (m✝.lxor n✝)

Tactic:
(try cases_type* Bool)

Goal state after:
case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).lxor (PosNum.bit false n✝) = bit (false != false) (m✝.lxor n✝)

case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).lxor (PosNum.bit true n✝) = bit (false != true) (m✝.lxor n✝)

case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).lxor (PosNum.bit false n✝) = bit (true != false) (m✝.lxor n✝)

case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).lxor (PosNum.bit true n✝) = bit (true != true) (m✝.lxor n✝)