awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
LL₁ c L₁ L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step c ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)} (eq₁ : (a, b) :: L₁ = c) (eq₂ : (a, b) :: L₂_1 = (a, b) :: L₂), Red L₁ L₂_1
h₁₂ : (∃ (L : List (α × Bool)), Step L₁ L ∧ c = (a, b) :: L) ∨ L₁ = (a, !b) :: c
head :
  ∀ (L : List (α × Bool)) (h₁₂ : Step L₁ L) (h : ReflTransGen Step ((a, b) :: L) ((a, b) :: L₂))
    (ih :
      ∀ {L₁ L₂_1 : List (α × Bool)} (eq₁ : (a, b) :: L₁ = (a, b) :: L) (eq₂ : (a, b) :: L₂_1 = (a, b) :: L₂),
        Red L₁ L₂_1),
    Red L₁ L₂
⊢ Red L₁ L₂
have head₁ : Red ((a, !b) :: c) L₂
Tactic: rcases h₁₂ with (⟨L, h₁₂, rfl⟩ | rfl)
Cleared hypotheses: L₁, h₁₂
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
LL₂ : List (α × Bool)
eq₂ : p :: L₂ = LL₂
h : Red LL₁ LL₂
⊢ Red L₁ L₂
have refl : ∀ {L₁ L₂ : List (α × Bool)} (eq₁ : p :: L₁ = LL₂) (eq₂ : p :: L₂ = LL₂), Red L₁ L₂
Tactic: induction h using Relation.ReflTransGen.head_induction_on generalizing L₁ L₂ with
      | refl =>
        subst_vars
        cases eq₂
        constructor
      | head h₁₂ h ih =>
        subst_vars
        obtain ⟨a, b⟩ := p
        rw [Step.cons_left_iff] at h₁₂
        rcases h₁₂ with (⟨L, h₁₂, rfl⟩ | rfl)
        · exact (ih rfl rfl).head h₁₂
        · exact (cons_cons h).tail Step.cons_not_rev
Cleared hypotheses: L₁, L₂, eq₁, eq₂, h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
LL₂ : List (α × Bool)
eq₂ : p :: L₂ = LL₂
h : Red LL₁ LL₂
refl : ∀ {L₁ L₂ : List (α × Bool)} (eq₁ : p :: L₁ = LL₂) (eq₂ : p :: L₂ = LL₂), Red L₁ L₂
⊢ Red L₁ L₂
have head : ∀ {a c : List (α × Bool)} (h₁₂ : Step a c) (h : ReflTransGen Step c LL₂)
  (ih : ∀ {L₁ L₂ : List (α × Bool)} (eq₁ : p :: L₁ = c) (eq₂ : p :: L₂ = LL₂), Red L₁ L₂) {L₁ L₂ : List (α × Bool)}
  (eq₁ : p :: L₁ = a) (eq₂ : p :: L₂ = LL₂), Red L₁ L₂
Tactic: induction h using Relation.ReflTransGen.head_induction_on generalizing L₁ L₂ with
      | refl =>
        subst_vars
        cases eq₂
        constructor
      | head h₁₂ h ih =>
        subst_vars
        obtain ⟨a, b⟩ := p
        rw [Step.cons_left_iff] at h₁₂
        rcases h₁₂ with (⟨L, h₁₂, rfl⟩ | rfl)
        · exact (ih rfl rfl).head h₁₂
        · exact (cons_cons h).tail Step.cons_not_rev
Cleared hypotheses: L₁, L₂, eq₁, eq₂, h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L L₁ L₂ : List (α × Bool)
⊢ Red L (L₁ ++ L₂) → ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
have generalize : ∀ (L₁₂ : List (α × Bool)) (eq : L₁ ++ L₂ = L₁₂),
  Red L L₁₂ → ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
Tactic: generalize eq : L₁ ++ L₂ = L₁₂
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L L₁₂ 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₂
have tail : ∀ {s e : List (α × Bool)} {a : α} {b : Bool} (hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: e))
  (ih :
    ∀ {L₁ L₂ : List (α × Bool)} (eq : L₁ ++ L₂ = s ++ (a, b) :: (a, !b) :: e),
      ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂)
  (eq : L₁ ++ L₂ = s ++ e), ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
Tactic: obtain @⟨s, e, a, b⟩ := h
Cleared hypotheses: b, c, hLL', h, ih, eq
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L L₁₂ L₁ L₂ s e : List (α × Bool)
a : α
b : Bool
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁ L₂ : List (α × Bool)} (eq : L₁ ++ L₂ = s ++ (a, b) :: (a, !b) :: e),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
eq : L₁ ++ L₂ = s ++ e
⊢ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
have tail : ∀ (s' : List (α × Bool)) (hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e))
  (ih :
    ∀ {L₁_1 L₂ : List (α × Bool)} (eq : L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e),
      ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂)
  (eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e),
  ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)
