awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Hom.Basic
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⁻¹) : β)
rw₃ 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⁻¹) : β)

Tactic:
rw [← map_inv_eq_map, inv_mul', inv_inv, div_eq_mul_inv]

Premises used: inv_mul', div_eq_mul_inv, GroupSeminormClass.map_inv_eq_map, inv_inv
-- Module: Mathlib.Algebra.Order.Hom.Basic
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 ≤ HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) y : β) ((f : (a : α) → β) (y / x) : β)

Tactic:
simpa only [add_comm, map_div_rev, div_mul_cancel] using map_mul_le_add f (x / y) y

Premises used: HDiv.hDiv, add_comm, MulLEAddHomClass.map_mul_le_add, map_div_rev, div_mul_cancel
-- Module: Mathlib.Algebra.Order.Hom.Basic
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 : α
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) : β)
⊢ |HSub.hSub (α := β) (β := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)| ≤ (f : (a : α) → β) (x / y)

Tactic:
rw [abs_sub_le_iff, sub_le_iff_le_add', sub_le_iff_le_add']

Premises used: abs_sub_le_iff, sub_le_iff_le_add'
-- Module: Mathlib.Algebra.Order.Hom.Basic
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 : α
⊢ (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:
⟨le_map_add_map_div _ _ _, le_map_add_map_div' _ _ _⟩

Premises used: le_map_add_map_div', And.intro, le_map_add_map_div
-- Module: Mathlib.Algebra.Order.Hom.Basic
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 : α
⊢ (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:
exact ⟨le_map_add_map_div _ _ _, le_map_add_map_div' _ _ _⟩
-- Module: Mathlib.Algebra.Order.Hom.Basic
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 : α
rw : (f : (a : α) → β) (a / a) ≤ HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a : β)
⊢ 0 ≤ HSMul.hSMul (α := ℕ) (β := β) 2 ((f : (a : α) → β) a : β)

Tactic:
rw [two_nsmul, ← map_one_eq_zero f, ← div_self' a]

Premises used: GroupSeminormClass.map_one_eq_zero, div_self', two_nsmul
-- Module: Mathlib.Algebra.Order.Hom.Basic
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 : α
⊢ (f : (a : α) → β) (a / a) ≤ HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a : β)

Tactic:
map_div_le_add _ _ _

Premises used: map_div_le_add
-- Module: Mathlib.Algebra.Order.Hom.Basic
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 : α
⊢ (f : (a : α) → β) (a / a) ≤ HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a : β)

Tactic:
exact map_div_le_add _ _ _

Premises used: map_div_le_add
-- Module: Mathlib.Algebra.Order.Hom.Basic
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 : GroupNormClass F α β
f : F
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) 1 : β) (0 : β)

Tactic:
map_one_eq_zero _

Premises used: GroupSeminormClass.map_one_eq_zero
-- Module: Mathlib.Algebra.Order.Hom.Basic
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 : GroupNormClass F α β
f : F
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) 1 : β) (0 : β)

Tactic:
exact map_one_eq_zero _

Premises used: GroupSeminormClass.map_one_eq_zero
-- Module: Mathlib.Algebra.Order.Hom.Basic
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 : GroupNormClass F α β
f : F
x : α
⊢ Ne.{u_4 + 1} (α := β) ((f : (a : α) → β) x : β) (0 : β) ↔ x ≠ 1

Tactic:
(map_eq_zero_iff_eq_one _).not

Premises used: map_eq_zero_iff_eq_one, Iff.not
-- Module: Mathlib.Algebra.Order.Hom.Basic
Goal:
F : Type u_2
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : Group α
inst_2 : AddCommMonoid β
inst_3 : LinearOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : GroupNormClass F α β
f : F
x : α
hx : x ≠ 1
⊢ LT.lt.{u_4} (α := β) (0 : β) ((f : (a : α) → β) x : β)

Tactic:
(apply_nonneg _ _).lt_of_ne <| ((map_ne_zero_iff_ne_one _).2 hx).symm

Premises used: Iff.mpr, map_ne_zero_iff_ne_one, Ne.symm, LE.le.lt_of_ne, NonnegHomClass.apply_nonneg
-- Module: Mathlib.Algebra.Order.Hom.Basic
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 : NonUnitalNonAssocRing α
inst_2 : Semiring β
inst_3 : LinearOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : RingSeminormClass F α β
⊢ NonnegHomClass F α β

Tactic:
AddGroupSeminormClass.toNonnegHomClass

Premises used: AddGroupSeminormClass.toNonnegHomClass
-- Module: Mathlib.Algebra.Order.Hom.Basic
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 : NonAssocRing α
inst_2 : Semiring β
inst_3 : PartialOrder β
inst_4 : MulRingSeminormClass F α β
⊢ RingSeminormClass F α β

