awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
x y : FreeAddGroup α
⊢ (FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
      (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) (x + y) :
        FreeAddGroup ℤ) =
    HAdd.hAdd (α := ℤ) (β := ℤ)
      ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
          (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) x :
            FreeAddGroup ℤ) :
        ℤ)
      ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
          (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) y :
            FreeAddGroup ℤ) :
        ℤ)

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
⊢ IsAddCyclic.{u} (FreeAddGroup α)

Tactic:
⟨FreeAddGroup.of default, fun x =>
  ⟨_root_.FreeAddGroup.addEquivIntOfUnique x, _root_.FreeAddGroup.addEquivIntOfUnique.left_inv x⟩⟩

Premises used: Inhabited.default, IsAddCyclic.mk, FreeAddGroup.addEquivIntOfUnique, FreeAddGroup.of, Exists.intro, AddEquiv.toEquiv, DFunLike.coe, Equiv.left_inv
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α β : Type u
f : α → β
x : α
⊢ Eq (α := FreeGroup β) (f <$> pure x) (pure (f x))

Tactic:
map.of

Premises used: FreeGroup.map.of
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α β : Type u
f : α → β
⊢ Eq (α := FreeGroup β) (f <$> 1) 1

Tactic:
(map f).map_one

Premises used: FreeGroup.map, MonoidHom.map_one
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α β : Type u
f : α → β
x y : FreeGroup α
⊢ f <$> (x * y) = f <$> x * f <$> y

Tactic:
(map f).map_mul x y

Premises used: FreeGroup.map, MonoidHom.map_mul
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α β : Type u
f : α → β
x : FreeGroup α
⊢ f <$> x⁻¹ = (f <$> x)⁻¹

Tactic:
(map f).map_inv x

Premises used: FreeGroup.map, MonoidHom.map_inv
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α β : Type u
f : α → FreeGroup β
x : α
⊢ pure x >>= f = f x

Tactic:
lift_apply_of

Premises used: FreeGroup.lift_apply_of
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α β : Type u
f : α → FreeGroup β
⊢ 1 >>= f = 1

Tactic:
(lift f).map_one

Premises used: FreeGroup.lift, MonoidHom.map_one, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α β : Type u
f : α → FreeGroup β
x y : FreeGroup α
⊢ x * y >>= f = (x >>= f) * (y >>= f)

Tactic:
(lift f).map_mul _ _

Premises used: FreeGroup.lift, DFunLike.coe, MonoidHom.map_mul
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α β : Type u
f : α → FreeGroup β
x : FreeGroup α
⊢ x⁻¹ >>= f = (x >>= f)⁻¹

Tactic:
(lift f).map_inv _

Premises used: FreeGroup.lift, MonoidHom.map_inv, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α_1 : Type u
x_1 : FreeGroup α_1
x : α_1
ih : id <$> of x = of x
rw : (id <$> of x)⁻¹ = (of x)⁻¹
rw₁ rw₂ : (of x)⁻¹ = (of x)⁻¹
⊢ id <$> (of x)⁻¹ = (of x)⁻¹

Tactic:
rw [map_inv, ih]

Premises used: FreeGroup.map_inv
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α_1 : Type u
x_1 x y : FreeGroup α_1
ihx : id <$> x = x
ihy : id <$> y = y
rw : id <$> x * id <$> y = x * y
rw₁ : x * id <$> y = x * y
rw₂ rw₃ : x * y = x * y
⊢ id <$> (x * y) = x * y

Tactic:
rw [map_mul, ihx, ihy]

