internlm/Lean-Github huggingface dataset:
Theorem: ftf_of_ge_8_le_10
Proof state before:
case inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
⊢ from_three_five n
Tactic:
eliminate (lt_or_le n 10) with htri10 htri10
Proof state after:
case inr.inl
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
htri10 : n < 10
⊢ from_three_five n

case inr.inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
htri10 : 10 ≤ n
⊢ from_three_five n
Theorem: ftf_of_ge_8_le_10
Proof state before:
case inr.inl
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
htri10 : n < 10
⊢ from_three_five n

case inr.inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
htri10 : 10 ≤ n
⊢ from_three_five n
Tactic:
{
  sorry
}
Proof state after:
case inr.inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
htri10 : 10 ≤ n
⊢ from_three_five n
Theorem: ftf_of_ge_8_le_10
Proof state before:
case inr.inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
htri10 : 10 ≤ n
⊢ from_three_five n
Tactic:
{
  sorry
}
Proof state after:
no goals
Theorem: ftf_of_ge_8_le_10
Proof state before:
case inr.inl
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
htri10 : n < 10
⊢ from_three_five n
Tactic:
sorry
Proof state after:
no goals
Theorem: ftf_of_ge_8_le_10
Proof state before:
case inr.inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
htri10 : 10 ≤ n
⊢ from_three_five n
Tactic:
sorry
Proof state after:
no goals
Theorem: ftf_add_3_of_ftf_self
Proof state before:
P : ℕ → Prop
n : ℕ
⊢ from_three_five n → from_three_five (n + 3)
Tactic:
sorry
Proof state after:
no goals
Theorem: ftf_of_ftf_sub_3
Proof state before:
P : ℕ → Prop
n : ℕ
⊢ 3 ≤ n → from_three_five (n - 3) → from_three_five n
Tactic:
intro h_3_le_n hftf
Proof state after:
P : ℕ → Prop
n : ℕ
h_3_le_n : 3 ≤ n
hftf : from_three_five (n - 3)
⊢ from_three_five n
Theorem: ftf_of_ftf_sub_3
Proof state before:
P : ℕ → Prop
n : ℕ
h_3_le_n : 3 ≤ n
hftf : from_three_five (n - 3)
⊢ from_three_five n
Tactic:
have : (n-3) + 3 = n := by {
  sorry
}
Proof state after:
P : ℕ → Prop
n : ℕ
h_3_le_n : 3 ≤ n
hftf : from_three_five (n - 3)
this : n - 3 + 3 = n
⊢ from_three_five n
Theorem: ftf_of_ftf_sub_3
Proof state before:
P : ℕ → Prop
n : ℕ
h_3_le_n : 3 ≤ n
hftf : from_three_five (n - 3)
this : n - 3 + 3 = n
⊢ from_three_five n
Tactic:
sorry
Proof state after:
no goals
Theorem: ftf_of_ftf_sub_3
Proof state before:
P : ℕ → Prop
n : ℕ
h_3_le_n : 3 ≤ n
hftf : from_three_five (n - 3)
⊢ n - 3 + 3 = n
Tactic:
sorry
Proof state after:
no goals
Theorem: all_from_three_five
Proof state before:
P : ℕ → Prop
⊢ ∀ (n : ℕ), 8 ≤ n → from_three_five n
Tactic:
strong_induction
Proof state after:
P : ℕ → Prop
⊢ ∀ (n : ℕ), (∀ (m : ℕ), m < n → 8 ≤ m → from_three_five m) → 8 ≤ n → from_three_five n
Theorem: all_from_three_five
Proof state before:
P : ℕ → Prop
⊢ ∀ (n : ℕ), (∀ (m : ℕ), m < n → 8 ≤ m → from_three_five m) → 8 ≤ n → from_three_five n
Tactic:
intro n hind h
Proof state after:
P : ℕ → Prop
n : ℕ
hind : ∀ (m : ℕ), m < n → 8 ≤ m → from_three_five m
h : 8 ≤ n
⊢ from_three_five n
Theorem: all_from_three_five
Proof state before:
P : ℕ → Prop
n : ℕ
hind : ∀ (m : ℕ), m < n → 8 ≤ m → from_three_five m
h : 8 ≤ n
⊢ from_three_five n
Tactic:
eliminate (lt_or_le n 11) with htri htri
Proof state after:
case inl
P : ℕ → Prop
n : ℕ
hind : ∀ (m : ℕ), m < n → 8 ≤ m → from_three_five m
h : 8 ≤ n
htri : n < 11
⊢ from_three_five n

