mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ {x | ¬u = v ∧ (¬x = u → x = v)} = ∅ ∨ {x | ¬u = v ∧ (¬x = u → x = v)}.card = 2

Tactic:
right

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ {x | ¬u = v ∧ (¬x = u → x = v)}.card = 2
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h✝ : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
v : V
hv : v ∈ Set.univ \ G.universalVerts
h : v ∉ M1.verts
⊢ v ∈ M1.verts ∪ M2.verts

Tactic:
right

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h✝ : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⋯
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
v : V
hv : v ∈ Set.univ \ G.universalVerts
h : v ∉ M1.verts
⊢ v ∈ M2.verts
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
⊢ μ.rowLens.length = μ.colLen 0

Tactic:
simp only [rowLens, List.length_map, List.length_range]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
this : ∀ (m k : ℕ), n ≤ k + m → Acc (lbp p) k
⊢ ∀ (a : ℕ), Acc (lbp p) a

Tactic:
exact fun a => this _ _ (Nat.le_add_left _ _)

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a ↦ List.foldr (fun b s ↦ (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ (F a).2 = List.recOn (f a) (g a) fun b l IH ↦ h a (b, l, IH)

Tactic:
suffices F a = (f a, List.recOn (f a) (g a) fun b l IH => h a (b, l, IH)) by rw [this]
    dsimp [F]
    induction f a <;> simp [*]

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : DecidableEq α
a : α
ps : List (α × β)
⊢ (List.recOn (a, ps).2 none fun b l IH ↦
      bif ((a, ps), b, l, IH).1.1 == ((a, ps), b, l, IH).2.1.1 then some ((a, ps), b, l, IH).2.1.2
      else ((a, ps), b, l, IH).2.2.2) =
    List.lookup a ps

Tactic:
induction ps with

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case prec.succ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Nat.Partrec ↑f✝
pg : Nat.Partrec ↑g✝
n m : ℕ
IH :
  Nat.rec (f✝ (unpair n).1) (fun y IH ↦ g✝ (Nat.pair (unpair n).1 (Nat.pair y IH))) m ∈
    Nat.rec (Part.some (f✝ (unpair n).1))
      (fun y IH ↦ IH.bind fun i ↦ Part.some (g✝ (Nat.pair (unpair n).1 (Nat.pair y i)))) m
⊢ Nat.rec (f✝ (unpair n).1) (fun y IH ↦ g✝ (Nat.pair (unpair n).1 (Nat.pair y IH))) (m + 1) ∈
    Nat.rec (Part.some (f✝ (unpair n).1))
      (fun y IH ↦ IH.bind fun i ↦ Part.some (g✝ (Nat.pair (unpair n).1 (Nat.pair y i)))) (m + 1)

Tactic:
simp only [mem_bind_iff, mem_some_iff]
      exact ⟨_, IH, rfl⟩

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
n : ℕ
hn : ∀ (i : α), ‖↑(r i n) - b i * ↑n‖ ≤ ↑n / log ↑n ^ 2
i : α
h₁ : 0 ≤ b i
⊢ b i * ↑n - ↑(r i n) = ‖b i * ↑n‖ - ‖↑(r i n)‖

Tactic:
simp only [norm_mul, RCLike.norm_natCast, Real.norm_of_nonneg h₁]

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)
hgt : c₂ < c₁
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0

Tactic:
right

Goal state after:
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)
hgt : c₂ < c₁
⊢ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:

Tactic:
b i * n
            _ ≤ 1 * n := by have := R.b_lt_one i; gcongr
            _ = n := by rw [one_mul]

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

Goal state before:
pp: case inr
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 : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0

Tactic:
right

Goal state after:
case inr
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 : ℝ) in atTop, f x ≤ 0
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
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
n : ℕ
hn : ⌈(b i)⁻¹⌉₊ < n
hn' : 1 < n
h₁ : 0 < b i
⊢ 1 < ↑n

Tactic:
rw [Nat.one_lt_cast]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
n : ℕ
hn : ⌈(b i)⁻¹⌉₊ < n
hn' : 1 < n
h₁ : 0 < b i
⊢ 1 < n
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:

Tactic:
_ ≤ f x + ‖g x‖ := by gcongr; exact le_norm_self (g x)
           _ ≤ f x + (-1 / 2 * f x) := by gcongr
           _ = 1 / 2 * f x := by ring

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: case a.h.inl
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
a : List α
ha : a ∈ m
b : List α
hb : b ∈ l
ih : b ∈ m∗ * n
hx : a ++ b ∈ m * l
hal : 0 < a.length
⊢ a ++ b ∈ n + m * (m∗ * n)

