[GOAL]
S : Type u_1
inst✝ : UnitalShelf S
x y : S
⊢ (x ◃ y) ◃ x = x ◃ y
[PROOFSTEP]
have h : (x ◃ y) ◃ x = (x ◃ y) ◃ (x ◃ 1) := by rw [act_one]
[GOAL]
S : Type u_1
inst✝ : UnitalShelf S
x y : S
⊢ (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1
[PROOFSTEP]
rw [act_one]
[GOAL]
S : Type u_1
inst✝ : UnitalShelf S
x y : S
h : (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1
⊢ (x ◃ y) ◃ x = x ◃ y
[PROOFSTEP]
rw [h, ← Shelf.self_distrib, act_one]
[GOAL]
S : Type u_1
inst✝ : UnitalShelf S
x : S
⊢ x ◃ x = x
[PROOFSTEP]
rw [← act_one x, ← Shelf.self_distrib, act_one, act_one]
[GOAL]
S : Type u_1
inst✝ : UnitalShelf S
x y : S
⊢ x ◃ x ◃ y = x ◃ y
[PROOFSTEP]
have h : x ◃ (x ◃ y) = (x ◃ 1) ◃ (x ◃ y) := by rw [act_one]
[GOAL]
S : Type u_1
inst✝ : UnitalShelf S
x y : S
⊢ x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y
[PROOFSTEP]
rw [act_one]
[GOAL]
S : Type u_1
inst✝ : UnitalShelf S
x y : S
h : x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y
⊢ x ◃ x ◃ y = x ◃ y
[PROOFSTEP]
rw [h, ← Shelf.self_distrib, one_act]
[GOAL]
S : Type u_1
inst✝ : UnitalShelf S
x y z : S
⊢ (x ◃ y) ◃ z = x ◃ y ◃ z
[PROOFSTEP]
rw [self_distrib, self_distrib, act_act_self_eq, act_self_act_eq]
[GOAL]
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ x ◃ y = x ◃ y' ↔ y = y'
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ x ◃ y = x ◃ y' → y = y'
case mpr R : Type u_1 inst✝ : Rack R x y y' : R ⊢ y = y' → x ◃ y = x ◃ y'
[PROOFSTEP]
apply (act' x).injective
[GOAL]
case mpr
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ y = y' → x ◃ y = x ◃ y'
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ y = x ◃ y
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ x ◃⁻¹ y = x ◃⁻¹ y' ↔ y = y'
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ x ◃⁻¹ y = x ◃⁻¹ y' → y = y'
case mpr R : Type u_1 inst✝ : Rack R x y y' : R ⊢ y = y' → x ◃⁻¹ y = x ◃⁻¹ y'
[PROOFSTEP]
apply (act' x).symm.injective
[GOAL]
case mpr
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ y = y' → x ◃⁻¹ y = x ◃⁻¹ y'
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃⁻¹ y = x ◃⁻¹ y
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : Rack R
x y z : R
⊢ x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z
[PROOFSTEP]
rw [← left_cancel (x ◃⁻¹ y), right_inv, ← left_cancel x, right_inv, self_distrib]
[GOAL]
R : Type u_1
inst✝ : Rack R
x y z : R
⊢ (x ◃ x ◃⁻¹ y) ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z
[PROOFSTEP]
repeat' rw [right_inv]
[GOAL]
R : Type u_1
inst✝ : Rack R
x y z : R
⊢ (x ◃ x ◃⁻¹ y) ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z
[PROOFSTEP]
rw [right_inv]
[GOAL]
R : Type u_1
inst✝ : Rack R
x y z : R
⊢ y ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z
[PROOFSTEP]
rw [right_inv]
[GOAL]
R : Type u_1
inst✝ : Rack R
x y z : R
⊢ y ◃ y ◃⁻¹ z = z
[PROOFSTEP]
rw [right_inv]
[GOAL]
R✝ : Type u_1
inst✝¹ : Rack R✝
R : Type u_2
inst✝ : Rack R
x y : R
⊢ act' (x ◃ y) = act' x * act' y * (act' x)⁻¹
[PROOFSTEP]
rw [eq_mul_inv_iff_mul_eq]
[GOAL]
R✝ : Type u_1
inst✝¹ : Rack R✝
R : Type u_2
inst✝ : Rack R
x y : R
⊢ act' (x ◃ y) * act' x = act' x * act' y
[PROOFSTEP]
ext z
[GOAL]
case H
R✝ : Type u_1
inst✝¹ : Rack R✝
R : Type u_2
inst✝ : Rack R
x y z : R
⊢ ↑(act' (x ◃ y) * act' x) z = ↑(act' x * act' y) z
[PROOFSTEP]
apply self_distrib.symm
[GOAL]
R : Type u_1
inst✝ : Rack R
⊢ ∀ {x y z : Rᵐᵒᵖ},
    (fun x y => op (unop x ◃⁻¹ unop y)) x ((fun x y => op (unop x ◃⁻¹ unop y)) y z) =
      (fun x y => op (unop x ◃⁻¹ unop y)) ((fun x y => op (unop x ◃⁻¹ unop y)) x y)
        ((fun x y => op (unop x ◃⁻¹ unop y)) x z)
[PROOFSTEP]
intro x y z
[GOAL]
R : Type u_1
inst✝ : Rack R
x y z : Rᵐᵒᵖ
⊢ (fun x y => op (unop x ◃⁻¹ unop y)) x ((fun x y => op (unop x ◃⁻¹ unop y)) y z) =
    (fun x y => op (unop x ◃⁻¹ unop y)) ((fun x y => op (unop x ◃⁻¹ unop y)) x y)
      ((fun x y => op (unop x ◃⁻¹ unop y)) x z)
[PROOFSTEP]
induction x using MulOpposite.rec'
[GOAL]
case h
R : Type u_1
inst✝ : Rack R
y z : Rᵐᵒᵖ
X✝ : R
⊢ (fun x y => op (unop x ◃⁻¹ unop y)) (op X✝) ((fun x y => op (unop x ◃⁻¹ unop y)) y z) =
    (fun x y => op (unop x ◃⁻¹ unop y)) ((fun x y => op (unop x ◃⁻¹ unop y)) (op X✝) y)
      ((fun x y => op (unop x ◃⁻¹ unop y)) (op X✝) z)
[PROOFSTEP]
induction y using MulOpposite.rec'
[GOAL]
case h.h
R : Type u_1
inst✝ : Rack R
z : Rᵐᵒᵖ
X✝¹ X✝ : R
⊢ (fun x y => op (unop x ◃⁻¹ unop y)) (op X✝¹) ((fun x y => op (unop x ◃⁻¹ unop y)) (op X✝) z) =
    (fun x y => op (unop x ◃⁻¹ unop y)) ((fun x y => op (unop x ◃⁻¹ unop y)) (op X✝¹) (op X✝))
      ((fun x y => op (unop x ◃⁻¹ unop y)) (op X✝¹) z)
[PROOFSTEP]
induction z using MulOpposite.rec'
[GOAL]
case h.h.h
R : Type u_1
inst✝ : Rack R
X✝² X✝¹ X✝ : R
⊢ (fun x y => op (unop x ◃⁻¹ unop y)) (op X✝²) ((fun x y => op (unop x ◃⁻¹ unop y)) (op X✝¹) (op X✝)) =
    (fun x y => op (unop x ◃⁻¹ unop y)) ((fun x y => op (unop x ◃⁻¹ unop y)) (op X✝²) (op X✝¹))
      ((fun x y => op (unop x ◃⁻¹ unop y)) (op X✝²) (op X✝))
[PROOFSTEP]
simp only [op_inj, unop_op, op_unop]
[GOAL]
case h.h.h
R : Type u_1
inst✝ : Rack R
X✝² X✝¹ X✝ : R
⊢ X✝² ◃⁻¹ X✝¹ ◃⁻¹ X✝ = (X✝² ◃⁻¹ X✝¹) ◃⁻¹ X✝² ◃⁻¹ X✝
[PROOFSTEP]
rw [self_distrib_inv]
[GOAL]
R : Type u_1
inst✝ : Rack R
x y : R
⊢ (fun x y => op (unop x ◃ unop y)) (op x) (op x ◃ op y) = op y
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : Rack R
x y : R
⊢ op x ◃ (fun x y => op (unop x ◃ unop y)) (op x) (op y) = op y
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : Rack R
x y : R
⊢ (x ◃ x) ◃ y = x ◃ y
[PROOFSTEP]
rw [← right_inv x y, ← self_distrib]
[GOAL]
R : Type u_1
inst✝ : Rack R
x y : R
⊢ (x ◃⁻¹ x) ◃⁻¹ y = x ◃⁻¹ y
[PROOFSTEP]
have h := @self_act_act_eq _ _ (op x) (op y)
[GOAL]
R : Type u_1
inst✝ : Rack R
x y : R
h : (op x ◃ op x) ◃ op y = op x ◃ op y
⊢ (x ◃⁻¹ x) ◃⁻¹ y = x ◃⁻¹ y
[PROOFSTEP]
simpa using h
[GOAL]
R : Type u_1
inst✝ : Rack R
x y : R
⊢ (x ◃ x) ◃⁻¹ y = x ◃⁻¹ y
[PROOFSTEP]
rw [← left_cancel (x ◃ x)]
[GOAL]
R : Type u_1
inst✝ : Rack R
x y : R
⊢ (x ◃ x) ◃ (x ◃ x) ◃⁻¹ y = (x ◃ x) ◃ x ◃⁻¹ y
[PROOFSTEP]
rw [right_inv]
[GOAL]
R : Type u_1
inst✝ : Rack R
x y : R
⊢ y = (x ◃ x) ◃ x ◃⁻¹ y
[PROOFSTEP]
rw [self_act_act_eq]
[GOAL]
R : Type u_1
inst✝ : Rack R
x y : R
⊢ y = x ◃ x ◃⁻¹ y
[PROOFSTEP]
rw [right_inv]
[GOAL]
R : Type u_1
inst✝ : Rack R
x y : R
⊢ (x ◃⁻¹ x) ◃ y = x ◃ y
[PROOFSTEP]
have h := @self_act_invAct_eq _ _ (op x) (op y)
[GOAL]
R : Type u_1
inst✝ : Rack R
x y : R
h : (op x ◃ op x) ◃⁻¹ op y = op x ◃⁻¹ op y
⊢ (x ◃⁻¹ x) ◃ y = x ◃ y
[PROOFSTEP]
simpa using h
[GOAL]
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y ↔ x = y
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y → x = y
case mpr R : Type u_1 inst✝ : Rack R x y : R ⊢ x = y → x ◃ x = y ◃ y
[PROOFSTEP]
swap
[GOAL]
case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x = y → x ◃ x = y ◃ y
case mp R : Type u_1 inst✝ : Rack R x y : R ⊢ x ◃ x = y ◃ y → x = y
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
R : Type u_1
inst✝ : Rack R
x : R
⊢ x ◃ x = x ◃ x
case mp R : Type u_1 inst✝ : Rack R x y : R ⊢ x ◃ x = y ◃ y → x = y
[PROOFSTEP]
rfl
[GOAL]
case mp
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y → x = y
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ x = y
[PROOFSTEP]
trans (x ◃ x) ◃⁻¹ x ◃ x
[GOAL]
R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ x = (x ◃ x) ◃⁻¹ x ◃ x
R : Type u_1 inst✝ : Rack R x y : R h : x ◃ x = y ◃ y ⊢ (x ◃ x) ◃⁻¹ x ◃ x = y
[PROOFSTEP]
rw [← left_cancel (x ◃ x), right_inv, self_act_act_eq]
[GOAL]
R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ (x ◃ x) ◃⁻¹ x ◃ x = y
[PROOFSTEP]
rw [h, ← left_cancel (y ◃ y), right_inv, self_act_act_eq]
[GOAL]
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃⁻¹ x = y ◃⁻¹ y ↔ x = y
[PROOFSTEP]
have h := @self_act_eq_iff_eq _ _ (op x) (op y)
[GOAL]
R : Type u_1
inst✝ : Rack R
x y : R
h : op x ◃ op x = op y ◃ op y ↔ op x = op y
⊢ x ◃⁻¹ x = y ◃⁻¹ y ↔ x = y
[PROOFSTEP]
simpa using h
[GOAL]
R✝ : Type u_1
inst✝¹ : Rack R✝
R : Type u_2
inst✝ : Rack R
x : R
⊢ (fun x => x ◃⁻¹ x) ((fun x => x ◃ x) x) = x
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u_1
inst✝¹ : Rack R✝
R : Type u_2
inst✝ : Rack R
x : R
⊢ (fun x => x ◃ x) ((fun x => x ◃⁻¹ x) x) = x
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u_1
inst✝¹ : Rack R✝
R : Type u_2
inst✝ : Rack R
h : IsInvolutory R
x y : R
⊢ x ◃⁻¹ y = x ◃ y
[PROOFSTEP]
rw [← left_cancel x, right_inv, h x]
[GOAL]
R✝ : Type u_1
inst✝¹ : Rack R✝
R : Type u_2
inst✝ : Rack R
x y z : R
⊢ x ◃ y ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
[PROOFSTEP]
rw [self_distrib]
[GOAL]
R✝ : Type u_1
inst✝¹ : Rack R✝
R : Type u_2
inst✝ : Rack R
x y z : R
⊢ (x ◃ y) ◃ x ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
[PROOFSTEP]
rw [left_cancel]
[GOAL]
S₁ : Type u_1
S₂ : Type u_2
S₃ : Type u_3
inst✝³ : Shelf S₁
inst✝² : Shelf S₂
inst✝¹ : Shelf S₃
S : Type u_4
inst✝ : Shelf S
⊢ ∀ {x y : S}, (fun x => x) (x ◃ y) = (fun x => x) x ◃ (fun x => x) y
[PROOFSTEP]
simp
[GOAL]
S₁ : Type u_1
S₂ : Type u_2
S₃ : Type u_3
inst✝² : Shelf S₁
inst✝¹ : Shelf S₂
inst✝ : Shelf S₃
g : S₂ →◃ S₃
f : S₁ →◃ S₂
⊢ ∀ {x y : S₁}, (g.toFun ∘ f.toFun) (x ◃ y) = (g.toFun ∘ f.toFun) x ◃ (g.toFun ∘ f.toFun) y
[PROOFSTEP]
simp
[GOAL]
Q : Type u_1
inst✝ : Quandle Q
x : Q
⊢ x ◃⁻¹ x = x
[PROOFSTEP]
rw [← left_cancel x]
[GOAL]
Q : Type u_1
inst✝ : Quandle Q
x : Q
⊢ x ◃ x ◃⁻¹ x = x ◃ x
[PROOFSTEP]
simp
[GOAL]
Q : Type u_1
inst✝ : Quandle Q
⊢ ∀ {x : Qᵐᵒᵖ}, x ◃ x = x
[PROOFSTEP]
intro x
[GOAL]
Q : Type u_1
inst✝ : Quandle Q
x : Qᵐᵒᵖ
⊢ x ◃ x = x
[PROOFSTEP]
induction' x using MulOpposite.rec'
[GOAL]
case h
Q : Type u_1
inst✝ : Quandle Q
X✝ : Q
⊢ op X✝ ◃ op X✝ = op X✝
[PROOFSTEP]
simp
[GOAL]
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
⊢ ∀ {x y z : Conj G},
    (fun x => ↑(↑MulAut.conj x)) x ((fun x => ↑(↑MulAut.conj x)) y z) =
      (fun x => ↑(↑MulAut.conj x)) ((fun x => ↑(↑MulAut.conj x)) x y) ((fun x => ↑(↑MulAut.conj x)) x z)
[PROOFSTEP]
intro x y z
[GOAL]
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y z : Conj G
⊢ (fun x => ↑(↑MulAut.conj x)) x ((fun x => ↑(↑MulAut.conj x)) y z) =
    (fun x => ↑(↑MulAut.conj x)) ((fun x => ↑(↑MulAut.conj x)) x y) ((fun x => ↑(↑MulAut.conj x)) x z)
[PROOFSTEP]
dsimp only [MulAut.conj_apply]
[GOAL]
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y z : Conj G
⊢ x * (y * z * y⁻¹) * x⁻¹ = x * y * x⁻¹ * (x * z * x⁻¹) * (x * y * x⁻¹)⁻¹
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ (fun x => ↑(MulEquiv.symm (↑MulAut.conj x))) x (x ◃ y) = y
[PROOFSTEP]
simp [act', mul_assoc]
[GOAL]
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ x ◃ (fun x => ↑(MulEquiv.symm (↑MulAut.conj x))) x y = y
[PROOFSTEP]
simp [act', mul_assoc]
[GOAL]
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
⊢ ∀ {x : Conj G}, x ◃ x = x
[PROOFSTEP]
simp
[GOAL]
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ x ◃ y = y ↔ y ◃ x = x
[PROOFSTEP]
dsimp [Conj] at *
[GOAL]
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ x * y * x⁻¹ = y ↔ y * x * y⁻¹ = x
[PROOFSTEP]
constructor
[GOAL]
case mp
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ x * y * x⁻¹ = y → y * x * y⁻¹ = x
case mpr Q : Type u_1 inst✝¹ : Quandle Q G : Type u_2 inst✝ : Group G x y : Conj G ⊢ y * x * y⁻¹ = x → x * y * x⁻¹ = y
[PROOFSTEP]
repeat' intro h; conv_rhs => rw [eq_mul_inv_of_mul_eq (eq_mul_inv_of_mul_eq h)]; simp
[GOAL]
case mp
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ x * y * x⁻¹ = y → y * x * y⁻¹ = x
[PROOFSTEP]
intro h
[GOAL]
case mp
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
h : x * y * x⁻¹ = y
⊢ y * x * y⁻¹ = x
[PROOFSTEP]
conv_rhs => rw [eq_mul_inv_of_mul_eq (eq_mul_inv_of_mul_eq h)]; simp
[GOAL]
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
h : x * y * x⁻¹ = y
| x
[PROOFSTEP]
rw [eq_mul_inv_of_mul_eq (eq_mul_inv_of_mul_eq h)]; simp
[GOAL]
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
h : x * y * x⁻¹ = y
| x
[PROOFSTEP]
rw [eq_mul_inv_of_mul_eq (eq_mul_inv_of_mul_eq h)]; simp
[GOAL]
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
h : x * y * x⁻¹ = y
| x
[PROOFSTEP]
rw [eq_mul_inv_of_mul_eq (eq_mul_inv_of_mul_eq h)]
[GOAL]
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
h : x * y * x⁻¹ = y
| y * x⁻¹⁻¹ * y⁻¹
[PROOFSTEP]
simp
[GOAL]
case mpr
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ y * x * y⁻¹ = x → x * y * x⁻¹ = y
[PROOFSTEP]
intro h
[GOAL]
case mpr
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
h : y * x * y⁻¹ = x
⊢ x * y * x⁻¹ = y
[PROOFSTEP]
conv_rhs => rw [eq_mul_inv_of_mul_eq (eq_mul_inv_of_mul_eq h)]; simp
[GOAL]
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
h : y * x * y⁻¹ = x
| y
[PROOFSTEP]
rw [eq_mul_inv_of_mul_eq (eq_mul_inv_of_mul_eq h)]; simp
[GOAL]
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
h : y * x * y⁻¹ = x
| y
[PROOFSTEP]
rw [eq_mul_inv_of_mul_eq (eq_mul_inv_of_mul_eq h)]; simp
[GOAL]
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
h : y * x * y⁻¹ = x
| y
[PROOFSTEP]
rw [eq_mul_inv_of_mul_eq (eq_mul_inv_of_mul_eq h)]
[GOAL]
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
h : y * x * y⁻¹ = x
| x * y⁻¹⁻¹ * x⁻¹
[PROOFSTEP]
simp
[GOAL]
Q : Type u_1
inst✝² : Quandle Q
G : Type u_2
H : Type u_3
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
⊢ ∀ {x y : Conj G}, ↑f (x ◃ y) = ↑f x ◃ ↑f y
[PROOFSTEP]
simp
[GOAL]
Q : Type u_1
inst✝ : Quandle Q
n : ℕ
a : ZMod n
⊢ Function.Involutive (dihedralAct n a)
[PROOFSTEP]
intro b
[GOAL]
Q : Type u_1
inst✝ : Quandle Q
n : ℕ
a b : ZMod n
⊢ dihedralAct n a (dihedralAct n a b) = b
[PROOFSTEP]
dsimp only [dihedralAct]
[GOAL]
Q : Type u_1
inst✝ : Quandle Q
n : ℕ
a b : ZMod n
⊢ 2 * a - (2 * a - b) = b
[PROOFSTEP]
simp
[GOAL]
Q : Type u_1
inst✝ : Quandle Q
n : ℕ
⊢ ∀ {x y z : Dihedral n}, dihedralAct n x (dihedralAct n y z) = dihedralAct n (dihedralAct n x y) (dihedralAct n x z)
[PROOFSTEP]
intro x y z
[GOAL]
Q : Type u_1
inst✝ : Quandle Q
n : ℕ
x y z : Dihedral n
⊢ dihedralAct n x (dihedralAct n y z) = dihedralAct n (dihedralAct n x y) (dihedralAct n x z)
[PROOFSTEP]
simp only [dihedralAct]
[GOAL]
Q : Type u_1
inst✝ : Quandle Q
n : ℕ
x y z : Dihedral n
⊢ 2 * x - (2 * y - z) = 2 * (2 * x - y) - (2 * x - z)
[PROOFSTEP]
ring_nf
[GOAL]
Q : Type u_1
inst✝ : Quandle Q
n : ℕ
⊢ ∀ {x : Dihedral n}, x ◃ x = x
[PROOFSTEP]
intro x
[GOAL]
Q : Type u_1
inst✝ : Quandle Q
n : ℕ
x : Dihedral n
⊢ x ◃ x = x
[PROOFSTEP]
simp only [dihedralAct]
[GOAL]
Q : Type u_1
inst✝ : Quandle Q
n : ℕ
x : Dihedral n
⊢ 2 * x - x = x
[PROOFSTEP]
ring_nf
[GOAL]
R : Type u_1
inst✝ : Rack R
⊢ ∀ {x y : R}, act' (x ◃ y) = act' x ◃ act' y
[PROOFSTEP]
intro x y
[GOAL]
R : Type u_1
inst✝ : Rack R
x y : R
⊢ act' (x ◃ y) = act' x ◃ act' y
[PROOFSTEP]
exact ad_conj x y
[GOAL]
R : Type u_1
inst✝ : Rack R
⊢ Equivalence (PreEnvelGroupRel R)
[PROOFSTEP]
constructor
[GOAL]
case refl
R : Type u_1
inst✝ : Rack R
⊢ ∀ (x : PreEnvelGroup R), PreEnvelGroupRel R x x
[PROOFSTEP]
apply PreEnvelGroupRel.refl
[GOAL]
case symm
R : Type u_1
inst✝ : Rack R
⊢ ∀ {x y : PreEnvelGroup R}, PreEnvelGroupRel R x y → PreEnvelGroupRel R y x
[PROOFSTEP]
apply PreEnvelGroupRel.symm
[GOAL]
case trans
R : Type u_1
inst✝ : Rack R
⊢ ∀ {x y z : PreEnvelGroup R}, PreEnvelGroupRel R x y → PreEnvelGroupRel R y z → PreEnvelGroupRel R x z
[PROOFSTEP]
apply PreEnvelGroupRel.trans
[GOAL]
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a✝ b✝ a'✝ b'✝ : PreEnvelGroup R
ha : PreEnvelGroupRel' R a✝ a'✝
hb : PreEnvelGroupRel' R b✝ b'✝
⊢ mapAux f (PreEnvelGroup.mul a✝ b✝) = mapAux f (PreEnvelGroup.mul a'✝ b'✝)
[PROOFSTEP]
simp [toEnvelGroup.mapAux, well_def f ha, well_def f hb]
[GOAL]
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a✝ a'✝ : PreEnvelGroup R
ha : PreEnvelGroupRel' R a✝ a'✝
⊢ mapAux f (PreEnvelGroup.inv a✝) = mapAux f (PreEnvelGroup.inv a'✝)
[PROOFSTEP]
simp [toEnvelGroup.mapAux, well_def f ha]
[GOAL]
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a b c : PreEnvelGroup R
⊢ mapAux f (PreEnvelGroup.mul (PreEnvelGroup.mul a b) c) = mapAux f (PreEnvelGroup.mul a (PreEnvelGroup.mul b c))
[PROOFSTEP]
apply mul_assoc
[GOAL]
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a : PreEnvelGroup R
⊢ mapAux f (PreEnvelGroup.mul unit a) = mapAux f a
[PROOFSTEP]
simp [toEnvelGroup.mapAux]
[GOAL]
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a : PreEnvelGroup R
⊢ mapAux f (PreEnvelGroup.mul a unit) = mapAux f a
[PROOFSTEP]
simp [toEnvelGroup.mapAux]
[GOAL]
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a : PreEnvelGroup R
⊢ mapAux f (PreEnvelGroup.mul (PreEnvelGroup.inv a) a) = mapAux f unit
[PROOFSTEP]
simp [toEnvelGroup.mapAux]
[GOAL]
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
x y : R
⊢ mapAux f (PreEnvelGroup.mul (PreEnvelGroup.mul (incl x) (incl y)) (PreEnvelGroup.inv (incl x))) =
    mapAux f (incl (x ◃ y))
[PROOFSTEP]
simp [toEnvelGroup.mapAux]
[GOAL]
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
⊢ (fun x => Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b)) 1 = 1
[PROOFSTEP]
change Quotient.liftOn ⟦Rack.PreEnvelGroup.unit⟧ (toEnvelGroup.mapAux f) _ = 1
[GOAL]
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
⊢ Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
      (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
    1
[PROOFSTEP]
simp only [Quotient.lift_mk, mapAux]
[GOAL]
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
x✝ y✝ : EnvelGroup R
x y : PreEnvelGroup R
⊢ OneHom.toFun
      { toFun := fun x => Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
        map_one' :=
          (_ :
            Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
              1) }
      (Quotient.mk (setoid R) x * Quotient.mk (setoid R) y) =
    OneHom.toFun
        {
          toFun := fun x =>
            Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
          map_one' :=
            (_ :
              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                1) }
        (Quotient.mk (setoid R) x) *
      OneHom.toFun
        {
          toFun := fun x =>
            Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
          map_one' :=
            (_ :
              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                1) }
        (Quotient.mk (setoid R) y)
[PROOFSTEP]
simp only [toEnvelGroup.mapAux]
[GOAL]
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
x✝ y✝ : EnvelGroup R
x y : PreEnvelGroup R
⊢ Quotient.liftOn (Quotient.mk (setoid R) x * Quotient.mk (setoid R) y) (mapAux f)
      (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
    Quotient.liftOn (Quotient.mk (setoid R) x) (mapAux f)
        (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) *
      Quotient.liftOn (Quotient.mk (setoid R) y) (mapAux f)
        (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b)
[PROOFSTEP]
change Quotient.liftOn ⟦mul x y⟧ (toEnvelGroup.mapAux f) _ = _
[GOAL]
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
x✝ y✝ : EnvelGroup R
x y : PreEnvelGroup R
⊢ Quotient.liftOn (Quotient.mk (setoid R) (PreEnvelGroup.mul x y)) (mapAux f)
      (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
    Quotient.liftOn (Quotient.mk (setoid R) x) (mapAux f)
        (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) *
      Quotient.liftOn (Quotient.mk (setoid R) y) (mapAux f)
        (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b)
[PROOFSTEP]
simp [toEnvelGroup.mapAux]
[GOAL]
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
⊢ (fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R))
      ((fun f =>
          {
            toOneHom :=
              {
                toFun := fun x =>
                  Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                map_one' :=
                  (_ :
                    Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                        (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                      1) },
            map_mul' :=
              (_ :
                ∀ (x y : EnvelGroup R),
                  OneHom.toFun
                      {
                        toFun := fun x =>
                          Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                        map_one' :=
                          (_ :
                            Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                              1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        y) })
        f) =
    f
[PROOFSTEP]
ext
[GOAL]
case toFun.h
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
x✝ : R
⊢ ShelfHom.toFun
      ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R))
        ((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          f))
      x✝ =
    ShelfHom.toFun f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x : PreEnvelGroup R
⊢ ↑((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) F))
      (Quotient.mk (setoid R) x) =
    ↑F (Quotient.mk (setoid R) x)
[PROOFSTEP]
induction' x with _ x y ih_x ih_y x ih_x
[GOAL]
case unit
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x : EnvelGroup R
⊢ ↑((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) F))
      (Quotient.mk (setoid R) unit) =
    ↑F (Quotient.mk (setoid R) unit)
[PROOFSTEP]
exact F.map_one.symm
[GOAL]
case incl
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x : EnvelGroup R
x✝ : R
⊢ ↑((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) F))
      (Quotient.mk (setoid R) (incl x✝)) =
    ↑F (Quotient.mk (setoid R) (incl x✝))
[PROOFSTEP]
rfl
[GOAL]
case mul
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x y : PreEnvelGroup R
ih_x :
  ↑((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) F))
      (Quotient.mk (setoid R) x) =
    ↑F (Quotient.mk (setoid R) x)
ih_y :
  ↑((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) F))
      (Quotient.mk (setoid R) y) =
    ↑F (Quotient.mk (setoid R) y)
⊢ ↑((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) F))
      (Quotient.mk (setoid R) (PreEnvelGroup.mul x y)) =
    ↑F (Quotient.mk (setoid R) (PreEnvelGroup.mul x y))
[PROOFSTEP]
have hm : ⟦x.mul y⟧ = @Mul.mul (EnvelGroup R) _ ⟦x⟧ ⟦y⟧ := rfl
[GOAL]
case mul
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x y : PreEnvelGroup R
ih_x :
  ↑((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) F))
      (Quotient.mk (setoid R) x) =
    ↑F (Quotient.mk (setoid R) x)
ih_y :
  ↑((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) F))
      (Quotient.mk (setoid R) y) =
    ↑F (Quotient.mk (setoid R) y)