case inr
P : ℕ → Prop
n : ℕ
hind : ∀ (m : ℕ), m < n → 8 ≤ m → from_three_five m
h : 8 ≤ n
htri : 11 ≤ n
⊢ from_three_five n
Theorem: all_from_three_five
Proof state before:
case inl
P : ℕ → Prop
n : ℕ
hind : ∀ (m : ℕ), m < n → 8 ≤ m → from_three_five m
h : 8 ≤ n
htri : n < 11
⊢ from_three_five n

case inr
P : ℕ → Prop
n : ℕ
hind : ∀ (m : ℕ), m < n → 8 ≤ m → from_three_five m
h : 8 ≤ n
htri : 11 ≤ n
⊢ from_three_five n
Tactic:
{
  sorry
}
Proof state after:
case inr
P : ℕ → Prop
n : ℕ
hind : ∀ (m : ℕ), m < n → 8 ≤ m → from_three_five m
h : 8 ≤ n
htri : 11 ≤ n
⊢ from_three_five n
Theorem: all_from_three_five
Proof state before:
case inr
P : ℕ → Prop
n : ℕ
hind : ∀ (m : ℕ), m < n → 8 ≤ m → from_three_five m
h : 8 ≤ n
htri : 11 ≤ n
⊢ from_three_five n
Tactic:
{
  sorry
}
Proof state after:
no goals
Theorem: all_from_three_five
Proof state before:
case inl
P : ℕ → Prop
n : ℕ
hind : ∀ (m : ℕ), m < n → 8 ≤ m → from_three_five m
h : 8 ≤ n
htri : n < 11
⊢ from_three_five n
Tactic:
sorry
Proof state after:
no goals
Theorem: all_from_three_five
Proof state before:
case inr
P : ℕ → Prop
n : ℕ
hind : ∀ (m : ℕ), m < n → 8 ≤ m → from_three_five m
h : 8 ≤ n
htri : 11 ≤ n
⊢ from_three_five n
Tactic:
sorry
Proof state after:
no goals
Theorem: BrownCs22.Int.ModEq.refl
Proof state before:
n a : ℤ
⊢ a - a = n * 0
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.ModEq.add
Proof state before:
n a b c d : ℤ
h1 : a ≡ b [ZMOD n]
h2 : c ≡ d [ZMOD n]
⊢ a + c ≡ b + d [ZMOD n]
Tactic:
obtain ⟨x, hx⟩ := h1
Proof state after:
case intro
n a b c d : ℤ
h2 : c ≡ d [ZMOD n]
x : ℤ
hx : a - b = n * x
⊢ a + c ≡ b + d [ZMOD n]
Theorem: BrownCs22.Int.ModEq.add
Proof state before:
case intro
n a b c d : ℤ
h2 : c ≡ d [ZMOD n]
x : ℤ
hx : a - b = n * x
⊢ a + c ≡ b + d [ZMOD n]
Tactic:
obtain ⟨y, hy⟩ := h2
Proof state after:
case intro.intro
n a b c d x : ℤ
hx : a - b = n * x
y : ℤ
hy : c - d = n * y
⊢ a + c ≡ b + d [ZMOD n]
Theorem: BrownCs22.Int.ModEq.add
Proof state before:
case intro.intro
n a b c d x : ℤ
hx : a - b = n * x
y : ℤ
hy : c - d = n * y
⊢ a + c ≡ b + d [ZMOD n]
Tactic:
exact ⟨x + y, by linear_combination hx + hy⟩
Proof state after:
no goals
Theorem: BrownCs22.Int.ModEq.add
Proof state before:
n a b c d x : ℤ
hx : a - b = n * x
y : ℤ
hy : c - d = n * y
⊢ a + c - (b + d) = n * (x + y)
Tactic:
linear_combination hx + hy
Proof state after:
no goals
Theorem: BrownCs22.Int.ModEq.sub
Proof state before:
n a b c d : ℤ
h1 : a ≡ b [ZMOD n]
h2 : c ≡ d [ZMOD n]
⊢ a - c ≡ b - d [ZMOD n]
Tactic:
obtain ⟨x, hx⟩ := h1
Proof state after:
case intro
n a b c d : ℤ
h2 : c ≡ d [ZMOD n]
x : ℤ
hx : a - b = n * x
⊢ a - c ≡ b - d [ZMOD n]
Theorem: BrownCs22.Int.ModEq.sub
Proof state before:
case intro
n a b c d : ℤ
h2 : c ≡ d [ZMOD n]
x : ℤ
hx : a - b = n * x
⊢ a - c ≡ b - d [ZMOD n]
Tactic:
obtain ⟨y, hy⟩ := h2
Proof state after:
case intro.intro
n a b c d x : ℤ
hx : a - b = n * x
y : ℤ
hy : c - d = n * y
⊢ a - c ≡ b - d [ZMOD n]
Theorem: BrownCs22.Int.ModEq.sub
Proof state before:
case intro.intro
n a b c d x : ℤ
hx : a - b = n * x
y : ℤ
hy : c - d = n * y
⊢ a - c ≡ b - d [ZMOD n]
Tactic:
exact ⟨x - y, by linear_combination hx - hy⟩
Proof state after:
no goals
Theorem: BrownCs22.Int.ModEq.sub
Proof state before:
n a b c d x : ℤ
hx : a - b = n * x
y : ℤ
hy : c - d = n * y
⊢ a - c - (b - d) = n * (x - y)
Tactic:
linear_combination hx - hy
Proof state after:
no goals
Theorem: BrownCs22.Int.ModEq.neg
Proof state before:
n a b : ℤ
h1 : a ≡ b [ZMOD n]
⊢ -a ≡ -b [ZMOD n]
Tactic:
obtain ⟨x, hx⟩ := h1
Proof state after:
case intro
n a b x : ℤ
hx : a - b = n * x
⊢ -a ≡ -b [ZMOD n]
Theorem: BrownCs22.Int.ModEq.neg
Proof state before:
case intro
n a b x : ℤ
hx : a - b = n * x
⊢ -a ≡ -b [ZMOD n]
Tactic:
exact ⟨-x, by linear_combination -hx⟩
Proof state after:
no goals
Theorem: BrownCs22.Int.ModEq.neg
Proof state before:
n a b x : ℤ
hx : a - b = n * x
⊢ -a - -b = n * -x
Tactic:
linear_combination -hx
Proof state after:
no goals
Theorem: BrownCs22.Int.ModEq.mul
Proof state before:
n a b c d : ℤ
h1 : a ≡ b [ZMOD n]
h2 : c ≡ d [ZMOD n]
⊢ a * c ≡ b * d [ZMOD n]
Tactic:
obtain ⟨x, hx⟩ := h1
Proof state after:
case intro
n a b c d : ℤ
h2 : c ≡ d [ZMOD n]
x : ℤ
hx : a - b = n * x
⊢ a * c ≡ b * d [ZMOD n]
Theorem: BrownCs22.Int.ModEq.mul
Proof state before:
case intro
n a b c d : ℤ
h2 : c ≡ d [ZMOD n]
x : ℤ
hx : a - b = n * x
⊢ a * c ≡ b * d [ZMOD n]
Tactic:
obtain ⟨y, hy⟩ := h2
Proof state after:
case intro.intro
n a b c d x : ℤ
hx : a - b = n * x
y : ℤ
hy : c - d = n * y
⊢ a * c ≡ b * d [ZMOD n]
Theorem: BrownCs22.Int.ModEq.mul
Proof state before:
case intro.intro
n a b c d x : ℤ
hx : a - b = n * x
y : ℤ
hy : c - d = n * y
⊢ a * c ≡ b * d [ZMOD n]
Tactic:
exact ⟨x * c + b * y, by linear_combination c * hx + b * hy⟩
Proof state after:
no goals
Theorem: BrownCs22.Int.ModEq.mul
Proof state before:
n a b c d x : ℤ
hx : a - b = n * x
y : ℤ
hy : c - d = n * y
⊢ a * c - b * d = n * (x * c + b * y)
Tactic:
linear_combination c * hx + b * hy
Proof state after:
no goals
Theorem: BrownCs22.Int.ModEq.pow
Proof state before:
n a b : ℤ
k : ℕ
h : a ≡ b [ZMOD n]
⊢ a ^ k ≡ b ^ k [ZMOD n]
Tactic:
induction k
Proof state after:
case zero
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ a ^ Nat.zero ≡ b ^ Nat.zero [ZMOD n]

