awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
a b : G
hab : 0 ≤ b
this : LE.le (α := ℤ) (0 : ℤ) ((addMonoidHom G : (a : G) → ℤ) b : ℤ)
⊢ ZeroHom.toFun (↑(addMonoidHom G) : ZeroHom G ℤ) a ≤
    ZeroHom.toFun (↑(addMonoidHom G) : ZeroHom G ℤ) ((fun (x : G) ↦ a + x) b)

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
a b : G
hab : 0 ≤ b
suffices : LE.le (α := ℤ) (0 : ℤ) ((addMonoidHom G : (a : G) → ℤ) b : ℤ)
⊢ ZeroHom.toFun (↑(addMonoidHom G) : ZeroHom G ℤ) a ≤
    ZeroHom.toFun (↑(addMonoidHom G) : ZeroHom G ℤ) ((fun (x : G) ↦ a + x) b)

Tactic:
suffices 0 ≤ addMonoidHom G b by simpa
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
a b : G
hab : 0 ≤ b
⊢ LE.le (α := ℤ) (0 : ℤ) ((addMonoidHom G : (a : G) → ℤ) b : ℤ)

Tactic:
simp [addMonoidHom, hab]

Premises used: LocallyFiniteOrder.addMonoidHom
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
⊢ Eq (α := G →+ ℤ) (↑(orderAddMonoidHom G) : G →+ ℤ) (addMonoidHom G)

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, LocallyFiniteOrder.addMonoidHom, rfl
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
x : G
⊢ Eq (α := ℤ) ((orderAddMonoidHom G : (a : G) → ℤ) x : ℤ) ((addMonoidHom G : (a : G) → ℤ) x : ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
rw : ∀ (a : G), 0 < a → LT.lt (α := ℤ) (0 : ℤ) ((orderAddMonoidHom G : (a : G) → ℤ) a : ℤ)
⊢ StrictMono (α := G) (β := ℤ) (⇑(orderAddMonoidHom G) : (a : G) → ℤ)

Tactic:
rw [strictMono_iff_map_pos]

Premises used: strictMono_iff_map_pos
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
g : G
H : 0 < g
⊢ LT.lt (α := ℤ) (0 : ℤ) ((orderAddMonoidHom G : (a : G) → ℤ) g : ℤ)

Tactic:
simpa [addMonoidHom, H.le]

Premises used: LT.lt.le, LocallyFiniteOrder.addMonoidHom
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
inst_4 : Nontrivial G
⊢ Function.Bijective (α := G) (β := ℤ) (⇑(orderAddMonoidHom G) : (a : G) → ℤ)

Tactic:
⟨orderAddMonoidHom_strictMono.injective, ?_⟩

Premises used: LocallyFiniteOrder.orderAddMonoidHom_strictMono, StrictMono.injective, And.intro, Function.Bijective
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
inst_4 : Nontrivial G
refine : Function.Surjective (α := G) (β := ℤ) (⇑(orderAddMonoidHom G) : (a : G) → ℤ)
⊢ Function.Bijective (α := G) (β := ℤ) (⇑(orderAddMonoidHom G) : (a : G) → ℤ)

Tactic:
refine ⟨orderAddMonoidHom_strictMono.injective, ?_⟩
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
inst_4 : Nontrivial G
this : 1 ∈ AddMonoidHom.range (OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G))
obtain :
  ∀ (x : G) (hx : Eq (α := ℤ) ((OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G) : (a : G) → ℤ) x : ℤ) (1 : ℤ)),
    Function.Surjective (α := G) (β := ℤ) (⇑(orderAddMonoidHom G) : (a : G) → ℤ)
⊢ Function.Surjective (α := G) (β := ℤ) (⇑(orderAddMonoidHom G) : (a : G) → ℤ)

Tactic:
obtain ⟨x, hx⟩ := this
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
inst_4 : Nontrivial G
x : G
hx : Eq (α := ℤ) ((OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G) : (a : G) → ℤ) x : ℤ) (1 : ℤ)
a : ℤ
⊢ (orderAddMonoidHom G : (a : G) → ℤ) (a • x) = a

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
inst_4 : Nontrivial G
x : G
hx : Eq (α := ℤ) ((OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G) : (a : G) → ℤ) x : ℤ) (1 : ℤ)
⊢ Function.Surjective (α := G) (β := ℤ) (⇑(orderAddMonoidHom G) : (a : G) → ℤ)

