awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
cases :
  ∀ (x_1 : List (α × Bool)) (r : reduce L1 = x_1),
    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)
          x_1 =
        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)
        (reduce L1) =
      L2 ++ (x', b') :: (x', !b') :: L3 →
    p

Tactic:
cases r : reduce L1 with
    | nil =>
      dsimp; intro h
      exfalso
      have := congr_arg List.length h
      grind
    | cons hd tail =>
      obtain ⟨y, c⟩ := hd
      dsimp only
      split_ifs with h <;> intro H
      · rw [H] at r
        exact @reduce.not _ L1 ((y, c) :: L2) L3 x' b' r
      rcases L2 with (_ | ⟨a, L2⟩)
      · injections; subst_vars
        simp at h
      · refine @reduce.not _ L1 L2 L3 x' b' ?_
        rw [List.cons_append] at H
        injection H with _ H
        rw [r, H]

Premises used: FreeGroup.reduce.cons, FreeGroup.reduce, List.cons_append
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
⊢ reduce L₁ = reduce L₁

Tactic:
rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
b c : List (α × Bool)
h : Relation.ReflTransGen Red.Step (reduce L₁) b
H1 : Red.Step b c
H2 : reduce L₁ = b
tail :
  ∀ {L₁_1 L₂ : List (α × Bool)} {x : α} {b : Bool},
    Relation.ReflTransGen Red.Step (reduce L₁) (L₁_1 ++ (x, b) :: (x, !b) :: L₂) →
      ∀ (H2 : reduce L₁ = L₁_1 ++ (x, b) :: (x, !b) :: L₂), reduce L₁ = L₁_1 ++ L₂
⊢ reduce L₁ = c

Tactic:
obtain ⟨L4, L5, x, b⟩ := H1
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
L₁_1 L₂_1 : List (α × Bool)
x : α
b : Bool
h : Relation.ReflTransGen Red.Step (reduce L₁) (L₁_1 ++ (x, b) :: (x, !b) :: L₂_1)
H2 : reduce L₁ = L₁_1 ++ (x, b) :: (x, !b) :: L₂_1
⊢ reduce L₁ = L₁_1 ++ L₂_1

Tactic:
reduce.not H2

Premises used: FreeGroup.reduce.not
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
L₁_1 L₂_1 : List (α × Bool)
x : α
b : Bool
h : Relation.ReflTransGen Red.Step (reduce L₁) (L₁_1 ++ (x, b) :: (x, !b) :: L₂_1)
H2 : reduce L₁ = L₁_1 ++ (x, b) :: (x, !b) :: L₂_1
⊢ reduce L₁ = L₁_1 ++ L₂_1

Tactic:
exact reduce.not H2

Premises used: FreeGroup.reduce.not
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
H : Red (reduce L₁) L₂
refl : reduce L₁ = reduce L₁
tail :
  ∀ {b c : List (α × Bool)},
    Relation.ReflTransGen Red.Step (reduce L₁) b → ∀ (H1 : Red.Step b c) (H2 : reduce L₁ = b), reduce L₁ = c
⊢ reduce L₁ = L₂

Tactic:
induction H with
  | refl => rfl
  | tail _ H1 H2 =>
    obtain ⟨L4, L5, x, b⟩ := H1
    exact reduce.not H2

Premises used: refl
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
⊢ reduce (reduce L) = reduce L

Tactic:
Eq.symm <| reduce.min reduce.red

Premises used: FreeGroup.reduce.red, FreeGroup.reduce.min, Eq.symm
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
H : Red.Step L₁ L₂
⊢ reduce L₁ = reduce L₂

Tactic:
let ⟨_L₃, HR13, HR23⟩ := Red.church_rosser reduce.red (reduce.red.head H)
  (reduce.min HR13).trans (reduce.min HR23).symm

Premises used: FreeGroup.Red.church_rosser, FreeGroup.reduce.red, Relation.ReflTransGen.head, FreeGroup.reduce.min, _private.0.FreeGroup.reduce.Step.eq.match_1, Eq.symm, Eq, FreeGroup.reduce, Eq.trans
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
H : Red L₁ L₂
⊢ reduce L₁ = reduce L₂

