awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₁₂ : List (α × Bool)
eq : L₁ ++ L₂ = L₁₂
h : Red L L₁₂
refl :
  ∀ {L₁ L₂ : List (α × Bool)} (eq : L₁ ++ L₂ = L),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
tail :
  ∀ {b c : List (α × Bool)} (hLL' : ReflTransGen Step L b) (h : Step b c)
    (ih :
      ∀ {L₁ L₂ : List (α × Bool)} (eq : L₁ ++ L₂ = b),
        ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂)
    {L₁ L₂ : List (α × Bool)} (eq : L₁ ++ L₂ = c),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
⊢ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Tactic:
induction h generalizing L₁ L₂ with
      | refl => exact ⟨_, _, eq.symm, by rfl, by rfl⟩
      | tail hLL' h ih =>
        obtain @⟨s, e, a, b⟩ := h
        rcases List.append_eq_append_iff.1 eq with (⟨s', rfl, rfl⟩ | ⟨e', rfl, rfl⟩)
        · have : L₁ ++ (s' ++ (a, b) :: (a, not b) :: e) =
            L₁ ++ s' ++ (a, b) :: (a, not b) :: e := by simp
          rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩
          exact ⟨w₁, w₂, rfl, h₁, h₂.tail Step.not⟩
        · have : s ++ (a, b) :: (a, not b) :: e' ++ L₂ =
            s ++ (a, b) :: (a, not b) :: (e' ++ L₂) := by simp
          rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩
          exact ⟨w₁, w₂, rfl, h₁.tail Step.not, h₂⟩

Premises used: FreeGroup.Red.refl, Iff.mp, rfl, List.append_eq_append_iff
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
⊢ Red [] L ↔ L = []

Tactic:
reflTransGen_iff_eq fun _ => Red.not_step_nil

Premises used: FreeGroup.Red.not_step_nil, Relation.reflTransGen_iff_eq, FreeGroup.Red
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ : List (α × Bool)
x : α × Bool
⊢ Red [x] L₁ ↔ L₁ = [x]

Tactic:
reflTransGen_iff_eq fun _ => not_step_singleton

Premises used: FreeGroup.Red.not_step_singleton, Relation.reflTransGen_iff_eq, FreeGroup.Red
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
⊢ Red ((x, !b) :: (x, b) :: L) [(x, !b)]

Tactic:
have h₁ : Red ((x, not b) :: (x, b) :: L) [(x, not b)] := cons_cons h
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
⊢ Red ((x, !b) :: (x, b) :: L) L

Tactic:
have h₂ : Red ((x, not b) :: (x, b) :: L) L := ReflTransGen.single Step.cons_not_rev
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂ : Red ((x, !b) :: (x, b) :: L) L
let : ∀ (L' : List (α × Bool)) (h₁ : Red [(x, !b)] L') (h₂ : Red L L'), Red L [(x, !b)]
⊢ Red L [(x, !b)]

Tactic:
let ⟨L', h₁, h₂⟩ := church_rosser h₁ h₂
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁_1 : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂_1 : Red ((x, !b) :: (x, b) :: L) L
L' : List (α × Bool)
h₁ : Red [(x, !b)] L'
h₂ : Red L L'
⊢ L' = [(x, !b)]

Tactic:
rw [singleton_iff] at h₁

Premises used: FreeGroup.Red.singleton_iff
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁_1 : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂_1 : Red ((x, !b) :: (x, b) :: L) L
L' : List (α × Bool)
h₁ : Red [(x, !b)] L'
h₂ : Red L L'
h₃ : L' = [(x, !b)]
⊢ Red L L'

Tactic:
rw [singleton_iff] at h₁

Premises used: FreeGroup.Red.singleton_iff
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁_1 : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂_1 : Red ((x, !b) :: (x, b) :: L) L
L' : List (α × Bool)
h₁ : L' = [(x, !b)]
h₂ : Red L L'
⊢ Red L [(x, !b)]

Tactic:
subst L'
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂_1 : Red ((x, !b) :: (x, b) :: L) L
h₂ : Red L [(x, !b)]
⊢ Red L [(x, !b)]

Tactic:
assumption
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
h₁ : ∀ (b : List (α × Bool)), ¬Step [(x1, !b1), (x2, b2)] b
⊢ Red [(x1, !b1), (x2, b2)] L ↔ L = [(x1, !b1), (x2, b2)]

Tactic:
apply reflTransGen_iff_eq

Premises used: Relation.reflTransGen_iff_eq
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
h₁ : ∀ (L' : List (α × Bool)) (eq : [(x1, !b1), (x2, b2)] = L') (b : List (α × Bool)), ¬Step L' b
⊢ ∀ (b : List (α × Bool)), ¬Step [(x1, !b1), (x2, b2)] b

Tactic:
generalize eq : [(x1, not b1), (x2, b2)] = L'

Premises used: Bool.not, Prod.mk
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L_1 : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L' : List (α × Bool)
eq : [(x1, !b1), (x2, b2)] = L'
L : List (α × Bool)
h' : Step L' L
h₁ : ∀ {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool} (eq : [(x1, !b1), (x2, b2)] = L₁ ++ (x, b) :: (x, !b) :: L₂), False
⊢ False

Tactic:
cases h'
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L₁ L₂ : List (α × Bool)
x : α
b : Bool
eq : [(x1, !b1), (x2, b2)] = L₁ ++ (x, b) :: (x, !b) :: L₂
⊢ L₁ = [] ∧ (x = x1 ∧ b = !b1) ∧ (x = x2 ∧ (!b) = b2) ∧ L₂ = []

Tactic:
simp only [List.cons_eq_append_iff, List.cons.injEq, Prod.mk.injEq, and_false,
    List.nil_eq_append_iff, exists_const, or_self, or_false, List.cons_ne_nil] at eq

Premises used: List.nil_eq_append_iff, List.cons.injEq, Prod.mk.injEq, List.cons_ne_nil, exists_const, or_self, or_false, and_false, List.cons_eq_append_iff
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L₁ L₂ : List (α × Bool)
x : α
b : Bool
eq : L₁ = [] ∧ (x = x1 ∧ b = !b1) ∧ (x = x2 ∧ (!b) = b2) ∧ L₂ = []
⊢ (x, b1) ≠ (x, !!b1)

Tactic:
rcases eq with ⟨rfl, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
b1 : Bool
x : α
h : (x, b1) ≠ (x, !!b1)
⊢ False

Tactic:
simp at h
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
⊢ Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)

Tactic:
have : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂) := H2
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
nil :
  ∀ (L₄ : List (α × Bool)) (eq : (x1, b1) :: L₁ = [] ++ L₄) (h₁ : Red [] [(x2, b2)]) (h₂ : Red L₄ L₂),
    Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
cons :
  ∀ (p : α × Bool) (L₃ L₄ : List (α × Bool)) (eq : (x1, b1) :: L₁ = p :: L₃ ++ L₄) (h₁ : Red (p :: L₃) [(x2, b2)])
    (h₂ : Red L₄ L₂), Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)

Tactic:
rcases to_append_iff.1 this with ⟨_ | ⟨p, L₃⟩, L₄, eq, h₁, h₂⟩

Premises used: FreeGroup.Red.to_append_iff, Iff.mp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
L₄ : List (α × Bool)
eq : (x1, b1) :: L₁ = [] ++ L₄
h₁ : Red [] [(x2, b2)]
h₂ : Red L₄ L₂
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)

