internlm/Lean-Github huggingface dataset:
Theorem: KolmogorovStreams.check_decent_words
Proof state before:
α : Type
is_decent : List α → Prop
a : Stream' α
hinit : all_prefixes is_decent a
hnot : ∀ (n : ℕ), ∃ k, 0 < k ∧ all_prefixes is_decent (Stream'.drop (n + k) a)
j : ℕ
⊢ is_decent
    (Stream'.get
      (fun i =>
        Stream'.take ((choose_decent_words is_decent a hinit hnot).get i).length
          (Stream'.drop ((choose_decent_words is_decent a hinit hnot).get i).start a))
      j)
Tactic:
exact ((choose_decent_words is_decent a hinit hnot).get j).h
Proof state after:
no goals
Theorem: KolmogorovStreams.not_all_prefixes
Proof state before:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ¬all_prefixes is_decent a
⊢ ∃ n, ¬is_decent (Stream'.take n.succ a)
Tactic:
simp[all_prefixes, Stream'.all_def] at h
Proof state after:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∃ x, ¬is_decent (Stream'.take (x + 1) a)
⊢ ∃ n, ¬is_decent (Stream'.take n.succ a)
Theorem: KolmogorovStreams.not_all_prefixes
Proof state before:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∃ x, ¬is_decent (Stream'.take (x + 1) a)
⊢ ∃ n, ¬is_decent (Stream'.take n.succ a)
Tactic:
exact h
Proof state after:
no goals
Theorem: KolmogorovStreams.chosen_indecent_closed_form
Proof state before:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
⊢ ∀ (n : ℕ),
    ((choose_indecent_words is_decent a h).get n).start =
      ∑ j ∈ Finset.range n, ((choose_indecent_words is_decent a h).get j).length
Tactic:
intro n
Proof state after:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
n : ℕ
⊢ ((choose_indecent_words is_decent a h).get n).start =
    ∑ j ∈ Finset.range n, ((choose_indecent_words is_decent a h).get j).length
Theorem: KolmogorovStreams.chosen_indecent_closed_form
Proof state before:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
n : ℕ
⊢ ((choose_indecent_words is_decent a h).get n).start =
    ∑ j ∈ Finset.range n, ((choose_indecent_words is_decent a h).get j).length
Tactic:
induction' n with n pn
Proof state after:
case zero
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
⊢ ((choose_indecent_words is_decent a h).get 0).start =
    ∑ j ∈ Finset.range 0, ((choose_indecent_words is_decent a h).get j).length

case succ
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
n : ℕ
pn :
  ((choose_indecent_words is_decent a h).get n).start =
    ∑ j ∈ Finset.range n, ((choose_indecent_words is_decent a h).get j).length
⊢ ((choose_indecent_words is_decent a h).get (n + 1)).start =
    ∑ j ∈ Finset.range (n + 1), ((choose_indecent_words is_decent a h).get j).length
Theorem: KolmogorovStreams.chosen_indecent_closed_form
Proof state before:
case zero
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
⊢ ((choose_indecent_words is_decent a h).get 0).start =
    ∑ j ∈ Finset.range 0, ((choose_indecent_words is_decent a h).get j).length
Tactic:
rfl
Proof state after:
no goals
Theorem: KolmogorovStreams.chosen_indecent_closed_form
Proof state before:
case succ
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
n : ℕ
pn :
  ((choose_indecent_words is_decent a h).get n).start =
    ∑ j ∈ Finset.range n, ((choose_indecent_words is_decent a h).get j).length
⊢ ((choose_indecent_words is_decent a h).get (n + 1)).start =
    ∑ j ∈ Finset.range (n + 1), ((choose_indecent_words is_decent a h).get j).length
Tactic:
rw [Finset.sum_range_succ, ← pn]
Proof state after:
case succ
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
n : ℕ
pn :
  ((choose_indecent_words is_decent a h).get n).start =
    ∑ j ∈ Finset.range n, ((choose_indecent_words is_decent a h).get j).length
⊢ ((choose_indecent_words is_decent a h).get (n + 1)).start =
    ((choose_indecent_words is_decent a h).get n).start + ((choose_indecent_words is_decent a h).get n).length
Theorem: KolmogorovStreams.chosen_indecent_closed_form
Proof state before:
case succ
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
n : ℕ
pn :
  ((choose_indecent_words is_decent a h).get n).start =
    ∑ j ∈ Finset.range n, ((choose_indecent_words is_decent a h).get j).length
⊢ ((choose_indecent_words is_decent a h).get (n + 1)).start =
    ((choose_indecent_words is_decent a h).get n).start + ((choose_indecent_words is_decent a h).get n).length
Tactic:
rfl
Proof state after:
no goals
Theorem: KolmogorovStreams.check_indecent_words
Proof state before:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
⊢ Stream'.All (fun x => ¬is_decent x)
    (break_into_words (fun i => ((choose_indecent_words is_decent a h).get i).length) a)
Tactic:
rw [break_into_words_closed_form]
Proof state after:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
⊢ Stream'.All (fun x => ¬is_decent x) fun i =>
    Stream'.take ((choose_indecent_words is_decent a h).get i).length
      (Stream'.drop (∑ j ∈ Finset.range i, ((choose_indecent_words is_decent a h).get j).length) a)
Theorem: KolmogorovStreams.check_indecent_words
Proof state before:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
⊢ Stream'.All (fun x => ¬is_decent x) fun i =>
    Stream'.take ((choose_indecent_words is_decent a h).get i).length
      (Stream'.drop (∑ j ∈ Finset.range i, ((choose_indecent_words is_decent a h).get j).length) a)
Tactic:
simp_rw [←chosen_indecent_closed_form]
Proof state after:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
⊢ Stream'.All (fun x => ¬is_decent x) fun i =>
    Stream'.take ((choose_indecent_words is_decent a h).get i).length
      (Stream'.drop ((choose_indecent_words is_decent a h).get i).start a)
Theorem: KolmogorovStreams.check_indecent_words
Proof state before:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
⊢ Stream'.All (fun x => ¬is_decent x) fun i =>
    Stream'.take ((choose_indecent_words is_decent a h).get i).length
      (Stream'.drop ((choose_indecent_words is_decent a h).get i).start a)
Tactic:
intro j
Proof state after:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
j : ℕ
⊢ ¬is_decent
      (Stream'.get
        (fun i =>
          Stream'.take ((choose_indecent_words is_decent a h).get i).length
            (Stream'.drop ((choose_indecent_words is_decent a h).get i).start a))
        j)
Theorem: KolmogorovStreams.check_indecent_words
Proof state before:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
j : ℕ
⊢ ¬is_decent
      (Stream'.get
        (fun i =>
          Stream'.take ((choose_indecent_words is_decent a h).get i).length
            (Stream'.drop ((choose_indecent_words is_decent a h).get i).start a))
        j)
Tactic:
exact ((choose_indecent_words is_decent a h).get j).h
Proof state after:
no goals
Theorem: Imo1962P2.lemma1
Proof state before:
x : ℝ
⊢ (15 / 8) ^ 2 - (3 - x) * (x + 1) = (x - (1 + √31 / 8)) * (x - (1 - √31 / 8))
Tactic:
have h1 : Real.sqrt 31 ^ 2 = 31 := Real.sq_sqrt (Nat.ofNat_nonneg _)
Proof state after:
x : ℝ
h1 : √31 ^ 2 = 31
⊢ (15 / 8) ^ 2 - (3 - x) * (x + 1) = (x - (1 + √31 / 8)) * (x - (1 - √31 / 8))
Theorem: Imo1962P2.lemma1
Proof state before:
x : ℝ
h1 : √31 ^ 2 = 31
⊢ (15 / 8) ^ 2 - (3 - x) * (x + 1) = (x - (1 + √31 / 8)) * (x - (1 - √31 / 8))
Tactic:
ring_nf
Proof state after:
x : ℝ
h1 : √31 ^ 2 = 31
⊢ 33 / 64 - x * 2 + x ^ 2 = 1 - x * 2 + x ^ 2 + √31 ^ 2 * (-1 / 64)
Theorem: Imo1962P2.lemma1
Proof state before:
x : ℝ
h1 : √31 ^ 2 = 31
⊢ 33 / 64 - x * 2 + x ^ 2 = 1 - x * 2 + x ^ 2 + √31 ^ 2 * (-1 / 64)
Tactic:
rw [h1]
Proof state after:
x : ℝ
h1 : √31 ^ 2 = 31
⊢ 33 / 64 - x * 2 + x ^ 2 = 1 - x * 2 + x ^ 2 + 31 * (-1 / 64)
Theorem: Imo1962P2.lemma1
Proof state before:
x : ℝ
h1 : √31 ^ 2 = 31
⊢ 33 / 64 - x * 2 + x ^ 2 = 1 - x * 2 + x ^ 2 + 31 * (-1 / 64)
Tactic:
ring
Proof state after:
no goals
Theorem: Imo1962P2.lemma2
Proof state before:
x : ℝ
hx4 : 0 ≤ 3 - x
hx5 : 0 ≤ x + 1
⊢ √(3 - x) ^ 2 - 2 * √(3 - x) * √(x + 1) + √(x + 1) ^ 2 = 3 - x - 2 * √(3 - x) * √(x + 1) + (x + 1)
Tactic:
rw [Real.sq_sqrt hx4, add_left_cancel_iff, Real.sq_sqrt hx5]
Proof state after:
no goals
Theorem: Imo1962P2.lemma2
Proof state before:
x : ℝ
hx4 : 0 ≤ 3 - x
hx5 : 0 ≤ x + 1
⊢ 3 - x - 2 * √(3 - x) * √(x + 1) + (x + 1) = 4 - 2 * (√(3 - x) * √(x + 1))
Tactic:
ring
Proof state after:
no goals
Theorem: Imo1962P2.lemma2
Proof state before:
x : ℝ
hx4 : 0 ≤ 3 - x
hx5 : 0 ≤ x + 1
⊢ 4 - 2 * (√(3 - x) * √(x + 1)) = 4 - 2 * √((3 - x) * (x + 1))
Tactic:
rw[←Real.sqrt_mul hx4]
Proof state after:
no goals
Theorem: Usa2003P1.nat_mod_inv
Proof state before:
a : ℕ
⊢ ∃ b, (a + b) % 5 = 0
Tactic:
use 5 - (a % 5)
Proof state after:
case h
a : ℕ
⊢ (a + (5 - a % 5)) % 5 = 0
Theorem: Usa2003P1.nat_mod_inv
Proof state before:
case h
a : ℕ
⊢ (a + (5 - a % 5)) % 5 = 0
Tactic:
have h : a % 5 < 5 := Nat.mod_lt _ (by norm_num)
Proof state after:
case h
a : ℕ
h : a % 5 < 5
⊢ (a + (5 - a % 5)) % 5 = 0
Theorem: Usa2003P1.nat_mod_inv
Proof state before:
case h
a : ℕ
h : a % 5 < 5
⊢ (a + (5 - a % 5)) % 5 = 0
Tactic:
have h' : a % 5 ≤ 5 := Nat.le_of_lt h
Proof state after:
case h
a : ℕ
h : a % 5 < 5
h' : a % 5 ≤ 5
⊢ (a + (5 - a % 5)) % 5 = 0
Theorem: Usa2003P1.nat_mod_inv
Proof state before:
case h
a : ℕ
h : a % 5 < 5
h' : a % 5 ≤ 5
⊢ (a + (5 - a % 5)) % 5 = 0
Tactic:
rw[Nat.add_mod]
Proof state after:
case h
a : ℕ
h : a % 5 < 5
h' : a % 5 ≤ 5
⊢ (a % 5 + (5 - a % 5) % 5) % 5 = 0
Theorem: Usa2003P1.nat_mod_inv
Proof state before:
case h
a : ℕ
h : a % 5 < 5
h' : a % 5 ≤ 5
⊢ (a % 5 + (5 - a % 5) % 5) % 5 = 0
Tactic:
have h2 : a % 5 = a % 5 % 5 := (Nat.mod_mod a 5).symm
Proof state after:
case h
a : ℕ
h : a % 5 < 5
h' : a % 5 ≤ 5
h2 : a % 5 = a % 5 % 5
⊢ (a % 5 + (5 - a % 5) % 5) % 5 = 0
Theorem: Usa2003P1.nat_mod_inv
Proof state before:
case h
a : ℕ
h : a % 5 < 5
h' : a % 5 ≤ 5
h2 : a % 5 = a % 5 % 5
⊢ (a % 5 + (5 - a % 5) % 5) % 5 = 0
Tactic:
rw[h2, ← Nat.add_mod, Nat.mod_mod]
Proof state after:
case h
a : ℕ
h : a % 5 < 5
h' : a % 5 ≤ 5
h2 : a % 5 = a % 5 % 5
⊢ (a % 5 + (5 - a % 5)) % 5 = 0
Theorem: Usa2003P1.nat_mod_inv
Proof state before:
case h
a : ℕ
h : a % 5 < 5
h' : a % 5 ≤ 5
h2 : a % 5 = a % 5 % 5
⊢ (a % 5 + (5 - a % 5)) % 5 = 0
Tactic:
rw[Nat.add_sub_of_le h']
Proof state after:
no goals
Theorem: Usa2003P1.nat_mod_inv
Proof state before:
a : ℕ
⊢ 5 > 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Usa2003P1.lemma2
Proof state before:
a b c : ℕ
hb : 0 < b
h : a.Coprime b
⊢ ∃ k < b, a * k ≡ c [MOD b]
Tactic:
let ⟨N, HN1, HN2⟩ := Nat.chineseRemainder h 0 c
Proof state after:
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
⊢ ∃ k < b, a * k ≡ c [MOD b]
Theorem: Usa2003P1.lemma2
Proof state before:
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
⊢ ∃ k < b, a * k ≡ c [MOD b]
Tactic:
have ⟨x, hx⟩ : a ∣ N := Nat.modEq_zero_iff_dvd.mp HN1
Proof state after:
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
x : ℕ
hx : N = a * x
⊢ ∃ k < b, a * k ≡ c [MOD b]
Theorem: Usa2003P1.lemma2
Proof state before:
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
x : ℕ
hx : N = a * x
⊢ ∃ k < b, a * k ≡ c [MOD b]
Tactic:
use x % b
Proof state after:
case h
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
x : ℕ
hx : N = a * x
⊢ x % b < b ∧ a * (x % b) ≡ c [MOD b]
Theorem: Usa2003P1.lemma2
Proof state before:
case h
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
x : ℕ
hx : N = a * x
⊢ x % b < b ∧ a * (x % b) ≡ c [MOD b]
Tactic:
constructor
Proof state after:
case h.left
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
x : ℕ
hx : N = a * x
⊢ x % b < b

case h.right
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
x : ℕ
hx : N = a * x
⊢ a * (x % b) ≡ c [MOD b]
Theorem: Usa2003P1.lemma2
Proof state before:
case h.left
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
x : ℕ
hx : N = a * x
⊢ x % b < b
Tactic:
exact Nat.mod_lt _ hb
Proof state after:
no goals
Theorem: Usa2003P1.lemma2
Proof state before:
case h.right
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
HN2 : N ≡ c [MOD b]
x : ℕ
hx : N = a * x
⊢ a * (x % b) ≡ c [MOD b]
Tactic:
change N % b = c % b at HN2
Proof state after:
case h.right
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
x : ℕ
hx : N = a * x
HN2 : N % b = c % b
⊢ a * (x % b) ≡ c [MOD b]
Theorem: Usa2003P1.lemma2
Proof state before:
case h.right
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
x : ℕ
hx : N = a * x
HN2 : N % b = c % b
⊢ a * (x % b) ≡ c [MOD b]
Tactic:
change (a * (x % b)) % b = c % b
Proof state after:
case h.right
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
x : ℕ
hx : N = a * x
HN2 : N % b = c % b
⊢ a * (x % b) % b = c % b
Theorem: Usa2003P1.lemma2
Proof state before:
case h.right
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
x : ℕ
hx : N = a * x
HN2 : N % b = c % b
⊢ a * (x % b) % b = c % b
Tactic:
rw [← HN2, hx, Nat.mul_mod, Nat.mod_mod, ←Nat.mul_mod]
Proof state after:
no goals
Theorem: Usa2003P1.prime_five
Proof state before:
⊢ Nat.Prime 5
Tactic:
norm_num
Proof state after:
no goals
Theorem: Imo1962P4.cos_sum_equiv
Proof state before:
x : ℝ
⊢ (x.cos ^ 2 + (2 * x).cos ^ 2 + (3 * x).cos ^ 2 - 1) / 4 = altFormula x
Tactic:
simp only [Real.cos_two_mul, cos_three_mul, altFormula]
Proof state after:
x : ℝ
⊢ (x.cos ^ 2 + (2 * x.cos ^ 2 - 1) ^ 2 + (4 * x.cos ^ 3 - 3 * x.cos) ^ 2 - 1) / 4 =
    x.cos * (x.cos ^ 2 - 1 / 2) * (4 * x.cos ^ 3 - 3 * x.cos)
Theorem: Imo1962P4.cos_sum_equiv
Proof state before:
x : ℝ
⊢ (x.cos ^ 2 + (2 * x.cos ^ 2 - 1) ^ 2 + (4 * x.cos ^ 3 - 3 * x.cos) ^ 2 - 1) / 4 =
    x.cos * (x.cos ^ 2 - 1 / 2) * (4 * x.cos ^ 3 - 3 * x.cos)
Tactic:
ring
Proof state after:
no goals
Theorem: Imo1962P4.alt_equiv
Proof state before:
x : ℝ
⊢ ProblemEquation x ↔ altFormula x = 0
Tactic:
rw [ProblemEquation, ← cos_sum_equiv, div_eq_zero_iff, sub_eq_zero]
Proof state after:
x : ℝ
⊢ x.cos ^ 2 + (2 * x).cos ^ 2 + (3 * x).cos ^ 2 = 1 ↔ x.cos ^ 2 + (2 * x).cos ^ 2 + (3 * x).cos ^ 2 = 1 ∨ 4 = 0
Theorem: Imo1962P4.alt_equiv
Proof state before:
x : ℝ
⊢ x.cos ^ 2 + (2 * x).cos ^ 2 + (3 * x).cos ^ 2 = 1 ↔ x.cos ^ 2 + (2 * x).cos ^ 2 + (3 * x).cos ^ 2 = 1 ∨ 4 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Imo1962P4.finding_zeros
Proof state before:
x : ℝ
⊢ altFormula x = 0 ↔ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
Tactic:
simp only [altFormula, mul_assoc, mul_eq_zero, sub_eq_zero]
Proof state after:
x : ℝ
⊢ x.cos = 0 ∨ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0 ↔ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
Theorem: Imo1962P4.finding_zeros
Proof state before:
x : ℝ
⊢ x.cos = 0 ∨ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0 ↔ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
Tactic:
constructor
Proof state after:
case mp
x : ℝ
⊢ x.cos = 0 ∨ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0 → x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0

case mpr
x : ℝ
⊢ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0 → x.cos = 0 ∨ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
Theorem: Imo1962P4.finding_zeros
Proof state before:
case mp
x : ℝ
⊢ x.cos = 0 ∨ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0 → x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
Tactic:
rintro (h1 | h2)
Proof state after:
case mp.inl
x : ℝ
h1 : x.cos = 0
⊢ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0

case mp.inr
x : ℝ
h2 : x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
⊢ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
Theorem: Imo1962P4.finding_zeros
Proof state before:
case mp.inl
x : ℝ
h1 : x.cos = 0
⊢ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
Tactic:
right
Proof state after:
case mp.inl.h
x : ℝ
h1 : x.cos = 0
⊢ (3 * x).cos = 0
Theorem: Imo1962P4.finding_zeros
Proof state before:
case mp.inl.h
x : ℝ
h1 : x.cos = 0
⊢ (3 * x).cos = 0
Tactic:
rw [cos_three_mul, h1]
Proof state after:
case mp.inl.h
x : ℝ
h1 : x.cos = 0
⊢ 4 * 0 ^ 3 - 3 * 0 = 0
Theorem: Imo1962P4.finding_zeros
Proof state before:
case mp.inl.h
x : ℝ
h1 : x.cos = 0
⊢ 4 * 0 ^ 3 - 3 * 0 = 0
Tactic:
ring
Proof state after:
no goals
Theorem: Imo1962P4.finding_zeros
Proof state before:
case mp.inr
x : ℝ
h2 : x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
⊢ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
Tactic:
exact h2
Proof state after:
no goals
Theorem: Imo1962P4.finding_zeros
Proof state before:
case mpr
x : ℝ
⊢ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0 → x.cos = 0 ∨ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
Tactic:
exact Or.inr
Proof state after:
no goals
Theorem: Imo1962P4.solve_cos2_half
Proof state before:
x : ℝ
⊢ x.cos ^ 2 = 1 / 2 ↔ ∃ k, x = (2 * ↑k + 1) * π / 4
Tactic:
rw [cos_sq]
Proof state after:
x : ℝ
⊢ 1 / 2 + (2 * x).cos / 2 = 1 / 2 ↔ ∃ k, x = (2 * ↑k + 1) * π / 4
Theorem: Imo1962P4.solve_cos2_half
Proof state before:
x : ℝ
⊢ 1 / 2 + (2 * x).cos / 2 = 1 / 2 ↔ ∃ k, x = (2 * ↑k + 1) * π / 4
Tactic:
simp only [add_right_eq_self, div_eq_zero_iff]
Proof state after:
x : ℝ
⊢ (2 * x).cos = 0 ∨ 2 = 0 ↔ ∃ k, x = (2 * ↑k + 1) * π / 4
Theorem: Imo1962P4.solve_cos2_half
Proof state before:
x : ℝ
⊢ (2 * x).cos = 0 ∨ 2 = 0 ↔ ∃ k, x = (2 * ↑k + 1) * π / 4
Tactic:
norm_num
Proof state after:
x : ℝ
⊢ (2 * x).cos = 0 ↔ ∃ k, x = (2 * ↑k + 1) * π / 4
Theorem: Imo1962P4.solve_cos2_half
Proof state before:
x : ℝ
⊢ (2 * x).cos = 0 ↔ ∃ k, x = (2 * ↑k + 1) * π / 4
Tactic:
rw [cos_eq_zero_iff]
Proof state after:
x : ℝ
⊢ (∃ k, 2 * x = (2 * ↑k + 1) * π / 2) ↔ ∃ k, x = (2 * ↑k + 1) * π / 4
Theorem: Imo1962P4.solve_cos2_half
Proof state before:
case mpr
x : ℝ
⊢ (∃ k, x = (2 * ↑k + 1) * π / 4) → ∃ k, 2 * x = (2 * ↑k + 1) * π / 2
Tactic:
rintro ⟨k, h⟩
Proof state after:
case mpr.intro
x : ℝ
k : ℤ
h : x = (2 * ↑k + 1) * π / 4
⊢ ∃ k, 2 * x = (2 * ↑k + 1) * π / 2
Theorem: Imo1962P4.solve_cos2_half
Proof state before:
case mpr.intro
x : ℝ
k : ℤ
h : x = (2 * ↑k + 1) * π / 4
⊢ ∃ k, 2 * x = (2 * ↑k + 1) * π / 2
Tactic:
use k
Proof state after:
case h
x : ℝ
k : ℤ
h : x = (2 * ↑k + 1) * π / 4
⊢ 2 * x = (2 * ↑k + 1) * π / 2
Theorem: Imo1962P4.solve_cos2_half
Proof state before:
case h
x : ℝ
k : ℤ
h : x = (2 * ↑k + 1) * π / 4
⊢ 2 * x = (2 * ↑k + 1) * π / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1962P4.solve_cos3x_0
Proof state before:
x : ℝ
⊢ (3 * x).cos = 0 ↔ ∃ k, x = (2 * ↑k + 1) * π / 6
Tactic:
rw [cos_eq_zero_iff]
Proof state after:
x : ℝ
⊢ (∃ k, 3 * x = (2 * ↑k + 1) * π / 2) ↔ ∃ k, x = (2 * ↑k + 1) * π / 6
Theorem: Imo1962P4.solve_cos3x_0
Proof state before:
x : ℝ
⊢ (∃ k, 3 * x = (2 * ↑k + 1) * π / 2) ↔ ∃ k, x = (2 * ↑k + 1) * π / 6
Tactic:
refine exists_congr fun k => ?_
Proof state after:
x : ℝ
k : ℤ
⊢ 3 * x = (2 * ↑k + 1) * π / 2 ↔ x = (2 * ↑k + 1) * π / 6
Theorem: Imo1962P4.solve_cos3x_0
Proof state before:
x : ℝ
k : ℤ
⊢ 3 * x = (2 * ↑k + 1) * π / 2 ↔ x = (2 * ↑k + 1) * π / 6
Tactic:
constructor <;> intro <;> linarith
Proof state after:
no goals
Theorem: Imo2019P1.additive_to_int_linear
Proof state before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x + y) = f x + f y
⊢ ∃ c, ∀ (a : ℤ), f a = c * a
Tactic:
let g := AddMonoidHom.toIntLinearMap <| AddMonoidHom.mk' f h
Proof state after:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x + y) = f x + f y
g : ℤ →ₗ[ℤ] ℤ := (AddMonoidHom.mk' f h).toIntLinearMap
⊢ ∃ c, ∀ (a : ℤ), f a = c * a
Theorem: Imo2019P1.additive_to_int_linear
Proof state before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x + y) = f x + f y
g : ℤ →ₗ[ℤ] ℤ := (AddMonoidHom.mk' f h).toIntLinearMap
⊢ ∃ c, ∀ (a : ℤ), f a = c * a
Tactic:
refine ⟨f 1, fun a => ?_⟩
Proof state after:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x + y) = f x + f y
g : ℤ →ₗ[ℤ] ℤ := (AddMonoidHom.mk' f h).toIntLinearMap
a : ℤ
⊢ f a = f 1 * a
Theorem: Imo2019P1.additive_to_int_linear
Proof state before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x + y) = f x + f y
g : ℤ →ₗ[ℤ] ℤ := (AddMonoidHom.mk' f h).toIntLinearMap
a : ℤ
⊢ f a = f 1 * a
Tactic:
change g a = g 1 * a
Proof state after:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x + y) = f x + f y
g : ℤ →ₗ[ℤ] ℤ := (AddMonoidHom.mk' f h).toIntLinearMap
a : ℤ
⊢ g a = g 1 * a
Theorem: Imo2019P1.additive_to_int_linear
Proof state before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x + y) = f x + f y
g : ℤ →ₗ[ℤ] ℤ := (AddMonoidHom.mk' f h).toIntLinearMap
a : ℤ
⊢ g a = g 1 * a
Tactic:
rw [mul_comm, ← smul_eq_mul, ← LinearMap.map_smul, smul_eq_mul, mul_one]
Proof state after:
no goals
Theorem: Imo2008P4.positive_pow_eq_pow
Proof state before:
n : ℕ
h : 0 < n
a b : PosReal
⊢ a ^ n = b ^ n ↔ a = b
Tactic:
rw [← Subtype.coe_inj, Positive.val_pow, ← Subtype.coe_inj, Positive.val_pow]
Proof state after:
n : ℕ
h : 0 < n
a b : PosReal
⊢ ↑a ^ n = ↑b ^ n ↔ ↑a = ↑b
Theorem: Imo2008P4.positive_pow_eq_pow
Proof state before:
n : ℕ
h : 0 < n
a b : PosReal
⊢ ↑a ^ n = ↑b ^ n ↔ ↑a = ↑b
Tactic:
exact pow_left_inj (le_of_lt a.2) (le_of_lt b.2) (Nat.ne_of_gt h)
Proof state after:
no goals
Theorem: Imo2008P4.PosReal.mul_two
Proof state before:
x : PosReal
⊢ x * ⟨2, ⋯⟩ = x + x
Tactic:
obtain ⟨x, hx⟩ := x
Proof state after:
case mk
x : ℝ
hx : 0 < x
⊢ ⟨x, hx⟩ * ⟨2, ⋯⟩ = ⟨x, hx⟩ + ⟨x, hx⟩
Theorem: Imo2008P4.PosReal.mul_two
Proof state before:
case mk
x : ℝ
hx : 0 < x
⊢ ⟨x, hx⟩ * ⟨2, ⋯⟩ = ⟨x, hx⟩ + ⟨x, hx⟩
Tactic:
rw [Subtype.ext_iff]
Proof state after:
case mk
x : ℝ
hx : 0 < x
⊢ ↑(⟨x, hx⟩ * ⟨2, ⋯⟩) = ↑(⟨x, hx⟩ + ⟨x, hx⟩)
Theorem: Imo2008P4.PosReal.mul_two
Proof state before:
case mk
x : ℝ
hx : 0 < x
⊢ ↑(⟨x, hx⟩ * ⟨2, ⋯⟩) = ↑(⟨x, hx⟩ + ⟨x, hx⟩)
Tactic:
simp [_root_.mul_two]
Proof state after:
no goals
Theorem: Imo2008P4.PosReal.two_mul
Proof state before:
x : PosReal
⊢ ⟨2, ⋯⟩ * x = x + x
Tactic:
obtain ⟨x, hx⟩ := x
Proof state after:
case mk
x : ℝ
hx : 0 < x
⊢ ⟨2, ⋯⟩ * ⟨x, hx⟩ = ⟨x, hx⟩ + ⟨x, hx⟩
Theorem: Imo2008P4.PosReal.two_mul
Proof state before:
case mk
x : ℝ
hx : 0 < x
⊢ ⟨2, ⋯⟩ * ⟨x, hx⟩ = ⟨x, hx⟩ + ⟨x, hx⟩
Tactic:
rw [Subtype.ext_iff]
Proof state after:
case mk
x : ℝ
hx : 0 < x
⊢ ↑(⟨2, ⋯⟩ * ⟨x, hx⟩) = ↑(⟨x, hx⟩ + ⟨x, hx⟩)
Theorem: Imo2008P4.PosReal.two_mul
Proof state before:
case mk
x : ℝ
hx : 0 < x
⊢ ↑(⟨2, ⋯⟩ * ⟨x, hx⟩) = ↑(⟨x, hx⟩ + ⟨x, hx⟩)
Tactic:
simp [_root_.two_mul]
Proof state after:
no goals
Theorem: Imo1959P1.calculation
Proof state before:
n k : ℕ
h1 : k ∣ 21 * n + 4
h2 : k ∣ 14 * n + 3
⊢ k ∣ 1
Tactic:
have h3 : k ∣ 2 * (21 * n + 4) := h1.mul_left 2
Proof state after:
n k : ℕ
h1 : k ∣ 21 * n + 4
h2 : k ∣ 14 * n + 3
h3 : k ∣ 2 * (21 * n + 4)
⊢ k ∣ 1
Theorem: Imo1959P1.calculation
Proof state before:
n k : ℕ
h1 : k ∣ 21 * n + 4
h2 : k ∣ 14 * n + 3
h3 : k ∣ 2 * (21 * n + 4)
⊢ k ∣ 1
Tactic:
have h4 : k ∣ 3 * (14 * n + 3) := h2.mul_left 3
Proof state after:
n k : ℕ
h1 : k ∣ 21 * n + 4
h2 : k ∣ 14 * n + 3
h3 : k ∣ 2 * (21 * n + 4)
h4 : k ∣ 3 * (14 * n + 3)
⊢ k ∣ 1
Theorem: Imo1959P1.calculation
Proof state before:
n k : ℕ
h1 : k ∣ 21 * n + 4
h2 : k ∣ 14 * n + 3
h3 : k ∣ 2 * (21 * n + 4)
h4 : k ∣ 3 * (14 * n + 3)
⊢ k ∣ 1
Tactic:
have h5 : 3 * (14 * n + 3) = 2 * (21 * n + 4) + 1 := by ring
Proof state after:
n k : ℕ
h1 : k ∣ 21 * n + 4
h2 : k ∣ 14 * n + 3
h3 : k ∣ 2 * (21 * n + 4)
h4 : k ∣ 3 * (14 * n + 3)
h5 : 3 * (14 * n + 3) = 2 * (21 * n + 4) + 1
⊢ k ∣ 1
Theorem: Imo1959P1.calculation
Proof state before:
n k : ℕ
h1 : k ∣ 21 * n + 4
h2 : k ∣ 14 * n + 3
h3 : k ∣ 2 * (21 * n + 4)
h4 : k ∣ 3 * (14 * n + 3)
h5 : 3 * (14 * n + 3) = 2 * (21 * n + 4) + 1
⊢ k ∣ 1
Tactic:
exact (Nat.dvd_add_right h3).mp (h5 ▸ h4)
Proof state after:
no goals
Theorem: Imo1959P1.calculation
Proof state before:
n k : ℕ
h1 : k ∣ 21 * n + 4
h2 : k ∣ 14 * n + 3
h3 : k ∣ 2 * (21 * n + 4)
h4 : k ∣ 3 * (14 * n + 3)
⊢ 3 * (14 * n + 3) = 2 * (21 * n + 4) + 1
Tactic:
ring
Proof state after:
no goals
Theorem: Usa2002P1.Finset.subtype_union
Proof state before:
α : Type u_1
p : α → Prop
inst✝¹ : DecidableEq α
inst✝ : DecidablePred p
s1 s2 : Finset α
⊢ Finset.subtype p (s1 ∪ s2) = Finset.subtype p s1 ∪ Finset.subtype p s2
Tactic:
ext a
Proof state after:
case a
α : Type u_1
p : α → Prop
inst✝¹ : DecidableEq α
inst✝ : DecidablePred p
s1 s2 : Finset α
a : Subtype p
⊢ a ∈ Finset.subtype p (s1 ∪ s2) ↔ a ∈ Finset.subtype p s1 ∪ Finset.subtype p s2