Tactic:
{ ‹MulRingSeminormClass F α β› with map_mul_le_mul := fun _ _ _ => (map_mul _ _ _).le }

Premises used: RingSeminormClass.mk
-- Module: Mathlib.Algebra.Order.Hom.Basic
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 : NonAssocRing α
inst_2 : Semiring β
inst_3 : PartialOrder β
inst_4 : MulRingNormClass F α β
⊢ RingNormClass F α β

Tactic:
{ ‹MulRingNormClass F α β›, MulRingSeminormClass.toRingSeminormClass with }

Premises used: RingNormClass.mk, MulRingNormClass.eq_zero_of_map_eq_zero, MulRingSeminormClass.toRingSeminormClass
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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 : α
h :
  ∀ (f g : F) (x : α),
    LE.le.{u_3} (α := β) ((f : (a : α) → β) x⁻¹ : β) ((g : (a : α) → β) x⁻¹ : β) →
      LE.le.{u_3} (α := β) ((g : (a : α) → β) x : β) ((f : (a : α) → β) x : β)
⊢ LE.le.{u_3} (α := β) ((g : (a : α) → β) x : β) ((f : (a : α) → β) x : β) →
    LE.le.{u_3} (α := β) ((f : (a : α) → β) x⁻¹ : β) ((g : (a : α) → β) x⁻¹ : β)

Tactic:
simpa using h g f x⁻¹

Premises used: Inv.inv
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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 : α
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 : β)
⊢ 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⁻¹⟩
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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_1 g_1 : F
x_1 : α
f g : F
x : α
hfg : LE.le.{u_3} (α := β) ((f : (a : α) → β) x⁻¹ : β) ((g : (a : α) → β) x⁻¹ : β)
⊢ (g : (a : α) → β) x =
    HMul.hMul (α := β) ((f : (a : α) → β) x : β)
      (HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x⁻¹ : β) ((g : (a : α) → β) x : β))

Tactic:
simp [← mul_assoc, ← map_mul]

Premises used: mul_assoc, map_mul
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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_1 g_1 : F
x_1 : α
f g : F
x : α
hfg : LE.le.{u_3} (α := β) ((f : (a : α) → β) x⁻¹ : β) ((g : (a : α) → β) x⁻¹ : β)
⊢ HMul.hMul (α := β) ((f : (a : α) → β) x : β)
      (HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x⁻¹ : β) ((g : (a : α) → β) x : β)) ≤
    HMul.hMul (α := β) ((f : (a : α) → β) x : β)
      (HMul.hMul (α := β) (β := β) ((g : (a : α) → β) x⁻¹ : β) ((g : (a : α) → β) x : β))

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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_1 g_1 : F
x_1 : α
f g : F
x : α
hfg : LE.le.{u_3} (α := β) ((f : (a : α) → β) x⁻¹ : β) ((g : (a : α) → β) x⁻¹ : β)
⊢ HMul.hMul (α := β) ((f : (a : α) → β) x : β)
      (HMul.hMul (α := β) (β := β) ((g : (a : α) → β) x⁻¹ : β) ((g : (a : α) → β) x : β)) =
    (f : (a : α) → β) x

Tactic:
simp [← map_mul]

Premises used: map_mul
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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 : α
⊢ ∀ (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:
exact fun f g x hfg ↦ calc
    _ = f x * (f x⁻¹ * g x) := by simp [← mul_assoc, ← map_mul]
    _ ≤ f x * (g x⁻¹ * g x) := by gcongr
    _ = f x                 := by simp [← map_mul]

Premises used: Trans.trans
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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 : PartialOrder β
inst_5 : MulRightMono β
inst_6 : MulLeftMono β
f g : F
⊢ f = g → ∀ (x : α), LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
simp +contextual
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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
rw : LE.le.{u_3} (α := β) ((f : (a : α) → β) 0 : β) ((f : (a : α) → β) a : β)
⊢ LE.le.{u_3} (α := β) (0 : β) ((f : (a : α) → β) a : β)

Tactic:
rw [← map_zero f]

Premises used: map_zero
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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} (α := β) ((f : (a : α) → β) 0 : β) ((f : (a : α) → β) a : β)

Tactic:
OrderHomClass.mono _ ha

Premises used: OrderHomClass.mono
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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} (α := β) ((f : (a : α) → β) 0 : β) ((f : (a : α) → β) a : β)

Tactic:
exact OrderHomClass.mono _ ha

Premises used: OrderHomClass.mono
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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
rw : LE.le.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) 0 : β)
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) a : β) (0 : β)

Tactic:
rw [← map_zero f]

Premises used: map_zero
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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 : β) ((f : (a : α) → β) 0 : β)

Tactic:
OrderHomClass.mono _ ha

Premises used: OrderHomClass.mono
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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 : β) ((f : (a : α) → β) 0 : β)

Tactic:
exact OrderHomClass.mono _ ha

