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)
β : Type v
inst : Group β
f_1 : α → β
x y : FreeGroup α
f : α → β
⊢ (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
have h : ∀ (x : α),
  (fun (g : MonoidHom.{u, v} (FreeGroup α) β) ↦ ((⇑g : (a : FreeGroup α) → β) ∘ of : α → β))
      ((fun (f : α → β) ↦
          (MonoidHom.mk' (Quot.lift (r := Red.Step) (Lift.aux f) sorry) sorry : MonoidHom.{u, v} (FreeGroup α) β))
        f)
      x =
    f x
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst : Group β
f : α → β
x y : FreeGroup α
g : MonoidHom.{u, v} (FreeGroup α) β
⊢ (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
have h : ∀ (a : α),
  Eq.{v + 1} (α := β)
    (((fun (f : α → β) ↦
              (MonoidHom.mk' (Quot.lift (r := Red.Step) (Lift.aux f) sorry) sorry : 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: ext
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Group β
f : α → β
⊢ Eq (α := Subgroup β) (MonoidHom.range.{u, v} (G := FreeGroup α) ((lift : (a : α → β) → FreeGroup α →* β) f))
    (Subgroup.closure (Set.range f))
have apply : LE.le (α := Subgroup β) (Subgroup.closure (Set.range f))
  (MonoidHom.range.{u, v} (G := FreeGroup α) ((lift : (a : α → β) → FreeGroup α →* β) f))
Tactic: apply le_antisymm (range_lift_le Subgroup.subset_closure)
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Group β
f : α → β
⊢ LE.le (α := Subgroup β) (Subgroup.closure (Set.range f))
    (MonoidHom.range.{u, v} (G := FreeGroup α) ((lift : (a : α → β) → FreeGroup α →* β) f))
have rw : Set.range f ⊆ (↑(MonoidHom.range.{u, v} (G := FreeGroup α) ((lift : (a : α → β) → FreeGroup α →* β) f)) : Set β)
Tactic: rw [Subgroup.closure_le]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
β : Type v
inst : Group β
s : Set β
⊢ Eq (α := Subgroup β) (Subgroup.closure s)
    (MonoidHom.range (G := FreeGroup { x : β // x ∈ s })
      ((lift : (a : { x : β // x ∈ s } → β) → FreeGroup { x : β // x ∈ s } →* β)
        (Subtype.val (p := fun (x : β) ↦ x ∈ s))))
have rw : Eq (α := Subgroup β) (Subgroup.closure s)
  (Subgroup.closure (Set.range (ι := { x : β // x ∈ s }) (Subtype.val (p := fun (x : β) ↦ x ∈ s))))
Tactic: rw [FreeGroup.range_lift_eq_closure, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
β : Type v
inst : Group β
s : Set β
rw :
  Eq (α := Subgroup β) (Subgroup.closure s)
    (Subgroup.closure (Set.range (ι := { x : β // x ∈ s }) (Subtype.val (p := fun (x : β) ↦ x ∈ s))))
⊢ Eq (α := Subgroup β) (Subgroup.closure s)
    (MonoidHom.range (G := FreeGroup { x : β // x ∈ s })
      ((lift : (a : { x : β // x ∈ s } → β) → FreeGroup { x : β // x ∈ s } →* β)
        (Subtype.val (p := fun (x : β) ↦ x ∈ s))))
have rw₁ : Eq (α := Subgroup β) (Subgroup.closure s) (Subgroup.closure s)
Tactic: rw [FreeGroup.range_lift_eq_closure, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Subgroup (FreeGroup α)) (Subgroup.closure (Set.range of)) ⊤
have rw : Eq.{u_1 + 1} (α := Subgroup (FreeGroup α)) (MonoidHom.range (MonoidHom.id (FreeGroup α))) ⊤
Tactic: rw [← range_lift_eq_closure, lift_of_eq_id]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L L₁_1 L₂_1 L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y : FreeGroup α
L₁ L₂ : List (α × Bool)
H : Red.Step L₁ L₂
⊢ Red.Step.{v} (α := β) (List.map (fun (x : α × Bool) ↦ (f x.1, x.2)) L₁)
    (List.map (fun (x : α × Bool) ↦ (f x.1, x.2)) L₂)
have not : ∀ {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool},
  Red.Step.{v} (α := β) (List.map (fun (x : α × Bool) ↦ (f x.1, x.2)) (L₁ ++ (x, b) :: (x, !b) :: L₂))
    (List.map (fun (x : α × Bool) ↦ (f x.1, x.2)) (L₁ ++ L₂))
Tactic: cases H
Cleared hypotheses: L₁, L₂, H
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
x : FreeGroup α
⊢ (map _root_.id : (a : FreeGroup α) → FreeGroup α) x = x
have mk : ∀ (L : List (α × Bool)),
  Eq (α := FreeGroup α) ((map _root_.id : (a : FreeGroup α) → FreeGroup α) (Quot.mk Red.Step L) : FreeGroup α)
    (Quot.mk Red.Step L : Quot (α := List (α × Bool)) Red.Step)
Tactic: rcases x with ⟨L⟩
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeGroup α
⊢ Eq.{w + 1} (α := FreeGroup γ)
    ((map g : (a : FreeGroup β) → FreeGroup γ) ((map f : (a : FreeGroup α) → FreeGroup β) x) : FreeGroup γ)
    ((map (g ∘ f) : (a : FreeGroup α) → FreeGroup γ) x : FreeGroup γ)
have mk : ∀ (L : List (α × Bool)),
  Eq.{w + 1} (α := FreeGroup γ)
    ((map g : (a : FreeGroup β) → FreeGroup γ) ((map f : (a : FreeGroup α) → FreeGroup β) (Quot.mk Red.Step L)) :
      FreeGroup γ)
    ((map (g ∘ f) : (a : FreeGroup α) → FreeGroup γ) (Quot.mk Red.Step L) : FreeGroup γ)
Tactic: rcases x with ⟨L⟩
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
⊢ map f = (lift : (a : α → FreeGroup β) → FreeGroup α →* FreeGroup β) (of ∘ f)
have h : ∀ (a : α),
  Eq.{v + 1} (α := FreeGroup β) ((map f : (a : FreeGroup α) → FreeGroup β) (of a) : FreeGroup β)
    ((((lift : (a : α → FreeGroup β) → FreeGroup α →* FreeGroup β) (of ∘ f) :
            MonoidHom.{u, v} (FreeGroup α) (FreeGroup β)) :
          (a : FreeGroup α) → FreeGroup β)
        (of a) :
      FreeGroup β)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
⊢ (map f).range = Subgroup.closure (of '' Set.range f)
have rw : Eq (α := Subgroup (FreeGroup β))
  (MonoidHom.range.{u, v} (G := FreeGroup α) ((lift : (a : α → FreeGroup β) → FreeGroup α →* FreeGroup β) (of ∘ f)))
  (Subgroup.closure (of '' Set.range f))
Tactic: rw [map_eq_lift, range_lift_eq_closure, Set.range_comp]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
rw :
  Eq (α := Subgroup (FreeGroup β))
    (MonoidHom.range.{u, v} (G := FreeGroup α) ((lift : (a : α → FreeGroup β) → FreeGroup α →* FreeGroup β) (of ∘ f)))
    (Subgroup.closure (of '' Set.range f))
⊢ (map f).range = Subgroup.closure (of '' Set.range f)
have rw₁ : Eq (α := Subgroup (FreeGroup β)) (Subgroup.closure (Set.range (of ∘ f))) (Subgroup.closure (of '' Set.range f))
Tactic: rw [map_eq_lift, range_lift_eq_closure, Set.range_comp]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
rw :
  Eq (α := Subgroup (FreeGroup β))
    (MonoidHom.range.{u, v} (G := FreeGroup α) ((lift : (a : α → FreeGroup β) → FreeGroup α →* FreeGroup β) (of ∘ f)))
    (Subgroup.closure (of '' Set.range f))
rw₁ : Eq (α := Subgroup (FreeGroup β)) (Subgroup.closure (Set.range (of ∘ f))) (Subgroup.closure (of '' Set.range f))
⊢ (map f).range = Subgroup.closure (of '' Set.range f)
have rw₂ : Eq (α := Subgroup (FreeGroup β)) (Subgroup.closure (of '' Set.range f)) (Subgroup.closure (of '' Set.range f))
Tactic: rw [map_eq_lift, range_lift_eq_closure, Set.range_comp]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
hf : Function.Surjective f
⊢ Function.Surjective.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)
have rw : (map f).range = ⊤
Tactic: rw [← MonoidHom.range_eq_top, range_map, hf.range_eq, Set.image_univ, closure_range_of]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
hf : Function.Surjective f
rw : (map f).range = ⊤
⊢ Function.Surjective.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)
have rw₁ : Eq (α := Subgroup (FreeGroup β)) (Subgroup.closure (of '' Set.range f)) ⊤
Tactic: rw [← MonoidHom.range_eq_top, range_map, hf.range_eq, Set.image_univ, closure_range_of]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
hf : Function.Surjective f
rw : (map f).range = ⊤
rw₁ : Eq (α := Subgroup (FreeGroup β)) (Subgroup.closure (of '' Set.range f)) ⊤
⊢ Function.Surjective.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)
have rw₂ : Eq.{v + 1} (α := Subgroup (FreeGroup β)) (Subgroup.closure (of '' Set.univ)) ⊤
Tactic: rw [← MonoidHom.range_eq_top, range_map, hf.range_eq, Set.image_univ, closure_range_of]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
hf : Function.Surjective f
rw : (map f).range = ⊤
rw₁ : Eq (α := Subgroup (FreeGroup β)) (Subgroup.closure (of '' Set.range f)) ⊤
rw₂ : Eq.{v + 1} (α := Subgroup (FreeGroup β)) (Subgroup.closure (of '' Set.univ)) ⊤
⊢ Function.Surjective.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)
have rw₃ : Eq.{v + 1} (α := Subgroup (FreeGroup β)) (Subgroup.closure (Set.range of)) ⊤
Tactic: rw [← MonoidHom.range_eq_top, range_map, hf.range_eq, Set.image_univ, closure_range_of]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
hf : Function.Surjective f
rw : (map f).range = ⊤
rw₁ : Eq (α := Subgroup (FreeGroup β)) (Subgroup.closure (of '' Set.range f)) ⊤
rw₂ : Eq.{v + 1} (α := Subgroup (FreeGroup β)) (Subgroup.closure (of '' Set.univ)) ⊤
rw₃ : Eq.{v + 1} (α := Subgroup (FreeGroup β)) (Subgroup.closure (Set.range of)) ⊤
⊢ Function.Surjective.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)
have rw₄ : Eq.{v + 1} (α := Subgroup (FreeGroup β)) ⊤ ⊤
Tactic: rw [← MonoidHom.range_eq_top, range_map, hf.range_eq, Set.image_univ, closure_range_of]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
⊢ Function.Injective.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)
have pos : ∀ (h : IsEmpty α),
  Function.Injective.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)
Tactic: by_cases! h : IsEmpty α
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
pos :
  ∀ (h : IsEmpty α),
    Function.Injective.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)
⊢ Function.Injective.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)
have neg : ∀ (h : Nonempty α),
  Function.Injective.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)
Tactic: by_cases! h : IsEmpty α
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
h : Nonempty α
⊢ Function.Injective.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)
have neg : Function.HasLeftInverse.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β)
  (⇑(map f) : (a : FreeGroup α) → FreeGroup β)
Tactic: rw [Function.injective_iff_hasLeftInverse]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
h : Nonempty α
⊢ Function.HasLeftInverse.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β)
    (⇑(map f) : (a : FreeGroup α) → FreeGroup β)
have h₁ : Function.LeftInverse.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β)
  (⇑(map (Function.invFun f)) : (a : FreeGroup β) → FreeGroup α) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)
Tactic: use map (Function.invFun f)
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Group β
f : α → β
x : FreeGroup α
⊢ Eq.{v + 1} (α := β)
    ((((lift : (a : α → β) → FreeGroup α →* β) f : MonoidHom.{u, v} (FreeGroup α) β) : (a : FreeGroup α) → β) x : β)
    ((prod : (a : FreeGroup β) → β) ((map f : (a : FreeGroup α) → FreeGroup β) x : FreeGroup β) : β)
have rw : Eq.{v + 1} (α := β) ((MonoidHom.comp prod (map f) : (a : FreeGroup α) → β) x : β)
  ((prod : (a : FreeGroup β) → β) ((map f : (a : FreeGroup α) → FreeGroup β) x : FreeGroup β) : β)
Tactic: rw [← lift_unique (prod.comp (map f)) (by simp), MonoidHom.coe_comp, Function.comp_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Group β
f : α → β
x : FreeGroup α
rw :
  Eq.{v + 1} (α := β) ((MonoidHom.comp prod (map f) : (a : FreeGroup α) → β) x : β)
    ((prod : (a : FreeGroup β) → β) ((map f : (a : FreeGroup α) → FreeGroup β) x : FreeGroup β) : β)
⊢ Eq.{v + 1} (α := β)
    ((((lift : (a : α → β) → FreeGroup α →* β) f : MonoidHom.{u, v} (FreeGroup α) β) : (a : FreeGroup α) → β) x : β)
    ((prod : (a : FreeGroup β) → β) ((map f : (a : FreeGroup α) → FreeGroup β) x : FreeGroup β) : β)
have rw₁ : Eq.{v + 1} (α := β)
  (Function.comp (β := FreeGroup β) (⇑prod : (a : FreeGroup β) → β) (⇑(map f) : (a : FreeGroup α) → FreeGroup β) x : β)
  ((prod : (a : FreeGroup β) → β) ((map f : (a : FreeGroup α) → FreeGroup β) x : FreeGroup β) : β)
Tactic: rw [← lift_unique (prod.comp (map f)) (by simp), MonoidHom.coe_comp, Function.comp_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Group β
f : α → β
x : FreeGroup α
rw :
  Eq.{v + 1} (α := β) ((MonoidHom.comp prod (map f) : (a : FreeGroup α) → β) x : β)
    ((prod : (a : FreeGroup β) → β) ((map f : (a : FreeGroup α) → FreeGroup β) x : FreeGroup β) : β)
rw₁ :
  Eq.{v + 1} (α := β)
    (Function.comp (β := FreeGroup β) (⇑prod : (a : FreeGroup β) → β) (⇑(map f) : (a : FreeGroup α) → FreeGroup β) x :
      β)
    ((prod : (a : FreeGroup β) → β) ((map f : (a : FreeGroup α) → FreeGroup β) x : FreeGroup β) : β)
⊢ Eq.{v + 1} (α := β)
    ((((lift : (a : α → β) → FreeGroup α →* β) f : MonoidHom.{u, v} (FreeGroup α) β) : (a : FreeGroup α) → β) x : β)
    ((prod : (a : FreeGroup β) → β) ((map f : (a : FreeGroup α) → FreeGroup β) x : FreeGroup β) : β)
have rw₂ : Eq.{v + 1} (α := β) ((prod : (a : FreeGroup β) → β) ((map f : (a : FreeGroup α) → FreeGroup β) x : FreeGroup β) : β)
  ((prod : (a : FreeGroup β) → β) ((map f : (a : FreeGroup α) → FreeGroup β) x : FreeGroup β) : β)
Tactic: rw [← lift_unique (prod.comp (map f)) (by simp), MonoidHom.coe_comp, Function.comp_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : FreeGroup Unit
⊢ FreeGroup ℤ
have revert : (x : FreeGroup Unit) → FreeGroup ℤ
Tactic: revert x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L_1 L₁ L₂ L₃ L₄ : List (α × Bool)
x : FreeGroup Unit
L : List (Unit × Bool)
⊢ Eq (α := FreeGroup Unit)
    ((fun (x : ℤ) ↦ of () ^ x)
      ((fun (x : FreeGroup Unit) ↦ (sum ((map fun (x : Unit) ↦ 1 : (a : FreeGroup Unit) → FreeGroup ℤ) x) : ℤ))
        (Quot.mk Red.Step L)))
    (Quot.mk Red.Step L)
have mk : 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: simp only [quot_mk_eq_mk, map.mk, sum_mk, List.map_map]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ 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)
have 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, false) :: tl))) =
  mk ((PUnit.unit, false) :: tl)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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)
⊢ 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)
have 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, true) :: tl))) =
  mk ((PUnit.unit, true) :: tl)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ 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, false) :: tl))) =
    mk ((PUnit.unit, false) :: tl)
