awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
x : α × Bool
zero : reduce (List.replicate 0 x) = List.replicate 0 x
succ :
  ∀ (n : ℕ) (ih : reduce (List.replicate n x) = List.replicate n x),
    reduce (List.replicate (n + 1) x) = List.replicate (n + 1) x
⊢ reduce (List.replicate n x) = List.replicate n x

Tactic:
induction n with
  | zero => simp [reduce]
  | succ n ih =>
    rw [List.replicate_succ, reduce.cons, ih]
    cases n with
    | zero => simp
    | succ n => simp [List.replicate_succ]

Premises used: FreeGroup.reduce.cons, List.replicate_succ, FreeGroup.reduce
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
⊢ Red.{u_1} (α := α) [] (reduce [])

Tactic:
constructor
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
ih : Red tl1 (reduce tl1)
cons :
  Red (hd1 :: tl1)
    (List.rec (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) [hd1]
      (fun (head : α × Bool) (tail tail_ih : List (α × Bool)) ↦
        if hd1.1 = head.1 ∧ hd1.2 = !head.2 then tail else hd1 :: head :: tail)
      (reduce tl1))
⊢ Red (hd1 :: tl1) (reduce (hd1 :: tl1))

Tactic:
dsimp
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
ih : Red tl1 (reduce tl1)
cons :
  ∀ (ih : Red tl1 (reduce tl1)),
    Red (hd1 :: tl1)
      (List.rec (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) [hd1]
        (fun (head : α × Bool) (tail tail_ih : List (α × Bool)) ↦
          if hd1.1 = head.1 ∧ hd1.2 = !head.2 then tail else hd1 :: head :: tail)
        (reduce tl1))
⊢ Red (hd1 :: tl1)
    (List.rec (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) [hd1]
      (fun (head : α × Bool) (tail tail_ih : List (α × Bool)) ↦
        if hd1.1 = head.1 ∧ hd1.2 = !head.2 then tail else hd1 :: head :: tail)
      (reduce tl1))

Tactic:
revert ih
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
cons :
  ∀ (TL : List (α × Bool)) (htl : reduce tl1 = TL) (ih : Red tl1 TL),
    Red (hd1 :: tl1)
      (List.rec (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) [hd1]
        (fun (head : α × Bool) (tail tail_ih : List (α × Bool)) ↦
          if hd1.1 = head.1 ∧ hd1.2 = !head.2 then tail else hd1 :: head :: tail)
        TL)
⊢ ∀ (ih : Red tl1 (reduce tl1)),
    Red (hd1 :: tl1)
      (List.rec (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) [hd1]
        (fun (head : α × Bool) (tail tail_ih : List (α × Bool)) ↦
          if hd1.1 = head.1 ∧ hd1.2 = !head.2 then tail else hd1 :: head :: tail)
        (reduce tl1))

Tactic:
generalize htl : reduce tl1 = TL

Premises used: FreeGroup.reduce
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
htl : reduce tl1 = []
ih : Red tl1 []
⊢ Red (hd1 :: tl1)
    (List.rec (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) [hd1]
      (fun (head : α × Bool) (tail tail_ih : List (α × Bool)) ↦
        if hd1.1 = head.1 ∧ hd1.2 = !head.2 then tail else hd1 :: head :: tail)
      [])

Tactic:
Red.cons_cons ih

Premises used: FreeGroup.Red.cons_cons
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
htl : reduce tl1 = []
ih : Red tl1 []
⊢ Red (hd1 :: tl1)
    (List.rec (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) [hd1]
      (fun (head : α × Bool) (tail tail_ih : List (α × Bool)) ↦
        if hd1.1 = head.1 ∧ hd1.2 = !head.2 then tail else hd1 :: head :: tail)
      [])

Tactic:
exact Red.cons_cons ih

Premises used: FreeGroup.Red.cons_cons
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
pos : ∀ (h : hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2), Red (hd1 :: tl1) tl2
neg : ∀ (h : ¬(hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2)), Red (hd1 :: tl1) (hd1 :: hd2 :: tl2)
⊢ Red (hd1 :: tl1) (if hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2 then tl2 else hd1 :: hd2 :: tl2)

