awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
β : Type u_2
inst_4 : Zero β
inst_5 : Mul β
inst_6 : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ 0 < f a
have rwa : f 0 < f a
Tactic: rwa [← zero, lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
ha : 0 < a
⊢ (mulLeft₀ a ha).symm = mulLeft₀ a⁻¹ ⋯
have h : ∀ (x : G₀), Eq (α := G₀) (((mulLeft₀ a ha).symm : (a : G₀) → G₀) x : G₀) ((mulLeft₀ a⁻¹ sorry : (a : G₀) → G₀) x : G₀)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a : G₀
ha : 0 < a
⊢ (mulRight₀ a ha).symm = mulRight₀ a⁻¹ ⋯
have h : ∀ (x : G₀), Eq (α := G₀) (((mulRight₀ a ha).symm : (a : G₀) → G₀) x : G₀) ((mulRight₀ a⁻¹ sorry : (a : G₀) → G₀) x : G₀)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a : G₀
ha : 0 < a
b c : G₀
⊢ LE.le (α := G₀) ((Equiv.divRight₀ a ⋯ : (a : G₀) → G₀) b : G₀) ((Equiv.divRight₀ a ⋯ : (a : G₀) → G₀) c : G₀) ↔ b ≤ c
have simp : b * a⁻¹ ≤ c * a⁻¹ ↔ b ≤ c
Tactic: simp only [Equiv.divRight₀_apply, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeInf G₀
inst_2 : PosMulReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
⊢ c * (a ⊓ b) = c * a ⊓ c * b
have inl : ∀ (hc : LE.le.{u_1} (α := G₀) 0 0), 0 * (a ⊓ b) = 0 * a ⊓ 0 * b
Tactic: obtain (rfl | hc) := hc.eq_or_lt
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeInf G₀
inst_2 : PosMulReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
inl : ∀ (hc : LE.le.{u_1} (α := G₀) 0 0), 0 * (a ⊓ b) = 0 * a ⊓ 0 * b
⊢ c * (a ⊓ b) = c * a ⊓ c * b
have inr : ∀ (hc : 0 < c), c * (a ⊓ b) = c * a ⊓ c * b
Tactic: obtain (rfl | hc) := hc.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
inst_2 : PosMulReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
⊢ c * (a ⊔ b) = c * a ⊔ c * b
have inl : ∀ (hc : LE.le.{u_1} (α := G₀) 0 0), 0 * (a ⊔ b) = 0 * a ⊔ 0 * b
Tactic: obtain (rfl | hc) := hc.eq_or_lt
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
inst_2 : PosMulReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
inl : ∀ (hc : LE.le.{u_1} (α := G₀) 0 0), 0 * (a ⊔ b) = 0 * a ⊔ 0 * b
⊢ c * (a ⊔ b) = c * a ⊔ c * b
have inr : ∀ (hc : 0 < c), c * (a ⊔ b) = c * a ⊔ c * b
Tactic: obtain (rfl | hc) := hc.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeInf G₀
inst_2 : MulPosReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
⊢ (a ⊓ b) * c = a * c ⊓ b * c
have inl : ∀ (hc : LE.le.{u_1} (α := G₀) 0 0), (a ⊓ b) * 0 = a * 0 ⊓ b * 0
Tactic: obtain (rfl | hc) := hc.eq_or_lt
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeInf G₀
inst_2 : MulPosReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
inl : ∀ (hc : LE.le.{u_1} (α := G₀) 0 0), (a ⊓ b) * 0 = a * 0 ⊓ b * 0
⊢ (a ⊓ b) * c = a * c ⊓ b * c
have inr : ∀ (hc : 0 < c), (a ⊓ b) * c = a * c ⊓ b * c
Tactic: obtain (rfl | hc) := hc.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
inst_2 : MulPosReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
⊢ (a ⊔ b) * c = a * c ⊔ b * c
have inl : ∀ (hc : LE.le.{u_1} (α := G₀) 0 0), (a ⊔ b) * 0 = a * 0 ⊔ b * 0
Tactic: obtain (rfl | hc) := hc.eq_or_lt
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso (goal)
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : SemilatticeSup G₀
inst_2 : MulPosReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
inl : ∀ (hc : LE.le.{u_1} (α := G₀) 0 0), (a ⊔ b) * 0 = a * 0 ⊔ b * 0
⊢ (a ⊔ b) * c = a * c ⊔ b * c
have inr : ∀ (hc : 0 < c), (a ⊔ b) * c = a * c ⊔ b * c
Tactic: obtain (rfl | hc) := hc.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
x : α
hx : 0 < (↑x : WithZero α)
a b : α
h : (↑a : WithZero α) < (↑b : WithZero α)
⊢ (↑x : WithZero α) * (↑a : WithZero α) < (↑x : WithZero α) * (↑b : WithZero α)
have norm_cast : ∀ (h : a < b), x * a < x * b
Tactic: norm_cast at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulRightStrictMono α
x : α
hx : 0 < (↑x : WithZero α)
a b : α
h : (↑a : WithZero α) < (↑b : WithZero α)
⊢ (↑a : WithZero α) * (↑x : WithZero α) < (↑b : WithZero α) * (↑x : WithZero α)
have norm_cast : ∀ (h : a < b), a * x < b * x
Tactic: norm_cast at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
x : α
hx : 0 ≤ (↑x : WithZero α)
a b : α
h : (↑a : WithZero α) ≤ (↑b : WithZero α)
⊢ (↑x : WithZero α) * (↑a : WithZero α) ≤ (↑x : WithZero α) * (↑b : WithZero α)
have norm_cast : ∀ (h : a ≤ b), x * a ≤ x * b
Tactic: norm_cast at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulRightMono α
x : α
hx : 0 ≤ (↑x : WithZero α)
a b : α
h : (↑a : WithZero α) ≤ (↑b : WithZero α)
⊢ (↑a : WithZero α) * (↑x : WithZero α) ≤ (↑b : WithZero α) * (↑x : WithZero α)
have norm_cast : ∀ (h : a ≤ b), a * x ≤ b * x
Tactic: norm_cast at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
a b : WithZero αˣ
⊢ a < b →
    LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) a : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) b : α)
