awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightMono α
h : a * b ≤ c * d
⊢ (a ≤ c ∨ a ≤ d) ∨ b ≤ c ∨ b ≤ d
have contrapose! : ∀ (h : (c < a ∧ d < a) ∧ c < b ∧ d < b), c * d < a * b
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftMono α
inst_3 : MulRightStrictMono α
h : a * b ≤ c * d
⊢ min a b ≤ max c d
have simp_rw : (a ≤ c ∨ a ≤ d) ∨ b ≤ c ∨ b ≤ d
Tactic: simp_rw [min_le_iff, le_max_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftMono α
inst_3 : MulRightStrictMono α
h : a * b ≤ c * d
⊢ (a ≤ c ∨ a ≤ d) ∨ b ≤ c ∨ b ≤ d
have contrapose! : ∀ (h : (c < a ∧ d < a) ∧ c < b ∧ d < b), c * d < a * b
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LE α
inst_2 : MulLeftMono α
inst_3 : MulLeftReflectLE α
a b : α
⊢ a ≤ a * b ↔ a * 1 ≤ a * b
have rw : a ≤ a * b ↔ a ≤ a * b
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LE α
inst_2 : MulRightMono α
inst_3 : MulRightReflectLE α
a b : α
⊢ a ≤ b * a ↔ 1 * a ≤ b * a
have rw : a ≤ b * a ↔ a ≤ b * a
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LE α
inst_2 : MulLeftMono α
inst_3 : MulLeftReflectLE α
a b : α
⊢ a * b ≤ a ↔ a * b ≤ a * 1
have rw : a * b ≤ a ↔ a * b ≤ a
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LE α
inst_2 : MulRightMono α
inst_3 : MulRightReflectLE α
a b : α
⊢ a * b ≤ b ↔ a * b ≤ 1 * b
have rw : a * b ≤ b ↔ a * b ≤ b
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
inst_3 : MulLeftReflectLT α
a b : α
⊢ a < a * b ↔ a * 1 < a * b
have rw : a < a * b ↔ a < a * b
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LT α
inst_2 : MulRightStrictMono α
inst_3 : MulRightReflectLT α
a b : α
⊢ a < b * a ↔ 1 * a < b * a
have rw : a < b * a ↔ a < b * a
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
inst_3 : MulLeftReflectLT α
a b : α
⊢ a * b < a ↔ a * b < a * 1
have rw : a * b < a ↔ a * b < a
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LT α
inst_2 : MulRightStrictMono α
inst_3 : MulRightReflectLT α
a b : α
⊢ a * b < b ↔ a * b < 1 * b
have rw : a * b < b ↔ a * b < b
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
ha hb : LE.le.{u_1} (α := α) 1 1
⊢ HMul.hMul (α := α) 1 1 = 1
have rw : Eq.{u_1 + 1} (α := α) 1 1
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LinearOrder α
inst_2 : MulLeftStrictMono α
a : α
⊢ ∃ (b : α), b * b ≤ a
have pos : ∀ (h : a < 1), ∃ (b : α), b * b ≤ a
Tactic: by_cases! h : a < 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LinearOrder α
inst_2 : MulLeftStrictMono α
a : α
pos : ∀ (h : a < 1), ∃ (b : α), b * b ≤ a
⊢ ∃ (b : α), b * b ≤ a
have neg : ∀ (h : 1 ≤ a), ∃ (b : α), b * b ≤ a
Tactic: by_cases! h : a < 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LinearOrder α
inst_2 : MulLeftStrictMono α
a : α
h : a < 1
⊢ ∃ (b : α), b * b ≤ a
have h₁ : a * a ≤ a
Tactic: use a
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (hypothesis)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LinearOrder α
inst_2 : MulLeftStrictMono α
a : α
h : a < 1
⊢ a * a ≤ a
have this : a * a < a * 1
Tactic: have : a * a < a * 1 := mul_lt_mul_right h a
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (hypothesis)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LinearOrder α
inst_2 : MulLeftStrictMono α
a : α
h : a < 1
this : a * a < a * 1
⊢ a * a ≤ a
have this₁ : a * a < a
Tactic: rw [mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LinearOrder α
inst_2 : MulLeftStrictMono α
a : α
h : 1 ≤ a
⊢ ∃ (b : α), b * b ≤ a
have h₁ : HMul.hMul (α := α) 1 1 ≤ a
Tactic: use 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : IsMulCommutative α
inst_2 : PartialOrder α
a : α
ha : MulLECancellable a
b c : α
h : Eq.{u_1 + 1} (α := α) ((fun (x : α) ↦ x * a) b) ((fun (x : α) ↦ x * a) c)
⊢ a * b = a * c
have rwa : b * a = a * c
Tactic: rwa [mul_comm' a, mul_comm' a]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : LE α
inst_1 : Mul α
inst_2 : IsMulCommutative α
inst_3 : MulLeftMono α
a b c : α
ha : MulLECancellable a
⊢ b * a ≤ c * a ↔ b ≤ c
have rw : a * b ≤ c * a ↔ b ≤ c
Tactic: rw [mul_comm' b, mul_comm' c, ha.mul_le_mul_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : LE α
inst_1 : Mul α
inst_2 : IsMulCommutative α
inst_3 : MulLeftMono α
a b c : α
ha : MulLECancellable a
rw : a * b ≤ c * a ↔ b ≤ c
⊢ b * a ≤ c * a ↔ b ≤ c
have rw₁ : a * b ≤ a * c ↔ b ≤ c
Tactic: rw [mul_comm' b, mul_comm' c, ha.mul_le_mul_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : LE α
inst_1 : Mul α
inst_2 : IsMulCommutative α
inst_3 : MulLeftMono α
a b c : α
ha : MulLECancellable a
rw : a * b ≤ c * a ↔ b ≤ c
rw₁ : a * b ≤ a * c ↔ b ≤ c
⊢ b * a ≤ c * a ↔ b ≤ c
have rw₂ : b ≤ c ↔ b ≤ c
Tactic: rw [mul_comm' b, mul_comm' c, ha.mul_le_mul_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : LE α
inst_1 : MulOneClass α
inst_2 : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ a ≤ a * b ↔ a * 1 ≤ a * b
have rw : a ≤ a * b ↔ a ≤ a * b
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : LE α
inst_1 : MulOneClass α
inst_2 : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ a * b ≤ a ↔ a * b ≤ a * 1
have rw : a * b ≤ a ↔ a * b ≤ a
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : LE α
inst_1 : MulOneClass α
inst_2 : IsMulCommutative α
inst_3 : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ a ≤ b * a ↔ 1 ≤ b
have rw : a ≤ a * b ↔ 1 ≤ b
Tactic: rw [mul_comm', ha.le_mul_iff_one_le_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : LE α
inst_1 : MulOneClass α
inst_2 : IsMulCommutative α
inst_3 : MulLeftMono α
a b : α
ha : MulLECancellable a
rw : a ≤ a * b ↔ 1 ≤ b
⊢ a ≤ b * a ↔ 1 ≤ b
have rw₁ : 1 ≤ b ↔ 1 ≤ b
Tactic: rw [mul_comm', ha.le_mul_iff_one_le_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : LE α
inst_1 : MulOneClass α
inst_2 : IsMulCommutative α
inst_3 : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ b * a ≤ a ↔ b ≤ 1
have rw : a * b ≤ a ↔ b ≤ 1
Tactic: rw [mul_comm', ha.mul_le_iff_le_one_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : LE α
inst_1 : MulOneClass α
inst_2 : IsMulCommutative α
inst_3 : MulLeftMono α
a b : α
ha : MulLECancellable a
rw : a * b ≤ a ↔ b ≤ 1
⊢ b * a ≤ a ↔ b ≤ 1
have rw₁ : b ≤ 1 ↔ b ≤ 1
Tactic: rw [mul_comm', ha.mul_le_iff_le_one_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : LE α
inst_1 : Semigroup α
a b : α
ha : MulLECancellable a
hb : MulLECancellable b
c d : α
hcd : a * b * c ≤ a * b * d
⊢ a * (b * c) ≤ a * (b * d)
have rwa : a * b * c ≤ a * (b * d)
Tactic: rwa [← mul_assoc, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : LE α
inst_1 : Semigroup α
inst_2 : MulLeftMono α
a b : α
h : MulLECancellable (a * b)
c d : α
hcd : b * c ≤ b * d
⊢ a * b * c ≤ a * b * d
have rw : a * (b * c) ≤ a * (b * d)
Tactic: rw [mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Defs (goal)
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
⊢ Covariant N N (fun (x1 x2 : N) ↦ x1 * x2) r ↔ Contravariant N N (fun (x1 x2 : N) ↦ x1 * x2) r
have refine_1 : ∀ (h : Covariant N N (fun (x1 x2 : N) ↦ x1 * x2) r) (a b c : N)
  (bc : r ((fun (x1 x2 : N) ↦ x1 * x2) a b) ((fun (x1 x2 : N) ↦ x1 * x2) a c)), r b c
Tactic: refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Defs (goal)
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
refine_1 :
  ∀ (h : Covariant N N (fun (x1 x2 : N) ↦ x1 * x2) r) (a b c : N)
    (bc : r ((fun (x1 x2 : N) ↦ x1 * x2) a b) ((fun (x1 x2 : N) ↦ x1 * x2) a c)), r b c
⊢ Covariant N N (fun (x1 x2 : N) ↦ x1 * x2) r ↔ Contravariant N N (fun (x1 x2 : N) ↦ x1 * x2) r
have refine_2 : ∀ (h : Contravariant N N (fun (x1 x2 : N) ↦ x1 * x2) r) (a b c : N) (bc : r b c),
  r ((fun (x1 x2 : N) ↦ x1 * x2) a b) ((fun (x1 x2 : N) ↦ x1 * x2) a c)
Tactic: refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Defs (goal)
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
h : Covariant N N (fun (x1 x2 : N) ↦ x1 * x2) r
a b c : N
bc : r ((fun (x1 x2 : N) ↦ x1 * x2) a b) ((fun (x1 x2 : N) ↦ x1 * x2) a c)
⊢ r b c
have refine_1 : r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
Tactic: rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Defs (hypothesis)
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
h : Contravariant N N (fun (x1 x2 : N) ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r ((fun (x1 x2 : N) ↦ x1 * x2) a b) ((fun (x1 x2 : N) ↦ x1 * x2) a c)
have bc₁ : r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
Tactic: rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c] at bc
Cleared hypotheses: bc
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Defs (goal)
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
⊢ Covariant N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r ↔
    Contravariant N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r
have refine_1 : ∀ (h : Covariant N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r) (a b c : N)
  (bc :
    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)),
  r b c
Tactic: refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Defs (goal)
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
refine_1 :
  ∀ (h : Covariant N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r) (a b c : N)
    (bc :
      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)),
    r b c
⊢ Covariant N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r ↔
    Contravariant N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r
have refine_2 : ∀ (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 (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: refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Defs (goal)
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
h : Covariant N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r
a b c : N
bc :
  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)
⊢ r b c
have refine_1 : r (b * a * a⁻¹) (c * a * a⁻¹)
Tactic: rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Defs (hypothesis)
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 (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)
have bc₁ : r (b * a * a⁻¹) (c * a * a⁻¹)
Tactic: rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a] at bc
Cleared hypotheses: bc
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Defs (goal)
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
⊢ μ a b ≤ μ a c
have inl : ∀ (bc : b ≤ b), μ a b ≤ μ a b
Tactic: rcases bc.eq_or_lt with (rfl | bc)
Cleared hypotheses: c, bc
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Defs (goal)
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
⊢ μ a b ≤ μ a c
have inr : ∀ (bc : b < c), μ a b ≤ μ a c
Tactic: rcases bc.eq_or_lt with (rfl | bc)
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Defs (goal)
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
have 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
Tactic: refine ⟨fun h ↦ ⟨fun a b c bc ↦ ?_, fun a b c bc ↦ ?_⟩, fun h ↦ fun a b c bc ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Defs (goal)
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
⊢ (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
have 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
Tactic: refine ⟨fun h ↦ ⟨fun a b c bc ↦ ?_, fun a b c bc ↦ ?_⟩, fun h ↦ fun a b c bc ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Defs (goal)
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
⊢ (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
have 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
Tactic: refine ⟨fun h ↦ ⟨fun a b c bc ↦ ?_, fun a b c bc ↦ ?_⟩, fun h ↦ fun a b c bc ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Defs (goal)
Goal:
N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Covariant N N (flip mu) r ↔ Covariant N N mu r
have unfold : Covariant N N (fun (b a : N) ↦ mu a b) r ↔ Covariant N N mu r
Tactic: unfold flip
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Defs (goal)
Goal:
N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Contravariant N N (flip mu) r ↔ Contravariant N N mu r
have unfold : Contravariant N N (fun (b a : N) ↦ mu a b) r ↔ Contravariant N N mu r
Tactic: unfold flip
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE (goal)
Goal:
α : Type u
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : ExistsMulOfLE α
a b : α
inst_3 : MulLeftReflectLE α
h : a ≤ b
⊢ ∃ (c : α), 1 ≤ c ∧ a * c = b
have obtain : ∀ (c : α) (h : a ≤ a * c), ∃ (c_1 : α), 1 ≤ c_1 ∧ a * c_1 = a * c
Tactic: obtain ⟨c, rfl⟩ := exists_mul_of_le h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE (goal)
Goal:
α : Type u
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : ExistsMulOfLE α
a b : α
inst_3 : MulLeftReflectLT α
h : a < b
⊢ ∃ (c : α), 1 < c ∧ a * c = b
have obtain : ∀ (c : α) (h : a < a * c), ∃ (c_1 : α), 1 < c_1 ∧ a * c_1 = a * c
Tactic: obtain ⟨c, rfl⟩ := exists_mul_of_le h.le
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE (goal)
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
⊢ a ≤ x
have obtain : ∀ (ε : α) (hxb : b < b * ε), a ≤ b * ε
Tactic: obtain ⟨ε, rfl⟩ := exists_mul_of_le hxb.le
Cleared hypotheses: x, hxb
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a₁ a₂ b₁ b₂ : α
⊢ a₁ * b₁ < a₂ * b₂ → a₁ < a₂ ∨ b₁ < b₂
have contrapose! : a₂ ≤ a₁ ∧ b₂ ≤ b₁ → a₂ * b₂ ≤ a₁ * b₁
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
⊢ a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ < b₂
have contrapose! : a₂ < a₁ ∧ b₂ ≤ b₁ → a₂ * b₂ < a₁ * b₁
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightMono α
a₁ a₂ b₁ b₂ : α
⊢ a₁ * b₁ ≤ a₂ * b₂ → a₁ < a₂ ∨ b₁ ≤ b₂
have contrapose! : a₂ ≤ a₁ ∧ b₂ < b₁ → a₂ * b₂ < a₁ * b₁
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
⊢ a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂
have contrapose! : a₂ < a₁ ∧ b₂ < b₁ → a₂ * b₂ < a₁ * b₁
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
inst_4 : MulLeftStrictMono α
inst_5 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ a₁ * b₁ < a₂ * b₂ ↔ a₁ < a₂ ∨ b₁ < b₂
have refine : ∀ (h : a₁ < a₂ ∨ b₁ < b₂), a₁ * b₁ < a₂ * b₂
Tactic: refine ⟨lt_or_lt_of_mul_lt_mul, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
inst_4 : MulLeftStrictMono α
inst_5 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h : a₁ < a₂ ∨ b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂
have inl : ∀ (ha' : a₁ < a₂), a₁ * b₁ < a₂ * b₂
Tactic: rcases h with ha' | hb'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
inst_4 : MulLeftStrictMono α
inst_5 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h : a₁ < a₂ ∨ b₁ < b₂
inl : ∀ (ha' : a₁ < a₂), a₁ * b₁ < a₂ * b₂
⊢ a₁ * b₁ < a₂ * b₂
have inr : ∀ (hb' : b₁ < b₂), a₁ * b₁ < a₂ * b₂
Tactic: rcases h with ha' | hb'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
ha : 1 ≤ a
k : ℕ
⊢ 1 ≤ a ^ (k + 1)
have rw : 1 ≤ a ^ k * a
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
n : ℕ
h : a < 1
hn : n ≠ 0
⊢ a ^ n < 1
have rcases : ∀ (k : ℕ) (hn : k.succ ≠ 0), a ^ k.succ < 1
Tactic: rcases Nat.exists_eq_succ_of_ne_zero hn with ⟨k, rfl⟩
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
h : a < 1
k : ℕ
hn : k.succ ≠ 0
⊢ a ^ k.succ < 1
have rw : a * a ^ k < 1
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
a : M
ha : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ (n + 1)
have rw : a ^ n ≤ a ^ n * a
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
a : M
ha : 1 < a
n : ℕ
⊢ a ^ n < a ^ (n + 1)
have rw : a ^ n < a ^ n * a
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
x : M
hx : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ (n + 1)
have rw : 1 ≤ x ^ n * x
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
n : ℕ
x : M
hn : 0 < n
h : x < 1
⊢ x ^ n < 1
have rcases : ∀ (k : ℕ) (hn : 0 < k.succ), x ^ k.succ < 1
Tactic: rcases Nat.exists_eq_succ_of_ne_zero hn.ne' with ⟨k, rfl⟩
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
x : M
h : x < 1
k : ℕ
hn : 0 < k.succ
⊢ x ^ k.succ < 1
have rw : x ^ k * x < 1
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
⊢ a ^ (n + 2) = a ^ (n + 1) * a
have rw : a ^ (n + 1) * a = a ^ (n + 1) * a
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
⊢ a ^ (n + 1) * a ≤ b ^ n * a * a
have grw : b ^ (n + 1 - 1) * a * a ≤ b ^ n * a * a
Tactic: grw [pow_le_pow_mul_of_sq_le_mul hab (by lia)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Pow (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
a b : M
hab : HPow.hPow (β := ℕ) a 2 ≤ b * a
n : ℕ
h : n + 2 ≠ 0
⊢ b ^ n * a * a = b ^ n * HPow.hPow (β := ℕ) a 2
have rw : b ^ n * (a * a) = b ^ n * HPow.hPow (β := ℕ) a 2
Tactic: rw [mul_assoc, sq]