Theorem: Lean4Axiomatic.Integer.lt_trans (Lean4Axiomatic/Integer/Order.lean)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
⊢ a < b → b < c → a < c
Tactic:
intro (_ : a < b) (_ : b < c)
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
⊢ a < c

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
⊢ a < c
Tactic:
have : Positive (b - a) := gt_iff_pos_diff.mp ‹a < b›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this : Positive (b - a)
⊢ a < c

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this : Positive (b - a)
⊢ a < c
Tactic:
have : Positive (c - b) := gt_iff_pos_diff.mp ‹b < c›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝ : Positive (b - a)
this : Positive (c - b)
⊢ a < c

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝ : Positive (b - a)
this : Positive (c - b)
⊢ a < c
Tactic:
apply gt_iff_pos_diff.mpr
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝ : Positive (b - a)
this : Positive (c - b)
⊢ Positive (c - a)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝ : Positive (b - a)
this : Positive (c - b)
⊢ Positive (c - a)
Tactic:
have : Positive ((c - b) + (b - a)) :=
  add_preserves_positive ‹Positive (c - b)› ‹Positive (b - a)›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝¹ : Positive (b - a)
this✝ : Positive (c - b)
this : Positive (c - b + (b - a))
⊢ Positive (c - a)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝¹ : Positive (b - a)
this✝ : Positive (c - b)
this : Positive (c - b + (b - a))
⊢ Positive (c - a)
Tactic:
have : (c - b) + (b - a) ≃ c - a := calc
  (c - b) + (b - a)   ≃ _ := AA.substL sub_defn
  (c + -b) + (b - a)  ≃ _ := AA.substR sub_defn
  (c + -b) + (b + -a) ≃ _ := AA.assoc
  c + (-b + (b + -a)) ≃ _ := AA.substR (Rel.symm AA.assoc)
  c + ((-b + b) + -a) ≃ _ := AA.substR (AA.substL AA.inverseL)
  c + (0 + -a)        ≃ _ := AA.substR AA.identL
  c + -a              ≃ _ := Rel.symm sub_defn
  c - a               ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝² : Positive (b - a)
this✝¹ : Positive (c - b)
this✝ : Positive (c - b + (b - a))
this : c - b + (b - a) ≃ c - a
⊢ Positive (c - a)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝² : Positive (b - a)
this✝¹ : Positive (c - b)
this✝ : Positive (c - b + (b - a))
this : c - b + (b - a) ≃ c - a
⊢ Positive (c - a)
Tactic:
have : Positive (c - a) :=
  AA.substFn ‹(c - b) + (b - a) ≃ c - a› ‹Positive ((c - b) + (b - a))›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝³ : Positive (b - a)
this✝² : Positive (c - b)
this✝¹ : Positive (c - b + (b - a))
this✝ : c - b + (b - a) ≃ c - a
this : Positive (c - a)
⊢ Positive (c - a)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝³ : Positive (b - a)
this✝² : Positive (c - b)
this✝¹ : Positive (c - b + (b - a))
this✝ : c - b + (b - a) ≃ c - a
this : Positive (c - a)
⊢ Positive (c - a)
Tactic:
exact this
State after:
no goals