awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α × Bool
n : ℕ
ih : reduce (List.replicate n x) = List.replicate n x
⊢ (List.casesOn (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) (List.replicate n x) [x]
      fun (hd : α × Bool) (tl : List (α × Bool)) ↦ if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
    x :: List.replicate n x
have succ : ∀ (ih : reduce (List.replicate 0 x) = List.replicate 0 x),
  (List.casesOn (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) (List.replicate 0 x) [x]
      fun (hd : α × Bool) (tl : List (α × Bool)) ↦ if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
    x :: List.replicate 0 x
Tactic: cases n with
    | zero => simp
    | succ n => simp [List.replicate_succ]
Cleared hypotheses: n, ih
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α × Bool
n : ℕ
ih : reduce (List.replicate n x) = List.replicate n x
succ :
  ∀ (ih : reduce (List.replicate 0 x) = List.replicate 0 x),
    (List.casesOn (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) (List.replicate 0 x) [x]
        fun (hd : α × Bool) (tl : List (α × Bool)) ↦ if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
      x :: List.replicate 0 x
⊢ (List.casesOn (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) (List.replicate n x) [x]
      fun (hd : α × Bool) (tl : List (α × Bool)) ↦ if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
    x :: List.replicate n x
have succ₁ : ∀ (n : ℕ) (ih : reduce (List.replicate (n + 1) x) = List.replicate (n + 1) x),
  (List.casesOn (motive := fun (x : List (α × Bool)) ↦ List (α × Bool)) (List.replicate (n + 1) x) [x]
      fun (hd : α × Bool) (tl : List (α × Bool)) ↦ if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
    x :: List.replicate (n + 1) x
Tactic: cases n with
    | zero => simp
    | succ n => simp [List.replicate_succ]
Cleared hypotheses: n, ih
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
x : α × Bool
⊢ reduce (List.replicate n x) = List.replicate n x
have zero : reduce (List.replicate 0 x) = List.replicate 0 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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
x : α × Bool
zero : reduce (List.replicate 0 x) = List.replicate 0 x
⊢ reduce (List.replicate n x) = List.replicate n x
have succ : ∀ (n : ℕ) (ih : reduce (List.replicate n x) = List.replicate n x),
  reduce (List.replicate (n + 1) x) = List.replicate (n + 1) 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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
ih : Red tl1 (reduce tl1)
⊢ Red (hd1 :: tl1) (reduce (hd1 :: tl1))
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
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))
have 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))
Tactic: revert ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
⊢ ∀ (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))
have 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)
Tactic: generalize htl : reduce tl1 = TL
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
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)
⊢ Red (hd1 :: tl1) (if hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2 then tl2 else hd1 :: hd2 :: tl2)
have pos : ∀ (h : hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2), Red (hd1 :: tl1) tl2
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
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
⊢ Red (hd1 :: tl1) (if hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2 then tl2 else hd1 :: hd2 :: tl2)
have neg : ∀ (h : ¬(hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2)), Red (hd1 :: tl1) (hd1 :: hd2 :: tl2)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
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) tl2
have pos : ∀ (fst : α) (snd : Bool) (h : (fst, snd).1 = hd2.1 ∧ (fst, snd).2 = !hd2.2), Red ((fst, snd) :: tl1) tl2
Tactic: cases hd1
Cleared hypotheses: hd1, h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
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
⊢ Red ((fst, snd) :: tl1) tl2
have 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
Tactic: cases hd2
Cleared hypotheses: hd2, htl, ih, h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (hypothesis)
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
⊢ Red ((fst, snd) :: tl1) tl2
have left : (fst, snd).1 = (fst_1, snd_1).1
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (hypothesis)
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
⊢ Red ((fst, snd) :: tl1) tl2
have right : (fst, snd).2 = !(fst_1, snd_1).2
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
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
⊢ Red ((fst, snd) :: tl1) tl2
have pos : Red ((fst_1, !snd_1) :: tl1) tl2
Tactic: subst_vars
Cleared hypotheses: fst, snd, left, right
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
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) :: tl1) tl2
have pos : Red ((fst, !snd) :: (fst, snd) :: tl2) tl2
Tactic: apply Red.trans (Red.cons_cons ih)
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
hd1 : α × Bool
tl1 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)
have 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)
      [])
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
Cleared hypotheses: TL, htl, ih
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
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)
        [])
