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

Goal state before:
pp: f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b, a ≤ b ∧ f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
ih : ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑k - 1) * x₀) (2 ^ (-↑k) * x₀) → f z = 0
z : ℝ
hxz : x ≤ z
hz : z ∈ Set.Icc (2 ^ (-(↑k + 1) - 1) * x₀) (2 ^ (-(↑k + 1)) * x₀)
⊢ z ≤ 2 ^ (-↑k - 1) * x₀

Tactic:
simp only [neg_add, ← sub_eq_add_neg] at hz

Goal state after:
f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b, a ≤ b ∧ f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
ih : ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑k - 1) * x₀) (2 ^ (-↑k) * x₀) → f z = 0
z : ℝ
hxz : x ≤ z
hz : z ∈ Set.Icc (2 ^ (-↑k - 1 - 1) * x₀) (2 ^ (-↑k - 1) * x₀)
⊢ z ≤ 2 ^ (-↑k - 1) * x₀
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc : ¬Fintype.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x y : ↑K.supp
hxy : x ≠ y ∧ ¬Gmax.deleteUniversalVerts.coe.Adj ↑x ↑y
p : K.toSimpleGraph.Walk x y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x y
⊢ False

Tactic:
obtain ⟨x, a, b, hxa, hxb, hnadjxb, hnxb⟩ := Walk.exists_adj_adj_not_adj_ne hp.2
      (p.reachable.one_lt_dist_of_ne_of_not_adj hxy.1 hxy.2)

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc : ¬Fintype.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x✝ y : ↑K.supp
hxy : x✝ ≠ y ∧ ¬Gmax.deleteUniversalVerts.coe.Adj ↑x✝ ↑y
p : K.toSimpleGraph.Walk x✝ y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x✝ y
x a b : ↥K
hxa : K.toSimpleGraph.Adj x a
hxb : K.toSimpleGraph.Adj a b
hnadjxb : ¬K.toSimpleGraph.Adj x b
hnxb : x ≠ b
⊢ False
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case hf
⊢ Partrec fun p ↦ (pappAck p.1).eval p.2

pp: case H
⊢ ∀ (n : ℕ × ℕ), ack n.1 n.2 ∈ (pappAck n.1).eval n.2

Tactic:
· change Partrec₂ (fun m n => (pappAck m).eval n)
    apply_rules only
      [Code.eval_part.comp₂, Computable.fst, Computable.snd, primrec_pappAck.to_comp.comp]

Goal state after:
case H
⊢ ∀ (n : ℕ × ℕ), ack n.1 n.2 ∈ (pappAck n.1).eval n.2
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
⊢ (∃ M, M.IsPerfectMatching) → ∀ (u : Set V), ¬G.IsTutteViolator u

Tactic:
rintro ⟨M, hM⟩; apply not_isTutteViolator_of_isPerfectMatching hM

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

Goal state before:
pp: ⊢ StrictAntiOn ε (Set.Ioi 1)

Tactic:
change StrictAntiOn (fun x => 1 / log x) (Set.Ioi 1)
  simp_rw [one_div]
  refine StrictAntiOn.comp_strictMonoOn inv_strictAntiOn ?log fun _ hx => log_pos hx
  refine StrictMonoOn.mono strictMonoOn_log (fun x hx => ?_)
  exact Set.Ioi_subset_Ioi zero_le_one hx

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

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
heq : c₁ = c₂
c : ℝ
hc✝ : ∀ᶠ (x : ℝ) in atTop, f x = c
hpos : 0 ≤ c
a✝ : ℝ
hc : f a✝ = c
⊢ 0 ≤ f a✝

Tactic:
simpa only [hc]

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

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
heq : c₁ = c₂
c : ℝ
hc✝ : ∀ᶠ (x : ℝ) in atTop, f x = c
hneg : c < 0
x : ℝ
hc : f x = c
⊢ f x < 0

Tactic:
simpa only [hc]

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

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hg✝ : GrowsPolynomially g
hf' : 0 ≤ᶠ[atTop] f
hg' : 0 ≤ᶠ[atTop] g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
left✝ : c₄ > 0
hg : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
⊢ min c₁ c₃ > 0

Tactic:
by change 0 < min c₁ c₃; positivity

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: c₁ c₂ : Code
n₁ n₂ : ℕ
h : c₁.curry n₁ = c₂.curry n₂
⊢ c₁ = c₂

Tactic:
by injection h

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

Goal state before:
pp: f g : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hg✝¹ : GrowsPolynomially g
hf'✝ : 0 ≤ᶠ[atTop] f
hg'✝ : 0 ≤ᶠ[atTop] g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
left✝ : c₄ > 0
hg✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hg : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
hf' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ f y
hg' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ g y
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
fx_nonneg : 0 ≤ f x
gx_nonneg : 0 ≤ g x
⊢ max c₂ c₄ * f x + max c₂ c₄ * g x ≥ c₂ * f x + c₄ * g x