Tactic:
let ⟨_L₃, HR13, HR23⟩ := Red.church_rosser reduce.red (Red.trans H reduce.red)
  (reduce.min HR13).trans (reduce.min HR23).symm

Premises used: FreeGroup.Red.church_rosser, FreeGroup.Red.trans, FreeGroup.reduce.red, FreeGroup.reduce.min, _private.0.FreeGroup.reduce.Step.eq.match_1, Eq.symm, Eq, FreeGroup.reduce, Eq.trans
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
h : Red L₁ L₂
⊢ Red L₁ (reduce L₂)

Tactic:
reduce.eq_of_red h ▸ reduce.red

Premises used: FreeGroup.reduce.eq_of_red, Eq.rec, FreeGroup.reduce.red
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
h : Red L₁ L₂
⊢ Red L₂ (reduce L₁)

Tactic:
(reduce.eq_of_red h).symm ▸ reduce.red

Premises used: FreeGroup.reduce.eq_of_red, Eq.rec, FreeGroup.reduce.red, Eq.symm
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
H : mk L₁ = mk L₂
⊢ reduce L₁ = reduce L₂

Tactic:
let ⟨_L₃, H13, H23⟩ := Red.exact.1 H
  (reduce.eq_of_red H13).trans (reduce.eq_of_red H23).symm

Premises used: FreeGroup.reduce.eq_of_red, FreeGroup.Red.exact, Iff.mp, _private.0.FreeGroup.reduce.sound.match_1, Eq.symm, Eq, FreeGroup.reduce, Eq.trans
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
H : reduce L₁ = reduce L₂
⊢ mk L₁ = mk L₂

Tactic:
Red.exact.2 ⟨reduce L₂, H ▸ reduce.red, reduce.red⟩

Premises used: Iff.mpr, Eq.rec, FreeGroup.Red.exact, FreeGroup.reduce.red, And.intro, Exists.intro, FreeGroup.reduce
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
⊢ mk (reduce L) = mk L

Tactic:
reduce.exact reduce.idem

Premises used: FreeGroup.reduce.exact, FreeGroup.reduce.idem
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
H : Red L₁ L₂
⊢ Red L₂ (reduce L₁)

Tactic:
(reduce.eq_of_red H).symm ▸ reduce.red

Premises used: FreeGroup.reduce.eq_of_red, Eq.rec, FreeGroup.reduce.red, Eq.symm
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
⊢ mk (toWord (Quot.mk Red.Step L)) = Quot.mk Red.Step L

Tactic:
reduce.self

Premises used: FreeGroup.toWord, FreeGroup.reduce.self, FreeGroup.mk
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
⊢ mk (toWord (Quot.mk Red.Step L)) = Quot.mk Red.Step L

Tactic:
exact reduce.self

Premises used: FreeGroup.reduce.self
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
a₁ : FreeGroup α
L₁ : List (α × Bool)
a₂ : FreeGroup α
L₂ : List (α × Bool)
⊢ toWord (Quot.mk Red.Step L₁) = toWord (Quot.mk Red.Step L₂) →
    Eq (α := FreeGroup α) (Quot.mk Red.Step L₁) (Quot.mk Red.Step L₂)

Tactic:
reduce.exact

Premises used: FreeGroup.toWord, FreeGroup.reduce.exact, FreeGroup.mk
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
a₁ : FreeGroup α
L₁ : List (α × Bool)
a₂ : FreeGroup α
L₂ : List (α × Bool)
⊢ toWord (Quot.mk Red.Step L₁) = toWord (Quot.mk Red.Step L₂) →
    Eq (α := FreeGroup α) (Quot.mk Red.Step L₁) (Quot.mk Red.Step L₂)

Tactic:
exact reduce.exact

Premises used: FreeGroup.reduce.exact
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
⊢ x.toWord = y.toWord ↔ x = y

Tactic:
toWord_injective.eq_iff

Premises used: Function.Injective.eq_iff, FreeGroup.toWord_injective
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L₁ : List (α × Bool)
inst : DecidableEq α
⊢ (mk L₁).toWord = reduce L₁

