Theorem: IntegerInduction (NazgandLean4/IntegerInduction.lean)

State before:
p : ℤ → Prop
⊢ (∀ (n : ℤ), p n) ↔ (∃ k, p k) ∧ ∀ (m : ℤ), p m ↔ p (m + 1)
Tactic:
constructor
State after:
case mp
p : ℤ → Prop
⊢ (∀ (n : ℤ), p n) → (∃ k, p k) ∧ ∀ (m : ℤ), p m ↔ p (m + 1)

case mpr
p : ℤ → Prop
⊢ ((∃ k, p k) ∧ ∀ (m : ℤ), p m ↔ p (m + 1)) → ∀ (n : ℤ), p n

State before:
case mp
p : ℤ → Prop
⊢ (∀ (n : ℤ), p n) → (∃ k, p k) ∧ ∀ (m : ℤ), p m ↔ p (m + 1)
Tactic:
intros h₀
State after:
case mp
p : ℤ → Prop
h₀ : ∀ (n : ℤ), p n
⊢ (∃ k, p k) ∧ ∀ (m : ℤ), p m ↔ p (m + 1)

State before:
case mp
p : ℤ → Prop
h₀ : ∀ (n : ℤ), p n
⊢ (∃ k, p k) ∧ ∀ (m : ℤ), p m ↔ p (m + 1)
Tactic:
constructor
State after:
case mp.left
p : ℤ → Prop
h₀ : ∀ (n : ℤ), p n
⊢ ∃ k, p k

case mp.right
p : ℤ → Prop
h₀ : ∀ (n : ℤ), p n
⊢ ∀ (m : ℤ), p m ↔ p (m + 1)

State before:
case mp.left
p : ℤ → Prop
h₀ : ∀ (n : ℤ), p n
⊢ ∃ k, p k
Tactic:
use 391547
State after:
case h
p : ℤ → Prop
h₀ : ∀ (n : ℤ), p n
⊢ p 391547

State before:
case h
p : ℤ → Prop
h₀ : ∀ (n : ℤ), p n
⊢ p 391547
Tactic:
exact h₀ 391547
State after:
no goals

State before:
case mp.right
p : ℤ → Prop
h₀ : ∀ (n : ℤ), p n
⊢ ∀ (m : ℤ), p m ↔ p (m + 1)
Tactic:
intros m
State after:
case mp.right
p : ℤ → Prop
h₀ : ∀ (n : ℤ), p n
m : ℤ
⊢ p m ↔ p (m + 1)

State before:
case mp.right
p : ℤ → Prop
h₀ : ∀ (n : ℤ), p n
m : ℤ
⊢ p m ↔ p (m + 1)
Tactic:
simp only [h₀ m, h₀ (m + 1)]
State after:
no goals

State before:
case mpr
p : ℤ → Prop
⊢ ((∃ k, p k) ∧ ∀ (m : ℤ), p m ↔ p (m + 1)) → ∀ (n : ℤ), p n
Tactic:
intros h₀
State after:
case mpr
p : ℤ → Prop
h₀ : (∃ k, p k) ∧ ∀ (m : ℤ), p m ↔ p (m + 1)
⊢ ∀ (n : ℤ), p n

State before:
case mpr
p : ℤ → Prop
h₀ : (∃ k, p k) ∧ ∀ (m : ℤ), p m ↔ p (m + 1)
⊢ ∀ (n : ℤ), p n
Tactic:
obtain ⟨he, hi⟩ := h₀
State after:
case mpr.intro
p : ℤ → Prop
he : ∃ k, p k
hi : ∀ (m : ℤ), p m ↔ p (m + 1)
⊢ ∀ (n : ℤ), p n

State before:
case mpr.intro
p : ℤ → Prop
he : ∃ k, p k
hi : ∀ (m : ℤ), p m ↔ p (m + 1)
⊢ ∀ (n : ℤ), p n
Tactic:
obtain ⟨k, hk⟩ := he
State after:
case mpr.intro.intro
p : ℤ → Prop
hi : ∀ (m : ℤ), p m ↔ p (m + 1)
k : ℤ
hk : p k
⊢ ∀ (n : ℤ), p n

State before:
case mpr.intro.intro
p : ℤ → Prop
hi : ∀ (m : ℤ), p m ↔ p (m + 1)
k : ℤ
hk : p k
⊢ ∀ (n : ℤ), p n
Tactic:
exact fun n => (Succ.rec_linear hi n k).mpr hk
State after:
no goals