awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L_1 L₁ L₂ L₃ L₄ : List (α × Bool)
x : FreeGroup Unit
L : List (Unit × Bool)
x_1 : Unit × Bool
tl : List (Unit × Bool)
ih :
  HPow.hPow (β := ℤ) (of ())
      (List.sum (List.map ((fun (x : ℤ × Bool) ↦ bif x.2 then x.1 else -x.1) ∘ fun (x : Unit × Bool) ↦ (1, x.2)) tl)) =
    mk tl
b : Bool
false :
  HPow.hPow (β := ℤ) (of ())
      (List.sum
        (List.map ((fun (x : ℤ × Bool) ↦ bif x.2 then x.1 else -x.1) ∘ fun (x : Unit × Bool) ↦ (1, x.2))
          ((PUnit.unit, Bool.false) :: tl))) =
    mk ((PUnit.unit, Bool.false) :: tl)
true :
  HPow.hPow (β := ℤ) (of ())
      (List.sum
        (List.map ((fun (x : ℤ × Bool) ↦ bif x.2 then x.1 else -x.1) ∘ fun (x : Unit × Bool) ↦ (1, x.2))
          ((PUnit.unit, Bool.true) :: tl))) =
    mk ((PUnit.unit, Bool.true) :: tl)
⊢ HPow.hPow (β := ℤ) (of ())
      (List.sum
        (List.map ((fun (x : ℤ × Bool) ↦ bif x.2 then x.1 else -x.1) ∘ fun (x : Unit × Bool) ↦ (1, x.2))
          ((PUnit.unit, b) :: tl))) =
    mk ((PUnit.unit, b) :: tl)

Tactic:
cases b
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L_1 L₁ L₂ L₃ L₄ : List (α × Bool)
x : FreeGroup Unit
L : List (Unit × Bool)
x_1 : Unit × Bool
tl : List (Unit × Bool)
ih :
  HPow.hPow (β := ℤ) (of ())
      (List.sum (List.map ((fun (x : ℤ × Bool) ↦ bif x.2 then x.1 else -x.1) ∘ fun (x : Unit × Bool) ↦ (1, x.2)) tl)) =
    mk tl
false : (of ())⁻¹ * mk tl = mk ((PUnit.unit, Bool.false) :: tl)
⊢ HPow.hPow (β := ℤ) (of ())
      (List.sum
        (List.map ((fun (x : ℤ × Bool) ↦ bif x.2 then x.1 else -x.1) ∘ fun (x : Unit × Bool) ↦ (1, x.2))
          ((PUnit.unit, Bool.false) :: tl))) =
    mk ((PUnit.unit, Bool.false) :: tl)

Tactic:
simp [zpow_add, ih]

Premises used: zpow_add
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L_1 L₁ L₂ L₃ L₄ : List (α × Bool)
x : FreeGroup Unit
L : List (Unit × Bool)
x_1 : Unit × Bool
tl : List (Unit × Bool)
ih :
  HPow.hPow (β := ℤ) (of ())
      (List.sum (List.map ((fun (x : ℤ × Bool) ↦ bif x.2 then x.1 else -x.1) ∘ fun (x : Unit × Bool) ↦ (1, x.2)) tl)) =
    mk tl
true : of () * mk tl = mk ((PUnit.unit, Bool.true) :: tl)
⊢ HPow.hPow (β := ℤ) (of ())
      (List.sum
        (List.map ((fun (x : ℤ × Bool) ↦ bif x.2 then x.1 else -x.1) ∘ fun (x : Unit × Bool) ↦ (1, x.2))
          ((PUnit.unit, Bool.true) :: tl))) =
    mk ((PUnit.unit, Bool.true) :: tl)

Tactic:
simp [zpow_add, ih]

Premises used: zpow_add
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L_1 L₁ L₂ L₃ L₄ : List (α × Bool)
x : FreeGroup Unit
L : List (Unit × Bool)
x_1 : Unit × Bool
tl : List (Unit × Bool)
ih :
  HPow.hPow (β := ℤ) (of ())
      (List.sum (List.map ((fun (x : ℤ × Bool) ↦ bif x.2 then x.1 else -x.1) ∘ fun (x : Unit × Bool) ↦ (1, x.2)) tl)) =
    mk tl
