[GOAL]
α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ optionCongr (swap x y) = swap (some x) (some y)
[PROOFSTEP]
ext (_ | i)
[GOAL]
case H.none.a
α : Type u_1
inst✝ : DecidableEq α
x y a✝ : α
⊢ a✝ ∈ ↑(optionCongr (swap x y)) none ↔ a✝ ∈ ↑(swap (some x) (some y)) none
[PROOFSTEP]
simp [swap_apply_of_ne_of_ne]
[GOAL]
case H.some.a
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
⊢ a✝ ∈ ↑(optionCongr (swap x y)) (some i) ↔ a✝ ∈ ↑(swap (some x) (some y)) (some i)
[PROOFSTEP]
by_cases hx : i = x
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : i = x
⊢ a✝ ∈ ↑(optionCongr (swap x y)) (some i) ↔ a✝ ∈ ↑(swap (some x) (some y)) (some i)
case neg
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : ¬i = x
⊢ a✝ ∈ ↑(optionCongr (swap x y)) (some i) ↔ a✝ ∈ ↑(swap (some x) (some y)) (some i)
[PROOFSTEP]
simp [hx, swap_apply_of_ne_of_ne]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : ¬i = x
⊢ a✝ ∈ ↑(optionCongr (swap x y)) (some i) ↔ a✝ ∈ ↑(swap (some x) (some y)) (some i)
[PROOFSTEP]
by_cases hy : i = y
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : ¬i = x
hy : i = y
⊢ a✝ ∈ ↑(optionCongr (swap x y)) (some i) ↔ a✝ ∈ ↑(swap (some x) (some y)) (some i)
[PROOFSTEP]
simp [hx, hy, swap_apply_of_ne_of_ne]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : ¬i = x
hy : ¬i = y
⊢ a✝ ∈ ↑(optionCongr (swap x y)) (some i) ↔ a✝ ∈ ↑(swap (some x) (some y)) (some i)
[PROOFSTEP]
simp [hx, hy, swap_apply_of_ne_of_ne]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ ↑Perm.sign (optionCongr e) = ↑Perm.sign e
[PROOFSTEP]
refine Perm.swap_induction_on e ?_ ?_
[GOAL]
case refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ ↑Perm.sign (optionCongr 1) = ↑Perm.sign 1
[PROOFSTEP]
simp [Perm.one_def]
[GOAL]
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ ∀ (f : Perm α) (x y : α),
    x ≠ y →
      ↑Perm.sign (optionCongr f) = ↑Perm.sign f → ↑Perm.sign (optionCongr (swap x y * f)) = ↑Perm.sign (swap x y * f)
[PROOFSTEP]
intro f x y hne h
[GOAL]
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e f : Perm α
x y : α
hne : x ≠ y
h : ↑Perm.sign (optionCongr f) = ↑Perm.sign f
⊢ ↑Perm.sign (optionCongr (swap x y * f)) = ↑Perm.sign (swap x y * f)
[PROOFSTEP]
simp [h, hne, Perm.mul_def, ← Equiv.optionCongr_trans]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
⊢ optionCongr (removeNone σ) = swap none (↑σ none) * σ
[PROOFSTEP]
ext1 x
[GOAL]
case H
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : Option α
⊢ ↑(optionCongr (removeNone σ)) x = ↑(swap none (↑σ none) * σ) x
[PROOFSTEP]
have : Option.map (⇑(removeNone σ)) x = (swap none (σ none)) (σ x) :=
  by
  cases' x with x
  · simp
  · cases h : σ (some _)
    · simp [removeNone_none _ h]
    · have hn : σ (some x) ≠ none := by simp [h]
      have hσn : σ (some x) ≠ σ none := σ.injective.ne (by simp)
      simp [removeNone_some _ ⟨_, h⟩, ← h, swap_apply_of_ne_of_ne hn hσn]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : Option α
