case mp
α : Type ?u.243566
n m : ℕ
⊢ Raised n m → n ≤ m ∧ m ≤ n + 1

case mpr
α : Type ?u.243566
n m : ℕ
⊢ n ≤ m ∧ m ≤ n + 1 → Raised n m
α : Type ?u.243566
n m : ℕ
⊢ Raised n m ↔ n ≤ m ∧ m ≤ n + 1
constructor
case mp.inl
α : Type ?u.243566
m : ℕ
⊢ m ≤ m ∧ m ≤ m + 1

case mp.inr
α : Type ?u.243566
n : ℕ
⊢ n ≤ n + 1 ∧ n + 1 ≤ n + 1

case mpr
α : Type ?u.243566
n m : ℕ
⊢ n ≤ m ∧ m ≤ n + 1 → Raised n m
case mp
α : Type ?u.243566
n m : ℕ
⊢ Raised n m → n ≤ m ∧ m ≤ n + 1

case mpr
α : Type ?u.243566
n m : ℕ
⊢ n ≤ m ∧ m ≤ n + 1 → Raised n m
rintro (rfl | rfl)
no goals
case mp.inl
α : Type ?u.243566
m : ℕ
⊢ m ≤ m ∧ m ≤ m + 1
exact ⟨le_rfl, Nat.le_succ _⟩
no goals
case mp.inr
α : Type ?u.243566
n : ℕ
⊢ n ≤ n + 1 ∧ n + 1 ≤ n + 1
exact ⟨Nat.le_succ _, le_rfl⟩
case mpr.intro
α : Type ?u.243566
n m : ℕ
h₁ : n ≤ m
h₂ : m ≤ n + 1
⊢ Raised n m
case mpr
α : Type ?u.243566
n m : ℕ
⊢ n ≤ m ∧ m ≤ n + 1 → Raised n m
rintro ⟨h₁, h₂⟩
case mpr.intro.inl
α : Type ?u.243566
n : ℕ
h₁ : n ≤ n
h₂ : n ≤ n + 1
⊢ Raised n n

case mpr.intro.inr
α : Type ?u.243566
n m : ℕ
h₁✝ : n ≤ m
h₂ : m ≤ n + 1
h₁ : n < m
⊢ Raised n m
case mpr.intro
α : Type ?u.243566
n m : ℕ
h₁ : n ≤ m
h₂ : m ≤ n + 1
⊢ Raised n m
rcases eq_or_lt_of_le h₁ with (rfl | h₁)
no goals
case mpr.intro.inl
α : Type ?u.243566
n : ℕ
h₁ : n ≤ n
h₂ : n ≤ n + 1
⊢ Raised n n
exact Or.inl rfl
no goals
case mpr.intro.inr
α : Type ?u.243566
n m : ℕ
h₁✝ : n ≤ m
h₂ : m ≤ n + 1
h₁ : n < m
⊢ Raised n m
exact Or.inr (le_antisymm h₂ h₁)