awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
nil : sizeOf ([] ++ L2) < sizeOf ([] ++ (x, b) :: (x, !b) :: L2)
⊢ sizeOf (L1 ++ L2) < sizeOf (L1 ++ (x, b) :: (x, !b) :: L2)
have cons : ∀ (hd : α × Bool) (tl : List (α × Bool)) (ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)),
  sizeOf (hd :: tl ++ L2) < sizeOf (hd :: tl ++ (x, b) :: (x, !b) :: L2)
Tactic: induction L1 with
    | nil =>
      dsimp
      lia
    | cons hd tl ih =>
      dsimp
      exact Nat.add_lt_add_left ih _
Cleared hypotheses: L1
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L₁ L₂ b c : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ b
h₂₃ : Step b c
ih : ∃ (n : ℕ), L₁.length = b.length + 2 * n
⊢ ∃ (n : ℕ), L₁.length = c.length + 2 * n
have tail : ∀ (n : ℕ) (eq : L₁.length = b.length + 2 * n), ∃ (n : ℕ), L₁.length = c.length + 2 * n
Tactic: rcases ih with ⟨n, eq⟩
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L₁ L₂ b c : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ b
h₂₃ : Step b c
n : ℕ
eq : L₁.length = b.length + 2 * n
⊢ ∃ (n : ℕ), L₁.length = c.length + 2 * n
have tail : L₁.length = c.length + 2 * (1 + n)
Tactic: exists 1 + n
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
h : Red L₁ L₂
⊢ ∃ (n : ℕ), L₁.length = L₂.length + 2 * n
have refl : ∃ (n : ℕ), L₁.length = L₁.length + 2 * n
Tactic: induction h with
  | refl => exact ⟨0, rfl⟩
  | tail _h₁₂ h₂₃ ih =>
    rcases ih with ⟨n, eq⟩
    exists 1 + n
    simp [Nat.mul_add, eq, (Step.length h₂₃).symm, add_assoc]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
h : Red L₁ L₂
refl : ∃ (n : ℕ), L₁.length = L₁.length + 2 * n
⊢ ∃ (n : ℕ), L₁.length = L₂.length + 2 * n
have tail : ∀ {b c : List (α × Bool)} (_h₁₂ : ReflTransGen Step L₁ b) (h₂₃ : Step b c)
  (ih : ∃ (n : ℕ), L₁.length = b.length + 2 * n), ∃ (n : ℕ), L₁.length = c.length + 2 * n
Tactic: induction h with
  | refl => exact ⟨0, rfl⟩
  | tail _h₁₂ h₂₃ ih =>
    rcases ih with ⟨n, eq⟩
    exists 1 + n
    simp [Nat.mul_add, eq, (Step.length h₂₃).symm, add_assoc]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
h : IsReduced L₁
step : Red.Step L₁ L₂
⊢ False
have not : ∀ {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool} (h : IsReduced (L₁ ++ (x, b) :: (x, !b) :: L₂)), False
Tactic: induction step
Cleared hypotheses: h, step
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
a₁ : α
b₁ : Bool
a₂ : α
b₂ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: (a₂, b₂) :: L₁) L₂
⊢ IsReduced ((a₁, b₁) :: (a₂, b₂) :: L₁)
have rw : ((a₁, b₁).1 = (a₂, b₂).1 → (a₁, b₁).2 = (a₂, b₂).2) ∧ IsReduced ((a₂, b₂) :: L₁)
Tactic: rw [isReduced_cons_cons]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
a₁ : α
b₁ : Bool
a₂ : α
b₂ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: (a₂, b₂) :: L₁) L₂
⊢ ((a₁, b₁).1 = (a₂, b₂).1 → (a₁, b₁).2 = (a₂, b₂).2) ∧ IsReduced ((a₂, b₂) :: L₁)
have refine : (a₁, b₁).1 = (a₂, b₂).1 → (a₁, b₁).2 = (a₂, b₂).2
Tactic: refine ⟨?_, .of_forall_not_step fun L₂ step ↦ hL₁ _ step.cons⟩
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
a₁ : α
b₁ b₂ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: ((a₁, b₁).1, b₂) :: L₁) L₂
⊢ (a₁, b₁).2 = ((a₁, b₁).1, b₂).2
have symm : ((a₁, b₁).1, b₂).2 = (a₁, b₁).2
Tactic: symm
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
a₁ : α
b₁ b₂ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: ((a₁, b₁).1, b₂) :: L₁) L₂
⊢ ((a₁, b₁).1, b₂).2 = (a₁, b₁).2
have rw : ((a₁, b₁).1, b₂).2 ≠ !(a₁, b₁).2
Tactic: rw [← Bool.ne_not]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L L₁ L₂ L₃ L₄ a b : List (α × Bool)
h : Red.Step a b
⊢ Red.Step (invRev a) (invRev b)
have not : ∀ {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool}, Red.Step (invRev (L₁ ++ (x, b) :: (x, !b) :: L₂)) (invRev (L₁ ++ L₂))
Tactic: cases h
Cleared hypotheses: a, b, h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
h : Step L₁ L₂
⊢ Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)
have obtain : ∀ {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool},
  Step (FreeGroup.invRev (L₁ ++ (x, b) :: (x, !b) :: L₂)) (FreeGroup.invRev (L₁ ++ L₂))