case succ
n a b : ℤ
h : a ≡ b [ZMOD n]
n✝ : ℕ
n_ih✝ : a ^ n✝ ≡ b ^ n✝ [ZMOD n]
⊢ a ^ Nat.succ n✝ ≡ b ^ Nat.succ n✝ [ZMOD n]
Theorem: BrownCs22.Int.ModEq.pow
Proof state before:
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ a ^ Nat.zero ≡ b ^ Nat.zero [ZMOD n]
Tactic:
case zero => exact Int.ModEq.refl _
Proof state after:
no goals
Theorem: BrownCs22.Int.ModEq.pow
Proof state before:
n a b : ℤ
h : a ≡ b [ZMOD n]
k : ℕ
hk : a ^ k ≡ b ^ k [ZMOD n]
⊢ a ^ Nat.succ k ≡ b ^ Nat.succ k [ZMOD n]
Tactic:
case succ k hk => exact Int.ModEq.mul hk h
Proof state after:
no goals
Theorem: BrownCs22.Int.ModEq.pow
Proof state before:
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ a ^ Nat.zero ≡ b ^ Nat.zero [ZMOD n]
Tactic:
exact Int.ModEq.refl _
Proof state after:
no goals
Theorem: BrownCs22.Int.ModEq.pow
Proof state before:
n a b : ℤ
h : a ≡ b [ZMOD n]
k : ℕ
hk : a ^ k ≡ b ^ k [ZMOD n]
⊢ a ^ Nat.succ k ≡ b ^ Nat.succ k [ZMOD n]
Tactic:
exact Int.ModEq.mul hk h
Proof state after:
no goals
Theorem: BrownCs22.Int.ModEq.symm
Proof state before:
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ b ≡ a [ZMOD n]
Tactic:
obtain ⟨x, hx⟩ := h
Proof state after:
case intro
n a b x : ℤ
hx : a - b = n * x
⊢ b ≡ a [ZMOD n]
Theorem: BrownCs22.Int.ModEq.symm
Proof state before:
case intro
n a b x : ℤ
hx : a - b = n * x
⊢ b ≡ a [ZMOD n]
Tactic:
exact ⟨-x, by linear_combination - hx⟩
Proof state after:
no goals
Theorem: BrownCs22.Int.ModEq.symm
Proof state before:
n a b x : ℤ
hx : a - b = n * x
⊢ b - a = n * -x
Tactic:
linear_combination - hx
Proof state after:
no goals
Theorem: BrownCs22.Int.ModEq.trans
Proof state before:
n a b c : ℤ
h1 : a ≡ b [ZMOD n]
h2 : b ≡ c [ZMOD n]
⊢ a ≡ c [ZMOD n]
Tactic:
obtain ⟨x, hx⟩ := h1
Proof state after:
case intro
n a b c : ℤ
h2 : b ≡ c [ZMOD n]
x : ℤ
hx : a - b = n * x
⊢ a ≡ c [ZMOD n]
Theorem: BrownCs22.Int.ModEq.trans
Proof state before:
case intro
n a b c : ℤ
h2 : b ≡ c [ZMOD n]
x : ℤ
hx : a - b = n * x
⊢ a ≡ c [ZMOD n]
Tactic:
obtain ⟨y, hy⟩ := h2
Proof state after:
case intro.intro
n a b c x : ℤ
hx : a - b = n * x
y : ℤ
hy : b - c = n * y
⊢ a ≡ c [ZMOD n]
Theorem: BrownCs22.Int.ModEq.trans
Proof state before:
case intro.intro
n a b c x : ℤ
hx : a - b = n * x
y : ℤ
hy : b - c = n * y
⊢ a ≡ c [ZMOD n]
Tactic:
exact ⟨x + y, by linear_combination hx + hy⟩
Proof state after:
no goals
Theorem: BrownCs22.Int.ModEq.trans
Proof state before:
n a b c x : ℤ
hx : a - b = n * x
y : ℤ
hy : b - c = n * y
⊢ a - c = n * (x + y)
Tactic:
linear_combination hx + hy
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_fac_zero
Proof state before:
n t : ℤ
⊢ n * t - 0 = n * t
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_fac_zero'
Proof state before:
n t : ℤ
⊢ t * n - 0 = n * t
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_zero_fac
Proof state before:
n t : ℤ
⊢ 0 - n * t = n * -t
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_zero_fac'
Proof state before:
n t : ℤ
⊢ 0 - t * n = n * -t
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_add_fac_self
Proof state before:
n a t : ℤ
⊢ a + n * t - a = n * t
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_add_fac_self'
Proof state before:
n t a : ℤ
⊢ n * t + a - a = n * t
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_add_fac_self''
Proof state before:
n a t : ℤ
⊢ a + t * n - a = n * t
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_add_fac_self'''
Proof state before:
n t a : ℤ
⊢ t * n + a - a = n * t
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_sub_fac_self
Proof state before:
n a t : ℤ
⊢ a - n * t - a = n * -t
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_sub_fac_self'
Proof state before:
n t a : ℤ
⊢ n * t - a - -a = n * t
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_sub_fac_self''
Proof state before:
n a t : ℤ
⊢ a - t * n - a = n * -t
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_sub_fac_self'''
Proof state before:
n t a : ℤ
⊢ t * n - a - -a = n * t
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_add_fac_self_symm
Proof state before:
n a t : ℤ
⊢ a - (a + n * t) = n * -t
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_add_fac_self_symm'
Proof state before:
n a t : ℤ
⊢ a - (n * t + a) = n * -t
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_add_fac_self_symm''
Proof state before:
n a t : ℤ
⊢ a - (a + t * n) = n * -t
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_add_fac_self_symm'''
Proof state before:
n a t : ℤ
⊢ a - (t * n + a) = n * -t
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_sub_fac_self_symm
Proof state before:
n a t : ℤ
⊢ a - (a - n * t) = n * t
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_sub_fac_self_symm'
Proof state before:
n a t : ℤ
⊢ -a - (n * t - a) = n * -t
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_sub_fac_self_symm''
Proof state before:
n a t : ℤ
⊢ a - (a - t * n) = n * t
Tactic:
ring
Proof state after:
no goals
Theorem: BrownCs22.Int.modEq_sub_fac_self_symm'''
Proof state before:
n a t : ℤ
⊢ -a - (t * n - a) = n * -t
Tactic:
ring
Proof state after:
no goals
Theorem: rsa_correct
Proof state before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
⊢ rsa_decrypt private_key (p * q) (rsa_encrypt public_key (p * q) message) = message
Tactic:
dsimp [rsa_decrypt, rsa_encrypt]
Proof state after:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
⊢ (message ^ public_key % (p * q)) ^ private_key % (p * q) = message
Theorem: rsa_correct
Proof state before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
⊢ (message ^ public_key % (p * q)) ^ private_key % (p * q) = message
Tactic:
have h_lin_combo : ∃ k, public_key * private_key = 1 + (p - 1)*(q - 1)*k := 
  sorry