Tactic:
rfl

Premises used: FreeGroup.toWord, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ (of a).toWord = [(a, true)]

Tactic:
rfl

Premises used: FreeGroup.toWord, FreeGroup.reduce, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
⊢ reduce (toWord (Quot.mk Red.Step L)) = toWord (Quot.mk Red.Step L)

Tactic:
reduce.idem

Premises used: FreeGroup.toWord, FreeGroup.reduce.idem
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
⊢ reduce (toWord (Quot.mk Red.Step L)) = toWord (Quot.mk Red.Step L)

Tactic:
exact reduce.idem

Premises used: FreeGroup.reduce.idem
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := List (α × Bool)) (toWord 1) []

Tactic:
rfl

Premises used: FreeGroup.toWord, FreeGroup.reduce, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
rw : (mk x.toWord * mk y.toWord).toWord = reduce ((mk x.toWord).toWord ++ (mk y.toWord).toWord)
⊢ (x * y).toWord = reduce (x.toWord ++ y.toWord)

Tactic:
rw [← mk_toWord (x := x), ← mk_toWord (x := y)]

Premises used: FreeGroup.mk_toWord
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
⊢ (mk x.toWord * mk y.toWord).toWord = reduce ((mk x.toWord).toWord ++ (mk y.toWord).toWord)

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x : FreeGroup α
n : ℕ
rw : (mk x.toWord ^ n).toWord = reduce (List.replicate n (mk x.toWord).toWord).flatten
⊢ (x ^ n).toWord = reduce (List.replicate n x.toWord).flatten

Tactic:
rw [← mk_toWord (x := x)]

Premises used: FreeGroup.mk_toWord
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x : FreeGroup α
n : ℕ
⊢ (mk x.toWord ^ n).toWord = reduce (List.replicate n (mk x.toWord).toWord).flatten

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
rw : Quot.lift (r := Red.Step) reduce ⋯ (mk (List.replicate n (a, true))) = List.replicate n (a, true)
⊢ (of a ^ n).toWord = List.replicate n (a, true)

Tactic:
rw [of, pow_mk, List.flatten_replicate_singleton, toWord]

Premises used: List.flatten_replicate_singleton, FreeGroup.of, FreeGroup.toWord, FreeGroup.pow_mk
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
⊢ Quot.lift (r := Red.Step) reduce ⋯ (mk (List.replicate n (a, true))) = List.replicate n (a, true)

Tactic:
reduce_replicate _ _

Premises used: FreeGroup.reduce_replicate
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
⊢ Quot.lift (r := Red.Step) reduce ⋯ (mk (List.replicate n (a, true))) = List.replicate n (a, true)

Tactic:
exact reduce_replicate _ _

Premises used: FreeGroup.reduce_replicate
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x : FreeGroup α
⊢ x.toWord = [] ↔ x = 1

Tactic:
toWord_injective.eq_iff' toWord_one

Premises used: Function.Injective.eq_iff', FreeGroup.toWord_one, FreeGroup.toWord_injective
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
w : List (α × Bool)
H : Red (reduce (invRev w)) (invRev (reduce w))
⊢ reduce (invRev w) = invRev (reduce w)

Tactic:
apply reduce.min

Premises used: FreeGroup.reduce.min
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
w : List (α × Bool)
H : Red (invRev (reduce (invRev w))) (reduce w)
⊢ Red (reduce (invRev w)) (invRev (reduce w))

Tactic:
rw [← red_invRev_iff, invRev_invRev]

Premises used: FreeGroup.red_invRev_iff, FreeGroup.invRev_invRev
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
w : List (α × Bool)
H : Red w (invRev (reduce (invRev w)))
⊢ Red (invRev (reduce (invRev w))) (reduce w)

Tactic:
apply Red.reduce_left

Premises used: FreeGroup.Red.reduce_left
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
w : List (α × Bool)
⊢ Red (invRev (invRev w)) (invRev (reduce (invRev w)))