Tactic:
exact fun a ↦ ⟨a • x, by simp_all⟩
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
inst_4 : Nontrivial G
suffices : 1 ∈ AddMonoidHom.range (OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G))
⊢ Function.Surjective (α := G) (β := ℤ) (⇑(orderAddMonoidHom G) : (a : G) → ℤ)

Tactic:
suffices 1 ∈ (orderAddMonoidHom G).range by
    obtain ⟨x, hx⟩ := this
    exact fun a ↦ ⟨a • x, by simp_all⟩
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
inst_4 : Nontrivial G
have : ∀ (a : G) (ha : 0 < a), 1 ∈ AddMonoidHom.range (OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G))
⊢ 1 ∈ AddMonoidHom.range (OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G))

Tactic:
have ⟨a, ha⟩ := exists_zero_lt (α := G)
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
⊢ 0 ∈ Icc 0 a

Tactic:
simpa using ha.le

Premises used: LT.lt.le
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
H : IsMax (α := ↥(Icc 0 a)) (Subtype.mk (p := fun (x : G) ↦ x ∈ Icc 0 a) 0 ⋯)
⊢ a ∈ Icc 0 a

Tactic:
simpa using ha.le

Premises used: LT.lt.le
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
obtain :
  ∀ (b : ↥(Icc 0 a)) (hb : Subtype.mk (p := fun (x : G) ↦ x ∈ Icc 0 a) 0 ⋯ ⋖ b),
    1 ∈ AddMonoidHom.range (OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G))
⊢ 1 ∈ AddMonoidHom.range (OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G))

Tactic:
obtain ⟨b, hb⟩ := exists_covBy_of_wellFoundedLT (α := Icc 0 a) (a := ⟨0, by simpa using ha.le⟩)
    (fun H ↦ ha.not_ge (@H ⟨a, by simpa using ha.le⟩ ha.le))

Premises used: LT.lt.le, LT.lt.not_ge, exists_covBy_of_wellFoundedLT
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
h : Eq (α := ℤ) ((OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G) : (a : G) → ℤ) (↑b : G) : ℤ) (1 : ℤ)
⊢ 1 ∈ AddMonoidHom.range (OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G))

Tactic:
use b.1

Premises used: Subtype.val
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
⊢ 0 ≤ (↑b : G)

Tactic:
have : 0 ≤ b.1 := hb.1.le
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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)
this : Ico 0 (↑b : G) = {0}
⊢ Eq (α := ℤ) ((OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G) : (a : G) → ℤ) (↑b : G) : ℤ) (1 : ℤ)

Tactic:
simpa [orderAddMonoidHom, addMonoidHom, this]

Premises used: LocallyFiniteOrder.orderAddMonoidHom, LocallyFiniteOrder.addMonoidHom
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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)
h : Ico 0 (↑b : G) = {0}
⊢ Eq (α := ℤ) ((OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G) : (a : G) → ℤ) (↑b : G) : ℤ) (1 : ℤ)

Tactic:
suffices Ico 0 b.1 = {0} by simpa [orderAddMonoidHom, addMonoidHom, this]
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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)
h : ∀ (x : G), x ∈ Ico 0 (↑b : G) ↔ Membership.mem (γ := Finset G) {0} x
⊢ Ico 0 (↑b : G) = {0}

Tactic:
ext x
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
⊢ x ∈ Ico 0 (↑b : G) ↔ Membership.mem (γ := Finset G) {0} x

Tactic:
simp only [mem_Ico, mem_singleton]

