[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₂)
