awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
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_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
have h : p ++ u = p ++ x ++ [Symbol.nonterminal r.input] ++ y ∧ p ++ v = p ++ x ++ r.output ++ y
Tactic: use p ++ x, y
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
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)
⊢ r.Rewrites (u ++ p) (v ++ p)
have 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
Tactic: rw [rewrites_iff] at *
Cleared hypotheses: hvw, p
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
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)
⊢ ∃ (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
have 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
Tactic: rcases hvw with ⟨x, y, hxy⟩
Cleared hypotheses: hvw
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
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_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
have h : u ++ p = x ++ [Symbol.nonterminal r.input] ++ (y ++ p) ∧ v ++ p = x ++ r.output ++ (y ++ p)
Tactic: use x, y ++ p
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
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)
⊢ g.Derives (p ++ v) (p ++ w)
have refl : Relation.ReflTransGen g.Produces (p ++ v) (p ++ v)
Tactic: induction hvw with
  | refl => rfl
  | tail _ last ih => exact ih.trans_produces <| last.append_left p
Cleared hypotheses: hvw
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
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)
⊢ g.Derives (p ++ v) (p ++ w)
have 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)
Tactic: induction hvw with
  | refl => rfl
  | tail _ last ih => exact ih.trans_produces <| last.append_left p
Cleared hypotheses: hvw
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
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)
⊢ g.Derives (v ++ p) (w ++ p)
have refl : Relation.ReflTransGen g.Produces (v ++ p) (v ++ p)
Tactic: induction hvw with
  | refl => rfl
  | tail _ last ih => exact ih.trans_produces <| last.append_right p
Cleared hypotheses: hvw
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
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 (v ++ p) (v ++ p)
⊢ g.Derives (v ++ p) (w ++ p)
have tail : ∀ {b c : List (Symbol T g.NT)},
  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: induction hvw with
  | refl => rfl
  | tail _ last ih => exact ih.trans_produces <| last.append_right p
