awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Star.Pi
Goal:
ι : Type u_1
inst : Finite ι
A : ι → Type u_2
inst_1 : (i : ι) → PartialOrder (A i)
inst_2 : (i : ι) → NonUnitalSemiring (A i)
inst_3 : (i : ι) → StarRing (A i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_2} (A i)
xa xy : (i : ι) → A i
this :
  Eq (α := AddSubmonoid ((i : ι) → A i)) (closure (Set.range fun (s : (i : ι) → A i) ↦ star s * s))
    (pi (M := A) Set.univ fun (i : ι) ↦ closure (Set.range fun (s : A i) ↦ star s * s))
refine_1 :
  ∀
    (h :
      ∀ (i : ι),
        ∃ (p : A i),
          Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) p ∧
            xy i = xa i + p),
    ∃ (p : (i : ι) → A i),
      (∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (p i)) ∧
        xy = xa + p
refine_2 :
  (∃ (p : (i : ι) → A i),
      (∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (p i)) ∧
        xy = xa + p) →
    ∀ (i : ι),
      ∃ (p : A i),
        Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) p ∧ xy i = xa i + p
⊢ (∀ (i : ι),
      ∃ (p : A i),
        Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) p ∧ xy i = xa i + p) ↔
    ∃ (p : (i : ι) → A i),
      (∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (p i)) ∧
        xy = xa + p

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Algebra.Order.Star.Pi
Goal:
ι : Type u_1
inst : Finite ι
A : ι → Type u_2
inst_1 : (i : ι) → PartialOrder (A i)
inst_2 : (i : ι) → NonUnitalSemiring (A i)
inst_3 : (i : ι) → StarRing (A i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_2} (A i)
xa xy : (i : ι) → A i
this :
  Eq (α := AddSubmonoid ((i : ι) → A i)) (closure (Set.range fun (s : (i : ι) → A i) ↦ star s * s))
    (pi (M := A) Set.univ fun (i : ι) ↦ closure (Set.range fun (s : A i) ↦ star s * s))
h :
  ∀ (i : ι),
    ∃ (p : A i),
      Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) p ∧ xy i = xa i + p
refine_1 :
  ∃ (p : (i : ι) → A i),
    (∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (p i)) ∧
      ∀ (x : ι), xy x = xa x + p x
⊢ ∃ (p : (i : ι) → A i),
    (∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (p i)) ∧
      xy = xa + p

Tactic:
simp only [funext_iff, add_apply]

Premises used: funext_iff, Pi.add_apply
-- Module: Mathlib.Algebra.Order.Star.Pi
Goal:
ι : Type u_1
inst : Finite ι
A : ι → Type u_2
inst_1 : (i : ι) → PartialOrder (A i)
inst_2 : (i : ι) → NonUnitalSemiring (A i)
inst_3 : (i : ι) → StarRing (A i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_2} (A i)
xa xy : (i : ι) → A i
this :
  Eq (α := AddSubmonoid ((i : ι) → A i)) (closure (Set.range fun (s : (i : ι) → A i) ↦ star s * s))
    (pi (M := A) Set.univ fun (i : ι) ↦ closure (Set.range fun (s : A i) ↦ star s * s))
h :
  ∀ (i : ι),
    ∃ (p : A i),
      Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) p ∧ xy i = xa i + p
⊢ ∃ (p : (i : ι) → A i),
    (∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (p i)) ∧
      ∀ (x : ι), xy x = xa x + p x

Tactic:
⟨fun i => h i |>.choose, fun i => h i |>.choose_spec.1, fun i => h i |>.choose_spec.2⟩

