internlm/Lean-Github huggingface dataset:
Theorem: sq2_pow_twice
Proof state before:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
⊢ Real.sqrt 2 ^ 2 = 2
Tactic:
have lm := Real.rpow_add sq2_pos 1 1
Proof state after:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
lm : Real.sqrt 2 ^ (1 + 1) = Real.sqrt 2 ^ 1 * Real.sqrt 2 ^ 1
⊢ Real.sqrt 2 ^ 2 = 2
Theorem: sq2_pow_twice
Proof state before:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
lm : Real.sqrt 2 ^ (1 + 1) = Real.sqrt 2 ^ 1 * Real.sqrt 2 ^ 1
⊢ Real.sqrt 2 ^ 2 = 2
Tactic:
have one_plus_one : (1: ℝ) + (1: ℝ) = 2 := by norm_num
Proof state after:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
lm : Real.sqrt 2 ^ (1 + 1) = Real.sqrt 2 ^ 1 * Real.sqrt 2 ^ 1
one_plus_one : 1 + 1 = 2
⊢ Real.sqrt 2 ^ 2 = 2
Theorem: sq2_pow_twice
Proof state before:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
lm : Real.sqrt 2 ^ (1 + 1) = Real.sqrt 2 ^ 1 * Real.sqrt 2 ^ 1
one_plus_one : 1 + 1 = 2
⊢ Real.sqrt 2 ^ 2 = 2
Tactic:
rw [one_plus_one] at lm
Proof state after:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
lm : Real.sqrt 2 ^ 2 = Real.sqrt 2 ^ 1 * Real.sqrt 2 ^ 1
one_plus_one : 1 + 1 = 2
⊢ Real.sqrt 2 ^ 2 = 2
Theorem: sq2_pow_twice
Proof state before:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
lm : Real.sqrt 2 ^ 2 = Real.sqrt 2 ^ 1 * Real.sqrt 2 ^ 1
one_plus_one : 1 + 1 = 2
⊢ Real.sqrt 2 ^ 2 = 2
Tactic:
rw [lm]
Proof state after:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
lm : Real.sqrt 2 ^ 2 = Real.sqrt 2 ^ 1 * Real.sqrt 2 ^ 1
one_plus_one : 1 + 1 = 2
⊢ Real.sqrt 2 ^ 1 * Real.sqrt 2 ^ 1 = 2
Theorem: sq2_pow_twice
Proof state before:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
lm : Real.sqrt 2 ^ 2 = Real.sqrt 2 ^ 1 * Real.sqrt 2 ^ 1
one_plus_one : 1 + 1 = 2
⊢ Real.sqrt 2 ^ 1 * Real.sqrt 2 ^ 1 = 2
Tactic:
simp [Real.rpow_one]
Proof state after:
no goals
Theorem: sq2_pow_twice
Proof state before:
⊢ 2 ≥ 0
Tactic:
norm_cast
Proof state after:
no goals
Theorem: sq2_pow_twice
Proof state before:
two_nonneg : 2 ≥ 0
⊢ Real.sqrt 2 > 0
Tactic:
simp [Real.sqrt_pos]
Proof state after:
no goals
Theorem: sq2_pow_twice
Proof state before:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
⊢ Real.sqrt 2 ≥ 0
Tactic:
apply Real.sqrt_nonneg
Proof state after:
no goals
Theorem: sq2_pow_twice
Proof state before:
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
lm : Real.sqrt 2 ^ (1 + 1) = Real.sqrt 2 ^ 1 * Real.sqrt 2 ^ 1
⊢ 1 + 1 = 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: exists_irrationals_pow_rational
Proof state before:
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)
Tactic:
let b := Real.sqrt 2
Proof state after:
b : ℝ := Real.sqrt 2
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)
Theorem: exists_irrationals_pow_rational
Proof state before:
b : ℝ := Real.sqrt 2
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)
Tactic:
by_cases c:Irrational (b ^ b)
Proof state after:
case pos
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)