Premises used: FreeGroup.map_mul
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α_1 β_1 γ : Type u
x : FreeGroup α_1
⊢ ∀ (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g

Tactic:
FreeGroup.induction_on x ?_ ?_ ?_ ?_

Premises used: FreeGroup.induction_on
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α_1 β_1 γ : Type u
x : FreeGroup α_1
refine_1 : ∀ (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), 1 >>= f >>= g = 1 >>= fun (x : α_1) ↦ f x >>= g
refine_2 :
  ∀ (x : α_1) (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), of x >>= f >>= g = of x >>= fun (x : α_1) ↦ f x >>= g
refine_3 :
  ∀ (x : α_1),
    (∀ (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), of x >>= f >>= g = of x >>= fun (x : α_1) ↦ f x >>= g) →
      ∀ (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), (of x)⁻¹ >>= f >>= g = (of x)⁻¹ >>= fun (x : α_1) ↦ f x >>= g
refine_4 :
  ∀ (x y : FreeGroup α_1),
    (∀ (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g) →
      (∀ (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), y >>= f >>= g = y >>= fun (x : α_1) ↦ f x >>= g) →
        ∀ (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), x * y >>= f >>= g = x * y >>= fun (x : α_1) ↦ f x >>= g
⊢ ∀ (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g

Tactic:
refine FreeGroup.induction_on x ?_ ?_ ?_ ?_
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α_1 β_1 γ : Type u
x : FreeGroup α_1
⊢ ∀ (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), 1 >>= f >>= g = 1 >>= fun (x : α_1) ↦ f x >>= g

Tactic:
simp +instances +contextual [instMonad]

Premises used: FreeGroup.instMonad
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α_1 β_1 γ : Type u
x : FreeGroup α_1
⊢ ∀ (x : α_1) (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), of x >>= f >>= g = of x >>= fun (x : α_1) ↦ f x >>= g

Tactic:
simp +instances +contextual [instMonad]

Premises used: FreeGroup.instMonad
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α_1 β_1 γ : Type u
x : FreeGroup α_1
⊢ ∀ (x : α_1),
    (∀ (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), of x >>= f >>= g = of x >>= fun (x : α_1) ↦ f x >>= g) →
      ∀ (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), (of x)⁻¹ >>= f >>= g = (of x)⁻¹ >>= fun (x : α_1) ↦ f x >>= g

Tactic:
simp +instances +contextual [instMonad]

Premises used: FreeGroup.instMonad
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α_1 β_1 γ : Type u
x : FreeGroup α_1
⊢ ∀ (x y : FreeGroup α_1),
    (∀ (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g) →
      (∀ (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), y >>= f >>= g = y >>= fun (x : α_1) ↦ f x >>= g) →
        ∀ (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), x * y >>= f >>= g = x * y >>= fun (x : α_1) ↦ f x >>= g

Tactic:
simp +instances +contextual [instMonad]

Premises used: FreeGroup.instMonad
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α_1 β_1 : Type u
f : α_1 → β_1
x : FreeGroup α_1
⊢ (do
      let y ← x
      pure (f y)) =
    f <$> x

Tactic:
FreeGroup.induction_on x ?_ ?_ ?_ ?_

Premises used: FreeGroup.induction_on
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α_1 β_1 : Type u
f : α_1 → β_1
x : FreeGroup α_1
refine_1 :
  Eq (α := FreeGroup β_1)
    (do
      let y ← 1
      pure (f y))
    (f <$> 1)
refine_2 :
  ∀ (x : α_1),
    (do
        let y ← of x
        pure (f y)) =
      f <$> of x
refine_3 :
  ∀ (x : α_1),
    (do
          let y ← of x
          pure (f y)) =
        f <$> of x →
      (do
          let y ← (of x)⁻¹
          pure (f y)) =
        f <$> (of x)⁻¹
refine_4 :
  ∀ (x y : FreeGroup α_1),
    (do
          let y ← x
          pure (f y)) =
        f <$> x →
      (do
            let y ← y
            pure (f y)) =
          f <$> y →
        (do
            let y ← x * y
            pure (f y)) =
          f <$> (x * y)
⊢ (do
      let y ← x
      pure (f y)) =
    f <$> x

Tactic:
refine FreeGroup.induction_on x ?_ ?_ ?_ ?_
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α_1 β_1 : Type u
f : α_1 → β_1
x : FreeGroup α_1
⊢ Eq (α := FreeGroup β_1)
    (do
      let y ← 1
      pure (f y))
    (f <$> 1)

Tactic:
simp +instances +contextual [instMonad]

Premises used: FreeGroup.instMonad
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α_1 β_1 : Type u
f : α_1 → β_1
x : FreeGroup α_1
⊢ ∀ (x : α_1),
    (do
        let y ← of x
        pure (f y)) =
      f <$> of x

Tactic:
simp +instances +contextual [instMonad]

Premises used: FreeGroup.instMonad
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α_1 β_1 : Type u
f : α_1 → β_1
x : FreeGroup α_1
⊢ ∀ (x : α_1),
    (do
          let y ← of x
          pure (f y)) =
        f <$> of x →
      (do
          let y ← (of x)⁻¹
          pure (f y)) =
        f <$> (of x)⁻¹

Tactic:
simp +instances +contextual [instMonad]

Premises used: FreeGroup.instMonad
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α_1 β_1 : Type u
f : α_1 → β_1
x : FreeGroup α_1
⊢ ∀ (x y : FreeGroup α_1),
    (do
          let y ← x
          pure (f y)) =
        f <$> x →
      (do
            let y ← y
            pure (f y)) =
          f <$> y →
        (do
            let y ← x * y
            pure (f y)) =
          f <$> (x * y)

Tactic:
simp +instances +contextual [instMonad]

Premises used: FreeGroup.instMonad
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
⊢ IsCyclicallyReduced L ↔ IsReduced L ∧ ∀ a ∈ L.getLast?, ∀ b ∈ L.head?, a.1 = b.1 → a.2 = b.2

Tactic:
Iff.rfl

Premises used: Iff.rfl, FreeGroup.IsCyclicallyReduced
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
a b : α × Bool
rw :
  (IsReduced (b :: L ++ [a]) ∧ ∀ a_1 ∈ some a, ∀ b_1 ∈ (b :: L ++ [a]).head?, a_1.1 = b_1.1 → a_1.2 = b_1.2) ↔
    IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)
⊢ IsCyclicallyReduced (b :: L ++ [a]) ↔ IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)

Tactic:
rw [isCyclicallyReduced_iff, List.getLast?_concat]

Premises used: FreeGroup.isCyclicallyReduced_iff, List.getLast?_concat
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
a b : α × Bool
⊢ (IsReduced (b :: L ++ [a]) ∧ ∀ a_1 ∈ some a, ∀ b_1 ∈ (b :: L ++ [a]).head?, a_1.1 = b_1.1 → a_1.2 = b_1.2) ↔
    IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
⊢ IsCyclicallyReduced.{u} (α := α) []

Tactic:
simp [IsCyclicallyReduced]

Premises used: FreeGroup.IsCyclicallyReduced
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
x : α × Bool
⊢ IsCyclicallyReduced [x]

Tactic:
simp [IsCyclicallyReduced]

Premises used: FreeGroup.IsCyclicallyReduced
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
h : IsCyclicallyReduced L
⊢ IsReduced L

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
n : ℕ
x : List (α × Bool)
h : IsCyclicallyReduced x
⊢ IsCyclicallyReduced (replicate 0 x).flatten

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
n_1 n : ℕ
h : IsCyclicallyReduced.{u} (α := α) []
⊢ IsCyclicallyReduced.{u} (α := α) (flatten (replicate (n + 1) []))

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
n_1 n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
⊢ [] ∉ replicate (n + 1) (head :: tail)

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
n_1 n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
rw :
  ((∀ l ∈ replicate (n + 1) (head :: tail), IsChain (fun (a b : α × Bool) ↦ a.1 = b.1 → a.2 = b.2) l) ∧
      IsChain (fun (l₁ l₂ : List (α × Bool)) ↦ ∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, x.1 = y.1 → x.2 = y.2)
        (replicate (n + 1) (head :: tail))) ∧
    ∀ a ∈ (replicate (n + 1) (head :: tail)).flatten.getLast?,
      ∀ b ∈ (replicate (n + 1) (head :: tail)).flatten.head?, a.1 = b.1 → a.2 = b.2
⊢ IsCyclicallyReduced (replicate (n + 1) (head :: tail)).flatten

Tactic:
rw [isCyclicallyReduced_iff, IsReduced, List.isChain_flatten (by simp)]

Premises used: FreeGroup.isCyclicallyReduced_iff, List.isChain_flatten, FreeGroup.IsReduced
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
n_1 n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
⊢ ∀ l ∈ replicate (n + 1) (head :: tail), IsChain (fun (a b : α × Bool) ↦ a.1 = b.1 → a.2 = b.2) l

Tactic:
simpa [IsReduced] using h.isReduced

Premises used: FreeGroup.IsCyclicallyReduced.isReduced, FreeGroup.IsReduced
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
n_1 n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
refine :
  ∀ (x : α × Bool) (ha : x ∈ (replicate (n + 1) (head :: tail)).flatten.getLast?) (x_1 : α × Bool)
    (hb : x_1 ∈ (replicate (n + 1) (head :: tail)).flatten.head?), x.1 = x_1.1 → x.2 = x_1.2
⊢ ((∀ l ∈ replicate (n + 1) (head :: tail), IsChain (fun (a b : α × Bool) ↦ a.1 = b.1 → a.2 = b.2) l) ∧
      IsChain (fun (l₁ l₂ : List (α × Bool)) ↦ ∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, x.1 = y.1 → x.2 = y.2)
        (replicate (n + 1) (head :: tail))) ∧
    ∀ a ∈ (replicate (n + 1) (head :: tail)).flatten.getLast?,
      ∀ b ∈ (replicate (n + 1) (head :: tail)).flatten.head?, a.1 = b.1 → a.2 = b.2

Tactic:
refine ⟨⟨by simpa [IsReduced] using h.isReduced, List.isChain_replicate_of_rel _ h.2⟩,
      fun _ ha _ hb ↦ ?_⟩
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
n_1 n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
x : α × Bool
ha : (replicate (n + 1) (head :: tail)).flatten.getLast? = some x
x_1 : α × Bool
hb : x_1 ∈ (replicate (n + 1) (head :: tail)).flatten.head?
⊢ n + 1 ≠ 0

Tactic:
simp +arith
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
n_1 n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
x : α × Bool
ha : x ∈ (replicate (n + 1) (head :: tail)).flatten.getLast?
x_1 : α × Bool
hb : x_1 ∈ (replicate (n + 1) (head :: tail)).flatten.head?
rw :
  ∀ (ha : (head :: tail).getLast? = some x) (x_2 : α × Bool)
    (hb : x_2 ∈ (replicate (n + 1) (head :: tail)).flatten.head?), x.1 = x_2.1 → x.2 = x_2.2
⊢ x.1 = x_1.1 → x.2 = x_1.2

Tactic:
rw [Option.mem_def, List.getLast?_flatten_replicate (h := by simp +arith)] at ha

Premises used: List.getLast?_flatten_replicate, Option.mem_def
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
n_1 n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
x : α × Bool
ha : (head :: tail).getLast? = some x
x_1 : α × Bool
hb : (replicate (n + 1) (head :: tail)).flatten.head? = some x_1
⊢ n + 1 ≠ 0

Tactic:
simp +arith
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
n_1 n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
x : α × Bool
ha : (head :: tail).getLast? = some x
x_1 : α × Bool
hb : x_1 ∈ (replicate (n + 1) (head :: tail)).flatten.head?
⊢ (head :: tail).head? = some x_1

Tactic:
rw [Option.mem_def, List.head?_flatten_replicate (h := by simp +arith)] at hb

Premises used: List.head?_flatten_replicate, Option.mem_def
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
n_1 n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
x : α × Bool
ha : (head :: tail).getLast? = some x
x_1 : α × Bool
hb : (head :: tail).head? = some x_1
⊢ x.1 = x_1.1 → x.2 = x_1.2

Tactic:
h.2 _ ha _ hb

Premises used: And.right
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
n_1 n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
x : α × Bool
ha : (head :: tail).getLast? = some x
x_1 : α × Bool
hb : (head :: tail).head? = some x_1
⊢ x.1 = x_1.1 → x.2 = x_1.2

Tactic:
exact h.2 _ ha _ hb

Premises used: And.right
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L : List (α × Bool)
h : IsCyclicallyReduced L
n : ℕ
⊢ IsCyclicallyReduced (replicate n L).flatten

Tactic:
match n, L with
  | 0, _ => simp
  | n + 1, [] => simp
  | n + 1, (head :: tail) =>
    rw [isCyclicallyReduced_iff, IsReduced, List.isChain_flatten (by simp)]
    refine ⟨⟨by simpa [IsReduced] using h.isReduced, List.isChain_replicate_of_rel _ h.2⟩,
      fun _ ha _ hb ↦ ?_⟩
    rw [Option.mem_def, List.getLast?_flatten_replicate (h := by simp +arith)] at ha
    rw [Option.mem_def, List.head?_flatten_replicate (h := by simp +arith)] at hb
    exact h.2 _ ha _ hb
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n : ℕ
hn : Ne (α := ℕ) 0 0
⊢ IsReduced (L₁ ++ (replicate 0 L₂).flatten ++ L₃)

Tactic:
contradiction
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n_1 n : ℕ
hn : n + 1 ≠ 0
h : L₂ = []
⊢ IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten ++ L₃)

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n_1 n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
⊢ (replicate (n + 1) L₂).flatten ≠ []

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n_1 n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
⊢ (replicate (n + 1) L₂).flatten ≠ []

Tactic:
have h' : (replicate (n + 1) L₂).flatten ≠ [] := by simp [h]
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n_1 n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten ++ L₃)