have zero : 0 < b →
  LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)
    ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) b : α)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
a b : WithZero αˣ
zero :
  0 < b →
    LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) b : α)
⊢ a < b →
    LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) a : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) b : α)
have coe : ∀ (a : αˣ),
  (↑a : WithZero αˣ) < b →
    LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) (↑a : WithZero αˣ) : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) b : α)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
b : WithZero αˣ
⊢ 0 < b →
    LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) b : α)
have zero : LT.lt.{u_1} (α := WithZero αˣ) 0 0 →
  LT.lt.{u_1} (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)
    ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
b : WithZero αˣ
zero :
  LT.lt.{u_1} (α := WithZero αˣ) 0 0 →
    LT.lt.{u_1} (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)
⊢ 0 < b →
    LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) b : α)
have zero₁ : ∀ (a : αˣ),
  0 < (↑a : WithZero αˣ) →
    LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) (↑a : WithZero αˣ) : α)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
b : WithZero αˣ
a : αˣ
⊢ (↑a : WithZero αˣ) < b →
    LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) (↑a : WithZero αˣ) : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) b : α)
have coe : (↑a : WithZero αˣ) < 0 →
  LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) (↑a : WithZero αˣ) : α)
    ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.GroupWithZero.WithZero (goal)
Goal:
α : Type u_1
inst : LinearOrderedCommGroupWithZero α
b : WithZero αˣ
a : αˣ
coe :
  (↑a : WithZero αˣ) < 0 →
    LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) (↑a : WithZero αˣ) : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) 0 : α)
