awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
β : Type v
f : List (α × Bool) → β
H : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → f L₁ = f L₂
⊢ Quot.lift (r := Red.Step) f H (mk L) = f L

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
β : Type v
f : List (α × Bool) → β
H : ∀ (L₁ L₂ : List (α × Bool)), Red.Step L₁ L₂ → f L₁ = f L₂
⊢ Quot.liftOn (r := Red.Step) (mk L) f H = f L

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
β : Type v
f : List (α × Bool) → List (β × Bool)
H : (Red.Step ⇒ Red.Step) f f
⊢ Quot.map (ra := Red.Step) (rb := Red.Step) f H (mk L) = mk (f L)

Tactic:
rfl

Premises used: FreeGroup.mk, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := FreeGroup α) 1 (mk [])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
⊢ mk L₁ * mk L₂ = mk (L₁ ++ L₂)

Tactic:
rfl

Premises used: FreeGroup.mk, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ : List (α × Bool)
⊢ (invRev L₁).length = L₁.length

Tactic:
simp [invRev]

Premises used: FreeGroup.invRev
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ : List (α × Bool)
⊢ invRev (invRev L₁) = L₁

Tactic:
simp [invRev, List.map_reverse, Function.comp_def]

Premises used: Function.comp_def, FreeGroup.invRev, List.map_reverse
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := List (α × Bool)) (invRev []) []

Tactic:
rfl

Premises used: List.reverseAux, FreeGroup.invRev, List.reverse, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
⊢ invRev (L₁ ++ L₂) = invRev L₂ ++ invRev L₁

Tactic:
simp [invRev]

Premises used: FreeGroup.invRev
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
a : α × Bool
⊢ invRev (a :: L) = invRev L ++ invRev [a]

Tactic:
simp [invRev]

Premises used: FreeGroup.invRev
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
⊢ Function.Involutive.{u + 1} (α := List (α × Bool)) invRev

Tactic:
fun _ => invRev_invRev

Premises used: FreeGroup.invRev_invRev, Function.Involutive
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
⊢ Function.Injective.{u + 1, u + 1} (α := List (α × Bool)) invRev

Tactic:
invRev_involutive.injective

Premises used: FreeGroup.invRev_involutive, Function.Involutive.injective
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
⊢ Function.Surjective.{u + 1, u + 1} (α := List (α × Bool)) invRev

Tactic:
invRev_involutive.surjective

Premises used: FreeGroup.invRev_involutive, Function.Involutive.surjective
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
⊢ Function.Bijective.{u + 1, u + 1} (α := List (α × Bool)) invRev

Tactic:
invRev_involutive.bijective

Premises used: FreeGroup.invRev_involutive, Function.Involutive.bijective
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ a b : List (α × Bool)
h : Red.Step a b
not :
  ∀ {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool}, Red.Step (invRev (L₁ ++ (x, b) :: (x, !b) :: L₂)) (invRev (L₁ ++ L₂))
⊢ Red.Step (invRev a) (invRev b)

Tactic:
cases h
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ L₁_1 L₂_1 : List (α × Bool)
x : α
b : Bool
⊢ Red.Step (invRev (L₁_1 ++ (x, b) :: (x, !b) :: L₂_1)) (invRev (L₁_1 ++ L₂_1))

Tactic:
simp [invRev]

Premises used: FreeGroup.invRev
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
⊢ (mk L)⁻¹ = mk (invRev L)

Tactic:
rfl

Premises used: FreeGroup.mk, Quot.map, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
h : Step L₁ L₂
obtain :
  ∀ {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool},
    Step (FreeGroup.invRev (L₁ ++ (x, b) :: (x, !b) :: L₂)) (FreeGroup.invRev (L₁ ++ L₂))
⊢ Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)

Tactic:
obtain ⟨a, b, x, y⟩ := h
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
x : α
b : Bool
⊢ Step (FreeGroup.invRev (L₁ ++ (x, b) :: (x, !b) :: L₂)) (FreeGroup.invRev (L₁ ++ L₂))

