awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
inst : Group β
f : α → β
s : Subgroup β
H : Set.range f ⊆ (↑s : Set β)
w : FreeGroup α
L : List (α × Bool)
x_1 : α × Bool
tl : List (α × Bool)
ih :
  Membership.mem (α := β) s
    ((((lift : (a : α → β) → FreeGroup α →* β) f : MonoidHom.{u, v} (FreeGroup α) β) : (a : FreeGroup α) → β)
        (Quot.mk Red.Step tl) :
      β)
x : α
b : Bool
⊢ Membership.mem (α := β) s
    ((((lift : (a : α → β) → FreeGroup α →* β) f : MonoidHom.{u, v} (FreeGroup α) β) : (a : FreeGroup α) → β)
        (Quot.mk Red.Step ((x, false) :: tl)) :
      β)

Tactic:
simpa using s.mul_mem (s.inv_mem <| H ⟨x, rfl⟩) ih

Premises used: Subgroup.inv_mem, Exists.intro, Subgroup.mul_mem, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
inst : Group β
f : α → β
s : Subgroup β
H : Set.range f ⊆ (↑s : Set β)
w : FreeGroup α
L : List (α × Bool)
x_1 : α × Bool
tl : List (α × Bool)
ih :
  Membership.mem (α := β) s
    ((((lift : (a : α → β) → FreeGroup α →* β) f : MonoidHom.{u, v} (FreeGroup α) β) : (a : FreeGroup α) → β)
        (Quot.mk Red.Step tl) :
      β)
x : α
b : Bool
⊢ Membership.mem (α := β) s
    ((((lift : (a : α → β) → FreeGroup α →* β) f : MonoidHom.{u, v} (FreeGroup α) β) : (a : FreeGroup α) → β)
        (Quot.mk Red.Step ((x, true) :: tl)) :
      β)

Tactic:
simpa using s.mul_mem (H ⟨x, rfl⟩) ih

Premises used: Exists.intro, Subgroup.mul_mem, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
inst : Group β
f : α → β
s : Subgroup β
H : Set.range f ⊆ (↑s : Set β)
w : FreeGroup α
L : List (α × Bool)
⊢ Membership.mem (α := β) s
    ((((lift : (a : α → β) → FreeGroup α →* β) f : MonoidHom.{u, v} (FreeGroup α) β) : (a : FreeGroup α) → β)
        (Quot.mk Red.Step L) :
      β)

Tactic:
exact List.recOn L s.one_mem fun ⟨x, b⟩ tl ih ↦
    Bool.recOn b (by simpa using s.mul_mem (s.inv_mem <| H ⟨x, rfl⟩) ih)
      (by simpa using s.mul_mem (H ⟨x, rfl⟩) ih)
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
inst : Group β
f : α → β
apply :
  LE.le (α := Subgroup β) (Subgroup.closure (Set.range f))
    (MonoidHom.range.{u, v} (G := FreeGroup α) ((lift : (a : α → β) → FreeGroup α →* β) f))
⊢ Eq (α := Subgroup β) (MonoidHom.range.{u, v} (G := FreeGroup α) ((lift : (a : α → β) → FreeGroup α →* β) f))
    (Subgroup.closure (Set.range f))

Tactic:
apply le_antisymm (range_lift_le Subgroup.subset_closure)

Premises used: Subgroup.subset_closure, le_antisymm, FreeGroup.range_lift_le
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
inst : Group β
f : α → β
rw : Set.range f ⊆ (↑(MonoidHom.range.{u, v} (G := FreeGroup α) ((lift : (a : α → β) → FreeGroup α →* β) f)) : Set β)
⊢ LE.le (α := Subgroup β) (Subgroup.closure (Set.range f))
    (MonoidHom.range.{u, v} (G := FreeGroup α) ((lift : (a : α → β) → FreeGroup α →* β) f))

Tactic:
rw [Subgroup.closure_le]

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

Tactic:
simp only [lift_apply_of]

Premises used: FreeGroup.lift_apply_of
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
inst : Group β
f : α → β
a : α
⊢ f a ∈ (↑(MonoidHom.range.{u, v} (G := FreeGroup α) ((lift : (a : α → β) → FreeGroup α →* β) f)) : Set β)

Tactic:
exact ⟨FreeGroup.of a, by simp only [lift_apply_of]⟩
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
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))))
rw₁ rw₂ : Eq (α := Subgroup β) (Subgroup.closure s) (Subgroup.closure 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))))