Proof state after:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
h_lin_combo : ∃ k, public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ (message ^ public_key % (p * q)) ^ private_key % (p * q) = message
Theorem: rsa_correct
Proof state before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
h_lin_combo : ∃ k, public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ (message ^ public_key % (p * q)) ^ private_key % (p * q) = message
Tactic:
eliminate h_lin_combo with k hk
Proof state after:
case intro
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ (message ^ public_key % (p * q)) ^ private_key % (p * q) = message
Theorem: rsa_correct
Proof state before:
case intro
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ (message ^ public_key % (p * q)) ^ private_key % (p * q) = message
Tactic:
calc 
  (message ^ public_key % (p * q)) ^ private_key % (p * q) 
    = (message ^ public_key) ^ private_key % (p * q)      := by rw [← Nat.pow_mod]
  _ = message ^ (public_key * private_key) % (p * q)      := by rw [pow_mul] 
  _ = message ^ (1 + (p - 1)*(q - 1)*k) % (p * q)         := by rw [hk]
  _ = message ^ (1 + totient (p*q)*k) % (p * q)           := by sorry 
  _ = (message * (message ^ totient (p * q))^k) % (p * q) := by rw [pow_add, pow_one, pow_mul]
  _ = (message % (p * q)) * ((message ^ totient (p * q))^k % (p * q)) % (p * q) 
                                                          := by rw [Nat.mul_mod]
  _ = (message % (p * q)) * 1 % (p * q)                   := by sorry 
  _ = message % (p * q)                                   := by rw [mul_one, Nat.mod_mod]
  _ = message                                             := by rw [Nat.mod_eq_of_lt h_msg]