Tactic:
right

Goal state after:
case a.h.inl
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
a : List α
ha : a ∈ m
b : List α
hb : b ∈ l
ih : b ∈ m∗ * n
hx : a ++ b ∈ m * l
hal : 0 < a.length
⊢ a ++ b ∈ m * (m∗ * n)
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
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf✝ : GrowsPolynomially fun x ↦ |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
⊢ ∃ c₂_1 > 0,
    ∀ᶠ (x : ℝ) in atTop,
      ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|⁻¹) u ∈ Set.Icc (c₂⁻¹ * (fun x ↦ |f x|⁻¹) x) (c₂_1 * (fun x ↦ |f x|⁻¹) x)

Tactic:
refine ⟨c₁⁻¹, by change 0 < c₁⁻¹; positivity, ?_⟩

Goal state after:
case inr
f : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf✝ : GrowsPolynomially fun x ↦ |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
⊢ ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|⁻¹) u ∈ Set.Icc (c₂⁻¹ * (fun x ↦ |f x|⁻¹) x) (c₁⁻¹ * (fun x ↦ |f x|⁻¹) x)
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: case pos.false
m n : ℕ
IH : shiftLeft' false m n ≠ 0 → (shiftLeft' false m n).size = m.size + n
h : ¬bit false 0 = 0
s0 : shiftLeft' false m n = 0
⊢ (size 0).succ = (m.size + n).succ

Tactic:
exact absurd rfl h

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
  · simp [List.getElem?_range kn]
  · rw [List.getElem?_eq_none]
    · cases e : evaln k c n
      · rfl
      exact kn.elim (evaln_bound e)
    simpa using kn

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

Goal state before:
pp: b : Bool
n : ℕ
hn : (∀ (i : ℕ), n.testBit i = false) → n = 0
h : ∀ (i : ℕ), (bit b n).testBit i = false
⊢ b = false

Tactic:
simpa using h 0

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

Goal state before:
pp: case inr.inl
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c

Tactic:
right

Goal state after:
case inr.inl
a b c : ℕ
v : ℕ := ⋯
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
⊢ c ^^^ a < b ∨ a ^^^ b < c
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inr.inr
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c

Tactic:
right

Goal state after:
case inr.inr
a b c : ℕ
v : ℕ := ⋯
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
⊢ c ^^^ a < b ∨ a ^^^ b < c
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inr.inr
a b c : ℕ
v : ℕ := ⋯
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
⊢ c ^^^ a < b ∨ a ^^^ b < c

Tactic:
right

Goal state after:
case inr.inr
a b c : ℕ
v : ℕ := ⋯
h✝ : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
⊢ a ^^^ b < c
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x y : List α
⊢ M.evalFrom S (x ++ y) = M.evalFrom (M.evalFrom S x) y

Tactic:
simp only [evalFrom, List.foldl_append]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: case mp.inr
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom T x
⊢ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T

Tactic:
right

Goal state after:
case mp.inr
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom T x
⊢ x ∈ M.acceptsFrom T
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit1.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn (m.cmp n).swap Ordering.lt Ordering.lt Ordering.gt

Tactic:
cases cmp m n

Goal state after:
case bit1.bit0.lt
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.lt Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn Ordering.lt.swap Ordering.lt Ordering.lt Ordering.gt

case bit1.bit0.eq
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.eq Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn Ordering.eq.swap Ordering.lt Ordering.lt Ordering.gt

case bit1.bit0.gt
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.gt Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn Ordering.gt.swap Ordering.lt Ordering.lt Ordering.gt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit0.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn (m.cmp n).swap Ordering.lt Ordering.gt Ordering.gt

Tactic:
cases cmp m n

Goal state after:
case bit0.bit1.lt
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.lt Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn Ordering.lt.swap Ordering.lt Ordering.gt Ordering.gt

case bit0.bit1.eq
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.eq Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn Ordering.eq.swap Ordering.lt Ordering.gt Ordering.gt

case bit0.bit1.gt
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn Ordering.gt Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn Ordering.gt.swap Ordering.lt Ordering.gt Ordering.gt
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case step
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure S s✝
ih : ∃ t ∈ S, s✝ ∈ M.εClosure {t}
⊢ ∃ t ∈ S, t✝ ∈ M.εClosure {t}

Tactic:
obtain ⟨s, _, _⟩ := ih
      use s
      solve_by_elim [εClosure.step]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s : σ
S : Set σ
x : List α
⊢ s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x

