α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
⊢ (∃ x, b = a * x ∧ a ≠ b) ↔ ∃ c, c > 1 ∧ b = a * c
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
⊢ a < b ↔ ∃ c, c > 1 ∧ b = a * c
rw [lt_iff_le_and_ne, le_iff_exists_mul, ←exists_and_right]
case h
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
⊢ ∀ (a_1 : α), b = a * a_1 ∧ a ≠ b ↔ a_1 > 1 ∧ b = a * a_1
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
⊢ (∃ x, b = a * x ∧ a ≠ b) ↔ ∃ c, c > 1 ∧ b = a * c
apply exists_congr
case h
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a b c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ b = a * c ∧ a ≠ b ↔ c > 1 ∧ b = a * c
case h
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
⊢ ∀ (a_1 : α), b = a * a_1 ∧ a ≠ b ↔ a_1 > 1 ∧ b = a * a_1
intro c
case h
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a b c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ b = a * c → (a ≠ b ↔ 1 < c)
case h
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a b c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ b = a * c ∧ a ≠ b ↔ c > 1 ∧ b = a * c
rw [and_comm, and_congr_left_iff, gt_iff_lt]
case h
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ a ≠ a * c ↔ 1 < c
case h
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a b c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ b = a * c → (a ≠ b ↔ 1 < c)
rintro rfl
case h.mp
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ a ≠ a * c → 1 < c

case h.mpr
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ 1 < c → a ≠ a * c
case h
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ a ≠ a * c ↔ 1 < c
constructor
case h.mp
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ a ≠ a * c → c ≠ 1
case h.mp
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ a ≠ a * c → 1 < c
rw [one_lt_iff_ne_one]
case h.mp.h₁
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ c = 1 → a = a * c
case h.mp
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ a ≠ a * c → c ≠ 1
apply mt
case h.mp.h₁
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
⊢ a = a * 1
case h.mp.h₁
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ c = 1 → a = a * c
rintro rfl
no goals
case h.mp.h₁
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
⊢ a = a * 1
rw [mul_one]
case h.mpr
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ 1 < c → a < a * c
case h.mpr
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ 1 < c → a ≠ a * c
rw [← (self_le_mul_right a c).lt_iff_ne]
no goals
case h.mpr
α : Type u
inst✝¹ : CanonicallyOrderedMonoid α
a c✝ d : α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
c : α
⊢ 1 < c → a < a * c
apply lt_mul_of_one_lt_right'