internlm/Lean-Github huggingface dataset:
Theorem: Usa1998P3.lemma2
Proof state before:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h3 :
  ∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j =
    ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
h4 :
  ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) =
    (∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) ^ (n + 1)
⊢ (∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)) *
      ∏ j ∈ Finset.range (n + 1), f j =
    ((∏ x ∈ Finset.range (n + 1), f x ^ ↑n) * ∏ x ∈ Finset.range (n + 1), f x) * f (n + 1) ^ ↑n.succ
Tactic:
rw [h4, ih, mul_right_comm]
Proof state after:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h3 :
  ∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j =
    ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
h4 :
  ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) =
    (∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) ^ (n + 1)
⊢ ((∏ i ∈ Finset.range (n + 1), f i ^ ↑n) * ∏ j ∈ Finset.range (n + 1), f j) * f (n + 1) ^ (n + 1) =
    ((∏ x ∈ Finset.range (n + 1), f x ^ ↑n) * ∏ x ∈ Finset.range (n + 1), f x) * f (n + 1) ^ ↑n.succ
Theorem: Usa1998P3.lemma2
Proof state before:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h3 :
  ∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j =
    ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
h4 :
  ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) =
    (∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) ^ (n + 1)
⊢ ((∏ i ∈ Finset.range (n + 1), f i ^ ↑n) * ∏ j ∈ Finset.range (n + 1), f j) * f (n + 1) ^ (n + 1) =
    ((∏ x ∈ Finset.range (n + 1), f x ^ ↑n) * ∏ x ∈ Finset.range (n + 1), f x) * f (n + 1) ^ ↑n.succ
