awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
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 : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
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
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1) ≠ 0

Tactic:
positivity
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
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 : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
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
rw : (1 - c₃) * c₂ * g (↑n : ℝ) / c₁ ^ (p a b + 1) = (1 - c₃) * c₂ / c₁ ^ (p a b + 1) * g (↑n : ℝ)
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1) / HPow.hPow (α := ℝ) (↑n : ℝ) (p a b + 1) * (1 - c₃) * c₂ * g (↑n : ℝ) /
      c₁ ^ (p a b + 1) =
    (1 - c₃) * c₂ / c₁ ^ (p a b + 1) * g (↑n : ℝ)

Tactic:
rw [div_self (by positivity), one_mul]

Premises used: one_mul, div_self
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
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 : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
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
⊢ (1 - c₃) * c₂ * g (↑n : ℝ) / c₁ ^ (p a b + 1) = (1 - c₃) * c₂ / c₁ ^ (p a b + 1) * g (↑n : ℝ)

Tactic:
ring
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
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 : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
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
hbc : min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) ≤ (1 - c₃) * c₂ / c₁ ^ (p a b + 1)
⊢ (1 - c₃) * c₂ / c₁ ^ (p a b + 1) * g (↑n : ℝ) ≥ min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) * g (↑n : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
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 : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
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
⊢ min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) ≤ (1 - c₃) * c₂ / c₁ ^ (p a b + 1)

Tactic:
min_le_right _ _

Premises used: min_le_right
-- Module: Mathlib.Computability.AkraBazzi.SumTransform
Goal:
α : Type u_1
inst : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst_1 : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₁
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 : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) c₃
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
⊢ min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ (p a b + 1)) ≤ (1 - c₃) * c₂ / c₁ ^ (p a b + 1)

Tactic:
exact min_le_right _ _

Premises used: min_le_right
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v s : List (Symbol T N)
h :
  Symbol.nonterminal r.input :: s = HAppend.hAppend (α := List (Symbol T N)) [] [Symbol.nonterminal r.input] ++ s ∧
    r.output ++ s = [] ++ r.output ++ s
⊢ ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
    Symbol.nonterminal r.input :: s = p ++ [Symbol.nonterminal r.input] ++ q ∧ r.output ++ s = p ++ r.output ++ q

Tactic:
use [], s
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v s : List (Symbol T N)
⊢ Symbol.nonterminal r.input :: s = HAppend.hAppend (α := List (Symbol T N)) [] [Symbol.nonterminal r.input] ++ s ∧
    r.output ++ s = [] ++ r.output ++ s

Tactic:
simp
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
x : Symbol T N
s₁ s₂ : List (Symbol T N)
hrs : r.Rewrites s₁ s₂
ih :
  ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
    s₁ = p ++ [Symbol.nonterminal r.input] ++ q ∧ s₂ = p ++ r.output ++ q
cons :
  ∀ (p' q' : List (Symbol T N)),
    r.Rewrites (p' ++ [Symbol.nonterminal r.input] ++ q') (p' ++ r.output ++ q') →
      ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
        x :: (p' ++ [Symbol.nonterminal r.input] ++ q') = p ++ [Symbol.nonterminal r.input] ++ q ∧
          x :: (p' ++ r.output ++ q') = p ++ r.output ++ q
⊢ ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
    x :: s₁ = p ++ [Symbol.nonterminal r.input] ++ q ∧ x :: s₂ = p ++ r.output ++ q

Tactic:
rcases ih with ⟨p', q', rfl, rfl⟩

Premises used: rfl
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
x : Symbol T N
p' q' : List (Symbol T N)
hrs : r.Rewrites (p' ++ [Symbol.nonterminal r.input] ++ q') (p' ++ r.output ++ q')
h :
  x :: (p' ++ [Symbol.nonterminal r.input] ++ q') = x :: p' ++ [Symbol.nonterminal r.input] ++ q' ∧
    x :: (p' ++ r.output ++ q') = x :: p' ++ r.output ++ q'