Premises used: Finset.mem_singleton, Finset.mem_Ico
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
h₁ : x = 0 → 0 ≤ x ∧ x < (↑b : G)
⊢ 0 ≤ x ∧ x < (↑b : G) ↔ x = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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)
h : ∀ (hx' : ¬x = 0), False
⊢ x = 0

Tactic:
by_contra hx'
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
⊢ (↑b : G) ∈ Icc 0 a

Tactic:
have := b.2
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
⊢ 0 ≤ (↑b : G) ∧ (↑b : G) ≤ a

Tactic:
simp only [Finset.mem_Icc] at this

Premises used: Finset.mem_Icc
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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 : 0 ≤ (↑b : G) ∧ (↑b : G) ≤ a
⊢ x ∈ Icc 0 a

Tactic:
simpa [h₁] using h₂.le.trans this.2

Premises used: LT.lt.le, And.right, LE.le.trans
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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 : 0 ≤ (↑b : G) ∧ (↑b : G) ≤ a
⊢ Ne (α := ↥(Icc 0 a)) (Subtype.mk (p := fun (x : G) ↦ x ∈ Icc 0 a) 0 ⋯)
    (Subtype.mk (p := fun (x : G) ↦ x ∈ Icc 0 a) x ⋯)

Tactic:
simpa using Ne.symm hx'

Premises used: Ne.symm
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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 : 0 ≤ (↑b : G) ∧ (↑b : G) ≤ a
⊢ False

Tactic:
exact hb.2 (c := ⟨x, by simpa [h₁] using h₂.le.trans this.2⟩)
      (lt_of_le_of_ne h₁ (by simpa using Ne.symm hx')) h₂

Premises used: And.right, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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)
⊢ LE.le.{u_2} (α := G) 0 0 ∧ 0 < (↑b : G)

Tactic:
simpa using hb.1

Premises used: And.left
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
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
⊢ ZeroHom.toFun (↑(OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G)) : ZeroHom G ℤ) a ≤
      ZeroHom.toFun (↑(OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G)) : ZeroHom G ℤ) b ↔
    a ≤ b

Tactic:
obtain ⟨b, rfl⟩ := add_left_surjective a b

Premises used: add_left_surjective, rfl
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
this : LE.le (α := ℤ) (0 : ℤ) ((orderAddMonoidHom G : (a : G) → ℤ) b : ℤ) ↔ 0 ≤ b
⊢ 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:
simpa
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
suffices : LE.le (α := ℤ) (0 : ℤ) ((orderAddMonoidHom G : (a : G) → ℤ) b : ℤ) ↔ 0 ≤ b
⊢ 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:
suffices 0 ≤ orderAddMonoidHom G b ↔ 0 ≤ b by simpa
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
inr : ∀ (hb : b ≤ 0), LE.le (α := ℤ) (0 : ℤ) ((orderAddMonoidHom G : (a : G) → ℤ) b : ℤ) ↔ 0 ≤ b
⊢ LE.le (α := ℤ) (0 : ℤ) ((orderAddMonoidHom G : (a : G) → ℤ) b : ℤ) ↔ 0 ≤ b

Tactic:
obtain hb | hb := le_total 0 b

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
hb : 0 ≤ b
⊢ LE.le (α := ℤ) (0 : ℤ) ((orderAddMonoidHom G : (a : G) → ℤ) b : ℤ) ↔ 0 ≤ b

Tactic:
simp [orderAddMonoidHom, addMonoidHom, hb]

Premises used: LocallyFiniteOrder.orderAddMonoidHom, LocallyFiniteOrder.addMonoidHom
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
hb : b ≤ 0
⊢ LE.le (α := ℤ) (0 : ℤ) ((orderAddMonoidHom G : (a : G) → ℤ) b : ℤ) ↔ 0 ≤ b

Tactic:
simp [orderAddMonoidHom, addMonoidHom, hb]

