awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
inst_4 : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : Subtype.mk (p := fun (x : G) ↦ x ∈ Icc 0 a) 0 ⋯ ⋖ b
⊢ 1 ∈ AddMonoidHom.range (OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G))
have h : Eq (α := ℤ) ((OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G) : (a : G) → ℤ) (↑b : G) : ℤ) (1 : ℤ)
Tactic: use b.1
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (hypothesis)
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
inst_4 : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : Subtype.mk (p := fun (x : G) ↦ x ∈ Icc 0 a) 0 ⋯ ⋖ b
⊢ Eq (α := ℤ) ((OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G) : (a : G) → ℤ) (↑b : G) : ℤ) (1 : ℤ)
have this : 0 ≤ (↑b : G)
Tactic: have : 0 ≤ b.1 := hb.1.le
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
inst_4 : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : Subtype.mk (p := fun (x : G) ↦ x ∈ Icc 0 a) 0 ⋯ ⋖ b
this : 0 ≤ (↑b : G)
⊢ Eq (α := ℤ) ((OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G) : (a : G) → ℤ) (↑b : G) : ℤ) (1 : ℤ)
have h : Ico 0 (↑b : G) = {0}
Tactic: suffices Ico 0 b.1 = {0} by simpa [orderAddMonoidHom, addMonoidHom, this]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
inst_4 : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : Subtype.mk (p := fun (x : G) ↦ x ∈ Icc 0 a) 0 ⋯ ⋖ b
this : 0 ≤ (↑b : G)
⊢ Ico 0 (↑b : G) = {0}
have h : ∀ (x : G), x ∈ Ico 0 (↑b : G) ↔ Membership.mem (γ := Finset G) {0} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
inst_4 : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : Subtype.mk (p := fun (x : G) ↦ x ∈ Icc 0 a) 0 ⋯ ⋖ b
this : 0 ≤ (↑b : G)
x : G
⊢ x ∈ Ico 0 (↑b : G) ↔ Membership.mem (γ := Finset G) {0} x
have h : 0 ≤ x ∧ x < (↑b : G) ↔ x = 0
Tactic: simp only [mem_Ico, mem_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
inst_4 : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : Subtype.mk (p := fun (x : G) ↦ x ∈ Icc 0 a) 0 ⋯ ⋖ b
this : 0 ≤ (↑b : G)
x : G
⊢ 0 ≤ x ∧ x < (↑b : G) ↔ x = 0
have h : 0 ≤ x ∧ x < (↑b : G) → x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
inst_4 : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : Subtype.mk (p := fun (x : G) ↦ x ∈ Icc 0 a) 0 ⋯ ⋖ b
this : 0 ≤ (↑b : G)
x : G
h : 0 ≤ x ∧ x < (↑b : G) → x = 0
⊢ 0 ≤ x ∧ x < (↑b : G) ↔ x = 0
have h₁ : x = 0 → 0 ≤ x ∧ x < (↑b : G)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
inst_4 : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : Subtype.mk (p := fun (x : G) ↦ x ∈ Icc 0 a) 0 ⋯ ⋖ b
this : 0 ≤ (↑b : G)
x : G
h₁ : 0 ≤ x
h₂ : x < (↑b : G)
⊢ x = 0
have h : ∀ (hx' : ¬x = 0), False
Tactic: by_contra hx'
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (hypothesis)
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
inst_4 : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : Subtype.mk (p := fun (x : G) ↦ x ∈ Icc 0 a) 0 ⋯ ⋖ b
this : 0 ≤ (↑b : G)
x : G
h₁ : 0 ≤ x
h₂ : x < (↑b : G)
hx' : ¬x = 0
⊢ False
have this₁ : (↑b : G) ∈ Icc 0 a
Tactic: have := b.2
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (hypothesis)
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
inst_4 : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : Subtype.mk (p := fun (x : G) ↦ x ∈ Icc 0 a) 0 ⋯ ⋖ b
this_1 : 0 ≤ (↑b : G)
x : G
h₁ : 0 ≤ x
h₂ : x < (↑b : G)
hx' : ¬x = 0
this : (↑b : G) ∈ Icc 0 a
⊢ False
have this₁ : 0 ≤ (↑b : G) ∧ (↑b : G) ≤ a
Tactic: simp only [Finset.mem_Icc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : AddCommGroup G
inst_5 : LinearOrder G
inst_6 : IsOrderedAddMonoid G
inst_7 : LocallyFiniteOrder G
inst_8 : Nontrivial G
a b : G
⊢ ZeroHom.toFun (↑(OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G)) : ZeroHom G ℤ) a ≤
      ZeroHom.toFun (↑(OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G)) : ZeroHom G ℤ) b ↔
    a ≤ b
have obtain : ∀ (b : G),
  ZeroHom.toFun (↑(OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G)) : ZeroHom G ℤ) a ≤
      ZeroHom.toFun (↑(OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G)) : ZeroHom G ℤ)
        ((fun (x : G) ↦ a + x) b) ↔
    a ≤ (fun (x : G) ↦ a + x) b
