internlm/Lean-Github huggingface dataset:
Theorem: MyNat.add_add_add
Proof state before:
a b c d : MyNat
⊢ a + b + (c + d) = a + c + (b + d)
Tactic:
rw [add_assoc, ← add_assoc b, add_comm b, add_assoc c, ← add_assoc a]
Proof state after:
no goals
Theorem: MyNat.zero_mul
Proof state before:
a : MyNat
⊢ 0 * a = 0
Tactic:
induction' a using MyNat.induction with d hd
Proof state after:
case zero

⊢ 0 * 0 = 0

case succ
d : MyNat
hd : 0 * d = 0
⊢ 0 * succ d = 0
Theorem: MyNat.zero_mul
Proof state before:
case zero

⊢ 0 * 0 = 0
Tactic:
rw [mul_zero]
Proof state after:
no goals
Theorem: MyNat.zero_mul
Proof state before:
case succ
d : MyNat
hd : 0 * d = 0
⊢ 0 * succ d = 0
Tactic:
rw [mul_succ, hd, add_zero]
Proof state after:
no goals
Theorem: MyNat.succ_eq_add_one
Proof state before:
a : MyNat
⊢ succ a = a + 1
Tactic:
rw [one_def, add_succ, add_zero]
Proof state after:
no goals
Theorem: MyNat.mul_one
Proof state before:
a : MyNat
⊢ a * 1 = a
Tactic:
rw [one_def, mul_succ, mul_zero, zero_add]
Proof state after:
no goals
Theorem: MyNat.one_mul
Proof state before:
a : MyNat
⊢ one * a = a
Tactic:
induction' a using MyNat.induction with d hd
Proof state after:
case zero

⊢ one * 0 = 0

case succ
d : MyNat
hd : one * d = d
⊢ one * succ d = succ d
Theorem: MyNat.one_mul
Proof state before:
case zero

⊢ one * 0 = 0
Tactic:
rw [mul_zero]
Proof state after:
no goals
Theorem: MyNat.one_mul
Proof state before:
case succ
d : MyNat
hd : one * d = d
⊢ one * succ d = succ d
Tactic:
rw [mul_succ, hd, one, add_succ, add_zero]
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
a b : MyNat
⊢ succ a * b = a * b + b
Tactic:
induction' b using MyNat.induction with d hd
Proof state after:
case zero
a : MyNat
⊢ succ a * 0 = a * 0 + 0

case succ
a d : MyNat
hd : succ a * d = a * d + d
⊢ succ a * succ d = a * succ d + succ d
Theorem: MyNat.succ_mul
Proof state before:
case zero
a : MyNat
⊢ succ a * 0 = a * 0 + 0
Tactic:
rw [mul_zero, mul_zero, add_zero]
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
case succ
a d : MyNat
hd : succ a * d = a * d + d
⊢ succ a * succ d = a * succ d + succ d
Tactic:
rw [mul_succ, hd, mul_succ, succ_eq_add_one, succ_eq_add_one, add_add_add]
Proof state after:
no goals
Theorem: MyGroup.mul_left_cancel
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
h : a * b = a * c
⊢ b = c
Tactic:
calc
     b = 1 * b         := by rw [one_mul]
     _ = a⁻¹ * a * b   := by rw [inv_mul_self]
     _ = a⁻¹ * (a * b) := by rw [mul_assoc]
     _ = a⁻¹ * (a * c) := by rw [h]
     _ = a⁻¹ * a * c   := by rw [mul_assoc]
     _ = 1 * c         := by rw [inv_mul_self]
     _ = c             := by rw [one_mul]