Proof state after:
no goals
Theorem: rsa_correct
Proof state before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ (message ^ public_key % (p * q)) ^ private_key % (p * q) = (message ^ public_key) ^ private_key % (p * q)
Tactic:
rw [← Nat.pow_mod]
Proof state after:
no goals
Theorem: rsa_correct
Proof state before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ (message ^ public_key) ^ private_key % (p * q) = message ^ (public_key * private_key) % (p * q)
Tactic:
rw [pow_mul]
Proof state after:
no goals
Theorem: rsa_correct
Proof state before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ message ^ (public_key * private_key) % (p * q) = message ^ (1 + (p - 1) * (q - 1) * k) % (p * q)
Tactic:
rw [hk]
Proof state after:
no goals
Theorem: rsa_correct
Proof state before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ message ^ (1 + (p - 1) * (q - 1) * k) % (p * q) = message ^ (1 + totient (p * q) * k) % (p * q)
Tactic:
sorry
Proof state after:
no goals
Theorem: rsa_correct
Proof state before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ message ^ (1 + totient (p * q) * k) % (p * q) = message * (message ^ totient (p * q)) ^ k % (p * q)
Tactic:
rw [pow_add, pow_one, pow_mul]
Proof state after:
no goals
Theorem: rsa_correct
Proof state before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ message * (message ^ totient (p * q)) ^ k % (p * q) =
    message % (p * q) * ((message ^ totient (p * q)) ^ k % (p * q)) % (p * q)