Tactic:
IsReduced.append_overlap ?_ ?_ (hn := h')

Premises used: FreeGroup.IsReduced.append_overlap
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n_1 n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
refine_1 : IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten)
refine_2 : IsReduced ((replicate (n + 1) L₂).flatten ++ L₃)
⊢ IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten ++ L₃)

Tactic:
refine IsReduced.append_overlap ?_ ?_ (hn := h')

Premises used: FreeGroup.IsReduced.append_overlap
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n_1 n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
refine_1 : IsReduced (L₁ ++ L₂ ++ (replicate n L₂).flatten)
⊢ IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten)

Tactic:
rw [replicate_succ, flatten_cons, ← append_assoc]

Premises used: List.append_assoc, List.replicate_succ, List.flatten_cons
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n_1 n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ [] ++ (L₁ ++ L₂) ++ L₃ = L₁ ++ L₂ ++ L₃

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n_1 n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
refine_1 : IsReduced (L₂ ++ (replicate n L₂).flatten)
⊢ IsReduced (L₁ ++ L₂ ++ (replicate n L₂).flatten)

Tactic:
refine IsReduced.append_overlap (h₂.infix ⟨[], L₃, by simp⟩) ?_ h

Premises used: FreeGroup.IsReduced.append_overlap, Exists.intro, FreeGroup.IsReduced.infix, List.nil
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n_1 n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced (replicate (n + 1) L₂).flatten