Premises used: Exists.choose_spec, And.right, And.left, And.intro, Exists.intro, Exists.choose
-- Module: Mathlib.Algebra.Order.Star.Pi
Goal:
ι : Type u_1
inst : Finite ι
A : ι → Type u_2
inst_1 : (i : ι) → PartialOrder (A i)
inst_2 : (i : ι) → NonUnitalSemiring (A i)
inst_3 : (i : ι) → StarRing (A i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_2} (A i)
xa xy : (i : ι) → A i
this :
  Eq (α := AddSubmonoid ((i : ι) → A i)) (closure (Set.range fun (s : (i : ι) → A i) ↦ star s * s))
    (pi (M := A) Set.univ fun (i : ι) ↦ closure (Set.range fun (s : A i) ↦ star s * s))
h :
  ∀ (i : ι),
    ∃ (p : A i),
      Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) p ∧ xy i = xa i + p
⊢ ∃ (p : (i : ι) → A i),
    (∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (p i)) ∧
      ∀ (x : ι), xy x = xa x + p x

Tactic:
exact ⟨fun i => h i |>.choose, fun i => h i |>.choose_spec.1, fun i => h i |>.choose_spec.2⟩
-- Module: Mathlib.Algebra.Order.Star.Pi
Goal:
ι : Type u_1
inst : Finite ι
A : ι → Type u_2
inst_1 : (i : ι) → PartialOrder (A i)
inst_2 : (i : ι) → NonUnitalSemiring (A i)
inst_3 : (i : ι) → StarRing (A i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_2} (A i)
xa xy : (i : ι) → A i
this :
  Eq (α := AddSubmonoid ((i : ι) → A i)) (closure (Set.range fun (s : (i : ι) → A i) ↦ star s * s))
    (pi (M := A) Set.univ fun (i : ι) ↦ closure (Set.range fun (s : A i) ↦ star s * s))
refine_2 :
  ∀ (x : (i : ι) → A i),
    (∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (x i)) →
      xy = xa + x →
        ∀ (i : ι),
          ∃ (p : A i),
            Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) p ∧
              xy i = xa i + p
⊢ (∃ (p : (i : ι) → A i),
      (∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (p i)) ∧
        xy = xa + p) →
    ∀ (i : ι),
      ∃ (p : A i),
        Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) p ∧ xy i = xa i + p

Tactic:
simp only [forall_exists_index, and_imp]

Premises used: and_imp, forall_exists_index
-- Module: Mathlib.Algebra.Order.Star.Pi
Goal:
ι : Type u_1
inst : Finite ι
A : ι → Type u_2
inst_1 : (i : ι) → PartialOrder (A i)
inst_2 : (i : ι) → NonUnitalSemiring (A i)
inst_3 : (i : ι) → StarRing (A i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_2} (A i)
xa : (i : ι) → A i
this :
  Eq (α := AddSubmonoid ((i : ι) → A i)) (closure (Set.range fun (s : (i : ι) → A i) ↦ star s * s))
    (pi (M := A) Set.univ fun (i : ι) ↦ closure (Set.range fun (s : A i) ↦ star s * s))
x : (i : ι) → A i
h : ∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (x i)
i : ι
⊢ Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (x i) ∧
    (xa + x) i = xa i + x i

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Order.Star.Pi
Goal:
ι : Type u_1
inst : Finite ι
A : ι → Type u_2
inst_1 : (i : ι) → PartialOrder (A i)
inst_2 : (i : ι) → NonUnitalSemiring (A i)
inst_3 : (i : ι) → StarRing (A i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_2} (A i)
xa : (i : ι) → A i
this :
  Eq (α := AddSubmonoid ((i : ι) → A i)) (closure (Set.range fun (s : (i : ι) → A i) ↦ star s * s))
    (pi (M := A) Set.univ fun (i : ι) ↦ closure (Set.range fun (s : A i) ↦ star s * s))
x : (i : ι) → A i
h : ∀ (i : ι), Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) (x i)
i : ι
⊢ ∃ (p : A i),
    Membership.mem (γ := AddSubmonoid (A i)) (closure (Set.range fun (s : A i) ↦ star s * s)) p ∧ (xa + x) i = xa i + p

