Theorem: Abstract.Matrix.lt_succ (YatimaStdLib/AbstractMatrix.lean)

State before:
A : Type ?u.204
inst✝³ : Inhabited A
inst✝² : Add A
inst✝¹ : Mul A
inst✝ : OfNat A 0
n : Nat
⊢ n < n + 1
Tactic:
rw [add_one]
State after:
A : Type ?u.204
inst✝³ : Inhabited A
inst✝² : Add A
inst✝¹ : Mul A
inst✝ : OfNat A 0
n : Nat
⊢ n < succ n

State before:
A : Type ?u.204
inst✝³ : Inhabited A
inst✝² : Add A
inst✝¹ : Mul A
inst✝ : OfNat A 0
n : Nat
⊢ n < succ n
Tactic:
apply lt_succ_of_le
State after:
case a
A : Type ?u.204
inst✝³ : Inhabited A
inst✝² : Add A
inst✝¹ : Mul A
inst✝ : OfNat A 0
n : Nat
⊢ n ≤ n

State before:
case a
A : Type ?u.204
inst✝³ : Inhabited A
inst✝² : Add A
inst✝¹ : Mul A
inst✝ : OfNat A 0
n : Nat
⊢ n ≤ n
Tactic:
apply Nat.le_refl
State after:
no goals