Cleared hypotheses: hvw
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
hguv : g.Produces u v
⊢ ∃ r ∈ g.rules, Symbol.nonterminal r.input ∈ u
have obtain : ∀ (w : ContextFreeRule T g.NT) (l : w ∈ g.rules) (r : w.Rewrites u v), ∃ r ∈ g.rules, Symbol.nonterminal r.input ∈ u
Tactic: obtain ⟨w, l, r⟩ := hguv
Cleared hypotheses: hguv
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
⊢ ¬g.Derives [Symbol.nonterminal t] s
have rw : ¬([Symbol.nonterminal t] = s ∨ ∃ (v : List (Symbol T g.NT)), g.Produces [Symbol.nonterminal t] v ∧ g.Derives v s)
Tactic: rw [derives_iff_eq_or_head]
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
⊢ ¬([Symbol.nonterminal t] = s ∨ ∃ (v : List (Symbol T g.NT)), g.Produces [Symbol.nonterminal t] v ∧ g.Derives v s)
have push : [Symbol.nonterminal t] ≠ s ∧ ∀ (v : List (Symbol T g.NT)) (_ : g.Produces [Symbol.nonterminal t] v), ¬g.Derives v s
Tactic: push Not
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
⊢ [Symbol.nonterminal t] ≠ s ∧ ∀ (v : List (Symbol T g.NT)) (_ : g.Produces [Symbol.nonterminal t] v), ¬g.Derives v s
have refine : ∀ (x : List (Symbol T g.NT)) (hx : g.Produces [Symbol.nonterminal t] x), ¬g.Derives x s
Tactic: refine ⟨hs.symm, fun _ hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (hypothesis)
Goal:
T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
x : List (Symbol T g.NT)
hx : g.Produces [Symbol.nonterminal t] x
⊢ ¬g.Derives x s
have hxr : ∃ r ∈ g.rules, Membership.mem (γ := List (Symbol T g.NT)) [Symbol.nonterminal t] (Symbol.nonterminal r.input)
Tactic: have hxr := hx.exists_nonterminal_input_mem
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (hypothesis)
Goal:
T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
x : List (Symbol T g.NT)
hx : g.Produces [Symbol.nonterminal t] x
hxr : ∃ r ∈ g.rules, Membership.mem (γ := List (Symbol T g.NT)) [Symbol.nonterminal t] (Symbol.nonterminal r.input)
⊢ ¬g.Derives x s
have hxr₁ : ∃ r ∈ g.rules, r.input = t
Tactic: simp_rw [List.mem_singleton, Symbol.nonterminal.injEq] at hxr
Cleared hypotheses: hxr
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
x : List (Symbol T g.NT)
hx : g.Produces [Symbol.nonterminal t] x
hxr : ∃ r ∈ g.rules, r.input = t
⊢ ¬g.Derives x s
have tauto : g.Derives x s → ∀ w ∈ g.rules, w.input = t → False
Tactic: tauto
Cleared hypotheses: hxr
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
g : ContextFreeGrammar T
hg : ∀ r ∈ g.rules, r.input ≠ g.initial
⊢ g.language = 0
have h : ∀ (x : List T), x ∈ g.language ↔ Membership.mem (γ := Language T) 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
N : Type u_2
⊢ Eq (α := ContextFreeRule T N → ContextFreeRule T N) (reverse ∘ reverse) id
have h : ∀ (x : ContextFreeRule T N), (reverse ∘ reverse) x = id x
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
⊢ r.reverse.Rewrites u v ↔ r.Rewrites u.reverse v.reverse
have rw : r.reverse.reverse.Rewrites u.reverse v.reverse ↔ r.Rewrites u.reverse v.reverse
Tactic: rw [← rewrites_reverse, reverse_reverse]
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
rw : r.reverse.reverse.Rewrites u.reverse v.reverse ↔ r.Rewrites u.reverse v.reverse
⊢ r.reverse.Rewrites u v ↔ r.Rewrites u.reverse v.reverse
have rw₁ : r.Rewrites u.reverse v.reverse ↔ r.Rewrites u.reverse v.reverse
Tactic: rw [← rewrites_reverse, reverse_reverse]
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
hg : g.Derives u v
⊢ g.reverse.Derives u.reverse v.reverse
have refl : Relation.ReflTransGen g.reverse.Produces u.reverse u.reverse
Tactic: induction hg with
  | refl => rfl
  | tail _ orig ih => exact ih.trans_produces orig.reverse
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
hg : g.Derives u v
refl : Relation.ReflTransGen g.reverse.Produces u.reverse u.reverse
⊢ g.reverse.Derives u.reverse v.reverse
have tail : ∀ {b c : List (Symbol T g.NT)},
  Relation.ReflTransGen g.Produces u b →
    ∀ (orig : g.Produces b c) (ih : g.reverse.Derives u.reverse b.reverse), g.reverse.Derives u.reverse c.reverse