Tactic:
exact ⟨x i, by simp [h]⟩
-- Module: Mathlib.Algebra.Order.Star.Prod
Goal:
α : Type u_1
β : Type u_2
inst : NonUnitalSemiring α
inst_1 : NonUnitalSemiring β
inst_2 : PartialOrder α
inst_3 : PartialOrder β
inst_4 : StarRing α
inst_5 : StarRing β
inst_6 : StarOrderedRing α
inst_7 : StarOrderedRing β
xa : α
xy : β
ya : α
yb : β
⊢ HMul.hMul (α := α) (star 0) 0 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Star.Prod
Goal:
α : Type u_1
β : Type u_2
inst : NonUnitalSemiring α
inst_1 : NonUnitalSemiring β
inst_2 : PartialOrder α
inst_3 : PartialOrder β
inst_4 : StarRing α
inst_5 : StarRing β
inst_6 : StarOrderedRing α
inst_7 : StarOrderedRing β
xa : α
xy : β
ya : α
yb : β
⊢ HMul.hMul (α := β) (star 0) 0 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Star.Prod
Goal:
α : Type u_1
β : Type u_2
inst : NonUnitalSemiring α
inst_1 : NonUnitalSemiring β
inst_2 : PartialOrder α
inst_3 : PartialOrder β
inst_4 : StarRing α
inst_5 : StarRing β
inst_6 : StarOrderedRing α
inst_7 : StarOrderedRing β
xa : α
xy : β
ya : α
yb : β
rw :
  Eq (α := AddSubmonoid (α × β)) (closure (Set.range fun (s : α × β) ↦ star s * s))
    (closure (Set.range fun (p : α × β) ↦ (star p.1 * p.1, star p.2 * p.2)))
⊢ Eq (α := AddSubmonoid (α × β)) (closure (Set.range fun (s : α × β) ↦ star s * s))
    (prod (closure (Set.range fun (s : α) ↦ star s * s)) (closure (Set.range fun (s : β) ↦ star s * s)))

Tactic:
rw [← closure_prod (Set.mem_range.2 ⟨0, by simp⟩) (Set.mem_range.2 ⟨0, by simp⟩),
        Set.prod_range_range_eq]

Premises used: Iff.mpr, Set.mem_range, AddSubmonoid.closure_prod, Exists.intro, Set.prod_range_range_eq, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Star.Prod
Goal:
α : Type u_1
β : Type u_2
inst : NonUnitalSemiring α
inst_1 : NonUnitalSemiring β
inst_2 : PartialOrder α
inst_3 : PartialOrder β
inst_4 : StarRing α
inst_5 : StarRing β
inst_6 : StarOrderedRing α
inst_7 : StarOrderedRing β
xa : α
xy : β
ya : α
yb : β
⊢ Eq (α := AddSubmonoid (α × β)) (closure (Set.range fun (s : α × β) ↦ star s * s))
    (prod (closure (Set.range fun (s : α) ↦ star s * s)) (closure (Set.range fun (s : β) ↦ star s * s)))

Tactic:
have :
        closure (Set.range fun s : α × β ↦ star s * s) =
          (closure <| Set.range fun s : α ↦ star s * s).prod
          (closure <| Set.range fun s : β ↦ star s * s) := by
      rw [← closure_prod (Set.mem_range.2 ⟨0, by simp⟩) (Set.mem_range.2 ⟨0, by simp⟩),
        Set.prod_range_range_eq]
      simp_rw [Prod.mul_def, Prod.star_def]
-- Module: Mathlib.Algebra.Order.Star.Prod
Goal:
α : Type u_1
β : Type u_2
inst : NonUnitalSemiring α
inst_1 : NonUnitalSemiring β
inst_2 : PartialOrder α
inst_3 : PartialOrder β
inst_4 : StarRing α
inst_5 : StarRing β
inst_6 : StarOrderedRing α
inst_7 : StarOrderedRing β
xa : α
xy : β
ya : α
yb : β
this :
  Eq (α := AddSubmonoid (α × β)) (closure (Set.range fun (s : α × β) ↦ star s * s))
    (prod (closure (Set.range fun (s : α) ↦ star s * s)) (closure (Set.range fun (s : β) ↦ star s * s)))