Premises used: LocallyFiniteOrder.orderAddMonoidHom, LocallyFiniteOrder.addMonoidHom
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
inst_4 : Nontrivial G
x : G
⊢ Eq (α := ℤ) ((orderAddMonoidEquiv G : (a : G) → ℤ) x : ℤ) ((addMonoidHom G : (a : G) → ℤ) x : ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
G : Type u_3
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : LocallyFiniteOrder G
⊢ StrictMono (α := G) (β := Multiplicative ℤ) (⇑(orderMonoidHom G) : (a : G) → Multiplicative ℤ)

Tactic:
let : LocallyFiniteOrder (Additive G) := ‹LocallyFiniteOrder G›
  fun a b h ↦ orderAddMonoidHom_strictMono h

Premises used: StrictMono, LocallyFiniteOrder.orderAddMonoidHom_strictMono, Int.sub, Int.add
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
⊢ Monotone.{u_3, 0} (α := Gˣ)
    (OneHom.toFun (↑(OrderMonoidHom.toMonoidHom (orderMonoidHom Gˣ)) : OneHom Gˣ (Multiplicative ℤ)))

Tactic:
have := (orderMonoidHom Gˣ).monotone'
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
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
this :
  Monotone.{u_3, 0} (α := Gˣ)
    (OneHom.toFun (↑(OrderMonoidHom.toMonoidHom (orderMonoidHom Gˣ)) : OneHom Gˣ (Multiplicative ℤ)))
⊢ 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

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
G : Type u_3
inst : LinearOrderedCommGroupWithZero G
inst_1 : LocallyFiniteOrder Gˣ
⊢ StrictMono.{u_3, 0} (α := Gˣ) (β := Multiplicative ℤ) (⇑(orderMonoidHom Gˣ) : (a : Gˣ) → Multiplicative ℤ)

Tactic:
have := orderMonoidHom_strictMono (G := Gˣ)
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
G : Type u_3
inst : LinearOrderedCommGroupWithZero G
inst_1 : LocallyFiniteOrder Gˣ
this : StrictMono.{u_3, 0} (α := Gˣ) (β := Multiplicative ℤ) (⇑(orderMonoidHom Gˣ) : (a : Gˣ) → Multiplicative ℤ)
a b : G
h : a < b
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    (((orderMonoidWithZeroHom G : G →*₀o WithZero (Multiplicative ℤ)) : (a : G) → WithZero (Multiplicative ℤ)) a :
      WithZero (Multiplicative ℤ))
    (((orderMonoidWithZeroHom G : G →*₀o WithZero (Multiplicative ℤ)) : (a : G) → WithZero (Multiplicative ℤ)) b :
      WithZero (Multiplicative ℤ))

Tactic:
aesop (add simp orderMonoidWithZeroHom)

Premises used: LocallyFiniteOrder.orderMonoidWithZeroHom
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : One α
inst_1 : AddZeroClass α
inst_2 : PartialOrder α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
inst_5 : AddLeftStrictMono α
a : α
⊢ a < a + 1

Tactic:
lt_add_of_pos_right _ zero_lt_one

Premises used: lt_add_of_pos_right, zero_lt_one
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : One α
inst_1 : AddZeroClass α
inst_2 : PartialOrder α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
inst_5 : AddRightStrictMono α
a : α
⊢ a < 1 + a

Tactic:
lt_add_of_pos_left _ zero_lt_one

Premises used: zero_lt_one, lt_add_of_pos_left
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : Preorder α
inst_2 : ZeroLEOneClass α
inst_3 : AddLeftMono α
rw : 0 ≤ HAdd.hAdd (α := α) 1 1
⊢ LE.le.{u_1} (α := α) 0 2

Tactic:
rw [← one_add_one_eq_two]

Premises used: one_add_one_eq_two
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : Preorder α
inst_2 : ZeroLEOneClass α
inst_3 : AddLeftMono α
⊢ 0 ≤ HAdd.hAdd (α := α) 1 1

Tactic:
add_nonneg zero_le_one zero_le_one

Premises used: add_nonneg, zero_le_one
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : Preorder α
inst_2 : ZeroLEOneClass α
inst_3 : AddLeftMono α
⊢ 0 ≤ HAdd.hAdd (α := α) 1 1

Tactic:
exact add_nonneg zero_le_one zero_le_one

Premises used: add_nonneg, zero_le_one
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : Preorder α
inst_2 : ZeroLEOneClass α
inst_3 : AddLeftMono α
rw : 0 ≤ HAdd.hAdd (α := α) 2 1
⊢ LE.le.{u_1} (α := α) 0 3

Tactic:
rw [← two_add_one_eq_three]

Premises used: two_add_one_eq_three
-- Module: Mathlib.Algebra.Order.Monoid.NatCast
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : Preorder α
inst_2 : ZeroLEOneClass α
inst_3 : AddLeftMono α
⊢ 0 ≤ HAdd.hAdd (α := α) 2 1

Tactic:
add_nonneg zero_le_two zero_le_one

Premises used: add_nonneg, zero_le_one, zero_le_two