awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b : M
ha : 1 ≤ a
hb : 1 ≤ b
⊢ Ico 1 b ∪ Ico (1 * b) (a * b) = Ico 1 (a * b)

Tactic:
simp [Ico_union_Ico, ha, hb, Right.one_le_mul ha hb]

Premises used: Right.one_le_mul, Finset.Ico_union_Ico
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b : M
ha : 1 ≤ a
hb : 1 ≤ b
⊢ Ico 1 b ∪ Ico (1 * b) (a * b) = Ico 1 (a * b)

Tactic:
have : Ico 1 b ∪ Ico (1 * b) (a * b) = Ico 1 (a * b) := by
    simp [Ico_union_Ico, ha, hb, Right.one_le_mul ha hb]
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b : M
ha : 1 ≤ a
hb : 1 ≤ b
this : Ico 1 b ∪ Ico (1 * b) (a * b) = Ico 1 (a * b)
rw : #(Ico 1 b) + #(Ico 1 a) - #(Ico 1 b ∩ Ico (1 * b) (a * b)) = #(Ico 1 a) + #(Ico 1 b)
⊢ #(Ico 1 (a * b)) = #(Ico 1 a) + #(Ico 1 b)

Tactic:
rw [← this, Finset.card_union, Finset.card_Ico_mul_right]

Premises used: Finset.card_Ico_mul_right, Finset.card_union
-- Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b : M
ha : 1 ≤ a
hb : 1 ≤ b
this : Ico 1 b ∪ Ico (1 * b) (a * b) = Ico 1 (a * b)
⊢ #(Ico 1 b) + #(Ico 1 a) - #(Ico 1 b ∩ Ico (1 * b) (a * b)) = #(Ico 1 a) + #(Ico 1 b)

Tactic:
simp [add_comm]

Premises used: add_comm
-- 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
⊢ HSub.hSub (α := ℤ) (↑(card.{u_2} (α := G) (Ico 0 0)) : ℤ) (↑(card.{u_2} (α := G) (Ico 0 (-0))) : ℤ) = 0

Tactic:
simp
-- 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
inr :
  ∀
    (this :
      ∀ (a b : G) (hab : a ≤ b),
        HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
          HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
            HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ))
    (hab : ¬a ≤ b),
    HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
      HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
        HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)
wlog :
  ∀ (a b : G) (hab : a ≤ b),
    HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
      HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
        HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
    HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
      HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)

Tactic:
wlog hab : a ≤ b generalizing a b
-- 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
this :
  ∀ (a b : G) (hab : a ≤ b),
    HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
      HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
        HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)
hab : ¬a ≤ b
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 (b + a))) : ℤ) (↑(#(Ico 0 (-(b + a)))) : ℤ) =
    HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ) +
      HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ)

Tactic:
this b a (le_of_not_ge hab)

Premises used: le_of_not_ge
-- 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
this :
  ∀ (a b : G) (hab : a ≤ b),
    HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
      HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
        HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)
hab : ¬a ≤ b
h :
  HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
    HSub.hSub (α := ℤ) (↑(#(Ico 0 (b + a))) : ℤ) (↑(#(Ico 0 (-(b + a)))) : ℤ)
h₁ :
  HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
      HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ) =
    HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ) +
      HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
    HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
      HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)

Tactic:
convert! this b a (le_of_not_ge hab) using 1

Premises used: le_of_not_ge
-- 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
this :
  ∀ (a b : G) (hab : a ≤ b),
    HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
      HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
        HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)
hab : ¬a ≤ b
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
    HSub.hSub (α := ℤ) (↑(#(Ico 0 (b + a))) : ℤ) (↑(#(Ico 0 (-(b + a)))) : ℤ)

Tactic:
simp only [add_comm]

Premises used: add_comm
-- 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
this :
  ∀ (a b : G) (hab : a ≤ b),
    HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
      HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
        HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)
hab : ¬a ≤ b
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
      HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ) =
    HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ) +
      HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ)

Tactic:
simp only [add_comm]

Premises used: add_comm
-- 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 : a ≤ b
inl :
  ∀ (ha : 0 ≤ a),
    HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
      HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
        HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)
inr :
  ∀ (ha : a ≤ 0),
    HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
      HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
        HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
    HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
      HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)

Tactic:
obtain ha | ha := le_total 0 a

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
a b : G
hab : a ≤ b
ha : 0 ≤ a
inl :
  ∀ (hb : 0 ≤ b),
    HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
      HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
        HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)
inl₁ :
  ∀ (hb : b ≤ 0),
    HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
      HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
        HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
    HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
      HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 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
a b : G
hab : a ≤ b
ha : a ≤ 0
inr :
  ∀ (hb : 0 ≤ b),
    HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
      HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
        HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)
inr₁ :
  ∀ (hb : b ≤ 0),
    HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
      HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
        HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
    HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
      HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 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
a b : G
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
trans : -b ≤ 0
trans₁ : 0 ≤ a
⊢ -b ≤ a