Proof state after:
no goals
Theorem: MyGroup.mul_left_cancel
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
h : a * b = a * c
⊢ b = 1 * b
Tactic:
rw [one_mul]
Proof state after:
no goals
Theorem: MyGroup.mul_left_cancel
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
h : a * b = a * c
⊢ 1 * b = a⁻¹ * a * b
Tactic:
rw [inv_mul_self]
Proof state after:
no goals
Theorem: MyGroup.mul_left_cancel
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
h : a * b = a * c
⊢ a⁻¹ * a * b = a⁻¹ * (a * b)
Tactic:
rw [mul_assoc]
Proof state after:
no goals
Theorem: MyGroup.mul_left_cancel
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
h : a * b = a * c
⊢ a⁻¹ * (a * b) = a⁻¹ * (a * c)
Tactic:
rw [h]
Proof state after:
no goals
Theorem: MyGroup.mul_left_cancel
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
h : a * b = a * c
⊢ a⁻¹ * (a * c) = a⁻¹ * a * c
Tactic:
rw [mul_assoc]
Proof state after:
no goals
Theorem: MyGroup.mul_left_cancel
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
h : a * b = a * c
⊢ a⁻¹ * a * c = 1 * c
Tactic:
rw [inv_mul_self]
Proof state after:
no goals
Theorem: MyGroup.mul_left_cancel
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
h : a * b = a * c
⊢ 1 * c = c
Tactic:
rw [one_mul]
Proof state after:
no goals
Theorem: MyGroup.mul_left_cancel'
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
h : a * b = a * c
⊢ b = c
Tactic:
rw [← one_mul b, ← inv_mul_self a, mul_assoc, h, ← mul_assoc, inv_mul_self, one_mul]
Proof state after:
no goals
Theorem: MyGroup.mul_eq_of_eq_inv_mul
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
h : b = a⁻¹ * c
⊢ a * b = c
Tactic:
apply mul_left_cancel a⁻¹
Proof state after:
case h
G : Type
inst✝ : MyGroup G
a b c : G
h : b = a⁻¹ * c
⊢ a⁻¹ * (a * b) = a⁻¹ * c
Theorem: MyGroup.mul_eq_of_eq_inv_mul
Proof state before:
case h
G : Type
inst✝ : MyGroup G
a b c : G
h : b = a⁻¹ * c
⊢ a⁻¹ * (a * b) = a⁻¹ * c
Tactic:
rw [← mul_assoc, inv_mul_self, one_mul, h]
Proof state after:
no goals
Theorem: MyGroup.mul_one
Proof state before:
G : Type
inst✝ : MyGroup G
a✝ b c a : G
⊢ a * 1 = a
Tactic:
apply mul_eq_of_eq_inv_mul
Proof state after:
case h
G : Type
inst✝ : MyGroup G
a✝ b c a : G
⊢ 1 = a⁻¹ * a
Theorem: MyGroup.mul_one
Proof state before:
case h
G : Type
inst✝ : MyGroup G
a✝ b c a : G
⊢ 1 = a⁻¹ * a
Tactic:
rw [inv_mul_self]
Proof state after:
no goals
Theorem: MyGroup.mul_inv_self
Proof state before:
G : Type
inst✝ : MyGroup G
a✝ b c a : G
⊢ a * a⁻¹ = 1
Tactic:
apply mul_eq_of_eq_inv_mul
Proof state after:
case h
G : Type
inst✝ : MyGroup G
a✝ b c a : G
⊢ a⁻¹ = a⁻¹ * 1
Theorem: MyGroup.mul_inv_self
Proof state before:
case h
G : Type
inst✝ : MyGroup G
a✝ b c a : G
⊢ a⁻¹ = a⁻¹ * 1
Tactic:
rw [mul_one]
Proof state after:
no goals
Theorem: MyGroup.inv_mul_cancel_left
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
⊢ a⁻¹ * (a * b) = b
Tactic:
simp [← mul_assoc]
Proof state after:
no goals
Theorem: MyGroup.mul_inv_cancel_left
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
⊢ a * (a⁻¹ * b) = b
Tactic:
simp [← mul_assoc]
Proof state after:
no goals
Theorem: MyGroup.left_inv_eq_right_inv
Proof state before:
G : Type
inst✝ : MyGroup G
a✝ b✝ c✝ a b c : G
h1 : b * a = 1
h2 : a * c = 1
⊢ b = c
Tactic:
have h : b * (a * c) = (b * a) * c := (mul_assoc b a c).symm
Proof state after:
G : Type
inst✝ : MyGroup G
a✝ b✝ c✝ a b c : G
h1 : b * a = 1
h2 : a * c = 1
h : b * (a * c) = b * a * c
⊢ b = c
Theorem: MyGroup.left_inv_eq_right_inv
Proof state before:
G : Type
inst✝ : MyGroup G
a✝ b✝ c✝ a b c : G
h1 : b * a = 1
h2 : a * c = 1
h : b * (a * c) = b * a * c
⊢ b = c
Tactic:
simpa [h2, h1] using h
Proof state after:
no goals
Theorem: MyGroup.mul_eq_one_iff_eq_inv
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
⊢ a⁻¹ = b → a * b = 1
Tactic:
rintro rfl
Proof state after:
G : Type
inst✝ : MyGroup G
a c : G
⊢ a * a⁻¹ = 1
Theorem: MyGroup.mul_eq_one_iff_eq_inv
Proof state before:
G : Type
inst✝ : MyGroup G
a c : G
⊢ a * a⁻¹ = 1
Tactic:
simp
Proof state after:
no goals
Theorem: MyGroup.one_inv
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
⊢ 1⁻¹ = 1
Tactic:
simp [← mul_eq_one_iff_eq_inv]
Proof state after:
no goals
Theorem: MyGroup.inv_inv
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
⊢ a⁻¹⁻¹ = a
Tactic:
simp [← mul_eq_one_iff_eq_inv]
Proof state after:
no goals
Theorem: MyGroup.mul_inv_rev
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
Tactic:
simp [← mul_eq_one_iff_eq_inv]
Proof state after:
no goals
Theorem: IntegerInduction
Proof state before:
p : ℤ → Prop
⊢ (∀ (n : ℤ), p n) ↔ (∃ k, p k) ∧ ∀ (m : ℤ), p m ↔ p (m + 1)
Tactic:
constructor
Proof 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
Theorem: IntegerInduction
Proof state before:
case mp
p : ℤ → Prop
⊢ (∀ (n : ℤ), p n) → (∃ k, p k) ∧ ∀ (m : ℤ), p m ↔ p (m + 1)
Tactic:
intros h₀
Proof state after:
case mp
p : ℤ → Prop
h₀ : ∀ (n : ℤ), p n
⊢ (∃ k, p k) ∧ ∀ (m : ℤ), p m ↔ p (m + 1)
Theorem: IntegerInduction
Proof state before:
case mp
p : ℤ → Prop
h₀ : ∀ (n : ℤ), p n
⊢ (∃ k, p k) ∧ ∀ (m : ℤ), p m ↔ p (m + 1)
Tactic:
constructor
Proof 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)
Theorem: IntegerInduction
Proof state before:
case mp.left
p : ℤ → Prop
h₀ : ∀ (n : ℤ), p n
⊢ ∃ k, p k
Tactic:
use 391547
Proof state after:
case h
p : ℤ → Prop
h₀ : ∀ (n : ℤ), p n
⊢ p 391547
Theorem: IntegerInduction
Proof state before:
case h
p : ℤ → Prop
h₀ : ∀ (n : ℤ), p n
⊢ p 391547
Tactic:
exact h₀ 391547
Proof state after:
no goals
Theorem: IntegerInduction
Proof state before:
case mp.right
p : ℤ → Prop
h₀ : ∀ (n : ℤ), p n
⊢ ∀ (m : ℤ), p m ↔ p (m + 1)
Tactic:
intros m
Proof state after:
case mp.right
p : ℤ → Prop
h₀ : ∀ (n : ℤ), p n
m : ℤ
⊢ p m ↔ p (m + 1)
Theorem: IntegerInduction
Proof 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)]
Proof state after:
no goals
Theorem: IntegerInduction
Proof state before:
case mpr
p : ℤ → Prop
⊢ ((∃ k, p k) ∧ ∀ (m : ℤ), p m ↔ p (m + 1)) → ∀ (n : ℤ), p n
Tactic:
intros h₀
Proof state after:
case mpr
p : ℤ → Prop
h₀ : (∃ k, p k) ∧ ∀ (m : ℤ), p m ↔ p (m + 1)
⊢ ∀ (n : ℤ), p n
Theorem: IntegerInduction
Proof state before:
case mpr
p : ℤ → Prop
h₀ : (∃ k, p k) ∧ ∀ (m : ℤ), p m ↔ p (m + 1)
⊢ ∀ (n : ℤ), p n
Tactic:
obtain ⟨he, hi⟩ := h₀
Proof state after:
case mpr.intro
p : ℤ → Prop
he : ∃ k, p k
hi : ∀ (m : ℤ), p m ↔ p (m + 1)
⊢ ∀ (n : ℤ), p n
Theorem: IntegerInduction
Proof 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
Proof state after:
case mpr.intro.intro
p : ℤ → Prop
hi : ∀ (m : ℤ), p m ↔ p (m + 1)
k : ℤ
hk : p k
⊢ ∀ (n : ℤ), p n
Theorem: IntegerInduction
Proof 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
Proof state after:
no goals
Theorem: WavelengthRestate
Proof state before:
p : ℤ → Prop
k : ℤ
⊢ (∀ (m : ℤ), p m ↔ p (m + k)) ↔ ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k)
Tactic:
constructor
Proof 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)
Theorem: WavelengthRestate
Proof state before:
case mp
p : ℤ → Prop
k : ℤ
⊢ (∀ (m : ℤ), p m ↔ p (m + k)) → ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k)
Tactic:
intros h
Proof state after:
case mp
p : ℤ → Prop
k : ℤ
h : ∀ (m : ℤ), p m ↔ p (m + k)
⊢ ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k)
Theorem: WavelengthRestate
Proof 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]
Proof 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)
Theorem: WavelengthRestate
Proof 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
Proof 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)
Theorem: WavelengthRestate
Proof 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
Proof state after:
case h
p : ℤ → Prop
k : ℤ
h : ∀ (m : ℤ), p m ↔ p (m + k)
⊢ ∀ (x : ℤ), p x ↔ p (x + 0 * k)
Theorem: WavelengthRestate
Proof 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]
Proof state after:
no goals
Theorem: WavelengthRestate
Proof 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
Proof 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)
Theorem: WavelengthRestate
Proof 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
Proof 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)
Theorem: WavelengthRestate
Proof 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₀
Proof 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)
Theorem: WavelengthRestate
Proof 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]
Proof 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)
Theorem: WavelengthRestate
Proof 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
Proof state after:
no goals
Theorem: WavelengthRestate
Proof 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₀
Proof 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)
Theorem: WavelengthRestate
Proof 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)]
Proof 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)
Theorem: WavelengthRestate
Proof 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
Proof state after:
no goals
Theorem: WavelengthRestate
Proof 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
Proof state after:
case mpr
p : ℤ → Prop
k : ℤ
h : ∀ (m k₀ : ℤ), p m ↔ p (m + k₀ * k)
m : ℤ
⊢ p m ↔ p (m + k)
Theorem: WavelengthRestate
Proof 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
Proof 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)
Theorem: WavelengthRestate
Proof 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₀
Proof 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)
Theorem: WavelengthRestate
Proof 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₀
Proof state after:
no goals
Theorem: associated_gcd_gcd
Proof state before:
a b : ℤ
⊢ Associated (IsBezout.gcd a b) (GCDMonoid.gcd a b)
Tactic:
exact IsBezout.associated_gcd_gcd ℤ
Proof state after:
no goals
Theorem: GcdLinearCombination
Proof state before:
k₀ k₁ : ℤ
⊢ ∃ m₀ m₁, ↑(k₀.gcd k₁) = m₀ * k₀ + m₁ * k₁
Tactic:
obtain ⟨m, n, h⟩ := IsBezout.gcd_eq_sum k₀ k₁
Proof state after:
case intro.intro
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
⊢ ∃ m₀ m₁, ↑(k₀.gcd k₁) = m₀ * k₀ + m₁ * k₁
Theorem: GcdLinearCombination
Proof state before:
case intro.intro
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
⊢ ∃ m₀ m₁, ↑(k₀.gcd k₁) = m₀ * k₀ + m₁ * k₁
Tactic:
have := associated_gcd_gcd k₀ k₁
Proof state after:
case intro.intro
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
this : Associated (IsBezout.gcd k₀ k₁) (GCDMonoid.gcd k₀ k₁)
⊢ ∃ m₀ m₁, ↑(k₀.gcd k₁) = m₀ * k₀ + m₁ * k₁
Theorem: GcdLinearCombination
Proof state before:
case intro.intro
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
this : Associated (IsBezout.gcd k₀ k₁) (GCDMonoid.gcd k₀ k₁)
⊢ ∃ m₀ m₁, ↑(k₀.gcd k₁) = m₀ * k₀ + m₁ * k₁
Tactic:
rw [Int.associated_iff] at this
Proof state after:
case intro.intro
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
this : IsBezout.gcd k₀ k₁ = GCDMonoid.gcd k₀ k₁ ∨ IsBezout.gcd k₀ k₁ = -GCDMonoid.gcd k₀ k₁
⊢ ∃ m₀ m₁, ↑(k₀.gcd k₁) = m₀ * k₀ + m₁ * k₁
Theorem: GcdLinearCombination
Proof state before:
case intro.intro
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
this : IsBezout.gcd k₀ k₁ = GCDMonoid.gcd k₀ k₁ ∨ IsBezout.gcd k₀ k₁ = -GCDMonoid.gcd k₀ k₁
⊢ ∃ m₀ m₁, ↑(k₀.gcd k₁) = m₀ * k₀ + m₁ * k₁
Tactic:
cases this with
| inl h' =>
  use m, n
  rw [h, Int.coe_gcd, h']
| inr h' =>
  use -m, -n
  rw [Int.coe_gcd]
  linarith
Proof state after:
no goals
Theorem: GcdLinearCombination
Proof state before:
case intro.intro.inl
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
h' : IsBezout.gcd k₀ k₁ = GCDMonoid.gcd k₀ k₁
⊢ ∃ m₀ m₁, ↑(k₀.gcd k₁) = m₀ * k₀ + m₁ * k₁
Tactic:
use m, n
Proof state after:
case h
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
h' : IsBezout.gcd k₀ k₁ = GCDMonoid.gcd k₀ k₁
⊢ ↑(k₀.gcd k₁) = m * k₀ + n * k₁
Theorem: GcdLinearCombination
Proof state before:
case h
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
h' : IsBezout.gcd k₀ k₁ = GCDMonoid.gcd k₀ k₁
⊢ ↑(k₀.gcd k₁) = m * k₀ + n * k₁
Tactic:
rw [h, Int.coe_gcd, h']
Proof state after:
no goals
Theorem: GcdLinearCombination
Proof state before:
case intro.intro.inr
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
h' : IsBezout.gcd k₀ k₁ = -GCDMonoid.gcd k₀ k₁
⊢ ∃ m₀ m₁, ↑(k₀.gcd k₁) = m₀ * k₀ + m₁ * k₁
Tactic:
use -m, -n
Proof state after:
case h
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
h' : IsBezout.gcd k₀ k₁ = -GCDMonoid.gcd k₀ k₁
⊢ ↑(k₀.gcd k₁) = -m * k₀ + -n * k₁
Theorem: GcdLinearCombination
Proof state before:
case h
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
h' : IsBezout.gcd k₀ k₁ = -GCDMonoid.gcd k₀ k₁
⊢ ↑(k₀.gcd k₁) = -m * k₀ + -n * k₁
Tactic:
rw [Int.coe_gcd]
Proof state after:
case h
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
h' : IsBezout.gcd k₀ k₁ = -GCDMonoid.gcd k₀ k₁
⊢ GCDMonoid.gcd k₀ k₁ = -m * k₀ + -n * k₁
Theorem: GcdLinearCombination
Proof state before:
case h
k₀ k₁ m n : ℤ
h : m * k₀ + n * k₁ = IsBezout.gcd k₀ k₁
h' : IsBezout.gcd k₀ k₁ = -GCDMonoid.gcd k₀ k₁
⊢ GCDMonoid.gcd k₀ k₁ = -m * k₀ + -n * k₁
Tactic:
linarith
Proof state after:
no goals
Theorem: WavelengthGcd
Proof 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
Proof 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₁))
Theorem: WavelengthGcd
Proof 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₀
Proof 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₁)
Theorem: WavelengthGcd
Proof 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₀
Proof 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₁)
Theorem: WavelengthGcd
Proof 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]
Proof 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₁)
Theorem: WavelengthGcd
Proof 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
Proof 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₁)
Theorem: WavelengthGcd
Proof 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
Proof 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₀)
Theorem: WavelengthGcd
Proof 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₁
Proof 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₀)
Theorem: WavelengthGcd
Proof 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
Proof 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₀)
Theorem: WavelengthGcd
Proof 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)]
Proof 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₀)
Theorem: WavelengthGcd
Proof 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]
Proof 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))
Theorem: WavelengthGcd
Proof 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
Proof state after:
no goals
Theorem: WavelengthGcd
Proof 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
Proof 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₁)