⊢ Option.map (↑(removeNone σ)) x = ↑(swap none (↑σ none)) (↑σ x)
[PROOFSTEP]
cases' x with x
[GOAL]
case none
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
⊢ Option.map (↑(removeNone σ)) none = ↑(swap none (↑σ none)) (↑σ none)
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : α
⊢ Option.map (↑(removeNone σ)) (some x) = ↑(swap none (↑σ none)) (↑σ (some x))
[PROOFSTEP]
cases h : σ (some _)
[GOAL]
case some.none
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : α
h : ↑σ (some x) = none
⊢ Option.map (↑(removeNone σ)) (some x) = ↑(swap none (↑σ none)) none
[PROOFSTEP]
simp [removeNone_none _ h]
[GOAL]
case some.some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : ↑σ (some x) = some val✝
⊢ Option.map (↑(removeNone σ)) (some x) = ↑(swap none (↑σ none)) (some val✝)
[PROOFSTEP]
have hn : σ (some x) ≠ none := by simp [h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : ↑σ (some x) = some val✝
⊢ ↑σ (some x) ≠ none
[PROOFSTEP]
simp [h]
[GOAL]
case some.some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : ↑σ (some x) = some val✝
hn : ↑σ (some x) ≠ none
⊢ Option.map (↑(removeNone σ)) (some x) = ↑(swap none (↑σ none)) (some val✝)
[PROOFSTEP]
have hσn : σ (some x) ≠ σ none := σ.injective.ne (by simp)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : ↑σ (some x) = some val✝
hn : ↑σ (some x) ≠ none
⊢ some x ≠ none
[PROOFSTEP]
simp
[GOAL]
case some.some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : ↑σ (some x) = some val✝
hn : ↑σ (some x) ≠ none
hσn : ↑σ (some x) ≠ ↑σ none
⊢ Option.map (↑(removeNone σ)) (some x) = ↑(swap none (↑σ none)) (some val✝)
[PROOFSTEP]
simp [removeNone_some _ ⟨_, h⟩, ← h, swap_apply_of_ne_of_ne hn hσn]
[GOAL]
case H
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : Option α
this : Option.map (↑(removeNone σ)) x = ↑(swap none (↑σ none)) (↑σ x)
⊢ ↑(optionCongr (removeNone σ)) x = ↑(swap none (↑σ none) * σ) x
[PROOFSTEP]
simpa using this
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
⊢ (fun i => swap none i.fst * optionCongr i.snd) ((fun σ => (↑σ none, removeNone σ)) σ) = σ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
x✝ : Option α × Perm α
x : Option α
σ : Perm α
⊢ (fun σ => (↑σ none, removeNone σ)) ((fun i => swap none i.fst * optionCongr i.snd) (x, σ)) = (x, σ)
[PROOFSTEP]
have : removeNone (swap none x * σ.optionCongr) = σ := Equiv.optionCongr_injective (by simp [← mul_assoc])
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
x✝ : Option α × Perm α
x : Option α
σ : Perm α
⊢ optionCongr (removeNone (swap none x * optionCongr σ)) = optionCongr σ
[PROOFSTEP]
simp [← mul_assoc]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
x✝ : Option α × Perm α
x : Option α
σ : Perm α
this : removeNone (swap none x * optionCongr σ) = σ
⊢ (fun σ => (↑σ none, removeNone σ)) ((fun i => swap none i.fst * optionCongr i.snd) (x, σ)) = (x, σ)
[PROOFSTEP]
simp [← Perm.eq_inv_iff_eq, this]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
e : Perm α
i : Option α
⊢ ↑(↑decomposeOption.symm (none, e)) i = Option.map (↑e) i
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ ↑sign (↑decomposeOption.symm (none, e)) = ↑sign e
[PROOFSTEP]
simp


[GOAL]
α : Type u_1
inst✝ : Semigroup α
s : Set α
a b : α
⊢ a *l (b *l s) = a * b *l s
[PROOFSTEP]
simp [leftCoset, rightCoset, (image_comp _ _ _).symm, Function.comp, mul_assoc]
[GOAL]
α : Type u_1
inst✝ : Semigroup α
s : Set α
a b : α
⊢ s *r a *r b = s *r (a * b)
[PROOFSTEP]
simp [leftCoset, rightCoset, (image_comp _ _ _).symm, Function.comp, mul_assoc]
[GOAL]
α : Type u_1
inst✝ : Semigroup α
s : Set α
a b : α
⊢ a *l s *r b = a *l (s *r b)
[PROOFSTEP]
simp [leftCoset, rightCoset, (image_comp _ _ _).symm, Function.comp, mul_assoc]
[GOAL]
α : Type u_1
inst✝ : Monoid α
s : Set α
⊢ ∀ (x : α), x ∈ 1 *l s ↔ x ∈ s
[PROOFSTEP]
simp [leftCoset]
[GOAL]
α : Type u_1
inst✝ : Monoid α
s : Set α
⊢ ∀ (x : α), x ∈ s *r 1 ↔ x ∈ s
[PROOFSTEP]
simp [rightCoset]
[GOAL]
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
this : a * 1 ∈ a *l ↑s
⊢ a ∈ a *l ↑s
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
this : 1 * a ∈ ↑s *r a
⊢ a ∈ ↑s *r a
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a *l ↑s = ↑s
⊢ a ∈ s
[PROOFSTEP]
rw [← SetLike.mem_coe, ← ha]
[GOAL]
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a *l ↑s = ↑s
⊢ a ∈ a *l ↑s
[PROOFSTEP]
exact mem_own_leftCoset s a
[GOAL]
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : ↑s *r a = ↑s
⊢ a ∈ s
[PROOFSTEP]
rw [← SetLike.mem_coe, ← ha]
[GOAL]
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : ↑s *r a = ↑s
⊢ a ∈ ↑s *r a
[PROOFSTEP]
exact mem_own_rightCoset s a
[GOAL]
α : Type u_1
inst✝ : Group α
s : Set α
x a : α
x✝ : x ∈ a *l s
b : α
hb : b ∈ s
Eq : (fun x => a * x) b = x
⊢ a⁻¹ * x ∈ s
[PROOFSTEP]
simp [Eq.symm, hb]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Set α
x a : α
h : a⁻¹ * x ∈ s
⊢ (fun x => a * x) (a⁻¹ * x) = x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Group α
s : Set α
x a : α
x✝ : x ∈ s *r a
b : α
hb : b ∈ s
Eq : (fun x => x * a) b = x
⊢ x * a⁻¹ ∈ s
[PROOFSTEP]
simp [Eq.symm, hb]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Set α
x a : α
h : x * a⁻¹ ∈ s
⊢ (fun x => x * a) (x * a⁻¹) = x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
⊢ ∀ (x : α), x ∈ a *l ↑s ↔ x ∈ ↑s
[PROOFSTEP]
simp [mem_leftCoset_iff, mul_mem_cancel_left (s.inv_mem ha)]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
b : α
⊢ b ∈ ↑s *r a ↔ b ∈ ↑s
[PROOFSTEP]
simp [mem_rightCoset_iff, mul_mem_cancel_right (s.inv_mem ha)]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
N : Normal s
g a : α
⊢ a ∈ g *l ↑s ↔ a ∈ ↑s *r g
[PROOFSTEP]
simp [mem_leftCoset_iff, mem_rightCoset_iff]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
N : Normal s
g a : α
⊢ g⁻¹ * a ∈ s ↔ a * g⁻¹ ∈ s
[PROOFSTEP]
rw [N.mem_comm_iff]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
h : ∀ (g : α), g *l ↑s = ↑s *r g
a : α
ha : a ∈ s
g : α
⊢ g * a * g⁻¹ ∈ ↑s
[PROOFSTEP]
rw [← mem_rightCoset_iff, ← h]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
h : ∀ (g : α), g *l ↑s = ↑s *r g
a : α
ha : a ∈ s
g : α
⊢ g * a ∈ g *l ↑s
[PROOFSTEP]
exact mem_leftCoset g ha
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ x *l ↑s = y *l ↑s ↔ x⁻¹ * y ∈ s
[PROOFSTEP]
rw [Set.ext_iff]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 ∈ x *l ↑s ↔ x_1 ∈ y *l ↑s) ↔ x⁻¹ * y ∈ s
[PROOFSTEP]
simp_rw [mem_leftCoset_iff, SetLike.mem_coe]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) ↔ x⁻¹ * y ∈ s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ s
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
⊢ x⁻¹ * y ∈ s
[PROOFSTEP]
apply (h y).mpr
[GOAL]
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
⊢ y⁻¹ * y ∈ s
[PROOFSTEP]
rw [mul_left_inv]
[GOAL]
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
⊢ 1 ∈ s
[PROOFSTEP]
exact s.one_mem
[GOAL]
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ x⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
[PROOFSTEP]
intro h z
[GOAL]
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s
[PROOFSTEP]
rw [← mul_inv_cancel_right x⁻¹ y]
[GOAL]
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * y⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * (y⁻¹ * z) ∈ s ↔ y⁻¹ * z ∈ s
[PROOFSTEP]
exact s.mul_mem_cancel_left h
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ ↑s *r x = ↑s *r y ↔ y * x⁻¹ ∈ s
[PROOFSTEP]
rw [Set.ext_iff]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 ∈ ↑s *r x ↔ x_1 ∈ ↑s *r y) ↔ y * x⁻¹ ∈ s
[PROOFSTEP]
simp_rw [mem_rightCoset_iff, SetLike.mem_coe]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) ↔ y * x⁻¹ ∈ s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ s
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ y * x⁻¹ ∈ s
[PROOFSTEP]
apply (h y).mpr
[GOAL]
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ y * y⁻¹ ∈ s
[PROOFSTEP]
rw [mul_right_inv]
[GOAL]
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ 1 ∈ s
[PROOFSTEP]
exact s.one_mem
[GOAL]
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ y * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
[PROOFSTEP]
intro h z
[GOAL]
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * x⁻¹ ∈ s ↔ z * y⁻¹ ∈ s
[PROOFSTEP]
rw [← inv_mul_cancel_left y x⁻¹]
[GOAL]
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * (y⁻¹ * (y * x⁻¹)) ∈ s ↔ z * y⁻¹ ∈ s
[PROOFSTEP]
rw [← mul_assoc]
[GOAL]
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * y⁻¹ * (y * x⁻¹) ∈ s ↔ z * y⁻¹ ∈ s
[PROOFSTEP]
exact s.mul_mem_cancel_right h
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, y * ↑a = x) ↔ ∃ a, x⁻¹ * y = ↑a⁻¹
[PROOFSTEP]
simp only [inv_mul_eq_iff_eq_mul, Subgroup.coe_inv, eq_mul_inv_iff_mul_eq]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, x⁻¹ * y = ↑a⁻¹) ↔ x⁻¹ * y ∈ s
[PROOFSTEP]
simp [exists_inv_mem_iff_exists_mem]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), Setoid.r a b = (a⁻¹ * b ∈ s)
[PROOFSTEP]
simp only [eq_iff_iff]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), Setoid.r a b ↔ a⁻¹ * b ∈ s
[PROOFSTEP]
apply leftRel_apply
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Setoid.r = LeftCosetEquivalence ↑s
[PROOFSTEP]
ext
[GOAL]
case h.h.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ Setoid.r x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝
[PROOFSTEP]
rw [leftRel_eq]
[GOAL]
case h.h.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (fun x y => x⁻¹ * y ∈ s) x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝
[PROOFSTEP]
exact (leftCoset_eq_iff s).symm
[GOAL]
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x => x ∈ s
x y : α
⊢ Decidable (Setoid.r x y)
[PROOFSTEP]
rw [leftRel_eq]
[GOAL]
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x => x ∈ s
x y : α
⊢ Decidable ((fun x y => x⁻¹ * y ∈ s) x y)
[PROOFSTEP]
exact ‹DecidablePred (· ∈ s)› _
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, ↑a * y = x) ↔ ∃ a, y * x⁻¹ = ↑a⁻¹
[PROOFSTEP]
simp only [mul_inv_eq_iff_eq_mul, Subgroup.coe_inv, eq_inv_mul_iff_mul_eq]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, y * x⁻¹ = ↑a⁻¹) ↔ y * x⁻¹ ∈ s
[PROOFSTEP]
simp [exists_inv_mem_iff_exists_mem]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), Setoid.r a b = (b * a⁻¹ ∈ s)
[PROOFSTEP]
simp only [eq_iff_iff]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), Setoid.r a b ↔ b * a⁻¹ ∈ s
[PROOFSTEP]
apply rightRel_apply
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Setoid.r = RightCosetEquivalence ↑s
[PROOFSTEP]
ext
[GOAL]
case h.h.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ Setoid.r x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝
[PROOFSTEP]
rw [rightRel_eq]
[GOAL]
case h.h.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (fun x y => y * x⁻¹ ∈ s) x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝
[PROOFSTEP]
exact (rightCoset_eq_iff s).symm
[GOAL]
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x => x ∈ s
x y : α
⊢ Decidable (Setoid.r x y)
[PROOFSTEP]
rw [rightRel_eq]
[GOAL]
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x => x ∈ s
x y : α
⊢ Decidable ((fun x y => y * x⁻¹ ∈ s) x y)
[PROOFSTEP]
exact ‹DecidablePred (· ∈ s)› _
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ Setoid.r a b → Setoid.r ((fun g => g⁻¹) a) ((fun g => g⁻¹) b)
[PROOFSTEP]
rw [leftRel_apply, rightRel_apply]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ b * a⁻¹ ∈ s → ((fun g => g⁻¹) a)⁻¹ * (fun g => g⁻¹) b ∈ s
[PROOFSTEP]
exact fun h =>
  (congr_arg (· ∈ s) (by simp [mul_assoc])).mp
    (s.inv_mem h)
      -- porting note: replace with `by group`
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
h : b * a⁻¹ ∈ s
⊢ (b * a⁻¹)⁻¹ = ((fun g => g⁻¹) a)⁻¹ * (fun g => g⁻¹) b
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ Setoid.r a b → Setoid.r ((fun g => g⁻¹) a) ((fun g => g⁻¹) b)
[PROOFSTEP]
rw [leftRel_apply, rightRel_apply]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ a⁻¹ * b ∈ s → (fun g => g⁻¹) b * ((fun g => g⁻¹) a)⁻¹ ∈ s
[PROOFSTEP]
exact fun h =>
  (congr_arg (· ∈ s) (by simp [mul_assoc])).mp
    (s.inv_mem h)
      -- porting note: replace with `by group`
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
h : a⁻¹ * b ∈ s
⊢ (a⁻¹ * b)⁻¹ = (fun g => g⁻¹) b * ((fun g => g⁻¹) a)⁻¹
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : Quotient (rightRel s)
g : α
⊢ Setoid.r ((fun g => g⁻¹) ((fun g => g⁻¹) g)) g
[PROOFSTEP]
simp only [inv_inv]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : Quotient (rightRel s)
g : α
⊢ Setoid.r g g
[PROOFSTEP]
exact Quotient.exact' rfl
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : α ⧸ s
g : α
⊢ Setoid.r ((fun g => g⁻¹) ((fun g => g⁻¹) g)) g
[PROOFSTEP]
simp only [inv_inv]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : α ⧸ s
g : α
⊢ Setoid.r g g
[PROOFSTEP]
exact Quotient.exact' rfl
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ Setoid.r a b ↔ a⁻¹ * b ∈ s
[PROOFSTEP]
rw [leftRel_apply]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
g : α
⊢ Quotient.out' ↑g = g * ↑{ val := g⁻¹ * Quotient.out' ↑g, property := (_ : g⁻¹ * Quotient.out' ↑g ∈ s) }
[PROOFSTEP]
rw [mul_inv_cancel_left]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a✝ b a : α
hb : b ∈ s
⊢ ↑(a * b) = ↑a
[PROOFSTEP]
rwa [eq', mul_inv_rev, inv_mul_cancel_right, s.inv_mem_iff]
[GOAL]
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
s : Subgroup α
g z : α
⊢ z ∈ {x | ↑x = ↑g} ↔ z ∈ g *l ↑s
[PROOFSTEP]
rw [mem_leftCoset_iff, Set.mem_setOf_eq, eq_comm, QuotientGroup.eq, SetLike.mem_coe]
[GOAL]
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
⊢ mk ⁻¹' (mk '' s) = ⋃ (x : { x // x ∈ N }), (fun x_1 => x_1 * ↑x) ⁻¹' s
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
x : α
⊢ x ∈ mk ⁻¹' (mk '' s) ↔ x ∈ ⋃ (x : { x // x ∈ N }), (fun x_1 => x_1 * ↑x) ⁻¹' s
[PROOFSTEP]
simp only [QuotientGroup.eq, SetLike.exists, exists_prop, Set.mem_preimage, Set.mem_iUnion, Set.mem_image, ←
  eq_inv_mul_iff_mul_eq]
[GOAL]
case h
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
x : α
⊢ (∃ x_1, x_1 ∈ s ∧ x_1⁻¹ * x ∈ N) ↔ ∃ x_1, x_1 ∈ N ∧ x * x_1 ∈ s
[PROOFSTEP]
exact ⟨fun ⟨y, hs, hN⟩ => ⟨_, N.inv_mem hN, by simpa using hs⟩, fun ⟨z, hz, hxz⟩ => ⟨x * z, hxz, by simpa using hz⟩⟩
[GOAL]
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
x : α
x✝ : ∃ x_1, x_1 ∈ s ∧ x_1⁻¹ * x ∈ N
y : α
hs : y ∈ s
hN : y⁻¹ * x ∈ N
⊢ x * (y⁻¹ * x)⁻¹ ∈ s
[PROOFSTEP]
simpa using hs
[GOAL]
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
x : α
x✝ : ∃ x_1, x_1 ∈ N ∧ x * x_1 ∈ s
z : α
hz : z ∈ N
hxz : x * z ∈ s
⊢ (x * z)⁻¹ * x ∈ N
[PROOFSTEP]
simpa using hz
[GOAL]
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
⊢ mk ⁻¹' (mk '' s) = ⋃ (x : { x // x ∈ N }), (fun x_1 => x_1 * ↑x) '' s
[PROOFSTEP]
rw [preimage_image_mk, iUnion_congr_of_surjective (·⁻¹) inv_surjective]
[GOAL]
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
⊢ ∀ (x : { x // x ∈ N }), (fun x_1 => x_1 * ↑x⁻¹) '' s = (fun x_1 => x_1 * ↑x) ⁻¹' s
[PROOFSTEP]
exact fun x ↦ image_mul_right'
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
g : α
x✝ : ↑(g *l ↑s)
x : α
hx : x ∈ g *l ↑s
⊢ ↑((fun x => { val := g * ↑x, property := (_ : ∃ a, a ∈ ↑s ∧ (fun x => g * x) a = g * ↑x) })
        ((fun x => { val := g⁻¹ * ↑x, property := (_ : g⁻¹ * ↑x ∈ ↑s) }) { val := x, property := hx })) =
    ↑{ val := x, property := hx }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : α
x✝ : { x // x ∈ s }
g : α
hg : g ∈ s
⊢ ↑((fun x => { val := g✝⁻¹ * ↑x, property := (_ : g✝⁻¹ * ↑x ∈ ↑s) })
        ((fun x => { val := g✝ * ↑x, property := (_ : ∃ a, a ∈ ↑s ∧ (fun x => g✝ * x) a = g✝ * ↑x) })
          { val := g, property := hg })) =
    ↑{ val := g, property := hg }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
g : α
x✝ : ↑(↑s *r g)
x : α
hx : x ∈ ↑s *r g
⊢ ↑((fun x => { val := ↑x * g, property := (_ : ∃ a, a ∈ ↑s ∧ (fun x => x * g) a = ↑x * g) })
        ((fun x => { val := ↑x * g⁻¹, property := (_ : ↑x * g⁻¹ ∈ ↑s) }) { val := x, property := hx })) =
    ↑{ val := x, property := hx }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : α
x✝ : { x // x ∈ s }
g : α
hg : g ∈ s
⊢ ↑((fun x => { val := ↑x * g✝⁻¹, property := (_ : ↑x * g✝⁻¹ ∈ ↑s) })
        ((fun x => { val := ↑x * g✝, property := (_ : ∃ a, a ∈ ↑s ∧ (fun x => x * g✝) a = ↑x * g✝) })
          { val := g, property := hg })) =
    ↑{ val := g, property := hg }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x // ↑x = L } ≃ ↑(Quotient.out' L *l ↑s)
[PROOFSTEP]
rw [← eq_class_eq_leftCoset]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x // ↑x = L } ≃ ↑{x | ↑x = ↑(Quotient.out' L)}
[PROOFSTEP]
show (_root_.Subtype fun x : α => Quotient.mk'' x = L) ≃ _root_.Subtype fun x : α => Quotient.mk'' x = Quotient.mk'' _
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x // Quotient.mk'' x = L } ≃ { x // Quotient.mk'' x = Quotient.mk'' (Quotient.out' L) }
[PROOFSTEP]
simp [-Quotient.eq'']
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x // Quotient.mk'' x = L } ≃ { x // Quotient.mk'' x = L }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : Setoid.r b c
⊢ Setoid.r ((fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) }) b)
    ((fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) }) c)
[PROOFSTEP]
rw [leftRel_apply]
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : Setoid.r b c
⊢ ((fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) }) b)⁻¹ *
      (fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) }) c ∈
    subgroupOf s t
