no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.37854
inst✝¹ : CommMonoid N
P : Type ?u.37860
inst✝ : CommMonoid P
x✝ : { x // x ∈ S }
⊢ ↑1 * (↑(↑x✝, x✝).snd * 1.fst) = ↑1 * (↑1.snd * (↑x✝, x✝).fst)
simp
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.37854
inst✝¹ : CommMonoid N
P : Type ?u.37860
inst✝ : CommMonoid P
b : Con (M × { x // x ∈ S })
H : b ∈ {c | ∀ (y : { x // x ∈ S }), ↑c 1 (↑y, y)}
x✝² x✝¹ : M × { x // x ∈ S }
p : M
q : { x // x ∈ S }
x : M
y : { x // x ∈ S }
x✝ : ↑(r' S) (p, q) (x, y)
t : { x // x ∈ S }
ht : ↑t * (↑(x, y).snd * (p, q).fst) = ↑t * (↑(p, q).snd * (x, y).fst)
⊢ ↑b (1 * (p, q)) (1 * (x, y))
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.37854
inst✝¹ : CommMonoid N
P : Type ?u.37860
inst✝ : CommMonoid P
b : Con (M × { x // x ∈ S })
H : b ∈ {c | ∀ (y : { x // x ∈ S }), ↑c 1 (↑y, y)}
x✝² x✝¹ : M × { x // x ∈ S }
p : M
q : { x // x ∈ S }
x : M
y : { x // x ∈ S }
x✝ : ↑(r' S) (p, q) (x, y)
t : { x // x ∈ S }
ht : ↑t * (↑(x, y).snd * (p, q).fst) = ↑t * (↑(p, q).snd * (x, y).fst)
⊢ ↑b (p, q) (x, y)
rw [← one_mul (p, q), ← one_mul (x, y)]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.37854
inst✝¹ : CommMonoid N
P : Type ?u.37860
inst✝ : CommMonoid P
b : Con (M × { x // x ∈ S })
H : b ∈ {c | ∀ (y : { x // x ∈ S }), ↑c 1 (↑y, y)}
x✝² x✝¹ : M × { x // x ∈ S }
p : M
q : { x // x ∈ S }
x : M
y : { x // x ∈ S }
x✝ : ↑(r' S) (p, q) (x, y)
t : { x // x ∈ S }
ht : ↑t * (↑(x, y).snd * (p, q).fst) = ↑t * (↑(p, q).snd * (x, y).fst)
⊢ ↑b ((↑(t * y), t * y) * (p, q)) (1 * (x, y))
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.37854
inst✝¹ : CommMonoid N
P : Type ?u.37860
inst✝ : CommMonoid P
b : Con (M × { x // x ∈ S })
H : b ∈ {c | ∀ (y : { x // x ∈ S }), ↑c 1 (↑y, y)}
x✝² x✝¹ : M × { x // x ∈ S }
p : M
q : { x // x ∈ S }
x : M
y : { x // x ∈ S }
x✝ : ↑(r' S) (p, q) (x, y)
t : { x // x ∈ S }
ht : ↑t * (↑(x, y).snd * (p, q).fst) = ↑t * (↑(p, q).snd * (x, y).fst)
⊢ ↑b (1 * (p, q)) (1 * (x, y))
refine b.trans (b.mul (H (t * y)) (b.refl _)) ?_
case h.e'_3
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.37854
inst✝¹ : CommMonoid N
P : Type ?u.37860
inst✝ : CommMonoid P
b : Con (M × { x // x ∈ S })
H : b ∈ {c | ∀ (y : { x // x ∈ S }), ↑c 1 (↑y, y)}
x✝² x✝¹ : M × { x // x ∈ S }
p : M
q : { x // x ∈ S }
x : M
y : { x // x ∈ S }
x✝ : ↑(r' S) (p, q) (x, y)
t : { x // x ∈ S }
ht : ↑t * (↑(x, y).snd * (p, q).fst) = ↑t * (↑(p, q).snd * (x, y).fst)
⊢ (↑(t * y), t * y) * (p, q) = (↑(t * q), t * q) * (x, y)
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.37854
inst✝¹ : CommMonoid N
P : Type ?u.37860
inst✝ : CommMonoid P
b : Con (M × { x // x ∈ S })
H : b ∈ {c | ∀ (y : { x // x ∈ S }), ↑c 1 (↑y, y)}
x✝² x✝¹ : M × { x // x ∈ S }
p : M
q : { x // x ∈ S }
x : M
y : { x // x ∈ S }
x✝ : ↑(r' S) (p, q) (x, y)
t : { x // x ∈ S }
ht : ↑t * (↑(x, y).snd * (p, q).fst) = ↑t * (↑(p, q).snd * (x, y).fst)
⊢ ↑b ((↑(t * y), t * y) * (p, q)) (1 * (x, y))
convert b.symm (b.mul (H (t * q)) (b.refl (x, y))) using 1
case h.e'_3
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.37854
inst✝¹ : CommMonoid N
P : Type ?u.37860
inst✝ : CommMonoid P
b : Con (M × { x // x ∈ S })
H : b ∈ {c | ∀ (y : { x // x ∈ S }), ↑c 1 (↑y, y)}
x✝² x✝¹ : M × { x // x ∈ S }
p : M
q : { x // x ∈ S }
x : M
y : { x // x ∈ S }
x✝ : ↑(r' S) (p, q) (x, y)
t : { x // x ∈ S }
ht : ↑t * (↑y * p) = ↑t * (↑q * x)
⊢ (↑t * ↑y * p, t * y * q) = (↑t * ↑q * x, t * q * y)
case h.e'_3
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.37854
inst✝¹ : CommMonoid N
P : Type ?u.37860
inst✝ : CommMonoid P
b : Con (M × { x // x ∈ S })
H : b ∈ {c | ∀ (y : { x // x ∈ S }), ↑c 1 (↑y, y)}
x✝² x✝¹ : M × { x // x ∈ S }
p : M
q : { x // x ∈ S }
x : M
y : { x // x ∈ S }
x✝ : ↑(r' S) (p, q) (x, y)
t : { x // x ∈ S }
ht : ↑t * (↑(x, y).snd * (p, q).fst) = ↑t * (↑(p, q).snd * (x, y).fst)
⊢ (↑(t * y), t * y) * (p, q) = (↑(t * q), t * q) * (x, y)
dsimp only [Prod.mk_mul_mk, Submonoid.coe_mul] at ht ⊢
no goals
case h.e'_3
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.37854
inst✝¹ : CommMonoid N
P : Type ?u.37860
inst✝ : CommMonoid P
b : Con (M × { x // x ∈ S })
H : b ∈ {c | ∀ (y : { x // x ∈ S }), ↑c 1 (↑y, y)}
x✝² x✝¹ : M × { x // x ∈ S }
p : M
q : { x // x ∈ S }
x : M
y : { x // x ∈ S }
x✝ : ↑(r' S) (p, q) (x, y)
t : { x // x ∈ S }
ht : ↑t * (↑y * p) = ↑t * (↑q * x)
⊢ (↑t * ↑y * p, t * y * q) = (↑t * ↑q * x, t * q * y)
simp_rw [mul_assoc, ht, mul_comm y q]