case neg
b : ℝ := Real.sqrt 2
c : ¬Irrational (b ^ b)
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)
Theorem: exists_irrationals_pow_rational
Proof state before:
case pos
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)
Tactic:
let a := b ^ b
Proof state after:
case pos
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)
Theorem: exists_irrationals_pow_rational
Proof state before:
case pos
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)
Tactic:
use a, b
Proof state after:
case h
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)
Theorem: exists_irrationals_pow_rational
Proof state before:
case h
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)
Tactic:
simp [irrational_sqrt_two, c, sq2_pow_twice]
Proof state after:
case h
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ ¬Irrational 2
Theorem: exists_irrationals_pow_rational
Proof state before:
case h
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ ¬Irrational 2
Tactic:
simp [irrational_iff_ne_rational]
Proof state after:
case h
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ ∃ x x_1, 2 = ↑x / ↑x_1
Theorem: exists_irrationals_pow_rational
Proof state before:
case h
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ ∃ x x_1, 2 = ↑x / ↑x_1
Tactic:
use 2, 1
Proof state after:
case h
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ 2 = ↑2 / ↑1
Theorem: exists_irrationals_pow_rational
Proof state before:
case h
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ 2 = ↑2 / ↑1
Tactic:
simp
Proof state after:
no goals
Theorem: exists_irrationals_pow_rational
Proof state before:
case neg
b : ℝ := Real.sqrt 2
c : ¬Irrational (b ^ b)
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)
Tactic:
use b, b
Proof state after:
case h
b : ℝ := Real.sqrt 2
c : ¬Irrational (b ^ b)
⊢ Irrational b ∧ Irrational b ∧ ¬Irrational (b ^ b)
Theorem: exists_irrationals_pow_rational
Proof state before:
case h
b : ℝ := Real.sqrt 2
c : ¬Irrational (b ^ b)
⊢ Irrational b ∧ Irrational b ∧ ¬Irrational (b ^ b)
Tactic:
simp [irrational_sqrt_two, c]
Proof state after:
no goals
Theorem: FreeGroup.reduced_nil
Proof state before:
α : Type
inst✝ : DecidableEq α
⊢ Reduced []
Tactic:
apply not_step_nil
Proof state after:
no goals
Theorem: FreeGroup.reduced_singleton
Proof state before:
α : Type
inst✝ : DecidableEq α
p : α × Bool
⊢ Reduced [p]
Tactic:
intro L' step
Proof state after:
α : Type
inst✝ : DecidableEq α
p : α × Bool
L' : List (α × Bool)
step : Step [p] L'
⊢ False
Theorem: FreeGroup.reduced_singleton
Proof state before:
α : Type
inst✝ : DecidableEq α
p : α × Bool
L' : List (α × Bool)
step : Step [p] L'
⊢ False
Tactic:
apply not_step_singleton step
Proof state after:
no goals
Theorem: split_drop
Proof state before:
α : Type
inst✝ : DecidableEq α
β : Type u_1
l : List β
p : l ≠ []
⊢ List.dropLast l ++ [List.getLast l p] = l
Tactic:
match l with
| cancP :: t =>
match t with 
| [] =>  simp [p] at *
| h' :: t' =>
  simp [List.dropLast, List.getLast, split_drop]
Proof state after:
no goals
Theorem: split_drop
Proof state before:
α : Type
inst✝ : DecidableEq α
β : Type u_1
l : List β
cancP : β
t : List β
p : cancP :: t ≠ []
⊢ List.dropLast (cancP :: t) ++ [List.getLast (cancP :: t) p] = cancP :: t
Tactic:
match t with 
| [] =>  simp [p] at *
| h' :: t' =>
  simp [List.dropLast, List.getLast, split_drop]
Proof state after:
no goals
Theorem: split_drop
Proof state before:
α : Type
inst✝ : DecidableEq α
β : Type u_1
l : List β
cancP : β
t : List β
p : [cancP] ≠ []
⊢ List.dropLast [cancP] ++ [List.getLast [cancP] p] = [cancP]
Tactic:
simp [p] at *
Proof state after:
no goals
Theorem: split_drop
Proof state before:
α : Type
inst✝ : DecidableEq α
β : Type u_1
l : List β
cancP : β
t : List β
h' : β
t' : List β
p : cancP :: h' :: t' ≠ []
⊢ List.dropLast (cancP :: h' :: t') ++ [List.getLast (cancP :: h' :: t') p] = cancP :: h' :: t'
Tactic:
simp [List.dropLast, List.getLast, split_drop]
Proof state after:
no goals
Theorem: FreeGroup.nil_nextVertex
Proof state before:
α : Type
inst✝ : DecidableEq α
letter : α × Bool
⊢ [] :+ letter = [letter]
Tactic:
rfl
Proof state after:
no goals
Theorem: FreeGroup.nonnil_nextVertex_extend
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
nonnil : start ≠ []
letter : α × Bool
neq : List.getLast start nonnil ≠ letter⁻¹
⊢ start :+ letter = List.concat start letter
Tactic:
simp [nextVertex,  neq, if_neg, nonnil]
Proof state after:
no goals
Theorem: FreeGroup.nonnil_nextVertex_cancel
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
nonnil : start ≠ []
letter : α × Bool
eql : List.getLast start nonnil = letter⁻¹
⊢ start :+ letter = List.dropLast start
Tactic:
simp [nextVertex,  eql, if_pos, nonnil]
Proof state after:
no goals
Theorem: FreeGroup.exists_of_step
Proof state before:
α : Type
inst✝ : DecidableEq α
L L' : List (α × Bool)
⊢ Step L L' → ∃ x b L₁ L₂, L = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
Tactic:
intro step
Proof state after:
α : Type
inst✝ : DecidableEq α
L L' : List (α × Bool)
step : Step L L'
⊢ ∃ x b L₁ L₂, L = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
Theorem: FreeGroup.exists_of_step
Proof state before:
α : Type
inst✝ : DecidableEq α
L L' : List (α × Bool)
step : Step L L'
⊢ ∃ x b L₁ L₂, L = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
Tactic:
induction step with
| @not L₁ L₂ x b =>  use x, b, L₁, L₂
Proof state after:
no goals
Theorem: FreeGroup.exists_of_step
Proof state before:
case not
α : Type
inst✝ : DecidableEq α
L L' L₁ L₂ : List (α × Bool)
x : α
b : Bool
⊢ ∃ x_1 b_1 L₁_1 L₂_1,
    L₁ ++ (x, b) :: (x, !b) :: L₂ = L₁_1 ++ (x_1, b_1) :: (x_1, !b_1) :: L₂_1 ∧ L₁ ++ L₂ = L₁_1 ++ L₂_1
