Theorem: Lean4Axiomatic.Integer.le_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 (Exists.intro (k : ℕ) (_ : b ≃ a₁ + coe k)) :=
  le_iff_add_nat.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
k : ℕ
h✝ : b ≃ a₁ + coe k
⊢ 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
k : ℕ
h✝ : b ≃ a₁ + coe k
⊢ a₂ ≤ b
Tactic:
apply le_iff_add_nat.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
k : ℕ
h✝ : b ≃ a₁ + coe k
⊢ ∃ k, b ≃ a₂ + coe k

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
k : ℕ
h✝ : b ≃ a₁ + coe k
⊢ ∃ k, b ≃ a₂ + coe k
Tactic:
have : b ≃ a₂ + coe k := Rel.trans ‹b ≃ a₁ + coe k› (AA.substL ‹a₁ ≃ 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✝ : a₁ ≤ b
k : ℕ
h✝ : b ≃ a₁ + coe k
this : b ≃ a₂ + coe k
⊢ ∃ k, b ≃ a₂ + coe k

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
k : ℕ
h✝ : b ≃ a₁ + coe k
this : b ≃ a₂ + coe k
⊢ ∃ k, b ≃ a₂ + coe k
Tactic:
exact Exists.intro k ‹b ≃ a₂ + coe k›
State after:
no goals