Tactic:
rw [FreeGroup.range_lift_eq_closure, Subtype.range_coe]

Premises used: FreeGroup.range_lift_eq_closure, Subtype.range_coe
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u_1
rw : Eq.{u_1 + 1} (α := Subgroup (FreeGroup α)) (MonoidHom.range (MonoidHom.id (FreeGroup α))) ⊤
⊢ Eq.{u_1 + 1} (α := Subgroup (FreeGroup α)) (Subgroup.closure (Set.range of)) ⊤

Tactic:
rw [← range_lift_eq_closure, lift_of_eq_id]

Premises used: FreeGroup.lift_of_eq_id, FreeGroup.range_lift_eq_closure
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Subgroup (FreeGroup α)) (MonoidHom.range (MonoidHom.id (FreeGroup α))) ⊤

Tactic:
MonoidHom.range_eq_top.2 Function.surjective_id

Premises used: Iff.mpr, MonoidHom.range_eq_top, Function.surjective_id
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Subgroup (FreeGroup α)) (MonoidHom.range (MonoidHom.id (FreeGroup α))) ⊤

Tactic:
exact MonoidHom.range_eq_top.2 Function.surjective_id

Premises used: Iff.mpr, MonoidHom.range_eq_top
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
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₂
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₂))
⊢ 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₂)

Tactic:
cases H
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y : FreeGroup α
L₁_1 L₂_1 : List (α × Bool)
x_1 : α
b : Bool
⊢ Red.Step.{v} (α := β) (List.map (fun (x : α × Bool) ↦ (f x.1, x.2)) (L₁_1 ++ (x_1, b) :: (x_1, !b) :: L₂_1))
    (List.map (fun (x : α × Bool) ↦ (f x.1, x.2)) (L₁_1 ++ L₂_1))

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁_1 L₂_1 L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y a : FreeGroup α
L₁ : List (α × Bool)
b : FreeGroup α
L₂ : List (α × Bool)
⊢ Quot.map (ra := Red.Step) (rb := Red.Step) (List.map fun (x : α × Bool) ↦ (f x.1, x.2)) ⋯
      (HMul.hMul (α := FreeGroup α) (Quot.mk Red.Step L₁) (Quot.mk Red.Step L₂)) =
    HMul.hMul (α := FreeGroup β)
      (Quot.map (ra := Red.Step) (rb := Red.Step) (List.map fun (x : α × Bool) ↦ (f x.1, x.2)) ⋯ (Quot.mk Red.Step L₁))
      (Quot.map (ra := Red.Step) (rb := Red.Step) (List.map fun (x : α × Bool) ↦ (f x.1, x.2)) ⋯ (Quot.mk Red.Step L₂))

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
β : Type v
f : α → β
⊢ Eq.{v + 1} (α := FreeGroup β) ((map f : (a : FreeGroup α) → FreeGroup β) (FreeGroup.mk L) : FreeGroup β)
    (FreeGroup.mk (List.map (fun (x : α × Bool) ↦ (f x.1, x.2)) L) : FreeGroup β)

Tactic:
rfl

Premises used: FreeGroup.mk, Quot.map, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x : FreeGroup α
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)
⊢ (map _root_.id : (a : FreeGroup α) → FreeGroup α) x = x

Tactic:
rcases x with ⟨L⟩
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x : FreeGroup α
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:
simp [List.map_id']

Premises used: List.map_id'
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
x : FreeGroup α
⊢ (map fun (z : α) ↦ z : (a : FreeGroup α) → FreeGroup α) x = x

Tactic:
map.id x

Premises used: FreeGroup.map.id
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeGroup α
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 γ)
⊢ Eq.{w + 1} (α := FreeGroup γ)
    ((map g : (a : FreeGroup β) → FreeGroup γ) ((map f : (a : FreeGroup α) → FreeGroup β) x) : FreeGroup γ)
    ((map (g ∘ f) : (a : FreeGroup α) → FreeGroup γ) x : FreeGroup γ)

Tactic:
rcases x with ⟨L⟩
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeGroup α
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:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
f : α → β
x : α
⊢ (map f : (a : FreeGroup α) → FreeGroup β) (FreeGroup.of x) = FreeGroup.of (f x)

Tactic:
rfl