Tactic:
simp [nil_iff] at h₁

Premises used: FreeGroup.Red.nil_iff
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
p : α × Bool
L₃ L₄ : List (α × Bool)
eq : (x1, b1) :: L₁ = p :: L₃ ++ L₄
h₁ : Red (p :: L₃) [(x2, b2)]
h₂ : Red L₄ L₂
cons :
  ∀ (h₁ : Red ((x1, b1) :: L₃) [(x2, b2)]) (H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂))
    (this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)), Red (L₃.append L₄) ((x1, !b1) :: (x2, b2) :: L₂)
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)

Tactic:
cases eq
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)
cons : Red (L₃ ++ L₄) ([(x1, !b1), (x2, b2)] ++ L₂)
⊢ Red (L₃.append L₄) ((x1, !b1) :: (x2, b2) :: L₂)

Tactic:
change Red (L₃ ++ L₄) ([(x1, not b1), (x2, b2)] ++ L₂)

Premises used: Bool.not, Prod.mk, List.cons, HAppend.hAppend, FreeGroup.Red, List.nil
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)
apply : Red L₃ [(x1, !b1), (x2, b2)]
⊢ Red (L₃ ++ L₄) ([(x1, !b1), (x2, b2)] ++ L₂)

Tactic:
apply append_append _ h₂

