case intro
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c✝ d : α
h : a < b
c : α
hc : b = a * c
⊢ ∃ c x, a * c = b
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
h : a < b
⊢ ∃ c x, a * c = b
obtain ⟨c, hc⟩ := le_iff_exists_mul.1 h.le
case intro
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c✝ d : α
h : a < b
c : α
hc : b = a * c
⊢ c ≠ 1
case intro
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c✝ d : α
h : a < b
c : α
hc : b = a * c
⊢ ∃ c x, a * c = b
refine' ⟨c, one_lt_iff_ne_one.2 _, hc.symm⟩
case intro
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
h : a < b
hc : b = a * 1
⊢ False
case intro
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c✝ d : α
h : a < b
c : α
hc : b = a * c
⊢ c ≠ 1
rintro rfl
no goals
case intro
α : Type u
inst✝ : CanonicallyOrderedMonoid α
a b c d : α
h : a < b
hc : b = a * 1
⊢ False
simp [hc, lt_irrefl] at h