Tactic:
simp [FreeGroup.invRev]

Premises used: FreeGroup.invRev
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
h : Red L₁ L₂
⊢ Red (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)

Tactic:
Relation.ReflTransGen.lift _ (fun _a _b => Red.Step.invRev) h

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

Tactic:
simpa only [invRev_invRev] using h.invRev

Premises used: FreeGroup.invRev_invRev, FreeGroup.Red.Step.invRev
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
h : Red (invRev L₁) (invRev L₂)
⊢ Red L₁ L₂

Tactic:
simpa only [invRev_invRev] using h.invRev

Premises used: FreeGroup.invRev_invRev, FreeGroup.Red.invRev
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁_1 L₂_1 L₃_1 L₄ : List (α × Bool)
a : FreeGroup α
L₁ : List (α × Bool)
b : FreeGroup α
L₂ : List (α × Bool)
c : FreeGroup α
L₃ : List (α × Bool)
⊢ HMul.hMul (α := FreeGroup α) (Quot.mk Red.Step L₁) (Quot.mk Red.Step L₂) * Quot.mk Red.Step L₃ =
    Quot.mk Red.Step L₁ * HMul.hMul (α := FreeGroup α) (Quot.mk Red.Step L₂) (Quot.mk Red.Step L₃)

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L_1 L₁ L₂ L₃ L₄ : List (α × Bool)
a : FreeGroup α
L : List (α × Bool)
⊢ HMul.hMul (α := FreeGroup α) 1 (Quot.mk Red.Step L) = Quot.mk Red.Step L

Tactic:
rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L_1 L₁ L₂ L₃ L₄ : List (α × Bool)
a : FreeGroup α
L : List (α × Bool)
⊢ HMul.hMul (α := FreeGroup α) (Quot.mk Red.Step L) 1 = Quot.mk Red.Step L

Tactic:
simp [one_eq_mk]

Premises used: FreeGroup.one_eq_mk
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L_1 L₁ L₂ L₃ L₄ : List (α × Bool)
a : FreeGroup α
L : List (α × Bool)
x_1 : α × Bool
tl : List (α × Bool)
ih : HMul.hMul (α := FreeGroup α) (Quot.mk Red.Step tl)⁻¹ (Quot.mk Red.Step tl) = 1
x : α
b : Bool
⊢ Red.Step (invRev ((x, b) :: tl) ++ (x, b) :: tl) (invRev tl ++ tl)

Tactic:
simp [invRev]

Premises used: FreeGroup.invRev
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L_1 L₁ L₂ L₃ L₄ : List (α × Bool)
a : FreeGroup α
L : List (α × Bool)
⊢ HMul.hMul (α := FreeGroup α) (Quot.mk Red.Step L)⁻¹ (Quot.mk Red.Step L) = 1

Tactic:
exact
      List.recOn L rfl fun ⟨x, b⟩ tl ih =>
          Eq.trans (Quot.sound <| by simp [invRev]) ih
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
n_1 n : ℕ
rw : mk L * mk L ^ n = mk (List.replicate (n + 1) L).flatten
rw₁ : mk L * mk (List.replicate n L).flatten = mk (List.replicate (n + 1) L).flatten
rw₂ : mk (L ++ (List.replicate n L).flatten) = mk (List.replicate (n + 1) L).flatten
rw₃ : mk (L ++ (List.replicate n L).flatten) = mk (L :: List.replicate n L).flatten
rw₄ rw₅ : mk (L ++ (List.replicate n L).flatten) = mk (L ++ (List.replicate n L).flatten)
⊢ mk L ^ (n + 1) = mk (List.replicate (n + 1) L).flatten