⊢ (xa, xy) ≤ (ya, yb) ↔
    ∃ (p : α × β),
      Membership.mem (γ := AddSubmonoid (α × β)) (closure (Set.range fun (s : α × β) ↦ star s * s)) p ∧
        (ya, yb) = (xa, xy) + p

Tactic:
simp only [mk_le_mk, Prod.exists, mk_add_mk, mk.injEq, StarOrderedRing.le_iff, this,
      AddSubmonoid.mem_prod, exists_and_exists_comm, and_and_and_comm]

Premises used: Prod.mk_add_mk, exists_and_exists_comm, AddSubmonoid.mem_prod, and_and_and_comm, StarOrderedRing.le_iff, Prod.mk.injEq, Prod.mk_le_mk, Prod.exists
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
⊢ a + (b - a) = b ↔ a ≤ b

Tactic:
⟨fun h => le_iff_exists_add.mpr ⟨b - a, h.symm⟩, add_tsub_cancel_of_le⟩

Premises used: Iff.mpr, le_iff_exists_add, HSub.hSub, Iff.intro, Exists.intro, Eq.symm, add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
rw : a + (b - a) = b ↔ a ≤ b
⊢ b - a + a = b ↔ a ≤ b

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
⊢ a + (b - a) = b ↔ a ≤ b

Tactic:
add_tsub_cancel_iff_le

Premises used: add_tsub_cancel_iff_le
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
⊢ a + (b - a) = b ↔ a ≤ b

Tactic:
exact add_tsub_cancel_iff_le

Premises used: add_tsub_cancel_iff_le
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
rw : a - b ≤ 0 ↔ a ≤ b
rw₁ : a ≤ b + 0 ↔ a ≤ b
rw₂ rw₃ : a ≤ b ↔ a ≤ b
⊢ a - b = 0 ↔ a ≤ b

Tactic:
rw [← nonpos_iff_eq_zero, tsub_le_iff_left, add_zero]

Premises used: tsub_le_iff_left, add_zero, nonpos_iff_eq_zero
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a : α
⊢ a - a = 0

Tactic:
tsub_eq_zero_of_le le_rfl

Premises used: le_rfl, tsub_eq_zero_of_le
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
⊢ a - b ≤ a

Tactic:
tsub_le_iff_left.mpr <| le_add_left le_rfl

Premises used: Iff.mpr, le_rfl, tsub_le_iff_left, le_add_left
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a : α
⊢ 0 - a = 0

Tactic:
tsub_eq_zero_of_le zero_le

Premises used: zero_le, tsub_eq_zero_of_le
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
⊢ a - (a + b) = 0

Tactic:
tsub_eq_zero_of_le <| self_le_add_right _ _

Premises used: tsub_eq_zero_of_le, self_le_add_right
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
rw : a - b ≠ 0 ↔ ¬a ≤ b
rw₁ : ¬a - b = 0 ↔ ¬a ≤ b
rw₂ rw₃ : ¬a ≤ b ↔ ¬a ≤ b
⊢ 0 < a - b ↔ ¬a ≤ b

Tactic:
rw [pos_iff_ne_zero, Ne, tsub_eq_zero_iff_le]

Premises used: Ne, tsub_eq_zero_iff_le, pos_iff_ne_zero
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
h : a < b
⊢ 0 < b - a

Tactic:
tsub_pos_iff_not_le.mpr h.not_ge

Premises used: Iff.mpr, LT.lt.not_ge, tsub_pos_iff_not_le
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
h : a < b
⊢ a - c < b