⊢ (of ())⁻¹ * mk tl = mk ((PUnit.unit, false) :: tl)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L_1 L₁ L₂ L₃ L₄ : List (α × Bool)
x : FreeGroup Unit
L : List (Unit × Bool)
x_1 : Unit × Bool
tl : List (Unit × Bool)
ih :
  HPow.hPow (β := ℤ) (of ())
      (List.sum (List.map ((fun (x : ℤ × Bool) ↦ bif x.2 then x.1 else -x.1) ∘ fun (x : Unit × Bool) ↦ (1, x.2)) tl)) =
    mk tl
⊢ of () * mk tl = mk ((PUnit.unit, true) :: tl)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L_1 L₁ L₂ L₃ L₄ : List (α × Bool)
x : FreeGroup Unit
L : List (Unit × Bool)
⊢ HPow.hPow (β := ℤ) (of ())
      (List.sum (List.map ((fun (x : ℤ × Bool) ↦ bif x.2 then x.1 else -x.1) ∘ fun (x : Unit × Bool) ↦ (1, x.2)) L)) =
    mk L

Tactic:
exact List.recOn L
     (by rfl)
     (fun ⟨⟨⟩, b⟩ tl ih => by
        cases b <;> simp [zpow_add, ih] <;> rfl)
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : ℤ
⊢ Eq (α := ℤ)
    ((fun (x : FreeGroup Unit) ↦ (sum ((map fun (x : Unit) ↦ 1 : (a : FreeGroup Unit) → FreeGroup ℤ) x) : ℤ))
      ((fun (x : ℤ) ↦ of () ^ x) 0))
    0

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : ℤ
i : ℕ
ih :
  Eq (α := ℤ)
    ((fun (x : FreeGroup Unit) ↦ (sum ((map fun (x : Unit) ↦ 1 : (a : FreeGroup Unit) → FreeGroup ℤ) x) : ℤ))
      ((fun (x : ℤ) ↦ of () ^ x) (↑i : ℤ)))
    (↑i : ℤ)
⊢ (HPow.hPow (α := FreeGroup ℤ) (of 1) i).sum = (↑i : ℤ)

Tactic:
simp only [zpow_natCast, map_pow, map.of] at ih

Premises used: zpow_natCast, map_pow, FreeGroup.map.of
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : ℤ
i : ℕ
ih : (HPow.hPow (α := FreeGroup ℤ) (of 1) i).sum = (↑i : ℤ)
⊢ (fun (x : FreeGroup Unit) ↦ (sum ((map fun (x : Unit) ↦ 1 : (a : FreeGroup Unit) → FreeGroup ℤ) x) : ℤ))
      ((fun (x : ℤ) ↦ of () ^ x) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)) =
    HAdd.hAdd (α := ℤ) (↑i : ℤ) 1

Tactic:
simp [zpow_add, ih]

Premises used: zpow_add
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : ℤ
i : ℕ
ih :
  Eq (α := ℤ)
    ((fun (x : FreeGroup Unit) ↦ (sum ((map fun (x : Unit) ↦ 1 : (a : FreeGroup Unit) → FreeGroup ℤ) x) : ℤ))
      ((fun (x : ℤ) ↦ of () ^ x) (-(↑i : ℤ))))
    (-(↑i : ℤ))
⊢ (HPow.hPow (α := FreeGroup ℤ) (of 1) i).sum = (↑i : ℤ)

Tactic:
simp only [zpow_neg, zpow_natCast, map_inv, map_pow, map.of, sum.map_inv, neg_inj] at ih

Premises used: zpow_natCast, map_inv, map_pow, FreeGroup.map.of, zpow_neg, neg_inj, FreeGroup.sum.map_inv
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : ℤ
i : ℕ
ih : (HPow.hPow (α := FreeGroup ℤ) (of 1) i).sum = (↑i : ℤ)
⊢ (fun (x : FreeGroup Unit) ↦ (sum ((map fun (x : Unit) ↦ 1 : (a : FreeGroup Unit) → FreeGroup ℤ) x) : ℤ))
      ((fun (x : ℤ) ↦ of () ^ x) (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)) =
    HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1

Tactic:
simp [zpow_add, ih, sub_eq_add_neg]