Tactic:
(h₁.flatten_replicate _).isReduced

Premises used: FreeGroup.IsCyclicallyReduced.isReduced, FreeGroup.IsCyclicallyReduced.flatten_replicate
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n_1 n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced (replicate (n + 1) L₂).flatten

Tactic:
exact (h₁.flatten_replicate _).isReduced

Premises used: FreeGroup.IsCyclicallyReduced.isReduced, FreeGroup.IsCyclicallyReduced.flatten_replicate
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n_1 n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
refine_2 : IsReduced ((replicate n L₂).flatten ++ L₂ ++ L₃)
⊢ IsReduced ((replicate (n + 1) L₂).flatten ++ L₃)

Tactic:
rw [replicate_succ', flatten_concat]

Premises used: List.replicate_succ', List.flatten_concat
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n_1 n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ L₁ ++ (L₂ ++ L₃) ++ [] = L₁ ++ L₂ ++ L₃

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n_1 n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
refine_2 : IsReduced ((replicate n L₂).flatten ++ L₂)
⊢ IsReduced ((replicate n L₂).flatten ++ L₂ ++ L₃)

Tactic:
refine IsReduced.append_overlap ?_ (h₂.infix ⟨L₁, [], by simp⟩) h

Premises used: FreeGroup.IsReduced.append_overlap, Exists.intro, FreeGroup.IsReduced.infix, List.nil
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n_1 n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
refine_2 : IsReduced (replicate (n + 1) L₂).flatten
⊢ IsReduced ((replicate n L₂).flatten ++ L₂)

Tactic:
rw [← flatten_concat, ← replicate_succ']

Premises used: List.replicate_succ', List.flatten_concat
-- Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
Goal:
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n_1 n : ℕ
hn : n + 1 ≠ 0
if : ∀ (h : L₂ = []), IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten ++ L₃)
if₁ : ∀ (h : ¬L₂ = []), IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten ++ L₃)
if₂ : ∀ (h : L₂ = []), IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten ++ L₃)
if₃ if₄ : ∀ (h : ¬L₂ = []), IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten ++ L₃)
⊢ IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten ++ L₃)

Tactic:
if h : L₂ = [] then simp_all else
    have h' : (replicate (n + 1) L₂).flatten ≠ [] := by simp [h]
    refine IsReduced.append_overlap ?_ ?_ (hn := h')
    · rw [replicate_succ, flatten_cons, ← append_assoc]
      refine IsReduced.append_overlap (h₂.infix ⟨[], L₃, by simp⟩) ?_ h
      rw [← flatten_cons, ← replicate_succ]
      exact (h₁.flatten_replicate _).isReduced
    · rw [replicate_succ', flatten_concat]
      refine IsReduced.append_overlap ?_ (h₂.infix ⟨L₁, [], by simp⟩) h
      rw [← flatten_concat, ← replicate_succ']
      exact (h₁.flatten_replicate _).isReduced

Premises used: FreeGroup.IsCyclicallyReduced.isReduced, List.replicate_succ', List.append_assoc, List.replicate_succ, FreeGroup.IsCyclicallyReduced.flatten_replicate, List.flatten_cons, List.flatten_concat