case of
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ (x y : M), r x y → Setoid.r x y

case refl
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ (x : M), Setoid.r x x

case symm
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {x y : M}, ConGen.Rel r x y → Setoid.r x y → Setoid.r y x

case trans
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {x y z : M}, ConGen.Rel r x y → ConGen.Rel r y z → Setoid.r x y → Setoid.r y z → Setoid.r x z

case mul
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → Setoid.r w x → Setoid.r y z → Setoid.r (w * y) (x * z)
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ Setoid.r x y
apply ConGen.Rel.recOn (motive := fun x y _ => s.r x y) hxy
case refl
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ (x : M), Setoid.r x x

case symm
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {x y : M}, ConGen.Rel r x y → Setoid.r x y → Setoid.r y x

case trans
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {x y z : M}, ConGen.Rel r x y → ConGen.Rel r y z → Setoid.r x y → Setoid.r y z → Setoid.r x z

case mul
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → Setoid.r w x → Setoid.r y z → Setoid.r (w * y) (x * z)
case of
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ (x y : M), r x y → Setoid.r x y

case refl
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ (x : M), Setoid.r x x

case symm
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {x y : M}, ConGen.Rel r x y → Setoid.r x y → Setoid.r y x

case trans
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {x y z : M}, ConGen.Rel r x y → ConGen.Rel r y z → Setoid.r x y → Setoid.r y z → Setoid.r x z

case mul
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → Setoid.r w x → Setoid.r y z → Setoid.r (w * y) (x * z)
. exact fun x y h => hs x y h
case symm
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {x y : M}, ConGen.Rel r x y → Setoid.r x y → Setoid.r y x

case trans
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {x y z : M}, ConGen.Rel r x y → ConGen.Rel r y z → Setoid.r x y → Setoid.r y z → Setoid.r x z

case mul
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → Setoid.r w x → Setoid.r y z → Setoid.r (w * y) (x * z)
case refl
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ (x : M), Setoid.r x x

case symm
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {x y : M}, ConGen.Rel r x y → Setoid.r x y → Setoid.r y x

case trans
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {x y z : M}, ConGen.Rel r x y → ConGen.Rel r y z → Setoid.r x y → Setoid.r y z → Setoid.r x z

case mul
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → Setoid.r w x → Setoid.r y z → Setoid.r (w * y) (x * z)
. exact s.refl'
case trans
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {x y z : M}, ConGen.Rel r x y → ConGen.Rel r y z → Setoid.r x y → Setoid.r y z → Setoid.r x z

case mul
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → Setoid.r w x → Setoid.r y z → Setoid.r (w * y) (x * z)
case symm
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {x y : M}, ConGen.Rel r x y → Setoid.r x y → Setoid.r y x

case trans
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {x y z : M}, ConGen.Rel r x y → ConGen.Rel r y z → Setoid.r x y → Setoid.r y z → Setoid.r x z

case mul
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → Setoid.r w x → Setoid.r y z → Setoid.r (w * y) (x * z)
. exact fun _ => s.symm'
case mul
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → Setoid.r w x → Setoid.r y z → Setoid.r (w * y) (x * z)
case trans
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {x y z : M}, ConGen.Rel r x y → ConGen.Rel r y z → Setoid.r x y → Setoid.r y z → Setoid.r x z

case mul
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → Setoid.r w x → Setoid.r y z → Setoid.r (w * y) (x * z)
. exact fun _ _ => s.trans'
no goals
case mul
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → Setoid.r w x → Setoid.r y z → Setoid.r (w * y) (x * z)
. exact fun _ _ => s.mul
no goals
case of
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ (x y : M), r x y → Setoid.r x y
exact fun x y h => hs x y h
no goals
case refl
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ (x : M), Setoid.r x x
exact s.refl'
no goals
case symm
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {x y : M}, ConGen.Rel r x y → Setoid.r x y → Setoid.r y x
exact fun _ => s.symm'
no goals
case trans
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {x y z : M}, ConGen.Rel r x y → ConGen.Rel r y z → Setoid.r x y → Setoid.r y z → Setoid.r x z
exact fun _ _ => s.trans'
no goals
case mul
M : Type u_1
N : Type ?u.26074
P : Type ?u.26077
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → ↑s x y}
x y : M
hxy : Setoid.r x y
⊢ ∀ {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → Setoid.r w x → Setoid.r y z → Setoid.r (w * y) (x * z)
exact fun _ _ => s.mul