Congruence.lean

theorem mem_normalClosure_of_subset
    (hR_to_S : R ⊆ S) {x : G}
    (hx : x ∈ Subgroup.normalClosure R) :
    x ∈ Subgroup.normalClosure S

theorem mem_normalClosure_union_left
    {x : G} (hx : x ∈ Subgroup.normalClosure R) :
    x ∈ Subgroup.normalClosure (R ∪ S)

theorem mem_normalClosure_union_right
    {x : G} (hx : x ∈ Subgroup.normalClosure S) :
    x ∈ Subgroup.normalClosure (R ∪ S)

theorem mem_normalClosure_iUnion
    {ι : Sort*} (R : ι → Set G) (i : ι)
    {x : G} (hx : x ∈ Subgroup.normalClosure (R i)) :
    x ∈ Subgroup.normalClosure (Set.iUnion R)

theorem mem_normalClosure_iUnion₂
    {ι : Sort*} {κ : ι → Sort*}
    (R : ∀ i : ι, κ i → Set G) (i : ι) (j : κ i)
    {x : G} (hx : x ∈ Subgroup.normalClosure (R i j)) :
    x ∈ Subgroup.normalClosure
        (Set.iUnion fun i : ι => Set.iUnion (R i)) :=
  mem_normalClosure_of_subset
    (R := R i j)
    (S := Set.iUnion fun i : ι => Set.iUnion (R i))
    (fun _ hy => Set.mem_iUnion.2 ⟨i, Set.mem_iUnion.2 ⟨j, hy⟩⟩) hx

theorem mem_normalClosure_iUnion₂_of_exists
    {ι : Sort*} {κ : ι → Sort*}
    (R : ∀ i : ι, κ i → Set G)
    {x : G} (hx : ∃ i : ι, ∃ j : κ i,
      x ∈ Subgroup.normalClosure (R i j)) :
    x ∈ Subgroup.normalClosure
        (Set.iUnion fun i : ι => Set.iUnion (R i)) := by
  rcases hx with ⟨i, j, hij⟩
  exact mem_normalClosure_iUnion₂ (R := R) i j hij

theorem maps_iUnion_relators_mem_normalClosure
    {ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
    (hR : ∀ i : ι, ∀ r ∈ R i, f r ∈ Subgroup.normalClosure S) :
    ∀ r ∈ Set.iUnion R, f r ∈ Subgroup.normalClosure S

theorem maps_iUnion₂_relators_mem_normalClosure
    {ι : Sort*} {κ : ι → Sort*}
    (f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
    (hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
      f r ∈ Subgroup.normalClosure S) :
    ∀ r ∈ Set.iUnion (fun i : ι => Set.iUnion (R i)),
      f r ∈ Subgroup.normalClosure S := by
  intro r hr
  rcases Set.mem_iUnion.1 hr with ⟨i, hi⟩
  rcases Set.mem_iUnion.1 hi with ⟨j, hj⟩
  exact hR i j r hj

theorem map_mem_normalClosure_of_relators
    (f : G →* H) {R : Set G} {S : Set H}
    (hR : ∀ r ∈ R, f r ∈ Subgroup.normalClosure S)
    {x : G} (hx : x ∈ Subgroup.normalClosure R) :
    f x ∈ Subgroup.normalClosure S

theorem hom_relatorEquivalent_of_maps_relators
    (f : G →* H) {R : Set G} {S : Set H}
    (hR : ∀ r ∈ R, f r ∈ Subgroup.normalClosure S)
    {u v : G} (h : RelatorEquivalent R u v) :
    RelatorEquivalent S (f u) (f v)

theorem hom_relatorEquivalent_of_maps_relators_relatorEquivalent
    (f : G →* H) {R : Set G} {S : Set H}
    (hR : ∀ r ∈ R, RelatorEquivalent S (f r) 1)
    {u v : G} (h : RelatorEquivalent R u v) :
    RelatorEquivalent S (f u) (f v)

theorem map_mem_normalClosure_iUnion_of_relators
    {ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
    (hR : ∀ i : ι, ∀ r ∈ R i, f r ∈ Subgroup.normalClosure S)
    {x : G} (hx : x ∈ Subgroup.normalClosure (Set.iUnion R)) :
    f x ∈ Subgroup.normalClosure S

theorem map_mem_normalClosure_iUnion₂_of_relators
    {ι : Sort*} {κ : ι → Sort*}
    (f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
    (hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
      f r ∈ Subgroup.normalClosure S)
    {x : G}
    (hx : x ∈ Subgroup.normalClosure
      (Set.iUnion fun i : ι => Set.iUnion (R i))) :
    f x ∈ Subgroup.normalClosure S :=
  map_mem_normalClosure_of_relators f
    (maps_iUnion₂_relators_mem_normalClosure f hR) hx

theorem hom_relatorEquivalent_of_maps_iUnion_relators
    {ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
    (hR : ∀ i : ι, ∀ r ∈ R i, f r ∈ Subgroup.normalClosure S)
    {u v : G} (h : RelatorEquivalent (Set.iUnion R) u v) :
    RelatorEquivalent S (f u) (f v)

theorem hom_relatorEquivalent_of_maps_iUnion_relators_relatorEquivalent
    {ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
    (hR : ∀ i : ι, ∀ r ∈ R i, RelatorEquivalent S (f r) 1)
    {u v : G} (h : RelatorEquivalent (Set.iUnion R) u v) :
    RelatorEquivalent S (f u) (f v)

theorem hom_relatorEquivalent_of_maps_iUnion₂_relators
    {ι : Sort*} {κ : ι → Sort*}
    (f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
    (hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
      f r ∈ Subgroup.normalClosure S)
    {u v : G}
    (h : RelatorEquivalent
      (Set.iUnion fun i : ι => Set.iUnion (R i)) u v) :
    RelatorEquivalent S (f u) (f v) :=
  hom_relatorEquivalent_of_maps_relators f
    (maps_iUnion₂_relators_mem_normalClosure f hR) h

theorem hom_relatorEquivalent_of_maps_iUnion₂_relators_relatorEquivalent
    {ι : Sort*} {κ : ι → Sort*}
    (f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
    (hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
      RelatorEquivalent S (f r) 1)
    {u v : G}
    (h : RelatorEquivalent
      (Set.iUnion fun i : ι => Set.iUnion (R i)) u v) :
    RelatorEquivalent S (f u) (f v) :=
  hom_relatorEquivalent_of_maps_iUnion₂_relators f
    (fun i j r hr => RelatorEquivalent.mem_normalClosure_of_eq_one (hR i j r hr)) h