awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
h : Contravariant N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r (b * a * a⁻¹) (c * a * a⁻¹)

Tactic:
rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a] at bc

Premises used: mul_inv_cancel_right
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
h : Contravariant N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r
a b c : N
bc : r (b * a * a⁻¹) (c * a * a⁻¹)
⊢ r (swap (φ := fun (a a_1 : N) ↦ N) (fun (x1 x2 : N) ↦ x1 * x2) a b)
    (swap (φ := fun (a a_1 : N) ↦ N) (fun (x1 x2 : N) ↦ x1 * x2) a c)

Tactic:
h a⁻¹ bc

Premises used: Inv.inv
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
h : Contravariant N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r
a b c : N
bc : r (b * a * a⁻¹) (c * a * a⁻¹)
⊢ r (swap (φ := fun (a a_1 : N) ↦ N) (fun (x1 x2 : N) ↦ x1 * x2) a b)
    (swap (φ := fun (a a_1 : N) ↦ N) (fun (x1 x2 : N) ↦ x1 * x2) a c)

Tactic:
exact h a⁻¹ bc

Premises used: Inv.inv
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst : CovariantClass M N μ r
inst_1 : Group N
inst_2 : CovariantClass N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r
⊢ ContravariantClass N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r

Tactic:
⟨Group.covariant_swap_iff_contravariant_swap.mp CovariantClass.elim⟩

Premises used: Group.covariant_swap_iff_contravariant_swap, CovariantClass.elim, ContravariantClass.mk, Iff.mp
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
inst : Group N
inst_1 : LT N
inst_2 : MulRightStrictMono N
⊢ MulRightReflectLT N

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst : CovariantClass M N μ r
inst_1 : IsTrans N r
m : M
a b c : N
ab : r a b
rl : r (μ m b) c
⊢ r (μ m a) c

Tactic:
_root_.trans (act_rel_act_of_rel m ab) rl

Premises used: trans, act_rel_act_of_rel
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst : CovariantClass M N μ r
inst_1 : IsTrans N r
m : M
a b c : N
ab : r a b
rr : r c (μ m a)
⊢ r c (μ m b)

Tactic:
_root_.trans rr (act_rel_act_of_rel _ ab)

Premises used: trans, act_rel_act_of_rel
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
mu : N → N → N
inst : IsTrans N r
i : CovariantClass N N mu r
i' : CovariantClass N N (swap (φ := fun (a a_1 : N) ↦ N) mu) r
a b c d : N
ab : r a b
cd : r c d
⊢ r (mu a c) (mu b d)

Tactic:
_root_.trans (@act_rel_act_of_rel _ _ (swap mu) r _ c _ _ ab) (act_rel_act_of_rel b cd)

Premises used: trans, act_rel_act_of_rel
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst : ContravariantClass M N μ r
m : M
a b : N
ab : r (μ m a) (μ m b)
⊢ r a b

Tactic:
ContravariantClass.elim _ ab

Premises used: ContravariantClass.elim
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst : ContravariantClass M N μ r
inst_1 : IsTrans N r
m : M
a b c : N
ab : r (μ m a) b
rl : r (μ m b) (μ m c)
⊢ r (μ m a) c

Tactic:
_root_.trans ab (rel_of_act_rel_act m rl)

Premises used: trans, rel_of_act_rel_act
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst : ContravariantClass M N μ r
inst_1 : IsTrans N r
m : M
a b c : N
ab : r (μ m a) (μ m b)
rr : r b (μ m c)
⊢ r a (μ m c)

Tactic:
_root_.trans (rel_of_act_rel_act m ab) rr

Premises used: trans, rel_of_act_rel_act
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
inst : Preorder N
inst_1 : CovariantClass M N μ fun (x1 x2 : N) ↦ x1 ≤ x2
m : M
⊢ Monotone (μ m)

Tactic:
fun _ _ ↦ CovariantClass.elim m

Premises used: Monotone, CovariantClass.elim
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
α : Type u_3
inst : Preorder α
inst_1 : Preorder N
f : N → α
inst_2 : CovariantClass M N μ fun (x1 x2 : N) ↦ x1 ≤ x2
hf : Monotone f
m : M
⊢ Monotone.{u_2, u_3} (β := α) fun (x : N) ↦ f (μ m x)

Tactic:
hf.comp (Covariant.monotone_of_const m)

