Theorem: WavelengthGcd (NazgandLean4/IntegerInduction.lean)

State before:
p : ℤ → Prop
k₀ k₁ : ℤ
⊢ (∀ (m : ℤ), p m ↔ p (m + ↑(k₀.gcd k₁))) ↔ (∀ (m : ℤ), p m ↔ p (m + k₀)) ∧ ∀ (m : ℤ), p m ↔ p (m + k₁)
Tactic:
constructor
State after:
case mp
p : ℤ → Prop
k₀ k₁ : ℤ
⊢ (∀ (m : ℤ), p m ↔ p (m + ↑(k₀.gcd k₁))) → (∀ (m : ℤ), p m ↔ p (m + k₀)) ∧ ∀ (m : ℤ), p m ↔ p (m + k₁)

case mpr
p : ℤ → Prop
k₀ k₁ : ℤ
⊢ ((∀ (m : ℤ), p m ↔ p (m + k₀)) ∧ ∀ (m : ℤ), p m ↔ p (m + k₁)) → ∀ (m : ℤ), p m ↔ p (m + ↑(k₀.gcd k₁))

State before:
case mp
p : ℤ → Prop
k₀ k₁ : ℤ
⊢ (∀ (m : ℤ), p m ↔ p (m + ↑(k₀.gcd k₁))) → (∀ (m : ℤ), p m ↔ p (m + k₀)) ∧ ∀ (m : ℤ), p m ↔ p (m + k₁)
Tactic:
intros h₀
State after:
case mp
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m : ℤ), p m ↔ p (m + ↑(k₀.gcd k₁))
⊢ (∀ (m : ℤ), p m ↔ p (m + k₀)) ∧ ∀ (m : ℤ), p m ↔ p (m + k₁)

State before:
case mp
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m : ℤ), p m ↔ p (m + ↑(k₀.gcd k₁))
⊢ (∀ (m : ℤ), p m ↔ p (m + k₀)) ∧ ∀ (m : ℤ), p m ↔ p (m + k₁)
Tactic:
rw [WavelengthRestate] at h₀
State after:
case mp
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
⊢ (∀ (m : ℤ), p m ↔ p (m + k₀)) ∧ ∀ (m : ℤ), p m ↔ p (m + k₁)

State before:
case mp
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
⊢ (∀ (m : ℤ), p m ↔ p (m + k₀)) ∧ ∀ (m : ℤ), p m ↔ p (m + k₁)
Tactic:
rw [WavelengthRestate]
State after:
case mp
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
⊢ (∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)) ∧ ∀ (m : ℤ), p m ↔ p (m + k₁)

State before:
case mp
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
⊢ (∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)) ∧ ∀ (m : ℤ), p m ↔ p (m + k₁)
Tactic:
constructor
State after:
case mp.left
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
⊢ ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)

case mp.right
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
⊢ ∀ (m : ℤ), p m ↔ p (m + k₁)

State before:
case mp.left
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
⊢ ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)
Tactic:
have h₁ : ↑(k₀.gcd k₁) ∣ k₀ := Int.gcd_dvd_left
State after:
case mp.left
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
h₁ : ↑(k₀.gcd k₁) ∣ k₀
⊢ ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)

State before:
case mp.left
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
h₁ : ↑(k₀.gcd k₁) ∣ k₀
⊢ ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)
Tactic:
obtain ⟨w, hw⟩ := h₁
State after:
case mp.left.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₀ = ↑(k₀.gcd k₁) * w
⊢ ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)

State before:
case mp.left.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₀ = ↑(k₀.gcd k₁) * w
⊢ ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)
Tactic:
intros m k
State after:
case mp.left.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₀ = ↑(k₀.gcd k₁) * w
m k : ℤ
⊢ p m ↔ p (m + k * k₀)

State before:
case mp.left.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₀ = ↑(k₀.gcd k₁) * w
m k : ℤ
⊢ p m ↔ p (m + k * k₀)
Tactic:
rw [h₀ m (w * k)]
State after:
case mp.left.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₀ = ↑(k₀.gcd k₁) * w
m k : ℤ
⊢ p (m + w * k * ↑(k₀.gcd k₁)) ↔ p (m + k * k₀)

State before:
case mp.left.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₀ = ↑(k₀.gcd k₁) * w
m k : ℤ
⊢ p (m + w * k * ↑(k₀.gcd k₁)) ↔ p (m + k * k₀)
Tactic:
nth_rw 2 [hw]
State after:
case mp.left.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₀ = ↑(k₀.gcd k₁) * w
m k : ℤ
⊢ p (m + w * k * ↑(k₀.gcd k₁)) ↔ p (m + k * (↑(k₀.gcd k₁) * w))

State before:
case mp.left.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₀ = ↑(k₀.gcd k₁) * w
m k : ℤ
⊢ p (m + w * k * ↑(k₀.gcd k₁)) ↔ p (m + k * (↑(k₀.gcd k₁) * w))
Tactic:
ring_nf
State after:
no goals

State before:
case mp.right
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
⊢ ∀ (m : ℤ), p m ↔ p (m + k₁)
Tactic:
have h₁ : ↑(k₀.gcd k₁) ∣ k₁ := Int.gcd_dvd_right
State after:
case mp.right
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
h₁ : ↑(k₀.gcd k₁) ∣ k₁
⊢ ∀ (m : ℤ), p m ↔ p (m + k₁)