Tactic:
have : Red (invRev (invRev w)) (invRev (reduce (invRev w))) := reduce.red.invRev
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
w : List (α × Bool)
this : Red (invRev (invRev w)) (invRev (reduce (invRev w)))
H H₁ H₂ H₃ : ∀ (this : Red w (invRev (reduce (invRev w)))), Red w (invRev (reduce (invRev w)))
⊢ Red w (invRev (reduce (invRev w)))

Tactic:
rwa [invRev_invRev] at this

Premises used: FreeGroup.invRev_invRev
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x : FreeGroup α
mk : ∀ (L : List (α × Bool)), toWord (Quot.mk Red.Step L)⁻¹ = invRev (toWord (Quot.mk Red.Step L))
⊢ x⁻¹.toWord = invRev x.toWord

Tactic:
rcases x with ⟨L⟩
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
mk : (FreeGroup.mk L)⁻¹.toWord = invRev (FreeGroup.mk L).toWord
mk₁ : (FreeGroup.mk (invRev L)).toWord = invRev (FreeGroup.mk L).toWord
mk₂ : reduce (invRev L) = invRev (FreeGroup.mk L).toWord
mk₃ : reduce (invRev L) = invRev (reduce L)
mk₄ mk₅ : invRev (reduce L) = invRev (reduce L)
⊢ toWord (Quot.mk Red.Step L)⁻¹ = invRev (toWord (Quot.mk Red.Step L))

Tactic:
rw [quot_mk_eq_mk, inv_mk, toWord_mk, toWord_mk, reduce_invRev]

Premises used: FreeGroup.toWord_mk, FreeGroup.inv_mk, FreeGroup.reduce_invRev, FreeGroup.quot_mk_eq_mk
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
rw : reduce (reduce L₁ ++ reduce L₂) = (mk (L₁ ++ L₂)).toWord
rw₁ : reduce (reduce L₁ ++ reduce L₂) = (mk L₁ * mk L₂).toWord
rw₂ : reduce (reduce L₁ ++ reduce L₂) = reduce ((mk L₁).toWord ++ (mk L₂).toWord)
rw₃ : reduce (reduce L₁ ++ reduce L₂) = reduce (reduce L₁ ++ (mk L₂).toWord)
rw₄ rw₅ : reduce (reduce L₁ ++ reduce L₂) = reduce (reduce L₁ ++ reduce L₂)
⊢ reduce (reduce L₁ ++ reduce L₂) = reduce (L₁ ++ L₂)

Tactic:
rw [← toWord_mk (L₁ := L₁ ++ L₂), ← mul_mk, toWord_mul, toWord_mk, toWord_mk]

Premises used: FreeGroup.toWord_mk, FreeGroup.mul_mk, FreeGroup.toWord_mul
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
a : α × Bool
⊢ reduce (a :: reduce L) = reduce (a :: L)

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
⊢ reduce (invRev L ++ L) = []

Tactic:
simp [← toWord_mk, ← mul_mk, ← inv_mk]

Premises used: FreeGroup.toWord_mk, FreeGroup.mul_mk, FreeGroup.inv_mk
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
⊢ (x * y).toWord <+ x.toWord ++ y.toWord

Tactic:
Red.sublist ?_

Premises used: FreeGroup.Red.sublist
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
refine : Red (x.toWord ++ y.toWord) (x * y).toWord
⊢ (x * y).toWord <+ x.toWord ++ y.toWord

Tactic:
refine Red.sublist ?_

Premises used: FreeGroup.Red.sublist
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
rw : x * y = mk x.toWord * mk y.toWord
rw₁ : x * y = x * mk y.toWord
rw₂ rw₃ : x * y = x * y
⊢ x * y = mk (x.toWord ++ y.toWord)

Tactic:
rw [← FreeGroup.mul_mk, FreeGroup.mk_toWord, FreeGroup.mk_toWord]

Premises used: FreeGroup.mk_toWord, FreeGroup.mul_mk
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
⊢ x * y = mk (x.toWord ++ y.toWord)