hm : Quotient.mk (setoid R) (PreEnvelGroup.mul x y) = Mul.mul (Quotient.mk (setoid R) x) (Quotient.mk (setoid R) y)
⊢ ↑((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) F))
      (Quotient.mk (setoid R) (PreEnvelGroup.mul x y)) =
    ↑F (Quotient.mk (setoid R) (PreEnvelGroup.mul x y))
[PROOFSTEP]
simp only [MonoidHom.coe_mk, OneHom.coe_mk, Quotient.lift_mk]
[GOAL]
case mul
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x y : PreEnvelGroup R
ih_x :
  ↑((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) F))
      (Quotient.mk (setoid R) x) =
    ↑F (Quotient.mk (setoid R) x)
ih_y :
  ↑((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) F))
      (Quotient.mk (setoid R) y) =
    ↑F (Quotient.mk (setoid R) y)
hm : Quotient.mk (setoid R) (PreEnvelGroup.mul x y) = Mul.mul (Quotient.mk (setoid R) x) (Quotient.mk (setoid R) y)
⊢ mapAux (ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) (PreEnvelGroup.mul x y) =
    ↑F (Quotient.mk (setoid R) (PreEnvelGroup.mul x y))
[PROOFSTEP]
suffices ∀ x y, F (Mul.mul x y) = F (x) * F (y)
  by
  simp_all only [MonoidHom.coe_mk, OneHom.coe_mk, Quotient.lift_mk, hm]
  rw [← ih_x, ← ih_y, mapAux]