Tactic:
split_ifs with h
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2
pos : ∀ (fst : α) (snd : Bool) (h : (fst, snd).1 = hd2.1 ∧ (fst, snd).2 = !hd2.2), Red ((fst, snd) :: tl1) tl2
⊢ Red (hd1 :: tl1) tl2

Tactic:
cases hd1
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
fst : α
snd : Bool
h : (fst, snd).1 = hd2.1 ∧ (fst, snd).2 = !hd2.2
pos :
  ∀ (fst_1 : α) (snd_1 : Bool) (htl : reduce tl1 = (fst_1, snd_1) :: tl2) (ih : Red tl1 ((fst_1, snd_1) :: tl2))
    (h : (fst, snd).1 = (fst_1, snd_1).1 ∧ (fst, snd).2 = !(fst_1, snd_1).2), Red ((fst, snd) :: tl1) tl2
⊢ Red ((fst, snd) :: tl1) tl2

Tactic:
cases hd2
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
tl1 tl2 : List (α × Bool)
fst : α
snd : Bool
fst_1 : α
snd_1 : Bool
htl : reduce tl1 = (fst_1, snd_1) :: tl2
ih : Red tl1 ((fst_1, snd_1) :: tl2)
h : (fst, snd).1 = (fst_1, snd_1).1 ∧ (fst, snd).2 = !(fst_1, snd_1).2
⊢ (fst, snd).1 = (fst_1, snd_1).1

Tactic:
cases h
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
tl1 tl2 : List (α × Bool)
fst : α
snd : Bool
fst_1 : α
snd_1 : Bool
htl : reduce tl1 = (fst_1, snd_1) :: tl2
ih : Red tl1 ((fst_1, snd_1) :: tl2)
h : (fst, snd).1 = (fst_1, snd_1).1 ∧ (fst, snd).2 = !(fst_1, snd_1).2
left : (fst, snd).1 = (fst_1, snd_1).1
⊢ (fst, snd).2 = !(fst_1, snd_1).2

Tactic:
cases h
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
tl1 tl2 : List (α × Bool)
fst : α
snd : Bool
fst_1 : α
snd_1 : Bool
htl : reduce tl1 = (fst_1, snd_1) :: tl2
ih : Red tl1 ((fst_1, snd_1) :: tl2)
left : fst = fst_1
right : snd = !snd_1
pos : Red ((fst_1, !snd_1) :: tl1) tl2
⊢ Red ((fst, snd) :: tl1) tl2

Tactic:
subst_vars
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
tl1 tl2 : List (α × Bool)
fst : α
snd : Bool
htl : reduce tl1 = (fst, snd) :: tl2
ih : Red tl1 ((fst, snd) :: tl2)
pos : Red ((fst, !snd) :: (fst, snd) :: tl2) tl2
⊢ Red ((fst, !snd) :: tl1) tl2

Tactic:
apply Red.trans (Red.cons_cons ih)

Premises used: FreeGroup.Red.cons_cons, FreeGroup.Red.trans
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
tl1 tl2 : List (α × Bool)
fst : α
snd : Bool
htl : reduce tl1 = (fst, snd) :: tl2
ih : Red tl1 ((fst, snd) :: tl2)
⊢ Red ((fst, !snd) :: (fst, snd) :: tl2) tl2

Tactic:
Red.Step.cons_not_rev.to_red

Premises used: FreeGroup.Red.Step.to_red, FreeGroup.Red.Step.cons_not_rev
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
tl1 tl2 : List (α × Bool)
fst : α
snd : Bool
htl : reduce tl1 = (fst, snd) :: tl2
ih : Red tl1 ((fst, snd) :: tl2)
⊢ Red ((fst, !snd) :: (fst, snd) :: tl2) tl2

Tactic:
exact Red.Step.cons_not_rev.to_red

Premises used: FreeGroup.Red.Step.to_red, FreeGroup.Red.Step.cons_not_rev
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : ¬(hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2)
⊢ Red (hd1 :: tl1) (hd1 :: hd2 :: tl2)

Tactic:
Red.cons_cons ih