Tactic: rcases List.append_eq_append_iff.1 eq with (⟨s', rfl, rfl⟩ | ⟨e', rfl, rfl⟩)
Cleared hypotheses: L₂, s, hLL', ih, eq
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L L₁₂ L₁ L₂ s e : List (α × Bool)
a : α
b : Bool
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁ L₂ : List (α × Bool)} (eq : L₁ ++ L₂ = s ++ (a, b) :: (a, !b) :: e),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
eq : L₁ ++ L₂ = s ++ e
tail :
  ∀ (s' : List (α × Bool)) (hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e))
    (ih :
      ∀ {L₁_1 L₂ : List (α × Bool)} (eq : L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e),
        ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂)
    (eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)
⊢ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
have tail₁ : ∀ (e' : List (α × Bool)) (hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: (e' ++ L₂)))
  (ih :
    ∀ {L₁ L₂_1 : List (α × Bool)} (eq : L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)),
      ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1)
  (eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)),
  ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂
Tactic: rcases List.append_eq_append_iff.1 eq with (⟨s', rfl, rfl⟩ | ⟨e', rfl, rfl⟩)
Cleared hypotheses: L₁, e, hLL', ih, eq
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
Goal:
α : Type u
L L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)} (eq : L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
⊢ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)
have this : L₁ ++ (s' ++ (a, b) :: (a, !b) :: e) = L₁ ++ s' ++ (a, b) :: (a, !b) :: e
Tactic: have : L₁ ++ (s' ++ (a, b) :: (a, not b) :: e) =
            L₁ ++ s' ++ (a, b) :: (a, not b) :: e := by simp
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)} (eq : L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
this : L₁ ++ (s' ++ (a, b) :: (a, !b) :: e) = L₁ ++ s' ++ (a, b) :: (a, !b) :: e
⊢ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)
have tail : ∀ (w₁ w₂ : List (α × Bool)) (hLL' : ReflTransGen Step (w₁ ++ w₂) (L₁ ++ s' ++ (a, b) :: (a, !b) :: e))
  (ih :
    ∀ {L₁_1 L₂ : List (α × Bool)} (eq : L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e),
      ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂)
  (h₁ : Red w₁ L₁) (h₂ : Red w₂ (s' ++ (a, b) :: (a, !b) :: e)),
  ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)
Tactic: rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩
Cleared hypotheses: L, hLL', ih
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
Goal:
α : Type u
L L₁₂ L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)} (eq : L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
⊢ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂
have this : s ++ (a, b) :: (a, !b) :: e' ++ L₂ = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)
Tactic: have : s ++ (a, b) :: (a, not b) :: e' ++ L₂ =
            s ++ (a, b) :: (a, not b) :: (e' ++ L₂) := by simp
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L L₁₂ L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)} (eq : L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)),
    ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
