Theorem: Lean4Axiomatic.Integer.lt_substL_eqv (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₁ a₂ b : ℤ
⊢ a₁ ≃ a₂ → a₁ < b → a₂ < b
Tactic:
intro (_ : a₁ ≃ a₂) (_ : a₁ < b)
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : a₁ < b
⊢ a₂ < b

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : a₁ < b
⊢ a₂ < b
Tactic:
have (And.intro (_ : a₁ ≤ b) (_ : a₁ ≄ b)) := lt_iff_le_neqv.mp ‹a₁ < b›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : a₁ < b
left✝ : a₁ ≤ b
right✝ : a₁ ≄ b
⊢ a₂ < b

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : a₁ < b
left✝ : a₁ ≤ b
right✝ : a₁ ≄ b
⊢ a₂ < b
Tactic:
apply lt_iff_le_neqv.mpr
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : a₁ < b
left✝ : a₁ ≤ b
right✝ : a₁ ≄ b
⊢ a₂ ≤ b ∧ a₂ ≄ b

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : a₁ < b
left✝ : a₁ ≤ b
right✝ : a₁ ≄ b
⊢ a₂ ≤ b ∧ a₂ ≄ b
Tactic:
have : a₂ ≤ b := AA.substLFn ‹a₁ ≃ a₂› ‹a₁ ≤ b›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : a₁ < b
left✝ : a₁ ≤ b
right✝ : a₁ ≄ b
this : a₂ ≤ b
⊢ a₂ ≤ b ∧ a₂ ≄ b

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : a₁ < b
left✝ : a₁ ≤ b
right✝ : a₁ ≄ b
this : a₂ ≤ b
⊢ a₂ ≤ b ∧ a₂ ≄ b
Tactic:
have : a₂ ≄ b := AA.neqv_substL ‹a₁ ≃ a₂› ‹a₁ ≄ b›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : a₁ < b
left✝ : a₁ ≤ b
right✝ : a₁ ≄ b
this✝ : a₂ ≤ b
this : a₂ ≄ b
⊢ a₂ ≤ b ∧ a₂ ≄ b

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : a₁ < b
left✝ : a₁ ≤ b
right✝ : a₁ ≄ b
this✝ : a₂ ≤ b
this : a₂ ≄ b
⊢ a₂ ≤ b ∧ a₂ ≄ b
Tactic:
exact And.intro ‹a₂ ≤ b› ‹a₂ ≄ b›
State after:
no goals