Tactic:
rw [pow_succ', pow_mk, mul_mk, List.replicate_succ, List.flatten_cons]

Premises used: List.replicate_succ, FreeGroup.mul_mk, List.flatten_cons, pow_succ'
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
C : FreeGroup α → Prop
z : FreeGroup α
C1 : C 1
of : ∀ (x : α), C (FreeGroup.of x)
inv_of : ∀ (x : α), C (FreeGroup.of x) → C (FreeGroup.of x)⁻¹
mul : ∀ (x y : FreeGroup α), C x → C y → C (x * y)
⊢ C z

Tactic:
Quot.inductionOn z fun L ↦ L.recOn C1 fun ⟨x, b⟩ _tl ih ↦
    b.recOn (mul _ _ (inv_of _ <| of x) ih) (mul _ _ (of x) ih)

Premises used: Quot.inductionOn
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
M : Type u_1
inst : Monoid M
f g : MonoidHom.{u, u_1} (FreeGroup α) M
h : ∀ (a : α), Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of a) : M) ((g : (a : FreeGroup α) → M) (of a) : M)
h₁ : ∀ (x : FreeGroup α), Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) x : M) ((g : (a : FreeGroup α) → M) x : M)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
M : Type u_1
inst : Monoid M
f g : MonoidHom.{u, u_1} (FreeGroup α) M
h : ∀ (a : α), Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of a) : M) ((g : (a : FreeGroup α) → M) (of a) : M)
x_1 : FreeGroup α
x : α
trans :
  (f : (a : FreeGroup α) → M) (of x)⁻¹ =
    HMul.hMul (β := M)
      (HMul.hMul (α := M) (β := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M) ((f : (a : FreeGroup α) → M) (of x) : M))
      ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M)
trans₁ :
  HMul.hMul (β := M)
      (HMul.hMul (α := M) (β := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M) ((f : (a : FreeGroup α) → M) (of x) : M))
      ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M) =
    (g : (a : FreeGroup α) → M) (of x)⁻¹
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M) ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M)

Tactic:
trans f (of x)⁻¹ * f (of x) * g (of x)⁻¹

Premises used: FreeGroup.of, Inv.inv, DFunLike.coe
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
M : Type u_1
inst : Monoid M
f g : MonoidHom.{u, u_1} (FreeGroup α) M
h : ∀ (a : α), Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of a) : M) ((g : (a : FreeGroup α) → M) (of a) : M)
x_1 : FreeGroup α
x : α
simp_rw :
  (f : (a : FreeGroup α) → M) (of x)⁻¹ =
    HMul.hMul (α := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M)
      (HMul.hMul (α := M) (β := M) ((f : (a : FreeGroup α) → M) (of x) : M) ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M))
simp_rw₁ :
  (f : (a : FreeGroup α) → M) (of x)⁻¹ =
    HMul.hMul (α := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M)
      (HMul.hMul (α := M) (β := M) ((g : (a : FreeGroup α) → M) (of x) : M) ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M))
simp_rw₂ :
  (f : (a : FreeGroup α) → M) (of x)⁻¹ =
    HMul.hMul (α := M) (β := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M)
      ((g : (a : FreeGroup α) → M) (of x * (of x)⁻¹) : M)
simp_rw₃ :
  (f : (a : FreeGroup α) → M) (of x)⁻¹ =
    HMul.hMul (α := M) (β := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M) ((g : (a : FreeGroup α) → M) 1 : M)
simp_rw₄ :
  (f : (a : FreeGroup α) → M) (of x)⁻¹ = HMul.hMul (α := M) (β := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M) (1 : M)
⊢ (f : (a : FreeGroup α) → M) (of x)⁻¹ =
    HMul.hMul (β := M)
      (HMul.hMul (α := M) (β := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M) ((f : (a : FreeGroup α) → M) (of x) : M))
      ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M)

Tactic:
simp_rw [mul_assoc, h, ← _root_.map_mul, mul_inv_cancel, _root_.map_one, mul_one]