Tactic:
have : x * y = FreeGroup.mk (x.toWord ++ y.toWord) := by
    rw [← FreeGroup.mul_mk, FreeGroup.mk_toWord, FreeGroup.mk_toWord]
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
this : x * y = mk (x.toWord ++ y.toWord)
rw : Red (x.toWord ++ y.toWord) (mk (x.toWord ++ y.toWord)).toWord
⊢ Red (x.toWord ++ y.toWord) (x * y).toWord

Tactic:
rw [this]
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
this : x * y = mk (x.toWord ++ y.toWord)
⊢ Red (x.toWord ++ y.toWord) (mk (x.toWord ++ y.toWord)).toWord

Tactic:
FreeGroup.reduce.red

Premises used: FreeGroup.toWord, FreeGroup.reduce.red
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
this : x * y = mk (x.toWord ++ y.toWord)
⊢ Red (x.toWord ++ y.toWord) (mk (x.toWord ++ y.toWord)).toWord

Tactic:
exact FreeGroup.reduce.red

Premises used: FreeGroup.reduce.red
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
H : L₂ ∈ filter (fun (b : List (α × Bool)) ↦ decide (Red L₁ b)) L₁.sublists
⊢ Red L₁ L₂

Tactic:
of_decide_eq_true (@List.of_mem_filter _ _ L₂ _ H)

Premises used: of_decide_eq_true, List.of_mem_filter
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst : DecidableEq α
H : Red L₁ L₂
⊢ L₂ ∈ enum L₁

Tactic:
List.mem_filter_of_mem (List.mem_sublists.2 <| Red.sublist H) (decide_eq_true H)

Premises used: Iff.mpr, decide_eq_true, List.mem_filter_of_mem, FreeGroup.Red.sublist, FreeGroup.Red.enum, List.mem_sublists
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
rw : Red L (reduce L)
⊢ reduce L = L

Tactic:
rw [← h.red_iff_eq]

Premises used: FreeGroup.IsReduced.red_iff_eq
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
⊢ Red L (reduce L)

Tactic:
reduce.red

Premises used: FreeGroup.reduce.red
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
h : IsReduced L
⊢ Red L (reduce L)

Tactic:
exact reduce.red

Premises used: FreeGroup.reduce.red
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
h : reduce L = L
rw : ∀ ⦃a b : α × Bool⦄ ⦃l₁ l₂ : List (α × Bool)⦄, L = l₁ ++ a :: b :: l₂ → a.1 = b.1 → a.2 = b.2
⊢ IsReduced L

Tactic:
rw [IsReduced, List.isChain_iff_forall_rel_of_append_cons_cons]

Premises used: FreeGroup.IsReduced, List.isChain_iff_forall_rel_of_append_cons_cons
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
h : reduce L = L
x₁ : α
x₂ y₂ : Bool
l₁ l₂ : List (α × Bool)
hl : L = l₁ ++ (x₁, x₂) :: ((x₁, x₂).1, y₂) :: l₂
rw : ((x₁, x₂).1, y₂).2 ≠ !(x₁, x₂).2
⊢ (x₁, x₂).2 = ((x₁, x₂).1, y₂).2

Tactic:
rw [eq_comm, ← Bool.ne_not]

Premises used: eq_comm, Bool.ne_not
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
h : reduce L = L
x₁ : α
x₂ : Bool
l₁ l₂ : List (α × Bool)
hl : L = l₁ ++ (x₁, x₂) :: ((x₁, x₂).1, !(x₁, x₂).2) :: l₂
⊢ False

Tactic:
reduce.not (h.trans hl)

Premises used: FreeGroup.reduce.not, Eq.trans
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L : List (α × Bool)
inst : DecidableEq α
h : reduce L = L
x₁ : α
x₂ : Bool
l₁ l₂ : List (α × Bool)
hl : L = l₁ ++ (x₁, x₂) :: ((x₁, x₂).1, !(x₁, x₂).2) :: l₂
⊢ False

Tactic:
exact reduce.not (h.trans hl)

Premises used: FreeGroup.reduce.not, Eq.trans
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x : FreeGroup α
⊢ IsReduced x.toWord

Tactic:
simp [isReduced_iff_reduce_eq]

