Theorem: Lean4Axiomatic.Integer.lt_substR_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₂ → b < a₁ → b < a₂
Tactic:
intro (_ : a₁ ≃ a₂) (_ : b < a₁)
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✝ : b < a₁
⊢ b < a₂

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✝ : b < a₁
⊢ b < a₂
Tactic:
have (And.intro (_ : b ≤ a₁) (_ : b ≄ a₁)) := lt_iff_le_neqv.mp ‹b < a₁›
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✝ : b < a₁
left✝ : b ≤ a₁
right✝ : b ≄ a₁
⊢ b < a₂

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✝ : b < a₁
left✝ : b ≤ a₁
right✝ : b ≄ a₁
⊢ b < a₂
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✝ : b < a₁
left✝ : b ≤ a₁
right✝ : b ≄ a₁
⊢ b ≤ a₂ ∧ b ≄ a₂

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✝ : b < a₁
left✝ : b ≤ a₁
right✝ : b ≄ a₁
⊢ b ≤ a₂ ∧ b ≄ a₂
Tactic:
have : b ≤ a₂ := AA.substRFn ‹a₁ ≃ a₂› ‹b ≤ a₁›
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✝ : b < a₁
left✝ : b ≤ a₁
right✝ : b ≄ a₁
this : b ≤ a₂
⊢ b ≤ a₂ ∧ b ≄ a₂

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✝ : b < a₁
left✝ : b ≤ a₁
right✝ : b ≄ a₁
this : b ≤ a₂
⊢ b ≤ a₂ ∧ b ≄ a₂
Tactic:
have : b ≄ a₂ := AA.neqv_substR ‹a₁ ≃ a₂› ‹b ≄ a₁›
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✝ : b < a₁
left✝ : b ≤ a₁
right✝ : b ≄ a₁
this✝ : b ≤ a₂
this : b ≄ a₂
⊢ b ≤ a₂ ∧ b ≄ a₂

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✝ : b < a₁
left✝ : b ≤ a₁
right✝ : b ≄ a₁
this✝ : b ≤ a₂
this : b ≄ a₂
⊢ b ≤ a₂ ∧ b ≄ a₂
Tactic:
exact And.intro ‹b ≤ a₂› ‹b ≄ a₂›
State after:
no goals