Premises used: FreeGroup.of, List.map, FreeGroup.mk, Quot.map, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
f : α → β
g : MonoidHom.{u, v} (FreeGroup α) (FreeGroup β)
hg : ∀ (x : α), (g : (a : FreeGroup α) → FreeGroup β) (FreeGroup.of x) = FreeGroup.of (f x)
x_1 : FreeGroup α
L : List (α × Bool)
x_2 : α × Bool
t : List (α × Bool)
ih :
  Eq.{v + 1} (α := FreeGroup β) ((g : (a : FreeGroup α) → FreeGroup β) (FreeGroup.mk t) : FreeGroup β)
    ((map f : (a : FreeGroup α) → FreeGroup β) (FreeGroup.mk t) : FreeGroup β)
x : α
b : Bool
⊢ Eq.{v + 1} (α := FreeGroup β)
    ((g : (a : FreeGroup α) → FreeGroup β) ((FreeGroup.of x)⁻¹ * FreeGroup.mk t) : FreeGroup β)
    ((map f : (a : FreeGroup α) → FreeGroup β) ((FreeGroup.of x)⁻¹ * FreeGroup.mk t) : FreeGroup β)

Tactic:
simp [g.map_mul, g.map_inv, hg, ih]

Premises used: MonoidHom.map_inv, MonoidHom.map_mul
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
f : α → β
g : MonoidHom.{u, v} (FreeGroup α) (FreeGroup β)
hg : ∀ (x : α), (g : (a : FreeGroup α) → FreeGroup β) (FreeGroup.of x) = FreeGroup.of (f x)
x_1 : FreeGroup α
L : List (α × Bool)
x_2 : α × Bool
t : List (α × Bool)
ih :
  Eq.{v + 1} (α := FreeGroup β) ((g : (a : FreeGroup α) → FreeGroup β) (FreeGroup.mk t) : FreeGroup β)
    ((map f : (a : FreeGroup α) → FreeGroup β) (FreeGroup.mk t) : FreeGroup β)
x : α
b : Bool
⊢ Eq.{v + 1} (α := FreeGroup β) ((g : (a : FreeGroup α) → FreeGroup β) (FreeGroup.of x * FreeGroup.mk t) : FreeGroup β)
    ((map f : (a : FreeGroup α) → FreeGroup β) (FreeGroup.of x * FreeGroup.mk t) : FreeGroup β)

Tactic:
simp [g.map_mul, hg, ih]

Premises used: MonoidHom.map_mul
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
f : α → β
g : MonoidHom.{u, v} (FreeGroup α) (FreeGroup β)
hg : ∀ (x : α), (g : (a : FreeGroup α) → FreeGroup β) (FreeGroup.of x) = FreeGroup.of (f x)
x : FreeGroup α
L : List (α × Bool)
⊢ Eq.{v + 1} (α := FreeGroup β) ((g : (a : FreeGroup α) → FreeGroup β) (Quot.mk Red.Step L) : FreeGroup β)
    ((map f : (a : FreeGroup α) → FreeGroup β) (Quot.mk Red.Step L) : FreeGroup β)

Tactic:
exact List.recOn L g.map_one fun ⟨x, b⟩ t (ih : g (FreeGroup.mk t) = map f (FreeGroup.mk t)) =>
    Bool.recOn b
      (show g ((FreeGroup.of x)⁻¹ * FreeGroup.mk t) =
          FreeGroup.map f ((FreeGroup.of x)⁻¹ * FreeGroup.mk t) by
        simp [g.map_mul, g.map_inv, hg, ih])
      (show g (FreeGroup.of x * FreeGroup.mk t) =
          FreeGroup.map f (FreeGroup.of x * FreeGroup.mk t) by simp [g.map_mul, hg, ih])
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
f : α → β
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 β)
⊢ map f = (lift : (a : α → FreeGroup β) → FreeGroup α →* FreeGroup β) (of ∘ f)

Tactic:
ext
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
f : α → β
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:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
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))
rw₂ rw₃ : Eq (α := Subgroup (FreeGroup β)) (Subgroup.closure (of '' Set.range f)) (Subgroup.closure (of '' Set.range f))
⊢ (map f).range = Subgroup.closure (of '' Set.range f)

Tactic:
rw [map_eq_lift, range_lift_eq_closure, Set.range_comp]