Premises used: FreeGroup.Red.cons_cons
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : ¬(hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2)
⊢ Red (hd1 :: tl1) (hd1 :: hd2 :: tl2)

Tactic:
exact Red.cons_cons ih

Premises used: FreeGroup.Red.cons_cons
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
hd1 : α × Bool
tl1 TL : List (α × Bool)
htl : reduce tl1 = TL
ih : Red tl1 TL
cons :
  ∀ (htl : reduce tl1 = []) (ih : Red tl1 []),
    Red (hd1 :: tl1)
      (List.rec (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) [hd1]
        (fun (head : α × Bool) (tail tail_ih : List (α × Bool)) ↦
          if hd1.1 = head.1 ∧ hd1.2 = !head.2 then tail else hd1 :: head :: tail)
        [])
cons₁ :
  ∀ (hd2 : α × Bool) (tl2 : List (α × Bool)) (htl : reduce tl1 = hd2 :: tl2) (ih : Red tl1 (hd2 :: tl2)),
    Red (hd1 :: tl1)
      (List.rec (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) [hd1]
        (fun (head : α × Bool) (tail tail_ih : List (α × Bool)) ↦
          if hd1.1 = head.1 ∧ hd1.2 = !head.2 then tail else hd1 :: head :: tail)
        (hd2 :: tl2))
⊢ Red (hd1 :: tl1)
    (List.rec (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) [hd1]
      (fun (head : α × Bool) (tail tail_ih : List (α × Bool)) ↦
        if hd1.1 = head.1 ∧ hd1.2 = !head.2 then tail else hd1 :: head :: tail)
      TL)

Tactic:
cases TL with
    | nil => exact Red.cons_cons ih
    | cons hd2 tl2 =>
      dsimp only
      split_ifs with h
      · cases hd1
        cases hd2
        cases h
        dsimp at *
        subst_vars
        apply Red.trans (Red.cons_cons ih)
        exact Red.Step.cons_not_rev.to_red
      · exact Red.cons_cons ih

Premises used: FreeGroup.Red.Step.to_red, FreeGroup.reduce.cons, FreeGroup.Red.cons_cons, FreeGroup.Red.Step.cons_not_rev, FreeGroup.Red.trans
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
nil : Red.{u_1} (α := α) [] (reduce [])
cons : ∀ (hd1 : α × Bool) (tl1 : List (α × Bool)) (ih : Red tl1 (reduce tl1)), Red (hd1 :: tl1) (reduce (hd1 :: tl1))
⊢ Red L (reduce L)

Tactic:
induction L with
  | nil => constructor
  | cons hd1 tl1 ih =>
    dsimp
    revert ih
    generalize htl : reduce tl1 = TL
    intro ih
    cases TL with
    | nil => exact Red.cons_cons ih
    | cons hd2 tl2 =>
      dsimp only
      split_ifs with h
      · cases hd1
        cases hd2
        cases h
        dsimp at *
        subst_vars
        apply Red.trans (Red.cons_cons ih)
        exact Red.Step.cons_not_rev.to_red
      · exact Red.cons_cons ih

Premises used: FreeGroup.Red.Step.to_red, FreeGroup.reduce.cons, FreeGroup.Red.Step.cons_not_rev
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
L2 L3 : List (α × Bool)
x : α
x_1 : Bool
h : reduce [] = L2 ++ (x, x_1) :: (x, !x_1) :: L3
nil : ∀ (h : reduce [] = [] ++ (x, x_1) :: (x, !x_1) :: L3), p
cons : ∀ (head : α × Bool) (tail : List (α × Bool)) (h : reduce [] = head :: tail ++ (x, x_1) :: (x, !x_1) :: L3), p
⊢ p

Tactic:
cases L2
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
L3 : List (α × Bool)
x : α
x_1 : Bool
h : reduce [] = [] ++ (x, x_1) :: (x, !x_1) :: L3
⊢ p

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
L3 : List (α × Bool)
x : α
x_1 : Bool
head : α × Bool
tail : List (α × Bool)
h : reduce [] = head :: tail ++ (x, x_1) :: (x, !x_1) :: L3
⊢ p

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
dsimp :
  List.rec (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) [(x, b)]
        (fun (head : α × Bool) (tail tail_ih : List (α × Bool)) ↦
          if x = head.1 ∧ b = !head.2 then tail else (x, b) :: head :: tail)
        (reduce L1) =
      L2 ++ (x', b') :: (x', !b') :: L3 →
    p
