[GOAL]
M : Type u_1
inst✝ : MulOneClass M
a b : M
h : 1 * a = b
⊢ a = b
[PROOFSTEP]
rwa [one_mul] at h


[GOAL]
G : Type u
inst✝ : Group G
⊢ commutator G = Subgroup.closure (commutatorSet G)
[PROOFSTEP]
simp [commutator, Subgroup.commutator_def, commutatorSet]
[GOAL]
G : Type u
inst✝ : Group G
⊢ commutator G = Subgroup.normalClosure (commutatorSet G)
[PROOFSTEP]
simp [commutator, Subgroup.commutator_def', commutatorSet]
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.FG { x // x ∈ commutator G }
[PROOFSTEP]
rw [commutator_eq_closure]
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.FG { x // x ∈ Subgroup.closure (commutatorSet G) }
[PROOFSTEP]
apply Group.closure_finite_fg
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank { x // x ∈ commutator G } ≤ Nat.card ↑(commutatorSet G)
[PROOFSTEP]
rw [Subgroup.rank_congr (commutator_eq_closure G)]
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank { x // x ∈ Subgroup.closure (commutatorSet G) } ≤ Nat.card ↑(commutatorSet G)
[PROOFSTEP]
apply Subgroup.rank_closure_finite_le_nat_card
[GOAL]
G : Type u
inst✝ : Group G
⊢ ⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆ ≤ Subgroup.center G
[PROOFSTEP]
rw [← Subgroup.centralizer_univ, ← Subgroup.coe_top, ← Subgroup.commutator_eq_bot_iff_le_centralizer]
[GOAL]
G : Type u
inst✝ : Group G
⊢ ⁅⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆, ⊤⁆ = ⊥
[PROOFSTEP]
suffices ⁅⁅⊤, centralizer (commutator G : Set G)⁆, centralizer (commutator G : Set G)⁆ = ⊥
  by
  refine' Subgroup.commutator_commutator_eq_bot_of_rotate _ this
  rwa [Subgroup.commutator_comm (centralizer (commutator G : Set G))]
[GOAL]
G : Type u
inst✝ : Group G
this : ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥
⊢ ⁅⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆, ⊤⁆ = ⊥
[PROOFSTEP]
refine' Subgroup.commutator_commutator_eq_bot_of_rotate _ this
[GOAL]
G : Type u
inst✝ : Group G
this : ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥
⊢ ⁅⁅centralizer ↑(commutator G), ⊤⁆, centralizer ↑(commutator G)⁆ = ⊥
[PROOFSTEP]
rwa [Subgroup.commutator_comm (centralizer (commutator G : Set G))]
[GOAL]
G : Type u
inst✝ : Group G
⊢ ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥
[PROOFSTEP]
rw [Subgroup.commutator_comm, Subgroup.commutator_eq_bot_iff_le_centralizer]
[GOAL]
G : Type u
inst✝ : Group G
⊢ centralizer ↑(commutator G) ≤ centralizer ↑⁅⊤, centralizer ↑(commutator G)⁆
[PROOFSTEP]
exact Set.centralizer_subset (Subgroup.commutator_mono le_top le_top)
[GOAL]
G : Type u
inst✝ : Group G
src✝ : Group (G ⧸ commutator G) := QuotientGroup.Quotient.group (commutator G)
x y : Abelianization G
a b : G
⊢ ⁅b⁻¹, a⁻¹⁆ = ((fun x x_1 => x * x_1) a b)⁻¹ * (fun x x_1 => x * x_1) b a
[PROOFSTEP]
group
[GOAL]
G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
⊢ commutator G ≤ MonoidHom.ker f
[PROOFSTEP]
rw [commutator_eq_closure, Subgroup.closure_le]
[GOAL]
G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
⊢ commutatorSet G ⊆ ↑(MonoidHom.ker f)
[PROOFSTEP]
rintro x ⟨p, q, rfl⟩
[GOAL]
case intro.intro
G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
p q : G
⊢ ⁅p, q⁆ ∈ ↑(MonoidHom.ker f)
[PROOFSTEP]
simp [MonoidHom.mem_ker, mul_right_comm (f p) (f q), commutatorElement_def]
[GOAL]
G : Type u
inst✝² inst✝¹ : Group G
H : Type v
inst✝ : Group H
e : G ≃* H
⊢ Function.LeftInverse ↑(Abelianization.map (toMonoidHom (symm e))) ↑(Abelianization.map (toMonoidHom e))
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case mk
G : Type u
inst✝² inst✝¹ : Group G
H : Type v
inst✝ : Group H
e : G ≃* H
x✝ : Abelianization G
a : G
⊢ ↑(Abelianization.map (toMonoidHom (symm e))) (↑(Abelianization.map (toMonoidHom e)) (Quot.mk Setoid.r a)) =
    Quot.mk Setoid.r a
[PROOFSTEP]
simp
[GOAL]
G : Type u
inst✝² inst✝¹ : Group G
H : Type v
inst✝ : Group H
e : G ≃* H
⊢ Function.RightInverse ↑(Abelianization.map (toMonoidHom (symm e))) ↑(Abelianization.map (toMonoidHom e))
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case mk
G : Type u
inst✝² inst✝¹ : Group G
H : Type v
inst✝ : Group H
e : G ≃* H
x✝ : Abelianization H
a : H
⊢ ↑(Abelianization.map (toMonoidHom e)) (↑(Abelianization.map (toMonoidHom (symm e))) (Quot.mk Setoid.r a)) =
    Quot.mk Setoid.r a
[PROOFSTEP]
simp
[GOAL]
G : Type u
inst✝¹ : Group G
H : Type u_1
inst✝ : CommGroup H
src✝ : H →* Abelianization H := of
⊢ Function.RightInverse ↑(↑lift (MonoidHom.id H)) ↑of
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case mk
G : Type u
inst✝¹ : Group G
H : Type u_1
inst✝ : CommGroup H
src✝ : H →* Abelianization H := of
x✝ : Abelianization H
a : H
⊢ ↑of (↑(↑lift (MonoidHom.id H)) (Quot.mk Setoid.r a)) = Quot.mk Setoid.r a
[PROOFSTEP]
rfl
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank { x // x ∈ closureCommutatorRepresentatives G } ≤ 2 * Nat.card ↑(commutatorSet G)
[PROOFSTEP]
rw [two_mul]
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank { x // x ∈ closureCommutatorRepresentatives G } ≤ Nat.card ↑(commutatorSet G) + Nat.card ↑(commutatorSet G)
[PROOFSTEP]
exact
  (Subgroup.rank_closure_finite_le_nat_card _).trans
    ((Set.card_union_le _ _).trans
      (add_le_add ((Finite.card_image_le _).trans (Finite.card_range_le _))
        ((Finite.card_image_le _).trans (Finite.card_range_le _))))
[GOAL]
G : Type u
inst✝ : Group G
⊢ ↑(Subgroup.subtype (closureCommutatorRepresentatives G)) ''
      commutatorSet { x // x ∈ closureCommutatorRepresentatives G } =
    commutatorSet G
[PROOFSTEP]
apply Set.Subset.antisymm
[GOAL]
case h₁
G : Type u
inst✝ : Group G
⊢ ↑(Subgroup.subtype (closureCommutatorRepresentatives G)) ''
      commutatorSet { x // x ∈ closureCommutatorRepresentatives G } ⊆
    commutatorSet G
[PROOFSTEP]
rintro - ⟨-, ⟨g₁, g₂, rfl⟩, rfl⟩
[GOAL]
case h₁.intro.intro.intro.intro
G : Type u
inst✝ : Group G
g₁ g₂ : { x // x ∈ closureCommutatorRepresentatives G }
⊢ ↑(Subgroup.subtype (closureCommutatorRepresentatives G)) ⁅g₁, g₂⁆ ∈ commutatorSet G
[PROOFSTEP]
exact ⟨g₁, g₂, rfl⟩
[GOAL]
case h₂
G : Type u
inst✝ : Group G
⊢ commutatorSet G ⊆
    ↑(Subgroup.subtype (closureCommutatorRepresentatives G)) ''
      commutatorSet { x // x ∈ closureCommutatorRepresentatives G }
[PROOFSTEP]
exact fun g hg =>
  ⟨_,
    ⟨⟨_, subset_closure (Or.inl ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩)⟩, ⟨_, subset_closure (Or.inr ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩)⟩, rfl⟩,
    hg.choose_spec.choose_spec⟩
[GOAL]
G : Type u
inst✝ : Group G
⊢ Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) = Nat.card ↑(commutatorSet G)
[PROOFSTEP]
rw [← image_commutatorSet_closureCommutatorRepresentatives G]
[GOAL]
G : Type u
inst✝ : Group G
⊢ Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) =
    Nat.card
      ↑(↑(Subgroup.subtype (closureCommutatorRepresentatives G)) ''
          commutatorSet { x // x ∈ closureCommutatorRepresentatives G })
[PROOFSTEP]
exact Nat.card_congr (Equiv.Set.image _ _ (subtype_injective _))
[GOAL]
G : Type u
inst✝ : Group G
⊢ Nat.card { x // x ∈ _root_.commutator { x // x ∈ closureCommutatorRepresentatives G } } =
    Nat.card { x // x ∈ _root_.commutator G }
[PROOFSTEP]
rw [commutator_eq_closure G, ← image_commutatorSet_closureCommutatorRepresentatives, ← MonoidHom.map_closure, ←
  commutator_eq_closure]
[GOAL]
G : Type u
inst✝ : Group G
⊢ Nat.card { x // x ∈ _root_.commutator { x // x ∈ closureCommutatorRepresentatives G } } =
    Nat.card
      { x //
        x ∈
          map (Subgroup.subtype (closureCommutatorRepresentatives G))
            (_root_.commutator { x // x ∈ closureCommutatorRepresentatives G }) }
[PROOFSTEP]
exact Nat.card_congr (Equiv.Set.image _ _ (subtype_injective _))
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Finite ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G })
[PROOFSTEP]
apply Nat.finite_of_card_ne_zero
[GOAL]
case h
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) ≠ 0
[PROOFSTEP]
rw [card_commutatorSet_closureCommutatorRepresentatives]
[GOAL]
case h
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Nat.card ↑(commutatorSet G) ≠ 0
[PROOFSTEP]
exact Finite.card_pos.ne'


[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype (ConjClasses G)
inst✝¹ : Fintype G
inst✝ : (x : ConjClasses G) → Fintype ↑(carrier x)
⊢ ∑ x : ConjClasses G, Finset.card (Set.toFinset (carrier x)) = Fintype.card G
[PROOFSTEP]
suffices : (Σ x : ConjClasses G, x.carrier) ≃ G
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype (ConjClasses G)
inst✝¹ : Fintype G
inst✝ : (x : ConjClasses G) → Fintype ↑(carrier x)
this : (x : ConjClasses G) × ↑(carrier x) ≃ G
⊢ ∑ x : ConjClasses G, Finset.card (Set.toFinset (carrier x)) = Fintype.card G
[PROOFSTEP]
simpa using (Fintype.card_congr this)
[GOAL]
case this
G : Type u
inst✝³ : Group G
inst✝² : Fintype (ConjClasses G)
inst✝¹ : Fintype G
inst✝ : (x : ConjClasses G) → Fintype ↑(carrier x)
⊢ (x : ConjClasses G) × ↑(carrier x) ≃ G
[PROOFSTEP]
simpa [carrier_eq_preimage_mk] using Equiv.sigmaFiberEquiv ConjClasses.mk
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
⊢ ∑ᶠ (x : ConjClasses G), Set.ncard (carrier x) = Nat.card G
[PROOFSTEP]
classical
cases nonempty_fintype G
rw [Nat.card_eq_fintype_card, ← sum_conjClasses_card_eq_card, finsum_eq_sum_of_fintype]
simp [Set.ncard_eq_toFinset_card']
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
⊢ ∑ᶠ (x : ConjClasses G), Set.ncard (carrier x) = Nat.card G
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ᶠ (x : ConjClasses G), Set.ncard (carrier x) = Nat.card G
[PROOFSTEP]
rw [Nat.card_eq_fintype_card, ← sum_conjClasses_card_eq_card, finsum_eq_sum_of_fintype]
[GOAL]
case intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ i : ConjClasses G, Set.ncard (carrier i) = ∑ x : ConjClasses G, Finset.card (Set.toFinset (carrier x))
[PROOFSTEP]
simp [Set.ncard_eq_toFinset_card']
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
⊢ Nat.card { x // x ∈ Subgroup.center G } + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑(carrier x) =
    Nat.card G
[PROOFSTEP]
classical
cases nonempty_fintype G
rw [@Nat.card_eq_fintype_card G, ← sum_conjClasses_card_eq_card, ←
  Finset.sum_sdiff (ConjClasses.noncenter G).toFinset.subset_univ]
simp only [Nat.card_eq_fintype_card, Set.toFinset_card]
congr 1
swap
· convert finsum_cond_eq_sum_of_cond_iff _ _
  simp [Set.mem_toFinset]
calc
  Fintype.card (Subgroup.center G) = Fintype.card ((noncenter G)ᶜ : Set _) := Fintype.card_congr ((mk_bijOn G).equiv _)
  _ = Finset.card (Finset.univ \ (noncenter G).toFinset) := by
    rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]
  _ = _ := ?_
rw [Finset.card_eq_sum_ones]
refine Finset.sum_congr rfl ?_
rintro ⟨g⟩ hg
simp only [noncenter, Set.not_subsingleton_iff, Set.toFinset_setOf, Finset.mem_univ, true_and, forall_true_left,
  Finset.mem_sdiff, Finset.mem_filter, Set.not_nontrivial_iff] at hg
rw [eq_comm, ← Set.toFinset_card, Finset.card_eq_one]
exact ⟨g, Finset.coe_injective <| by simpa using hg.eq_singleton_of_mem mem_carrier_mk⟩
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
⊢ Nat.card { x // x ∈ Subgroup.center G } + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑(carrier x) =
    Nat.card G
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Nat.card { x // x ∈ Subgroup.center G } + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑(carrier x) =
    Nat.card G
[PROOFSTEP]
rw [@Nat.card_eq_fintype_card G, ← sum_conjClasses_card_eq_card, ←
  Finset.sum_sdiff (ConjClasses.noncenter G).toFinset.subset_univ]
[GOAL]
case intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Nat.card { x // x ∈ Subgroup.center G } + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑(carrier x) =
    ∑ x in Finset.univ \ Set.toFinset (noncenter G), Finset.card (Set.toFinset (carrier x)) +
      ∑ x in Set.toFinset (noncenter G), Finset.card (Set.toFinset (carrier x))
[PROOFSTEP]
simp only [Nat.card_eq_fintype_card, Set.toFinset_card]
[GOAL]
case intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card { x // x ∈ Subgroup.center G } +
      ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Fintype.card ↑(carrier x) =
    ∑ x in Finset.univ \ Set.toFinset (noncenter G), Fintype.card ↑(carrier x) +
      ∑ x in Set.toFinset (noncenter G), Fintype.card ↑(carrier x)
[PROOFSTEP]
congr 1
[GOAL]
case intro.e_a
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card { x // x ∈ Subgroup.center G } =
    ∑ x in Finset.univ \ Set.toFinset (noncenter G), Fintype.card ↑(carrier x)
case intro.e_a
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Fintype.card ↑(carrier x) =
    ∑ x in Set.toFinset (noncenter G), Fintype.card ↑(carrier x)
[PROOFSTEP]
swap
[GOAL]
case intro.e_a
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Fintype.card ↑(carrier x) =
    ∑ x in Set.toFinset (noncenter G), Fintype.card ↑(carrier x)
[PROOFSTEP]
convert finsum_cond_eq_sum_of_cond_iff _ _
[GOAL]
case intro.e_a.convert_7
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∀ {x : ConjClasses G}, Fintype.card ↑(carrier x) ≠ 0 → (x ∈ noncenter G ↔ x ∈ Set.toFinset (noncenter G))
[PROOFSTEP]
simp [Set.mem_toFinset]
[GOAL]
case intro.e_a
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card { x // x ∈ Subgroup.center G } =
    ∑ x in Finset.univ \ Set.toFinset (noncenter G), Fintype.card ↑(carrier x)
[PROOFSTEP]
calc
  Fintype.card (Subgroup.center G) = Fintype.card ((noncenter G)ᶜ : Set _) := Fintype.card_congr ((mk_bijOn G).equiv _)
  _ = Finset.card (Finset.univ \ (noncenter G).toFinset) := by
    rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]
  _ = _ := ?_
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card ↑(noncenter G)ᶜ = Finset.card (Finset.univ \ Set.toFinset (noncenter G))
[PROOFSTEP]
rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]
[GOAL]
case intro.e_a
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Finset.card (Finset.univ \ Set.toFinset (noncenter G)) =
    ∑ x in Finset.univ \ Set.toFinset (noncenter G), Fintype.card ↑(carrier x)
[PROOFSTEP]
rw [Finset.card_eq_sum_ones]
[GOAL]
case intro.e_a
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ x in Finset.univ \ Set.toFinset (noncenter G), 1 =
    ∑ x in Finset.univ \ Set.toFinset (noncenter G), Fintype.card ↑(carrier x)
[PROOFSTEP]
refine Finset.sum_congr rfl ?_
[GOAL]
case intro.e_a
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∀ (x : ConjClasses G), x ∈ Finset.univ \ Set.toFinset (noncenter G) → 1 = Fintype.card ↑(carrier x)
[PROOFSTEP]
rintro ⟨g⟩ hg
[GOAL]
case intro.e_a.mk
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : Quot.mk Setoid.r g ∈ Finset.univ \ Set.toFinset (noncenter G)
⊢ 1 = Fintype.card ↑(carrier (Quot.mk Setoid.r g))
[PROOFSTEP]
simp only [noncenter, Set.not_subsingleton_iff, Set.toFinset_setOf, Finset.mem_univ, true_and, forall_true_left,
  Finset.mem_sdiff, Finset.mem_filter, Set.not_nontrivial_iff] at hg
[GOAL]
case intro.e_a.mk
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : Set.Subsingleton (carrier (Quot.mk Setoid.r g))
⊢ 1 = Fintype.card ↑(carrier (Quot.mk Setoid.r g))
[PROOFSTEP]
rw [eq_comm, ← Set.toFinset_card, Finset.card_eq_one]
[GOAL]
case intro.e_a.mk
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : Set.Subsingleton (carrier (Quot.mk Setoid.r g))
⊢ ∃ a, Set.toFinset (carrier (Quot.mk Setoid.r g)) = {a}
[PROOFSTEP]
exact ⟨g, Finset.coe_injective <| by simpa using hg.eq_singleton_of_mem mem_carrier_mk⟩
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : Set.Subsingleton (carrier (Quot.mk Setoid.r g))
⊢ ↑(Set.toFinset (carrier (Quot.mk Setoid.r g))) = ↑{g}
[PROOFSTEP]
simpa using hg.eq_singleton_of_mem mem_carrier_mk
[GOAL]
G✝ : Type u
inst✝⁵ : Group G✝
G : Type u_1
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑(carrier x)
inst✝² : Fintype G
inst✝¹ : Fintype { x // x ∈ Subgroup.center G }
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card { x // x ∈ Subgroup.center G } +
      ∑ x in Set.toFinset (noncenter G), Finset.card (Set.toFinset (carrier x)) =
    Fintype.card G
[PROOFSTEP]
convert Group.nat_card_center_add_sum_card_noncenter_eq_card G using 2
[GOAL]
case h.e'_2.h.e'_5
G✝ : Type u
inst✝⁵ : Group G✝
G : Type u_1
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑(carrier x)
inst✝² : Fintype G
inst✝¹ : Fintype { x // x ∈ Subgroup.center G }
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card { x // x ∈ Subgroup.center G } = Nat.card { x // x ∈ Subgroup.center G }
[PROOFSTEP]
simp
[GOAL]
case h.e'_2.h.e'_6
G✝ : Type u
inst✝⁵ : Group G✝
G : Type u_1
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑(carrier x)
inst✝² : Fintype G
inst✝¹ : Fintype { x // x ∈ Subgroup.center G }
inst✝ : Fintype ↑(noncenter G)
⊢ ∑ x in Set.toFinset (noncenter G), Finset.card (Set.toFinset (carrier x)) =
    ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑(carrier x)
[PROOFSTEP]
rw [← finsum_set_coe_eq_finsum_mem (noncenter G), finsum_eq_sum_of_fintype, ← Finset.sum_set_coe]
[GOAL]
case h.e'_2.h.e'_6
G✝ : Type u
inst✝⁵ : Group G✝
G : Type u_1
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑(carrier x)
inst✝² : Fintype G
inst✝¹ : Fintype { x // x ∈ Subgroup.center G }
inst✝ : Fintype ↑(noncenter G)
⊢ ∑ i : ↑(noncenter G), Finset.card (Set.toFinset (carrier ↑i)) = ∑ i : ↑(noncenter G), Nat.card ↑(carrier ↑i)
[PROOFSTEP]
simp
[GOAL]
case h.e'_3
G✝ : Type u
inst✝⁵ : Group G✝
G : Type u_1
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑(carrier x)
inst✝² : Fintype G
inst✝¹ : Fintype { x // x ∈ Subgroup.center G }
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card G = Nat.card G
[PROOFSTEP]
simp


[GOAL]
G : Type u_1
inst✝² : Group G
inst✝¹ : IsFreeGroup G
H : Type u_2
inst✝ : Group H
f : FreeGroup (Generators G) →* H
⊢ (fun f => MonoidHom.comp f (MulEquiv.toMonoidHom (MulEquiv G)))
      ((fun f => MonoidHom.comp f (MulEquiv.toMonoidHom (MulEquiv.symm (MulEquiv G)))) f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : IsFreeGroup G
H : Type u_2
inst✝ : Group H
f : FreeGroup (Generators G) →* H
a✝ : Generators G
⊢ ↑((fun f => MonoidHom.comp f (MulEquiv.toMonoidHom (MulEquiv G)))
          ((fun f => MonoidHom.comp f (MulEquiv.toMonoidHom (MulEquiv.symm (MulEquiv G)))) f))
      (FreeGroup.of a✝) =
    ↑f (FreeGroup.of a✝)
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
inst✝² : Group G
inst✝¹ : IsFreeGroup G
H : Type u_2
inst✝ : Group H
f : G →* H
⊢ (fun f => MonoidHom.comp f (MulEquiv.toMonoidHom (MulEquiv.symm (MulEquiv G))))
      ((fun f => MonoidHom.comp f (MulEquiv.toMonoidHom (MulEquiv G))) f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : IsFreeGroup G
H : Type u_2
inst✝ : Group H
f : G →* H
x✝ : G
⊢ ↑((fun f => MonoidHom.comp f (MulEquiv.toMonoidHom (MulEquiv.symm (MulEquiv G))))
          ((fun f => MonoidHom.comp f (MulEquiv.toMonoidHom (MulEquiv G))) f))
      x✝ =
    ↑f x✝
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
inst✝² : Group G
inst✝¹ : IsFreeGroup G
H : Type u_2
inst✝ : Group H
f : Generators G → H
⊢ ∃! F, ∀ (a : Generators G), ↑F (of a) = f a
[PROOFSTEP]
simpa only [Function.funext_iff] using lift.symm.bijective.existsUnique f
[GOAL]
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : IsFreeGroup G✝
H : Type u_2
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), ↑(↑lift f) (of a) = f a
⊢ MonoidHom.comp (↑lift FreeGroup.of) (↑FreeGroup.lift of) = MonoidHom.id (FreeGroup X)
[PROOFSTEP]
apply FreeGroup.ext_hom
[GOAL]
case h
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : IsFreeGroup G✝
H : Type u_2
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), ↑(↑lift f) (of a) = f a
⊢ ∀ (a : X),
    ↑(MonoidHom.comp (↑lift FreeGroup.of) (↑FreeGroup.lift of)) (FreeGroup.of a) =
      ↑(MonoidHom.id (FreeGroup X)) (FreeGroup.of a)
[PROOFSTEP]
intro x
[GOAL]
case h
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : IsFreeGroup G✝
H : Type u_2
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), ↑(↑lift f) (of a) = f a
x : X
⊢ ↑(MonoidHom.comp (↑lift FreeGroup.of) (↑FreeGroup.lift of)) (FreeGroup.of x) =
    ↑(MonoidHom.id (FreeGroup X)) (FreeGroup.of x)
[PROOFSTEP]
simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.id_apply, FreeGroup.lift.of, lift_of]
[GOAL]
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : IsFreeGroup G✝
H : Type u_2
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), ↑(↑lift f) (of a) = f a
⊢ MonoidHom.comp (↑FreeGroup.lift of) (↑lift FreeGroup.of) = MonoidHom.id G
[PROOFSTEP]
let lift_symm_of : ∀ {H : Type u} [Group H], ∀ (f : G →* H) (a), lift.symm f a = f (of a) := by intro H _ f a;
  simp [← lift_of (lift.symm f)]
[GOAL]
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : IsFreeGroup G✝
H : Type u_2
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), ↑(↑lift f) (of a) = f a
⊢ ∀ {H : Type u} [inst : Group H] (f : G →* H) (a : X), ↑lift.symm f a = ↑f (of a)
[PROOFSTEP]
intro H _ f a
[GOAL]
G✝ : Type u_1
inst✝⁴ : Group G✝
inst✝³ : IsFreeGroup G✝
H✝ : Type u_2
inst✝² : Group H✝
G : Type u
inst✝¹ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), ↑(↑lift f) (of a) = f a
H : Type u
inst✝ : Group H
f : G →* H
a : X
⊢ ↑lift.symm f a = ↑f (of a)
[PROOFSTEP]
simp [← lift_of (lift.symm f)]
[GOAL]
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : IsFreeGroup G✝
H : Type u_2
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), ↑(↑lift f) (of a) = f a
lift_symm_of : ∀ {H : Type u} [inst : Group H] (f : G →* H) (a : X), ↑lift.symm f a = ↑f (of a) :=
  fun {H} [Group H] f a =>
    of_eq_true
      (Eq.trans
        (congrFun
          (congrArg Eq
            (Eq.trans ((fun a => Eq.symm (lift_of (↑lift.symm f) a)) a)
              (congrFun (congrArg FunLike.coe (Equiv.apply_symm_apply lift f)) (of a))))
          (↑f (of a)))
        (eq_self (↑f (of a))))
⊢ MonoidHom.comp (↑FreeGroup.lift of) (↑lift FreeGroup.of) = MonoidHom.id G
[PROOFSTEP]
apply lift.symm.injective
[GOAL]
case a
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : IsFreeGroup G✝
H : Type u_2
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), ↑(↑lift f) (of a) = f a
lift_symm_of : ∀ {H : Type u} [inst : Group H] (f : G →* H) (a : X), ↑lift.symm f a = ↑f (of a) :=
  fun {H} [Group H] f a =>
    of_eq_true
      (Eq.trans
        (congrFun
          (congrArg Eq
            (Eq.trans ((fun a => Eq.symm (lift_of (↑lift.symm f) a)) a)
              (congrFun (congrArg FunLike.coe (Equiv.apply_symm_apply lift f)) (of a))))
          (↑f (of a)))
        (eq_self (↑f (of a))))
⊢ ↑lift.symm (MonoidHom.comp (↑FreeGroup.lift of) (↑lift FreeGroup.of)) = ↑lift.symm (MonoidHom.id G)
[PROOFSTEP]
ext x
[GOAL]
case a.h
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : IsFreeGroup G✝
H : Type u_2
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), ↑(↑lift f) (of a) = f a
lift_symm_of : ∀ {H : Type u} [inst : Group H] (f : G →* H) (a : X), ↑lift.symm f a = ↑f (of a) :=
  fun {H} [Group H] f a =>
    of_eq_true
      (Eq.trans
        (congrFun
          (congrArg Eq
            (Eq.trans ((fun a => Eq.symm (lift_of (↑lift.symm f) a)) a)
              (congrFun (congrArg FunLike.coe (Equiv.apply_symm_apply lift f)) (of a))))
          (↑f (of a)))
        (eq_self (↑f (of a))))
x : X
⊢ ↑lift.symm (MonoidHom.comp (↑FreeGroup.lift of) (↑lift FreeGroup.of)) x = ↑lift.symm (MonoidHom.id G) x
[PROOFSTEP]
simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.id_apply, FreeGroup.lift.of, lift_of, lift_symm_of]


[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c x y : Con M
h : (fun c x y => r x y) x = (fun c x y => r x y) y
⊢ x = y
[PROOFSTEP]
rcases x with ⟨⟨x, _⟩, _⟩
[GOAL]
case mk.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c y : Con M
x : M → M → Prop
iseqv✝ : Equivalence x
mul'✝ : ∀ {w x_1 y z : M}, r w x_1 → r y z → r (w * y) (x_1 * z)
h : (fun c x y => r x y) { toSetoid := { r := x, iseqv := iseqv✝ }, mul' := mul'✝ } = (fun c x y => r x y) y
⊢ { toSetoid := { r := x, iseqv := iseqv✝ }, mul' := mul'✝ } = y
[PROOFSTEP]
rcases y with ⟨⟨y, _⟩, _⟩
[GOAL]
case mk.mk.mk.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
x : M → M → Prop
iseqv✝¹ : Equivalence x
mul'✝¹ : ∀ {w x_1 y z : M}, r w x_1 → r y z → r (w * y) (x_1 * z)
y : M → M → Prop
iseqv✝ : Equivalence y
mul'✝ : ∀ {w x y_1 z : M}, r w x → r y_1 z → r (w * y_1) (x * z)
h :
  (fun c x y => r x y) { toSetoid := { r := x, iseqv := iseqv✝¹ }, mul' := mul'✝¹ } =
    (fun c x y => r x y) { toSetoid := { r := y, iseqv := iseqv✝ }, mul' := mul'✝ }
⊢ { toSetoid := { r := x, iseqv := iseqv✝¹ }, mul' := mul'✝¹ } =
    { toSetoid := { r := y, iseqv := iseqv✝ }, mul' := mul'✝ }
[PROOFSTEP]
have : x = y := h
[GOAL]
case mk.mk.mk.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
x : M → M → Prop
iseqv✝¹ : Equivalence x
mul'✝¹ : ∀ {w x_1 y z : M}, r w x_1 → r y z → r (w * y) (x_1 * z)
y : M → M → Prop
iseqv✝ : Equivalence y
mul'✝ : ∀ {w x y_1 z : M}, r w x → r y_1 z → r (w * y_1) (x * z)
h :
  (fun c x y => r x y) { toSetoid := { r := x, iseqv := iseqv✝¹ }, mul' := mul'✝¹ } =
    (fun c x y => r x y) { toSetoid := { r := y, iseqv := iseqv✝ }, mul' := mul'✝ }
this : x = y
⊢ { toSetoid := { r := x, iseqv := iseqv✝¹ }, mul' := mul'✝¹ } =
    { toSetoid := { r := y, iseqv := iseqv✝ }, mul' := mul'✝ }
[PROOFSTEP]
subst x
[GOAL]
case mk.mk.mk.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
y : M → M → Prop
iseqv✝¹ : Equivalence y
mul'✝¹ : ∀ {w x y_1 z : M}, r w x → r y_1 z → r (w * y_1) (x * z)
iseqv✝ : Equivalence y
mul'✝ : ∀ {w x y_1 z : M}, r w x → r y_1 z → r (w * y_1) (x * z)
h :
  (fun c x y => r x y) { toSetoid := { r := y, iseqv := iseqv✝ }, mul' := mul'✝ } =
    (fun c x y => r x y) { toSetoid := { r := y, iseqv := iseqv✝¹ }, mul' := mul'✝¹ }
⊢ { toSetoid := { r := y, iseqv := iseqv✝ }, mul' := mul'✝ } =
    { toSetoid := { r := y, iseqv := iseqv✝¹ }, mul' := mul'✝¹ }
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
H : r = r
⊢ c = d
[PROOFSTEP]
rcases c with ⟨⟨⟩⟩
[GOAL]
case mk.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c d : Con M
r✝ : M → M → Prop
iseqv✝ : Equivalence r✝
mul'✝ : ∀ {w x y z : M}, r w x → r y z → r (w * y) (x * z)
H : r = r
⊢ { toSetoid := { r := r✝, iseqv := iseqv✝ }, mul' := mul'✝ } = d
[PROOFSTEP]
rcases d with ⟨⟨⟩⟩
[GOAL]
case mk.mk.mk.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r✝¹ : M → M → Prop
iseqv✝¹ : Equivalence r✝¹
mul'✝¹ : ∀ {w x y z : M}, r w x → r y z → r (w * y) (x * z)
r✝ : M → M → Prop
iseqv✝ : Equivalence r✝
mul'✝ : ∀ {w x y z : M}, r w x → r y z → r (w * y) (x * z)
H : r = r
⊢ { toSetoid := { r := r✝¹, iseqv := iseqv✝¹ }, mul' := mul'✝¹ } =
    { toSetoid := { r := r✝, iseqv := iseqv✝ }, mul' := mul'✝ }
[PROOFSTEP]
cases H
[GOAL]
case mk.mk.mk.mk.refl
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r✝ : M → M → Prop
iseqv✝¹ : Equivalence r✝
mul'✝¹ : ∀ {w x y z : M}, r w x → r y z → r (w * y) (x * z)
iseqv✝ : Equivalence r✝
mul'✝ : ∀ {w x y z : M}, r w x → r y z → r (w * y) (x * z)
⊢ { toSetoid := { r := r✝, iseqv := iseqv✝¹ }, mul' := mul'✝¹ } =
    { toSetoid := { r := r✝, iseqv := iseqv✝ }, mul' := mul'✝ }
[PROOFSTEP]
congr
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
H : ∀ (x y : M), ↑c x y ↔ ↑d x y
⊢ r = r
[PROOFSTEP]
ext
[GOAL]
case h.h.a
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
H : ∀ (x y : M), ↑c x y ↔ ↑d x y
x✝¹ x✝ : M
⊢ r x✝¹ x✝ ↔ r x✝¹ x✝
[PROOFSTEP]
apply H
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
f : M → P
h : ∀ (x y : M), f (x * y) = f x * f y
w✝ x✝ y✝ z✝ : M
h1 : r w✝ x✝
h2 : r y✝ z✝
⊢ r (w✝ * y✝) (x✝ * z✝)
[PROOFSTEP]
dsimp [Setoid.ker, onFun] at *
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
f : M → P
h : ∀ (x y : M), f (x * y) = f x * f y
w✝ x✝ y✝ z✝ : M
h1 : f w✝ = f x✝
h2 : f y✝ = f z✝
⊢ f (w✝ * y✝) = f (x✝ * z✝)
[PROOFSTEP]
rw [h, h1, h2, h]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
h : c = d
⊢ ∀ (a₁ a₂ : M), r a₁ a₂ ↔ r (↑(Equiv.refl M) a₁) (↑(Equiv.refl M) a₂)
[PROOFSTEP]
apply ext_iff.2 h
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
h : c = d
src✝ : Quotient c.toSetoid ≃ Quotient d.toSetoid := Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)
x y : Con.Quotient c
⊢ Equiv.toFun
      { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (x * y) =
    Equiv.toFun
        { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        x *
      Equiv.toFun
        { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        y
[PROOFSTEP]
rcases x with ⟨⟩
[GOAL]
case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
h : c = d
src✝ : Quotient c.toSetoid ≃ Quotient d.toSetoid := Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)
x y : Con.Quotient c
a✝ : M
⊢ Equiv.toFun
      { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (Quot.mk r a✝ * y) =
    Equiv.toFun
        { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (Quot.mk r a✝) *
      Equiv.toFun
        { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        y
[PROOFSTEP]
rcases y with ⟨⟩
[GOAL]
case mk.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
h : c = d
src✝ : Quotient c.toSetoid ≃ Quotient d.toSetoid := Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)
x y : Con.Quotient c
a✝¹ a✝ : M
⊢ Equiv.toFun
      { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (Quot.mk r a✝¹ * Quot.mk r a✝) =
    Equiv.toFun
        { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (Quot.mk r a✝¹) *
      Equiv.toFun
        { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (Quot.mk r a✝)
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ : Con M
S : Set (Con M)
x y : M
h : Rel (sInf S).toSetoid x y
r : Setoid M
x✝ : r ∈ toSetoid '' S
c : Con M
hS : c ∈ S
hr : c.toSetoid = r
⊢ Rel r x y
[PROOFSTEP]
rw [← hr]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ : Con M
S : Set (Con M)
x y : M
h : Rel (sInf S).toSetoid x y
r : Setoid M
x✝ : r ∈ toSetoid '' S
c : Con M
hS : c ∈ S
hr : c.toSetoid = r
⊢ Rel c.toSetoid x y
[PROOFSTEP]
exact h c hS
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
⊢ ↑(sInf S) = sInf (FunLike.coe '' S)
[PROOFSTEP]
ext
[GOAL]
case h.h.a
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
x✝¹ x✝ : M
⊢ ↑(sInf S) x✝¹ x✝ ↔ sInf (FunLike.coe '' S) x✝¹ x✝
[PROOFSTEP]
simp only [sInf_image, iInf_apply, iInf_Prop_eq]
[GOAL]
case h.h.a
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
x✝¹ x✝ : M
⊢ ↑(sInf S) x✝¹ x✝ ↔ ∀ (i : Con M), i ∈ S → ↑i x✝¹ x✝
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
src✝¹ : CompleteLattice (Con M) :=
  completeLatticeOfInf (Con M) (_ : ∀ (s : Set (Con M)), sInf s ∈ lowerBounds s ∧ sInf s ∈ upperBounds (lowerBounds s))
src✝ : Setoid M := ⊤
⊢ ∀ {w x y z : M}, r w x → r y z → r (w * y) (x * z)
[PROOFSTEP]
tauto
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ Setoid.r x y
[PROOFSTEP]
apply ConGen.Rel.recOn (motive := fun x y _ => s.r x y) hxy
[GOAL]
case of
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ (x y : M), r x y → Setoid.r x y
[PROOFSTEP]
exact fun x y h => hs x y h
[GOAL]
case refl
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ (x : M), Setoid.r x x
[PROOFSTEP]
exact s.refl'
[GOAL]
case symm
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {x y : M}, ConGen.Rel r x y → Setoid.r x y → Setoid.r y x
[PROOFSTEP]
exact fun _ => s.symm'
[GOAL]
case trans
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {x y z : M}, ConGen.Rel r x y → ConGen.Rel r y z → Setoid.r x y → Setoid.r y z → Setoid.r x z
[PROOFSTEP]
exact fun _ _ => s.trans'
[GOAL]
case mul
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → Setoid.r w x → Setoid.r y z → Setoid.r (w * y) (x * z)
[PROOFSTEP]
exact fun _ _ => s.mul
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ : Con M
r : M → M → Prop
c : Con M
h : ∀ (x y : M), r x y → Setoid.r x y
⊢ conGen r ≤ c
[PROOFSTEP]
rw [conGen_eq]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ : Con M
r : M → M → Prop
c : Con M
h : ∀ (x y : M), r x y → Setoid.r x y
⊢ sInf {s | ∀ (x y : M), r x y → ↑s x y} ≤ c
[PROOFSTEP]
exact sInf_le h
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c : Con M
⊢ conGen ↑c ≤ c
[PROOFSTEP]
rw [conGen_eq]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c : Con M
⊢ sInf {s | ∀ (x y : M), ↑c x y → ↑s x y} ≤ c
[PROOFSTEP]
exact sInf_le fun _ _ => id
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
⊢ c ⊔ d = conGen fun x y => ↑c x y ∨ ↑d x y
[PROOFSTEP]
rw [conGen_eq]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
⊢ c ⊔ d = sInf {s | ∀ (x y : M), ↑c x y ∨ ↑d x y → ↑s x y}
[PROOFSTEP]
apply congr_arg sInf
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
⊢ {x | c ≤ x ∧ d ≤ x} = {s | ∀ (x y : M), ↑c x y ∨ ↑d x y → ↑s x y}
[PROOFSTEP]
simp only [le_def, or_imp, ← forall_and]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
⊢ c ⊔ d = conGen (r ⊔ r)
[PROOFSTEP]
rw [sup_eq_conGen]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
⊢ (conGen fun x y => ↑c x y ∨ ↑d x y) = conGen (r ⊔ r)
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
⊢ sSup S = conGen fun x y => ∃ c, c ∈ S ∧ ↑c x y
[PROOFSTEP]
rw [conGen_eq]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
⊢ sSup S = sInf {s | ∀ (x y : M), (∃ c, c ∈ S ∧ ↑c x y) → ↑s x y}
[PROOFSTEP]
apply congr_arg sInf
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
⊢ upperBounds S = {s | ∀ (x y : M), (∃ c, c ∈ S ∧ ↑c x y) → ↑s x y}
[PROOFSTEP]
ext
[GOAL]
case h
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
x✝ : Con M
⊢ x✝ ∈ upperBounds S ↔ x✝ ∈ {s | ∀ (x y : M), (∃ c, c ∈ S ∧ ↑c x y) → ↑s x y}
[PROOFSTEP]
exact ⟨fun h _ _ ⟨r, hr⟩ => h hr.1 hr.2, fun h r hS _ _ hr => h _ _ ⟨r, hS, hr⟩⟩
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
⊢ sSup S = conGen (sSup (FunLike.coe '' S))
[PROOFSTEP]
rw [sSup_eq_conGen, sSup_image]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
⊢ (conGen fun x y => ∃ c, c ∈ S ∧ ↑c x y) = conGen (⨆ (a : Con M) (_ : a ∈ S), ↑a)
[PROOFSTEP]
congr with (x y)
[GOAL]
case e_r.h.h.a
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
x y : M
⊢ (∃ c, c ∈ S ∧ ↑c x y) ↔ iSup (fun a => ⨆ (_ : a ∈ S), ↑a) x y
[PROOFSTEP]
simp only [sSup_image, iSup_apply, iSup_Prop_eq, exists_prop, rel_eq_coe]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
h : mulKer f H ≤ c
hf : Surjective f
src✝ : Setoid N := Setoid.mapOfSurjective c.toSetoid f h hf
w✝ x✝ y✝ z✝ : N
h₁ : r w✝ x✝
h₂ : r y✝ z✝
⊢ r (w✝ * y✝) (x✝ * z✝)
[PROOFSTEP]
rcases h₁ with ⟨a, b, rfl, rfl, h1⟩
[GOAL]
case intro.intro.intro.intro
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
h : mulKer f H ≤ c
hf : Surjective f
src✝ : Setoid N := Setoid.mapOfSurjective c.toSetoid f h hf
y✝ z✝ : N
h₂ : r y✝ z✝
a b : M
h1 : Rel c.toSetoid a b
⊢ r (f a * y✝) (f b * z✝)
[PROOFSTEP]
rcases h₂ with ⟨p, q, rfl, rfl, h2⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
h : mulKer f H ≤ c
hf : Surjective f
src✝ : Setoid N := Setoid.mapOfSurjective c.toSetoid f h hf
a b : M
h1 : Rel c.toSetoid a b
p q : M
h2 : Rel c.toSetoid p q
⊢ r (f a * f p) (f b * f q)
[PROOFSTEP]
exact ⟨a * p, b * q, by rw [H], by rw [H], c.mul h1 h2⟩
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
h : mulKer f H ≤ c
hf : Surjective f
src✝ : Setoid N := Setoid.mapOfSurjective c.toSetoid f h hf
a b : M
h1 : Rel c.toSetoid a b
p q : M
h2 : Rel c.toSetoid p q
⊢ f (a * p) = f a * f p
[PROOFSTEP]
rw [H]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
h : mulKer f H ≤ c
hf : Surjective f
src✝ : Setoid N := Setoid.mapOfSurjective c.toSetoid f h hf
a b : M
h1 : Rel c.toSetoid a b
p q : M
h2 : Rel c.toSetoid p q
⊢ f (b * q) = f b * f q
[PROOFSTEP]
rw [H]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
h : mulKer f H ≤ c
hf : Surjective f
⊢ mapGen c f = mapOfSurjective c f H h hf
[PROOFSTEP]
rw [← conGen_of_con (c.mapOfSurjective f H h hf)]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
h : mulKer f H ≤ c
hf : Surjective f
⊢ mapGen c f = conGen ↑(mapOfSurjective c f H h hf)
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
c : Con N
src✝ : Setoid M := Setoid.comap f c.toSetoid
w x y z : M
h1 : r w x
h2 : r y z
⊢ ↑c (f (w * y)) (f (x * z))
[PROOFSTEP]
rw [H, H]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
c : Con N
src✝ : Setoid M := Setoid.comap f c.toSetoid
w x y z : M
h1 : r w x
h2 : r y z
⊢ ↑c (f w * f y) (f x * f z)
[PROOFSTEP]
exact c.mul h1 h2
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
d : { d // c ≤ d }
⊢ mulKer toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑x * ↑y) ≤ ↑d
[PROOFSTEP]
rw [mul_ker_mk_eq]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
d : { d // c ≤ d }
⊢ c ≤ ↑d
[PROOFSTEP]
exact d.2
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
d : Con (Con.Quotient c)
x y : M
h : ↑c x y
⊢ ↑d ↑x ↑y
[PROOFSTEP]
rw [c.eq.2 h]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
d : Con (Con.Quotient c)
x y : M
h : ↑c x y
⊢ ↑d ↑y ↑y
[PROOFSTEP]
exact d.refl _
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
d : { d // c ≤ d }
⊢ (fun d =>
        { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
          property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
      ((fun d =>
          mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
            (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
            (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
        d) =
    d
[PROOFSTEP]
exact
  Subtype.ext_iff_val.2 <|
    ext fun x y =>
      ⟨fun h =>
        let ⟨a, b, hx, hy, H⟩ := h
        d.1.trans (d.1.symm <| d.2 <| c.eq.1 hx) <| d.1.trans H <| d.2 <| c.eq.1 hy,
        fun h => ⟨_, _, rfl, rfl, h⟩⟩
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
d : Con (Con.Quotient c)
⊢ (fun d =>
        mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
          (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
          (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
      ((fun d =>
          { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
            property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
        d) =
    d
[PROOFSTEP]
exact
  ext fun x y =>
    ⟨fun h =>
      let ⟨_, _, hx, hy, H⟩ := h
      hx ▸ hy ▸ H,
      Con.induction_on₂ x y fun w z h => ⟨w, z, rfl, rfl, h⟩⟩
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
s t : { d // c ≤ d }
⊢ ↑{
            toFun := fun d =>
              mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q),
            invFun := fun d =>
              { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) },
            left_inv :=
              (_ :
                ∀ (d : { d // c ≤ d }),
                  (fun d =>
                        { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                          property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                      ((fun d =>
                          mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                            (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                            (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                        d) =
                    d),
            right_inv :=
              (_ :
                ∀ (d : Con (Con.Quotient c)),
                  (fun d =>
                        mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                          (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                          (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                      ((fun d =>
                          { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                            property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                        d) =
                    d) }
        s ≤
      ↑{
            toFun := fun d =>
              mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q),
            invFun := fun d =>
              { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) },
            left_inv :=
              (_ :
                ∀ (d : { d // c ≤ d }),
                  (fun d =>
                        { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                          property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                      ((fun d =>
                          mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                            (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                            (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                        d) =
                    d),
            right_inv :=
              (_ :
                ∀ (d : Con (Con.Quotient c)),
                  (fun d =>
                        mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                          (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                          (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                      ((fun d =>
                          { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                            property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                        d) =
                    d) }
        t ↔
    s ≤ t
[PROOFSTEP]
constructor
[GOAL]
case mp
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
s t : { d // c ≤ d }
⊢ ↑{
            toFun := fun d =>
              mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q),
            invFun := fun d =>
              { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) },
            left_inv :=
              (_ :
                ∀ (d : { d // c ≤ d }),
                  (fun d =>
                        { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                          property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                      ((fun d =>
                          mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                            (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                            (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                        d) =
                    d),
            right_inv :=
              (_ :
                ∀ (d : Con (Con.Quotient c)),
                  (fun d =>
                        mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                          (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                          (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                      ((fun d =>
                          { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                            property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                        d) =
                    d) }
        s ≤
      ↑{
            toFun := fun d =>
              mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q),
            invFun := fun d =>
              { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) },
            left_inv :=
              (_ :
                ∀ (d : { d // c ≤ d }),
                  (fun d =>
                        { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                          property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                      ((fun d =>
                          mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                            (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                            (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                        d) =
                    d),
            right_inv :=
              (_ :
                ∀ (d : Con (Con.Quotient c)),
                  (fun d =>
                        mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                          (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                          (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                      ((fun d =>
                          { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                            property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                        d) =
                    d) }
        t →
    s ≤ t
[PROOFSTEP]
intros h x y hs
[GOAL]
case mp
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
s t : { d // c ≤ d }
h :
  ↑{
          toFun := fun d =>
            mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
              (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
              (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q),
          invFun := fun d =>
            { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
              property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) },
          left_inv :=
            (_ :
              ∀ (d : { d // c ≤ d }),
                (fun d =>
                      { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                        property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                    ((fun d =>
                        mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                          (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                          (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                      d) =
                  d),
          right_inv :=
            (_ :
              ∀ (d : Con (Con.Quotient c)),
                (fun d =>
                      mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                        (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                        (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                    ((fun d =>
                        { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                          property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                      d) =
                  d) }
      s ≤
    ↑{
          toFun := fun d =>
            mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
              (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
              (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q),
          invFun := fun d =>
            { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
              property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) },
          left_inv :=
            (_ :
              ∀ (d : { d // c ≤ d }),
                (fun d =>
                      { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                        property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                    ((fun d =>
                        mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                          (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                          (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                      d) =
                  d),
          right_inv :=
            (_ :
              ∀ (d : Con (Con.Quotient c)),
                (fun d =>
                      mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                        (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                        (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                    ((fun d =>
                        { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                          property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                      d) =
                  d) }
      t
x y : M
hs : ↑↑s x y
⊢ ↑↑t x y
[PROOFSTEP]
rcases h ⟨x, y, rfl, rfl, hs⟩ with ⟨a, b, hx, hy, ht⟩
[GOAL]
case mp.intro.intro.intro.intro
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
s t : { d // c ≤ d }
h :
  ↑{
          toFun := fun d =>
            mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
              (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
              (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q),
          invFun := fun d =>
            { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
              property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) },
          left_inv :=
            (_ :
              ∀ (d : { d // c ≤ d }),
                (fun d =>
                      { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                        property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                    ((fun d =>
                        mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                          (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                          (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                      d) =
                  d),
          right_inv :=
            (_ :
              ∀ (d : Con (Con.Quotient c)),
                (fun d =>
                      mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                        (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                        (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                    ((fun d =>
                        { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                          property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                      d) =
                  d) }
      s ≤
    ↑{
          toFun := fun d =>
            mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
              (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
              (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q),
          invFun := fun d =>
            { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
              property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) },
          left_inv :=
            (_ :
              ∀ (d : { d // c ≤ d }),
                (fun d =>
                      { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                        property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                    ((fun d =>
                        mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                          (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                          (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                      d) =
                  d),
          right_inv :=
            (_ :
              ∀ (d : Con (Con.Quotient c)),
                (fun d =>
                      mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                        (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                        (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                    ((fun d =>
                        { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                          property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                      d) =
                  d) }
      t
x y : M
hs : ↑↑s x y
a b : M
hx : ↑a = ↑x
hy : ↑b = ↑y
ht : Rel (↑t).toSetoid a b
⊢ ↑↑t x y
[PROOFSTEP]
exact t.1.trans (t.1.symm <| t.2 <| eq_rel.1 hx) (t.1.trans ht (t.2 <| eq_rel.1 hy))
[GOAL]
case mpr
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
s t : { d // c ≤ d }
⊢ s ≤ t →
    ↑{
            toFun := fun d =>
              mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q),
            invFun := fun d =>
              { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) },
            left_inv :=
              (_ :
                ∀ (d : { d // c ≤ d }),
                  (fun d =>
                        { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                          property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                      ((fun d =>
                          mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                            (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                            (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                        d) =
                    d),
            right_inv :=
              (_ :
                ∀ (d : Con (Con.Quotient c)),
                  (fun d =>
                        mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                          (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                          (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                      ((fun d =>
                          { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                            property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                        d) =
                    d) }
        s ≤
      ↑{
            toFun := fun d =>
              mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q),
            invFun := fun d =>
              { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) },
            left_inv :=
              (_ :
                ∀ (d : { d // c ≤ d }),
                  (fun d =>
                        { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                          property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                      ((fun d =>
                          mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                            (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                            (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                        d) =
                    d),
            right_inv :=
              (_ :
                ∀ (d : Con (Con.Quotient c)),
                  (fun d =>
                        mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                          (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                          (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                      ((fun d =>
                          { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                            property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                        d) =
                    d) }
        t
[PROOFSTEP]
intros h _ _ hs
[GOAL]
case mpr
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
s t : { d // c ≤ d }
h : s ≤ t
x✝ y✝ : Con.Quotient c
hs :
  ↑(↑{
            toFun := fun d =>
              mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q),
            invFun := fun d =>
              { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) },
            left_inv :=
              (_ :
                ∀ (d : { d // c ≤ d }),
                  (fun d =>
                        { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                          property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                      ((fun d =>
                          mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                            (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                            (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                        d) =
                    d),
            right_inv :=
              (_ :
                ∀ (d : Con (Con.Quotient c)),
                  (fun d =>
                        mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                          (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                          (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                      ((fun d =>
                          { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                            property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                        d) =
                    d) }
        s)
    x✝ y✝
⊢ ↑(↑{
            toFun := fun d =>
              mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q),
            invFun := fun d =>
              { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) },
            left_inv :=
              (_ :
                ∀ (d : { d // c ≤ d }),
                  (fun d =>
                        { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                          property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                      ((fun d =>
                          mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                            (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                            (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                        d) =
                    d),
            right_inv :=
              (_ :
                ∀ (d : Con (Con.Quotient c)),
                  (fun d =>
                        mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                          (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                          (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                      ((fun d =>
                          { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                            property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                        d) =
                    d) }
        t)
    x✝ y✝
[PROOFSTEP]
rcases hs with ⟨a, b, hx, hy, Hs⟩
[GOAL]
case mpr.intro.intro.intro.intro
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
s t : { d // c ≤ d }
h : s ≤ t
x✝ y✝ : Con.Quotient c
a b : M
hx : ↑a = x✝
hy : ↑b = y✝
Hs : Rel (↑s).toSetoid a b
⊢ ↑(↑{
            toFun := fun d =>
              mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q),
            invFun := fun d =>
              { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) },
            left_inv :=
              (_ :
                ∀ (d : { d // c ≤ d }),
                  (fun d =>
                        { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                          property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                      ((fun d =>
                          mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                            (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                            (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                        d) =
                    d),
            right_inv :=
              (_ :
                ∀ (d : Con (Con.Quotient c)),
                  (fun d =>
                        mapOfSurjective (↑d) toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1))
                          (_ : mulKer toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) ≤ ↑d)
                          (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q))
                      ((fun d =>
                          { val := comap toQuotient (_ : ∀ (x y : M), ↑(x * y) = ↑(x * y)) d,
                            property := (_ : ∀ (x y : M), ↑c x y → ↑d ↑x ↑y) })
                        d) =
                    d) }
        t)
    x✝ y✝
[PROOFSTEP]
exact ⟨a, b, hx, hy, h Hs⟩
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f : N →* M
x y : N
⊢ ↑c (↑f x) (↑f y) ↔ ↑(mk' c) (↑f x) = ↑(mk' c) (↑f y)
[PROOFSTEP]
rw [← c.eq]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f : N →* M
x y : N
⊢ ↑(↑f x) = ↑(↑f y) ↔ ↑(mk' c) (↑f x) = ↑(mk' c) (↑f y)
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f : M →* P
H : c ≤ ker f
⊢ (fun x => Con.liftOn x ↑f (_ : ∀ (x x_1 : M), ↑c x x_1 → ↑(ker f) x x_1)) 1 = 1
[PROOFSTEP]
rw [← f.map_one]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f : M →* P
H : c ≤ ker f
⊢ (fun x => Con.liftOn x ↑f (_ : ∀ (x x_1 : M), ↑c x x_1 → ↑(ker f) x x_1)) 1 = ↑f 1
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f : M →* P
H : c ≤ ker f
x y : Con.Quotient c
m n : M
⊢ OneHom.toFun
      { toFun := fun x => Con.liftOn x ↑f (_ : ∀ (x x_1 : M), ↑c x x_1 → ↑(ker f) x x_1),
        map_one' := (_ : (fun x => Con.liftOn x ↑f (_ : ∀ (x x_1 : M), ↑c x x_1 → ↑(ker f) x x_1)) 1 = 1) }
      (↑m * ↑n) =
    OneHom.toFun
        { toFun := fun x => Con.liftOn x ↑f (_ : ∀ (x x_1 : M), ↑c x x_1 → ↑(ker f) x x_1),
          map_one' := (_ : (fun x => Con.liftOn x ↑f (_ : ∀ (x x_1 : M), ↑c x x_1 → ↑(ker f) x x_1)) 1 = 1) }
        ↑m *
      OneHom.toFun
        { toFun := fun x => Con.liftOn x ↑f (_ : ∀ (x x_1 : M), ↑c x x_1 → ↑(ker f) x x_1),
          map_one' := (_ : (fun x => Con.liftOn x ↑f (_ : ∀ (x x_1 : M), ↑c x x_1 → ↑(ker f) x x_1)) 1 = 1) }
        ↑n
[PROOFSTEP]
dsimp only [← coe_mul, Con.liftOn_coe]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f : M →* P
H : c ≤ ker f
x y : Con.Quotient c
m n : M
⊢ ↑f (m * n) = ↑f m * ↑f n
[PROOFSTEP]
rw [map_mul]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f : M →* P
H : c ≤ ker f
⊢ MonoidHom.comp (lift c f H) (mk' c) = f
[PROOFSTEP]
ext
[GOAL]
case h
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f : M →* P
H : c ≤ ker f
x✝ : M
⊢ ↑(MonoidHom.comp (lift c f H) (mk' c)) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f✝ : M →* P
f : Con.Quotient c →* P
x y : M
h : ↑c x y
⊢ ↑f ↑x = ↑f ↑y
[PROOFSTEP]
rw [c.eq.2 h]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f✝ : M →* P
f : Con.Quotient c →* P
⊢ lift c (MonoidHom.comp f (mk' c)) (_ : ∀ (x y : M), ↑c x y → ↑f ↑x = ↑f ↑y) = f
[PROOFSTEP]
ext x
[GOAL]
case h
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
f✝ : M →* P
f : Con.Quotient c →* P
x : Con.Quotient c
⊢ ↑(lift c (MonoidHom.comp f (mk' c)) (_ : ∀ (x y : M), ↑c x y → ↑f ↑x = ↑f ↑y)) x = ↑f x
[PROOFSTEP]
rcases x with ⟨⟩
[GOAL]
case h.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
f✝ : M →* P
f : Con.Quotient c →* P
x : Con.Quotient c
a✝ : M
⊢ ↑(lift c (MonoidHom.comp f (mk' c)) (_ : ∀ (x y : M), ↑c x y → ↑f ↑x = ↑f ↑y)) (Quot.mk r a✝) = ↑f (Quot.mk r a✝)
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f✝ : M →* P
f g : Con.Quotient c →* P
h : ∀ (a : M), ↑f ↑a = ↑g ↑a
⊢ f = g
[PROOFSTEP]
rw [← lift_apply_mk' f, ← lift_apply_mk' g]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f✝ : M →* P
f g : Con.Quotient c →* P
h : ∀ (a : M), ↑f ↑a = ↑g ↑a
⊢ lift c (MonoidHom.comp f (mk' c)) (_ : ∀ (x y : M), ↑c x y → ↑f ↑x = ↑f ↑y) =
    lift c (MonoidHom.comp g (mk' c)) (_ : ∀ (x y : M), ↑c x y → ↑g ↑x = ↑g ↑y)
[PROOFSTEP]
congr 1
[GOAL]
case e_f
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f✝ : M →* P
f g : Con.Quotient c →* P
h : ∀ (a : M), ↑f ↑a = ↑g ↑a
⊢ MonoidHom.comp f (mk' c) = MonoidHom.comp g (mk' c)
[PROOFSTEP]
exact FunLike.ext_iff.2 h
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
f : M →* P
H : c ≤ ker f
g : Con.Quotient c →* P
Hg : MonoidHom.comp g (mk' c) = f
x : M
⊢ ↑g ↑x = ↑(lift c f H) ↑x
[PROOFSTEP]
subst f
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
g : Con.Quotient c →* P
x : M
H : c ≤ ker (MonoidHom.comp g (mk' c))
⊢ ↑g ↑x = ↑(lift c (MonoidHom.comp g (mk' c)) H) ↑x
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
f : M →* P
H : c ≤ ker f
x : P
⊢ x ∈ MonoidHom.mrange (lift c f H) → x ∈ MonoidHom.mrange f
[PROOFSTEP]
rintro ⟨⟨y⟩, hy⟩
[GOAL]
case intro.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f : M →* P
H : c ≤ ker f
x : P
w✝ : Con.Quotient c
y : M
hy : ↑(lift c f H) (Quot.mk r y) = x
⊢ x ∈ MonoidHom.mrange f
[PROOFSTEP]
exact ⟨y, hy⟩
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f✝ f : M →* P
x y : Con.Quotient (ker f)
h : (fun x => ↑(MonoidHom.mrangeRestrict (kerLift f)) x) x = (fun x => ↑(MonoidHom.mrangeRestrict (kerLift f)) x) y
⊢ ↑(kerLift f) x = ↑(kerLift f) y
[PROOFSTEP]
rcases x with ⟨⟩
[GOAL]
case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f✝ f : M →* P
x y : Con.Quotient (ker f)
a✝ : M
h :
  (fun x => ↑(MonoidHom.mrangeRestrict (kerLift f)) x) (Quot.mk r a✝) =
    (fun x => ↑(MonoidHom.mrangeRestrict (kerLift f)) x) y
⊢ ↑(kerLift f) (Quot.mk r a✝) = ↑(kerLift f) y
[PROOFSTEP]
rcases y with ⟨⟩
[GOAL]
case mk.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f✝ f : M →* P
x y : Con.Quotient (ker f)
a✝¹ a✝ : M
h :
  (fun x => ↑(MonoidHom.mrangeRestrict (kerLift f)) x) (Quot.mk r a✝¹) =
    (fun x => ↑(MonoidHom.mrangeRestrict (kerLift f)) x) (Quot.mk r a✝)
⊢ ↑(kerLift f) (Quot.mk r a✝¹) = ↑(kerLift f) (Quot.mk r a✝)
[PROOFSTEP]
injections
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f✝ f : M →* P
x✝ : { x // x ∈ MonoidHom.mrange (kerLift f) }
w : P
z : Con.Quotient (ker f)
hz : ↑(kerLift f) z = w
⊢ (fun x => ↑(MonoidHom.mrangeRestrict (kerLift f)) x) z = { val := w, property := (_ : ∃ y, ↑(kerLift f) y = w) }
[PROOFSTEP]
rcases hz with ⟨⟩
[GOAL]
case refl
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f✝ f : M →* P
x✝ : { x // x ∈ MonoidHom.mrange (kerLift f) }
z : Con.Quotient (ker f)
⊢ (fun x => ↑(MonoidHom.mrangeRestrict (kerLift f)) x) z =
    { val := ↑(kerLift f) z, property := (_ : ∃ y, ↑(kerLift f) y = ↑(kerLift f) z) }
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
f✝ f : M →* P
g : P → M
hf : Function.RightInverse g ↑f
src✝ : Con.Quotient (ker f) →* P := kerLift f
x : Con.Quotient (ker f)
⊢ ↑(kerLift f) ((toQuotient ∘ g) (↑(kerLift f) x)) = ↑(kerLift f) x
[PROOFSTEP]
rw [Function.comp_apply, kerLift_mk, hf]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
f✝ f : M →* P
g : P → M
hf : Function.RightInverse g ↑f
src✝ : Con.Quotient (ker f) →* P := kerLift f
x : P
⊢ ↑(kerLift f) ((toQuotient ∘ g) x) = x
[PROOFSTEP]
conv_rhs => rw [← hf x]; rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
f✝ f : M →* P
g : P → M
hf : Function.RightInverse g ↑f
src✝ : Con.Quotient (ker f) →* P := kerLift f
x : P
| x
[PROOFSTEP]
rw [← hf x]; rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
f✝ f : M →* P
g : P → M
hf : Function.RightInverse g ↑f
src✝ : Con.Quotient (ker f) →* P := kerLift f
x : P
| x
[PROOFSTEP]
rw [← hf x]; rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
f✝ f : M →* P
g : P → M
hf : Function.RightInverse g ↑f
src✝ : Con.Quotient (ker f) →* P := kerLift f
x : P
| x
[PROOFSTEP]
rw [← hf x]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
f✝ f : M →* P
g : P → M
hf : Function.RightInverse g ↑f
src✝ : Con.Quotient (ker f) →* P := kerLift f
x : P
| ↑f (g x)
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c✝ : Con M
x✝ y✝ : M
f : M →* P
c d : Con M
h : c ≤ d
src✝ : Quotient (Setoid.ker (Quot.mapRight h)) ≃ Quotient d.toSetoid :=
  Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h
x y : Con.Quotient (ker (map c d h))
w z : Con.Quotient c
a b : M
⊢ Equiv.toFun
      { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (↑↑a * ↑↑b) =
    ↑(mk' d) a * ↑(mk' d) b
[PROOFSTEP]
rw [← d.mk'.map_mul]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c✝ : Con M
x✝ y✝ : M
f : M →* P
c d : Con M
h : c ≤ d
src✝ : Quotient (Setoid.ker (Quot.mapRight h)) ≃ Quotient d.toSetoid :=
  Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h
x y : Con.Quotient (ker (map c d h))
w z : Con.Quotient c
a b : M
⊢ Equiv.toFun
      { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (↑↑a * ↑↑b) =
    ↑(mk' d) (a * b)
[PROOFSTEP]
rfl
[GOAL]
M✝ : Type u_1
N : Type u_2
P : Type u_3
M : Type u_4
inst✝ : Monoid M
c : Con M
w x : M
x✝ : ↑c w x
⊢ ↑c (w ^ 0) (x ^ 0)
[PROOFSTEP]
simpa using c.refl _
[GOAL]
M✝ : Type u_1
N : Type u_2
P : Type u_3
M : Type u_4
inst✝ : Monoid M
c : Con M
n : ℕ
w x : M
h : ↑c w x
⊢ ↑c (w ^ Nat.succ n) (x ^ Nat.succ n)
[PROOFSTEP]
simpa [pow_succ] using c.mul h (Con.pow c n h)
[GOAL]
M✝ : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
M : Type u_5
inst✝² : MulOneClass M
inst✝¹ : SMul α M
inst✝ : IsScalarTower α M M
c : Con M
a : α
w x : M
h : ↑c w x
⊢ ↑c (a • w) (a • x)
[PROOFSTEP]
simpa only [smul_one_mul] using c.mul (c.refl' (a • (1 : M) : M)) h
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
c : Con M
x y : M
h : ↑c x y
⊢ ↑c x⁻¹ y⁻¹
[PROOFSTEP]
simpa using c.symm (c.mul (c.mul (c.refl x⁻¹) h) (c.refl y⁻¹))
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
c : Con M
w x y z : M
h1 : ↑c w x
h2 : ↑c y z
⊢ ↑c (w / y) (x / z)
[PROOFSTEP]
simpa only [div_eq_mul_inv] using c.mul h1 (c.inv h2)
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
c : Con M
n : ℕ
w x : M
h : ↑c w x
⊢ ↑c (w ^ Int.ofNat n) (x ^ Int.ofNat n)
[PROOFSTEP]
simpa only [zpow_ofNat, Int.ofNat_eq_coe] using c.pow n h
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
c : Con M
n : ℕ
w x : M
h : ↑c w x
⊢ ↑c (w ^ Int.negSucc n) (x ^ Int.negSucc n)
[PROOFSTEP]
simpa only [zpow_negSucc] using c.inv (c.pow _ h)
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : (Con.Quotient c)ˣ
f : (x y : M) → ↑c (x * y) 1 → ↑c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : ↑c (x * y) 1) (hyx : ↑c (y * x) 1) (x' y' : M) (hxy' : ↑c (x' * y') 1) (hyx' : ↑c (y' * x') 1),
    ↑c x x' → ↑c y y' → f x y hxy hyx = f x' y' hxy' hyx'
⊢ α
[PROOFSTEP]
refine'
  @Con.hrecOn₂ M M _ _ c c (fun x y => x * y = 1 → y * x = 1 → α) (u : c.Quotient) (↑u⁻¹ : c.Quotient)
    (fun (x y : M) (hxy : (x * y : c.Quotient) = 1) (hyx : (y * x : c.Quotient) = 1) => f x y (c.eq.1 hxy) (c.eq.1 hyx))
    (fun x y x' y' hx hy => _) u.3 u.4
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : (Con.Quotient c)ˣ
f : (x y : M) → ↑c (x * y) 1 → ↑c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : ↑c (x * y) 1) (hyx : ↑c (y * x) 1) (x' y' : M) (hxy' : ↑c (x' * y') 1) (hyx' : ↑c (y' * x') 1),
    ↑c x x' → ↑c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : ↑c x x'
hy : ↑c y y'
⊢ HEq ((fun x y hxy hyx => f x y (_ : ↑c (x * y) 1) (_ : ↑c (y * x) 1)) x y)
    ((fun x y hxy hyx => f x y (_ : ↑c (x * y) 1) (_ : ↑c (y * x) 1)) x' y')
[PROOFSTEP]
refine' Function.hfunext _ _
[GOAL]
case refine'_1
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : (Con.Quotient c)ˣ
f : (x y : M) → ↑c (x * y) 1 → ↑c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : ↑c (x * y) 1) (hyx : ↑c (y * x) 1) (x' y' : M) (hxy' : ↑c (x' * y') 1) (hyx' : ↑c (y' * x') 1),
    ↑c x x' → ↑c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : ↑c x x'
hy : ↑c y y'
⊢ (↑x * ↑y = 1) = (↑x' * ↑y' = 1)
case refine'_2
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : (Con.Quotient c)ˣ
f : (x y : M) → ↑c (x * y) 1 → ↑c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : ↑c (x * y) 1) (hyx : ↑c (y * x) 1) (x' y' : M) (hxy' : ↑c (x' * y') 1) (hyx' : ↑c (y' * x') 1),
    ↑c x x' → ↑c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : ↑c x x'
hy : ↑c y y'
⊢ ∀ (a : ↑x * ↑y = 1) (a' : ↑x' * ↑y' = 1),
    HEq a a' →
      HEq ((fun x y hxy hyx => f x y (_ : ↑c (x * y) 1) (_ : ↑c (y * x) 1)) x y a)
        ((fun x y hxy hyx => f x y (_ : ↑c (x * y) 1) (_ : ↑c (y * x) 1)) x' y' a')
[PROOFSTEP]
rw [c.eq.2 hx, c.eq.2 hy]
[GOAL]
case refine'_2
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : (Con.Quotient c)ˣ
f : (x y : M) → ↑c (x * y) 1 → ↑c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : ↑c (x * y) 1) (hyx : ↑c (y * x) 1) (x' y' : M) (hxy' : ↑c (x' * y') 1) (hyx' : ↑c (y' * x') 1),
    ↑c x x' → ↑c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : ↑c x x'
hy : ↑c y y'
⊢ ∀ (a : ↑x * ↑y = 1) (a' : ↑x' * ↑y' = 1),
    HEq a a' →
      HEq ((fun x y hxy hyx => f x y (_ : ↑c (x * y) 1) (_ : ↑c (y * x) 1)) x y a)
        ((fun x y hxy hyx => f x y (_ : ↑c (x * y) 1) (_ : ↑c (y * x) 1)) x' y' a')
[PROOFSTEP]
rintro Hxy Hxy' -
[GOAL]
case refine'_2
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : (Con.Quotient c)ˣ
f : (x y : M) → ↑c (x * y) 1 → ↑c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : ↑c (x * y) 1) (hyx : ↑c (y * x) 1) (x' y' : M) (hxy' : ↑c (x' * y') 1) (hyx' : ↑c (y' * x') 1),
    ↑c x x' → ↑c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : ↑c x x'
hy : ↑c y y'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ HEq ((fun x y hxy hyx => f x y (_ : ↑c (x * y) 1) (_ : ↑c (y * x) 1)) x y Hxy)
    ((fun x y hxy hyx => f x y (_ : ↑c (x * y) 1) (_ : ↑c (y * x) 1)) x' y' Hxy')
[PROOFSTEP]
refine' Function.hfunext _ _
[GOAL]
case refine'_2.refine'_1
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : (Con.Quotient c)ˣ
f : (x y : M) → ↑c (x * y) 1 → ↑c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : ↑c (x * y) 1) (hyx : ↑c (y * x) 1) (x' y' : M) (hxy' : ↑c (x' * y') 1) (hyx' : ↑c (y' * x') 1),
    ↑c x x' → ↑c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : ↑c x x'
hy : ↑c y y'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ (↑y * ↑x = 1) = (↑y' * ↑x' = 1)
[PROOFSTEP]
rw [c.eq.2 hx, c.eq.2 hy]
[GOAL]
case refine'_2.refine'_2
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : (Con.Quotient c)ˣ
f : (x y : M) → ↑c (x * y) 1 → ↑c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : ↑c (x * y) 1) (hyx : ↑c (y * x) 1) (x' y' : M) (hxy' : ↑c (x' * y') 1) (hyx' : ↑c (y' * x') 1),
    ↑c x x' → ↑c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : ↑c x x'
hy : ↑c y y'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ ∀ (a : ↑y * ↑x = 1) (a' : ↑y' * ↑x' = 1),
    HEq a a' →
      HEq ((fun x y hxy hyx => f x y (_ : ↑c (x * y) 1) (_ : ↑c (y * x) 1)) x y Hxy a)
        ((fun x y hxy hyx => f x y (_ : ↑c (x * y) 1) (_ : ↑c (y * x) 1)) x' y' Hxy' a')
[PROOFSTEP]
rintro Hyx Hyx' -
[GOAL]
case refine'_2.refine'_2
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : (Con.Quotient c)ˣ
f : (x y : M) → ↑c (x * y) 1 → ↑c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : ↑c (x * y) 1) (hyx : ↑c (y * x) 1) (x' y' : M) (hxy' : ↑c (x' * y') 1) (hyx' : ↑c (y' * x') 1),
    ↑c x x' → ↑c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : ↑c x x'
hy : ↑c y y'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
Hyx : ↑y * ↑x = 1
Hyx' : ↑y' * ↑x' = 1
⊢ HEq ((fun x y hxy hyx => f x y (_ : ↑c (x * y) 1) (_ : ↑c (y * x) 1)) x y Hxy Hyx)
    ((fun x y hxy hyx => f x y (_ : ↑c (x * y) 1) (_ : ↑c (y * x) 1)) x' y' Hxy' Hyx')
[PROOFSTEP]
exact heq_of_eq (Hf _ _ _ _ _ _ _ _ hx hy)
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
p : (Con.Quotient c)ˣ → Prop
u : (Con.Quotient c)ˣ
H :
  ∀ (x y : M) (hxy : ↑c (x * y) 1) (hyx : ↑c (y * x) 1),
    p
      { val := ↑x, inv := ↑y, val_inv := (_ : ↑((fun x x_1 => x * x_1) x y) = ↑1),
        inv_val := (_ : ↑((fun x x_1 => x * x_1) y x) = ↑1) }
⊢ p u
[PROOFSTEP]
rcases u with ⟨⟨x⟩, ⟨y⟩, h₁, h₂⟩
[GOAL]
case mk.mk.mk
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
p : (Con.Quotient c)ˣ → Prop
H :
  ∀ (x y : M) (hxy : ↑c (x * y) 1) (hyx : ↑c (y * x) 1),
    p
      { val := ↑x, inv := ↑y, val_inv := (_ : ↑((fun x x_1 => x * x_1) x y) = ↑1),
        inv_val := (_ : ↑((fun x x_1 => x * x_1) y x) = ↑1) }
val✝ inv✝ : Con.Quotient c
x y : M
h₁ : Quot.mk r x * Quot.mk r y = 1
h₂ : Quot.mk r y * Quot.mk r x = 1
⊢ p { val := Quot.mk r x, inv := Quot.mk r y, val_inv := h₁, inv_val := h₂ }
[PROOFSTEP]
exact H x y (c.eq.1 h₁) (c.eq.1 h₂)