Premises used: zpow_add, sub_eq_add_neg
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
⊢ Eq.{u + 1} (α := FreeGroup α)
    ((fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x)
      ((fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
        1))
    1

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
x : α
⊢ (fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x)
      ((fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
        (of x)) =
    of x

Tactic:
simp [Unique.default_eq x]

Premises used: Unique.default_eq
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
x : α
hx :
  (fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x)
      ((fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
        (of x)) =
    of x
⊢ (fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x)
      ((fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
        (of x)⁻¹) =
    (of x)⁻¹

Tactic:
simp [Unique.default_eq x]

Premises used: Unique.default_eq
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
x y : FreeGroup α
hx :
  (fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x)
      ((fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
        x) =
    x
hy :
  (fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x)
      ((fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
        y) =
    y
⊢ (fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x)
      ((fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
        (x * y)) =
    x * y

Tactic:
simp [zpow_add, hx, hy]

Premises used: zpow_add
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
x : FreeGroup α
C1 :
  Eq.{u + 1} (α := FreeGroup α)
    ((fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (FreeGroup.of default) x)
      ((fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
        1))
    1
of :
  ∀ (x : α),
    (fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (FreeGroup.of default) x)
        ((fun (x : FreeGroup α) ↦
            (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
          (FreeGroup.of x)) =
      FreeGroup.of x
inv_of :
  ∀ (x : α)
    (hx :
      (fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (FreeGroup.of default) x)
          ((fun (x : FreeGroup α) ↦
              (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
            (FreeGroup.of x)) =
        FreeGroup.of x),
    (fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (FreeGroup.of default) x)
        ((fun (x : FreeGroup α) ↦
            (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
          (FreeGroup.of x)⁻¹) =
      (FreeGroup.of x)⁻¹
mul :
  ∀ (x y : FreeGroup α)
    (hx :
      (fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (FreeGroup.of default) x)
          ((fun (x : FreeGroup α) ↦
              (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
            x) =
        x)
    (hy :
      (fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (FreeGroup.of default) x)
          ((fun (x : FreeGroup α) ↦
              (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
            y) =
        y),
    (fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (FreeGroup.of default) x)
        ((fun (x : FreeGroup α) ↦
            (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
          (x * y)) =
      x * y
⊢ (fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (FreeGroup.of default) x)
      ((fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
        x) =
    x

Tactic:
induction x with
    | C1 => simp
    | of x => simp [Unique.default_eq x]
    | inv_of x hx => simp [Unique.default_eq x]
    | mul x y hx hy => simp [zpow_add, hx, hy]

Premises used: FreeGroup.of, zpow_add
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
⊢ Eq (α := ℤ)
    ((fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
      ((fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x) 0))
    0

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
x : ℕ
hx :
  Eq (α := ℤ)
    ((fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
      ((fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x) (↑x : ℤ)))
    (↑x : ℤ)
⊢ (fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
      ((fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x) (HAdd.hAdd (α := ℤ) (↑x : ℤ) 1)) =
    HAdd.hAdd (α := ℤ) (↑x : ℤ) 1

Tactic:
simpa [zpow_add_one] using hx

Premises used: zpow_add_one
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
x : ℕ
hx :
  Eq (α := ℤ)
    ((fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
      ((fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x) (-(↑x : ℤ))))
    (-(↑x : ℤ))
⊢ (fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
      ((fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x) (HSub.hSub (α := ℤ) (-(↑x : ℤ)) 1)) =
    HSub.hSub (α := ℤ) (-(↑x : ℤ)) 1

Tactic:
simpa [zpow_sub_one, ← sub_eq_add_neg] using hx

Premises used: zpow_sub_one, sub_eq_add_neg
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
x : ℤ
zero :
  Eq (α := ℤ)
    ((fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
      ((fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x) 0))
    0
succ :
  ∀ (x : ℕ)
    (hx :
      Eq (α := ℤ)
        ((fun (x : FreeGroup α) ↦
            (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
          ((fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x) (↑x : ℤ)))
        (↑x : ℤ)),
    (fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
        ((fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x) (HAdd.hAdd (α := ℤ) (↑x : ℤ) 1)) =
      HAdd.hAdd (α := ℤ) (↑x : ℤ) 1
pred :
  ∀ (x : ℕ)
    (hx :
      Eq (α := ℤ)
        ((fun (x : FreeGroup α) ↦
            (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
          ((fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x) (-(↑x : ℤ))))
        (-(↑x : ℤ))),
    (fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
        ((fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x) (HSub.hSub (α := ℤ) (-(↑x : ℤ)) 1)) =
      HSub.hSub (α := ℤ) (-(↑x : ℤ)) 1
⊢ (fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
      ((fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x) x) =
    x

Tactic:
induction x with
    | zero => simp
    | succ x hx => simpa [zpow_add_one] using hx
    | pred x hx => simpa [zpow_sub_one, ← sub_eq_add_neg] using hx

Premises used: zpow_sub_one, sub_eq_add_neg, zpow_add_one
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
x : FreeGroup α
⊢ Function.comp (α := Multiplicative ℤ) (β := ℤ) (⇑(Equiv.symm equivIntOfUnique) : (a : ℤ) → FreeGroup α)
      (⇑Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ)
      (Function.comp (β := ℤ) (⇑Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ)
        (⇑equivIntOfUnique : (a : FreeGroup α) → ℤ) x) =
    x

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
x : Multiplicative ℤ
⊢ Function.comp.{u + 1, 1, 1} (α := FreeGroup α) (β := ℤ) (⇑Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ)
      (⇑equivIntOfUnique : (a : FreeGroup α) → ℤ)
      (Function.comp (β := ℤ) (⇑(Equiv.symm equivIntOfUnique) : (a : ℤ) → FreeGroup α)
        (⇑Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) x) =
    x

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
x x_1 : FreeGroup α
⊢ Function.comp (β := ℤ) (⇑Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ)
      (⇑equivIntOfUnique : (a : FreeGroup α) → ℤ) (x * x_1) =
    HMul.hMul (α := Multiplicative ℤ)
      (Function.comp (β := ℤ) (⇑Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ)
        (⇑equivIntOfUnique : (a : FreeGroup α) → ℤ) x)
      (Function.comp (β := ℤ) (⇑Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ)
        (⇑equivIntOfUnique : (a : FreeGroup α) → ℤ) x_1)

Tactic:
simp [equivIntOfUnique]

Premises used: FreeGroup.equivIntOfUnique
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
⊢ IsCyclic.{u} (FreeGroup α)

Tactic:
⟨of default, fun x => ⟨equivIntOfUnique x, equivIntOfUnique.left_inv x⟩⟩

Premises used: FreeGroup.of, Inhabited.default, FreeGroup.equivIntOfUnique, Exists.intro, IsCyclic.mk, DFunLike.coe, Equiv.left_inv
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
⊢ Eq.{u + 1} (α := FreeAddGroup α)
    ((fun (x : ℤ) ↦ HSMul.hSMul (β := FreeAddGroup α) x (FreeAddGroup.of default))
      ((fun (x : FreeAddGroup α) ↦
          ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
              (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) x :
                FreeAddGroup ℤ) :
            ℤ))
        0))
    0

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
x : α
⊢ (fun (x : ℤ) ↦ HSMul.hSMul (β := FreeAddGroup α) x (FreeAddGroup.of default))
      ((fun (x : FreeAddGroup α) ↦
          ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
              (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) x :
                FreeAddGroup ℤ) :
            ℤ))
        (FreeAddGroup.of x)) =
    FreeAddGroup.of x

Tactic:
simp [Unique.default_eq x]

Premises used: Unique.default_eq
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
x : α
hx :
  (fun (x : ℤ) ↦ HSMul.hSMul (β := FreeAddGroup α) x (FreeAddGroup.of default))
      ((fun (x : FreeAddGroup α) ↦
          ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
              (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) x :
                FreeAddGroup ℤ) :
            ℤ))
        (FreeAddGroup.of x)) =
    FreeAddGroup.of x
⊢ (fun (x : ℤ) ↦ HSMul.hSMul (β := FreeAddGroup α) x (FreeAddGroup.of default))
      ((fun (x : FreeAddGroup α) ↦
          ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
              (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) x :
                FreeAddGroup ℤ) :
            ℤ))
        (-FreeAddGroup.of x)) =
    -FreeAddGroup.of x

Tactic:
simp [Unique.default_eq x]

Premises used: Unique.default_eq
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
x y : FreeAddGroup α
hx :
  (fun (x : ℤ) ↦ HSMul.hSMul (β := FreeAddGroup α) x (FreeAddGroup.of default))
      ((fun (x : FreeAddGroup α) ↦
          ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
              (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) x :
                FreeAddGroup ℤ) :
            ℤ))
        x) =
    x
hy :
  (fun (x : ℤ) ↦ HSMul.hSMul (β := FreeAddGroup α) x (FreeAddGroup.of default))
      ((fun (x : FreeAddGroup α) ↦
          ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
              (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) x :
                FreeAddGroup ℤ) :
            ℤ))
        y) =
    y
⊢ (fun (x : ℤ) ↦ HSMul.hSMul (β := FreeAddGroup α) x (FreeAddGroup.of default))
      ((fun (x : FreeAddGroup α) ↦
          ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
              (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) x :
                FreeAddGroup ℤ) :
            ℤ))
        (x + y)) =
    x + y

Tactic:
simp [add_zsmul, hx, hy]

Premises used: add_zsmul
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
x : ℤ
zero :
  Eq (α := ℤ)
    ((fun (x : FreeAddGroup α) ↦
        ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
            (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) x :
              FreeAddGroup ℤ) :
          ℤ))
      ((fun (x : ℤ) ↦ HSMul.hSMul (β := FreeAddGroup α) x (FreeAddGroup.of default)) 0))
    0
succ :
  ∀ (i : ℕ),
    Eq (α := ℤ)
        ((fun (x : FreeAddGroup α) ↦
            ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
                (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) x :
                  FreeAddGroup ℤ) :
              ℤ))
          ((fun (x : ℤ) ↦ HSMul.hSMul (β := FreeAddGroup α) x (FreeAddGroup.of default)) (↑i : ℤ)))
        (↑i : ℤ) →
      (fun (x : FreeAddGroup α) ↦
            ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
                (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) x :
                  FreeAddGroup ℤ) :
              ℤ))
          ((fun (x : ℤ) ↦ HSMul.hSMul (β := FreeAddGroup α) x (FreeAddGroup.of default))
            (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)) =
        HAdd.hAdd (α := ℤ) (↑i : ℤ) 1
pred :
  ∀ (i : ℕ),
    Eq (α := ℤ)
        ((fun (x : FreeAddGroup α) ↦
            ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
                (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) x :
                  FreeAddGroup ℤ) :
              ℤ))
          ((fun (x : ℤ) ↦ HSMul.hSMul (β := FreeAddGroup α) x (FreeAddGroup.of default)) (-(↑i : ℤ))))
        (-(↑i : ℤ)) →
      (fun (x : FreeAddGroup α) ↦
            ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
                (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) x :
                  FreeAddGroup ℤ) :
              ℤ))
          ((fun (x : ℤ) ↦ HSMul.hSMul (β := FreeAddGroup α) x (FreeAddGroup.of default))
            (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)) =
        HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1
⊢ (fun (x : FreeAddGroup α) ↦
        ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
            (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) x :
              FreeAddGroup ℤ) :
          ℤ))
      ((fun (x : ℤ) ↦ HSMul.hSMul (β := FreeAddGroup α) x (FreeAddGroup.of default)) x) =
    x

Tactic:
induction x
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
⊢ Eq (α := ℤ)
    ((fun (x : FreeAddGroup α) ↦
        ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
            (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) x :
              FreeAddGroup ℤ) :
          ℤ))
      ((fun (x : ℤ) ↦ HSMul.hSMul (β := FreeAddGroup α) x (FreeAddGroup.of default)) 0))
    0

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
i : ℕ
h :
  Eq (α := ℤ)
    ((fun (x : FreeAddGroup α) ↦
        ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
            (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) x :
              FreeAddGroup ℤ) :
          ℤ))
      ((fun (x : ℤ) ↦ HSMul.hSMul (β := FreeAddGroup α) x (FreeAddGroup.of default)) (↑i : ℤ)))
    (↑i : ℤ)
⊢ (fun (x : FreeAddGroup α) ↦
        ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
            (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) x :
              FreeAddGroup ℤ) :
          ℤ))
      ((fun (x : ℤ) ↦ HSMul.hSMul (β := FreeAddGroup α) x (FreeAddGroup.of default)) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)) =
    HAdd.hAdd (α := ℤ) (↑i : ℤ) 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
i : ℕ
h :
  Eq (α := ℤ)
    ((fun (x : FreeAddGroup α) ↦
        ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
            (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) x :
              FreeAddGroup ℤ) :
          ℤ))
      ((fun (x : ℤ) ↦ HSMul.hSMul (β := FreeAddGroup α) x (FreeAddGroup.of default)) (-(↑i : ℤ))))
    (-(↑i : ℤ))
⊢ (fun (x : FreeAddGroup α) ↦
        ((FreeAddGroup.sum : (a : FreeAddGroup ℤ) → ℤ)
            (((FreeAddGroup.map 1 : FreeAddGroup α →+ FreeAddGroup ℤ) : (a : FreeAddGroup α) → FreeAddGroup ℤ) x :
              FreeAddGroup ℤ) :
          ℤ))
      ((fun (x : ℤ) ↦ HSMul.hSMul (β := FreeAddGroup α) x (FreeAddGroup.of default))
        (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)) =
    HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1

Tactic:
simp