⊢ reduce ((x, b) :: L1) = L2 ++ (x', b') :: (x', !b') :: L3 → p

Tactic:
dsimp
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
r : reduce L1 = []
h : [(x, b)] = L2 ++ (x', b') :: (x', !b') :: L3
nil : False
⊢ p

Tactic:
exfalso
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
r : reduce L1 = []
h : [(x, b)] = L2 ++ (x', b') :: (x', !b') :: L3
⊢ [(x, b)].length = (L2 ++ (x', b') :: (x', !b') :: L3).length

Tactic:
have := congr_arg List.length h
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
r : reduce L1 = []
h : [(x, b)] = L2 ++ (x', b') :: (x', !b') :: L3
this : [(x, b)].length = (L2 ++ (x', b') :: (x', !b') :: L3).length
⊢ False

Tactic:
grind
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
hd : α × Bool
tail : List (α × Bool)
r : reduce L1 = hd :: tail
cons :
  ∀ (y : α) (c : Bool) (r : reduce L1 = (y, c) :: tail),
    List.rec (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) [(x, b)]
          (fun (head : α × Bool) (tail tail_ih : List (α × Bool)) ↦
            if x = head.1 ∧ b = !head.2 then tail else (x, b) :: head :: tail)
          ((y, c) :: tail) =
        L2 ++ (x', b') :: (x', !b') :: L3 →
      p
⊢ List.rec (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) [(x, b)]
        (fun (head : α × Bool) (tail tail_ih : List (α × Bool)) ↦
          if x = head.1 ∧ b = !head.2 then tail else (x, b) :: head :: tail)
        (hd :: tail) =
      L2 ++ (x', b') :: (x', !b') :: L3 →
    p

Tactic:
obtain ⟨y, c⟩ := hd
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
cons : (if x = y ∧ b = !c then tail else (x, b) :: (y, c) :: tail) = L2 ++ (x', b') :: (x', !b') :: L3 → p
⊢ List.rec (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) [(x, b)]
        (fun (head : α × Bool) (tail tail_ih : List (α × Bool)) ↦
          if x = head.1 ∧ b = !head.2 then tail else (x, b) :: head :: tail)
        ((y, c) :: tail) =
      L2 ++ (x', b') :: (x', !b') :: L3 →
    p