Premises used: Set.range_comp, FreeGroup.range_lift_eq_closure, FreeGroup.map_eq_lift
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
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)) ⊤
rw₄ rw₅ : Eq.{v + 1} (α := Subgroup (FreeGroup β)) ⊤ ⊤
⊢ Function.Surjective.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)

Tactic:
rw [← MonoidHom.range_eq_top, range_map, hf.range_eq, Set.image_univ, closure_range_of]

Premises used: Set.image_univ, FreeGroup.closure_range_of, FreeGroup.range_map, Function.Surjective.range_eq, MonoidHom.range_eq_top
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
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 β)
neg :
  ∀ (h : Nonempty α),
    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 β)

Tactic:
by_cases! h : IsEmpty α

Premises used: IsEmpty
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
h : IsEmpty α
⊢ Function.Injective.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)

Tactic:
Function.injective_of_subsingleton _

Premises used: Function.injective_of_subsingleton
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
h : IsEmpty α
⊢ Function.Injective.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)

Tactic:
exact Function.injective_of_subsingleton _

Premises used: Function.injective_of_subsingleton
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
h : Nonempty α
neg :
  Function.HasLeftInverse.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β)
    (⇑(map f) : (a : FreeGroup α) → FreeGroup β)
⊢ Function.Injective.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)

Tactic:
rw [Function.injective_iff_hasLeftInverse]

Premises used: Function.injective_iff_hasLeftInverse
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
h : Nonempty α
h₁ :
  Function.LeftInverse.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β)
    (⇑(map (Function.invFun f)) : (a : FreeGroup β) → FreeGroup α) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)
⊢ Function.HasLeftInverse.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β)
    (⇑(map f) : (a : FreeGroup α) → FreeGroup β)

Tactic:
use map (Function.invFun f)

Premises used: Function.invFun, FreeGroup.map
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
h : Nonempty α
⊢ Function.LeftInverse.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β)
    (⇑(map (Function.invFun f)) : (a : FreeGroup β) → FreeGroup α) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)

Tactic:
simp [Function.LeftInverse, map.comp, Function.invFun_comp hf]

Premises used: Function.LeftInverse, Function.invFun_comp, FreeGroup.map.comp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
f : α → β
hf : Function.Bijective f
⊢ Function.Bijective.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)

Tactic:
⟨map_injective hf.injective, map_surjective hf.surjective⟩

Premises used: FreeGroup.map_injective, Function.Bijective.injective, Function.Bijective.surjective, And.intro, Function.Bijective, FreeGroup.map_surjective
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
f : α → β
hf : Function.Bijective f
⊢ Function.Bijective.{u + 1, v + 1} (α := FreeGroup α) (β := FreeGroup β) (⇑(map f) : (a : FreeGroup α) → FreeGroup β)

Tactic:
exact ⟨map_injective hf.injective, map_surjective hf.surjective⟩
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α_1 : Type u
L L₁ L₂ L₃ L₄ : List (α_1 × Bool)
β_1 : Type v
f : α_1 → β_1
x_1 y : FreeGroup α_1
α : Type u_1
β : Type u_2
e : α ≃ β
x : FreeGroup α
⊢ (map (⇑e.symm : (a : β) → α) : (a : FreeGroup β) → FreeGroup α)
      ((map (⇑e : (a : α) → β) : (a : FreeGroup α) → FreeGroup β) x) =
    x

Tactic:
simp [map.comp]

Premises used: FreeGroup.map.comp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α_1 : Type u
L L₁ L₂ L₃ L₄ : List (α_1 × Bool)
β_1 : Type v
f : α_1 → β_1
x_1 y : FreeGroup α_1
α : Type u_1
β : Type u_2
e : α ≃ β
x : FreeGroup β
⊢ (map (⇑e : (a : α) → β) : (a : FreeGroup α) → FreeGroup β)
      ((map (⇑e.symm : (a : β) → α) : (a : FreeGroup β) → FreeGroup α) x) =
    x

Tactic:
simp [map.comp]

Premises used: FreeGroup.map.comp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
⊢ freeGroupCongr (Equiv.refl α) = MulEquiv.refl (FreeGroup α)

Tactic:
MulEquiv.ext map.id

Premises used: FreeGroup.map.id, MulEquiv.ext
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
⊢ (freeGroupCongr e).symm = freeGroupCongr e.symm

Tactic:
rfl