Tactic: induction hg with
  | refl => rfl
  | tail _ orig ih => exact ih.trans_produces orig.reverse
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
h : g.reverse.Derives u.reverse v.reverse
⊢ g.Derives u v
have h₁ : Eq.{max 2 (u_1 + 1)} g g.reverse.reverse
Tactic: convert! h.reverse
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
h : g.reverse.Derives u.reverse v.reverse
h₁ : Eq.{max 2 (u_1 + 1)} g g.reverse.reverse
⊢ g.Derives u v
have h₂ : Eq.{max 2 (u_1 + 1)} g g.reverse.reverse → u = u.reverse.reverse
Tactic: convert! h.reverse
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
h : g.reverse.Derives u.reverse v.reverse
h₁ : Eq.{max 2 (u_1 + 1)} g g.reverse.reverse
h₂ : Eq.{max 2 (u_1 + 1)} g g.reverse.reverse → u = u.reverse.reverse
⊢ g.Derives u v
have h₃ : Eq.{max 2 (u_1 + 1)} g g.reverse.reverse → v = v.reverse.reverse
Tactic: convert! h.reverse
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
⊢ g.reverse.Derives u v ↔ g.Derives u.reverse v.reverse
have rw : g.Derives u.reverse v.reverse ↔ g.reverse.Derives u v
Tactic: rw [iff_comm, ← derives_reverse, List.reverse_reverse, List.reverse_reverse]
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
rw : g.Derives u.reverse v.reverse ↔ g.reverse.Derives u v
⊢ g.reverse.Derives u v ↔ g.Derives u.reverse v.reverse
have rw₁ : g.reverse.Derives u.reverse.reverse v.reverse.reverse ↔ g.reverse.Derives u v
Tactic: rw [iff_comm, ← derives_reverse, List.reverse_reverse, List.reverse_reverse]
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
rw : g.Derives u.reverse v.reverse ↔ g.reverse.Derives u v
rw₁ : g.reverse.Derives u.reverse.reverse v.reverse.reverse ↔ g.reverse.Derives u v
⊢ g.reverse.Derives u v ↔ g.Derives u.reverse v.reverse
have rw₂ : g.reverse.Derives u v.reverse.reverse ↔ g.reverse.Derives u v
Tactic: rw [iff_comm, ← derives_reverse, List.reverse_reverse, List.reverse_reverse]
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
rw : g.Derives u.reverse v.reverse ↔ g.reverse.Derives u v
rw₁ : g.reverse.Derives u.reverse.reverse v.reverse.reverse ↔ g.reverse.Derives u v
rw₂ : g.reverse.Derives u v.reverse.reverse ↔ g.reverse.Derives u v
⊢ g.reverse.Derives u v ↔ g.Derives u.reverse v.reverse
have rw₃ : g.reverse.Derives u v ↔ g.reverse.Derives u v
Tactic: rw [iff_comm, ← derives_reverse, List.reverse_reverse, List.reverse_reverse]
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
g : ContextFreeGrammar T
⊢ g.reverse.language = g.language.reverse
have h : ∀ (x : List T), x ∈ g.reverse.language ↔ x ∈ g.language.reverse
Tactic: ext
-- Lean 4 proof step from Mathlib.Computability.ContextFreeGrammar (goal)
Goal:
T : Type u_1
L : Language T
h : L.IsContextFree
⊢ L.reverse.IsContextFree
have rcases : ∀ (g : ContextFreeGrammar T), g.language.reverse.IsContextFree
Tactic: rcases h with ⟨g, rfl⟩
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
⊢ ∃ (q : σ) (a : List α) (b : List α) (c : List α),
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
have obtain : ∀ (n m : Fin (Fintype.card σ + 1)) (hneq : n ≠ m)
  (heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)),
  ∃ (q : σ) (a : List α) (b : List α) (c : List α),
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
Tactic: obtain ⟨n, m, hneq, heq⟩ :=
    Fintype.exists_ne_map_eq_of_card_lt
      (fun n : Fin (Fintype.card σ + 1) => M.evalFrom s (x.take n)) (by simp)
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
⊢ ∃ (q : σ) (a : List α) (b : List α) (c : List α),
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
have inr : ∀
  (this :
    ∀ (n m : Fin (Fintype.card σ + 1)) (hneq : n ≠ m)
      (heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)) (hle : (↑n : ℕ) ≤ (↑m : ℕ)),
      ∃ (q : σ) (a : List α) (b : List α) (c : List α),
        x = a ++ b ++ c ∧
          a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t)
  (hle : ¬(↑n : ℕ) ≤ (↑m : ℕ)),
  ∃ (q : σ) (a : List α) (b : List α) (c : List α),
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
Tactic: wlog hle : (n : ℕ) ≤ m generalizing n m
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
inr :
  ∀
    (this :
      ∀ (n m : Fin (Fintype.card σ + 1)) (hneq : n ≠ m)
        (heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)) (hle : (↑n : ℕ) ≤ (↑m : ℕ)),
        ∃ (q : σ) (a : List α) (b : List α) (c : List α),
          x = a ++ b ++ c ∧
            a.length + b.length ≤ Fintype.card σ ∧
              b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t)
    (hle : ¬(↑n : ℕ) ≤ (↑m : ℕ)),
    ∃ (q : σ) (a : List α) (b : List α) (c : List α),
      x = a ++ b ++ c ∧
        a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