Premises used: Monotone.comp, Covariant.monotone_of_const
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
α : Type u_3
inst : Preorder α
inst_1 : Preorder N
f : N → α
μ : N → N → N
inst_2 : CovariantClass N N (swap (φ := fun (a a_1 : N) ↦ N) μ) fun (x1 x2 : N) ↦ x1 ≤ x2
hf : Monotone f
m : N
⊢ Monotone.{u_2, u_3} (β := α) fun (x : N) ↦ f (μ x m)

Tactic:
Monotone.covariant_of_const (μ := swap μ) hf m

Premises used: Monotone.covariant_of_const
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
α : Type u_3
inst : Preorder α
inst_1 : Preorder N
f : N → α
inst_2 : CovariantClass M N μ fun (x1 x2 : N) ↦ x1 ≤ x2
hf : Antitone f
m : M
⊢ Antitone.{u_2, u_3} (β := α) fun (x : N) ↦ f (μ m x)

Tactic:
hf.comp_monotone <| Covariant.monotone_of_const m

Premises used: Antitone.comp_monotone, Covariant.monotone_of_const
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
α : Type u_3
inst : Preorder α
inst_1 : Preorder N
f : N → α
μ : N → N → N
inst_2 : CovariantClass N N (swap (φ := fun (a a_1 : N) ↦ N) μ) fun (x1 x2 : N) ↦ x1 ≤ x2
hf : Antitone f
m : N
⊢ Antitone.{u_2, u_3} (β := α) fun (x : N) ↦ f (μ x m)

Tactic:
Antitone.covariant_of_const (μ := swap μ) hf m

Premises used: Antitone.covariant_of_const
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
inst : PartialOrder N
h : Covariant M N μ fun (x1 x2 : N) ↦ x1 < x2
a : M
b c : N
bc : b ≤ c
inl : ∀ (bc : b ≤ b), μ a b ≤ μ a b
inr : ∀ (bc : b < c), μ a b ≤ μ a c
⊢ μ a b ≤ μ a c

Tactic:
rcases bc.eq_or_lt with (rfl | bc)

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
inst : PartialOrder N
h : Covariant M N μ fun (x1 x2 : N) ↦ x1 < x2
a : M
b : N
bc : b ≤ b
⊢ μ a b ≤ μ a b

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
inst : PartialOrder N
h : Covariant M N μ fun (x1 x2 : N) ↦ x1 < x2
a : M
b : N
bc : b ≤ b
⊢ μ a b ≤ μ a b

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
inst : PartialOrder N
h : Covariant M N μ fun (x1 x2 : N) ↦ x1 < x2
a : M
b c : N
bc_1 : b ≤ c
bc : b < c
⊢ μ a b ≤ μ a c

Tactic:
(h _ bc).le

Premises used: LT.lt.le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
inst : PartialOrder N
h : Covariant M N μ fun (x1 x2 : N) ↦ x1 < x2
a : M
b c : N
bc_1 : b ≤ c
bc : b < c
⊢ μ a b ≤ μ a c

Tactic:
exact (h _ bc).le

Premises used: LT.lt.le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
inst : PartialOrder N
inst_1 : CovariantClass M N μ fun (x1 x2 : N) ↦ x1 < x2
⊢ CovariantClass M N μ fun (x1 x2 : N) ↦ x1 ≤ x2

Tactic:
⟨covariant_le_of_covariant_lt _ _ _ CovariantClass.elim⟩

Premises used: CovariantClass.mk, CovariantClass.elim, covariant_le_of_covariant_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_3
inst : Mul M
inst_1 : PartialOrder M
inst_2 : MulLeftStrictMono M
⊢ MulLeftMono M

Tactic:
covariantClass_le_of_lt _ _ _

Premises used: covariantClass_le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_3
inst : Mul M
inst_1 : PartialOrder M
inst_2 : MulRightStrictMono M
⊢ MulRightMono M

Tactic:
covariantClass_le_of_lt _ _ _

Premises used: covariantClass_le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
inst : PartialOrder N
⊢ (Contravariant M N μ fun (x1 x2 : N) ↦ x1 ≤ x2) ↔
    (Contravariant M N μ fun (x1 x2 : N) ↦ x1 < x2) ∧ Contravariant M N μ fun (x1 x2 : N) ↦ x1 = x2

Tactic:
⟨fun h ↦ ⟨fun a b c bc ↦ ?_, fun a b c bc ↦ ?_⟩, fun h ↦ fun a b c bc ↦ ?_⟩