Premises used: FreeGroup.isReduced_iff_reduce_eq
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
a : α
this : DecidableEq α := Classical.decEq α
⊢ toWord 1 ≠ (of a).toWord

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
a : α
⊢ of a ≠ 1

Tactic:
one_ne_of _ |>.symm

Premises used: Ne.symm, FreeGroup.one_ne_of
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x : FreeGroup α
⊢ x⁻¹.norm = x.norm

Tactic:
simp only [norm, toWord_inv, invRev_length]

Premises used: FreeGroup.invRev_length, FreeGroup.norm, FreeGroup.toWord_inv
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x : FreeGroup α
⊢ x.norm = 0 ↔ x = 1

Tactic:
simp only [norm, List.length_eq_zero_iff, toWord_eq_nil_iff]

Premises used: FreeGroup.norm, List.length_eq_zero_iff, FreeGroup.toWord_eq_nil_iff
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
⊢ norm.{u_1} (α := α) 1 = 0

Tactic:
rfl

Premises used: FreeGroup.norm, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ (of a).norm = 1

Tactic:
rfl

Premises used: FreeGroup.norm, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
L₁ : List (α × Bool)
inst : DecidableEq α
⊢ (mk L₁).norm ≤ L₁.length

Tactic:
reduce.red.length_le

Premises used: FreeGroup.Red.length_le, FreeGroup.toWord, FreeGroup.norm, FreeGroup.reduce.red
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
x y : FreeGroup α
rw : (x * y).norm = (mk x.toWord * mk y.toWord).norm
rw₁ : (x * y).norm = (x * mk y.toWord).norm
rw₂ rw₃ : (x * y).norm = (x * y).norm
⊢ (x * y).norm = (mk (x.toWord ++ y.toWord)).norm

Tactic:
rw [← mul_mk, mk_toWord, mk_toWord]

Premises used: FreeGroup.mk_toWord, FreeGroup.mul_mk
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
rw : (of a ^ n).toWord.length = n
rw₁ : (List.replicate n (a, true)).length = n
rw₂ rw₃ : n = n
⊢ (of a ^ n).norm = n

Tactic:
rw [norm, toWord_of_pow, List.length_replicate]

Premises used: FreeGroup.norm, FreeGroup.toWord_of_pow, List.length_replicate
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Nonempty α
let : ∀ (a : α), Function.Surjective.{u_1 + 1, 1} (α := FreeGroup α) norm
⊢ Function.Surjective.{u_1 + 1, 1} (α := FreeGroup α) norm

Tactic:
let ⟨a⟩ := ‹Nonempty α›
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Nonempty α
a : α
⊢ Function.Surjective.{u_1 + 1, 1} (α := FreeGroup α) norm

Tactic:
Function.RightInverse.surjective <| norm_of_pow a

Premises used: FreeGroup.norm_of_pow, Function.RightInverse.surjective
-- Module: Mathlib.GroupTheory.FreeGroup.Reduce
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Nonempty α
a : α
⊢ Function.Surjective.{u_1 + 1, 1} (α := FreeGroup α) norm

Tactic:
exact Function.RightInverse.surjective <| norm_of_pow a

Premises used: FreeGroup.norm_of_pow, Function.RightInverse.surjective
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
g : G
⊢ g ∈ I.goursatFst ↔ (g, 1) ∈ I

Tactic:
simp [goursatFst]

Premises used: Subgroup.goursatFst
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
h : H
⊢ h ∈ I.goursatSnd ↔ (1, h) ∈ I

Tactic:
simp [goursatSnd]

Premises used: Subgroup.goursatSnd
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
⊢ I.goursatFst.Normal

Tactic:
.map inferInstance _ hI₁

Premises used: inferInstance, Subgroup.goursatFst, Subgroup.Normal.map
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
⊢ I.goursatSnd.Normal

Tactic:
.map inferInstance _ hI₂

Premises used: inferInstance, Subgroup.Normal.map, Subgroup.goursatSnd
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
x y : G × H
hx : x ∈ I
hy : y ∈ I
⊢ I.goursatFst.Normal

Tactic:
have := normal_goursatFst hI₁