awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
n : β
hn : n ≠ 0
⊢ Eq (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    ((inr α β : (a : β) → WithZero (Lex (αˣ × βˣ))) n : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    ((↑((OrderMonoidHom.inrₗ αˣ βˣ : (a : βˣ) → Lex (αˣ × βˣ)) (Units.mk0 n hn)) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
      WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
have lift : ∀ (n : βˣ) (hn : (↑n : β) ≠ 0),
  Eq (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    ((inr α β : (a : β) → WithZero (Lex (αˣ × βˣ))) (↑n : β) : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    ((↑((OrderMonoidHom.inrₗ αˣ βˣ : (a : βˣ) → Lex (αˣ × βˣ)) (Units.mk0 (↑n : β) hn)) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
      WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
Tactic: lift n to βˣ using isUnit_iff_ne_zero.mpr hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
m : α
n : β
hm : m ≠ 0
hn : n ≠ 0
⊢ HMul.hMul (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((inl α β : (a : α) → WithZero (Lex (αˣ × βˣ))) m : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((inr α β : (a : β) → WithZero (Lex (αˣ × βˣ))) n : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) =
    (↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) : WithZero (Lex (αˣ × βˣ)))
have rw : HMul.hMul (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    ((↑((OrderMonoidHom.inlₗ αˣ βˣ : (a : αˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm)) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
      WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    ((inr α β : (a : β) → WithZero (Lex (αˣ × βˣ))) n : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) =
  (↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) : WithZero (Lex (αˣ × βˣ)))
Tactic: rw [inl_eq_coe_inlₗ hm, inr_eq_coe_inrₗ hn,
      ← WithZero.coe_mul, OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
m : α
n : β
hm : m ≠ 0
hn : n ≠ 0
rw :
  HMul.hMul (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((↑((OrderMonoidHom.inlₗ αˣ βˣ : (a : αˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm)) :
          WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((inr α β : (a : β) → WithZero (Lex (αˣ × βˣ))) n : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) =
    (↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) : WithZero (Lex (αˣ × βˣ)))
⊢ HMul.hMul (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((inl α β : (a : α) → WithZero (Lex (αˣ × βˣ))) m : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((inr α β : (a : β) → WithZero (Lex (αˣ × βˣ))) n : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) =
    (↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) : WithZero (Lex (αˣ × βˣ)))
have rw₁ : HMul.hMul (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    ((↑((OrderMonoidHom.inlₗ αˣ βˣ : (a : αˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm)) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
      WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
    ((↑((OrderMonoidHom.inrₗ αˣ βˣ : (a : βˣ) → Lex (αˣ × βˣ)) (Units.mk0 n hn)) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
      WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) =
  (↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) : WithZero (Lex (αˣ × βˣ)))
Tactic: rw [inl_eq_coe_inlₗ hm, inr_eq_coe_inrₗ hn,
      ← WithZero.coe_mul, OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
m : α
n : β
hm : m ≠ 0
hn : n ≠ 0
rw :
  HMul.hMul (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((↑((OrderMonoidHom.inlₗ αˣ βˣ : (a : αˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm)) :
          WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((inr α β : (a : β) → WithZero (Lex (αˣ × βˣ))) n : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) =
    (↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) : WithZero (Lex (αˣ × βˣ)))
rw₁ :
  HMul.hMul (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((↑((OrderMonoidHom.inlₗ αˣ βˣ : (a : αˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm)) :
          WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((↑((OrderMonoidHom.inrₗ αˣ βˣ : (a : βˣ) → Lex (αˣ × βˣ)) (Units.mk0 n hn)) :
          WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) =
    (↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) : WithZero (Lex (αˣ × βˣ)))
⊢ HMul.hMul (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((inl α β : (a : α) → WithZero (Lex (αˣ × βˣ))) m : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((inr α β : (a : β) → WithZero (Lex (αˣ × βˣ))) n : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) =
    (↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) : WithZero (Lex (αˣ × βˣ)))
have rw₂ : (↑(HMul.hMul (α := Lex (Prod.{u_1, u_2} αˣ βˣ)) (β := Lex (Prod.{u_1, u_2} αˣ βˣ))
        ((OrderMonoidHom.inlₗ αˣ βˣ : (a : αˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm) : Lex (Prod.{u_1, u_2} αˣ βˣ))
        ((OrderMonoidHom.inrₗ αˣ βˣ : (a : βˣ) → Lex (αˣ × βˣ)) (Units.mk0 n hn) : Lex (Prod.{u_1, u_2} αˣ βˣ))) :
    WithZero (Lex (αˣ × βˣ))) =
  (↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) : WithZero (Lex (αˣ × βˣ)))
Tactic: rw [inl_eq_coe_inlₗ hm, inr_eq_coe_inrₗ hn,
      ← WithZero.coe_mul, OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrderedCommGroupWithZero α
inst_1 : LinearOrderedCommGroupWithZero β
m : α
n : β
hm : m ≠ 0
hn : n ≠ 0
rw :
  HMul.hMul (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((↑((OrderMonoidHom.inlₗ αˣ βˣ : (a : αˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm)) :
          WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((inr α β : (a : β) → WithZero (Lex (αˣ × βˣ))) n : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) =
    (↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) : WithZero (Lex (αˣ × βˣ)))
rw₁ :
  HMul.hMul (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((↑((OrderMonoidHom.inlₗ αˣ βˣ : (a : αˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm)) :
          WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((↑((OrderMonoidHom.inrₗ αˣ βˣ : (a : βˣ) → Lex (αˣ × βˣ)) (Units.mk0 n hn)) :
          WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
        WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) =
    (↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) : WithZero (Lex (αˣ × βˣ)))
rw₂ :
  (↑(HMul.hMul (α := Lex (Prod.{u_1, u_2} αˣ βˣ)) (β := Lex (Prod.{u_1, u_2} αˣ βˣ))
          ((OrderMonoidHom.inlₗ αˣ βˣ : (a : αˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm) : Lex (Prod.{u_1, u_2} αˣ βˣ))
          ((OrderMonoidHom.inrₗ αˣ βˣ : (a : βˣ) → Lex (αˣ × βˣ)) (Units.mk0 n hn) : Lex (Prod.{u_1, u_2} αˣ βˣ))) :
      WithZero (Lex (αˣ × βˣ))) =
    (↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) : WithZero (Lex (αˣ × βˣ)))
⊢ HMul.hMul (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) (β := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((inl α β : (a : α) → WithZero (Lex (αˣ × βˣ))) m : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
      ((inr α β : (a : β) → WithZero (Lex (αˣ × βˣ))) n : WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) =
    (↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) : WithZero (Lex (αˣ × βˣ)))
have rw₃ : Eq (α := WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
  ((↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) :
      WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
    WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
  ((↑((toLex : (a : αˣ × βˣ) → Lex (αˣ × βˣ)) (Units.mk0 m hm, Units.mk0 n hn)) :
      WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ))) :
    WithZero (Lex (Prod.{u_1, u_2} αˣ βˣ)))
Tactic: rw [inl_eq_coe_inlₗ hm, inr_eq_coe_inrₗ hn,
      ← WithZero.coe_mul, OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Range (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : MonoidWithZero A
inst_1 : LinearOrderedCommGroupWithZero B
f : A →*₀ B
x y : ValueGroup₀ f
hxy : x < y
⊢ LT.lt (α := B) ((embedding : (a : ValueGroup₀ f) → B) x : B) ((embedding : (a : ValueGroup₀ f) → B) y : B)
have hxy₁ : LT.lt (α := WithZero Bˣ) ((orderMonoidWithZeroHom f : (a : ValueGroup₀ f) → WithZero Bˣ) x : WithZero Bˣ)
  ((orderMonoidWithZeroHom f : (a : ValueGroup₀ f) → WithZero Bˣ) y : WithZero Bˣ)
Tactic: rw [← monoidWithZeroHom_strictMono.lt_iff_lt] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Range (goal)
Goal:
A : Type u_1
B : Type u_2
inst : MonoidWithZero A
inst_1 : LinearOrderedCommGroupWithZero B
f : A →*₀ B
a : ValueGroup₀ f
ha : 0 < a
b c : ValueGroup₀ f
hbc : b < c
⊢ a * b < a * c
have simp : ∀ (ha : LT.lt (α := B) ((embedding : (a : ValueGroup₀ f) → B) 0 : B) ((embedding : (a : ValueGroup₀ f) → B) a : B))
  (hbc : LT.lt (α := B) ((embedding : (a : ValueGroup₀ f) → B) b : B) ((embedding : (a : ValueGroup₀ f) → B) c : B)),
  HMul.hMul (α := B) (β := B) ((embedding : (a : ValueGroup₀ f) → B) a : B)
      ((embedding : (a : ValueGroup₀ f) → B) b : B) <
    HMul.hMul (α := B) (β := B) ((embedding : (a : ValueGroup₀ f) → B) a : B)
      ((embedding : (a : ValueGroup₀ f) → B) c : B)
Tactic: simp only [← (embedding_strictMono (f := f)).lt_iff_lt, map_mul] at *
Cleared hypotheses: ha, hbc
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Range (goal)
Goal:
A : Type u_1
B : Type u_2
inst : MonoidWithZero A
inst_1 : LinearOrderedCommGroupWithZero B
f : A →*₀ B
a : (ValueGroup₀ f)ˣ
| (0 : B)
have rw : ((embedding : (a : ValueGroup₀ f) → B)
    (((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) 0) :
  B)
Tactic: rw [← map_zero f, ← ValueGroup₀.embedding_restrict₀ (0 : A)]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Range (goal)
Goal:
A : Type u_1
B : Type u_2
inst : MonoidWithZero A
inst_1 : LinearOrderedCommGroupWithZero B
f : A →*₀ B
a : (ValueGroup₀ f)ˣ
⊢ LT.lt (α := B) (0 : B) ((embedding : (a : ValueGroup₀ f) → B) (↑a : ValueGroup₀ f) : B)
have conv_lhs : LT.lt (α := B)
  ((embedding : (a : ValueGroup₀ f) → B)
      (((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) 0) :
    B)
  ((embedding : (a : ValueGroup₀ f) → B) (↑a : ValueGroup₀ f) : B)
Tactic: conv_lhs => rw [← map_zero f, ← ValueGroup₀.embedding_restrict₀ (0 : A)]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Range (goal)
Goal:
A : Type u_1
B : Type u_2
inst : MonoidWithZero A
inst_1 : LinearOrderedCommGroupWithZero B
f : A →*₀ B
a : (ValueGroup₀ f)ˣ
⊢ LT.lt (α := B)
    ((embedding : (a : ValueGroup₀ f) → B)
        (((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) 0) :
      B)
    ((embedding : (a : ValueGroup₀ f) → B) (↑a : ValueGroup₀ f) : B)
have rw : ((restrict₀ f : MonoidWithZeroHom.{u_1, u_2} A (ValueGroup₀ f)) : (a : A) → ValueGroup₀ f) 0 < (↑a : ValueGroup₀ f)
Tactic: rw [embedding_strictMono.lt_iff_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h : CovariantClass α>0 α (fun (x : α>0) (y : α) ↦ (↑x : α) * y) fun (x1 x2 : α) ↦ x1 ≤ x2
a : α
ha : 0 ≤ a
b c : α
hbc : b ≤ c
⊢ a * b ≤ a * c
have inl : ∀ (ha : 0 = a), a * b ≤ a * c
Tactic: obtain ha | ha := ha.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h : CovariantClass α>0 α (fun (x : α>0) (y : α) ↦ (↑x : α) * y) fun (x1 x2 : α) ↦ x1 ≤ x2
a : α
ha : 0 ≤ a
b c : α
hbc : b ≤ c
inl : ∀ (ha : 0 = a), a * b ≤ a * c
⊢ a * b ≤ a * c
have inr : ∀ (ha : 0 < a), a * b ≤ a * c
Tactic: obtain ha | ha := ha.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h : CovariantClass α>0 α (fun (x : α>0) (y : α) ↦ y * (↑x : α)) fun (x1 x2 : α) ↦ x1 ≤ x2
a : α
ha : 0 ≤ a
b c : α
hbc : b ≤ c
⊢ b * a ≤ c * a
have inl : ∀ (ha : 0 = a), b * a ≤ c * a
Tactic: obtain ha | ha := ha.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h : CovariantClass α>0 α (fun (x : α>0) (y : α) ↦ y * (↑x : α)) fun (x1 x2 : α) ↦ x1 ≤ x2
a : α
ha : 0 ≤ a
b c : α
hbc : b ≤ c
inl : ∀ (ha : 0 = a), b * a ≤ c * a
⊢ b * a ≤ c * a
have inr : ∀ (ha : 0 < a), b * a ≤ c * a
Tactic: obtain ha | ha := ha.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h_1 : ContravariantClass α>0 α (fun (x : α>0) (y : α) ↦ (↑x : α) * y) fun (x1 x2 : α) ↦ x1 < x2
a : { x : α // 0 ≤ x }
b c : α
h :
  (fun (x1 x2 : α) ↦ x1 < x2) ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ (↑x : α) * y) a b)
    ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ (↑x : α) * y) a c)
⊢ (fun (x1 x2 : α) ↦ x1 < x2) b c
have inl : ∀ (ha : 0 = (↑a : α)), b < c
Tactic: obtain ha | ha := a.prop.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h_1 : ContravariantClass α>0 α (fun (x : α>0) (y : α) ↦ (↑x : α) * y) fun (x1 x2 : α) ↦ x1 < x2
a : { x : α // 0 ≤ x }
b c : α
h :
  (fun (x1 x2 : α) ↦ x1 < x2) ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ (↑x : α) * y) a b)
    ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ (↑x : α) * y) a c)
inl : ∀ (ha : 0 = (↑a : α)), b < c
⊢ b < c
have inr : ∀ (ha : 0 < (↑a : α)), b < c
Tactic: obtain ha | ha := a.prop.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h_1 : ContravariantClass α>0 α (fun (x : α>0) (y : α) ↦ y * (↑x : α)) fun (x1 x2 : α) ↦ x1 < x2
a : { x : α // 0 ≤ x }
b c : α
h :
  (fun (x1 x2 : α) ↦ x1 < x2) ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ y * (↑x : α)) a b)
    ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ y * (↑x : α)) a c)
⊢ (fun (x1 x2 : α) ↦ x1 < x2) b c
have inl : ∀ (ha : 0 = (↑a : α)), b < c
Tactic: obtain ha | ha := a.prop.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
inst_1 : PartialOrder α
h_1 : ContravariantClass α>0 α (fun (x : α>0) (y : α) ↦ y * (↑x : α)) fun (x1 x2 : α) ↦ x1 < x2
a : { x : α // 0 ≤ x }
b c : α
h :
  (fun (x1 x2 : α) ↦ x1 < x2) ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ y * (↑x : α)) a b)
    ((fun (x : { x : α // 0 ≤ x }) (y : α) ↦ y * (↑x : α)) a c)
inl : ∀ (ha : 0 = (↑a : α)), b < c
⊢ b < c
have inr : ∀ (ha : 0 < (↑a : α)), b < c
Tactic: obtain ha | ha := a.prop.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
⊢ a * c = b * d ↔ a = b ∧ c = d
have refine : ∀ (h : a * c = b * d), a = b ∧ c = d
Tactic: refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
⊢ a = b ∧ c = d
have simp : ¬a < b ∧ ¬c < d
Tactic: simp only [eq_iff_le_not_lt, hab, hcd, true_and]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
⊢ ¬a < b ∧ ¬c < d
have refine_1 : ∀ (hab : a < b), a * c < b * d
Tactic: refine ⟨fun hab ↦ h.not_lt ?_, fun hcd ↦ h.not_lt ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
refine_1 : ∀ (hab : a < b), a * c < b * d
⊢ ¬a < b ∧ ¬c < d
have refine_2 : ∀ (hcd : c < d), a * c < b * d
Tactic: refine ⟨fun hab ↦ h.not_lt ?_, fun hcd ↦ h.not_lt ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
⊢ a * c = b * d ↔ a = b ∧ c = d
have refine : ∀ (h : a * c = b * d), a = b ∧ c = d
Tactic: refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
⊢ a = b ∧ c = d
have simp : ¬a < b ∧ ¬c < d
Tactic: simp only [eq_iff_le_not_lt, hab, hcd, true_and]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
⊢ ¬a < b ∧ ¬c < d
have refine_1 : ∀ (hab : a < b), a * c < b * d
Tactic: refine ⟨fun hab ↦ h.not_lt ?_, fun hcd ↦ h.not_lt ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
refine_1 : ∀ (hab : a < b), a * c < b * d
⊢ ¬a < b ∧ ¬c < d
have refine_2 : ∀ (hcd : c < d), a * c < b * d
Tactic: refine ⟨fun hab ↦ h.not_lt ?_, fun hcd ↦ h.not_lt ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
hab : 0 < a * b
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have inl : ∀ (ha : a < 0), 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
Tactic: rcases lt_trichotomy a 0 with (ha | rfl | ha)
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
hab : 0 < a * b
inl : ∀ (ha : a < 0), 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have inr : ∀ (hab : 0 < 0 * b), LT.lt.{u_1} (α := α) 0 0 ∧ 0 < b ∨ LT.lt.{u_1} (α := α) 0 0 ∧ b < 0
Tactic: rcases lt_trichotomy a 0 with (ha | rfl | ha)
Cleared hypotheses: a, hab
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
hab : 0 < a * b
inl : ∀ (ha : a < 0), 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
inr : ∀ (hab : 0 < 0 * b), LT.lt.{u_1} (α := α) 0 0 ∧ 0 < b ∨ LT.lt.{u_1} (α := α) 0 0 ∧ b < 0
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have inr₁ : ∀ (ha : 0 < a), 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
Tactic: rcases lt_trichotomy a 0 with (ha | rfl | ha)
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
hab : 0 < a * b
ha : a < 0
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have inl : ∀ (hb : 0 ≤ b), a * b ≤ 0
Tactic: refine Or.inr ⟨ha, lt_imp_lt_of_le_imp_le (fun hb => ?_) hab⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (hypothesis)
Goal:
α : Type u_1
inst : MulZeroClass α
b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
hab : 0 < 0 * b
⊢ LT.lt.{u_1} (α := α) 0 0 ∧ 0 < b ∨ LT.lt.{u_1} (α := α) 0 0 ∧ b < 0
have hab₁ : LT.lt.{u_1} (α := α) 0 0
Tactic: rw [zero_mul] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
hab : 0 < a * b
ha : 0 < a
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have inr : ∀ (hb : b ≤ 0), a * b ≤ 0
Tactic: refine Or.inl ⟨ha, lt_imp_lt_of_le_imp_le (fun hb => ?_) hab⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : PosMulMono α
inst_4 : PosMulReflectLE α
a0 : 0 < 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.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
inst_4 : PosMulReflectLT α
a0 : 0 < 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.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : PosMulMono α
inst_4 : PosMulReflectLE α
a0 : 0 < 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.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
inst_4 : PosMulReflectLT α
a0 : 0 < 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.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : MulPosMono α
inst_4 : MulPosReflectLE α
a0 : 0 < a
⊢ 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.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
inst_4 : MulPosReflectLT α
a0 : 0 < a
⊢ 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.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : MulPosMono α
inst_4 : MulPosReflectLE α
b0 : 0 < 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.GroupWithZero.Unbundled.Basic (goal)
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
inst_4 : MulPosReflectLT α
b0 : 0 < b
⊢ a * b < b ↔ a * b < 1 * b
have rw : a * b < b ↔ a * b < b
Tactic: rw [one_mul]