⊢ (↑a : WithZero αˣ) < b →
    LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) (↑a : WithZero αˣ) : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) b : α)
have coe₁ : ∀ (a_1 : αˣ),
  (↑a : WithZero αˣ) < (↑a_1 : WithZero αˣ) →
    LT.lt (α := α) ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) (↑a : WithZero αˣ) : α)
      ((withZeroUnitsEquiv : (a : WithZero αˣ) → α) (↑a_1 : WithZero αˣ) : α)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Basic (goal)
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : Group α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : GroupSeminormClass F α β
f : F
x y : α
⊢ (f : (a : α) → β) (x / y) ≤ HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)
have rw : (f : (a : α) → β) (x * y⁻¹) ≤ HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y⁻¹ : β)
Tactic: rw [div_eq_mul_inv, ← map_inv_eq_map f y]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Basic (goal)
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : Group α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : GroupSeminormClass F α β
f : F
x y : α
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (x / y) : β) ((f : (a : α) → β) (y / x) : β)
have rw : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (y / x)⁻¹ : β) ((f : (a : α) → β) (y / x) : β)
Tactic: rw [← inv_div, map_inv_eq_map]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Basic (goal)
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : Group α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : GroupSeminormClass F α β
f : F
x y : α
rw : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (y / x)⁻¹ : β) ((f : (a : α) → β) (y / x) : β)
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (x / y) : β) ((f : (a : α) → β) (y / x) : β)
have rw₁ : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (y / x) : β) ((f : (a : α) → β) (y / x) : β)
Tactic: rw [← inv_div, map_inv_eq_map]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Basic (goal)
Goal:
F : Type u_2
β : Type u_4
inst : AddCommMonoid β
inst_1 : PartialOrder β
f : F
α : Type u_7
inst_2 : FunLike F α β
inst_3 : CommGroup α
inst_4 : GroupSeminormClass F α β
x y : α
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (x⁻¹ * y) : β) ((f : (a : α) → β) (x * y⁻¹) : β)
have rw : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (x⁻¹ * y)⁻¹ : β) ((f : (a : α) → β) (x * y⁻¹) : β)
Tactic: rw [← map_inv_eq_map, inv_mul', inv_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Basic (goal)
Goal:
F : Type u_2
β : Type u_4
inst : AddCommMonoid β
inst_1 : PartialOrder β
f : F
α : Type u_7
inst_2 : FunLike F α β
inst_3 : CommGroup α
inst_4 : GroupSeminormClass F α β
x y : α
rw : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (x⁻¹ * y)⁻¹ : β) ((f : (a : α) → β) (x * y⁻¹) : β)
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (x⁻¹ * y) : β) ((f : (a : α) → β) (x * y⁻¹) : β)
have rw₁ : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (x⁻¹⁻¹ / y) : β) ((f : (a : α) → β) (x * y⁻¹) : β)
Tactic: rw [← map_inv_eq_map, inv_mul', inv_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Basic (goal)
Goal:
F : Type u_2
β : Type u_4
inst : AddCommMonoid β
inst_1 : PartialOrder β
f : F
α : Type u_7
inst_2 : FunLike F α β
inst_3 : CommGroup α
inst_4 : GroupSeminormClass F α β
x y : α
rw : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (x⁻¹ * y)⁻¹ : β) ((f : (a : α) → β) (x * y⁻¹) : β)
rw₁ : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (x⁻¹⁻¹ / y) : β) ((f : (a : α) → β) (x * y⁻¹) : β)
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (x⁻¹ * y) : β) ((f : (a : α) → β) (x * y⁻¹) : β)
have rw₂ : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (x / y) : β) ((f : (a : α) → β) (x * y⁻¹) : β)
Tactic: rw [← map_inv_eq_map, inv_mul', inv_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Basic (goal)
Goal:
F : Type u_2
β : Type u_4
inst : AddCommMonoid β
inst_1 : PartialOrder β
f : F
α : Type u_7
inst_2 : FunLike F α β
inst_3 : CommGroup α
inst_4 : GroupSeminormClass F α β
x y : α
rw : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (x⁻¹ * y)⁻¹ : β) ((f : (a : α) → β) (x * y⁻¹) : β)
rw₁ : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (x⁻¹⁻¹ / y) : β) ((f : (a : α) → β) (x * y⁻¹) : β)
rw₂ : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (x / y) : β) ((f : (a : α) → β) (x * y⁻¹) : β)
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (x⁻¹ * y) : β) ((f : (a : α) → β) (x * y⁻¹) : β)
have rw₃ : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (x * y⁻¹) : β) ((f : (a : α) → β) (x * y⁻¹) : β)
Tactic: rw [← map_inv_eq_map, inv_mul', inv_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Basic (goal)
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : Group α
inst_2 : AddCommGroup β
inst_3 : LinearOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : GroupSeminormClass F α β
f : F
x y : α
⊢ |HSub.hSub (α := β) (β := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)| ≤ (f : (a : α) → β) (x / y)
have rw : (f : (a : α) → β) x ≤ HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) y : β) ((f : (a : α) → β) (x / y) : β) ∧
  (f : (a : α) → β) y ≤ HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) (x / y) : β)