[PROOFSTEP]
change ((f b)⁻¹ * b)⁻¹ * ((f c)⁻¹ * c) ∈ s
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : Setoid.r b c
⊢ ((f ↑b)⁻¹ * b)⁻¹ * ((f ↑c)⁻¹ * c) ∈ s
[PROOFSTEP]
have key : f b = f c := congr_arg f (Quotient.sound' (leftRel_apply.mpr (h_le (leftRel_apply.mp h))))
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : Setoid.r b c
key : f ↑b = f ↑c
⊢ ((f ↑b)⁻¹ * b)⁻¹ * ((f ↑c)⁻¹ * c) ∈ s
[PROOFSTEP]
rwa [key, mul_inv_rev, inv_inv, mul_assoc, mul_inv_cancel_left, ← leftRel_apply]
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : (α ⧸ t) × { x // x ∈ t } ⧸ subgroupOf s t
⊢ α ⧸ s
[PROOFSTEP]
refine
  a.2.map' (fun (b : { x // x ∈ t }) => f a.1 * b) fun b c h =>
    by
    rw [leftRel_apply] at h ⊢
    change (f a.1 * b)⁻¹ * (f a.1 * c) ∈ s
    rwa [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : (α ⧸ t) × { x // x ∈ t } ⧸ subgroupOf s t
b c : { x // x ∈ t }
h : Setoid.r b c
⊢ Setoid.r ((fun b => f a.fst * ↑b) b) ((fun b => f a.fst * ↑b) c)
[PROOFSTEP]
rw [leftRel_apply] at h ⊢
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : (α ⧸ t) × { x // x ∈ t } ⧸ subgroupOf s t
b c : { x // x ∈ t }
h : b⁻¹ * c ∈ subgroupOf s t
⊢ ((fun b => f a.fst * ↑b) b)⁻¹ * (fun b => f a.fst * ↑b) c ∈ s
[PROOFSTEP]
change (f a.1 * b)⁻¹ * (f a.1 * c) ∈ s
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : (α ⧸ t) × { x // x ∈ t } ⧸ subgroupOf s t
b c : { x // x ∈ t }
h : b⁻¹ * c ∈ subgroupOf s t
⊢ (f a.fst * ↑b)⁻¹ * (f a.fst * ↑c) ∈ s
[PROOFSTEP]
rwa [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
⊢ LeftInverse
    (fun a =>
      Quotient.map' (fun b => f a.fst * ↑b)
        (_ : ∀ (b c : { x // x ∈ t }), Setoid.r b c → Setoid.r ((fun b => f a.fst * ↑b) b) ((fun b => f a.fst * ↑b) c))
        a.snd)
    fun a =>
    (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a,
      Quotient.map' (fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
        (_ :
          ∀ (b c : α),
            Setoid.r b c →
              Setoid.r
                ((fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) }) b)
                ((fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                  c))
        a)
[PROOFSTEP]
refine' Quotient.ind' fun a => _
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : α
⊢ (fun a =>
        Quotient.map' (fun b => f a.fst * ↑b)
          (_ :
            ∀ (b c : { x // x ∈ t }), Setoid.r b c → Setoid.r ((fun b => f a.fst * ↑b) b) ((fun b => f a.fst * ↑b) c))
          a.snd)
      ((fun a =>
          (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a,
            Quotient.map'
              (fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
              (_ :
                ∀ (b c : α),
                  Setoid.r b c →
                    Setoid.r
                      ((fun g =>
                          { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                        b)
                      ((fun g =>
                          { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                        c))
              a))
        (Quotient.mk'' a)) =
    Quotient.mk'' a
[PROOFSTEP]
simp_rw [Quotient.map'_mk'', id.def, mul_inv_cancel_left]
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
⊢ Function.RightInverse
    (fun a =>
      Quotient.map' (fun b => f a.fst * ↑b)
        (_ : ∀ (b c : { x // x ∈ t }), Setoid.r b c → Setoid.r ((fun b => f a.fst * ↑b) b) ((fun b => f a.fst * ↑b) c))
        a.snd)
    fun a =>
    (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a,
      Quotient.map' (fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
        (_ :
          ∀ (b c : α),
            Setoid.r b c →
              Setoid.r
                ((fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) }) b)
                ((fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                  c))
        a)
[PROOFSTEP]
refine' Prod.rec _
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
⊢ ∀ (fst : α ⧸ t) (snd : { x // x ∈ t } ⧸ subgroupOf s t),
    (fun a =>
          (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a,
            Quotient.map'
              (fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
              (_ :
                ∀ (b c : α),
                  Setoid.r b c →
                    Setoid.r
                      ((fun g =>
                          { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                        b)
                      ((fun g =>
                          { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                        c))
              a))
        ((fun a =>
            Quotient.map' (fun b => f a.fst * ↑b)
              (_ :
                ∀ (b c : { x // x ∈ t }),
                  Setoid.r b c → Setoid.r ((fun b => f a.fst * ↑b) b) ((fun b => f a.fst * ↑b) c))
              a.snd)
          (fst, snd)) =
      (fst, snd)
[PROOFSTEP]
refine' Quotient.ind' fun a => _
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : α
⊢ ∀ (snd : { x // x ∈ t } ⧸ subgroupOf s t),
    (fun a =>
          (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a,
            Quotient.map'
              (fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
              (_ :
                ∀ (b c : α),
                  Setoid.r b c →
                    Setoid.r
                      ((fun g =>
                          { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                        b)
                      ((fun g =>
                          { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                        c))
              a))
        ((fun a =>
            Quotient.map' (fun b => f a.fst * ↑b)
              (_ :
                ∀ (b c : { x // x ∈ t }),
                  Setoid.r b c → Setoid.r ((fun b => f a.fst * ↑b) b) ((fun b => f a.fst * ↑b) c))
              a.snd)
          (Quotient.mk'' a, snd)) =
      (Quotient.mk'' a, snd)
[PROOFSTEP]
refine' Quotient.ind' fun b => _
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : α
b : { x // x ∈ t }
⊢ (fun a =>
        (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a,
          Quotient.map'
            (fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
            (_ :
              ∀ (b c : α),
                Setoid.r b c →
                  Setoid.r
                    ((fun g =>
                        { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                      b)
                    ((fun g =>
                        { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                      c))
            a))
      ((fun a =>
          Quotient.map' (fun b => f a.fst * ↑b)
            (_ :
              ∀ (b c : { x // x ∈ t }), Setoid.r b c → Setoid.r ((fun b => f a.fst * ↑b) b) ((fun b => f a.fst * ↑b) c))
            a.snd)
        (Quotient.mk'' a, Quotient.mk'' b)) =
    (Quotient.mk'' a, Quotient.mk'' b)
[PROOFSTEP]
have key : Quotient.mk'' (f (Quotient.mk'' a) * b) = Quotient.mk'' a :=
  (QuotientGroup.mk_mul_of_mem (f a) b.2).trans (hf a)
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : α
b : { x // x ∈ t }
key : Quotient.mk'' (f (Quotient.mk'' a) * ↑b) = Quotient.mk'' a
⊢ (fun a =>
        (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a,
          Quotient.map'
            (fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
            (_ :
              ∀ (b c : α),
                Setoid.r b c →
                  Setoid.r
                    ((fun g =>
                        { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                      b)
                    ((fun g =>
                        { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                      c))
            a))
      ((fun a =>
          Quotient.map' (fun b => f a.fst * ↑b)
            (_ :
              ∀ (b c : { x // x ∈ t }), Setoid.r b c → Setoid.r ((fun b => f a.fst * ↑b) b) ((fun b => f a.fst * ↑b) c))
            a.snd)
        (Quotient.mk'' a, Quotient.mk'' b)) =
    (Quotient.mk'' a, Quotient.mk'' b)
[PROOFSTEP]
simp_rw [Quotient.map'_mk'', id.def, key, inv_mul_cancel_left]
[GOAL]
α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : { x // x ∈ s }
⊢ Setoid.r a b → Setoid.r (↑(inclusion h) a) (↑(inclusion h) b)
[PROOFSTEP]
simp_rw [leftRel_eq]
[GOAL]
α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : { x // x ∈ s }
⊢ a⁻¹ * b ∈ subgroupOf H s → (↑(inclusion h) a)⁻¹ * ↑(inclusion h) b ∈ subgroupOf H t
[PROOFSTEP]
exact id
[GOAL]
α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
⊢ ∀ (a₁ a₂ : { x // x ∈ s }),
    Quotient.map' ↑(inclusion h)
          (_ : ∀ (a b : { x // x ∈ s }), Setoid.r a b → Setoid.r (↑(inclusion h) a) (↑(inclusion h) b))
          (Quotient.mk'' a₁) =
        Quotient.map' ↑(inclusion h)
          (_ : ∀ (a b : { x // x ∈ s }), Setoid.r a b → Setoid.r (↑(inclusion h) a) (↑(inclusion h) b))
          (Quotient.mk'' a₂) →
      Quotient.mk'' a₁ = Quotient.mk'' a₂
[PROOFSTEP]
intro a b h
[GOAL]
α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h✝ : s ≤ t
a b : { x // x ∈ s }
h :
  Quotient.map' ↑(inclusion h✝)
      (_ : ∀ (a b : { x // x ∈ s }), Setoid.r a b → Setoid.r (↑(inclusion h✝) a) (↑(inclusion h✝) b))
      (Quotient.mk'' a) =
    Quotient.map' ↑(inclusion h✝)
      (_ : ∀ (a b : { x // x ∈ s }), Setoid.r a b → Setoid.r (↑(inclusion h✝) a) (↑(inclusion h✝) b)) (Quotient.mk'' b)
⊢ Quotient.mk'' a = Quotient.mk'' b
[PROOFSTEP]
simpa only [Quotient.map'_mk'', eq'] using h
[GOAL]
α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : { x // x ∈ H }
⊢ Setoid.r a b → Setoid.r (id a) (id b)
[PROOFSTEP]
simp_rw [leftRel_eq]
[GOAL]
α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : { x // x ∈ H }
⊢ a⁻¹ * b ∈ subgroupOf s H → (id a)⁻¹ * id b ∈ subgroupOf t H
[PROOFSTEP]
apply h
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h : s ≤ t
a b : α
⊢ Setoid.r a b → Setoid.r (id a) (id b)
[PROOFSTEP]
simp_rw [leftRel_eq]
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h : s ≤ t
a b : α
⊢ a⁻¹ * b ∈ s → (id a)⁻¹ * id b ∈ t
[PROOFSTEP]
apply h
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
H : Subgroup α
⊢ ∀ (a₁ a₂ : { x // x ∈ H }),
    (fun q i => quotientSubgroupOfMapOfLE H (_ : iInf f ≤ f i) q) (Quotient.mk'' a₁) =
        (fun q i => quotientSubgroupOfMapOfLE H (_ : iInf f ≤ f i) q) (Quotient.mk'' a₂) →
      Quotient.mk'' a₁ = Quotient.mk'' a₂
[PROOFSTEP]
simp_rw [funext_iff, quotientSubgroupOfMapOfLE_apply_mk, eq', mem_subgroupOf, mem_iInf, imp_self, forall_const]
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
⊢ ∀ (a₁ a₂ : α),
    (fun q i => quotientMapOfLE (_ : iInf f ≤ f i) q) (Quotient.mk'' a₁) =
        (fun q i => quotientMapOfLE (_ : iInf f ≤ f i) q) (Quotient.mk'' a₂) →
      Quotient.mk'' a₁ = Quotient.mk'' a₂
[PROOFSTEP]
simp_rw [funext_iff, quotientMapOfLE_apply_mk, eq', mem_iInf, imp_self, forall_const]
[GOAL]
α : Type u_1
inst✝³ : Group α
s✝ t : Subgroup α
inst✝² : Fintype α
s : Subgroup α
inst✝¹ : Fintype { x // x ∈ s }
inst✝ : DecidablePred fun a => a ∈ s
⊢ Fintype.card α = Fintype.card (α ⧸ s) * Fintype.card { x // x ∈ s }
[PROOFSTEP]
rw [← Fintype.card_prod]
[GOAL]
α : Type u_1
inst✝³ : Group α
s✝ t : Subgroup α
inst✝² : Fintype α
s : Subgroup α
inst✝¹ : Fintype { x // x ∈ s }
inst✝ : DecidablePred fun a => a ∈ s
⊢ Fintype.card α = Fintype.card ((α ⧸ s) × { x // x ∈ s })
[PROOFSTEP]
exact Fintype.card_congr Subgroup.groupEquivQuotientProdSubgroup
[GOAL]
α : Type u_1
inst✝² : Group α
s✝ t : Subgroup α
inst✝¹ : Fintype α
s : Subgroup α
inst✝ : Fintype { x // x ∈ s }
⊢ Fintype.card { x // x ∈ s } ∣ Fintype.card α
[PROOFSTEP]
classical simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_left ℕ]
[GOAL]
α : Type u_1
inst✝² : Group α
s✝ t : Subgroup α
inst✝¹ : Fintype α
s : Subgroup α
inst✝ : Fintype { x // x ∈ s }
⊢ Fintype.card { x // x ∈ s } ∣ Fintype.card α
[PROOFSTEP]
simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_left ℕ]
[GOAL]
α : Type u_1
inst✝² : Group α
s✝ t : Subgroup α
inst✝¹ : Fintype α
s : Subgroup α
inst✝ : DecidablePred fun x => x ∈ s
⊢ Fintype.card (α ⧸ s) ∣ Fintype.card α
[PROOFSTEP]
simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_right ℕ]
[GOAL]
α : Type u_1
inst✝³ : Group α
s t : Subgroup α
H : Type u_2
inst✝² : Group H
inst✝¹ : Fintype α
inst✝ : Fintype H
f : α →* H
hf : Injective ↑f
⊢ card α ∣ card H
[PROOFSTEP]
classical calc
  card α = card (f.range : Subgroup H) := card_congr (Equiv.ofInjective f hf)
  _ ∣ card H := card_subgroup_dvd_card _
[GOAL]
α : Type u_1
inst✝³ : Group α
s t : Subgroup α
H : Type u_2
inst✝² : Group H
inst✝¹ : Fintype α
inst✝ : Fintype H
f : α →* H
hf : Injective ↑f
⊢ card α ∣ card H
[PROOFSTEP]
calc
  card α = card (f.range : Subgroup H) := card_congr (Equiv.ofInjective f hf)
  _ ∣ card H := card_subgroup_dvd_card _
[GOAL]
α : Type u_1
inst✝³ : Group α
s t : Subgroup α
H : Type u_2
inst✝² : Group H
K : Subgroup H
inst✝¹ : Fintype { x // x ∈ K }
f : α →* H
inst✝ : Fintype { x // x ∈ comap f K }
hf : Injective ↑f
⊢ card { x // x ∈ comap f K } ∣ card { x // x ∈ K }
[PROOFSTEP]
haveI : Fintype ((K.comap f).map f) := Fintype.ofEquiv _ (equivMapOfInjective _ _ hf).toEquiv
[GOAL]
α : Type u_1
inst✝³ : Group α
s t : Subgroup α
H : Type u_2
inst✝² : Group H
K : Subgroup H
inst✝¹ : Fintype { x // x ∈ K }
f : α →* H
inst✝ : Fintype { x // x ∈ comap f K }
hf : Injective ↑f
this : Fintype { x // x ∈ map f (comap f K) }
⊢ card { x // x ∈ comap f K } ∣ card { x // x ∈ K }
[PROOFSTEP]
calc
  Fintype.card (K.comap f) = Fintype.card ((K.comap f).map f) := Fintype.card_congr (equivMapOfInjective _ _ hf).toEquiv
  _ ∣ Fintype.card K := card_dvd_of_le (map_comap_le _ _)
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
a : { x // x ∈ s } × ↑t
⊢ ↑(Quotient.out' ↑a.snd * ↑a.fst) ∈ t
[PROOFSTEP]
rw [mk_mul_of_mem _ a.1.2, out_eq']
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
a : { x // x ∈ s } × ↑t
⊢ ↑a.snd ∈ t
[PROOFSTEP]
exact a.2.2
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
x✝ : ↑(mk ⁻¹' t)
a : α
ha : a ∈ mk ⁻¹' t
⊢ Quotient.out'
        ↑((fun a =>
                ({ val := (Quotient.out' ↑↑a)⁻¹ * ↑a, property := (_ : (Quotient.out' ↑↑a)⁻¹ * ↑a ∈ s) },
                  { val := ↑↑a, property := (_ : ↑a ∈ mk ⁻¹' t) }))
              { val := a, property := ha }).snd *
      ↑((fun a =>
              ({ val := (Quotient.out' ↑↑a)⁻¹ * ↑a, property := (_ : (Quotient.out' ↑↑a)⁻¹ * ↑a ∈ s) },
                { val := ↑↑a, property := (_ : ↑a ∈ mk ⁻¹' t) }))
            { val := a, property := ha }).fst =
    a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
x✝ : { x // x ∈ s } × ↑t
a : α
ha : a ∈ s
x : α ⧸ s
hx : x ∈ t
⊢ (fun a =>
        ({ val := (Quotient.out' ↑↑a)⁻¹ * ↑a, property := (_ : (Quotient.out' ↑↑a)⁻¹ * ↑a ∈ s) },
          { val := ↑↑a, property := (_ : ↑a ∈ mk ⁻¹' t) }))
      ((fun a => { val := Quotient.out' ↑a.snd * ↑a.fst, property := (_ : ↑(Quotient.out' ↑a.snd * ↑a.fst) ∈ t) })
        ({ val := a, property := ha }, { val := x, property := hx })) =
    ({ val := a, property := ha }, { val := x, property := hx })
[PROOFSTEP]
ext
[GOAL]
case h₁.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
x✝ : { x // x ∈ s } × ↑t
a : α
ha : a ∈ s
x : α ⧸ s
hx : x ∈ t
⊢ ↑((fun a =>
            ({ val := (Quotient.out' ↑↑a)⁻¹ * ↑a, property := (_ : (Quotient.out' ↑↑a)⁻¹ * ↑a ∈ s) },
              { val := ↑↑a, property := (_ : ↑a ∈ mk ⁻¹' t) }))
          ((fun a => { val := Quotient.out' ↑a.snd * ↑a.fst, property := (_ : ↑(Quotient.out' ↑a.snd * ↑a.fst) ∈ t) })
            ({ val := a, property := ha }, { val := x, property := hx }))).fst =
    ↑({ val := a, property := ha }, { val := x, property := hx }).fst
[PROOFSTEP]
simp [ha]
[GOAL]
case h₂.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
x✝ : { x // x ∈ s } × ↑t
a : α
ha : a ∈ s
x : α ⧸ s
hx : x ∈ t
⊢ ↑((fun a =>
            ({ val := (Quotient.out' ↑↑a)⁻¹ * ↑a, property := (_ : (Quotient.out' ↑↑a)⁻¹ * ↑a ∈ s) },
              { val := ↑↑a, property := (_ : ↑a ∈ mk ⁻¹' t) }))
          ((fun a => { val := Quotient.out' ↑a.snd * ↑a.fst, property := (_ : ↑(Quotient.out' ↑a.snd * ↑a.fst) ∈ t) })
            ({ val := a, property := ha }, { val := x, property := hx }))).snd =
    ↑({ val := a, property := ha }, { val := x, property := hx }).snd
[PROOFSTEP]
simp [ha]


[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
a b c d : G
hab : Setoid.r a b
hcd : Setoid.r c d
⊢ Setoid.r (a * c) (b * d)
[PROOFSTEP]
rw [leftRel_eq] at hab hcd ⊢
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
a b c d : G
hab : a⁻¹ * b ∈ N
hcd : c⁻¹ * d ∈ N
⊢ (fun x y => x⁻¹ * y ∈ N) (a * c) (b * d)
[PROOFSTEP]
dsimp only
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
a b c d : G
hab : a⁻¹ * b ∈ N
hcd : c⁻¹ * d ∈ N
⊢ (a * c)⁻¹ * (b * d) ∈ N
[PROOFSTEP]
calc
  (a * c)⁻¹ * (b * d) = c⁻¹ * (a⁻¹ * b) * c⁻¹⁻¹ * (c⁻¹ * d) := by
    simp only [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
  _ ∈ N := N.mul_mem (nN.conj_mem _ hab _) hcd
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
a b c d : G
hab : a⁻¹ * b ∈ N
hcd : c⁻¹ * d ∈ N
⊢ (a * c)⁻¹ * (b * d) = c⁻¹ * (a⁻¹ * b) * c⁻¹⁻¹ * (c⁻¹ * d)
[PROOFSTEP]
simp only [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
x y : G
⊢ x⁻¹ * y ∈ N ↔ ∃ z, z ∈ N ∧ x * z = y
[PROOFSTEP]
simp only [← _root_.eq_inv_mul_iff_mul_eq, exists_prop, exists_eq_right]
[GOAL]
G : Type u
inst✝¹ : Group G
N✝ : Subgroup G
nN✝ : Subgroup.Normal N✝
H : Type v
inst✝ : Group H
N : Subgroup G
nN : Subgroup.Normal N
x : G
⊢ ↑x = 1 ↔ x ∈ N
[PROOFSTEP]
refine' QuotientGroup.eq.trans _
[GOAL]
G : Type u
inst✝¹ : Group G
N✝ : Subgroup G
nN✝ : Subgroup.Normal N✝
H : Type v
inst✝ : Group H
N : Subgroup G
nN : Subgroup.Normal N
x : G
⊢ x⁻¹ * 1 ∈ N ↔ x ∈ N
[PROOFSTEP]
rw [mul_one, Subgroup.inv_mem_iff]
[GOAL]
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
I : Type w
inst✝¹ : Group I
f : G →* H
inst✝ : Subgroup.Normal (MonoidHom.range f)
g : H →* I
h : MonoidHom.comp (mk' (MonoidHom.range f)) (Subgroup.subtype (MonoidHom.ker g)) = 1
x : H
hx : x ∈ MonoidHom.ker g
⊢ ↑x = 1
[PROOFSTEP]
exact FunLike.congr_fun h ⟨x, hx⟩
[GOAL]
G : Type u
inst✝¹ : Group G
N✝ : Subgroup G
nN✝ : Subgroup.Normal N✝
H : Type v
inst✝ : Group H
N : Subgroup G
nN : Subgroup.Normal N
x y : G
⊢ ↑x = ↑y ↔ x / y ∈ N
[PROOFSTEP]
refine' eq_comm.trans (QuotientGroup.eq.trans _)
[GOAL]
G : Type u
inst✝¹ : Group G
N✝ : Subgroup G
nN✝ : Subgroup.Normal N✝
H : Type v
inst✝ : Group H
N : Subgroup G
nN : Subgroup.Normal N
x y : G
⊢ y⁻¹ * x ∈ N ↔ x / y ∈ N
[PROOFSTEP]
rw [nN.mem_comm_iff, div_eq_mul_inv]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
HN : ∀ (x : G), x ∈ N → ↑φ x = 1
x y : G
h : ↑(QuotientGroup.con N) x y
⊢ ↑(Con.ker φ) x y
[PROOFSTEP]
simp only [QuotientGroup.con, leftRel_apply, Con.rel_mk] at h
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
HN : ∀ (x : G), x ∈ N → ↑φ x = 1
x y : G
h : x⁻¹ * y ∈ N
⊢ ↑(Con.ker φ) x y
[PROOFSTEP]
rw [Con.ker_rel]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
HN : ∀ (x : G), x ∈ N → ↑φ x = 1
x y : G
h : x⁻¹ * y ∈ N
⊢ ↑φ x = ↑φ y
[PROOFSTEP]
calc
  φ x = φ (y * (x⁻¹ * y)⁻¹) := by rw [mul_inv_rev, inv_inv, mul_inv_cancel_left]
  _ = φ y := by rw [φ.map_mul, HN _ (N.inv_mem h), mul_one]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
HN : ∀ (x : G), x ∈ N → ↑φ x = 1
x y : G
h : x⁻¹ * y ∈ N
⊢ ↑φ x = ↑φ (y * (x⁻¹ * y)⁻¹)
[PROOFSTEP]
rw [mul_inv_rev, inv_inv, mul_inv_cancel_left]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
HN : ∀ (x : G), x ∈ N → ↑φ x = 1
x y : G
h : x⁻¹ * y ∈ N
⊢ ↑φ (y * (x⁻¹ * y)⁻¹) = ↑φ y
[PROOFSTEP]
rw [φ.map_mul, HN _ (N.inv_mem h), mul_one]
[GOAL]
G : Type u
inst✝² : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝¹ : Group H
M : Subgroup H
inst✝ : Subgroup.Normal M
f : G →* H
h : N ≤ Subgroup.comap f M
⊢ G ⧸ N →* H ⧸ M
[PROOFSTEP]
refine' QuotientGroup.lift N ((mk' M).comp f) _
[GOAL]
G : Type u
inst✝² : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝¹ : Group H
M : Subgroup H
inst✝ : Subgroup.Normal M
f : G →* H
h : N ≤ Subgroup.comap f M
⊢ ∀ (x : G), x ∈ N → ↑(MonoidHom.comp (mk' M) f) x = 1
[PROOFSTEP]
intro x hx
[GOAL]
G : Type u
inst✝² : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝¹ : Group H
M : Subgroup H
inst✝ : Subgroup.Normal M
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
hx : x ∈ N
⊢ ↑(MonoidHom.comp (mk' M) f) x = 1
[PROOFSTEP]
refine' QuotientGroup.eq.2 _
[GOAL]
G : Type u
inst✝² : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝¹ : Group H
M : Subgroup H
inst✝ : Subgroup.Normal M
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
hx : x ∈ N
⊢ (↑f x)⁻¹ * 1 ∈ M
[PROOFSTEP]
rw [mul_one, Subgroup.inv_mem_iff]
[GOAL]
G : Type u
inst✝² : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝¹ : Group H
M : Subgroup H
inst✝ : Subgroup.Normal M
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
hx : x ∈ N
⊢ ↑f x ∈ M
[PROOFSTEP]
exact h hx
[GOAL]
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
I : Type u_1
inst✝² : Group I
M : Subgroup H
O : Subgroup I
inst✝¹ : Subgroup.Normal M
inst✝ : Subgroup.Normal O
f : G →* H
g : H →* I
hf : N ≤ Subgroup.comap f M
hg : M ≤ Subgroup.comap g O
hgf : optParam (N ≤ Subgroup.comap (MonoidHom.comp g f) O) (_ : N ≤ Subgroup.comap (MonoidHom.comp g f) O)
x : G ⧸ N
⊢ ↑(map M O g hg) (↑(map N M f hf) x) = ↑(map N O (MonoidHom.comp g f) hgf) x
[PROOFSTEP]
refine' induction_on' x fun x => _
[GOAL]
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
I : Type u_1
inst✝² : Group I
M : Subgroup H
O : Subgroup I
inst✝¹ : Subgroup.Normal M
inst✝ : Subgroup.Normal O
f : G →* H
g : H →* I
hf : N ≤ Subgroup.comap f M
hg : M ≤ Subgroup.comap g O
hgf : optParam (N ≤ Subgroup.comap (MonoidHom.comp g f) O) (_ : N ≤ Subgroup.comap (MonoidHom.comp g f) O)
x✝ : G ⧸ N
x : G
⊢ ↑(map M O g hg) (↑(map N M f hf) ↑x) = ↑(map N O (MonoidHom.comp g f) hgf) ↑x
[PROOFSTEP]
simp only [map_mk, MonoidHom.comp_apply]
[GOAL]
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
G' : Subgroup G
H' : Subgroup H
inst✝¹ : Subgroup.Normal G'
inst✝ : Subgroup.Normal H'
e : G ≃* H
he : Subgroup.map (↑e) G' = H'
src✝ : G ⧸ G' →* H ⧸ H' := map G' H' ↑e (_ : G' ≤ Subgroup.comap (↑e) H')
x : G ⧸ G'
⊢ ↑(map H' G' ↑(MulEquiv.symm e) (_ : H' ≤ Subgroup.comap (↑(MulEquiv.symm e)) G'))
      (↑(map G' H' ↑e (_ : G' ≤ Subgroup.comap (↑e) H')) x) =
    x
[PROOFSTEP]
rw [map_map G' H' G' e e.symm (he ▸ G'.le_comap_map (e : G →* H)) (he ▸ (G'.map_equiv_eq_comap_symm e).le)]
[GOAL]
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
G' : Subgroup G
H' : Subgroup H
inst✝¹ : Subgroup.Normal G'
inst✝ : Subgroup.Normal H'
e : G ≃* H
he : Subgroup.map (↑e) G' = H'
src✝ : G ⧸ G' →* H ⧸ H' := map G' H' ↑e (_ : G' ≤ Subgroup.comap (↑e) H')
x : G ⧸ G'
⊢ ↑(map G' G' (MonoidHom.comp ↑(MulEquiv.symm e) ↑e)
          (_ : G' ≤ Subgroup.comap (MonoidHom.comp ↑(MulEquiv.symm e) ↑e) G'))
      x =
    x
[PROOFSTEP]
simp only [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm, MulEquiv.coe_monoidHom_refl, map_id_apply]
[GOAL]
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
G' : Subgroup G
H' : Subgroup H
inst✝¹ : Subgroup.Normal G'
inst✝ : Subgroup.Normal H'
e : G ≃* H
he : Subgroup.map (↑e) G' = H'
src✝ : G ⧸ G' →* H ⧸ H' := map G' H' ↑e (_ : G' ≤ Subgroup.comap (↑e) H')
x : H ⧸ H'
⊢ ↑(map G' H' ↑e (_ : G' ≤ Subgroup.comap (↑e) H'))
      (↑(map H' G' ↑(MulEquiv.symm e) (_ : H' ≤ Subgroup.comap (↑(MulEquiv.symm e)) G')) x) =
    x
[PROOFSTEP]
rw [map_map H' G' H' e.symm e (he ▸ (G'.map_equiv_eq_comap_symm e).le) (he ▸ G'.le_comap_map (e : G →* H))]
[GOAL]
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
G' : Subgroup G
H' : Subgroup H
inst✝¹ : Subgroup.Normal G'
inst✝ : Subgroup.Normal H'
e : G ≃* H
he : Subgroup.map (↑e) G' = H'
src✝ : G ⧸ G' →* H ⧸ H' := map G' H' ↑e (_ : G' ≤ Subgroup.comap (↑e) H')
x : H ⧸ H'
⊢ ↑(map H' H' (MonoidHom.comp ↑e ↑(MulEquiv.symm e))
          (_ : H' ≤ Subgroup.comap (MonoidHom.comp ↑e ↑(MulEquiv.symm e)) H'))
      x =
    x
[PROOFSTEP]
simp only [← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self, MulEquiv.coe_monoidHom_refl, map_id_apply]
[GOAL]
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
G' : Subgroup G
H' : Subgroup H
inst✝¹ : Subgroup.Normal G'
inst✝ : Subgroup.Normal H'
he : optParam (Subgroup.map (↑(MulEquiv.refl G)) G' = G') (_ : Subgroup.map (MonoidHom.id G) G' = G')
⊢ congr G' G' (MulEquiv.refl G) he = MulEquiv.refl (G ⧸ G')
[PROOFSTEP]
ext ⟨x⟩
[GOAL]
case h.mk
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
G' : Subgroup G
H' : Subgroup H
inst✝¹ : Subgroup.Normal G'
inst✝ : Subgroup.Normal H'
he : optParam (Subgroup.map (↑(MulEquiv.refl G)) G' = G') (_ : Subgroup.map (MonoidHom.id G) G' = G')
x✝ : G ⧸ G'
x : G
⊢ ↑(congr G' G' (MulEquiv.refl G) he) (Quot.mk Setoid.r x) = ↑(MulEquiv.refl (G ⧸ G')) (Quot.mk Setoid.r x)
[PROOFSTEP]
rfl
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ ker φ
a b : G
h : ↑φ a = ↑φ b
⊢ Setoid.r a b
[PROOFSTEP]
rw [leftRel_apply, mem_ker, φ.map_mul, ← h, φ.map_inv, inv_mul_self]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
g : G
hg : g ∈ ker φ
⊢ g ∈ ker (rangeRestrict φ)
[PROOFSTEP]
rwa [ker_rangeRestrict]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ ker φ
a b : G
h : ↑(rangeRestrict φ) a = ↑(rangeRestrict φ) b
⊢ Setoid.r a b
[PROOFSTEP]
rw [leftRel_apply, ← ker_rangeRestrict, mem_ker, φ.rangeRestrict.map_mul, ← h, φ.rangeRestrict.map_inv, inv_mul_self]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
⊢ Surjective ↑(rangeKerLift φ)
[PROOFSTEP]
rintro ⟨_, g, rfl⟩
[GOAL]
case mk.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
g : G
⊢ ∃ a, ↑(rangeKerLift φ) a = { val := ↑φ g, property := (_ : ∃ y, ↑φ y = ↑φ g) }
[PROOFSTEP]
use mk g
[GOAL]
case h
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
g : G
⊢ ↑(rangeKerLift φ) ↑g = { val := ↑φ g, property := (_ : ∃ y, ↑φ y = ↑φ g) }
[PROOFSTEP]
rfl
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
ψ : H → G
hφ : Function.RightInverse ψ ↑φ
src✝ : G ⧸ ker φ →* H := kerLift φ
x : G ⧸ ker φ
⊢ ↑(kerLift φ) ((mk ∘ ψ) (↑(kerLift φ) x)) = ↑(kerLift φ) x
[PROOFSTEP]
rw [Function.comp_apply, kerLift_mk', hφ]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
A' A B' B : Subgroup G
hAN : Subgroup.Normal (Subgroup.subgroupOf A' A)
hBN : Subgroup.Normal (Subgroup.subgroupOf B' B)
h' : A' = B'
h : A = B
⊢ MonoidHom.comp (quotientMapSubgroupOfOfLe (_ : B' ≤ A') (_ : B ≤ A))
      (quotientMapSubgroupOfOfLe (_ : A' ≤ B') (_ : A ≤ B)) =
    MonoidHom.id ({ x // x ∈ A } ⧸ Subgroup.subgroupOf A' A)
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case h.h.mk
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
A' A B' B : Subgroup G
hAN : Subgroup.Normal (Subgroup.subgroupOf A' A)
hBN : Subgroup.Normal (Subgroup.subgroupOf B' B)
h' : A' = B'
h : A = B
x : G
hx : x ∈ A
⊢ ↑(MonoidHom.comp
          (MonoidHom.comp (quotientMapSubgroupOfOfLe (_ : B' ≤ A') (_ : B ≤ A))
            (quotientMapSubgroupOfOfLe (_ : A' ≤ B') (_ : A ≤ B)))
          (mk' (Subgroup.subgroupOf A' A)))
      { val := x, property := hx } =
    ↑(MonoidHom.comp (MonoidHom.id ({ x // x ∈ A } ⧸ Subgroup.subgroupOf A' A)) (mk' (Subgroup.subgroupOf A' A)))
      { val := x, property := hx }
[PROOFSTEP]
rfl
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
A' A B' B : Subgroup G
hAN : Subgroup.Normal (Subgroup.subgroupOf A' A)
hBN : Subgroup.Normal (Subgroup.subgroupOf B' B)
h' : A' = B'
h : A = B
⊢ MonoidHom.comp (quotientMapSubgroupOfOfLe (_ : A' ≤ B') (_ : A ≤ B))
      (quotientMapSubgroupOfOfLe (_ : B' ≤ A') (_ : B ≤ A)) =
    MonoidHom.id ({ x // x ∈ B } ⧸ Subgroup.subgroupOf B' B)
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case h.h.mk
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
A' A B' B : Subgroup G
hAN : Subgroup.Normal (Subgroup.subgroupOf A' A)
hBN : Subgroup.Normal (Subgroup.subgroupOf B' B)
h' : A' = B'
h : A = B
x : G
hx : x ∈ B
⊢ ↑(MonoidHom.comp
          (MonoidHom.comp (quotientMapSubgroupOfOfLe (_ : A' ≤ B') (_ : A ≤ B))
            (quotientMapSubgroupOfOfLe (_ : B' ≤ A') (_ : B ≤ A)))
          (mk' (Subgroup.subgroupOf B' B)))
      { val := x, property := hx } =
    ↑(MonoidHom.comp (MonoidHom.id ({ x // x ∈ B } ⧸ Subgroup.subgroupOf B' B)) (mk' (Subgroup.subgroupOf B' B)))
      { val := x, property := hx }
[PROOFSTEP]
rfl
[GOAL]
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
φ : G →* H
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
f : A →* B
g✝ : B →* A
e : A ≃* B
d : B ≃* C
n : ℤ
g : A
x✝ : g ∈ range (zpowGroupHom n)
h : A
hg : h ^ n = g
⊢ ↑(zpowGroupHom n) (↑f h) = ↑f g
[PROOFSTEP]
simp only [← hg, map_zpow, zpowGroupHom_apply]
[GOAL]
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
φ : G →* H
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
f : A →* B
g : B →* A
e : A ≃* B
d : B ≃* C
n : ℤ
⊢ MulEquiv.refl (A ⧸ range (zpowGroupHom n)) = equivQuotientZPowOfEquiv (MulEquiv.refl A) n
[PROOFSTEP]
ext x
[GOAL]
case h
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
φ : G →* H
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
f : A →* B
g : B →* A
e : A ≃* B
d : B ≃* C
n : ℤ
x : A ⧸ range (zpowGroupHom n)
⊢ ↑(MulEquiv.refl (A ⧸ range (zpowGroupHom n))) x = ↑(equivQuotientZPowOfEquiv (MulEquiv.refl A) n) x
[PROOFSTEP]
rw [← Quotient.out_eq' x]
[GOAL]
case h
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
φ : G →* H
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
f : A →* B
g : B →* A
e : A ≃* B
d : B ≃* C
n : ℤ
x : A ⧸ range (zpowGroupHom n)
⊢ ↑(MulEquiv.refl (A ⧸ range (zpowGroupHom n))) (Quotient.mk'' (Quotient.out' x)) =
    ↑(equivQuotientZPowOfEquiv (MulEquiv.refl A) n) (Quotient.mk'' (Quotient.out' x))
[PROOFSTEP]
rfl
[GOAL]
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
φ : G →* H
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
f : A →* B
g : B →* A
e : A ≃* B
d : B ≃* C
n : ℤ
⊢ MulEquiv.trans (equivQuotientZPowOfEquiv e n) (equivQuotientZPowOfEquiv d n) =
    equivQuotientZPowOfEquiv (MulEquiv.trans e d) n
[PROOFSTEP]
ext x
[GOAL]
case h
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
φ : G →* H
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
f : A →* B
g : B →* A
e : A ≃* B
d : B ≃* C
n : ℤ
x : A ⧸ range (zpowGroupHom n)
⊢ ↑(MulEquiv.trans (equivQuotientZPowOfEquiv e n) (equivQuotientZPowOfEquiv d n)) x =
    ↑(equivQuotientZPowOfEquiv (MulEquiv.trans e d) n) x
[PROOFSTEP]
rw [← Quotient.out_eq' x]
[GOAL]
case h
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝³ : Group H
φ : G →* H
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
f : A →* B
g : B →* A
e : A ≃* B
d : B ≃* C
n : ℤ
x : A ⧸ range (zpowGroupHom n)
⊢ ↑(MulEquiv.trans (equivQuotientZPowOfEquiv e n) (equivQuotientZPowOfEquiv d n)) (Quotient.mk'' (Quotient.out' x)) =
    ↑(equivQuotientZPowOfEquiv (MulEquiv.trans e d) n) (Quotient.mk'' (Quotient.out' x))
[PROOFSTEP]
rfl
[GOAL]
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
⊢ ∀ (a : { x // x ∈ H ⊔ N }), ∃ a_1, ↑φ a_1 = Quotient.mk'' a
[PROOFSTEP]
rintro ⟨y, hy : y ∈ (H ⊔ N)⟩
[GOAL]
case mk
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
y : G
hy : y ∈ H ⊔ N
⊢ ∃ a, ↑φ a = Quotient.mk'' { val := y, property := hy }
[PROOFSTEP]
rw [← SetLike.mem_coe] at hy
[GOAL]
case mk
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
y : G
hy✝ : y ∈ H ⊔ N
hy : y ∈ ↑(H ⊔ N)
⊢ ∃ a, ↑φ a = Quotient.mk'' { val := y, property := hy✝ }
[PROOFSTEP]
rw [mul_normal H N] at hy
[GOAL]
case mk
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
y : G
hy✝ : y ∈ H ⊔ N
hy : y ∈ ↑H * ↑N
⊢ ∃ a, ↑φ a = Quotient.mk'' { val := y, property := hy✝ }
[PROOFSTEP]
rcases hy with ⟨h, n, hh, hn, rfl⟩
[GOAL]
case mk.intro.intro.intro.intro
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
h n : G
hh : h ∈ ↑H
hn : n ∈ ↑N
hy : (fun x x_1 => x * x_1) h n ∈ H ⊔ N
⊢ ∃ a, ↑φ a = Quotient.mk'' { val := (fun x x_1 => x * x_1) h n, property := hy }
[PROOFSTEP]
use⟨h, hh⟩
[GOAL]
case h
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
h n : G
hh : h ∈ ↑H
hn : n ∈ ↑N
hy : (fun x x_1 => x * x_1) h n ∈ H ⊔ N
⊢ ↑φ { val := h, property := hh } = Quotient.mk'' { val := (fun x x_1 => x * x_1) h n, property := hy }
[PROOFSTEP]
let _ : Setoid ↑(H ⊔ N) :=
  (@leftRel ↑(H ⊔ N) (H ⊔ N : Subgroup G).toGroup (N.subgroupOf (H ⊔ N)))
    -- porting note: Lean couldn't find this automatically
[GOAL]
case h
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
h n : G
hh : h ∈ ↑H
hn : n ∈ ↑N
hy : (fun x x_1 => x * x_1) h n ∈ H ⊔ N
x✝ : Setoid { x // x ∈ H ⊔ N } := leftRel (subgroupOf N (H ⊔ N))
⊢ ↑φ { val := h, property := hh } = Quotient.mk'' { val := (fun x x_1 => x * x_1) h n, property := hy }
[PROOFSTEP]
refine Quotient.eq.mpr ?_
[GOAL]
case h
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
h n : G
hh : h ∈ ↑H
hn : n ∈ ↑N
hy : (fun x x_1 => x * x_1) h n ∈ H ⊔ N
x✝ : Setoid { x // x ∈ H ⊔ N } := leftRel (subgroupOf N (H ⊔ N))
⊢ ↑(inclusion (_ : H ≤ H ⊔ N)) { val := h, property := hh } ≈ { val := (fun x x_1 => x * x_1) h n, property := hy }
[PROOFSTEP]
change Setoid.r _ _
[GOAL]
case h
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
h n : G
hh : h ∈ ↑H
hn : n ∈ ↑N
hy : (fun x x_1 => x * x_1) h n ∈ H ⊔ N
x✝ : Setoid { x // x ∈ H ⊔ N } := leftRel (subgroupOf N (H ⊔ N))
⊢ Setoid.r (↑(inclusion (_ : H ≤ H ⊔ N)) { val := h, property := hh })
    { val := (fun x x_1 => x * x_1) h n, property := hy }
[PROOFSTEP]
rw [leftRel_apply]
[GOAL]
case h
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
h n : G
hh : h ∈ ↑H
hn : n ∈ ↑N
hy : (fun x x_1 => x * x_1) h n ∈ H ⊔ N
x✝ : Setoid { x // x ∈ H ⊔ N } := leftRel (subgroupOf N (H ⊔ N))
⊢ (↑(inclusion (_ : H ≤ H ⊔ N)) { val := h, property := hh })⁻¹ *
      { val := (fun x x_1 => x * x_1) h n, property := hy } ∈
    subgroupOf N (H ⊔ N)
[PROOFSTEP]
change h⁻¹ * (h * n) ∈ N
[GOAL]
case h
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
x : { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N)
h n : G
hh : h ∈ ↑H
hn : n ∈ ↑N
hy : (fun x x_1 => x * x_1) h n ∈ H ⊔ N
x✝ : Setoid { x // x ∈ H ⊔ N } := leftRel (subgroupOf N (H ⊔ N))
⊢ h⁻¹ * (h * n) ∈ N
[PROOFSTEP]
rwa [← mul_assoc, inv_mul_self, one_mul]
[GOAL]
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : Normal N✝
H✝ : Type v
inst✝¹ : Group H✝
φ✝ : G →* H✝
H N : Subgroup G
inst✝ : Normal N
φ : { x // x ∈ H } →* { x // x ∈ H ⊔ N } ⧸ subgroupOf N (H ⊔ N) :=
  MonoidHom.comp (mk' (subgroupOf N (H ⊔ N))) (inclusion (_ : H ≤ H ⊔ N))
φ_surjective : Surjective ↑φ
⊢ subgroupOf N H = ker φ
[PROOFSTEP]
simp [← comap_ker]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
M : Subgroup G
nM : Subgroup.Normal M
h : N ≤ M
⊢ ∀ (x : G ⧸ N), x ∈ Subgroup.map (mk' N) M → ↑(map N M (MonoidHom.id G) h) x = 1
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
M : Subgroup G
nM : Subgroup.Normal M
h : N ≤ M
x : G
hx : x ∈ ↑M
⊢ ↑(map N M (MonoidHom.id G) h) (↑(mk' N) x) = 1
[PROOFSTEP]
rw [map_mk' N M _ _ x]
[GOAL]
case intro.intro
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
M : Subgroup G
nM : Subgroup.Normal M
h : N ≤ M
x : G
hx : x ∈ ↑M
⊢ ↑(↑(MonoidHom.id G) x) = 1
[PROOFSTEP]
exact (QuotientGroup.eq_one_iff _).mpr hx
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
M : Subgroup G
nM : Subgroup.Normal M
h : N ≤ M
⊢ MonoidHom.comp (map M (Subgroup.map (mk' N) M) (mk' N) (_ : M ≤ Subgroup.comap (mk' N) (Subgroup.map (mk' N) M)))
      (quotientQuotientEquivQuotientAux N M h) =
    MonoidHom.id ((G ⧸ N) ⧸ Subgroup.map (mk' N) M)
[PROOFSTEP]
ext
[GOAL]
case h.h.h
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
M : Subgroup G
nM : Subgroup.Normal M
h : N ≤ M
x✝ : G
⊢ ↑(MonoidHom.comp
          (MonoidHom.comp
            (MonoidHom.comp
              (map M (Subgroup.map (mk' N) M) (mk' N) (_ : M ≤ Subgroup.comap (mk' N) (Subgroup.map (mk' N) M)))
              (quotientQuotientEquivQuotientAux N M h))
            (mk' (Subgroup.map (mk' N) M)))
          (mk' N))
      x✝ =
    ↑(MonoidHom.comp (MonoidHom.comp (MonoidHom.id ((G ⧸ N) ⧸ Subgroup.map (mk' N) M)) (mk' (Subgroup.map (mk' N) M)))
          (mk' N))
      x✝
[PROOFSTEP]
simp
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
M : Subgroup G
nM : Subgroup.Normal M
h : N ≤ M
⊢ MonoidHom.comp (quotientQuotientEquivQuotientAux N M h)
      (map M (Subgroup.map (mk' N) M) (mk' N) (_ : M ≤ Subgroup.comap (mk' N) (Subgroup.map (mk' N) M))) =
    MonoidHom.id (G ⧸ M)
[PROOFSTEP]
ext
[GOAL]
case h.h
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
M : Subgroup G
nM : Subgroup.Normal M
h : N ≤ M
x✝ : G
⊢ ↑(MonoidHom.comp
          (MonoidHom.comp (quotientQuotientEquivQuotientAux N M h)
            (map M (Subgroup.map (mk' N) M) (mk' N) (_ : M ≤ Subgroup.comap (mk' N) (Subgroup.map (mk' N) M))))
          (mk' M))
      x✝ =
    ↑(MonoidHom.comp (MonoidHom.id (G ⧸ M)) (mk' M)) x✝
[PROOFSTEP]
simp
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
⊢ Subsingleton (G ⧸ ⊤)
[PROOFSTEP]
dsimp [HasQuotient.Quotient, QuotientGroup.instHasQuotientSubgroup, Quotient]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
⊢ Subsingleton (Quot Setoid.r)
[PROOFSTEP]
rw [leftRel_eq]
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
⊢ Subsingleton (Quot fun x y => x⁻¹ * y ∈ ⊤)
[PROOFSTEP]
exact Trunc.instSubsingletonTrunc
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H✝ : Type v
inst✝ : Group H✝
φ : G →* H✝
H : Subgroup G
h : Subsingleton (G ⧸ H)
x : G
x✝ : x ∈ ⊤
⊢ x ∈ H
[PROOFSTEP]
have this : 1⁻¹ * x ∈ H := QuotientGroup.eq.1 (Subsingleton.elim _ _)
[GOAL]
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H✝ : Type v
inst✝ : Group H✝
φ : G →* H✝
H : Subgroup G
h : Subsingleton (G ⧸ H)
x : G
x✝ : x ∈ ⊤
this : 1⁻¹ * x ∈ H
⊢ x ∈ H
[PROOFSTEP]
rwa [inv_one, one_mul] at this
[GOAL]
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
φ : G →* H
H₁ : Subgroup G
inst✝¹ : Subgroup.Normal H₁
H₂ : Subgroup (G ⧸ H₁)
inst✝ : Subgroup.Normal H₂
⊢ Subgroup.comap (mk' H₁) (Subgroup.comap (mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) =
    Subgroup.comap (mk' (Subgroup.comap (mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (mk' H₁) H₂))
[PROOFSTEP]
ext x
[GOAL]
case h
G : Type u
inst✝³ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝² : Group H
φ : G →* H
H₁ : Subgroup G
inst✝¹ : Subgroup.Normal H₁
H₂ : Subgroup (G ⧸ H₁)
inst✝ : Subgroup.Normal H₂
x : G
⊢ x ∈ Subgroup.comap (mk' H₁) (Subgroup.comap (mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) ↔
    x ∈ Subgroup.comap (mk' (Subgroup.comap (mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (mk' H₁) H₂))
[PROOFSTEP]
simp only [mk'_apply, Subgroup.mem_comap, Subgroup.mem_center_iff, forall_mk, ← mk_mul, eq_iff_div_mem, mk_div]


[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ ⨆ (i : ι), S i ↔ ∃ i, x ∈ S i
[PROOFSTEP]
refine' ⟨_, fun ⟨i, hi⟩ => (SetLike.le_def.1 <| le_iSup S i) hi⟩
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
suffices x ∈ closure (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by simpa only [closure_iUnion, closure_eq (S _)] using this
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
this : x ∈ closure (⋃ (i : ι), ↑(S i)) → ∃ i, x ∈ S i
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
simpa only [closure_iUnion, closure_eq (S _)] using this
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ closure (⋃ (i : ι), ↑(S i)) → ∃ i, x ∈ S i
[PROOFSTEP]
refine' fun hx => closure_induction hx (fun y hy => mem_iUnion.mp hy) _
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
⊢ ∀ (x y : M), (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S i
[PROOFSTEP]
rintro x y ⟨i, hi⟩ ⟨j, hj⟩
[GOAL]
case intro.intro
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : M
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x y : M
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
⊢ ∃ i, x * y ∈ S i
[PROOFSTEP]
rcases hS i j with ⟨k, hki, hkj⟩
[GOAL]
case intro.intro.intro.intro
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x x_1 => x ≤ x_1) S
x✝ : M
hx : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
x y : M
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
k : ι
hki : S i ≤ S k
hkj : S j ≤ S k
⊢ ∃ i, x * y ∈ S i
[PROOFSTEP]
exact ⟨k, (S k).mul_mem (hki hi) (hkj hj)⟩
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ ↑(⨆ (i : ι), S i) ↔ x ∈ ⋃ (i : ι), ↑(S i)
[PROOFSTEP]
simp [mem_iSup_of_directed hS]
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : Set (Subsemigroup M)
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
[PROOFSTEP]
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, Subtype.coe_mk, exists_prop]
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : Set (Subsemigroup M)
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ (s : Subsemigroup M) (_ : s ∈ S), ↑s
[PROOFSTEP]
simp [mem_sSup_of_directed_on hS]
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S T : Subsemigroup M
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
[PROOFSTEP]
have : S ≤ S ⊔ T := le_sup_left
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S T : Subsemigroup M
this : S ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
[PROOFSTEP]
tauto
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S T : Subsemigroup M
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T
[PROOFSTEP]
have : T ≤ S ⊔ T := le_sup_right
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S T : Subsemigroup M
this : T ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T
[PROOFSTEP]
tauto
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
i : ι
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S
[PROOFSTEP]
have : S i ≤ iSup S := le_iSup _ _
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
i : ι
this : S i ≤ iSup S
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S
[PROOFSTEP]
tauto
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : Set (Subsemigroup M)
s : Subsemigroup M
hs : s ∈ S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S
[PROOFSTEP]
have : s ≤ sSup S := le_sSup hs
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : Set (Subsemigroup M)
s : Subsemigroup M
hs : s ∈ S
this : s ≤ sSup S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S
[PROOFSTEP]
tauto
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ ⨆ (i : ι), S i
hp : ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂
hmul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x₁
[PROOFSTEP]
rw [iSup_eq_closure] at hx₁
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂
hmul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x₁
[PROOFSTEP]
refine' closure_induction hx₁ (fun x₂ hx₂ => _) hmul
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂
hmul : ∀ (x y : M), C x → C y → C (x * y)
x₂ : M
hx₂ : x₂ ∈ ⋃ (i : ι), ↑(S i)
⊢ C x₂
[PROOFSTEP]
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx₂
[GOAL]
case intro
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x₂ : M), x₂ ∈ S i → C x₂
hmul : ∀ (x y : M), C x → C y → C (x * y)
x₂ : M
hx₂ : x₂ ∈ ⋃ (i : ι), ↑(S i)
i : ι
hi : x₂ ∈ ↑(S i)
⊢ C x₂
[PROOFSTEP]
exact hp _ _ hi
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x₁ : M
hx₁ : x₁ ∈ ⨆ (i : ι), S i
⊢ C x₁ hx₁
[PROOFSTEP]
refine Exists.elim ?_ fun (hx₁' : x₁ ∈ ⨆ i, S i) (hc : C x₁ hx₁') => hc
[GOAL]
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x₁ : M
hx₁ : x₁ ∈ ⨆ (i : ι), S i
⊢ ∃ x, C x₁ x
[PROOFSTEP]
refine @iSup_induction _ _ _ S (fun x' => ∃ hx'', C x' hx'') _ hx₁ (fun i x₂ hx₂ => ?_) fun x₃ y => ?_
[GOAL]
case refine_1
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x₁ : M
hx₁ : x₁ ∈ ⨆ (i : ι), S i
i : ι
x₂ : M
hx₂ : x₂ ∈ S i
⊢ (fun x' => ∃ hx'', C x' hx'') x₂
[PROOFSTEP]
exact ⟨_, hp _ _ hx₂⟩
[GOAL]
case refine_2
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x₁ : M
hx₁ : x₁ ∈ ⨆ (i : ι), S i
x₃ y : M
⊢ (fun x' => ∃ hx'', C x' hx'') x₃ → (fun x' => ∃ hx'', C x' hx'') y → (fun x' => ∃ hx'', C x' hx'') (x₃ * y)
[PROOFSTEP]
rintro ⟨_, Cx⟩ ⟨_, Cy⟩
[GOAL]
case refine_2.intro.intro
ι : Sort u_1
M : Type u_2
A : Type u_3
B : Type u_4
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x₁ : M
hx₁ : x₁ ∈ ⨆ (i : ι), S i
x₃ y : M
w✝¹ : x₃ ∈ ⨆ (i : ι), S i
Cx : C x₃ w✝¹
w✝ : y ∈ ⨆ (i : ι), S i
Cy : C y w✝
⊢ ∃ hx'', C (x₃ * y) hx''
[PROOFSTEP]
exact ⟨_, hmul _ _ _ _ Cx Cy⟩


[GOAL]
M : Type u_1
S T : Set M
inst✝ : MulOneClass M
⊢ 1 ∈ centralizer S
[PROOFSTEP]
simp [mem_centralizer_iff]
[GOAL]
M : Type u_1
S T : Set M
inst✝ : MulZeroClass M
⊢ 0 ∈ centralizer S
[PROOFSTEP]
simp [mem_centralizer_iff]
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : Semigroup M
ha : a ∈ centralizer S
hb : b ∈ centralizer S
g : M
hg : g ∈ S
⊢ g * (a * b) = a * b * g
[PROOFSTEP]
rw [mul_assoc, ← hb g hg, ← mul_assoc, ha g hg, mul_assoc]
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : Group M
ha : a ∈ centralizer S
g : M
hg : g ∈ S
⊢ g * a⁻¹ = a⁻¹ * g
[PROOFSTEP]
rw [mul_inv_eq_iff_eq_mul, mul_assoc, eq_inv_mul_iff_mul_eq, ha g hg]
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : Distrib M
ha : a ∈ centralizer S
hb : b ∈ centralizer S
c : M
hc : c ∈ S
⊢ c * (a + b) = (a + b) * c
[PROOFSTEP]
rw [add_mul, mul_add, ha c hc, hb c hc]
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝¹ : Mul M
inst✝ : HasDistribNeg M
ha : a ∈ centralizer S
c : M
hc : c ∈ S
⊢ c * -a = -a * c
[PROOFSTEP]
rw [mul_neg, ha c hc, neg_mul]
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : GroupWithZero M
ha : a ∈ centralizer S
h : a = 0
⊢ a⁻¹ ∈ centralizer S
[PROOFSTEP]
rw [h, inv_zero]
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : GroupWithZero M
ha : a ∈ centralizer S
h : a = 0
⊢ 0 ∈ centralizer S
[PROOFSTEP]
exact zero_mem_centralizer S
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : GroupWithZero M
ha : a ∈ centralizer S
ha0 : a ≠ 0
c : M
hc : c ∈ S
⊢ c * a⁻¹ = a⁻¹ * c
[PROOFSTEP]
rw [mul_inv_eq_iff_eq_mul₀ ha0, mul_assoc, eq_inv_mul_iff_mul_eq₀ ha0, ha c hc]
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : Group M
ha : a ∈ centralizer S
hb : b ∈ centralizer S
⊢ a / b ∈ centralizer S
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : Group M
ha : a ∈ centralizer S
hb : b ∈ centralizer S
⊢ a * b⁻¹ ∈ centralizer S
[PROOFSTEP]
exact mul_mem_centralizer ha (inv_mem_centralizer hb)
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : GroupWithZero M
ha : a ∈ centralizer S
hb : b ∈ centralizer S
⊢ a / b ∈ centralizer S
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
M : Type u_1
S T : Set M
a b : M
inst✝ : GroupWithZero M
ha : a ∈ centralizer S
hb : b ∈ centralizer S
⊢ a * b⁻¹ ∈ centralizer S
[PROOFSTEP]
exact mul_mem_centralizer ha (inv_mem_centralizer₀ hb)


[GOAL]
M : Type u_1
inst✝ : MulOneClass M
⊢ 1 ∈ center M
[PROOFSTEP]
simp [mem_center_iff]
[GOAL]
M : Type u_1
inst✝ : MulZeroClass M
⊢ 0 ∈ center M
[PROOFSTEP]
simp [mem_center_iff]
[GOAL]
M : Type u_1
inst✝ : Semigroup M
a b : M
ha : a ∈ center M
hb : b ∈ center M
g : M
⊢ g * (a * b) = a * b * g
[PROOFSTEP]
rw [mul_assoc, ← hb g, ← mul_assoc, ha g, mul_assoc]
[GOAL]
M : Type u_1
inst✝ : Group M
a : M
ha : a ∈ center M
g : M
⊢ g * a⁻¹ = a⁻¹ * g
[PROOFSTEP]
rw [← inv_inj, mul_inv_rev, inv_inv, ← ha, mul_inv_rev, inv_inv]
[GOAL]
M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
c : M
⊢ c * (a + b) = (a + b) * c
[PROOFSTEP]
rw [add_mul, mul_add, ha c, hb c]
[GOAL]
M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
c : M
⊢ c * -a = -a * c
[PROOFSTEP]
rw [← neg_mul_comm, ha (-c), neg_mul_comm]
[GOAL]
M : Type u_1
inst✝ : GroupWithZero M
a : Mˣ
ha : a ∈ center Mˣ
b : M
⊢ b * ↑a = ↑a * b
[PROOFSTEP]
obtain rfl | hb := eq_or_ne b 0
[GOAL]
case inl
M : Type u_1
inst✝ : GroupWithZero M
a : Mˣ
ha : a ∈ center Mˣ
⊢ 0 * ↑a = ↑a * 0
[PROOFSTEP]
rw [zero_mul, mul_zero]
[GOAL]
case inr
M : Type u_1
inst✝ : GroupWithZero M
a : Mˣ
ha : a ∈ center Mˣ
b : M
hb : b ≠ 0
⊢ b * ↑a = ↑a * b
[PROOFSTEP]
exact Units.ext_iff.mp (ha (Units.mk0 _ hb))
[GOAL]
M : Type u_1
inst✝ : GroupWithZero M
a : M
ha : a ∈ center M
⊢ a⁻¹ ∈ center M
[PROOFSTEP]
obtain rfl | ha0 := eq_or_ne a 0
[GOAL]
case inl
M : Type u_1
inst✝ : GroupWithZero M
ha : 0 ∈ center M
⊢ 0⁻¹ ∈ center M
[PROOFSTEP]
rw [inv_zero]
[GOAL]
case inl
M : Type u_1
inst✝ : GroupWithZero M
ha : 0 ∈ center M
⊢ 0 ∈ center M
[PROOFSTEP]
exact zero_mem_center M
[GOAL]
case inr
M : Type u_1
inst✝ : GroupWithZero M
a : M
ha : a ∈ center M
ha0 : a ≠ 0
⊢ a⁻¹ ∈ center M
[PROOFSTEP]
rcases IsUnit.mk0 _ ha0 with ⟨a, rfl⟩
[GOAL]
case inr.intro
M : Type u_1
inst✝ : GroupWithZero M
a : Mˣ
ha : ↑a ∈ center M
ha0 : ↑a ≠ 0
⊢ (↑a)⁻¹ ∈ center M
[PROOFSTEP]
rw [← Units.val_inv_eq_inv_val]
[GOAL]
case inr.intro
M : Type u_1
inst✝ : GroupWithZero M
a : Mˣ
ha : ↑a ∈ center M
ha0 : ↑a ≠ 0
⊢ ↑a⁻¹ ∈ center M
[PROOFSTEP]
exact center_units_subset (inv_mem_center (subset_center_units ha))
[GOAL]
M : Type u_1
inst✝ : Group M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a / b ∈ center M
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
M : Type u_1
inst✝ : Group M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a * b⁻¹ ∈ center M
[PROOFSTEP]
exact mul_mem_center ha (inv_mem_center hb)
[GOAL]
M : Type u_1
inst✝ : GroupWithZero M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a / b ∈ center M
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
M : Type u_1
inst✝ : GroupWithZero M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a * b⁻¹ ∈ center M
[PROOFSTEP]
exact mul_mem_center ha (inv_mem_center₀ hb)