awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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)⁻¹
⊢ (fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (FreeGroup.of default) x)
      ((fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
        x) =
    x
have 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
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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
x : ℤ
⊢ (fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
      ((fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x) x) =
    x
have zero : Eq (α := ℤ)
  ((fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
    ((fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x) 0))
  0
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
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ (fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
      ((fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x) x) =
    x
have 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
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
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ (fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
      ((fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x) x) =
    x
have 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
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
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
x : ℤ
⊢ (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
have 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
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ (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
have 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
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ (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
have 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
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ id <$> (of x)⁻¹ = (of x)⁻¹
have rw : (id <$> of x)⁻¹ = (of x)⁻¹
Tactic: rw [map_inv, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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)⁻¹
⊢ id <$> (of x)⁻¹ = (of x)⁻¹
have rw₁ : (of x)⁻¹ = (of x)⁻¹
Tactic: rw [map_inv, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ id <$> (x * y) = x * y
have rw : id <$> x * id <$> y = x * y
Tactic: rw [map_mul, ihx, ihy]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ id <$> (x * y) = x * y
have rw₁ : x * id <$> y = x * y
Tactic: rw [map_mul, ihx, ihy]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ id <$> (x * y) = x * y
have rw₂ : x * y = x * y
Tactic: rw [map_mul, ihx, ihy]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
have refine_1 : ∀ (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), 1 >>= f >>= g = 1 >>= fun (x : α_1) ↦ f x >>= g
Tactic: refine FreeGroup.induction_on x ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ ∀ (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
have refine_2 : ∀ (x : α_1) (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), of x >>= f >>= g = of x >>= fun (x : α_1) ↦ f x >>= g
Tactic: refine FreeGroup.induction_on x ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ ∀ (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
have 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
Tactic: refine FreeGroup.induction_on x ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ ∀ (f : α_1 → FreeGroup β_1) (g : β_1 → FreeGroup γ), x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
have 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
Tactic: refine FreeGroup.induction_on x ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
have refine_1 : Eq (α := FreeGroup β_1)
  (do
    let y ← 1
    pure (f y))
  (f <$> 1)
Tactic: refine FreeGroup.induction_on x ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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)
⊢ (do
      let y ← x
      pure (f y)) =
    f <$> x
have refine_2 : ∀ (x : α_1),
  (do
      let y ← of x
      pure (f y)) =
    f <$> of x
Tactic: refine FreeGroup.induction_on x ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ (do
      let y ← x
      pure (f y)) =
    f <$> x
have 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)⁻¹
Tactic: refine FreeGroup.induction_on x ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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)⁻¹
⊢ (do
      let y ← x
      pure (f y)) =
    f <$> x
have 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)
Tactic: refine FreeGroup.induction_on x ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
Goal:
α : Type u
L : List (α × Bool)
a b : α × Bool
⊢ IsCyclicallyReduced (b :: L ++ [a]) ↔ IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)
have 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)
Tactic: rw [isCyclicallyReduced_iff, List.getLast?_concat]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
Goal:
α : Type u
L : List (α × Bool)
n_1 n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
⊢ IsCyclicallyReduced (replicate (n + 1) (head :: tail)).flatten
have 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
Tactic: rw [isCyclicallyReduced_iff, IsReduced, List.isChain_flatten (by simp)]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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) ∧
      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
have 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
Tactic: refine ⟨⟨by simpa [IsReduced] using h.isReduced, List.isChain_replicate_of_rel _ h.2⟩,
      fun _ ha _ hb ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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?
⊢ x.1 = x_1.1 → x.2 = x_1.2
have 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
Tactic: rw [Option.mem_def, List.getLast?_flatten_replicate (h := by simp +arith)] at ha
Cleared hypotheses: ha, x_1, hb
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (hypothesis)
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?
⊢ x.1 = x_1.1 → x.2 = x_1.2
have hb₁ : (head :: tail).head? = some x_1
Tactic: rw [Option.mem_def, List.head?_flatten_replicate (h := by simp +arith)] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (hypothesis)
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₃)
have h' : (replicate (n + 1) L₂).flatten ≠ []
Tactic: have h' : (replicate (n + 1) L₂).flatten ≠ [] := by simp [h]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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₃)
have refine_1 : IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten)
Tactic: refine IsReduced.append_overlap ?_ ?_ (hn := h')
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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)
⊢ IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten ++ L₃)
have refine_2 : IsReduced ((replicate (n + 1) L₂).flatten ++ L₃)
Tactic: refine IsReduced.append_overlap ?_ ?_ (hn := h')
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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)
have refine_1 : IsReduced (L₁ ++ L₂ ++ (replicate n L₂).flatten)
Tactic: rw [replicate_succ, flatten_cons, ← append_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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₁ ++ L₂ ++ (replicate n L₂).flatten)
have refine_1 : IsReduced (L₂ ++ (replicate n L₂).flatten)
Tactic: refine IsReduced.append_overlap (h₂.infix ⟨[], L₃, by simp⟩) ?_ h
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced (goal)
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 ++ L₃)
have refine_2 : IsReduced ((replicate n L₂).flatten ++ L₂ ++ L₃)
Tactic: rw [replicate_succ', flatten_concat]