[GOAL]
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x y : PreEnvelGroup R
ih_x :
  ↑((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) F))
      (Quotient.mk (setoid R) x) =
    ↑F (Quotient.mk (setoid R) x)
ih_y :
  ↑((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) F))
      (Quotient.mk (setoid R) y) =
    ↑F (Quotient.mk (setoid R) y)
hm : Quotient.mk (setoid R) (PreEnvelGroup.mul x y) = Mul.mul (Quotient.mk (setoid R) x) (Quotient.mk (setoid R) y)
this : ∀ (x y : EnvelGroup R), ↑F (Mul.mul x y) = ↑F x * ↑F y
⊢ mapAux (ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) (PreEnvelGroup.mul x y) =
    ↑F (Quotient.mk (setoid R) (PreEnvelGroup.mul x y))
[PROOFSTEP]
simp_all only [MonoidHom.coe_mk, OneHom.coe_mk, Quotient.lift_mk, hm]
[GOAL]
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x y : PreEnvelGroup R
ih_x : mapAux (ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) x = ↑F (Quotient.mk (setoid R) x)
ih_y : mapAux (ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) y = ↑F (Quotient.mk (setoid R) y)
hm : Quotient.mk (setoid R) (PreEnvelGroup.mul x y) = Mul.mul (Quotient.mk (setoid R) x) (Quotient.mk (setoid R) y)
this : ∀ (x y : EnvelGroup R), ↑F (Mul.mul x y) = ↑F x * ↑F y
⊢ mapAux (ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) (PreEnvelGroup.mul x y) =
    ↑F (Quotient.mk (setoid R) x) * ↑F (Quotient.mk (setoid R) y)