Tactic:
norm_cast
Proof state after:
no goals
Theorem: Usa1998P3.lemma2
Proof state before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ ∏ i ∈ Finset.range (n.succ + 1), f i ^ ↑n.succ = (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ
Tactic:
rw [Finset.prod_range_succ]
Proof state after:
no goals
Theorem: Usa1998P3.lemma2
Proof state before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ ∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n * f i
Tactic:
congr
Proof state after:
case e_f
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ (fun i => f i ^ ↑n.succ) = fun i => f i ^ ↑n * f i
Theorem: Usa1998P3.lemma2
Proof state before:
case e_f
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ (fun i => f i ^ ↑n.succ) = fun i => f i ^ ↑n * f i
Tactic:
funext x
Proof state after:
case e_f.h
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
⊢ f x ^ ↑n.succ = f x ^ ↑n * f x
Theorem: Usa1998P3.lemma2
Proof state before:
case e_f.h
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
⊢ f x ^ ↑n.succ = f x ^ ↑n * f x
Tactic:
norm_cast
Proof state after:
no goals
Theorem: Usa1998P3.lemma2
Proof state before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ ∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j =
    ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
Tactic:
apply Finset.prod_congr rfl
Proof state after:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ ∀ x ∈ Finset.range (n + 1),
    ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j = (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
Theorem: Usa1998P3.lemma2
Proof state before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ ∀ x ∈ Finset.range (n + 1),
    ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j = (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
Tactic:
intro x hx
Proof state after:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
⊢ ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j = (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
Theorem: Usa1998P3.lemma2
Proof state before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
⊢ ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j = (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
Tactic:
have h7' : (n + 1) ∉ (Finset.erase (Finset.range (n + 1)) x) := by simp_all
Proof state after:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
⊢ ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j = (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
Theorem: Usa1998P3.lemma2
Proof state before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
h7 : (Finset.range (n.succ + 1)).erase x = insert (n + 1) ((Finset.range (n + 1)).erase x)
⊢ ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j = (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
Tactic:
rw [h7, Finset.prod_insert h7']
Proof state after:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
h7 : (Finset.range (n.succ + 1)).erase x = insert (n + 1) ((Finset.range (n + 1)).erase x)
⊢ f (n + 1) * ∏ x ∈ (Finset.range (n + 1)).erase x, f x = (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
Theorem: Usa1998P3.lemma2
Proof state before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
h7 : (Finset.range (n.succ + 1)).erase x = insert (n + 1) ((Finset.range (n + 1)).erase x)
⊢ f (n + 1) * ∏ x ∈ (Finset.range (n + 1)).erase x, f x = (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: Usa1998P3.lemma2
Proof state before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
⊢ n + 1 ∉ (Finset.range (n + 1)).erase x
Tactic:
simp_all
Proof state after:
no goals
Theorem: Usa1998P3.lemma2
Proof state before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
⊢ (Finset.range (n.succ + 1)).erase x = insert (n + 1) ((Finset.range (n + 1)).erase x)
Tactic:
ext y
Proof state after:
case a
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
⊢ y ∈ (Finset.range (n.succ + 1)).erase x ↔ y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)
Theorem: Usa1998P3.lemma2
Proof state before:
case a
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
⊢ y ∈ (Finset.range (n.succ + 1)).erase x ↔ y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)
Tactic:
constructor
Proof state after:
case a.mp
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
⊢ y ∈ (Finset.range (n.succ + 1)).erase x → y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)

case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
⊢ y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x) → y ∈ (Finset.range (n.succ + 1)).erase x
Theorem: Usa1998P3.lemma2
Proof state before:
case a.mp
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
⊢ y ∈ (Finset.range (n.succ + 1)).erase x → y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)
Tactic:
intro hy
Proof state after:
case a.mp
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y ∈ (Finset.range (n.succ + 1)).erase x
⊢ y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)
Theorem: Usa1998P3.lemma2
Proof state before:
case a.mp
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y ∈ (Finset.range (n.succ + 1)).erase x
⊢ y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)
Tactic:
rw [Finset.mem_erase, Finset.mem_range] at hy
Proof state after:
case a.mp
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y ≠ x ∧ y < n.succ + 1
⊢ y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)
Theorem: Usa1998P3.lemma2
Proof state before:
case a.mp
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y ≠ x ∧ y < n.succ + 1
⊢ y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)
Tactic:
rw [Finset.mem_insert, Finset.mem_erase, Finset.mem_range]
Proof state after:
case a.mp
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y ≠ x ∧ y < n.succ + 1
⊢ y = n + 1 ∨ y ≠ x ∧ y < n + 1
Theorem: Usa1998P3.lemma2
Proof state before:
case a.mp
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y ≠ x ∧ y < n.succ + 1
⊢ y = n + 1 ∨ y ≠ x ∧ y < n + 1
Tactic:
omega
Proof state after:
no goals
Theorem: Usa1998P3.lemma2
Proof state before:
case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
⊢ y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x) → y ∈ (Finset.range (n.succ + 1)).erase x
Tactic:
intro hy
Proof state after:
case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)
⊢ y ∈ (Finset.range (n.succ + 1)).erase x
Theorem: Usa1998P3.lemma2
Proof state before:
case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)
⊢ y ∈ (Finset.range (n.succ + 1)).erase x
Tactic:
rw [Finset.mem_insert, Finset.mem_erase, Finset.mem_range] at hy
Proof state after:
case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y = n + 1 ∨ y ≠ x ∧ y < n + 1
⊢ y ∈ (Finset.range (n.succ + 1)).erase x
Theorem: Usa1998P3.lemma2
Proof state before:
case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y = n + 1 ∨ y ≠ x ∧ y < n + 1
⊢ y ∈ (Finset.range (n.succ + 1)).erase x
Tactic:
rw [Finset.mem_range] at hx
Proof state after:
case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x < n + 1
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y = n + 1 ∨ y ≠ x ∧ y < n + 1
⊢ y ∈ (Finset.range (n.succ + 1)).erase x
Theorem: Usa1998P3.lemma2
Proof state before:
case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x < n + 1
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y = n + 1 ∨ y ≠ x ∧ y < n + 1
⊢ y ∈ (Finset.range (n.succ + 1)).erase x
Tactic:
rw [Finset.mem_erase, Finset.mem_range]
Proof state after:
case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x < n + 1
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y = n + 1 ∨ y ≠ x ∧ y < n + 1
⊢ y ≠ x ∧ y < n.succ + 1
Theorem: Usa1998P3.lemma2
Proof state before:
case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x < n + 1
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y = n + 1 ∨ y ≠ x ∧ y < n + 1
⊢ y ≠ x ∧ y < n.succ + 1
Tactic:
omega
Proof state after:
no goals
Theorem: Usa1998P3.lemma2
Proof state before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h3 :
  ∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j =
    ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
⊢ ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) =
    (∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) ^ (n + 1)