Premises used: And.intro, Iff.intro
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
inst : PartialOrder N
refine_1 :
  ∀ (h : Contravariant M N μ fun (x1 x2 : N) ↦ x1 ≤ x2) (a : M) (b c : N)
    (bc : (fun (x1 x2 : N) ↦ x1 < x2) (μ a b) (μ a c)), (fun (x1 x2 : N) ↦ x1 < x2) b c
refine_2 :
  ∀ (h : Contravariant M N μ fun (x1 x2 : N) ↦ x1 ≤ x2) (a : M) (b c : N)
    (bc : (fun (x1 x2 : N) ↦ x1 = x2) (μ a b) (μ a c)), (fun (x1 x2 : N) ↦ x1 = x2) b c
refine_3 :
  ∀ (h : (Contravariant M N μ fun (x1 x2 : N) ↦ x1 < x2) ∧ Contravariant M N μ fun (x1 x2 : N) ↦ x1 = x2) (a : M)
    (b c : N) (bc : (fun (x1 x2 : N) ↦ x1 ≤ x2) (μ a b) (μ a c)), (fun (x1 x2 : N) ↦ x1 ≤ x2) b c
⊢ (Contravariant M N μ fun (x1 x2 : N) ↦ x1 ≤ x2) ↔
    (Contravariant M N μ fun (x1 x2 : N) ↦ x1 < x2) ∧ Contravariant M N μ fun (x1 x2 : N) ↦ x1 = x2

Tactic:
refine ⟨fun h ↦ ⟨fun a b c bc ↦ ?_, fun a b c bc ↦ ?_⟩, fun h ↦ fun a b c bc ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
inst : PartialOrder N
h : Contravariant M N μ fun (x1 x2 : N) ↦ x1 ≤ x2
a : M
b : N
bc : μ a b < μ a b
⊢ False

Tactic:
lt_irrefl _ bc

Premises used: lt_irrefl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
inst : PartialOrder N
h : Contravariant M N μ fun (x1 x2 : N) ↦ x1 ≤ x2
a : M
b : N
bc : μ a b < μ a b
⊢ False

Tactic:
exact lt_irrefl _ bc

Premises used: lt_irrefl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
inst : PartialOrder N
h : Contravariant M N μ fun (x1 x2 : N) ↦ x1 ≤ x2
a : M
b c : N
bc : (fun (x1 x2 : N) ↦ x1 < x2) (μ a b) (μ a c)
⊢ (fun (x1 x2 : N) ↦ x1 < x2) b c

Tactic:
exact (h a bc.le).lt_of_ne (by rintro rfl; exact lt_irrefl _ bc)

Premises used: LT.lt.le, LE.le.lt_of_ne
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
inst : PartialOrder N
h : Contravariant M N μ fun (x1 x2 : N) ↦ x1 ≤ x2
a : M
b c : N
bc : (fun (x1 x2 : N) ↦ x1 = x2) (μ a b) (μ a c)
⊢ (fun (x1 x2 : N) ↦ x1 = x2) b c

Tactic:
(h a bc.le).antisymm (h a bc.ge)

Premises used: Eq.ge, LE.le.antisymm, Eq.le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
inst : PartialOrder N
h : Contravariant M N μ fun (x1 x2 : N) ↦ x1 ≤ x2
a : M
b c : N
bc : (fun (x1 x2 : N) ↦ x1 = x2) (μ a b) (μ a c)
⊢ (fun (x1 x2 : N) ↦ x1 = x2) b c

Tactic:
exact (h a bc.le).antisymm (h a bc.ge)

Premises used: Eq.ge, LE.le.antisymm, Eq.le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
inst : PartialOrder N
h : (Contravariant M N μ fun (x1 x2 : N) ↦ x1 < x2) ∧ Contravariant M N μ fun (x1 x2 : N) ↦ x1 = x2
a : M
b c : N
bc : (fun (x1 x2 : N) ↦ x1 ≤ x2) (μ a b) (μ a c)
⊢ (fun (x1 x2 : N) ↦ x1 ≤ x2) b c

Tactic:
bc.lt_or_eq.elim (fun bc ↦ (h.1 a bc).le) (fun bc ↦ (h.2 a bc).le)