Premises used: OrderHomClass.mono
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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 : α
rw : 0 ≤ a → LE.le.{u_3} (α := β) ((f : (a : α) → β) 0 : β) ((f : (a : α) → β) a : β)
⊢ 0 ≤ a → LE.le.{u_3} (α := β) (0 : β) ((f : (a : α) → β) a : β)

Tactic:
rw [← map_zero f]

Premises used: map_zero
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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} (α := β) ((f : (a : α) → β) 0 : β) ((f : (a : α) → β) a : β)

Tactic:
apply h
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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
rw : (f : (a : α) → β) a ≤ HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) (b - a) : β) ((f : (a : α) → β) a : β)
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)

Tactic:
rw [← sub_add_cancel b a, map_add f]

Premises used: map_add, sub_add_cancel
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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
⊢ (f : (a : α) → β) a ≤ HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) (b - a) : β) ((f : (a : α) → β) a : β)

Tactic:
le_add_of_nonneg_left (h _ <| sub_nonneg.2 hl)

Premises used: Iff.mpr, sub_nonneg, le_add_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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
⊢ (f : (a : α) → β) a ≤ HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) (b - a) : β) ((f : (a : α) → β) a : β)

Tactic:
exact le_add_of_nonneg_left (h _ <| sub_nonneg.2 hl)

Premises used: Iff.mpr, sub_nonneg, le_add_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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 α β
⊢ Antitone.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β) ↔
    ∀ (a : α), 0 ≤ a → LE.le.{u_3} (α := β) ((f : (a : α) → β) a : β) (0 : β)

Tactic:
monotone_toDual_comp_iff.symm.trans <| monotone_iff_map_nonneg (β := βᵒᵈ) (iamhc := iamhc) _

Premises used: monotone_iff_map_nonneg, monotone_toDual_comp_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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 α β
⊢ Monotone.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β) ↔
    ∀ (a : α), a ≤ 0 → LE.le.{u_3} (α := β) ((f : (a : α) → β) a : β) (0 : β)

Tactic:
antitone_comp_ofDual_iff.symm.trans <| antitone_iff_map_nonpos (α := αᵒᵈ) (iamhc := iamhc) _

Premises used: antitone_iff_map_nonpos, Iff.trans, antitone_comp_ofDual_iff, Iff.symm
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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 α β
⊢ Antitone.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β) ↔
    ∀ (a : α), a ≤ 0 → LE.le.{u_3} (α := β) (0 : β) ((f : (a : α) → β) a : β)

Tactic:
monotone_comp_ofDual_iff.symm.trans <| monotone_iff_map_nonneg (α := αᵒᵈ) (iamhc := iamhc) _

Premises used: monotone_iff_map_nonneg, Iff.trans, monotone_comp_ofDual_iff, Iff.symm
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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 : β)

Tactic:
⟨fun h a => ?_, fun h a b hl => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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 : β)
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 : β)
⊢ 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 => ?_⟩
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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 : α
refine_1 : 0 < a → LT.lt.{u_3} (α := β) ((f : (a : α) → β) 0 : β) ((f : (a : α) → β) a : β)
⊢ 0 < a → LT.lt.{u_3} (α := β) (0 : β) ((f : (a : α) → β) a : β)

Tactic:
rw [← map_zero f]

Premises used: map_zero
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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} (α := β) ((f : (a : α) → β) 0 : β) ((f : (a : α) → β) a : β)

Tactic:
apply h
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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
refine_2 : (f : (a : α) → β) a < HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) (b - a) : β) ((f : (a : α) → β) a : β)
⊢ LT.lt.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)

Tactic:
rw [← sub_add_cancel b a, map_add f]

Premises used: map_add, sub_add_cancel
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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
⊢ (f : (a : α) → β) a < HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) (b - a) : β) ((f : (a : α) → β) a : β)

Tactic:
lt_add_of_pos_left _ (h _ <| sub_pos.2 hl)

Premises used: Iff.mpr, sub_pos, lt_add_of_pos_left
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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
⊢ (f : (a : α) → β) a < HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) (b - a) : β) ((f : (a : α) → β) a : β)

Tactic:
exact lt_add_of_pos_left _ (h _ <| sub_pos.2 hl)

Premises used: Iff.mpr, sub_pos, lt_add_of_pos_left
-- Module: Mathlib.Algebra.Order.Hom.Monoid
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 α β
⊢ StrictAnti.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β) ↔
    ∀ (a : α), 0 < a → LT.lt.{u_3} (α := β) ((f : (a : α) → β) a : β) (0 : β)

Tactic:
strictMono_toDual_comp_iff.symm.trans <| strictMono_iff_map_pos (β := βᵒᵈ) (iamhc := iamhc) _

Premises used: strictMono_iff_map_pos, Iff.trans, strictMono_toDual_comp_iff, Iff.symm