Theorem: WavelengthRestate (NazgandLean4/IntegerInduction.lean)

State before:
p : ℤ → Prop
k : ℤ
⊢ (∀ (m : ℤ), p m ↔ p (m + k)) ↔ ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k)
Tactic:
constructor
State after:
case mp
p : ℤ → Prop
k : ℤ
⊢ (∀ (m : ℤ), p m ↔ p (m + k)) → ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k)

case mpr
p : ℤ → Prop
k : ℤ
⊢ (∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k)) → ∀ (m : ℤ), p m ↔ p (m + k)

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

State before:
case mp
p : ℤ → Prop
k : ℤ
h : ∀ (m : ℤ), p m ↔ p (m + k)
⊢ ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k)
Tactic:
rw [forall_swap, IntegerInduction]
State after:
case mp
p : ℤ → Prop
k : ℤ
h : ∀ (m : ℤ), p m ↔ p (m + k)
⊢ (∃ k_1, ∀ (x : ℤ), p x ↔ p (x + k_1 * k)) ∧
    ∀ (m : ℤ), (∀ (x : ℤ), p x ↔ p (x + m * k)) ↔ ∀ (x : ℤ), p x ↔ p (x + (m + 1) * k)

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

case mp.right
p : ℤ → Prop
k : ℤ
h : ∀ (m : ℤ), p m ↔ p (m + k)
⊢ ∀ (m : ℤ), (∀ (x : ℤ), p x ↔ p (x + m * k)) ↔ ∀ (x : ℤ), p x ↔ p (x + (m + 1) * k)

State before:
case mp.left
p : ℤ → Prop
k : ℤ
h : ∀ (m : ℤ), p m ↔ p (m + k)
⊢ ∃ k_1, ∀ (x : ℤ), p x ↔ p (x + k_1 * k)
Tactic:
use 0
State after:
case h
p : ℤ → Prop
k : ℤ
h : ∀ (m : ℤ), p m ↔ p (m + k)
⊢ ∀ (x : ℤ), p x ↔ p (x + 0 * k)

State before:
case h
p : ℤ → Prop
k : ℤ
h : ∀ (m : ℤ), p m ↔ p (m + k)
⊢ ∀ (x : ℤ), p x ↔ p (x + 0 * k)
Tactic:
simp only [zero_mul, add_zero, forall_const]
State after:
no goals

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

State before:
case mp.right
p : ℤ → Prop
k : ℤ
h : ∀ (m : ℤ), p m ↔ p (m + k)
m : ℤ
⊢ (∀ (x : ℤ), p x ↔ p (x + m * k)) ↔ ∀ (x : ℤ), p x ↔ p (x + (m + 1) * k)
Tactic:
constructor
State after:
case mp.right.mp
p : ℤ → Prop
k : ℤ
h : ∀ (m : ℤ), p m ↔ p (m + k)
m : ℤ
⊢ (∀ (x : ℤ), p x ↔ p (x + m * k)) → ∀ (x : ℤ), p x ↔ p (x + (m + 1) * k)

case mp.right.mpr
p : ℤ → Prop
k : ℤ
h : ∀ (m : ℤ), p m ↔ p (m + k)
m : ℤ
⊢ (∀ (x : ℤ), p x ↔ p (x + (m + 1) * k)) → ∀ (x : ℤ), p x ↔ p (x + m * k)

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

State before:
case mp.right.mp
p : ℤ → Prop
k : ℤ
h : ∀ (m : ℤ), p m ↔ p (m + k)
m : ℤ
h₀ : ∀ (x : ℤ), p x ↔ p (x + m * k)
k₀ : ℤ
⊢ p k₀ ↔ p (k₀ + (m + 1) * k)
Tactic:
rw [h₀ k₀, h]
State after:
case mp.right.mp
p : ℤ → Prop
k : ℤ
h : ∀ (m : ℤ), p m ↔ p (m + k)
m : ℤ
h₀ : ∀ (x : ℤ), p x ↔ p (x + m * k)
k₀ : ℤ
⊢ p (k₀ + m * k + k) ↔ p (k₀ + (m + 1) * k)

State before:
case mp.right.mp
p : ℤ → Prop
k : ℤ
h : ∀ (m : ℤ), p m ↔ p (m + k)
m : ℤ
h₀ : ∀ (x : ℤ), p x ↔ p (x + m * k)
k₀ : ℤ
⊢ p (k₀ + m * k + k) ↔ p (k₀ + (m + 1) * k)
Tactic:
ring_nf
State after:
no goals

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

State before:
case mp.right.mpr
p : ℤ → Prop
k : ℤ
h : ∀ (m : ℤ), p m ↔ p (m + k)
m : ℤ
h₀ : ∀ (x : ℤ), p x ↔ p (x + (m + 1) * k)
k₀ : ℤ
⊢ p k₀ ↔ p (k₀ + m * k)
Tactic:
rw [h₀ k₀, h (k₀ + m * k)]
State after:
case mp.right.mpr
p : ℤ → Prop
k : ℤ
h : ∀ (m : ℤ), p m ↔ p (m + k)
m : ℤ
h₀ : ∀ (x : ℤ), p x ↔ p (x + (m + 1) * k)
k₀ : ℤ
⊢ p (k₀ + (m + 1) * k) ↔ p (k₀ + m * k + k)

State before:
case mp.right.mpr
p : ℤ → Prop
k : ℤ
h : ∀ (m : ℤ), p m ↔ p (m + k)
m : ℤ
h₀ : ∀ (x : ℤ), p x ↔ p (x + (m + 1) * k)
k₀ : ℤ
⊢ p (k₀ + (m + 1) * k) ↔ p (k₀ + m * k + k)
Tactic:
ring_nf
State after:
no goals

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

State before:
case mpr
p : ℤ → Prop
k : ℤ
h : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k)
m : ℤ
⊢ p m ↔ p (m + k)
Tactic:
have h₀ := h m 1
State after:
case mpr
p : ℤ → Prop
k : ℤ
h : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k)
m : ℤ
h₀ : p m ↔ p (m + 1 * k)
⊢ p m ↔ p (m + k)

State before:
case mpr
p : ℤ → Prop
k : ℤ
h : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k)
m : ℤ
h₀ : p m ↔ p (m + 1 * k)
⊢ p m ↔ p (m + k)
Tactic:
simp only [one_mul] at h₀
State after:
case mpr
p : ℤ → Prop
k : ℤ
h : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k)
m : ℤ
h₀ : p m ↔ p (m + k)
⊢ p m ↔ p (m + k)

State before:
case mpr
p : ℤ → Prop
k : ℤ
h : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k)
m : ℤ
h₀ : p m ↔ p (m + k)
⊢ p m ↔ p (m + k)
Tactic:
exact h₀
State after:
no goals