[PROOFSTEP]
rw [← ih_x, ← ih_y, mapAux]
[GOAL]
case mul
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x y : PreEnvelGroup R
ih_x :
  ↑((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) F))
      (Quotient.mk (setoid R) x) =
    ↑F (Quotient.mk (setoid R) x)
ih_y :
  ↑((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) F))
      (Quotient.mk (setoid R) y) =
    ↑F (Quotient.mk (setoid R) y)
hm : Quotient.mk (setoid R) (PreEnvelGroup.mul x y) = Mul.mul (Quotient.mk (setoid R) x) (Quotient.mk (setoid R) y)
⊢ ∀ (x y : EnvelGroup R), ↑F (Mul.mul x y) = ↑F x * ↑F y
[PROOFSTEP]
exact F.map_mul
[GOAL]
case inv
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x : PreEnvelGroup R
ih_x :
  ↑((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) F))
      (Quotient.mk (setoid R) x) =
    ↑F (Quotient.mk (setoid R) x)
⊢ ↑((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) F))
      (Quotient.mk (setoid R) (PreEnvelGroup.inv x)) =
    ↑F (Quotient.mk (setoid R) (PreEnvelGroup.inv x))
[PROOFSTEP]
have hm : ⟦x.inv⟧ = @Inv.inv (EnvelGroup R) _ ⟦x⟧ := rfl
[GOAL]
case inv
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x : PreEnvelGroup R
ih_x :
  ↑((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) F))
      (Quotient.mk (setoid R) x) =
    ↑F (Quotient.mk (setoid R) x)