Tactic:
gcongr
                                    · exact le_max_left _ _
                                    · exact le_max_right _ _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
⊢ ↑n ^ p a b * ↑n * (1 - c₃) * (c₂ * g ↑n / (c₁ * ↑n) ^ (p a b + 1)) =
    ↑n ^ p a b * ↑n * (1 - c₃) * (c₂ * g ↑n / (c₁ ^ (p a b + 1) * ↑n ^ (p a b + 1)))

Tactic:
rw [Real.mul_rpow (by positivity) (by positivity)]

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
⊢ 1 * n ≤ m * l + n

Tactic:
one_mul,

Goal state after:
case a.zero
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
⊢ n ≤ m * l + n
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
⊢ g.reverse.Derives u.reverse.reverse v.reverse.reverse ↔ g.reverse.Derives u v

Tactic:
List.reverse_reverse,

Goal state after:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
⊢ g.reverse.Derives u v.reverse.reverse ↔ g.reverse.Derives u v
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
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound2 : ∀ (i : α), b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))
h_smoothing_pos : 0 < 1 + ε ↑n
h_sumTransform : ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
h_smoothing_gt_half : 1 / 2 < 1 - ε ↑n
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
n₀_div_le_n : ⌈↑n₀ / b'⌉₊ ≤ n
h_exp : ⌈rexp 1⌉₊ ≤ n
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁
h_ind : ∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
this : 1 + ε ↑n < 2
⊢ c₁ * 2 ≤ C

Tactic:
mul_comm,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound2 : ∀ (i : α), b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))
h_smoothing_pos : 0 < 1 + ε ↑n
h_sumTransform : ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
h_smoothing_gt_half : 1 / 2 < 1 - ε ↑n
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
n₀_div_le_n : ⌈↑n₀ / b'⌉₊ ≤ n
h_exp : ⌈rexp 1⌉₊ ≤ n
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁
h_ind : ∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
this : 1 + ε ↑n < 2
⊢ 2 * c₁ ≤ C
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
mod_two_iff_bod : ∀ (x : ℕ), decide (x % 2 = 1) = x.bodd
⊢ (if n = 0 then if f false true = true then m else 0
    else
      if m = 0 then if f true false = true then n else 0
      else
        have n' := n / 2;
        have m' := m / 2;
        let b₁ := n % 2 = 1;
        let b₂ := m % 2 = 1;
        have r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bit (f n.bodd m.bodd) (bitwise f (n / 2) (m / 2))

Tactic:
simp [hn, hm, mod_two_iff_bod, bit, two_mul]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: k : ℕ
c : Code
n : ℕ
⊢ ((List.range k)[n]?.bind fun a ↦ evaln k c a) = evaln k c n

Tactic:
by_cases kn : n < k

Goal state after:
case pos
k : ℕ
c : Code
n : ℕ
kn : n < k
⊢ ((List.range k)[n]?.bind fun a ↦ evaln k c a) = evaln k c n

case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ ((List.range k)[n]?.bind fun a ↦ evaln k c a) = evaln k c n
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 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 y)

Tactic:
bit_div_two,

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 x y) =
    ⋯ ▸
      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 y)
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inr.false
n i j : ℕ
hij : i ≠ j
h : n.testBit i = false
⊢ (n &&& 2 ^ i).testBit j = (false.toNat * 2 ^ i).testBit j

Tactic:
simp [testBit_two_pow_of_ne hij]

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

Goal state before:
pp: case inr.true
n i j : ℕ
hij : i ≠ j
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit j = (true.toNat * 2 ^ i).testBit j

Tactic:
simp [testBit_two_pow_of_ne hij]

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

Goal state before:
pp: n i : ℕ
⊢ 2 ^ i &&& n = 2 ^ i * (n.testBit i).toNat

Tactic:
mul_comm,

Goal state after:
n i : ℕ
⊢ 2 ^ i &&& n = (n.testBit i).toNat * 2 ^ i
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: a b c : ℕ
h : a < b ^^^ c
⊢ a ^^^ c < b ∨ a ^^^ b < c

Tactic:
by
  obtain ha | hb | hc := xor_trichotomy <| Nat.xor_assoc _ _ _ ▸ xor_ne_zero_iff.2 h.ne
  exacts [(h.asymm ha).elim, Or.inl <| Nat.xor_comm _ _ ▸ hb, Or.inr hc]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case step
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {s₁} s✝
ih : ∃ n, M.IsPath s₁ s✝ (List.replicate n none)
⊢ ∃ n, M.IsPath s₁ t✝ (List.replicate n none)

Tactic:
obtain ⟨n, _⟩ := ih
      use n + 1
      rw [List.replicate_add, isPath_append]
      tauto

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

Goal state before:
pp: p : PosNum
⊢ castNum <$> some p.pred' = (↑(pos p)).ppred

Tactic:
Option.map_eq_map,