⊢ ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
    x :: (p' ++ [Symbol.nonterminal r.input] ++ q') = p ++ [Symbol.nonterminal r.input] ++ q ∧
      x :: (p' ++ r.output ++ q') = p ++ r.output ++ q

Tactic:
use x :: p', q'
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
x : Symbol T N
p' q' : List (Symbol T N)
hrs : r.Rewrites (p' ++ [Symbol.nonterminal r.input] ++ q') (p' ++ r.output ++ q')
⊢ x :: (p' ++ [Symbol.nonterminal r.input] ++ q') = x :: p' ++ [Symbol.nonterminal r.input] ++ q' ∧
    x :: (p' ++ r.output ++ q') = x :: p' ++ r.output ++ q'

Tactic:
simp
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hr : r.Rewrites u v
head :
  ∀ (s : List (Symbol T N)),
    ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
      Symbol.nonterminal r.input :: s = p ++ [Symbol.nonterminal r.input] ++ q ∧ r.output ++ s = p ++ r.output ++ q
cons :
  ∀ (x : Symbol T N) {s₁ s₂ : List (Symbol T N)},
    r.Rewrites s₁ s₂ →
      ∀
        (ih :
          ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
            s₁ = p ++ [Symbol.nonterminal r.input] ++ q ∧ s₂ = p ++ r.output ++ q),
        ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
          x :: s₁ = p ++ [Symbol.nonterminal r.input] ++ q ∧ x :: s₂ = p ++ r.output ++ q
⊢ ∃ (p : List (Symbol T N)) (q : List (Symbol T N)), u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q

Tactic:
induction hr with
  | head s =>
    use [], s
    simp
  | cons x _ ih =>
    rcases ih with ⟨p', q', rfl, rfl⟩
    use x :: p', q'
    simp

Premises used: ContextFreeRule.Rewrites.head, ContextFreeRule.Rewrites.cons, rfl
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
⊢ r.Rewrites [Symbol.nonterminal r.input] r.output

Tactic:
simpa using head []

Premises used: ContextFreeRule.Rewrites.head, List.nil
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
q : List (Symbol T N)
⊢ r.Rewrites (HAppend.hAppend (α := List (Symbol T N)) [] [Symbol.nonterminal r.input] ++ q) ([] ++ r.output ++ q)

Tactic:
Rewrites.head q

Premises used: ContextFreeRule.Rewrites.head, List.append
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
q : List (Symbol T N)
⊢ r.Rewrites (HAppend.hAppend (α := List (Symbol T N)) [] [Symbol.nonterminal r.input] ++ q) ([] ++ r.output ++ q)

Tactic:
exact Rewrites.head q

Premises used: ContextFreeRule.Rewrites.head
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
q : List (Symbol T N)
d : Symbol T N
l : List (Symbol T N)
ih : r.Rewrites (l ++ [Symbol.nonterminal r.input] ++ q) (l ++ r.output ++ q)
⊢ r.Rewrites (d :: l ++ [Symbol.nonterminal r.input] ++ q) (d :: l ++ r.output ++ q)

Tactic:
Rewrites.cons d ih

Premises used: ContextFreeRule.Rewrites.cons, List.append
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
q : List (Symbol T N)
d : Symbol T N
l : List (Symbol T N)
ih : r.Rewrites (l ++ [Symbol.nonterminal r.input] ++ q) (l ++ r.output ++ q)
⊢ r.Rewrites (d :: l ++ [Symbol.nonterminal r.input] ++ q) (d :: l ++ r.output ++ q)

Tactic:
exact Rewrites.cons d ih

Premises used: ContextFreeRule.Rewrites.cons
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
p q : List (Symbol T N)
nil : r.Rewrites (HAppend.hAppend (α := List (Symbol T N)) [] [Symbol.nonterminal r.input] ++ q) ([] ++ r.output ++ q)
cons :
  ∀ (d : Symbol T N) (l : List (Symbol T N))
    (ih : r.Rewrites (l ++ [Symbol.nonterminal r.input] ++ q) (l ++ r.output ++ q)),
    r.Rewrites (d :: l ++ [Symbol.nonterminal r.input] ++ q) (d :: l ++ r.output ++ q)