⊢ 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)
have 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))
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
Cleared hypotheses: TL, htl, ih
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
⊢ Red L (reduce L)
have nil : Red.{u_1} (α := α) [] (reduce [])
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
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
nil : Red.{u_1} (α := α) [] (reduce [])
⊢ Red L (reduce L)
have cons : ∀ (hd1 : α × Bool) (tl1 : List (α × Bool)) (ih : Red tl1 (reduce tl1)), Red (hd1 :: tl1) (reduce (hd1 :: tl1))
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
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
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
⊢ p
have nil : ∀ (h : reduce [] = [] ++ (x, x_1) :: (x, !x_1) :: L3), p
Tactic: cases L2
Cleared hypotheses: L2, h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
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
⊢ p
have cons : ∀ (head : α × Bool) (tail : List (α × Bool)) (h : reduce [] = head :: tail ++ (x, x_1) :: (x, !x_1) :: L3), p
Tactic: cases L2
Cleared hypotheses: L2, h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
⊢ reduce ((x, b) :: L1) = L2 ++ (x', b') :: (x', !b') :: L3 → p
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
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
⊢ p
have nil : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (hypothesis)
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
⊢ False
have this : [(x, b)].length = (L2 ++ (x', b') :: (x', !b') :: L3).length
Tactic: have := congr_arg List.length h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
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
⊢ 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
have 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
Tactic: obtain ⟨y, c⟩ := hd
Cleared hypotheses: hd, r
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
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
⊢ 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
have cons : (if x = y ∧ b = !c then tail else (x, b) :: (y, c) :: tail) = L2 ++ (x', b') :: (x', !b') :: L3 → p
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
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
⊢ (if x = y ∧ b = !c then tail else (x, b) :: (y, c) :: tail) = L2 ++ (x', b') :: (x', !b') :: L3 → p
have pos : ∀ (h : x = y ∧ b = !c), tail = L2 ++ (x', b') :: (x', !b') :: L3 → p
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
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
⊢ (if x = y ∧ b = !c then tail else (x, b) :: (y, c) :: tail) = L2 ++ (x', b') :: (x', !b') :: L3 → p
have neg : ∀ (h : ¬(x = y ∧ b = !c)), (x, b) :: (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3 → p
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (hypothesis)
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
⊢ p
have r₁ : reduce L1 = (y, c) :: (L2 ++ (x', b') :: (x', !b') :: L3)
Tactic: rw [H] at r
Cleared hypotheses: r, h, H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
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
⊢ p
have neg : ∀ (H : (x, b) :: (y, c) :: tail = [] ++ (x', b') :: (x', !b') :: L3), p
Tactic: rcases L2 with (_ | ⟨a, L2⟩)
Cleared hypotheses: L2, H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
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
⊢ p
have neg₁ : ∀ (a : α × Bool) (L2 : List (α × Bool)) (H : (x, b) :: (y, c) :: tail = a :: L2 ++ (x', b') :: (x', !b') :: L3), p
Tactic: rcases L2 with (_ | ⟨a, L2⟩)
Cleared hypotheses: L2, H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (hypothesis)
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
⊢ p
have fst_eq : x = x'
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (hypothesis)
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'
⊢ p
have snd_eq : b = b'
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (hypothesis)
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'
⊢ p
have tail_eq : tail = L3
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (hypothesis)
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
⊢ p
have fst_eq₁ : y = x'
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (hypothesis)
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'
⊢ p
have snd_eq₁ : c = !b'
Tactic: injections
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (hypothesis)
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'
⊢ p
have r₁ : reduce L1 = (y, !b') :: tail
Tactic: subst_vars
Cleared hypotheses: x, b, L3, x', c, r, h, fst_eq, snd_eq, tail_eq, fst_eq_1, snd_eq_1
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (hypothesis)
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
⊢ p
have h₁ : ¬(y = y ∧ b' = !!b')
Tactic: subst_vars
Cleared hypotheses: x, b, L3, x', c, r, h, fst_eq, snd_eq, tail_eq, fst_eq_1, snd_eq_1
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (goal)
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
have neg : reduce L1 = L2 ++ (x', b') :: (x', !b') :: L3
Tactic: refine @reduce.not _ L1 L2 L3 x' b' ?_
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (hypothesis)
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
⊢ reduce L1 = L2 ++ (x', b') :: (x', !b') :: L3
have H₁ : (x, b) :: (y, c) :: tail = a :: (L2 ++ (x', b') :: (x', !b') :: L3)
Tactic: rw [List.cons_append] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Reduce (hypothesis)
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)
⊢ reduce L1 = L2 ++ (x', b') :: (x', !b') :: L3
have head_eq : (x, b) = a
Tactic: injection H with _ H
Cleared hypotheses: H