Tactic:
by
  induction x using List.reverseRecOn generalizing s with
  | nil => apply mem_εClosure_iff_exists
  | append_singleton _ _ ih =>
    simp_rw [evalFrom_append_singleton, mem_stepSet_iff, ih]
    tauto

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
| base t =>

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

Goal state before:
pp: n : PosNum
this : (↑n.pred').succ = ↑n
p : PosNum
h : (↑p).succ = ↑n
⊢ ↑(Num.casesOn (pos p) 1 bit1) = (↑n + ↑n).pred

Tactic:
by rw [← h]; exact (Nat.succ_add p p).symm

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : PosNum), a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
intro a b
    transfer_rw
    apply lt_iff_le_not_ge

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
by
  ext a
  refine ⟨?_, εNFA.εClosure.base _⟩
  rintro (⟨_, h⟩ | ⟨_, _, h, _⟩)
  · exact h
  · cases h

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

Goal state before:
pp: m n : PosNum
⊢ Ordering.casesOn (m.cmp n) (m < n) (m = n) (n < m) → (m.cmp n = Ordering.eq ↔ m = n)

Tactic:
cases cmp m n

Goal state after:
case lt
m n : PosNum
⊢ Ordering.casesOn Ordering.lt (m < n) (m = n) (n < m) → (Ordering.lt = Ordering.eq ↔ m = n)

case eq
m n : PosNum
⊢ Ordering.casesOn Ordering.eq (m < n) (m = n) (n < m) → (Ordering.eq = Ordering.eq ↔ m = n)

case gt
m n : PosNum
⊢ Ordering.casesOn Ordering.gt (m < n) (m = n) (n < m) → (Ordering.gt = Ordering.eq ↔ m = n)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : PosNum
⊢ (m.cmp n).swap = Ordering.lt ↔ m.cmp n = Ordering.gt

Tactic:
cases cmp m n

Goal state after:
case lt
m n : PosNum
⊢ Ordering.lt.swap = Ordering.lt ↔ Ordering.lt = Ordering.gt

case eq
m n : PosNum
⊢ Ordering.eq.swap = Ordering.lt ↔ Ordering.eq = Ordering.gt

case gt
m n : PosNum
⊢ Ordering.gt.swap = Ordering.lt ↔ Ordering.gt = Ordering.gt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : Num
⊢ Ordering.casesOn (m.cmp n) (m < n) (m = n) (n < m) → (m.cmp n = Ordering.eq ↔ m = n)

Tactic:
cases cmp m n

Goal state after:
case lt
m n : Num
⊢ Ordering.casesOn Ordering.lt (m < n) (m = n) (n < m) → (Ordering.lt = Ordering.eq ↔ m = n)

case eq
m n : Num
⊢ Ordering.casesOn Ordering.eq (m < n) (m = n) (n < m) → (Ordering.eq = Ordering.eq ↔ m = n)

case gt
m n : Num
⊢ Ordering.casesOn Ordering.gt (m < n) (m = n) (n < m) → (Ordering.gt = Ordering.eq ↔ m = n)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : Num
⊢ (m.cmp n).swap = Ordering.lt ↔ m.cmp n = Ordering.gt

Tactic:
cases cmp m n

Goal state after:
case lt
m n : Num
⊢ Ordering.lt.swap = Ordering.lt ↔ Ordering.lt = Ordering.gt

case eq
m n : Num
⊢ Ordering.eq.swap = Ordering.lt ↔ Ordering.eq = Ordering.gt

case gt
m n : Num
⊢ Ordering.gt.swap = Ordering.lt ↔ Ordering.gt = Ordering.gt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.one.one
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
⊢ ↑(p 1 1) = Nat.bitwise g (Nat.bit true 0) (Nat.bit true 0)

Tactic:
rw [Nat.bitwise_bit gff]

Goal state after:
case pos.pos.one.one
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
⊢ ↑(p 1 1) = Nat.bit (g true true) (Nat.bitwise g 0 0)
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.one.bit1
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
n : PosNum
⊢ ↑(p 1 (PosNum.bit true n)) = Nat.bitwise g (Nat.bit true 0) (Nat.bit true ↑n)

Tactic:
rw [Nat.bitwise_bit gff]

Goal state after:
case pos.pos.one.bit1
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
n : PosNum
⊢ ↑(p 1 (PosNum.bit true n)) = Nat.bit (g true true) (Nat.bitwise g 0 ↑n)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case succ.zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
⊢ (modifyNth f (n + 1) L).nth 0 = L.nth 0

Tactic:
simp only [ListBlank.nth_zero, ListBlank.head_cons, ListBlank.modifyNth]

Goal state after: