case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y : FreeGroup α
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), ↑g (FreeGroup.of x) = FreeGroup.of (f x)
x✝ : FreeGroup α
L : List (α × Bool)
⊢ ↑g (Quot.mk Red.Step L) = ↑(map f) (Quot.mk Red.Step L)
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y : FreeGroup α
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), ↑g (FreeGroup.of x) = FreeGroup.of (f x)
⊢ ∀ {x : FreeGroup α}, ↑g x = ↑(map f) x
rintro ⟨L⟩
no goals
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y : FreeGroup α
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), ↑g (FreeGroup.of x) = FreeGroup.of (f x)
x✝ : FreeGroup α
L : List (α × Bool)
⊢ ↑g (Quot.mk Red.Step L) = ↑(map f) (Quot.mk Red.Step L)
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])
no goals
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x✝² y : FreeGroup α
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), ↑g (FreeGroup.of x) = FreeGroup.of (f x)
x✝¹ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
t : List (α × Bool)
ih : ↑g (FreeGroup.mk t) = ↑(map f) (FreeGroup.mk t)
x : α
b : Bool
⊢ ↑g ((FreeGroup.of x)⁻¹ * FreeGroup.mk t) = ↑(map f) ((FreeGroup.of x)⁻¹ * FreeGroup.mk t)
simp [g.map_mul, g.map_inv, hg, ih]
no goals
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x✝² y : FreeGroup α
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), ↑g (FreeGroup.of x) = FreeGroup.of (f x)
x✝¹ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
t : List (α × Bool)
ih : ↑g (FreeGroup.mk t) = ↑(map f) (FreeGroup.mk t)
x : α
b : Bool
⊢ ↑g (FreeGroup.of x * FreeGroup.mk t) = ↑(map f) (FreeGroup.of x * FreeGroup.mk t)
simp [g.map_mul, hg, ih]