case intro.mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
⊢ ↑(↑lift f) (Quot.mk Red.Step L) ∈ s
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
s : Subgroup β
H : Set.range f ⊆ ↑s
⊢ MonoidHom.range (↑lift f) ≤ s
rintro _ ⟨⟨L⟩, rfl⟩
no goals
case intro.mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
⊢ ↑(↑lift f) (Quot.mk Red.Step L) ∈ s
exact
  List.recOn L s.one_mem fun ⟨x, b⟩ tl ih =>
    Bool.recOn b (by simp at ih⊢; exact s.mul_mem (s.inv_mem <| H ⟨x, rfl⟩) ih)
      (by simp at ih⊢; exact s.mul_mem (H ⟨x, rfl⟩) ih)
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x✝¹ y : FreeGroup α
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
tl : List (α × Bool)
ih : List.prod (List.map (fun x => bif x.snd then f x.fst else (f x.fst)⁻¹) tl) ∈ s
x : α
b : Bool
⊢ (f x)⁻¹ * List.prod (List.map (fun x => bif x.snd then f x.fst else (f x.fst)⁻¹) tl) ∈ s
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x✝¹ y : FreeGroup α
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
tl : List (α × Bool)
ih : ↑(↑lift f) (Quot.mk Red.Step tl) ∈ s
x : α
b : Bool
⊢ ↑(↑lift f) (Quot.mk Red.Step ((x, false) :: tl)) ∈ s
simp at ih⊢
no goals
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x✝¹ y : FreeGroup α
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
tl : List (α × Bool)
ih : List.prod (List.map (fun x => bif x.snd then f x.fst else (f x.fst)⁻¹) tl) ∈ s
x : α
b : Bool
⊢ (f x)⁻¹ * List.prod (List.map (fun x => bif x.snd then f x.fst else (f x.fst)⁻¹) tl) ∈ s
exact s.mul_mem (s.inv_mem <| H ⟨x, rfl⟩) ih
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x✝¹ y : FreeGroup α
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
tl : List (α × Bool)
ih : List.prod (List.map (fun x => bif x.snd then f x.fst else (f x.fst)⁻¹) tl) ∈ s
x : α
b : Bool
⊢ f x * List.prod (List.map (fun x => bif x.snd then f x.fst else (f x.fst)⁻¹) tl) ∈ s
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x✝¹ y : FreeGroup α
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
tl : List (α × Bool)
ih : ↑(↑lift f) (Quot.mk Red.Step tl) ∈ s
x : α
b : Bool
⊢ ↑(↑lift f) (Quot.mk Red.Step ((x, true) :: tl)) ∈ s
simp at ih⊢
no goals
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x✝¹ y : FreeGroup α
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
tl : List (α × Bool)
ih : List.prod (List.map (fun x => bif x.snd then f x.fst else (f x.fst)⁻¹) tl) ∈ s
x : α
b : Bool
⊢ f x * List.prod (List.map (fun x => bif x.snd then f x.fst else (f x.fst)⁻¹) tl) ∈ s
exact s.mul_mem (H ⟨x, rfl⟩) ih