Tactic: obtain ⟨b, rfl⟩ := add_left_surjective a b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : AddCommGroup G
inst_5 : LinearOrder G
inst_6 : IsOrderedAddMonoid G
inst_7 : LocallyFiniteOrder G
inst_8 : Nontrivial G
a b : G
⊢ ZeroHom.toFun (↑(OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G)) : ZeroHom G ℤ) a ≤
      ZeroHom.toFun (↑(OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G)) : ZeroHom G ℤ)
        ((fun (x : G) ↦ a + x) b) ↔
    a ≤ (fun (x : G) ↦ a + x) b
have suffices : LE.le (α := ℤ) (0 : ℤ) ((orderAddMonoidHom G : (a : G) → ℤ) b : ℤ) ↔ 0 ≤ b
Tactic: suffices 0 ≤ orderAddMonoidHom G b ↔ 0 ≤ b by simpa
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : AddCommGroup G
inst_5 : LinearOrder G
inst_6 : IsOrderedAddMonoid G
inst_7 : LocallyFiniteOrder G
inst_8 : Nontrivial G
a b : G
⊢ LE.le (α := ℤ) (0 : ℤ) ((orderAddMonoidHom G : (a : G) → ℤ) b : ℤ) ↔ 0 ≤ b
have inl : ∀ (hb : 0 ≤ b), LE.le (α := ℤ) (0 : ℤ) ((orderAddMonoidHom G : (a : G) → ℤ) b : ℤ) ↔ 0 ≤ b
Tactic: obtain hb | hb := le_total 0 b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : AddCommGroup G
inst_5 : LinearOrder G
inst_6 : IsOrderedAddMonoid G
inst_7 : LocallyFiniteOrder G
inst_8 : Nontrivial G
a b : G
inl : ∀ (hb : 0 ≤ b), LE.le (α := ℤ) (0 : ℤ) ((orderAddMonoidHom G : (a : G) → ℤ) b : ℤ) ↔ 0 ≤ b
⊢ LE.le (α := ℤ) (0 : ℤ) ((orderAddMonoidHom G : (a : G) → ℤ) b : ℤ) ↔ 0 ≤ b
have inr : ∀ (hb : b ≤ 0), LE.le (α := ℤ) (0 : ℤ) ((orderAddMonoidHom G : (a : G) → ℤ) b : ℤ) ↔ 0 ≤ b
Tactic: obtain hb | hb := le_total 0 b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (hypothesis)
Goal:
M : Type u_1
G_1 : Type u_2
inst : AddCancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : AddCommGroup G_1
inst_5 : LinearOrder G_1
inst_6 : IsOrderedAddMonoid G_1
inst_7 : LocallyFiniteOrder G_1
G : Type u_3
inst_8 : LinearOrderedCommGroupWithZero G
inst_9 : LocallyFiniteOrder Gˣ
a b : G
h : a ≤ b
⊢ ZeroHom.toFun
      (↑(MonoidWithZeroHom.comp (WithZero.map' (↑(orderMonoidHom Gˣ) : Gˣ →* Multiplicative ℤ))
            (MulEquiv.toMonoidWithZeroHom
              (OrderMonoidIso.toMulEquiv (OrderMonoidIso.symm OrderMonoidIso.withZeroUnits)))) :
        ZeroHom G (WithZero (Multiplicative ℤ)))
      a ≤
    ZeroHom.toFun
      (↑(MonoidWithZeroHom.comp (WithZero.map' (↑(orderMonoidHom Gˣ) : Gˣ →* Multiplicative ℤ))
            (MulEquiv.toMonoidWithZeroHom
              (OrderMonoidIso.toMulEquiv (OrderMonoidIso.symm OrderMonoidIso.withZeroUnits)))) :
        ZeroHom G (WithZero (Multiplicative ℤ)))
      b
have this : Monotone.{u_3, 0} (α := Gˣ)
  (OneHom.toFun (↑(OrderMonoidHom.toMonoidHom (orderMonoidHom Gˣ)) : OneHom Gˣ (Multiplicative ℤ)))
Tactic: have := (orderMonoidHom Gˣ).monotone'
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (hypothesis)
Goal:
G : Type u_3
inst : LinearOrderedCommGroupWithZero G
inst_1 : LocallyFiniteOrder Gˣ
⊢ StrictMono (α := G) (β := WithZero (Multiplicative ℤ))
    (⇑(orderMonoidWithZeroHom G) : (a : G) → WithZero (Multiplicative ℤ))
have this : StrictMono.{u_3, 0} (α := Gˣ) (β := Multiplicative ℤ) (⇑(orderMonoidHom Gˣ) : (a : Gˣ) → Multiplicative ℤ)
Tactic: have := orderMonoidHom_strictMono (G := Gˣ)
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.NatCast (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : Preorder α
inst_2 : ZeroLEOneClass α
inst_3 : AddLeftMono α
⊢ LE.le.{u_1} (α := α) 0 2
have rw : 0 ≤ HAdd.hAdd (α := α) 1 1
Tactic: rw [← one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.NatCast (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : Preorder α
inst_2 : ZeroLEOneClass α
inst_3 : AddLeftMono α
⊢ LE.le.{u_1} (α := α) 0 3
have rw : 0 ≤ HAdd.hAdd (α := α) 2 1
Tactic: rw [← two_add_one_eq_three]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.NatCast (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : Preorder α
inst_2 : ZeroLEOneClass α
inst_3 : AddLeftMono α
⊢ LE.le.{u_1} (α := α) 0 4
have rw : 0 ≤ HAdd.hAdd (α := α) 3 1
Tactic: rw [← three_add_one_eq_four]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.NatCast (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : LE α
inst_2 : ZeroLEOneClass α
inst_3 : AddLeftMono α
⊢ HAdd.hAdd (α := α) 1 0 ≤ HAdd.hAdd (α := α) 1 1
have bc : LE.le.{u_1} (α := α) 0 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.NatCast (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : LE α
inst_2 : ZeroLEOneClass α
inst_3 : AddRightMono α
⊢ HAdd.hAdd (α := α) 0 1 ≤ HAdd.hAdd (α := α) 1 1
have bc : LE.le.{u_1} (α := α) 0 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.NatCast (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : AddLeftMono α
⊢ LT.lt.{u_1} (α := α) 0 3
have rw : 0 < HAdd.hAdd (α := α) 2 1
Tactic: rw [← two_add_one_eq_three]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.NatCast (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : AddLeftMono α
⊢ LT.lt.{u_1} (α := α) 0 4
have rw : 0 < HAdd.hAdd (α := α) 3 1
Tactic: rw [← three_add_one_eq_four]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.NatCast (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : AddLeftStrictMono α
⊢ LT.lt.{u_1} (α := α) 1 2
have rw : 1 < HAdd.hAdd (α := α) 1 1
Tactic: rw [← one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b c d : α
h₁ : a ≤ b
h₂ : c ≤ d
⊢ a * c ≤ b * d
have grw : b * c ≤ b * d
Tactic: grw [h₁, h₂]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b c d : α
h₁ : a ≤ b
h₂ : c ≤ d
grw : b * c ≤ b * d
⊢ a * c ≤ b * d
have grw₁ : b * d ≤ b * d
Tactic: grw [h₁, h₂]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (hypothesis)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ a₂ * b₂ ≤ a₁ * b₁ ↔ a₁ = a₂ ∧ b₁ = b₂
have this : MulLeftMono α
Tactic: haveI := mulLeftMono_of_mulLeftStrictMono α
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (hypothesis)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
this : MulLeftMono α
⊢ a₂ * b₂ ≤ a₁ * b₁ ↔ a₁ = a₂ ∧ b₁ = b₂
have this₁ : MulRightMono α
Tactic: haveI := mulRightMono_of_mulRightStrictMono α
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
this_1 : MulLeftMono α
this : MulRightMono α
⊢ a₂ * b₂ ≤ a₁ * b₁ ↔ a₁ = a₂ ∧ b₁ = b₂
have refine : ∀ (h : a₂ * b₂ ≤ a₁ * b₁), a₁ = a₂ ∧ b₁ = b₂
Tactic: refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
this_1 : MulLeftMono α
this : MulRightMono α
h : a₂ * b₂ ≤ a₁ * b₁
⊢ a₁ = a₂ ∧ b₁ = b₂
have simp : ¬a₁ < a₂ ∧ ¬b₁ < b₂
Tactic: simp only [eq_iff_le_not_lt, ha, hb, true_and]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
this_1 : MulLeftMono α
this : MulRightMono α
h : a₂ * b₂ ≤ a₁ * b₁
⊢ ¬a₁ < a₂ ∧ ¬b₁ < b₂
have refine_1 : ∀ (ha : a₁ < a₂), a₁ * b₁ < a₂ * b₂
Tactic: refine ⟨fun ha ↦ h.not_gt ?_, fun hb ↦ h.not_gt ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
this_1 : MulLeftMono α
this : MulRightMono α
h : a₂ * b₂ ≤ a₁ * b₁
refine_1 : ∀ (ha : a₁ < a₂), a₁ * b₁ < a₂ * b₂
⊢ ¬a₁ < a₂ ∧ ¬b₁ < b₂
have refine_2 : ∀ (hb : b₁ < b₂), a₁ * b₁ < a₂ * b₂
Tactic: refine ⟨fun ha ↦ h.not_gt ?_, fun hb ↦ h.not_gt ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (hypothesis)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
⊢ a * b = c * d ↔ a = c ∧ b = d
have this : MulLeftMono α
Tactic: haveI := mulLeftMono_of_mulLeftStrictMono α
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (hypothesis)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this : MulLeftMono α
⊢ a * b = c * d ↔ a = c ∧ b = d
have this₁ : MulRightMono α
Tactic: haveI := mulRightMono_of_mulRightStrictMono α
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this_1 : MulLeftMono α
this : MulRightMono α
⊢ a * b = c * d ↔ a = c ∧ b = d
have rw : a * b ≤ c * d ∧ c * d ≤ a * b ↔ a = c ∧ b = d
Tactic: rw [le_antisymm_iff, eq_true (mul_le_mul' hac hbd), true_and, mul_le_mul_iff_of_ge hac hbd]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this_1 : MulLeftMono α
this : MulRightMono α
rw : a * b ≤ c * d ∧ c * d ≤ a * b ↔ a = c ∧ b = d
⊢ a * b = c * d ↔ a = c ∧ b = d
have rw₁ : True ∧ c * d ≤ a * b ↔ a = c ∧ b = d
Tactic: rw [le_antisymm_iff, eq_true (mul_le_mul' hac hbd), true_and, mul_le_mul_iff_of_ge hac hbd]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this_1 : MulLeftMono α
this : MulRightMono α
rw : a * b ≤ c * d ∧ c * d ≤ a * b ↔ a = c ∧ b = d
rw₁ : True ∧ c * d ≤ a * b ↔ a = c ∧ b = d
⊢ a * b = c * d ↔ a = c ∧ b = d
have rw₂ : c * d ≤ a * b ↔ a = c ∧ b = d
Tactic: rw [le_antisymm_iff, eq_true (mul_le_mul' hac hbd), true_and, mul_le_mul_iff_of_ge hac hbd]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this_1 : MulLeftMono α
this : MulRightMono α
rw : a * b ≤ c * d ∧ c * d ≤ a * b ↔ a = c ∧ b = d
rw₁ : True ∧ c * d ≤ a * b ↔ a = c ∧ b = d
rw₂ : c * d ≤ a * b ↔ a = c ∧ b = d
⊢ a * b = c * d ↔ a = c ∧ b = d
have rw₃ : a = c ∧ b = d ↔ a = c ∧ b = d
Tactic: rw [le_antisymm_iff, eq_true (mul_le_mul' hac hbd), true_and, mul_le_mul_iff_of_ge hac hbd]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulRightStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
⊢ c * a = b * a ↔ c = b
have refine : ∀ (h' : c * a = b * a), c = b
Tactic: refine ⟨fun h' => ?_, (· ▸ rfl)⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulRightStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : c * a = b * a
⊢ c = b
have contrapose : ∀ (h' : ¬c = b), ¬c * a = b * a
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 : PartialOrder α
inst_2 : MulRightStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : ¬c = b
⊢ ¬c * a = b * a
have inl : ∀ (h : b ≤ c), ¬c * a = b * a
Tactic: obtain h | h := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulRightStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : ¬c = b
inl : ∀ (h : b ≤ c), ¬c * a = b * a
⊢ ¬c * a = b * a
have inr : ∀ (h : c ≤ b), ¬c * a = b * a
Tactic: obtain h | h := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
⊢ a * c = a * b ↔ c = b
have refine : ∀ (h' : a * c = a * b), c = b
Tactic: refine ⟨fun h' => ?_, (· ▸ rfl)⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : a * c = a * b
⊢ c = b
have contrapose : ∀ (h' : ¬c = b), ¬a * c = 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 : PartialOrder α
inst_2 : MulLeftStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : ¬c = b
⊢ ¬a * c = a * b
have inl : ∀ (h : b ≤ c), ¬a * c = a * b
Tactic: obtain h | h := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : ¬c = b
inl : ∀ (h : b ≤ c), ¬a * c = a * b
⊢ ¬a * c = a * b
have inr : ∀ (h : c ≤ b), ¬a * c = a * b
Tactic: obtain h | h := 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 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
h : a * b = c * d
⊢ a = c ∧ b = d ∨ a < c ∨ b < d
have inl : ∀ (hac : a < c), a = c ∧ b = d ∨ a < c ∨ b < d
Tactic: obtain hac | rfl | hca := lt_trichotomy a c
-- 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 : MulRightStrictMono α
h : a * b = c * d
inl : ∀ (hac : a < c), a = c ∧ b = d ∨ a < c ∨ b < d
⊢ a = c ∧ b = d ∨ a < c ∨ b < d
have inr : ∀ (h : a * b = a * d), a = a ∧ b = d ∨ a < a ∨ b < d
Tactic: obtain hac | rfl | hca := lt_trichotomy a c
Cleared hypotheses: c, 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 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
h : a * b = c * d
inl : ∀ (hac : a < c), a = c ∧ b = d ∨ a < c ∨ b < d
inr : ∀ (h : a * b = a * d), a = a ∧ b = d ∨ a < a ∨ b < d
⊢ a = c ∧ b = d ∨ a < c ∨ b < d
have inr₁ : ∀ (hca : c < a), a = c ∧ b = d ∨ a < c ∨ b < d
Tactic: obtain hac | rfl | hca := lt_trichotomy a c
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b d : α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
h : a * b = a * d
⊢ a = a ∧ b = d ∨ a < a ∨ b < d
have inr : a = a ∧ b = d
Tactic: left
-- 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 : MulRightStrictMono α
h : a * b = c * d
hca : c < a
⊢ a = c ∧ b = d ∨ a < c ∨ b < d
have inr : ∀ (hbd : b < d), a = c ∧ b = d ∨ a < c ∨ b < d
Tactic: obtain hbd | rfl | hdb := lt_trichotomy b d
-- 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 : MulRightStrictMono α
h : a * b = c * d
hca : c < a
inr : ∀ (hbd : b < d), a = c ∧ b = d ∨ a < c ∨ b < d
⊢ a = c ∧ b = d ∨ a < c ∨ b < d
have inr₁ : ∀ (h : a * b = c * b), a = c ∧ b = b ∨ a < c ∨ b < b
Tactic: obtain hbd | rfl | hdb := lt_trichotomy b d
Cleared hypotheses: d, 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 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
h : a * b = c * d
hca : c < a
inr : ∀ (hbd : b < d), a = c ∧ b = d ∨ a < c ∨ b < d
inr₁ : ∀ (h : a * b = c * b), a = c ∧ b = b ∨ a < c ∨ b < b
⊢ a = c ∧ b = d ∨ a < c ∨ b < d
have inr₂ : ∀ (hdb : d < b), a = c ∧ b = d ∨ a < c ∨ b < d
Tactic: obtain hbd | rfl | hdb := lt_trichotomy b d
-- 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 : MulRightMono α
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_lt_iff, lt_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 : 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 : MulLeftStrictMono α
inst_3 : MulRightMono α
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]