Premises used: FreeGroup.Red.append_append
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)
⊢ Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]

Tactic:
have h₁ : Red ((x1, not b1) :: (x1, b1) :: L₃) [(x1, not b1), (x2, b2)] := cons_cons h₁
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁_1 : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)
h₁ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
⊢ Red ((x1, !b1) :: (x1, b1) :: L₃) L₃

Tactic:
have h₂ : Red ((x1, not b1) :: (x1, b1) :: L₃) L₃ := Step.cons_not_rev.to_red
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂_1 : Red L₄ L₂
h₁_1 : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)
h₁ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂ : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
rcases : ∀ (L' : List (α × Bool)) (h₁ : Red [(x1, !b1), (x2, b2)] L') (h₂ : Red L₃ L'), Red L₃ [(x1, !b1), (x2, b2)]
⊢ Red L₃ [(x1, !b1), (x2, b2)]

Tactic:
rcases church_rosser h₁ h₂ with ⟨L', h₁, h₂⟩

Premises used: FreeGroup.Red.church_rosser
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂_1 : Red L₄ L₂
h₁_1 : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)
h₁_2 : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂_2 : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
L' : List (α × Bool)
h₁ : Red [(x1, !b1), (x2, b2)] L'
h₂ : Red L₃ L'
⊢ L' = [(x1, !b1), (x2, b2)]

Tactic:
rw [red_iff_irreducible H1] at h₁

Premises used: FreeGroup.Red.red_iff_irreducible
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂_1 : Red L₄ L₂
h₁_1 : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)
h₁_2 : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂_2 : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
L' : List (α × Bool)
h₁ : Red [(x1, !b1), (x2, b2)] L'
h₂ : Red L₃ L'
h₃ : L' = [(x1, !b1), (x2, b2)]
⊢ Red L₃ L'

Tactic:
rw [red_iff_irreducible H1] at h₁

Premises used: FreeGroup.Red.red_iff_irreducible
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂_1 : Red L₄ L₂
h₁_1 : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)
h₁_2 : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂_2 : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
L' : List (α × Bool)
h₁ : L' = [(x1, !b1), (x2, b2)]
h₂ : Red L₃ L'
rwa rwa₁ rwa₂ rwa₃ : ∀ (h₂ : Red L₃ [(x1, !b1), (x2, b2)]), Red L₃ [(x1, !b1), (x2, b2)]
⊢ Red L₃ [(x1, !b1), (x2, b2)]

Tactic:
rwa [h₁] at h₂
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
H : Step L₁ L₂
not : ∀ {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool}, L₁ ++ L₂ <+ L₁ ++ (x, b) :: (x, !b) :: L₂
⊢ L₂ <+ L₁

Tactic:
cases H
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
x : α
b : Bool
⊢ L₁ ++ L₂ <+ L₁ ++ (x, b) :: (x, !b) :: L₂

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
⊢ Red L₁ L₂ → L₂ <+ L₁