Tactic:
rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range]
Proof state after:
no goals
Theorem: Imo2002P5.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
⊢ u x = f x
Tactic:
by_contra! hx
Proof state after:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
⊢ False
Theorem: Imo2002P5.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
⊢ False
Tactic:
let ε : ℝ := |u x - f x|
Proof state after:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
⊢ False
Theorem: Imo2002P5.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
⊢ False
Tactic:
have hε : 0 < ε := abs_sub_pos.mpr hx
Proof state after:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
⊢ False
Theorem: Imo2002P5.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
⊢ False
Tactic:
obtain ⟨δ, hδ0, hδ⟩ := Metric.continuous_iff.mp f_cont x ε hε
Proof state after:
case intro.intro
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
⊢ False
Theorem: Imo2002P5.extend_function_mono
Proof state before:
case intro.intro
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
⊢ False
Tactic:
obtain h1 | h2 | h3 := lt_trichotomy (u x) (f x)
Proof state after:
case intro.intro.inl
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
⊢ False

case intro.intro.inr.inl
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h2 : u x = f x
⊢ False

case intro.intro.inr.inr
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
⊢ False
Theorem: Imo2002P5.extend_function_mono
Proof state before:
case intro.intro.inl
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
this : ∃ z, ↑z < x ∧ dist (↑z) x < δ ∧ 0 < ↑z
⊢ False
Tactic:
obtain ⟨z, h_z_lt_x, hxz, zpos⟩ := this
Proof state after:
case intro.intro.inl.intro.intro.intro
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
z : ℚ
h_z_lt_x : ↑z < x
hxz : dist (↑z) x < δ
zpos : 0 < ↑z
⊢ False
Theorem: Imo2002P5.extend_function_mono
Proof state before:
case intro.intro.inl.intro.intro.intro
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
z : ℚ
h_z_lt_x : ↑z < x
hxz : dist (↑z) x < δ
zpos : 0 < ↑z
⊢ False
Tactic:
have hbzb := hδ z hxz
Proof state after:
case intro.intro.inl.intro.intro.intro
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
z : ℚ
h_z_lt_x : ↑z < x
hxz : dist (↑z) x < δ
zpos : 0 < ↑z
hbzb : dist (f ↑z) (f x) < ε
⊢ False
Theorem: Imo2002P5.extend_function_mono
Proof state before:
case intro.intro.inl.intro.intro.intro
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
z : ℚ
h_z_lt_x : ↑z < x
hxz : dist (↑z) x < δ
zpos : 0 < ↑z
hbzb : dist (f ↑z) (f x) < ε
⊢ False
Tactic:
rw [←h z] at hbzb
Proof state after:
case intro.intro.inl.intro.intro.intro
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
z : ℚ
h_z_lt_x : ↑z < x
hxz : dist (↑z) x < δ
zpos : 0 < ↑z
hbzb : dist (u ↑z) (f x) < ε
⊢ False
Theorem: Imo2002P5.extend_function_mono
Proof state before:
case intro.intro.inl.intro.intro.intro
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
z : ℚ
h_z_lt_x : ↑z < x
hxz : dist (↑z) x < δ
zpos : 0 < ↑z
hbzb : dist (u ↑z) (f x) < ε
huzuy : u x < u ↑z
⊢ False
Tactic:
have := u_mono z x zpos.le h_z_lt_x.le
Proof state after:
case intro.intro.inl.intro.intro.intro
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
z : ℚ
h_z_lt_x : ↑z < x
hxz : dist (↑z) x < δ
zpos : 0 < ↑z
hbzb : dist (u ↑z) (f x) < ε
huzuy : u x < u ↑z
this : u ↑z ≤ u x
⊢ False
Theorem: Imo2002P5.extend_function_mono
Proof state before:
case intro.intro.inl.intro.intro.intro
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
z : ℚ
h_z_lt_x : ↑z < x
hxz : dist (↑z) x < δ
zpos : 0 < ↑z
hbzb : dist (u ↑z) (f x) < ε
huzuy : u x < u ↑z
this : u ↑z ≤ u x
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo2002P5.extend_function_mono
Proof state before:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
⊢ ∃ z, ↑z < x ∧ dist (↑z) x < δ ∧ 0 < ↑z
Tactic:
obtain h3 | h4 := le_or_lt x δ
Proof state after:
case inl
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
h3 : x ≤ δ
⊢ ∃ z, ↑z < x ∧ dist (↑z) x < δ ∧ 0 < ↑z

case inr
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
h4 : δ < x
⊢ ∃ z, ↑z < x ∧ dist (↑z) x < δ ∧ 0 < ↑z