Tactic: obtain ⟨a, b, x, y⟩ := h
Cleared hypotheses: L₁, L₂, h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L : List (α × Bool)
n_1 n : ℕ
⊢ mk L ^ (n + 1) = mk (List.replicate (n + 1) L).flatten
have rw : mk L * mk L ^ n = mk (List.replicate (n + 1) L).flatten
Tactic: rw [pow_succ', pow_mk, mul_mk, List.replicate_succ, List.flatten_cons]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L : List (α × Bool)
n_1 n : ℕ
rw : mk L * mk L ^ n = mk (List.replicate (n + 1) L).flatten
⊢ mk L ^ (n + 1) = mk (List.replicate (n + 1) L).flatten
have rw₁ : mk L * mk (List.replicate n L).flatten = mk (List.replicate (n + 1) L).flatten
Tactic: rw [pow_succ', pow_mk, mul_mk, List.replicate_succ, List.flatten_cons]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ mk L ^ (n + 1) = mk (List.replicate (n + 1) L).flatten
have rw₂ : mk (L ++ (List.replicate n L).flatten) = mk (List.replicate (n + 1) L).flatten
Tactic: rw [pow_succ', pow_mk, mul_mk, List.replicate_succ, List.flatten_cons]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ mk L ^ (n + 1) = mk (List.replicate (n + 1) L).flatten
have rw₃ : mk (L ++ (List.replicate n L).flatten) = mk (L :: List.replicate n L).flatten
Tactic: rw [pow_succ', pow_mk, mul_mk, List.replicate_succ, List.flatten_cons]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ mk L ^ (n + 1) = mk (List.replicate (n + 1) L).flatten
have rw₄ : mk (L ++ (List.replicate n L).flatten) = mk (L ++ (List.replicate n L).flatten)
Tactic: rw [pow_succ', pow_mk, mul_mk, List.replicate_succ, List.flatten_cons]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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)
⊢ f = g
have h₁ : ∀ (x : FreeGroup α), Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) x : M) ((g : (a : FreeGroup α) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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 : α
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M) ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M)
have 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)
Tactic: trans f (of x)⁻¹ * f (of x) * g (of x)⁻¹
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M) ((g : (a : FreeGroup α) → M) (of x)⁻¹ : M)
have 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)⁻¹
Tactic: trans f (of x)⁻¹ * f (of x) * g (of x)⁻¹
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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 : α
⊢ (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)
have 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))
Tactic: simp_rw [mul_assoc, h, ← _root_.map_mul, mul_inv_cancel, _root_.map_one, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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))
⊢ (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)
have 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))
Tactic: simp_rw [mul_assoc, h, ← _root_.map_mul, mul_inv_cancel, _root_.map_one, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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))
⊢ (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)
have 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)
Tactic: simp_rw [mul_assoc, h, ← _root_.map_mul, mul_inv_cancel, _root_.map_one, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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)
⊢ (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)
have 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)
Tactic: simp_rw [mul_assoc, h, ← _root_.map_mul, mul_inv_cancel, _root_.map_one, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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)
⊢ (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)
have simp_rw₄ : (f : (a : FreeGroup α) → M) (of x)⁻¹ = HMul.hMul (α := M) (β := M) ((f : (a : FreeGroup α) → M) (of x)⁻¹ : M) (1 : M)
Tactic: simp_rw [mul_assoc, h, ← _root_.map_mul, mul_inv_cancel, _root_.map_one, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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 : α
⊢ 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)⁻¹
have 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)⁻¹
Tactic: simp_rw [← _root_.map_mul, inv_mul_cancel, _root_.map_one, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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)⁻¹
⊢ 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)⁻¹
have 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)⁻¹
Tactic: simp_rw [← _root_.map_mul, inv_mul_cancel, _root_.map_one, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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)⁻¹
⊢ 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)⁻¹
have simp_rw₂ : HMul.hMul (α := M) (β := M) (1 : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 α
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) x : M) ((g : (a : FreeGroup α) → M) x : M)
have this : ∀ (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]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) x : M) ((g : (a : FreeGroup α) → M) x : M)
have h₁ : Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) 1 : M) ((g : (a : FreeGroup α) → M) 1 : M)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) x : M) ((g : (a : FreeGroup α) → M) x : M)
have 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)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : FreeGroup α) → M) x : M) ((g : (a : FreeGroup α) → M) x : M)
have 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)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
x x_1 : α
H : of x = of x_1
⊢ x = x_1
have let : ∀ (L₁ : List (α × Bool)) (hx : Red [(x, true)] L₁) (hy : Red [(x_1, true)] L₁), x = x_1
Tactic: let ⟨L₁, hx, hy⟩ := Red.exact.1 H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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₁
⊢ x = x_1
have hx₁ : L₁ = [(x, true)]
Tactic: simp [Red.singleton_iff] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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)]
⊢ x = x_1
have hy₁ : L₁ = [(x_1, true)]
Tactic: simp [Red.singleton_iff] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L₁ L₂ : List (α × Bool)
β : Type v
inst : Group β
f : α → β
H : Step L₁ L₂
⊢ Lift.aux f L₁ = Lift.aux f L₂
have obtain : ∀ {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool}, Lift.aux f (L₁ ++ (x, b) :: (x, !b) :: L₂) = Lift.aux f (L₁ ++ L₂)
Tactic: obtain @⟨_, _, _, b⟩ := H
Cleared hypotheses: L₁, L₂, H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Group β
f : α → β
L₁ L₂ : List (α × Bool)
x : α
b : Bool
⊢ Lift.aux f (L₁ ++ (x, b) :: (x, !b) :: L₂) = Lift.aux f (L₁ ++ L₂)
have false : Lift.aux f (L₁ ++ (x, false) :: (x, !false) :: L₂) = Lift.aux f (L₁ ++ L₂)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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₂)
⊢ Lift.aux f (L₁ ++ (x, b) :: (x, !b) :: L₂) = Lift.aux f (L₁ ++ L₂)
have true : Lift.aux f (L₁ ++ (x, true) :: (x, !true) :: L₂) = Lift.aux f (L₁ ++ L₂)
Tactic: cases b
Cleared hypotheses: b