Tactic:
rw [Nat.mul_mod]
Proof state after:
no goals
Theorem: rsa_correct
Proof state before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ message % (p * q) * ((message ^ totient (p * q)) ^ k % (p * q)) % (p * q) = message % (p * q) * 1 % (p * q)
Tactic:
sorry
Proof state after:
no goals
Theorem: rsa_correct
Proof state before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ message % (p * q) * 1 % (p * q) = message % (p * q)
Tactic:
rw [mul_one, Nat.mod_mod]
Proof state after:
no goals
Theorem: rsa_correct
Proof state before:
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ message % (p * q) = message
Tactic:
rw [Nat.mod_eq_of_lt h_msg]
Proof state after:
no goals
Theorem: Hw7.problem_1
Proof state before:
a b c d : ℕ
⊢ a ≤ b → c < d → a + c < b + d
Tactic:
sorry
Proof state after:
no goals
Theorem: Hw7.problem_2
Proof state before:
a b c d e f : ℕ
⊢ a < b → c < d → e < f → a * c + e < b * d + f
Tactic:
sorry
Proof state after:
no goals
Theorem: Hw7.tri_formula
Proof state before:
⊢ ∀ (n : ℕ), 2 * tri_nums n = n * (n + 1)
Tactic:
basic_induction
Proof state after:
case a

⊢ 2 * tri_nums 0 = 0 * (0 + 1)

case a

⊢ ∀ (n : ℕ), 2 * tri_nums n = n * (n + 1) → 2 * tri_nums (n + 1) = (n + 1) * (n + 1 + 1)
Theorem: Hw7.tri_formula
Proof state before:
case a