Tactic:
lt_of_le_of_lt tsub_le_self h

Premises used: lt_of_le_of_lt, tsub_le_self
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a - b ≤ a - c ↔ c ≤ b

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

Premises used: tsub_le_tsub_left, Iff.intro
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
refine : a - b ≤ a - c → c ≤ b
⊢ a - b ≤ a - c ↔ c ≤ b

Tactic:
refine ⟨?_, fun h => tsub_le_tsub_left h a⟩
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
rw : a + c ≤ a + b → c ≤ b
⊢ a - b ≤ a - c → c ≤ b

Tactic:
rw [tsub_le_iff_left, ← hc.add_tsub_assoc_of_le h, hc.le_tsub_iff_right (h.trans le_add_self),
    add_comm b]

Premises used: AddLECancellable.le_tsub_iff_right, tsub_le_iff_left, add_comm, AddLECancellable.add_tsub_assoc_of_le, LE.le.trans, le_add_self
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a + c ≤ a + b → c ≤ b

Tactic:
apply ha
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
ha : AddLECancellable a
hb : AddLECancellable b
hc : AddLECancellable c
hba : b ≤ a
hca : c ≤ a
simp_rw : a - b ≤ a - c ∧ a - c ≤ a - b ↔ b ≤ c ∧ c ≤ b
simp_rw₁ : a - b ≤ a - c ∧ b ≤ c ↔ b ≤ c ∧ c ≤ b
simp_rw₂ : c ≤ b ∧ b ≤ c ↔ b ≤ c ∧ c ≤ b
⊢ a - b = a - c ↔ b = c

Tactic:
simp_rw [le_antisymm_iff, ha.tsub_le_tsub_iff_left hb hba, ha.tsub_le_tsub_iff_left hc hca,
    and_comm]

Premises used: AddLECancellable.tsub_le_tsub_iff_left, and_comm, le_antisymm_iff
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
inst_5 : AddLeftReflectLE α
h : c ≤ a
⊢ a - b ≤ a - c ↔ c ≤ b

Tactic:
Contravariant.AddLECancellable.tsub_le_tsub_iff_left Contravariant.AddLECancellable h

Premises used: AddLECancellable.tsub_le_tsub_iff_left, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
inst_5 : AddLeftReflectLE α
hba : b ≤ a
hca : c ≤ a
⊢ a - b = a - c ↔ b = c

Tactic:
Contravariant.AddLECancellable.tsub_right_inj Contravariant.AddLECancellable
    Contravariant.AddLECancellable hba hca

Premises used: AddLECancellable.tsub_right_inj, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
inst_5 : AddLeftReflectLE α
⊢ AddCommMonoid α

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a_1 b_1 c_1 : α
inst_5 : AddLeftReflectLE α
a b c : α
h : Eq.{u_1 + 1} (α := α) ((fun (x : α) ↦ a + x) b) ((fun (x : α) ↦ a + x) c)
⊢ b = c

Tactic:
simpa only [add_tsub_cancel_left] using congr_arg (fun x => x - a) h

Premises used: HSub.hSub, add_tsub_cancel_left, congr_arg
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
rw : ¬a ≤ b ↔ b < a
rw₁ rw₂ : b < a ↔ b < a
⊢ 0 < a - b ↔ b < a

Tactic:
rw [tsub_pos_iff_not_le, not_le]

Premises used: not_le, tsub_pos_iff_not_le
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
inl : ∀ (h : a ≤ b), a - b = a - min a b
inr : ∀ (h : b ≤ a), a - b = a - min a b
⊢ a - b = a - min a b

Tactic:
rcases le_total a b with h | h

Premises used: le_total
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
h : a ≤ b
inl : a - b = a - a
inl₁ : a - b = 0
inl₂ inl₃ : Eq.{u_1 + 1} (α := α) 0 0
⊢ a - b = a - min a b

Tactic:
rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]