⊢ r.Rewrites (p ++ [Symbol.nonterminal r.input] ++ q) (p ++ r.output ++ q)

Tactic:
induction p with
  | nil => exact Rewrites.head q
  | cons d l ih => exact Rewrites.cons d ih

Premises used: ContextFreeRule.Rewrites.head
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
p q : List (Symbol T N)
⊢ r.Rewrites (p ++ [Symbol.nonterminal r.input] ++ q) (p ++ r.output ++ q)

Tactic:
apply rewrites_of_exists_parts

Premises used: ContextFreeRule.rewrites_of_exists_parts
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
⊢ r.Rewrites u v → Symbol.nonterminal r.input ∈ u

Tactic:
simp +contextual [rewrites_iff, List.append_assoc]

Premises used: List.append_assoc, ContextFreeRule.rewrites_iff
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
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)
rw :
  ∀
    (hvw :
      ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
        u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q)
    (p : List (Symbol T N)),
    ∃ (p_1 : List (Symbol T N)) (q : List (Symbol T N)),
      p ++ u = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ p ++ v = p_1 ++ r.output ++ q
⊢ r.Rewrites (p ++ u) (p ++ v)

Tactic:
rw [rewrites_iff] at *

Premises used: ContextFreeRule.rewrites_iff
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hvw :
  ∃ (p : List (Symbol T N)) (q : List (Symbol T N)), u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q
p : List (Symbol T N)
rcases :
  ∀ (x y : List (Symbol T N)) (hxy : u = x ++ [Symbol.nonterminal r.input] ++ y ∧ v = x ++ r.output ++ y),
    ∃ (p_1 : List (Symbol T N)) (q : List (Symbol T N)),
      p ++ u = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ p ++ v = p_1 ++ r.output ++ q
⊢ ∃ (p_1 : List (Symbol T N)) (q : List (Symbol T N)),
    p ++ u = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ p ++ v = p_1 ++ r.output ++ q

Tactic:
rcases hvw with ⟨x, y, hxy⟩
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v p x y : List (Symbol T N)
hxy : u = x ++ [Symbol.nonterminal r.input] ++ y ∧ v = x ++ r.output ++ y
h : p ++ u = p ++ x ++ [Symbol.nonterminal r.input] ++ y ∧ p ++ v = p ++ x ++ r.output ++ y
⊢ ∃ (p_1 : List (Symbol T N)) (q : List (Symbol T N)),
    p ++ u = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ p ++ v = p_1 ++ r.output ++ q

Tactic:
use p ++ x, y
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v p x y : List (Symbol T N)
hxy : u = x ++ [Symbol.nonterminal r.input] ++ y ∧ v = x ++ r.output ++ y
⊢ p ++ u = p ++ x ++ [Symbol.nonterminal r.input] ++ y ∧ p ++ v = p ++ x ++ r.output ++ y

Tactic:
simp_all
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
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)
rw :
  ∀
    (hvw :
      ∃ (p : List (Symbol T N)) (q : List (Symbol T N)),
        u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q)
    (p : List (Symbol T N)),
    ∃ (p_1 : List (Symbol T N)) (q : List (Symbol T N)),
      u ++ p = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ v ++ p = p_1 ++ r.output ++ q
⊢ r.Rewrites (u ++ p) (v ++ p)

Tactic:
rw [rewrites_iff] at *

Premises used: ContextFreeRule.rewrites_iff
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hvw :
  ∃ (p : List (Symbol T N)) (q : List (Symbol T N)), u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q
p : List (Symbol T N)
rcases :
  ∀ (x y : List (Symbol T N)) (hxy : u = x ++ [Symbol.nonterminal r.input] ++ y ∧ v = x ++ r.output ++ y),
    ∃ (p_1 : List (Symbol T N)) (q : List (Symbol T N)),
      u ++ p = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ v ++ p = p_1 ++ r.output ++ q