Premises used: FreeGroup.freeGroupCongr, Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
f : β ≃ γ
⊢ (freeGroupCongr e).trans (freeGroupCongr f) = freeGroupCongr (e.trans f)

Tactic:
MulEquiv.ext <| map.comp _ _

Premises used: FreeGroup.map.comp, MulEquiv.ext
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
inst : Group α
⊢ Eq (α := α) ((prod : (a : FreeGroup α) → α) (mk L) : α)
    (List.prod (List.map (fun (x : α × Bool) ↦ bif x.2 then x.1 else x.1⁻¹) L) : α)

Tactic:
rfl

Premises used: FreeGroup.Lift.aux, rfl, List.prod
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
inst : Group α
x : α
⊢ (prod : (a : FreeGroup α) → α) (FreeGroup.of x) = x

Tactic:
lift_apply_of

Premises used: FreeGroup.lift_apply_of
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
inst : Group α
g : FreeGroup α →* α
hg : ∀ (x : α), (g : (a : FreeGroup α) → α) (FreeGroup.of x) = x
x : FreeGroup α
⊢ Eq (α := α) ((g : (a : FreeGroup α) → α) x : α) ((prod : (a : FreeGroup α) → α) x : α)

Tactic:
lift_unique g hg

Premises used: FreeGroup.lift_unique
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
β : Type v
inst : Group β
f : α → β
x : FreeGroup α
⊢ ∀ (x : α), (MonoidHom.comp prod (map f) : (a : FreeGroup α) → β) (of x) = f x

Tactic:
simp
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
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 β) : β)
rw₂ rw₃ :
  Eq.{v + 1} (α := β) ((prod : (a : FreeGroup β) → β) ((map f : (a : FreeGroup α) → FreeGroup β) x : FreeGroup β) : β)
    ((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 β) : β)

Tactic:
rw [← lift_unique (prod.comp (map f)) (by simp), MonoidHom.coe_comp, Function.comp_apply]

Premises used: MonoidHom.coe_comp, FreeGroup.prod, FreeGroup.lift_unique, MonoidHom.comp, FreeGroup.map, Function.comp_apply
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L : List (α × Bool)
inst : AddGroup α
⊢ (mk L).sum = List.sum (List.map (fun (x : α × Bool) ↦ bif x.2 then x.1 else -x.1) L)

Tactic:
rfl

Premises used: List.sum, FreeGroup.Lift.aux, Multiplicative, FreeGroup.sum, rfl, List.prod
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
inst : AddGroup α
x : α
⊢ (FreeGroup.of x).sum = x

Tactic:
@prod.of _ (_) _

Premises used: FreeGroup.prod.of, Multiplicative, FreeGroup.sum
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
inst : AddGroup α
x y : FreeGroup α
⊢ (x * y).sum = x.sum + y.sum

Tactic:
(@prod (Multiplicative _) _).map_mul _ _

Premises used: FreeGroup.prod, Multiplicative, FreeGroup.sum, MonoidHom.map_mul
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
inst : AddGroup α
⊢ Eq.{u + 1} (α := α) (sum 1) 0

Tactic:
(@prod (Multiplicative _) _).map_one

Premises used: FreeGroup.prod, Multiplicative, MonoidHom.map_one, FreeGroup.sum
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
inst : AddGroup α
x : FreeGroup α
⊢ x⁻¹.sum = -x.sum

Tactic:
(prod : FreeGroup (Multiplicative α) →* Multiplicative α).map_inv _

Premises used: FreeGroup.prod, Multiplicative, MonoidHom.map_inv, FreeGroup.sum
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : FreeGroup Unit
revert : (x : FreeGroup Unit) → FreeGroup ℤ
⊢ FreeGroup ℤ

Tactic:
revert x
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ (x : FreeGroup Unit) → FreeGroup ℤ

Tactic:
exact ↑(map fun _ => (1 : ℤ))

Premises used: FreeGroup.map, OfNat.ofNat
-- Module: Mathlib.GroupTheory.FreeGroup.Basic
Goal:
α : Type u
L_1 L₁ L₂ L₃ L₄ : List (α × Bool)
x : FreeGroup Unit
L : List (Unit × Bool)
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)) =
    FreeGroup.mk L
⊢ 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)

Tactic:
simp only [quot_mk_eq_mk, map.mk, sum_mk, List.map_map]

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

Tactic:
rfl