Premises used: tsub_eq_zero_of_le, tsub_self, min_eq_left
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
h : b ≤ a
inr inr₁ : a - b = a - b
⊢ a - b = a - min a b

Tactic:
rw [min_eq_right h]

Premises used: min_eq_right
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
hc : AddLECancellable c
⊢ a < b - c ↔ a + c < b

Tactic:
⟨lt_imp_lt_of_le_imp_le tsub_le_iff_right.mpr, hc.lt_tsub_of_add_lt_right⟩

Premises used: Iff.mpr, tsub_le_iff_right, AddLECancellable.lt_tsub_of_add_lt_right, Iff.intro, lt_imp_lt_of_le_imp_le
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
hc : AddLECancellable c
⊢ a < b - c ↔ c + a < b

Tactic:
⟨lt_imp_lt_of_le_imp_le tsub_le_iff_left.mpr, hc.lt_tsub_of_add_lt_left⟩

Premises used: Iff.mpr, tsub_le_iff_left, AddLECancellable.lt_tsub_of_add_lt_left, Iff.intro, lt_imp_lt_of_le_imp_le
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ a
rw : c + (a - c) < b ↔ a < b
rw₁ rw₂ : a < b ↔ a < b
⊢ a - c < b - c ↔ a < b

Tactic:
rw [hc.lt_tsub_iff_left, add_tsub_cancel_of_le h]

Premises used: AddLECancellable.lt_tsub_iff_left, add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : 0 < a
h₂ : 0 < b
⊢ a - b < a

Tactic:
tsub_le_self.lt_of_ne fun h => ?_

Premises used: LE.le.lt_of_ne, tsub_le_self
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : 0 < a
h₂ : 0 < b
refine : ∀ (h : a - b = a), False
⊢ a - b < a

Tactic:
refine tsub_le_self.lt_of_ne fun h => ?_

Premises used: LE.le.lt_of_ne, tsub_le_self
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : 0 < a
h₂ : 0 < b
h : a - b = a
⊢ b < a

Tactic:
rw [← h, tsub_pos_iff_lt] at h₁

Premises used: tsub_pos_iff_lt
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : 0 < a
h₂ : 0 < b
h : a - b = a
h₃ : b < a
⊢ 0 < b

Tactic:
rw [← h, tsub_pos_iff_lt] at h₁

Premises used: tsub_pos_iff_lt
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : 0 < a
h₂ : 0 < b
h : a - b = a
h₃ : b < a
h₄ : 0 < b
⊢ a - b = a

Tactic:
rw [← h, tsub_pos_iff_lt] at h₁

Premises used: tsub_pos_iff_lt
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : b < a
h₂ : 0 < b
h : a - b = a
⊢ False

Tactic:
h₂.not_ge (ha.add_le_iff_nonpos_left.1 <| add_le_of_le_tsub_left_of_le h₁.le h.ge)

Premises used: Eq.ge, AddLECancellable.add_le_iff_nonpos_left, LT.lt.le, Iff.mp, add_le_of_le_tsub_left_of_le, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : b < a
h₂ : 0 < b
h : a - b = a
⊢ False

Tactic:
exact h₂.not_ge (ha.add_le_iff_nonpos_left.1 <| add_le_of_le_tsub_left_of_le h₁.le h.ge)

Premises used: Eq.ge, AddLECancellable.add_le_iff_nonpos_left, LT.lt.le, Iff.mp, add_le_of_le_tsub_left_of_le, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
ha : AddLECancellable a
⊢ a - b < a ↔ 0 < a ∧ 0 < b

Tactic:
⟨fun h => ⟨h.pos, pos_of_ne_zero ?_⟩, fun h => ha.tsub_lt_self h.1 h.2⟩

Premises used: LT.lt.pos, AddLECancellable.tsub_lt_self, And.right, And.left, And.intro, Iff.intro, pos_of_ne_zero