case intro
α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ExistsMulOfLE α
a c : α
h : a < a * c
⊢ ∃ c_1, 1 < c_1 ∧ a * c_1 = a * c
α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ExistsMulOfLE α
a b : α
h : a < b
⊢ ∃ c, 1 < c ∧ a * c = b
obtain ⟨c, rfl⟩ := exists_mul_of_le h.le
no goals
case intro
α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ExistsMulOfLE α
a c : α
h : a < a * c
⊢ ∃ c_1, 1 < c_1 ∧ a * c_1 = a * c
exact ⟨c, one_lt_of_lt_mul_right h, rfl⟩