case intro
ι : Type ?u.42313
α : Type u
β : Type v
γ : Type w
δ : Type ?u.42322
π : ι → Type ?u.42327
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
hab : a < a + ↑(Nat.succ n)
⊢ r (f a) (f (a + ↑(Nat.succ n)))
ι : Type ?u.42313
α : Type u
β : Type v
γ : Type w
δ : Type ?u.42322
π : ι → Type ?u.42327
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a b : ℤ
hab : a < b
⊢ r (f a) (f b)
rcases lt.dest hab with ⟨n, rfl⟩
case intro
ι : Type ?u.42313
α : Type u
β : Type v
γ : Type w
δ : Type ?u.42322
π : ι → Type ?u.42327
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
⊢ r (f a) (f (a + ↑(Nat.succ n)))
case intro
ι : Type ?u.42313
α : Type u
β : Type v
γ : Type w
δ : Type ?u.42322
π : ι → Type ?u.42327
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
hab : a < a + ↑(Nat.succ n)
⊢ r (f a) (f (a + ↑(Nat.succ n)))
clear hab
case intro.zero
ι : Type ?u.42313
α : Type u
β : Type v
γ : Type w
δ : Type ?u.42322
π : ι → Type ?u.42327
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
⊢ r (f a) (f (a + ↑(Nat.succ Nat.zero)))

case intro.succ
ι : Type ?u.42313
α : Type u
β : Type v
γ : Type w
δ : Type ?u.42322
π : ι → Type ?u.42327
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + ↑(Nat.succ n)))
⊢ r (f a) (f (a + ↑(Nat.succ (Nat.succ n))))
case intro
ι : Type ?u.42313
α : Type u
β : Type v
γ : Type w
δ : Type ?u.42322
π : ι → Type ?u.42327
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
⊢ r (f a) (f (a + ↑(Nat.succ n)))
induction' n with n ihn
case intro.zero
ι : Type ?u.42313
α : Type u
β : Type v
γ : Type w
δ : Type ?u.42322
π : ι → Type ?u.42327
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
⊢ r (f a) (f (a + 1))
case intro.zero
ι : Type ?u.42313
α : Type u
β : Type v
γ : Type w
δ : Type ?u.42322
π : ι → Type ?u.42327
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
⊢ r (f a) (f (a + ↑(Nat.succ Nat.zero)))
rw [Int.ofNat_one]
no goals
case intro.zero
ι : Type ?u.42313
α : Type u
β : Type v
γ : Type w
δ : Type ?u.42322
π : ι → Type ?u.42327
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
⊢ r (f a) (f (a + 1))
apply h
case intro.succ
ι : Type ?u.42313
α : Type u
β : Type v
γ : Type w
δ : Type ?u.42322
π : ι → Type ?u.42327
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + ↑(Nat.succ n)))
⊢ r (f a) (f (a + ↑(n + 1) + 1))
case intro.succ
ι : Type ?u.42313
α : Type u
β : Type v
γ : Type w
δ : Type ?u.42322
π : ι → Type ?u.42327
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + ↑(Nat.succ n)))
⊢ r (f a) (f (a + ↑(Nat.succ (Nat.succ n))))
rw [Int.ofNat_succ, ← Int.add_assoc]
no goals
case intro.succ
ι : Type ?u.42313
α : Type u
β : Type v
γ : Type w
δ : Type ?u.42322
π : ι → Type ?u.42327
r✝ : α → α → Prop
inst✝¹ : Preorder α
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + ↑(Nat.succ n)))
⊢ r (f a) (f (a + ↑(n + 1) + 1))
exact _root_.trans ihn (h _)