⊢ ∃ (p_1 : List (Symbol T N)) (q : List (Symbol T N)),
    u ++ p = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ v ++ p = p_1 ++ r.output ++ q

Tactic:
rcases hvw with ⟨x, y, hxy⟩
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v p x y : List (Symbol T N)
hxy : u = x ++ [Symbol.nonterminal r.input] ++ y ∧ v = x ++ r.output ++ y
h : u ++ p = x ++ [Symbol.nonterminal r.input] ++ (y ++ p) ∧ v ++ p = x ++ r.output ++ (y ++ p)
⊢ ∃ (p_1 : List (Symbol T N)) (q : List (Symbol T N)),
    u ++ p = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ v ++ p = p_1 ++ r.output ++ q

Tactic:
use x, y ++ p
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v p x y : List (Symbol T N)
hxy : u = x ++ [Symbol.nonterminal r.input] ++ y ∧ v = x ++ r.output ++ y
⊢ u ++ p = x ++ [Symbol.nonterminal r.input] ++ (y ++ p) ∧ v ++ p = x ++ r.output ++ (y ++ p)

Tactic:
simp_all
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
w : List T
⊢ w ∈ g.language ↔ g.Derives [Symbol.nonterminal g.initial] (List.map Symbol.terminal w)

Tactic:
rfl
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
w : List (Symbol T g.NT)
⊢ g.Derives w w

Tactic:
Relation.ReflTransGen.refl

Premises used: Relation.ReflTransGen.refl
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
v w : List (Symbol T g.NT)
hvw : g.Produces v w
⊢ g.Derives v w

Tactic:
Relation.ReflTransGen.single hvw

Premises used: Relation.ReflTransGen.single
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v w : List (Symbol T g.NT)
huv : g.Derives u v
hvw : g.Derives v w
⊢ g.Derives u w

Tactic:
Relation.ReflTransGen.trans huv hvw

Premises used: Relation.ReflTransGen.trans
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v w : List (Symbol T g.NT)
huv : g.Derives u v
hvw : g.Produces v w
⊢ g.Derives u w

Tactic:
huv.trans hvw.single

Premises used: ContextFreeGrammar.Produces.single, ContextFreeGrammar.Derives.trans
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v w : List (Symbol T g.NT)
huv : g.Produces u v
hvw : g.Derives v w
⊢ g.Derives u w

Tactic:
huv.single.trans hvw

Premises used: ContextFreeGrammar.Produces.single, ContextFreeGrammar.Derives.trans
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u w : List (Symbol T g.NT)
huw : g.Derives u w
⊢ u = w ∨ ∃ (v : List (Symbol T g.NT)), g.Produces u v ∧ g.Derives v w

Tactic:
Relation.ReflTransGen.cases_head huw

Premises used: Relation.ReflTransGen.cases_head
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u w : List (Symbol T g.NT)
⊢ g.Derives u w ↔ u = w ∨ ∃ (v : List (Symbol T g.NT)), g.Produces u v ∧ g.Derives v w

Tactic:
Relation.ReflTransGen.cases_head_iff

Premises used: Relation.ReflTransGen.cases_head_iff
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u w : List (Symbol T g.NT)
huw : g.Derives u w
⊢ w = u ∨ ∃ (v : List (Symbol T g.NT)), g.Derives u v ∧ g.Produces v w

Tactic:
Relation.ReflTransGen.cases_tail huw

Premises used: Relation.ReflTransGen.cases_tail
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
u w : List (Symbol T g.NT)
⊢ g.Derives u w ↔ w = u ∨ ∃ (v : List (Symbol T g.NT)), g.Derives u v ∧ g.Produces v w

Tactic:
Relation.ReflTransGen.cases_tail_iff g.Produces u w

