case mk.mk.mk
M : Type u_1
N : Type ?u.116933
P : Type ?u.116936
α : Type ?u.116939
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₂ }
M : Type u_1
N : Type ?u.116933
P : Type ?u.116936
α : Type ?u.116939
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
rcases u with ⟨⟨x⟩, ⟨y⟩, h₁, h₂⟩
no goals
case mk.mk.mk
M : Type u_1
N : Type ?u.116933
P : Type ?u.116936
α : Type ?u.116939
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₂ }
exact H x y (c.eq.1 h₁) (c.eq.1 h₂)