State before:
case mp.right
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
h₁ : ↑(k₀.gcd k₁) ∣ k₁
⊢ ∀ (m : ℤ), p m ↔ p (m + k₁)
Tactic:
obtain ⟨w, hw⟩ := h₁
State after:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
⊢ ∀ (m : ℤ), p m ↔ p (m + k₁)

State before:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
⊢ ∀ (m : ℤ), p m ↔ p (m + k₁)
Tactic:
rw [WavelengthRestate]
State after:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
⊢ ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)

State before:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
⊢ ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)
Tactic:
intros m k
State after:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
m k : ℤ
⊢ p m ↔ p (m + k * k₁)

State before:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
m k : ℤ
⊢ p m ↔ p (m + k * k₁)
Tactic:
rw [h₀ m (w * k)]
State after:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
m k : ℤ
⊢ p (m + w * k * ↑(k₀.gcd k₁)) ↔ p (m + k * k₁)

State before:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
m k : ℤ
⊢ p (m + w * k * ↑(k₀.gcd k₁)) ↔ p (m + k * k₁)
Tactic:
nth_rw 2 [hw]
State after:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
m k : ℤ
⊢ p (m + w * k * ↑(k₀.gcd k₁)) ↔ p (m + k * (↑(k₀.gcd k₁) * w))

State before:
case mp.right.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
w : ℤ
hw : k₁ = ↑(k₀.gcd k₁) * w
m k : ℤ
⊢ p (m + w * k * ↑(k₀.gcd k₁)) ↔ p (m + k * (↑(k₀.gcd k₁) * w))
Tactic:
ring_nf
State after:
no goals

State before:
case mpr
p : ℤ → Prop
k₀ k₁ : ℤ
⊢ ((∀ (m : ℤ), p m ↔ p (m + k₀)) ∧ ∀ (m : ℤ), p m ↔ p (m + k₁)) → ∀ (m : ℤ), p m ↔ p (m + ↑(k₀.gcd k₁))
Tactic:
intros h₀
State after:
case mpr
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : (∀ (m : ℤ), p m ↔ p (m + k₀)) ∧ ∀ (m : ℤ), p m ↔ p (m + k₁)
⊢ ∀ (m : ℤ), p m ↔ p (m + ↑(k₀.gcd k₁))

State before:
case mpr
p : ℤ → Prop
k₀ k₁ : ℤ
h₀ : (∀ (m : ℤ), p m ↔ p (m + k₀)) ∧ ∀ (m : ℤ), p m ↔ p (m + k₁)
⊢ ∀ (m : ℤ), p m ↔ p (m + ↑(k₀.gcd k₁))
Tactic:
obtain ⟨h₁, h₂⟩ := h₀
State after:
case mpr.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m : ℤ), p m ↔ p (m + k₀)
h₂ : ∀ (m : ℤ), p m ↔ p (m + k₁)
⊢ ∀ (m : ℤ), p m ↔ p (m + ↑(k₀.gcd k₁))

State before:
case mpr.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m : ℤ), p m ↔ p (m + k₀)
h₂ : ∀ (m : ℤ), p m ↔ p (m + k₁)
⊢ ∀ (m : ℤ), p m ↔ p (m + ↑(k₀.gcd k₁))
Tactic:
rw [WavelengthRestate] at *
State after:
case mpr.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)
h₂ : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)
⊢ ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))

State before:
case mpr.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)
h₂ : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)
⊢ ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * ↑(k₀.gcd k₁))
Tactic:
intros m j
State after:
case mpr.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)
h₂ : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)
m j : ℤ
⊢ p m ↔ p (m + j * ↑(k₀.gcd k₁))

State before:
case mpr.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)
h₂ : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)
m j : ℤ
⊢ p m ↔ p (m + j * ↑(k₀.gcd k₁))
Tactic:
obtain ⟨w₀, w₁, h₃⟩ := GcdLinearCombination k₀ k₁
State after:
case mpr.intro.intro.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)
h₂ : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)
m j w₀ w₁ : ℤ
h₃ : ↑(k₀.gcd k₁) = w₀ * k₀ + w₁ * k₁
⊢ p m ↔ p (m + j * ↑(k₀.gcd k₁))

State before:
case mpr.intro.intro.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)
h₂ : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)
m j w₀ w₁ : ℤ
h₃ : ↑(k₀.gcd k₁) = w₀ * k₀ + w₁ * k₁
⊢ p m ↔ p (m + j * ↑(k₀.gcd k₁))
Tactic:
rw [h₃, h₁ m (j * w₀), h₂ (m + j * w₀ * k₀) (j * w₁)]
State after:
case mpr.intro.intro.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)
h₂ : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)
m j w₀ w₁ : ℤ
h₃ : ↑(k₀.gcd k₁) = w₀ * k₀ + w₁ * k₁
⊢ p (m + j * w₀ * k₀ + j * w₁ * k₁) ↔ p (m + j * (w₀ * k₀ + w₁ * k₁))

State before:
case mpr.intro.intro.intro
p : ℤ → Prop
k₀ k₁ : ℤ
h₁ : ∀ (m k₀_1 : ℤ), p m ↔ p (m + k₀_1 * k₀)
h₂ : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k₁)
m j w₀ w₁ : ℤ
h₃ : ↑(k₀.gcd k₁) = w₀ * k₀ + w₁ * k₁
⊢ p (m + j * w₀ * k₀ + j * w₁ * k₁) ↔ p (m + j * (w₀ * k₀ + w₁ * k₁))
Tactic:
ring_nf
State after:
no goals