awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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 (a * b)) = #(Ico 1 a) + #(Ico 1 b)
have rw : #(Ico 1 b) + #(Ico 1 a) - #(Ico 1 b ∩ Ico (1 * b) (a * b)) = #(Ico 1 a) + #(Ico 1 b)
Tactic: rw [← this, Finset.card_union, Finset.card_Ico_mul_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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
⊢ 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))) : ℤ)
have 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))) : ℤ)
Tactic: wlog hab : a ≤ b generalizing a b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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))) : ℤ)
⊢ 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))) : ℤ)
have 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))) : ℤ)
Tactic: wlog hab : a ≤ b generalizing a b
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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 a)) : ℤ) (↑(#(Ico 0 (-a))) : ℤ) +
      HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ)
have h : HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-(a + b)))) : ℤ) =
  HSub.hSub (α := ℤ) (↑(#(Ico 0 (b + a))) : ℤ) (↑(#(Ico 0 (-(b + a)))) : ℤ)
Tactic: convert! this b a (le_of_not_ge hab) using 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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)))) : ℤ)
⊢ 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))) : ℤ)
have 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))) : ℤ)
Tactic: convert! this b a (le_of_not_ge hab) using 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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
⊢ 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))) : ℤ)
have 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))) : ℤ)
Tactic: obtain ha | ha := le_total 0 a
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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))) : ℤ)
⊢ 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))) : ℤ)
have 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))) : ℤ)
Tactic: obtain ha | ha := le_total 0 a
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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
⊢ 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))) : ℤ)
have 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))) : ℤ)
Tactic: obtain hb | hb := le_total 0 b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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))) : ℤ)
⊢ 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))) : ℤ)
have 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))) : ℤ)
Tactic: obtain hb | hb := le_total 0 b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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
⊢ 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))) : ℤ)
have 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))) : ℤ)
Tactic: obtain hb | hb := le_total 0 b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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))) : ℤ)
⊢ 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))) : ℤ)
have 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))) : ℤ)
Tactic: obtain hb | hb := le_total 0 b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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
have trans : -b ≤ 0
Tactic: trans 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (hypothesis)
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
⊢ 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))) : ℤ)
have this : -b ≤ a
Tactic: have : -b ≤ a := by trans 0 <;> simp [ha, hb]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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
⊢ 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))) : ℤ)
have 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))) : ℤ)
Tactic: obtain rfl := hb.antisymm (ha.trans hab)
Cleared hypotheses: b, hab, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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
⊢ 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))) : ℤ)
have 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))) : ℤ)
Tactic: obtain rfl := ha.antisymm hab
Cleared hypotheses: a, ha, hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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
⊢ 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))) : ℤ)
have inr : HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-b + -a))) : ℤ) =
  HAdd.hAdd (α := ℤ) (-(↑(#(Ico 0 (-a))) : ℤ)) (↑(#(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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + b))) : ℤ) (↑(#(Ico 0 (-b + -a))) : ℤ) =
    HAdd.hAdd (α := ℤ) (-(↑(#(Ico 0 (-a))) : ℤ)) (↑(#(Ico 0 b)) : ℤ)
have 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))) : ℤ)
Tactic: obtain ⟨b, rfl⟩ : ∃ r, b = r - a := ⟨a + b, by abel⟩
Cleared hypotheses: b, hab, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 (a + (b - a)))) : ℤ) (↑(#(Ico 0 (-(b - a) + -a))) : ℤ) =
    HAdd.hAdd (α := ℤ) (-(↑(#(Ico 0 (-a))) : ℤ)) (↑(#(Ico 0 (b - a))) : ℤ)
have inr : HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ) =
  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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ) =
    HAdd.hAdd (α := ℤ) (-(↑(#(Ico 0 (-a))) : ℤ)) (↑(#(Ico 0 (b - a))) : ℤ)
have inr : ∀ (hb' : 0 ≤ b),
  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
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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))) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(#(Ico 0 b)) : ℤ) (↑(#(Ico 0 (-b))) : ℤ) =
    HAdd.hAdd (α := ℤ) (-(↑(#(Ico 0 (-a))) : ℤ)) (↑(#(Ico 0 (b - a))) : ℤ)
have inr₁ : ∀ (hb' : b ≤ 0),
  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
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (hypothesis)
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
⊢ 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))) : ℤ)
have this : ¬0 < a + b
Tactic: have : ¬0 < a + b := by simpa using add_nonpos ha hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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
⊢ ZeroHom.toFun (↑(addMonoidHom G) : ZeroHom G ℤ) a ≤ ZeroHom.toFun (↑(addMonoidHom G) : ZeroHom G ℤ) b
have 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)
Tactic: obtain ⟨b, rfl⟩ := add_left_surjective a b
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (hypothesis)
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
⊢ ZeroHom.toFun (↑(addMonoidHom G) : ZeroHom G ℤ) a ≤
    ZeroHom.toFun (↑(addMonoidHom G) : ZeroHom G ℤ) ((fun (x : G) ↦ a + x) b)
have hab₁ : 0 ≤ b
Tactic: replace hab : 0 ≤ b := by simpa using hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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
⊢ ZeroHom.toFun (↑(addMonoidHom G) : ZeroHom G ℤ) a ≤
    ZeroHom.toFun (↑(addMonoidHom G) : ZeroHom G ℤ) ((fun (x : G) ↦ a + x) b)
have suffices : LE.le (α := ℤ) (0 : ℤ) ((addMonoidHom G : (a : G) → ℤ) b : ℤ)
Tactic: suffices 0 ≤ addMonoidHom G b by simpa
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
⊢ StrictMono (α := G) (β := ℤ) (⇑(orderAddMonoidHom G) : (a : G) → ℤ)
have rw : ∀ (a : G), 0 < a → LT.lt (α := ℤ) (0 : ℤ) ((orderAddMonoidHom G : (a : G) → ℤ) a : ℤ)
Tactic: rw [strictMono_iff_map_pos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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) → ℤ)
have refine : Function.Surjective (α := G) (β := ℤ) (⇑(orderAddMonoidHom G) : (a : G) → ℤ)
Tactic: refine ⟨orderAddMonoidHom_strictMono.injective, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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))
⊢ Function.Surjective (α := G) (β := ℤ) (⇑(orderAddMonoidHom G) : (a : G) → ℤ)
have obtain : ∀ (x : G) (hx : Eq (α := ℤ) ((OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G) : (a : G) → ℤ) x : ℤ) (1 : ℤ)),
  Function.Surjective (α := G) (β := ℤ) (⇑(orderAddMonoidHom G) : (a : G) → ℤ)
Tactic: obtain ⟨x, hx⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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.Surjective (α := G) (β := ℤ) (⇑(orderAddMonoidHom G) : (a : G) → ℤ)
have suffices : 1 ∈ AddMonoidHom.range (OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G))
Tactic: suffices 1 ∈ (orderAddMonoidHom G).range by
    obtain ⟨x, hx⟩ := this
    exact fun a ↦ ⟨a • x, by simp_all⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
Goal:
G : Type u_2
inst : AddCommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedAddMonoid G
inst_3 : LocallyFiniteOrder G
inst_4 : Nontrivial G
⊢ 1 ∈ AddMonoidHom.range (OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G))
have have : ∀ (a : G) (ha : 0 < a), 1 ∈ AddMonoidHom.range (OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G))
Tactic: have ⟨a, ha⟩ := exists_zero_lt (α := G)
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
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
⊢ 1 ∈ AddMonoidHom.range (OrderAddMonoidHom.toAddMonoidHom (orderAddMonoidHom G))
have obtain : ∀ (b : ↥(Icc 0 a)) (hb : Subtype.mk (p := fun (x : G) ↦ x ∈ Icc 0 a) 0 sorry ⋖ b),
  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))