Tactic:
@reflTransGen_of_isTrans_reflexive
    _ (fun a b => b <+ a) _ _ _
    ⟨List.Sublist.refl⟩
    ⟨fun _a _b _c hab hbc => List.Sublist.trans hbc hab⟩
    (fun _ _ => Red.Step.sublist)

Premises used: Relation.reflTransGen_of_isTrans_reflexive, FreeGroup.Red, FreeGroup.Red.Step.sublist
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
h : Red L₁ L₂
⊢ L₂.length ≤ L₁.length

Tactic:
h.sublist.length_le

Premises used: List.Sublist.length_le, FreeGroup.Red.sublist
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
nil : sizeOf L2 < 1 + (1 + sizeOf b) + (1 + (1 + sizeOf !b) + sizeOf L2)
⊢ sizeOf ([] ++ L2) < sizeOf ([] ++ (x, b) :: (x, !b) :: L2)

Tactic:
dsimp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf L2 < 1 + (1 + sizeOf b) + (1 + (1 + sizeOf !b) + sizeOf L2)

Tactic:
lia
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
cons : 1 + sizeOf hd + sizeOf (tl ++ L2) < 1 + sizeOf hd + sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ sizeOf (hd :: tl ++ L2) < sizeOf (hd :: tl ++ (x, b) :: (x, !b) :: L2)

Tactic:
dsimp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ 1 + sizeOf hd + sizeOf (tl ++ L2) < 1 + sizeOf hd + sizeOf (tl ++ (x, b) :: (x, !b) :: L2)

Tactic:
Nat.add_lt_add_left ih _

Premises used: Nat.add_lt_add_left
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ 1 + sizeOf hd + sizeOf (tl ++ L2) < 1 + sizeOf hd + sizeOf (tl ++ (x, b) :: (x, !b) :: L2)

Tactic:
exact Nat.add_lt_add_left ih _

Premises used: Nat.add_lt_add_left
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
nil : sizeOf ([] ++ L2) < sizeOf ([] ++ (x, b) :: (x, !b) :: L2)
cons :
  ∀ (hd : α × Bool) (tl : List (α × Bool)) (ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)),
    sizeOf (hd :: tl ++ L2) < sizeOf (hd :: tl ++ (x, b) :: (x, !b) :: L2)
⊢ sizeOf (L1 ++ L2) < sizeOf (L1 ++ (x, b) :: (x, !b) :: L2)

Tactic:
induction L1 with
    | nil =>
      dsimp
      lia
    | cons hd tl ih =>
      dsimp
      exact Nat.add_lt_add_left ih _

Premises used: List.cons, List.nil
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
⊢ ∃ (n : ℕ), L₁.length = L₁.length + 2 * n

Tactic:
⟨0, rfl⟩

Premises used: Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
⊢ ∃ (n : ℕ), L₁.length = L₁.length + 2 * n

Tactic:
exact ⟨0, rfl⟩
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ b c : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ b
h₂₃ : Step b c
ih : ∃ (n : ℕ), L₁.length = b.length + 2 * n
tail : ∀ (n : ℕ) (eq : L₁.length = b.length + 2 * n), ∃ (n : ℕ), L₁.length = c.length + 2 * n
⊢ ∃ (n : ℕ), L₁.length = c.length + 2 * n

Tactic:
rcases ih with ⟨n, eq⟩
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ b c : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ b
h₂₃ : Step b c
n : ℕ
eq : L₁.length = b.length + 2 * n
tail : L₁.length = c.length + 2 * (1 + n)
⊢ ∃ (n : ℕ), L₁.length = c.length + 2 * n

Tactic:
exists 1 + n
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ b c : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ b
h₂₃ : Step b c
n : ℕ
eq : L₁.length = b.length + 2 * n
⊢ L₁.length = c.length + 2 * (1 + n)

Tactic:
simp [Nat.mul_add, eq, (Step.length h₂₃).symm, add_assoc]