Goal state after:
p : PosNum
⊢ Option.map castNum (some p.pred') = (↑(pos p)).ppred
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
⊢ GrowsPolynomially f

Tactic:
have : f = g + (f - g) := by ext; simp

Goal state after:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
this : f = g + (f - g)
⊢ GrowsPolynomially f
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
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a ∈ f a_2, encode a = x) ∨
          ∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a ∈ g a_2, encode a = x) ∧
      ((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)
⊢ (↑(decode ((k (encode a)).get hk))).Dom

Tactic:
obtain ⟨a', _, y, _, e⟩ | ⟨a', _, y, _, e⟩ := (H _).1 _ ⟨hk, rfl⟩

Goal state after:
case inl
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk✝ : Nat.Partrec k
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a ∈ f a_2, encode a = x) ∨
          ∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a ∈ g a_2, encode a = x) ∧
      ((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)
a' : α
left✝¹ : decode₂ α (encode a) = Option.some a'
y : σ
left✝ : y ∈ f a'
e : encode y = (k (encode a)).get hk
⊢ (↑(decode ((k (encode a)).get hk))).Dom

case inr
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk✝ : Nat.Partrec k
k' : α → Part σ := fun a ↦ (k (encode a)).bind fun n ↦ ↑(decode n)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a ∈ f a_2, encode a = x) ∨
          ∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a ∈ g a_2, encode a = x) ∧
      ((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)
a' : α
left✝¹ : decode₂ α (encode a) = Option.some a'
y : σ
left✝ : y ∈ g a'
e : encode y = (k (encode a)).get hk
⊢ (↑(decode ((k (encode a)).get hk))).Dom
Module: Mathlib.Computability.TuringMachine.Tape

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

Tactic:
apply_fun List.length at e

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

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
l : List Γ
⊢ Part.map (fun c ↦ c.Tape.right₀)
      (trCfg M <$> eval (TM1.step M) { l := some default, var := default, Tape := Tape.mk₁ l }) =
    TM1.eval M l

Tactic:
rw [Part.map_eq_map, Part.map_map, TM1.eval]

Goal state after:
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
l : List Γ
⊢ Part.map ((fun c ↦ c.Tape.right₀) ∘ trCfg M)
      (eval (TM1.step M) { l := some default, var := default, Tape := Tape.mk₁ l }) =
    Part.map (fun c ↦ c.Tape.right₀) (eval (TM1.step M) (TM1.init l))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
inst✝¹ : Inhabited Γ
inst✝ : Finite Γ
⊢ ∃ n enc dec, enc default = List.Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a

Tactic:
by
  rcases Finite.exists_equiv_fin Γ with ⟨n, ⟨e⟩⟩
  let : DecidableEq Γ := e.decidableEq
  let G : Fin n ↪ Fin n → Bool :=
    ⟨fun a b ↦ a = b, fun a b h ↦
      Bool.of_decide_true <| (congr_fun h b).trans <| Bool.decide_true rfl⟩
  let H := (e.toEmbedding.trans G).trans (Equiv.vectorEquivFin _ _).symm.toEmbedding
  let enc := H.setValue default (List.Vector.replicate n false)
  exact ⟨_, enc, Function.invFun enc, H.setValue_eq _ _, Function.leftInverse_invFun enc.2⟩

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

Goal state before:
pp: case nil
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ R'✝ : ListBlank Bool
l₂ : List Bool
e : (enc a).toList = [].reverseAux l₂
⊢ (Tape.move Dir.left)^[[].length] (Tape.mk' (ListBlank.append [] L'✝) (ListBlank.append l₂ R'✝)) =
    Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)

Tactic:
cases e; rfl

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

Goal state before:
pp: n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
m : PosNum
m✝ : ℕ
⊢ (m✝ + m✝).div2 = m✝

Tactic:
rw [Nat.div2_val]

Goal state after:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
m : PosNum
m✝ : ℕ
⊢ (m✝ + m✝) / 2 = m✝
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case prim.prec
n✝¹ : ℕ
f✝¹ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
a✝¹ : Nat.Primrec' f
a✝ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n + 1)
hf : cf.eval (↑v).tail = Part.some (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = Part.some (pure (g (a ::ᵥ b ::ᵥ v.tail)))
⊢ (cf.prec cg).eval (v.head :: (↑v).tail) =
    Part.some
      (pure
        (Nat.rec (f (v.head ::ᵥ v.tail).tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ (v.head ::ᵥ v.tail).tail))
          (v.head ::ᵥ v.tail).head))

Tactic:
simp only [← Part.pure_eq_some] at hf hg ⊢

Goal state after:
case prim.prec
n✝¹ : ℕ
f✝¹ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
a✝¹ : Nat.Primrec' f
a✝ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n + 1)
hf : cf.eval (↑v).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
⊢ (cf.prec cg).eval (v.head :: (↑v).tail) =
    pure
      (pure
        (Nat.rec (f (v.head ::ᵥ v.tail).tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ (v.head ::ᵥ v.tail).tail))
          (v.head ::ᵥ v.tail).head))