hm : Quotient.mk (setoid R) (PreEnvelGroup.inv x) = (Quotient.mk (setoid R) x)⁻¹
⊢ ↑((fun f =>
            {
              toOneHom :=
                {
                  toFun := fun x =>
                    Quotient.liftOn x (mapAux f) (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                  map_one' :=
                    (_ :
                      Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                          (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : EnvelGroup R),
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn x (mapAux f)
                              (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                          map_one' :=
                            (_ :
                              Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                  (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun x =>
                              Quotient.liftOn x (mapAux f)
                                (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b),
                            map_one' :=
                              (_ :
                                Quotient.liftOn (Quotient.mk (setoid R) unit) (mapAux f)
                                    (_ : ∀ (a b : PreEnvelGroup R), a ≈ b → mapAux f a = mapAux f b) =
                                  1) }
                          y) })
          ((fun F => ShelfHom.comp (Quandle.Conj.map F) (toEnvelGroup R)) F))
      (Quotient.mk (setoid R) (PreEnvelGroup.inv x)) =
    ↑F (Quotient.mk (setoid R) (PreEnvelGroup.inv x))
[PROOFSTEP]
rw [hm, F.map_inv, MonoidHom.map_inv, ih_x]


[GOAL]
ι : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : ConditionallyCompleteLattice G
inst✝¹ : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : Nonempty ι
f : ι → G
hf : BddAbove (range f)
a : G
⊢ (⨆ (i : ι), f i) / a = ⨆ (i : ι), f i / a
[PROOFSTEP]
simp only [div_eq_mul_inv, ciSup_mul hf]


[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
terminated_at_n : TerminatedAt g n
⊢ continuantsAux g (n + 2) = continuantsAux g (n + 1)
[PROOFSTEP]
rw [terminatedAt_iff_s_none] at terminated_at_n
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
terminated_at_n : Stream'.Seq.get? g.s n = none
⊢ continuantsAux g (n + 2) = continuantsAux g (n + 1)
[PROOFSTEP]
simp only [continuantsAux, Nat.add_eq, add_zero, terminated_at_n]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminated_at_n : TerminatedAt g n
⊢ continuantsAux g m = continuantsAux g (n + 1)
[PROOFSTEP]
refine' Nat.le_induction rfl (fun k hnk hk => _) _ n_lt_m
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminated_at_n : TerminatedAt g n
k : ℕ
hnk : Nat.succ n ≤ k
hk : continuantsAux g k = continuantsAux g (n + 1)
⊢ continuantsAux g (k + 1) = continuantsAux g (n + 1)
[PROOFSTEP]
rcases Nat.exists_eq_add_of_lt hnk with ⟨k, rfl⟩
[GOAL]
case intro
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminated_at_n : TerminatedAt g n
k : ℕ
hnk : Nat.succ n ≤ n + k + 1
hk : continuantsAux g (n + k + 1) = continuantsAux g (n + 1)
⊢ continuantsAux g (n + k + 1 + 1) = continuantsAux g (n + 1)
[PROOFSTEP]
refine' (continuantsAux_stable_step_of_terminated _).trans hk
[GOAL]
case intro
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminated_at_n : TerminatedAt g n
k : ℕ
hnk : Nat.succ n ≤ n + k + 1
hk : continuantsAux g (n + k + 1) = continuantsAux g (n + 1)
⊢ TerminatedAt g (n + k)
[PROOFSTEP]
exact terminated_stable (Nat.le_add_right _ _) terminated_at_n
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.TerminatedAt s n
⊢ convergents'Aux s (n + 1) = convergents'Aux s n
[PROOFSTEP]
change s.get? n = none at terminated_at_n
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s n = none
⊢ convergents'Aux s (n + 1) = convergents'Aux s n
[PROOFSTEP]
induction' n with n IH generalizing s
[GOAL]
case zero
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n = none
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s Nat.zero = none
⊢ convergents'Aux s (Nat.zero + 1) = convergents'Aux s Nat.zero
case succ
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
[PROOFSTEP]
case zero => simp only [convergents'Aux, terminated_at_n, Stream'.Seq.head]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n = none
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s Nat.zero = none
⊢ convergents'Aux s (Nat.zero + 1) = convergents'Aux s Nat.zero
[PROOFSTEP]
case zero => simp only [convergents'Aux, terminated_at_n, Stream'.Seq.head]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n = none
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s Nat.zero = none
⊢ convergents'Aux s (Nat.zero + 1) = convergents'Aux s Nat.zero
[PROOFSTEP]
simp only [convergents'Aux, terminated_at_n, Stream'.Seq.head]
[GOAL]
case succ
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
[PROOFSTEP]
case succ =>
  cases' s_head_eq : s.head with gp_head
  case none => simp only [convergents'Aux, s_head_eq]
  case
    some =>
    have : s.tail.TerminatedAt n := by simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminated_at_n]
    have := IH this
    rw [convergents'Aux] at this
    simp [this, Nat.add_eq, add_zero, convergents'Aux, s_head_eq]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
[PROOFSTEP]
case succ =>
  cases' s_head_eq : s.head with gp_head
  case none => simp only [convergents'Aux, s_head_eq]
  case
    some =>
    have : s.tail.TerminatedAt n := by simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminated_at_n]
    have := IH this
    rw [convergents'Aux] at this
    simp [this, Nat.add_eq, add_zero, convergents'Aux, s_head_eq]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
[PROOFSTEP]
cases' s_head_eq : s.head with gp_head
[GOAL]
case none
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
s_head_eq : Stream'.Seq.head s = none
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
case some
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
[PROOFSTEP]
case none => simp only [convergents'Aux, s_head_eq]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
s_head_eq : Stream'.Seq.head s = none
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
[PROOFSTEP]
case none => simp only [convergents'Aux, s_head_eq]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
s_head_eq : Stream'.Seq.head s = none
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
[PROOFSTEP]
simp only [convergents'Aux, s_head_eq]
[GOAL]
case some
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
[PROOFSTEP]
case
  some =>
  have : s.tail.TerminatedAt n := by simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminated_at_n]
  have := IH this
  rw [convergents'Aux] at this
  simp [this, Nat.add_eq, add_zero, convergents'Aux, s_head_eq]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
[PROOFSTEP]
case
  some =>
  have : s.tail.TerminatedAt n := by simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminated_at_n]
  have := IH this
  rw [convergents'Aux] at this
  simp [this, Nat.add_eq, add_zero, convergents'Aux, s_head_eq]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
[PROOFSTEP]
have : s.tail.TerminatedAt n := by simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminated_at_n]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
⊢ Stream'.Seq.TerminatedAt (Stream'.Seq.tail s) n
[PROOFSTEP]
simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminated_at_n]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
this : Stream'.Seq.TerminatedAt (Stream'.Seq.tail s) n
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
[PROOFSTEP]
have := IH this
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
this✝ : Stream'.Seq.TerminatedAt (Stream'.Seq.tail s) n
this : convergents'Aux (Stream'.Seq.tail s) (n + 1) = convergents'Aux (Stream'.Seq.tail s) n
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
[PROOFSTEP]
rw [convergents'Aux] at this
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ m : ℕ
inst✝ : DivisionRing K
s✝ : Stream'.Seq (Pair K)
terminated_at_n✝ : Stream'.Seq.get? s✝ n✝ = none
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, Stream'.Seq.get? s n = none → convergents'Aux s (n + 1) = convergents'Aux s n
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.get? s (Nat.succ n) = none
gp_head : Pair K
s_head_eq : Stream'.Seq.head s = some gp_head
this✝ : Stream'.Seq.TerminatedAt (Stream'.Seq.tail s) n
this :
  (match Stream'.Seq.head (Stream'.Seq.tail s) with
    | none => 0
    | some gp => gp.a / (gp.b + convergents'Aux (Stream'.Seq.tail (Stream'.Seq.tail s)) n)) =
    convergents'Aux (Stream'.Seq.tail s) n
⊢ convergents'Aux s (Nat.succ n + 1) = convergents'Aux s (Nat.succ n)
[PROOFSTEP]
simp [this, Nat.add_eq, add_zero, convergents'Aux, s_head_eq]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
n_le_m : n ≤ m
terminated_at_n : Stream'.Seq.TerminatedAt s n
⊢ convergents'Aux s m = convergents'Aux s n
[PROOFSTEP]
induction' n_le_m with m n_le_m IH
[GOAL]
case refl
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.TerminatedAt s n
⊢ convergents'Aux s n = convergents'Aux s n
[PROOFSTEP]
rfl
[GOAL]
case step
K : Type u_1
g : GeneralizedContinuedFraction K
n m✝ : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.TerminatedAt s n
m : ℕ
n_le_m : Nat.le n m
IH : convergents'Aux s m = convergents'Aux s n
⊢ convergents'Aux s (Nat.succ m) = convergents'Aux s n
[PROOFSTEP]
refine' (convergents'Aux_stable_step_of_terminated _).trans IH
[GOAL]
case step
K : Type u_1
g : GeneralizedContinuedFraction K
n m✝ : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminated_at_n : Stream'.Seq.TerminatedAt s n
m : ℕ
n_le_m : Nat.le n m
IH : convergents'Aux s m = convergents'Aux s n
⊢ Stream'.Seq.TerminatedAt s m
[PROOFSTEP]
exact s.terminated_stable n_le_m terminated_at_n
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_le_m : n ≤ m
terminated_at_n : TerminatedAt g n
⊢ continuants g m = continuants g n
[PROOFSTEP]
simp only [nth_cont_eq_succ_nth_cont_aux,
  continuantsAux_stable_of_terminated (Nat.pred_le_iff.mp n_le_m) terminated_at_n]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_le_m : n ≤ m
terminated_at_n : TerminatedAt g n
⊢ numerators g m = numerators g n
[PROOFSTEP]
simp only [num_eq_conts_a, continuants_stable_of_terminated n_le_m terminated_at_n]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_le_m : n ≤ m
terminated_at_n : TerminatedAt g n
⊢ denominators g m = denominators g n
[PROOFSTEP]
simp only [denom_eq_conts_b, continuants_stable_of_terminated n_le_m terminated_at_n]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_le_m : n ≤ m
terminated_at_n : TerminatedAt g n
⊢ convergents g m = convergents g n
[PROOFSTEP]
simp only [convergents, denominators_stable_of_terminated n_le_m terminated_at_n,
  numerators_stable_of_terminated n_le_m terminated_at_n]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n m : ℕ
inst✝ : DivisionRing K
n_le_m : n ≤ m
terminated_at_n : TerminatedAt g n
⊢ convergents' g m = convergents' g n
[PROOFSTEP]
simp only [convergents', convergents'Aux_stable_of_terminated n_le_m terminated_at_n]