Tactic:
use x, b, L₁, L₂
Proof state after:
no goals
Theorem: FreeGroup.nextVertex_reduced
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
⊢ Reduced start → Reduced (start :+ letter)
Tactic:
intro reduced_start
Proof state after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
⊢ Reduced (start :+ letter)
Theorem: FreeGroup.nextVertex_reduced
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
⊢ Reduced (start :+ letter)
Tactic:
if nilP: start = [] 
then 
  simp [nil_nextVertex, nilP]
  apply reduced_singleton
else
  intro L' step
  let ⟨x, b, L₁, L₂, eqs⟩ := exists_of_step step
  let eq1 := eqs.1
  if cancP:start.getLast nilP = letter⁻¹ 
  then 
    simp [cancP, nilP, nonnil_nextVertex_cancel] at eq1
    have eq1' : start.dropLast.concat (start.getLast nilP) = 
        (L₁ ++ (x, b) :: (x, !b) :: L₂).concat (start.getLast nilP) :=
      by rw [eq1]
    simp [split_drop, nilP] at eq1'
    let L₂' := L₂ ++ [start.getLast nilP]
    apply reduced_start (L₁ ++ L₂')
    rw [eq1']
    apply Step.not
  else 
    simp [cancP, nilP, nonnil_nextVertex_extend] at eq1
    if endP : L₂ = [] 
    then
      simp [endP] at eq1
      rw [←List.concat_eq_append] at eq1
      have : L₁ ++ [(x, b), (x, !b)] = 
        (L₁ ++ [(x, b)]).concat (x, !b) := by simp
      rw [this] at eq1
      let eq1' := List.of_concat_eq_concat eq1
      let eq1'' := eq1'.1
      let sp := split_drop start nilP
      rw [← sp, ←List.concat_eq_append, ←List.concat_eq_append] at eq1''
      let eq1''' := eq1'.2
      let eq2' := List.of_concat_eq_concat eq1''
      let _eq2'' := eq2'.2
      rw [eq1''', _eq2''] at cancP
      simp [inv_def] at cancP
    else
      rw [← split_drop L₂ endP] at eq1
      rw [← List.cons_append, ← List.cons_append, 
        ← List.append_assoc, ← List.concat_eq_append,
        ← List.concat_eq_append] at eq1
      let eq1' := List.of_concat_eq_concat eq1
      let eq1'' := eq1'.1
      apply reduced_start (L₁ ++ L₂.dropLast)
      rw [eq1'']
      apply Step.not
Proof state after:
no goals
Theorem: FreeGroup.nextVertex_reduced
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : start = []
⊢ Reduced (start :+ letter)
Tactic:
simp [nil_nextVertex, nilP]
Proof state after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : start = []
⊢ Reduced [letter]
Theorem: FreeGroup.nextVertex_reduced
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : start = []
⊢ Reduced [letter]
Tactic:
apply reduced_singleton
Proof state after:
no goals
Theorem: FreeGroup.nextVertex_reduced
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
⊢ Reduced (start :+ letter)
Tactic:
intro L' step
Proof state after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
⊢ False
Theorem: FreeGroup.nextVertex_reduced
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
⊢ False
Tactic:
let ⟨x, b, L₁, L₂, eqs⟩ := exists_of_step step
Proof state after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
⊢ False
Theorem: FreeGroup.nextVertex_reduced
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
⊢ False
Tactic:
let eq1 := eqs.1
Proof state after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
eq1 : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ := eqs.left
⊢ False
Theorem: FreeGroup.nextVertex_reduced
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
eq1 : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ := eqs.left
⊢ False
Tactic:
if cancP:start.getLast nilP = letter⁻¹ 
then 
  simp [cancP, nilP, nonnil_nextVertex_cancel] at eq1
  have eq1' : start.dropLast.concat (start.getLast nilP) = 
      (L₁ ++ (x, b) :: (x, !b) :: L₂).concat (start.getLast nilP) :=
    by rw [eq1]
  simp [split_drop, nilP] at eq1'
  let L₂' := L₂ ++ [start.getLast nilP]
  apply reduced_start (L₁ ++ L₂')
  rw [eq1']
  apply Step.not
else 
  simp [cancP, nilP, nonnil_nextVertex_extend] at eq1
  if endP : L₂ = [] 
  then
    simp [endP] at eq1
    rw [←List.concat_eq_append] at eq1
    have : L₁ ++ [(x, b), (x, !b)] = 
      (L₁ ++ [(x, b)]).concat (x, !b) := by simp
    rw [this] at eq1
    let eq1' := List.of_concat_eq_concat eq1
    let eq1'' := eq1'.1
    let sp := split_drop start nilP
    rw [← sp, ←List.concat_eq_append, ←List.concat_eq_append] at eq1''
    let eq1''' := eq1'.2
    let eq2' := List.of_concat_eq_concat eq1''
    let _eq2'' := eq2'.2
    rw [eq1''', _eq2''] at cancP
    simp [inv_def] at cancP
  else
    rw [← split_drop L₂ endP] at eq1
    rw [← List.cons_append, ← List.cons_append, 
      ← List.append_assoc, ← List.concat_eq_append,
      ← List.concat_eq_append] at eq1
    let eq1' := List.of_concat_eq_concat eq1
    let eq1'' := eq1'.1
    apply reduced_start (L₁ ++ L₂.dropLast)
    rw [eq1'']
    apply Step.not
Proof state after:
no goals
Theorem: FreeGroup.nextVertex_reduced
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
eq1 : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ := eqs.left
cancP : List.getLast start nilP = letter⁻¹
⊢ False
Tactic:
simp [cancP, nilP, nonnil_nextVertex_cancel] at eq1
Proof state after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
⊢ False
Theorem: FreeGroup.nextVertex_reduced
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
⊢ False
Tactic:
have eq1' : start.dropLast.concat (start.getLast nilP) = 
    (L₁ ++ (x, b) :: (x, !b) :: L₂).concat (start.getLast nilP) :=
  by rw [eq1]
Proof state after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' :
  List.concat (List.dropLast start) (List.getLast start nilP) =
    List.concat (L₁ ++ (x, b) :: (x, !b) :: L₂) (List.getLast start nilP)
⊢ False
Theorem: FreeGroup.nextVertex_reduced
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' :
  List.concat (List.dropLast start) (List.getLast start nilP) =
    List.concat (L₁ ++ (x, b) :: (x, !b) :: L₂) (List.getLast start nilP)
⊢ False
Tactic:
simp [split_drop, nilP] at eq1'
Proof state after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])
⊢ False
Theorem: FreeGroup.nextVertex_reduced
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])
⊢ False
Tactic:
let L₂' := L₂ ++ [start.getLast nilP]
Proof state after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])
L₂' : List (α × Bool) := L₂ ++ [List.getLast start nilP]
⊢ False
Theorem: FreeGroup.nextVertex_reduced
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])
L₂' : List (α × Bool) := L₂ ++ [List.getLast start nilP]
⊢ False
Tactic:
apply reduced_start (L₁ ++ L₂')
Proof state after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])
L₂' : List (α × Bool) := L₂ ++ [List.getLast start nilP]
⊢ Step start (L₁ ++ L₂')
Theorem: FreeGroup.nextVertex_reduced
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])
L₂' : List (α × Bool) := L₂ ++ [List.getLast start nilP]
⊢ Step start (L₁ ++ L₂')
Tactic:
rw [eq1']
Proof state after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])
L₂' : List (α × Bool) := L₂ ++ [List.getLast start nilP]
⊢ Step (L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])) (L₁ ++ L₂')
Theorem: FreeGroup.nextVertex_reduced
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])
L₂' : List (α × Bool) := L₂ ++ [List.getLast start nilP]
⊢ Step (L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])) (L₁ ++ L₂')
Tactic:
apply Step.not
Proof state after:
no goals
Theorem: FreeGroup.nextVertex_reduced
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
⊢ List.concat (List.dropLast start) (List.getLast start nilP) =
    List.concat (L₁ ++ (x, b) :: (x, !b) :: L₂) (List.getLast start nilP)
Tactic:
rw [eq1]
Proof state after:
no goals