Premises used: add_assoc, FreeGroup.Red.Step.length, Eq.symm, Nat.mul_add
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
h : Red L₁ L₂
refl : ∃ (n : ℕ), L₁.length = L₁.length + 2 * n
tail :
  ∀ {b c : List (α × Bool)} (_h₁₂ : ReflTransGen Step L₁ b) (h₂₃ : Step b c)
    (ih : ∃ (n : ℕ), L₁.length = b.length + 2 * n), ∃ (n : ℕ), L₁.length = c.length + 2 * n
⊢ ∃ (n : ℕ), L₁.length = L₂.length + 2 * n

Tactic:
induction h with
  | refl => exact ⟨0, rfl⟩
  | tail _h₁₂ h₂₃ ih =>
    rcases ih with ⟨n, eq⟩
    exists 1 + n
    simp [Nat.mul_add, eq, (Step.length h₂₃).symm, add_assoc]

Premises used: add_assoc, List.tail, FreeGroup.Red.refl, Nat.mul_add
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
h₁₂ : Red L₁ L₂
h₂₁ : Red L₂ L₁
⊢ L₁ = L₂

Tactic:
h₂₁.sublist.antisymm h₁₂.sublist

Premises used: FreeGroup.Red.sublist, List.Sublist.antisymm
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x b_1 c b : List (α × Bool)
hab hac : Red.Step x b
⊢ ReflGen Red.Step b b

Tactic:
rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x b_1 c b : List (α × Bool)
hab hac : Red.Step x b
⊢ ReflTransGen Red.Step b b

Tactic:
rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
h : Red.Step L₁ L₂
⊢ Join (ReflTransGen Red.Step) L₁ L₂

Tactic:
join_of_single h.to_red

Premises used: FreeGroup.Red.Step.to_red, Relation.join_of_single
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
h : Red.Step L₁ L₂
⊢ Join (ReflTransGen Red.Step) L₁ L₂

Tactic:
exact join_of_single h.to_red
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
⊢ EqvGen Red.Step L₁ L₂ ↔ Join Red L₁ L₂

Tactic:
Iff.intro
    (fun h =>
      have : EqvGen (Join Red) L₁ L₂ := h.mono fun _ _ => join_red_of_step
      equivalence_join_red.eqvGen_iff.1 this)
    (join_of_equivalence (Relation.EqvGen.is_equivalence _) fun _ _ =>
      reflTransGen_of_equivalence (Relation.EqvGen.is_equivalence _) EqvGen.rel)

Premises used: FreeGroup.join_red_of_step, FreeGroup.Red.Step, Relation.reflTransGen_of_equivalence, Relation.EqvGen.mono, FreeGroup.equivalence_join_red, Relation.EqvGen.is_equivalence, Relation.join_of_equivalence, Iff.intro, Relation.EqvGen.rel, Iff.mp, Equivalence.eqvGen_iff
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
⊢ IsReduced.{u} (α := α) []

Tactic:
isChain_nil

Premises used: List.isChain_nil, FreeGroup.IsReduced
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
a : α × Bool
⊢ IsReduced [a]

Tactic:
isChain_singleton a

Premises used: List.isChain_singleton, FreeGroup.IsReduced
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
a b : α × Bool
⊢ IsReduced (a :: b :: L) ↔ (a.1 = b.1 → a.2 = b.2) ∧ IsReduced (b :: L)

Tactic:
isChain_cons_cons

Premises used: FreeGroup.IsReduced, List.isChain_cons_cons
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
h : IsReduced L₁
step : Red.Step L₁ L₂
not : ∀ {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool} (h : IsReduced (L₁ ++ (x, b) :: (x, !b) :: L₂)), False
⊢ False

Tactic:
induction step
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ L₁_1 L₂_1 : List (α × Bool)
x : α
b : Bool
h : IsReduced (L₁_1 ++ (x, b) :: (x, !b) :: L₂_1)
⊢ False