Premises used: LE.le.lt_or_eq, LT.lt.le, Eq.le, And.right, And.left, Or.elim
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
inst : PartialOrder N
h : (Contravariant M N μ fun (x1 x2 : N) ↦ x1 < x2) ∧ Contravariant M N μ fun (x1 x2 : N) ↦ x1 = x2
a : M
b c : N
bc : (fun (x1 x2 : N) ↦ x1 ≤ x2) (μ a b) (μ a c)
⊢ (fun (x1 x2 : N) ↦ x1 ≤ x2) b c

Tactic:
exact bc.lt_or_eq.elim (fun bc ↦ (h.1 a bc).le) (fun bc ↦ (h.2 a bc).le)

Premises used: LE.le.lt_or_eq, LT.lt.le, Eq.le, And.right, And.left, Or.elim
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
inst : PartialOrder N
⊢ (Contravariant M N μ fun (x1 x2 : N) ↦ x1 ≤ x2) → Contravariant M N μ fun (x1 x2 : N) ↦ x1 < x2

Tactic:
And.left ∘ (contravariant_le_iff_contravariant_lt_and_eq M N μ).mp

Premises used: Function.comp, And.left, contravariant_le_iff_contravariant_lt_and_eq, Iff.mp
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
inst : LinearOrder N
⊢ (Covariant M N μ fun (x1 x2 : N) ↦ x1 ≤ x2) ↔ Contravariant M N μ fun (x1 x2 : N) ↦ x1 < x2

Tactic:
⟨fun h _ _ _ bc ↦ not_le.mp fun k ↦ bc.not_ge (h _ k),
   fun h _ _ _ bc ↦ not_lt.mp fun k ↦ bc.not_gt (h _ k)⟩

Premises used: not_le, not_lt, LE.le.not_gt, Iff.intro, Iff.mp, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
inst : LinearOrder N
⊢ (Covariant M N μ fun (x1 x2 : N) ↦ x1 < x2) ↔ Contravariant M N μ fun (x1 x2 : N) ↦ x1 ≤ x2

Tactic:
⟨fun h _ _ _ bc ↦ not_lt.mp fun k ↦ bc.not_gt (h _ k),
   fun h _ _ _ bc ↦ not_le.mp fun k ↦ bc.not_ge (h _ k)⟩

Premises used: not_le, not_lt, LE.le.not_gt, Iff.intro, Iff.mp, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
unfold : Covariant N N (fun (b a : N) ↦ mu a b) r ↔ Covariant N N mu r
⊢ Covariant N N (flip mu) r ↔ Covariant N N mu r

Tactic:
unfold flip

Premises used: flip
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Covariant N N (fun (b a : N) ↦ mu a b) r ↔ Covariant N N mu r

Tactic:
simp_rw [h.comm]

Premises used: Std.Commutative.comm
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
unfold : Contravariant N N (fun (b a : N) ↦ mu a b) r ↔ Contravariant N N mu r
⊢ Contravariant N N (flip mu) r ↔ Contravariant N N mu r

Tactic:
unfold flip

Premises used: flip
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Contravariant N N (fun (b a : N) ↦ mu a b) r ↔ Contravariant N N mu r

Tactic:
simp_rw [h.comm]

Premises used: Std.Commutative.comm
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
inst : Mul N
inst_1 : LinearOrder N
inst_2 : MulLeftMono N
⊢ MulLeftReflectLT N

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
inst : Mul N
inst_1 : LinearOrder N
inst_2 : MulRightMono N
⊢ MulRightReflectLT N

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
inst : CommSemigroup N
inst_1 : LE N
inst_2 : MulLeftMono N
⊢ MulRightMono N

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
inst : CommSemigroup N
inst_1 : LT N
inst_2 : MulLeftStrictMono N
⊢ MulRightStrictMono N

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
inst : CommSemigroup N
inst_1 : LT N
inst_2 : MulLeftReflectLT N
⊢ MulRightReflectLT N

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Goal:
α_1 α : Type u
inst : Group α
inst_1 : LE α
⊢ ExistsMulOfLE α

Tactic:
⟨fun {a b} _ => ⟨a⁻¹ * b, (mul_inv_cancel_left _ _).symm⟩⟩

Premises used: HMul.hMul, ExistsMulOfLE.mk, Inv.inv, Exists.intro, Eq.symm, mul_inv_cancel_left
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Goal:
α : Type u
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : ExistsMulOfLE α
a b : α
inst_3 : MulLeftReflectLE α
h : a ≤ b
obtain : ∀ (c : α) (h : a ≤ a * c), ∃ (c_1 : α), 1 ≤ c_1 ∧ a * c_1 = a * c
⊢ ∃ (c : α), 1 ≤ c ∧ a * c = b