have false : (of ())⁻¹ * mk tl = mk ((PUnit.unit, false) :: tl)
Tactic: simp [zpow_add, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
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
⊢ 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, true) :: tl))) =
    mk ((PUnit.unit, true) :: tl)
have true : of () * mk tl = mk ((PUnit.unit, true) :: tl)
Tactic: simp [zpow_add, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 : ℤ)
⊢ (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
have ih₁ : (HPow.hPow (α := FreeGroup ℤ) (of 1) i).sum = (↑i : ℤ)
Tactic: simp only [zpow_natCast, map_pow, map.of] at ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (hypothesis)
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 : ℤ))
⊢ (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
have ih₁ : (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
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.GroupTheory.FreeGroup.Basic (goal)
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst : Unique α
x : FreeGroup α
⊢ (fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x)
      ((fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
        x) =
    x
have C1 : 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: 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 : FreeGroup α
C1 :
  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
⊢ (fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (of default) x)
      ((fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
        x) =
    x
have 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: 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 : 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
⊢ (fun (x : ℤ) ↦ HPow.hPow (α := FreeGroup α) (FreeGroup.of default) x)
      ((fun (x : FreeGroup α) ↦ (sum (((map 1 : FreeGroup α →* FreeGroup ℤ) : (a : FreeGroup α) → FreeGroup ℤ) x) : ℤ))
        x) =
    x
have 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)⁻¹
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