case refine_1
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n : ℤ
⊢ m ≤ m → P m

case refine_2
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n : ℤ
⊢ ∀ (k : ℤ), m ≤ k → (m ≤ k → P k) → m ≤ k + 1 → P (k + 1)

case refine_3
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n : ℤ
⊢ ∀ (k : ℤ), k ≤ m → (m ≤ k → P k) → m ≤ k - 1 → P (k - 1)
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n : ℤ
⊢ m ≤ n → P n
refine Int.inductionOn' n m ?_ ?_ ?_
case refine_1
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n : ℤ
a✝ : m ≤ m
⊢ P m
case refine_1
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n : ℤ
⊢ m ≤ m → P m
intro
no goals
case refine_1
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n : ℤ
a✝ : m ≤ m
⊢ P m
exact h0
case refine_2
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n k : ℤ
hle : m ≤ k
hi : m ≤ k → P k
a✝ : m ≤ k + 1
⊢ P (k + 1)
case refine_2
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n : ℤ
⊢ ∀ (k : ℤ), m ≤ k → (m ≤ k → P k) → m ≤ k + 1 → P (k + 1)
intro k hle hi _
no goals
case refine_2
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n k : ℤ
hle : m ≤ k
hi : m ≤ k → P k
a✝ : m ≤ k + 1
⊢ P (k + 1)
exact h1 k hle (hi hle)
case refine_3
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n k : ℤ
hle : k ≤ m
a✝ : m ≤ k → P k
hle' : m ≤ k - 1
⊢ P (k - 1)
case refine_3
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n : ℤ
⊢ ∀ (k : ℤ), k ≤ m → (m ≤ k → P k) → m ≤ k - 1 → P (k - 1)
intro k hle _ hle'
case refine_3.h
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n k : ℤ
hle : k ≤ m
a✝ : m ≤ k → P k
hle' : m ≤ k - 1
⊢ False
case refine_3
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n k : ℤ
hle : k ≤ m
a✝ : m ≤ k → P k
hle' : m ≤ k - 1
⊢ P (k - 1)
exfalso
no goals
case refine_3.h
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n k : ℤ
hle : k ≤ m
a✝ : m ≤ k → P k
hle' : m ≤ k - 1
⊢ False
exact lt_irrefl k (le_sub_one_iff.mp (hle.trans hle'))