Tactic:
obtain ⟨c, rfl⟩ := exists_mul_of_le h

Premises used: rfl, ExistsMulOfLE.exists_mul_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Goal:
α : Type u
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : ExistsMulOfLE α
a : α
inst_3 : MulLeftReflectLE α
c : α
h : a ≤ a * c
⊢ ∃ (c_1 : α), 1 ≤ c_1 ∧ a * c_1 = a * c

Tactic:
⟨c, one_le_of_le_mul_right h, rfl⟩

Premises used: one_le_of_le_mul_right, And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Goal:
α : Type u
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : ExistsMulOfLE α
a : α
inst_3 : MulLeftReflectLE α
c : α
h : a ≤ a * c
⊢ ∃ (c_1 : α), 1 ≤ c_1 ∧ a * c_1 = a * c

Tactic:
exact ⟨c, one_le_of_le_mul_right h, rfl⟩
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Goal:
α : Type u
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : ExistsMulOfLE α
a b : α
inst_3 : MulLeftReflectLT α
h : a < b
obtain : ∀ (c : α) (h : a < a * c), ∃ (c_1 : α), 1 < c_1 ∧ a * c_1 = a * c
⊢ ∃ (c : α), 1 < c ∧ a * c = b

Tactic:
obtain ⟨c, rfl⟩ := exists_mul_of_le h.le

Premises used: LT.lt.le, rfl, ExistsMulOfLE.exists_mul_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Goal:
α : Type u
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : ExistsMulOfLE α
a : α
inst_3 : MulLeftReflectLT α
c : α
h : a < a * c
⊢ ∃ (c_1 : α), 1 < c_1 ∧ a * c_1 = a * c

Tactic:
⟨c, one_lt_of_lt_mul_right h, rfl⟩

Premises used: one_lt_of_lt_mul_right, And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Goal:
α : Type u
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : ExistsMulOfLE α
a : α
inst_3 : MulLeftReflectLT α
c : α
h : a < a * c
⊢ ∃ (c_1 : α), 1 < c_1 ∧ a * c_1 = a * c

Tactic:
exact ⟨c, one_lt_of_lt_mul_right h, rfl⟩
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Goal:
α : Type u
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : ExistsMulOfLE α
a : α
inst_3 : MulLeftMono α
inst_4 : MulLeftReflectLE α
c : α
hc : 1 ≤ c
⊢ a ≤ a * c

Tactic:
le_mul_of_one_le_right' hc

Premises used: le_mul_of_one_le_right'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Goal:
α : Type u
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : ExistsMulOfLE α
a : α
inst_3 : MulLeftMono α
inst_4 : MulLeftReflectLE α
c : α
hc : 1 ≤ c
⊢ a ≤ a * c

Tactic:
exact le_mul_of_one_le_right' hc

Premises used: le_mul_of_one_le_right'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Goal:
α : Type u
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : ExistsMulOfLE α
a : α
inst_3 : MulLeftStrictMono α
inst_4 : MulLeftReflectLT α
c : α
hc : 1 < c
⊢ a < a * c

Tactic:
lt_mul_of_one_lt_right' _ hc

Premises used: lt_mul_of_one_lt_right'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Goal:
α : Type u
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : ExistsMulOfLE α
a : α
inst_3 : MulLeftStrictMono α
inst_4 : MulLeftReflectLT α
c : α
hc : 1 < c
⊢ a < a * c

Tactic:
exact lt_mul_of_one_lt_right' _ hc

Premises used: lt_mul_of_one_lt_right'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Goal:
α : Type u
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : Monoid α
inst_3 : ExistsMulOfLE α
inst_4 : MulLeftReflectLT α
a b : α
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
x : α
hxb : b < x
obtain : ∀ (ε : α) (hxb : b < b * ε), a ≤ b * ε
⊢ a ≤ x

Tactic:
obtain ⟨ε, rfl⟩ := exists_mul_of_le hxb.le

Premises used: LT.lt.le, rfl, ExistsMulOfLE.exists_mul_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Goal:
α : Type u
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : Monoid α
inst_3 : ExistsMulOfLE α
inst_4 : MulLeftReflectLT α
a b : α
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
ε : α
hxb : b < b * ε
⊢ a ≤ b * ε