⊢ 2 * tri_nums 0 = 0 * (0 + 1)

case a

⊢ ∀ (n : ℕ), 2 * tri_nums n = n * (n + 1) → 2 * tri_nums (n + 1) = (n + 1) * (n + 1 + 1)
Tactic:
{
  dsimp [tri_nums]
}
Proof state after:
case a

⊢ ∀ (n : ℕ), 2 * tri_nums n = n * (n + 1) → 2 * tri_nums (n + 1) = (n + 1) * (n + 1 + 1)
Theorem: Hw7.tri_formula
Proof state before:
case a

⊢ ∀ (n : ℕ), 2 * tri_nums n = n * (n + 1) → 2 * tri_nums (n + 1) = (n + 1) * (n + 1 + 1)
Tactic:
{
  intros n h
  dsimp [tri_nums]
  simp
  rewrite [Nat.left_distrib, h]
  linarith
}
Proof state after:
no goals
Theorem: Hw7.tri_formula
Proof state before:
case a

⊢ 2 * tri_nums 0 = 0 * (0 + 1)
Tactic:
dsimp [tri_nums]
Proof state after:
no goals
Theorem: Hw7.tri_formula
Proof state before:
case a

⊢ ∀ (n : ℕ), 2 * tri_nums n = n * (n + 1) → 2 * tri_nums (n + 1) = (n + 1) * (n + 1 + 1)
Tactic:
intros n h
Proof state after:
case a
n : ℕ
h : 2 * tri_nums n = n * (n + 1)
⊢ 2 * tri_nums (n + 1) = (n + 1) * (n + 1 + 1)
Theorem: Hw7.tri_formula
Proof state before:
case a
n : ℕ
h : 2 * tri_nums n = n * (n + 1)
⊢ 2 * tri_nums (n + 1) = (n + 1) * (n + 1 + 1)
Tactic:
dsimp [tri_nums]
Proof state after:
case a
n : ℕ
h : 2 * tri_nums n = n * (n + 1)
⊢ 2 * (tri_nums (n + 0) + (n + 0 + 1)) = (n + 1) * (n + 1 + 1)
Theorem: Hw7.tri_formula
Proof state before:
case a
n : ℕ
h : 2 * tri_nums n = n * (n + 1)
⊢ 2 * (tri_nums (n + 0) + (n + 0 + 1)) = (n + 1) * (n + 1 + 1)
Tactic:
simp
Proof state after:
case a
n : ℕ
h : 2 * tri_nums n = n * (n + 1)
⊢ 2 * (tri_nums n + (n + 1)) = (n + 1) * (n + 1 + 1)
Theorem: Hw7.tri_formula
Proof state before:
case a
n : ℕ
h : 2 * tri_nums n = n * (n + 1)
⊢ 2 * (tri_nums n + (n + 1)) = (n + 1) * (n + 1 + 1)
Tactic:
rewrite [Nat.left_distrib, h]
Proof state after:
case a
n : ℕ
h : 2 * tri_nums n = n * (n + 1)
⊢ n * (n + 1) + 2 * (n + 1) = (n + 1) * (n + 1 + 1)
Theorem: Hw7.tri_formula
Proof state before:
case a
n : ℕ
h : 2 * tri_nums n = n * (n + 1)
⊢ n * (n + 1) + 2 * (n + 1) = (n + 1) * (n + 1 + 1)
Tactic:
linarith
Proof state after:
no goals
Theorem: Hw7.square_formula
Proof state before:
⊢ ∀ (n : ℕ), recursive_square n = n * n
Tactic:
sorry
Proof state after:
no goals
Theorem: Hw7.zero_is_even
Proof state before:
⊢ MyEven 0
Tactic:
dsimp [MyEven]
Proof state after:
⊢ ∃ k, 2 * k = 0
Theorem: Hw7.zero_is_even
Proof state before:
⊢ ∃ k, 2 * k = 0
Tactic:
existsi 0
Proof state after:
⊢ 2 * 0 = 0
Theorem: Hw7.zero_is_even
Proof state before:
⊢ 2 * 0 = 0
Tactic:
numbers
Proof state after:
no goals