Premises used: Relation.ReflTransGen.cases_tail_iff, ContextFreeGrammar.Produces
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
v w : List (Symbol T g.NT)
hvw : g.Produces v w
p : List (Symbol T g.NT)
⊢ g.Produces (p ++ v) (p ++ w)

Tactic:
match hvw with | ⟨r, hrmem, hrvw⟩ => ⟨r, hrmem, hrvw.append_left p⟩

Premises used: ContextFreeGrammar.Produces, _private.0.ContextFreeGrammar.Produces.append_left.match_1, And.intro, Exists.intro, ContextFreeRule.Rewrites.append_left, HAppend.hAppend
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
v w : List (Symbol T g.NT)
hvw : g.Produces v w
p : List (Symbol T g.NT)
⊢ g.Produces (v ++ p) (w ++ p)

Tactic:
match hvw with | ⟨r, hrmem, hrvw⟩ => ⟨r, hrmem, hrvw.append_right p⟩

Premises used: ContextFreeGrammar.Produces, _private.0.ContextFreeGrammar.Produces.append_left.match_1, And.intro, Exists.intro, ContextFreeRule.Rewrites.append_right, HAppend.hAppend
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
v w p : List (Symbol T g.NT)
⊢ Relation.ReflTransGen g.Produces (p ++ v) (p ++ v)

Tactic:
rfl
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
v w p b c : List (Symbol T g.NT)
h : Relation.ReflTransGen g.Produces v b
last : g.Produces b c
ih : g.Derives (p ++ v) (p ++ b)
⊢ g.Derives (p ++ v) (p ++ c)

Tactic:
ih.trans_produces <| last.append_left p

Premises used: ContextFreeGrammar.Produces.append_left, ContextFreeGrammar.Derives.trans_produces
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
v w p b c : List (Symbol T g.NT)
h : Relation.ReflTransGen g.Produces v b
last : g.Produces b c
ih : g.Derives (p ++ v) (p ++ b)
⊢ g.Derives (p ++ v) (p ++ c)

Tactic:
exact ih.trans_produces <| last.append_left p

Premises used: ContextFreeGrammar.Produces.append_left, ContextFreeGrammar.Derives.trans_produces
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
v w : List (Symbol T g.NT)
hvw : g.Derives v w
p : List (Symbol T g.NT)
refl : Relation.ReflTransGen g.Produces (p ++ v) (p ++ v)
tail :
  ∀ {b c : List (Symbol T g.NT)},
    Relation.ReflTransGen g.Produces v b →
      ∀ (last : g.Produces b c) (ih : g.Derives (p ++ v) (p ++ b)), g.Derives (p ++ v) (p ++ c)
⊢ g.Derives (p ++ v) (p ++ w)

Tactic:
induction hvw with
  | refl => rfl
  | tail _ last ih => exact ih.trans_produces <| last.append_left p

Premises used: ContextFreeGrammar.Derives.refl
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
v w p : List (Symbol T g.NT)
⊢ Relation.ReflTransGen g.Produces (v ++ p) (v ++ p)

Tactic:
rfl
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
v w p b c : List (Symbol T g.NT)
h : Relation.ReflTransGen g.Produces v b
last : g.Produces b c
ih : g.Derives (v ++ p) (b ++ p)
⊢ g.Derives (v ++ p) (c ++ p)

Tactic:
ih.trans_produces <| last.append_right p

Premises used: ContextFreeGrammar.Derives.trans_produces, ContextFreeGrammar.Produces.append_right
-- Module: Mathlib.Computability.ContextFreeGrammar
Goal:
T : Type u_1
g : ContextFreeGrammar T
v w p b c : List (Symbol T g.NT)
h : Relation.ReflTransGen g.Produces v b
last : g.Produces b c
ih : g.Derives (v ++ p) (b ++ p)
⊢ g.Derives (v ++ p) (c ++ p)

Tactic:
exact ih.trans_produces <| last.append_right p

Premises used: ContextFreeGrammar.Derives.trans_produces, ContextFreeGrammar.Produces.append_right