Tactic:
trans 0
-- 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 : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ -b ≤ 0

Tactic:
simp [ha, hb]
-- 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 : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a

Tactic:
simp [ha, hb]
-- 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 : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ -b ≤ a

Tactic:
have : -b ≤ a := by trans 0 <;> simp [ha, hb]
-- 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 : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
this : -b ≤ a
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
    HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
      HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)

Tactic:
simp [ha, hb, card_Ico_zero_add, this]

Premises used: card_Ico_zero_add
-- 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 : a ≤ b
ha : 0 ≤ a
hb : b ≤ 0
inl :
  ∀ (hab : a ≤ 0) (hb : LE.le.{u_2} (α := G) 0 0),
    HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + 0))) : ℤ) (↑(#(Ico 0 (-(a + 0)))) : ℤ) =
      HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
        HSub.hSub (α := ℤ) (↑(card.{u_2} (α := G) (Ico 0 0)) : ℤ) (↑(card.{u_2} (α := G) (Ico 0 (-0))) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
    HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
      HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)

Tactic:
obtain rfl := hb.antisymm (ha.trans hab)

Premises used: LE.le.antisymm, LE.le.trans, 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
a : G
ha : 0 ≤ a
hab : a ≤ 0
hb : LE.le.{u_2} (α := G) 0 0
inl :
  ∀ (ha : LE.le.{u_2} (α := G) 0 0) (hab : LE.le.{u_2} (α := G) 0 0),
    HSub.hSub (α := ℤ) (↑(#(Ico 0 (HAdd.hAdd (α := G) 0 0))) : ℤ) (↑(#(Ico 0 (-HAdd.hAdd (α := G) 0 0))) : ℤ) =
      HSub.hSub (α := ℤ) (↑(card.{u_2} (α := G) (Ico 0 0)) : ℤ) (↑(card.{u_2} (α := G) (Ico 0 (-0))) : ℤ) +
        HSub.hSub (α := ℤ) (↑(card.{u_2} (α := G) (Ico 0 0)) : ℤ) (↑(card.{u_2} (α := G) (Ico 0 (-0))) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + 0))) : ℤ) (↑(#(Ico 0 (-(a + 0)))) : ℤ) =
    HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
      HSub.hSub (α := ℤ) (↑(card.{u_2} (α := G) (Ico 0 0)) : ℤ) (↑(card.{u_2} (α := G) (Ico 0 (-0))) : ℤ)

Tactic:
obtain rfl := ha.antisymm hab

Premises used: LE.le.antisymm, 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
hb ha : LE.le.{u_2} (α := G) 0 0
hab : LE.le.{u_2} (α := G) 0 0
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 (HAdd.hAdd (α := G) 0 0))) : ℤ) (↑(#(Ico 0 (-HAdd.hAdd (α := G) 0 0))) : ℤ) =
    HSub.hSub (α := ℤ) (↑(card.{u_2} (α := G) (Ico 0 0)) : ℤ) (↑(card.{u_2} (α := G) (Ico 0 (-0))) : ℤ) +
      HSub.hSub (α := ℤ) (↑(card.{u_2} (α := G) (Ico 0 0)) : ℤ) (↑(card.{u_2} (α := G) (Ico 0 (-0))) : ℤ)

Tactic:
simp
-- 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 : a ≤ b
ha : a ≤ 0
hb : 0 ≤ b
inr :
  HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-b + -a))) : ℤ) =
    HAdd.hAdd (α := ℤ) (-(↑(#(Ico 0 (-a))) : ℤ)) (↑(#(Ico 0 b)) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
    HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
      HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)

Tactic:
simp only [neg_add_rev, ha, Ico_eq_empty_of_le, card_empty, Nat.cast_zero, zero_sub,
        Left.neg_nonpos_iff, hb, sub_zero]

Premises used: neg_add_rev, sub_zero, Left.neg_nonpos_iff, Finset.Ico_eq_empty_of_le, Finset.card_empty, Nat.cast_zero, zero_sub
-- 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 : a ≤ b
ha : a ≤ 0
hb : 0 ≤ b
⊢ b = a + b - a

Tactic:
abel
-- 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 : a ≤ b
ha : a ≤ 0
hb : 0 ≤ b
inr :
  ∀ (b : G) (hab : a ≤ b - a) (hb : 0 ≤ b - a),
    HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + (b - a)))) : ℤ) (↑(#(Ico 0 (-(b - a) + -a))) : ℤ) =
      HAdd.hAdd (α := ℤ) (-(↑(#(Ico 0 (-a))) : ℤ)) (↑(#(Ico 0 (b - a))) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-b + -a))) : ℤ) =
    HAdd.hAdd (α := ℤ) (-(↑(#(Ico 0 (-a))) : ℤ)) (↑(#(Ico 0 b)) : ℤ)

Tactic:
obtain ⟨b, rfl⟩ : ∃ r, b = r - a := ⟨a + b, by abel⟩

Premises used: 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
a : G
ha : a ≤ 0
b : G
hab : a ≤ b - a
hb : 0 ≤ b - a
inr :
  HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ) =
    HAdd.hAdd (α := ℤ) (-(↑(#(Ico 0 (-a))) : ℤ)) (↑(#(Ico 0 (b - a))) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + (b - a)))) : ℤ) (↑(#(Ico 0 (-(b - a) + -a))) : ℤ) =
    HAdd.hAdd (α := ℤ) (-(↑(#(Ico 0 (-a))) : ℤ)) (↑(#(Ico 0 (b - a))) : ℤ)

Tactic:
simp only [add_sub_cancel, neg_sub, sub_add_eq_add_sub, add_neg_cancel, zero_sub]

Premises used: add_neg_cancel, neg_sub, add_sub_cancel, sub_add_eq_add_sub, zero_sub
-- 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 : G
ha : a ≤ 0
b : G
hab : a ≤ b - a
hb : 0 ≤ b - a
inr :
  ∀ (hb' : 0 ≤ b),
    HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ) =
      HAdd.hAdd (α := ℤ) (-(↑(#(Ico 0 (-a))) : ℤ)) (↑(#(Ico 0 (b - a))) : ℤ)
inr₁ :
  ∀ (hb' : b ≤ 0),
    HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ) =
      HAdd.hAdd (α := ℤ) (-(↑(#(Ico 0 (-a))) : ℤ)) (↑(#(Ico 0 (b - a))) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ) =
    HAdd.hAdd (α := ℤ) (-(↑(#(Ico 0 (-a))) : ℤ)) (↑(#(Ico 0 (b - a))) : ℤ)

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
a : G
ha : a ≤ 0
b : G
hab : a ≤ b - a
hb : 0 ≤ b - a
hb' : 0 ≤ b
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ) =
    HAdd.hAdd (α := ℤ) (-(↑(#(Ico 0 (-a))) : ℤ)) (↑(#(Ico 0 (b - a))) : ℤ)

Tactic:
simp [hb', neg_add_eq_sub, eq_sub_iff_add_eq, ← Nat.cast_add,
          ← card_Ico_zero_add, ha, ← sub_eq_add_neg]

Premises used: neg_add_eq_sub, sub_eq_add_neg, eq_sub_iff_add_eq, card_Ico_zero_add, Nat.cast_add
-- 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 : G
ha : a ≤ 0
b : G
hab : a ≤ b - a
hb : 0 ≤ b - a
hb' : b ≤ 0
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ) =
    HAdd.hAdd (α := ℤ) (-(↑(#(Ico 0 (-a))) : ℤ)) (↑(#(Ico 0 (b - a))) : ℤ)

Tactic:
simp [hb', neg_add_eq_sub, eq_sub_iff_add_eq, sub_eq_iff_eq_add,
          ← Nat.cast_add, ← card_Ico_zero_add, hb, sub_add_eq_add_sub]

Premises used: neg_add_eq_sub, eq_sub_iff_add_eq, card_Ico_zero_add, Nat.cast_add, sub_eq_iff_eq_add, sub_add_eq_add_sub
-- 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 : a ≤ b
ha : a ≤ 0
hb : b ≤ 0
⊢ ¬0 < a + b

Tactic:
simpa using add_nonpos ha hb

Premises used: add_nonpos
-- 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 : a ≤ b
ha : a ≤ 0
hb : b ≤ 0
⊢ ¬0 < a + b

Tactic:
have : ¬0 < a + b := by simpa using add_nonpos ha hb
-- 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 : a ≤ b
ha : a ≤ 0
hb : b ≤ 0
this : ¬0 < a + b
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
    HSub.hSub (α := ℤ) (↑(#(Ico 0 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
      HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)

Tactic:
simp [ha, hb, card_Ico_zero_add, Ico_eq_empty, this]

Premises used: Finset.Ico_eq_empty, card_Ico_zero_add
-- 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 : a ≤ b
obtain :
  ∀ (b : G) (hab : a ≤ (fun (x : G) ↦ a + x) b),
    ZeroHom.toFun (↑(addMonoidHom G) : ZeroHom G ℤ) a ≤
      ZeroHom.toFun (↑(addMonoidHom G) : ZeroHom G ℤ) ((fun (x : G) ↦ a + x) b)
⊢ ZeroHom.toFun (↑(addMonoidHom G) : ZeroHom G ℤ) a ≤ ZeroHom.toFun (↑(addMonoidHom G) : ZeroHom G ℤ) 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
a b : G
hab : a ≤ (fun (x : G) ↦ a + x) b
⊢ 0 ≤ b

Tactic:
simpa using hab
-- 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 : a ≤ (fun (x : G) ↦ a + x) b
⊢ 0 ≤ b

Tactic:
replace hab : 0 ≤ b := by simpa using hab