Premises used: mul_assoc, map_mul, map_one, mul_inv_cancel, mul_one
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
M : Type u_1
inst : Monoid M
f g : MonoidHom.{u, u_1} (FreeGroup α) M
h : ∀ (a : α), Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of a) : M) ((g : (a : FreeGroup α) → M) (of a) : M)
x_1 : FreeGroup α
x : α
simp_rw :
  HMul.hMul (α := M) (β := M) ((f : (a : FreeGroup α) → M) ((of x)⁻¹ * of x) : M)
      ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M) =
    (g : (a : FreeGroup α) → M) (of x)⁻¹
simp_rw₁ :
  HMul.hMul (α := M) (β := M) ((f : (a : FreeGroup α) → M) 1 : M) ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M) =
    (g : (a : FreeGroup α) → M) (of x)⁻¹
simp_rw₂ :
  HMul.hMul (α := M) (β := M) (1 : M) ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M) = (g : (a : FreeGroup α) → M) (of x)⁻¹
⊢ HMul.hMul (β := M)
      (HMul.hMul (α := M) (β := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M) ((f : (a : FreeGroup α) → M) (of x) : M))
      ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M) =
    (g : (a : FreeGroup α) → M) (of x)⁻¹

Tactic:
simp_rw [← _root_.map_mul, inv_mul_cancel, _root_.map_one, one_mul]

Premises used: inv_mul_cancel, map_mul, map_one, one_mul
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
M : Type u_1
inst : Monoid M
f g : MonoidHom.{u, u_1} (FreeGroup α) M
h : ∀ (a : α), Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of a) : M) ((g : (a : FreeGroup α) → M) (of a) : M)
x : FreeGroup α
⊢ ∀ (x : α), Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M) ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M)

Tactic:
have this (x) : f (of x)⁻¹ = g (of x)⁻¹ := by
    trans f (of x)⁻¹ * f (of x) * g (of x)⁻¹
    · simp_rw [mul_assoc, h, ← _root_.map_mul, mul_inv_cancel, _root_.map_one, mul_one]
    · simp_rw [← _root_.map_mul, inv_mul_cancel, _root_.map_one, one_mul]
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
M : Type u_1
inst : Monoid M
f g : MonoidHom.{u, u_1} (FreeGroup α) M
h : ∀ (a : α), Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of a) : M) ((g : (a : FreeGroup α) → M) (of a) : M)
x : FreeGroup α
this :
  ∀ (x : α), Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M) ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M)
h₁ : Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) 1 : M) ((g : (a : FreeGroup α) → M) 1 : M)
h₂ : ∀ (x : α), Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of x) : M) ((g : (a : FreeGroup α) → M) (of x) : M)
h₃ :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of x) : M) ((g : (a : FreeGroup α) → M) (of x) : M) →
      Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M) ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M)
h₄ :
  ∀ (x y : FreeGroup α),
    Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) x : M) ((g : (a : FreeGroup α) → M) x : M) →
      Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) y : M) ((g : (a : FreeGroup α) → M) y : M) →
        Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (x * y) : M) ((g : (a : FreeGroup α) → M) (x * y) : M)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) x : M) ((g : (a : FreeGroup α) → M) x : M)

Tactic:
induction x
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
M : Type u_1
inst : Monoid M
f g : MonoidHom.{u, u_1} (FreeGroup α) M
h : ∀ (a : α), Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of a) : M) ((g : (a : FreeGroup α) → M) (of a) : M)
this :
  ∀ (x : α), Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M) ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) 1 : M) ((g : (a : FreeGroup α) → M) 1 : M)

Tactic:
simp [*]
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
M : Type u_1
inst : Monoid M
f g : MonoidHom.{u, u_1} (FreeGroup α) M
h : ∀ (a : α), Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of a) : M) ((g : (a : FreeGroup α) → M) (of a) : M)
this :
  ∀ (x : α), Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M) ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M)
x : α
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of x) : M) ((g : (a : FreeGroup α) → M) (of x) : M)