Tactic:
simp [IsReduced] at h

Premises used: FreeGroup.IsReduced
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
a₁ : α
b₁ : Bool
a₂ : α
b₂ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: (a₂, b₂) :: L₁) L₂
rw : ((a₁, b₁).1 = (a₂, b₂).1 → (a₁, b₁).2 = (a₂, b₂).2) ∧ IsReduced ((a₂, b₂) :: L₁)
⊢ IsReduced ((a₁, b₁) :: (a₂, b₂) :: L₁)

Tactic:
rw [isReduced_cons_cons]

Premises used: FreeGroup.isReduced_cons_cons
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
a₁ : α
b₁ : Bool
a₂ : α
b₂ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: (a₂, b₂) :: L₁) L₂
⊢ ((a₁, b₁).1 = (a₂, b₂).1 → (a₁, b₁).2 = (a₂, b₂).2) ∧ IsReduced ((a₂, b₂) :: L₁)

Tactic:
⟨?_, .of_forall_not_step fun L₂ step ↦ hL₁ _ step.cons⟩

Premises used: Prod.mk, List.cons, And.intro, FreeGroup.Red.Step.cons
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
a₁ : α
b₁ : Bool
a₂ : α
b₂ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: (a₂, b₂) :: L₁) L₂
refine : (a₁, b₁).1 = (a₂, b₂).1 → (a₁, b₁).2 = (a₂, b₂).2
⊢ ((a₁, b₁).1 = (a₂, b₂).1 → (a₁, b₁).2 = (a₂, b₂).2) ∧ IsReduced ((a₂, b₂) :: L₁)

Tactic:
refine ⟨?_, .of_forall_not_step fun L₂ step ↦ hL₁ _ step.cons⟩
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
a₁ : α
b₁ b₂ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: ((a₁, b₁).1, b₂) :: L₁) L₂
symm : ((a₁, b₁).1, b₂).2 = (a₁, b₁).2
⊢ (a₁, b₁).2 = ((a₁, b₁).1, b₂).2

Tactic:
symm
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
a₁ : α
b₁ b₂ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: ((a₁, b₁).1, b₂) :: L₁) L₂
rw : ((a₁, b₁).1, b₂).2 ≠ !(a₁, b₁).2
⊢ ((a₁, b₁).1, b₂).2 = (a₁, b₁).2

Tactic:
rw [← Bool.ne_not]

Premises used: Bool.ne_not
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
a₁ : α
b₁ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: ((a₁, b₁).1, !(a₁, b₁).2) :: L₁) L₂
⊢ False

Tactic:
hL₁ L₁ <| .not (L₁ := [])

Premises used: FreeGroup.Red.Step.not
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
a₁ : α
b₁ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: ((a₁, b₁).1, !(a₁, b₁).2) :: L₁) L₂
⊢ False

Tactic:
exact hL₁ L₁ <| .not (L₁ := [])
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
h : IsReduced L₁
⊢ Red L₁ L₂ ↔ L₂ = L₁

Tactic:
Relation.reflTransGen_iff_eq fun _ => h.not_step

Premises used: FreeGroup.IsReduced.not_step, Relation.reflTransGen_iff_eq, FreeGroup.Red
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsReduced (L₁ ++ L₂)
h₂ : IsReduced (L₂ ++ L₃)
hn : L₂ ≠ []
⊢ IsReduced (L₁ ++ L₂ ++ L₃)

Tactic:
IsChain.append_overlap h₁ h₂ hn

Premises used: FreeGroup.IsReduced, List.IsChain.append_overlap
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
h : IsReduced L₂
h' : L₁ <:+: L₂
⊢ IsReduced L₁

Tactic:
IsChain.infix h h'

Premises used: List.IsChain.infix, FreeGroup.IsReduced
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
⊢ Quot.mk Red.Step L = mk L

Tactic:
rfl

Premises used: FreeGroup.mk, rfl