Tactic: rw [abs_sub_le_iff, sub_le_iff_le_add', sub_le_iff_le_add']
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Basic (goal)
Goal:
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst : FunLike F α β
inst_1 : Group α
inst_2 : AddCommMonoid β
inst_3 : LinearOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : GroupSeminormClass F α β
f : F
a : α
⊢ 0 ≤ HSMul.hSMul (α := ℕ) (β := β) 2 ((f : (a : α) → β) a : β)
have rw : (f : (a : α) → β) (a / a) ≤ HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a : β)
Tactic: rw [two_nsmul, ← map_one_eq_zero f, ← div_self' a]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Group α
inst_1 : Monoid β
F : Type u_6
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
inst_4 : LE β
inst_5 : MulRightMono β
inst_6 : MulLeftMono β
f g : F
x : α
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) x⁻¹ : β) ((g : (a : α) → β) x⁻¹ : β) ↔
    LE.le.{u_3} (α := β) ((g : (a : α) → β) x : β) ((f : (a : α) → β) x : β)
have suffices : ∀ (f g : F) (x : α),
  LE.le.{u_3} (α := β) ((f : (a : α) → β) x⁻¹ : β) ((g : (a : α) → β) x⁻¹ : β) →
    LE.le.{u_3} (α := β) ((g : (a : α) → β) x : β) ((f : (a : α) → β) x : β)
Tactic: suffices h : ∀ (f g : F) (x), f x⁻¹ ≤ g x⁻¹ → g x ≤ f x from
    ⟨h f g x, by simpa using h g f x⁻¹⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : Preorder α
inst_2 : Zero α
inst_3 : Preorder β
inst_4 : Zero β
inst_5 : OrderHomClass F α β
inst_6 : ZeroHomClass F α β
f : F
a : α
ha : 0 ≤ a
⊢ LE.le.{u_3} (α := β) (0 : β) ((f : (a : α) → β) a : β)
have rw : LE.le.{u_3} (α := β) ((f : (a : α) → β) 0 : β) ((f : (a : α) → β) a : β)
Tactic: rw [← map_zero f]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : Preorder α
inst_2 : Zero α
inst_3 : Preorder β
inst_4 : Zero β
inst_5 : OrderHomClass F α β
inst_6 : ZeroHomClass F α β
f : F
a : α
ha : a ≤ 0
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) a : β) (0 : β)
have rw : LE.le.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) 0 : β)
Tactic: rw [← map_zero f]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : Monotone.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)
a : α
⊢ 0 ≤ a → LE.le.{u_3} (α := β) (0 : β) ((f : (a : α) → β) a : β)
have rw : 0 ≤ a → LE.le.{u_3} (α := β) ((f : (a : α) → β) 0 : β) ((f : (a : α) → β) a : β)
Tactic: rw [← map_zero f]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : ∀ (a : α), 0 ≤ a → LE.le.{u_3} (α := β) (0 : β) ((f : (a : α) → β) a : β)
a b : α
hl : a ≤ b
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
have rw : (f : (a : α) → β) a ≤ HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) (b - a) : β) ((f : (a : α) → β) a : β)
Tactic: rw [← sub_add_cancel b a, map_add f]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
⊢ StrictMono.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β) ↔
    ∀ (a : α), 0 < a → LT.lt.{u_3} (α := β) (0 : β) ((f : (a : α) → β) a : β)