Tactic:
simp [*]
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
M : Type u_1
inst : Monoid M
f g : MonoidHom.{u, u_1} (FreeGroup α) M
h : ∀ (a : α), Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of a) : M) ((g : (a : FreeGroup α) → M) (of a) : M)
this :
  ∀ (x : α), Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M) ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M)
x : α
h_1 : Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of x) : M) ((g : (a : FreeGroup α) → M) (of x) : M)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M) ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M)

Tactic:
simp [*]
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
M : Type u_1
inst : Monoid M
f g : MonoidHom.{u, u_1} (FreeGroup α) M
h : ∀ (a : α), Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of a) : M) ((g : (a : FreeGroup α) → M) (of a) : M)
this :
  ∀ (x : α), Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M) ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M)
x y : FreeGroup α
h_1 : Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) x : M) ((g : (a : FreeGroup α) → M) x : M)
h_2 : Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) y : M) ((g : (a : FreeGroup α) → M) y : M)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (x * y) : M) ((g : (a : FreeGroup α) → M) (x * y) : M)

Tactic:
simp [*]
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
⊢ mk L₁ = mk L₂ ↔ Join Red L₁ L₂

Tactic:
calc
    mk L₁ = mk L₂ ↔ EqvGen Red.Step L₁ L₂ := Iff.intro Quot.eqvGen_exact Quot.eqvGen_sound
    _ ↔ Join Red L₁ L₂ := eqvGen_step_iff_join_red

Premises used: Quot.eqvGen_sound, Trans.trans, Iff.intro, FreeGroup.eqvGen_step_iff_join_red, Quot.eqvGen_exact
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x x_1 : α
H : of x = of x_1
let : ∀ (L₁ : List (α × Bool)) (hx : Red [(x, true)] L₁) (hy : Red [(x_1, true)] L₁), x = x_1
⊢ x = x_1

Tactic:
let ⟨L₁, hx, hy⟩ := Red.exact.1 H
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x x_1 : α
H : of x = of x_1
L₁ : List (α × Bool)
hx : Red [(x, true)] L₁
hy : Red [(x_1, true)] L₁
⊢ L₁ = [(x, true)]

Tactic:
simp [Red.singleton_iff] at hx hy

Premises used: FreeGroup.Red.singleton_iff
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x x_1 : α
H : of x = of x_1
L₁ : List (α × Bool)
hx : Red [(x, true)] L₁
hy : Red [(x_1, true)] L₁
hx₁ : L₁ = [(x, true)]
⊢ L₁ = [(x_1, true)]

Tactic:
simp [Red.singleton_iff] at hx hy

Premises used: FreeGroup.Red.singleton_iff
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x x_1 : α
H : of x = of x_1
L₁ : List (α × Bool)
hx : L₁ = [(x, true)]
hy : L₁ = [(x_1, true)]
⊢ x = x_1

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
β : Type v
inst : Group β
f : α → β
H : Step L₁ L₂
obtain :
  ∀ {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool}, Lift.aux f (L₁ ++ (x, b) :: (x, !b) :: L₂) = Lift.aux f (L₁ ++ L₂)
⊢ Lift.aux f L₁ = Lift.aux f L₂

Tactic:
obtain @⟨_, _, _, b⟩ := H
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
inst : Group β
f : α → β
L₁ L₂ : List (α × Bool)
x : α
b : Bool
false : Lift.aux f (L₁ ++ (x, Bool.false) :: (x, !Bool.false) :: L₂) = Lift.aux f (L₁ ++ L₂)
true : Lift.aux f (L₁ ++ (x, Bool.true) :: (x, !Bool.true) :: L₂) = Lift.aux f (L₁ ++ L₂)
⊢ Lift.aux f (L₁ ++ (x, b) :: (x, !b) :: L₂) = Lift.aux f (L₁ ++ L₂)