⊢ ∃ (q : σ) (a : List α) (b : List α) (c : List α),
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
have wlog : ∀ (n m : Fin (Fintype.card σ + 1)) (hneq : n ≠ m)
  (heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)) (hle : (↑n : ℕ) ≤ (↑m : ℕ)),
  ∃ (q : σ) (a : List α) (b : List α) (c : List α),
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
Tactic: wlog hle : (n : ℕ) ≤ m generalizing n m
Cleared hypotheses: n, m, hneq, heq
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
⊢ ∃ (q : σ) (a : List α) (b : List α) (c : List α),
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
have refine_1 : x = List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x
Tactic: refine
    ⟨M.evalFrom s ((x.take m).take n), (x.take m).take n, (x.take m).drop n,
                    x.drop m, ?_, ?_, ?_, by rfl, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
refine_1 :
  x = List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x
⊢ ∃ (q : σ) (a : List α) (b : List α) (c : List α),
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
have refine_2 : (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)).length + (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)).length ≤ Fintype.card σ
Tactic: refine
    ⟨M.evalFrom s ((x.take m).take n), (x.take m).take n, (x.take m).drop n,
                    x.drop m, ?_, ?_, ?_, by rfl, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
refine_1 :
  x = List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x
refine_2 :
  (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)).length + (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)).length ≤
    Fintype.card σ
⊢ ∃ (q : σ) (a : List α) (b : List α) (c : List α),
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
have refine_3 : List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ≠ []
Tactic: refine
    ⟨M.evalFrom s ((x.take m).take n), (x.take m).take n, (x.take m).drop n,
                    x.drop m, ?_, ?_, ?_, by rfl, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
refine_1 :
  x = List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x
refine_2 :
  (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)).length + (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)).length ≤
    Fintype.card σ
refine_3 : List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ≠ []
⊢ ∃ (q : σ) (a : List α) (b : List α) (c : List α),
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
have refine_4 : M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)) =
    M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)) ∧
  M.evalFrom (M.evalFrom s (List.take (↑n : ℕ) (List.take (↑m : ℕ) x))) (List.drop (↑m : ℕ) x) = t
Tactic: refine
    ⟨M.evalFrom s ((x.take m).take n), (x.take m).take n, (x.take m).drop n,
                    x.drop m, ?_, ?_, ?_, by rfl, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
⊢ x = List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x
have refine_1 : x = List.take (↑m : ℕ) x ++ List.drop (↑m : ℕ) x
Tactic: rw [List.take_append_drop, List.take_append_drop]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
refine_1 : x = List.take (↑m : ℕ) x ++ List.drop (↑m : ℕ) x
⊢ x = List.take (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) ++ List.drop (↑m : ℕ) x
have refine_1₁ : x = x
Tactic: rw [List.take_append_drop, List.take_append_drop]
-- Lean 4 proof step from Mathlib.Computability.DFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
⊢ (List.take (↑n : ℕ) (List.take (↑m : ℕ) x)).length + (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)).length ≤
    Fintype.card σ
have refine_2 : min (↑n : ℕ) (min (↑m : ℕ) x.length) + (min (↑m : ℕ) x.length - (↑n : ℕ)) ≤ Fintype.card σ
Tactic: simp only [List.length_drop, List.length_take]
-- Lean 4 proof step from Mathlib.Computability.DFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
h : List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) = []
⊢ False
have hlen' : (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)).length = List.length.{u} (α := α) []
Tactic: have hlen' := congr_arg List.length h
-- Lean 4 proof step from Mathlib.Computability.DFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : DFA α σ
inst : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n : ℕ) x) = M.evalFrom s (List.take (↑m : ℕ) x)
hle : (↑n : ℕ) ≤ (↑m : ℕ)
h : List.drop (↑n : ℕ) (List.take (↑m : ℕ) x) = []
hlen' : (List.drop (↑n : ℕ) (List.take (↑m : ℕ) x)).length = List.length.{u} (α := α) []
⊢ False
have hlen'₁ : min (↑m : ℕ) x.length - (↑n : ℕ) = 0
Tactic: simp only [List.length_drop, List.length, List.length_take] at hlen'
Cleared hypotheses: hlen'