have refine_1 : ∀ (h : StrictMono.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)) (a : α),
  0 < a → LT.lt.{u_3} (α := β) (0 : β) ((f : (a : α) → β) a : β)
Tactic: refine ⟨fun h a => ?_, fun h a b hl => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
refine_1 :
  ∀ (h : StrictMono.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)) (a : α),
    0 < a → LT.lt.{u_3} (α := β) (0 : β) ((f : (a : α) → β) a : β)
⊢ StrictMono.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β) ↔
    ∀ (a : α), 0 < a → LT.lt.{u_3} (α := β) (0 : β) ((f : (a : α) → β) a : β)
have refine_2 : ∀ (h : ∀ (a : α), 0 < a → LT.lt.{u_3} (α := β) (0 : β) ((f : (a : α) → β) a : β)) (a b : α) (hl : a < b),
  LT.lt.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
Tactic: refine ⟨fun h a => ?_, fun h a b hl => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : StrictMono.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)
a : α
⊢ 0 < a → LT.lt.{u_3} (α := β) (0 : β) ((f : (a : α) → β) a : β)
have refine_1 : 0 < a → LT.lt.{u_3} (α := β) ((f : (a : α) → β) 0 : β) ((f : (a : α) → β) a : β)
Tactic: rw [← map_zero f]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : ∀ (a : α), 0 < a → LT.lt.{u_3} (α := β) (0 : β) ((f : (a : α) → β) a : β)
a b : α
hl : a < b
⊢ LT.lt.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
have refine_2 : (f : (a : α) → β) a < HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) (b - a) : β) ((f : (a : α) → β) a : β)
Tactic: rw [← sub_add_cancel b a, map_add f]
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.Monoid (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
inst_4 : MulOneClass α
inst_5 : MulOneClass β
inst_6 : MulOneClass γ
inst_7 : MulOneClass δ
f_1 g_1 f g : α →*o β
h :
  Eq (α := (a : α) → β) ((fun (f : α →*o β) ↦ (↑f.toMonoidHom : OneHom α β).toFun) f)
    ((fun (f : α →*o β) ↦ (↑f.toMonoidHom : OneHom α β).toFun) g)
⊢ f = g
have obtain : ∀ (toFun : α → β) (map_one' : toFun 1 = 1)
  (map_mul' :
    ∀ (x y : α),
      { toFun := toFun, map_one' := map_one' : OneHom α β }.toFun (x * y) =
        { toFun := toFun, map_one' := map_one' : OneHom α β }.toFun x *
          { toFun := toFun, map_one' := map_one' : OneHom α β }.toFun y)
  (monotone' : Monotone (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : α →* β } : OneHom α β).toFun)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : α →*o β) ↦ (↑f.toMonoidHom : OneHom α β).toFun)
        { toFun := toFun, map_one' := map_one', map_mul' := map_mul', monotone' := monotone' })
      ((fun (f : α →*o β) ↦ (↑f.toMonoidHom : OneHom α β).toFun) g)),
  { toFun := toFun, map_one' := map_one', map_mul' := map_mul', monotone' := monotone' : α →*o β } = g
Tactic: obtain ⟨⟨⟨_, _⟩⟩, _⟩ := f
Cleared hypotheses: f, h