Tactic:
cases b
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
inst : Group β
f : α → β
L₁ L₂ : List (α × Bool)
x : α
⊢ Lift.aux f (L₁ ++ (x, false) :: (x, !false) :: L₂) = Lift.aux f (L₁ ++ L₂)

Tactic:
simp [Lift.aux, List.prod_append]

Premises used: List.prod_append, FreeGroup.Lift.aux
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
inst : Group β
f : α → β
L₁ L₂ : List (α × Bool)
x : α
⊢ Lift.aux f (L₁ ++ (x, true) :: (x, !true) :: L₂) = Lift.aux f (L₁ ++ L₂)

Tactic:
simp [Lift.aux, List.prod_append]

Premises used: List.prod_append, FreeGroup.Lift.aux
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁_1 L₂_1 L₃ L₄ : List (α × Bool)
β : Type v
inst : Group β
f_1 : α → β
x y : FreeGroup α
f : α → β
a : FreeGroup α
L₁ : List (α × Bool)
b : FreeGroup α
L₂ : List (α × Bool)
⊢ Quot.lift (r := Red.Step) (Lift.aux f) ⋯ (HMul.hMul (α := FreeGroup α) (Quot.mk Red.Step L₁) (Quot.mk Red.Step L₂)) =
    Quot.lift (r := Red.Step) (Lift.aux f) ⋯ (Quot.mk Red.Step L₁) *
      Quot.lift (r := Red.Step) (Lift.aux f) ⋯ (Quot.mk Red.Step L₂)

Tactic:
simp [Lift.aux, List.prod_append]