Tactic:
dsimp only
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
pos : ∀ (h : x = y ∧ b = !c), tail = L2 ++ (x', b') :: (x', !b') :: L3 → p
neg : ∀ (h : ¬(x = y ∧ b = !c)), (x, b) :: (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3 → p
⊢ (if x = y ∧ b = !c then tail else (x, b) :: (y, c) :: tail) = L2 ++ (x', b') :: (x', !b') :: L3 → p

Tactic:
split_ifs with h
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : x = y ∧ b = !c
H : tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ reduce L1 = (y, c) :: (L2 ++ (x', b') :: (x', !b') :: L3)

Tactic:
rw [H] at r
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : x = y ∧ b = !c
H : tail = L2 ++ (x', b') :: (x', !b') :: L3
r₁ : reduce L1 = (y, c) :: (L2 ++ (x', b') :: (x', !b') :: L3)
⊢ x = y ∧ b = !c

Tactic:
rw [H] at r
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : x = y ∧ b = !c
H : tail = L2 ++ (x', b') :: (x', !b') :: L3
r₁ : reduce L1 = (y, c) :: (L2 ++ (x', b') :: (x', !b') :: L3)
h₁ : x = y ∧ b = !c
⊢ tail = L2 ++ (x', b') :: (x', !b') :: L3

Tactic:
rw [H] at r
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: (L2 ++ (x', b') :: (x', !b') :: L3)
h : x = y ∧ b = !c
H : tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ p

Tactic:
@reduce.not _ L1 ((y, c) :: L2) L3 x' b' r
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: (L2 ++ (x', b') :: (x', !b') :: L3)
h : x = y ∧ b = !c
H : tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ p

Tactic:
exact @reduce.not _ L1 ((y, c) :: L2) L3 x' b' r
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
H : (x, b) :: (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3
neg : ∀ (H : (x, b) :: (y, c) :: tail = [] ++ (x', b') :: (x', !b') :: L3), p
neg₁ :
  ∀ (a : α × Bool) (L2 : List (α × Bool)) (H : (x, b) :: (y, c) :: tail = a :: L2 ++ (x', b') :: (x', !b') :: L3), p
⊢ p

Tactic:
rcases L2 with (_ | ⟨a, L2⟩)
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
H : (x, b) :: (y, c) :: tail = [] ++ (x', b') :: (x', !b') :: L3
⊢ x = x'

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
H : (x, b) :: (y, c) :: tail = [] ++ (x', b') :: (x', !b') :: L3
fst_eq : x = x'
⊢ b = b'

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
H : (x, b) :: (y, c) :: tail = [] ++ (x', b') :: (x', !b') :: L3
fst_eq : x = x'
snd_eq : b = b'
⊢ tail = L3

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
H : (x, b) :: (y, c) :: tail = [] ++ (x', b') :: (x', !b') :: L3
fst_eq : x = x'
snd_eq : b = b'
tail_eq : tail = L3
⊢ y = x'

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
H : (x, b) :: (y, c) :: tail = [] ++ (x', b') :: (x', !b') :: L3
fst_eq : x = x'
snd_eq : b = b'
tail_eq : tail = L3
fst_eq₁ : y = x'
⊢ c = !b'

Tactic:
injections
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
fst_eq : x = x'
snd_eq : b = b'
tail_eq : tail = L3
fst_eq_1 : y = x'
snd_eq_1 : c = !b'
⊢ reduce L1 = (y, !b') :: tail

Tactic:
subst_vars
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
fst_eq : x = x'
snd_eq : b = b'
tail_eq : tail = L3
fst_eq_1 : y = x'
snd_eq_1 : c = !b'
r₁ : reduce L1 = (y, !b') :: tail
⊢ ¬(y = y ∧ b' = !!b')

Tactic:
subst_vars
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
L1 : List (α × Bool)
b' : Bool
tail : List (α × Bool)
y : α
r : reduce L1 = (y, !b') :: tail
h : ¬(y = y ∧ b' = !!b')
⊢ p

Tactic:
simp at h
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
H : (x, b) :: (y, c) :: tail = a :: L2 ++ (x', b') :: (x', !b') :: L3
⊢ p

Tactic:
@reduce.not _ L1 L2 L3 x' b' ?_
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
H : (x, b) :: (y, c) :: tail = a :: L2 ++ (x', b') :: (x', !b') :: L3
neg : reduce L1 = L2 ++ (x', b') :: (x', !b') :: L3
⊢ p

Tactic:
refine @reduce.not _ L1 L2 L3 x' b' ?_
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
H : (x, b) :: (y, c) :: tail = a :: L2 ++ (x', b') :: (x', !b') :: L3
⊢ (x, b) :: (y, c) :: tail = a :: (L2 ++ (x', b') :: (x', !b') :: L3)

Tactic:
rw [List.cons_append] at H

Premises used: List.cons_append
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
H : (x, b) :: (y, c) :: tail = a :: (L2 ++ (x', b') :: (x', !b') :: L3)
⊢ (x, b) = a

Tactic:
injection H with _ H
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
H : (x, b) :: (y, c) :: tail = a :: (L2 ++ (x', b') :: (x', !b') :: L3)
head_eq : (x, b) = a
⊢ (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3

Tactic:
injection H with _ H
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
head_eq : (x, b) = a
H neg : (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3
neg₁ neg₂ : L2 ++ (x', b') :: (x', !b') :: L3 = L2 ++ (x', b') :: (x', !b') :: L3
⊢ reduce L1 = L2 ++ (x', b') :: (x', !b') :: L3

Tactic:
rw [r, H]