Tactic:
h _ (one_lt_of_lt_mul_right hxb)

Premises used: one_lt_of_lt_mul_right
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Goal:
α : Type u
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : Monoid α
inst_3 : ExistsMulOfLE α
inst_4 : MulLeftReflectLT α
a b : α
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
ε : α
hxb : b < b * ε
⊢ a ≤ b * ε

Tactic:
exact h _ (one_lt_of_lt_mul_right hxb)

Premises used: one_lt_of_lt_mul_right
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Goal:
α : Type u
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : Monoid α
inst_3 : ExistsMulOfLE α
inst_4 : MulLeftReflectLT α
a b : α
h : ∀ (ε : α), 1 < ε → a < b * ε
⊢ a ≤ b

Tactic:
le_of_forall_one_lt_le_mul fun ε hε => (h ε hε).le

Premises used: le_of_forall_one_lt_le_mul, LT.lt.le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Goal:
α : Type u
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : Monoid α
inst_3 : ExistsMulOfLE α
inst_4 : MulLeftReflectLT α
a b : α
inst_5 : MulLeftStrictMono α
⊢ a ≤ b ↔ ∀ (ε : α), 1 < ε → a < b * ε

Tactic:
⟨fun h _ => lt_mul_of_le_of_one_lt h, le_of_forall_one_lt_lt_mul'⟩

Premises used: le_of_forall_one_lt_lt_mul', Iff.intro, lt_mul_of_le_of_one_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Goal:
α : Type u
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : Monoid α
inst_3 : ExistsMulOfLE α
inst_4 : MulLeftReflectLT α
a b : α
inst_5 : MulLeftStrictMono α
⊢ a ≤ b ↔ ∀ (ε : α), 1 < ε → a ≤ b * ε

Tactic:
⟨fun h _ hε ↦ lt_mul_of_le_of_one_lt h hε |>.le, le_of_forall_one_lt_le_mul⟩

Premises used: le_of_forall_one_lt_le_mul, LT.lt.le, Iff.intro, lt_mul_of_le_of_one_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommSemigroup β
f : α → β
a b : α
⊢ f (min a b) * f (max a b) = f a * f b

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommSemigroup β
f : α → β
a b : α
⊢ f (max a b) * f (min a b) = f a * f b

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : CommSemigroup α
a b : α
⊢ min a b * max a b = a * b

Tactic:
fn_min_mul_fn_max id _ _

Premises used: id, fn_min_mul_fn_max
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : CommSemigroup α
a b : α
⊢ max a b * min a b = a * b

Tactic:
fn_max_mul_fn_min id _ _

Premises used: id, fn_max_mul_fn_min
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
a b c : α
⊢ min (a * b) (a * c) = a * min b c

Tactic:
(monotone_id.const_mul' a).map_min.symm

Premises used: monotone_id, Monotone.const_mul', Monotone.map_min, Eq.symm
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
a b c : α
⊢ max (a * b) (a * c) = a * max b c

Tactic:
(monotone_id.const_mul' a).map_max.symm

Premises used: monotone_id, Monotone.const_mul', Monotone.map_max, Eq.symm
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulRightMono α
a b c : α
⊢ min (a * c) (b * c) = min a b * c

Tactic:
(monotone_id.mul_const' c).map_min.symm

Premises used: monotone_id, Monotone.mul_const', Monotone.map_min, Eq.symm
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulRightMono α
a b c : α
⊢ max (a * c) (b * c) = max a b * c

Tactic:
(monotone_id.mul_const' c).map_max.symm

Premises used: monotone_id, Monotone.mul_const', Monotone.map_max, Eq.symm
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a₁ a₂ b₁ b₂ : α
contrapose! : a₂ ≤ a₁ ∧ b₂ ≤ b₁ → a₂ * b₂ ≤ a₁ * b₁
⊢ a₁ * b₁ < a₂ * b₂ → a₁ < a₂ ∨ b₁ < b₂

Tactic:
contrapose!
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ ≤ a₁ ∧ b₂ ≤ b₁ → a₂ * b₂ ≤ a₁ * b₁

Tactic:
fun h => mul_le_mul' h.1 h.2

Premises used: And.right, And.left, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ ≤ a₁ ∧ b₂ ≤ b₁ → a₂ * b₂ ≤ a₁ * b₁

Tactic:
exact fun h => mul_le_mul' h.1 h.2

Premises used: mul_le_mul'