this : s ++ (a, b) :: (a, !b) :: e' ++ L₂ = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)
⊢ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂
have tail : ∀ (w₁ w₂ : List (α × Bool)) (hLL' : ReflTransGen Step (w₁ ++ w₂) (s ++ (a, b) :: (a, !b) :: (e' ++ L₂)))
  (ih :
    ∀ {L₁ L₂_1 : List (α × Bool)} (eq : L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)),
      ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1)
  (h₁ : Red w₁ (s ++ (a, b) :: (a, !b) :: e')) (h₂ : Red w₂ L₂),
  ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂
Tactic: rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩
Cleared hypotheses: L, hLL', ih
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L L₁ L₂ L₁₂ : List (α × Bool)
eq : L₁ ++ L₂ = L₁₂
h : Red L L₁₂
⊢ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
have refl : ∀ {L₁ L₂ : List (α × Bool)} (eq : L₁ ++ 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₂⟩
Cleared hypotheses: L₁, L₂, eq, h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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₂
⊢ ∃ (L₃ : List (α × Bool)) (L₄ : List (α × Bool)), L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
have 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₂
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₂⟩
Cleared hypotheses: L₁, L₂, eq, h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
Goal:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
⊢ Red L [(x, !b)]
have h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
Tactic: have h₁ : Red ((x, not b) :: (x, b) :: L) [(x, not b)] := cons_cons h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
Goal:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
⊢ Red L [(x, !b)]
have h₂ : Red ((x, !b) :: (x, b) :: L) L
Tactic: have h₂ : Red ((x, not b) :: (x, b) :: L) L := ReflTransGen.single Step.cons_not_rev
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ Red L [(x, !b)]
have let : ∀ (L' : List (α × Bool)) (h₁ : Red [(x, !b)] L') (h₂ : Red L L'), Red L [(x, !b)]
Tactic: let ⟨L', h₁, h₂⟩ := church_rosser h₁ h₂
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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'
⊢ Red L [(x, !b)]
have h₃ : L' = [(x, !b)]
Tactic: rw [singleton_iff] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
⊢ Red [(x1, !b1), (x2, b2)] L ↔ L = [(x1, !b1), (x2, b2)]
have h₁ : ∀ (b : List (α × Bool)), ¬Step [(x1, !b1), (x2, b2)] b
Tactic: apply reflTransGen_iff_eq
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
⊢ ∀ (b : List (α × Bool)), ¬Step [(x1, !b1), (x2, b2)] b
have h₁ : ∀ (L' : List (α × Bool)) (eq : [(x1, !b1), (x2, b2)] = L') (b : List (α × Bool)), ¬Step L' b
Tactic: generalize eq : [(x1, not b1), (x2, b2)] = L'
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ False
have h₁ : ∀ {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool} (eq : [(x1, !b1), (x2, b2)] = L₁ ++ (x, b) :: (x, !b) :: L₂), False
Tactic: cases h'
Cleared hypotheses: L', eq, L, h'
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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₂
⊢ False
have eq₁ : 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
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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₂ = []
⊢ False
have h₁ : (x, b1) ≠ (x, !!b1)
Tactic: rcases eq with ⟨rfl, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩, rfl⟩
Cleared hypotheses: x1, x2, b2, h, L₁, L₂, b, eq
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 L₁ ((x1, !b1) :: (x2, b2) :: L₂)
have this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
Tactic: have : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂) := H2
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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₂)
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
have nil : ∀ (L₄ : List (α × Bool)) (eq : (x1, b1) :: L₁ = [] ++ L₄) (h₁ : Red [] [(x2, b2)]) (h₂ : Red L₄ L₂),
  Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
Tactic: rcases to_append_iff.1 this with ⟨_ | ⟨p, L₃⟩, L₄, eq, h₁, h₂⟩
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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₂)
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
have 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₂)
Tactic: rcases to_append_iff.1 this with ⟨_ | ⟨p, L₃⟩, L₄, eq, h₁, h₂⟩
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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₂
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
have 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₂)
Tactic: cases eq
Cleared hypotheses: L₁, H2, this, p, eq, h₁
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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 (L₃.append L₄) ((x1, !b1) :: (x2, b2) :: L₂)
have cons : Red (L₃ ++ L₄) ([(x1, !b1), (x2, b2)] ++ L₂)
Tactic: change Red (L₃ ++ L₄) ([(x1, not b1), (x2, b2)] ++ L₂)
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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 (L₃ ++ L₄) ([(x1, !b1), (x2, b2)] ++ L₂)
have apply : Red L₃ [(x1, !b1), (x2, b2)]
Tactic: apply append_append _ h₂
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 L₃ [(x1, !b1), (x2, b2)]
have h₃ : 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₁
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 L₃ [(x1, !b1), (x2, b2)]
have h₃ : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
Tactic: have h₂ : Red ((x1, not b1) :: (x1, b1) :: L₃) L₃ := Step.cons_not_rev.to_red
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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₃
⊢ Red L₃ [(x1, !b1), (x2, b2)]
have rcases : ∀ (L' : List (α × Bool)) (h₁ : Red [(x1, !b1), (x2, b2)] L') (h₂ : Red L₃ L'), Red L₃ [(x1, !b1), (x2, b2)]
Tactic: rcases church_rosser h₁ h₂ with ⟨L', h₁, h₂⟩
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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'
⊢ Red L₃ [(x1, !b1), (x2, b2)]
have h₃ : L' = [(x1, !b1), (x2, b2)]
Tactic: rw [red_iff_irreducible H1] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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'
⊢ Red L₃ [(x1, !b1), (x2, b2)]
have rwa : ∀ (h₂ : Red L₃ [(x1, !b1), (x2, b2)]), Red L₃ [(x1, !b1), (x2, b2)]
Tactic: rwa [h₁] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
H : Step L₁ L₂
⊢ L₂ <+ L₁
have not : ∀ {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool}, L₁ ++ L₂ <+ L₁ ++ (x, b) :: (x, !b) :: L₂
Tactic: cases H
Cleared hypotheses: L₁, L₂, H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf ([] ++ L2) < sizeOf ([] ++ (x, b) :: (x, !b) :: L2)
have nil : sizeOf L2 < 1 + (1 + sizeOf b) + (1 + (1 + sizeOf !b) + sizeOf L2)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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)
⊢ sizeOf (hd :: tl ++ L2) < sizeOf (hd :: tl ++ (x, b) :: (x, !b) :: L2)
have cons : 1 + sizeOf hd + sizeOf (tl ++ L2) < 1 + sizeOf hd + sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf (L1 ++ L2) < sizeOf (L1 ++ (x, b) :: (x, !b) :: L2)
have nil : sizeOf ([] ++ L2) < sizeOf ([] ++ (x, b) :: (x, !b) :: L2)
Tactic: induction L1 with
    | nil =>
      dsimp
      lia
    | cons hd tl ih =>
      dsimp
      exact Nat.add_lt_add_left ih _
Cleared hypotheses: L1