Premises used: List.prod_append, FreeGroup.Lift.aux
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst : Group β
f_1 : α → β
x y : FreeGroup α
f : α → β
h :
  ∀ (x : α),
    (fun (g : MonoidHom.{u, v} (FreeGroup α) β) ↦ ((⇑g : (a : FreeGroup α) → β) ∘ of : α → β))
        ((fun (f : α → β) ↦
            (MonoidHom.mk' (Quot.lift (r := Red.Step) (Lift.aux f) ⋯) ⋯ : MonoidHom.{u, v} (FreeGroup α) β))
          f)
        x =
      f x
⊢ (fun (g : MonoidHom.{u, v} (FreeGroup α) β) ↦ ((⇑g : (a : FreeGroup α) → β) ∘ of : α → β))
      ((fun (f : α → β) ↦
          (MonoidHom.mk' (Quot.lift (r := Red.Step) (Lift.aux f) ⋯) ⋯ : MonoidHom.{u, v} (FreeGroup α) β))
        f) =
    f

Tactic:
ext
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst : Group β
f_1 : α → β
x y : FreeGroup α
f : α → β
x_1 : α
⊢ (fun (g : MonoidHom.{u, v} (FreeGroup α) β) ↦ ((⇑g : (a : FreeGroup α) → β) ∘ of : α → β))
      ((fun (f : α → β) ↦
          (MonoidHom.mk' (Quot.lift (r := Red.Step) (Lift.aux f) ⋯) ⋯ : MonoidHom.{u, v} (FreeGroup α) β))
        f)
      x_1 =
    f x_1

Tactic:
simp [of, Lift.aux]

Premises used: FreeGroup.of, FreeGroup.Lift.aux
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst : Group β
f : α → β
x y : FreeGroup α
g : MonoidHom.{u, v} (FreeGroup α) β
h :
  ∀ (a : α),
    Eq.{v + 1} (α := β)
      (((fun (f : α → β) ↦
                (MonoidHom.mk' (Quot.lift (r := Red.Step) (Lift.aux f) ⋯) ⋯ : MonoidHom.{u, v} (FreeGroup α) β))
              ((fun (g : MonoidHom.{u, v} (FreeGroup α) β) ↦ ((⇑g : (a : FreeGroup α) → β) ∘ of : α → β)) g) :
            (a : FreeGroup α) → β)
          (of a) :
        β)
      ((g : (a : FreeGroup α) → β) (of a) : β)
⊢ (fun (f : α → β) ↦ (MonoidHom.mk' (Quot.lift (r := Red.Step) (Lift.aux f) ⋯) ⋯ : MonoidHom.{u, v} (FreeGroup α) β))
      ((fun (g : MonoidHom.{u, v} (FreeGroup α) β) ↦ ((⇑g : (a : FreeGroup α) → β) ∘ of : α → β)) g) =
    g

Tactic:
ext
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst : Group β
f : α → β
x y : FreeGroup α
g : MonoidHom.{u, v} (FreeGroup α) β
a : α
⊢ Eq.{v + 1} (α := β)
    (((fun (f : α → β) ↦
              (MonoidHom.mk' (Quot.lift (r := Red.Step) (Lift.aux f) ⋯) ⋯ : MonoidHom.{u, v} (FreeGroup α) β))
            ((fun (g : MonoidHom.{u, v} (FreeGroup α) β) ↦ ((⇑g : (a : FreeGroup α) → β) ∘ of : α → β)) g) :
          (a : FreeGroup α) → β)
        (of a) :
      β)
    ((g : (a : FreeGroup α) → β) (of a) : β)

Tactic:
simp [of, Lift.aux]

Premises used: FreeGroup.of, FreeGroup.Lift.aux
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
β : Type v
inst : Group β
f : α → β
⊢ Eq.{v + 1} (α := β)
    ((((lift : (a : α → β) → FreeGroup α →* β) f : MonoidHom.{u, v} (FreeGroup α) β) : (a : FreeGroup α) → β) (mk L) :
      β)
    (List.prod (List.map (fun (x : α × Bool) ↦ bif x.2 then f x.1 else (f x.1)⁻¹) L) : β)

Tactic:
rfl

Premises used: FreeGroup.Lift.aux, rfl, List.prod
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
inst : Group β
f : α → β
x : α
⊢ (((lift : (a : α → β) → FreeGroup α →* β) f : MonoidHom.{u, v} (FreeGroup α) β) : (a : FreeGroup α) → β) (of x) = f x

Tactic:
simp [of]

Premises used: FreeGroup.of
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
inst : Group β
f : α → β
g : MonoidHom.{u, v} (FreeGroup α) β
hg : ∀ (x : α), (g : (a : FreeGroup α) → β) (of x) = f x
x : FreeGroup α
⊢ Eq.{v + 1} (α := β) ((g : (a : FreeGroup α) → β) x : β)
    ((((lift : (a : α → β) → FreeGroup α →* β) f : MonoidHom.{u, v} (FreeGroup α) β) : (a : FreeGroup α) → β) x : β)

Tactic:
DFunLike.congr_fun (lift.symm_apply_eq.mp (funext hg : g ∘ FreeGroup.of = f)) x

Premises used: DFunLike.congr_fun, Equiv.symm_apply_eq, FreeGroup.lift, funext, Iff.mp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := FreeGroup α →* FreeGroup α)
    ((lift : (a : α → FreeGroup α) → FreeGroup α →* FreeGroup α) of : FreeGroup α →* FreeGroup α)
    (MonoidHom.id (FreeGroup α) : FreeGroup α →* FreeGroup α)

Tactic:
lift.apply_symm_apply (MonoidHom.id _)

Premises used: FreeGroup.of, Equiv.apply_symm_apply, FreeGroup.lift, MonoidHom.id, FreeGroup.mk
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x : FreeGroup α
⊢ (((lift : (a : α → FreeGroup α) → FreeGroup α →* FreeGroup α) of : FreeGroup α →* FreeGroup α) :
        (a : FreeGroup α) → FreeGroup α)
      x =
    x

Tactic:
DFunLike.congr_fun (lift_of_eq_id α) x

Premises used: DFunLike.congr_fun, FreeGroup.lift_of_eq_id