internlm/Lean-Github huggingface dataset:
Theorem: Usa1998P3.lemma1
Proof state before:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
⊢ (x - Real.pi / 4).tan < (Real.pi / 4).tan
Tactic:
rw [h4]
Proof state after:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
⊢ (x - Real.pi / 4).tan < y' (Real.pi / 2)
Theorem: Usa1998P3.lemma1
Proof state before:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
⊢ (x - Real.pi / 4).tan < y' (Real.pi / 2)
Tactic:
let y1 x := x - Real.pi / 4
Proof state after:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
⊢ (x - Real.pi / 4).tan < y' (Real.pi / 2)
Theorem: Usa1998P3.lemma1
Proof state before:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
⊢ (x - Real.pi / 4).tan < y' (Real.pi / 2)
Tactic:
have h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2)) := by
  intro a _ b _ hab
  exact sub_lt_sub_right hab _
Proof state after:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
⊢ (x - Real.pi / 4).tan < y' (Real.pi / 2)
Theorem: Usa1998P3.lemma1
Proof state before:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
h6 : StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
⊢ (x - Real.pi / 4).tan < y' (Real.pi / 2)
Tactic:
apply h6
Proof state after:
case x
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
h6 : StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
⊢ x ∈ Set.Icc 0 (Real.pi / 2)

case x
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
h6 : StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
⊢ Real.pi / 2 ∈ Set.Icc 0 (Real.pi / 2)

case a
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
h6 : StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
⊢ x < Real.pi / 2
Theorem: Usa1998P3.lemma1
Proof state before:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
⊢ (Real.pi / 4).tan = y' (Real.pi / 2)
Tactic:
dsimp only [y']
Proof state after:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
⊢ (Real.pi / 4).tan = (Real.pi / 2 - Real.pi / 4).tan
Theorem: Usa1998P3.lemma1
Proof state before:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
⊢ (Real.pi / 4).tan = (Real.pi / 2 - Real.pi / 4).tan
Tactic:
rw [Real.tan_pi_div_two_sub, Real.tan_pi_div_four, one_eq_inv]
Proof state after:
no goals
Theorem: Usa1998P3.lemma1
Proof state before:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
⊢ StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
Tactic:
intro a _ b _ hab
Proof state after:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
a : ℝ
x✝¹ : a ∈ Set.Icc 0 (Real.pi / 2)
b : ℝ
x✝ : b ∈ Set.Icc 0 (Real.pi / 2)
hab : a < b
⊢ y1 a < y1 b
Theorem: Usa1998P3.lemma1
Proof state before:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
a : ℝ
x✝¹ : a ∈ Set.Icc 0 (Real.pi / 2)
b : ℝ
x✝ : b ∈ Set.Icc 0 (Real.pi / 2)
hab : a < b
⊢ y1 a < y1 b
Tactic:
exact sub_lt_sub_right hab _
Proof state after:
no goals
Theorem: Usa1998P3.lemma1
Proof state before:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
⊢ StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
Tactic:
apply StrictMonoOn.comp (g := Real.tan) (f := y1)
     (t := (Set.Icc (-Real.pi / 4) (Real.pi / 4)))
     (StrictMonoOn.mono Real.strictMonoOn_tan lemma0)
     h5
Proof state after:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
⊢ Set.MapsTo y1 (Set.Icc 0 (Real.pi / 2)) (Set.Icc (-Real.pi / 4) (Real.pi / 4))
Theorem: Usa1998P3.lemma1
Proof state before:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
⊢ Set.MapsTo y1 (Set.Icc 0 (Real.pi / 2)) (Set.Icc (-Real.pi / 4) (Real.pi / 4))
Tactic:
intro a ha
Proof state after:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
a : ℝ
ha : a ∈ Set.Icc 0 (Real.pi / 2)
⊢ y1 a ∈ Set.Icc (-Real.pi / 4) (Real.pi / 4)
Theorem: Usa1998P3.lemma1
Proof state before:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
a : ℝ
ha : a ∈ Set.Icc 0 (Real.pi / 2)
⊢ y1 a ∈ Set.Icc (-Real.pi / 4) (Real.pi / 4)
Tactic:
obtain ⟨ha1, ha2⟩ := ha
Proof state after:
case intro
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
a : ℝ
ha1 : 0 ≤ a
ha2 : a ≤ Real.pi / 2
⊢ y1 a ∈ Set.Icc (-Real.pi / 4) (Real.pi / 4)
Theorem: Usa1998P3.lemma1
Proof state before:
case intro
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
a : ℝ
ha1 : 0 ≤ a
ha2 : a ≤ Real.pi / 2
⊢ y1 a ∈ Set.Icc (-Real.pi / 4) (Real.pi / 4)
Tactic:
constructor
Proof state after:
case intro.left
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
a : ℝ
ha1 : 0 ≤ a
ha2 : a ≤ Real.pi / 2
⊢ -Real.pi / 4 ≤ y1 a

case intro.right
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
a : ℝ
ha1 : 0 ≤ a
ha2 : a ≤ Real.pi / 2
⊢ y1 a ≤ Real.pi / 4
Theorem: Usa1998P3.lemma1
Proof state before:
case intro.left
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
a : ℝ
ha1 : 0 ≤ a
ha2 : a ≤ Real.pi / 2
⊢ -Real.pi / 4 ≤ y1 a
Tactic:
dsimp [y1]
Proof state after:
case intro.left
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
a : ℝ
ha1 : 0 ≤ a
ha2 : a ≤ Real.pi / 2
⊢ -Real.pi / 4 ≤ a - Real.pi / 4
Theorem: Usa1998P3.lemma1
Proof state before:
case intro.left
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
a : ℝ
ha1 : 0 ≤ a
ha2 : a ≤ Real.pi / 2
⊢ -Real.pi / 4 ≤ a - Real.pi / 4
Tactic:
linarith
Proof state after:
no goals
Theorem: Usa1998P3.lemma1
Proof state before:
case intro.right
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
a : ℝ
ha1 : 0 ≤ a
ha2 : a ≤ Real.pi / 2
⊢ y1 a ≤ Real.pi / 4
Tactic:
dsimp [y1]
Proof state after:
case intro.right
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
a : ℝ
ha1 : 0 ≤ a
ha2 : a ≤ Real.pi / 2
⊢ a - Real.pi / 4 ≤ Real.pi / 4
Theorem: Usa1998P3.lemma1
Proof state before:
case intro.right
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
a : ℝ
ha1 : 0 ≤ a
ha2 : a ≤ Real.pi / 2
⊢ a - Real.pi / 4 ≤ Real.pi / 4
Tactic:
linarith
Proof state after:
no goals
Theorem: Usa1998P3.lemma1
Proof state before:
case x
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
h6 : StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
⊢ x ∈ Set.Icc 0 (Real.pi / 2)
Tactic:
exact Set.mem_Icc_of_Ioo hx
Proof state after:
no goals
Theorem: Usa1998P3.lemma1
Proof state before:
case x
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
h6 : StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
⊢ Real.pi / 2 ∈ Set.Icc 0 (Real.pi / 2)
Tactic:
constructor
Proof state after:
case x.left
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
h6 : StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
⊢ 0 ≤ Real.pi / 2

case x.right
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
h6 : StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
⊢ Real.pi / 2 ≤ Real.pi / 2
Theorem: Usa1998P3.lemma1
Proof state before:
case x.left
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
h6 : StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
⊢ 0 ≤ Real.pi / 2

case x.right
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
h6 : StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
⊢ Real.pi / 2 ≤ Real.pi / 2
Tactic:
. exact le_of_lt Real.pi_div_two_pos
Proof state after:
case x.right
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
h6 : StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
⊢ Real.pi / 2 ≤ Real.pi / 2
Theorem: Usa1998P3.lemma1
Proof state before:
case x.right
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
h6 : StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
⊢ Real.pi / 2 ≤ Real.pi / 2
Tactic:
. exact Eq.le rfl
Proof state after:
no goals
Theorem: Usa1998P3.lemma1
Proof state before:
case x.left
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
h6 : StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
⊢ 0 ≤ Real.pi / 2
Tactic:
exact le_of_lt Real.pi_div_two_pos
Proof state after:
no goals
Theorem: Usa1998P3.lemma1
Proof state before:
case x.right
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
h6 : StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
⊢ Real.pi / 2 ≤ Real.pi / 2
Tactic:
exact Eq.le rfl
Proof state after:
no goals
Theorem: Usa1998P3.lemma1
Proof state before:
case a
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
h6 : StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
⊢ x < Real.pi / 2
Tactic:
exact hx.2
Proof state after:
no goals
Theorem: Usa1998P3.lemma2'
Proof state before:
n : ℕ
⊢ (Finset.range (n + 1)).erase n = Finset.range n
Tactic:
rw [←Nat.succ_eq_add_one, Finset.range_succ]
Proof state after:
n : ℕ
⊢ (insert n (Finset.range n)).erase n = Finset.range n
Theorem: Usa1998P3.lemma2'
Proof state before:
n : ℕ
⊢ (insert n (Finset.range n)).erase n = Finset.range n
Tactic:
simp
Proof state after:
no goals
Theorem: Usa1998P3.lemma2
Proof state before:
case zero
f : ℕ → ℝ
⊢ ∏ i ∈ Finset.range (0 + 1), ∏ j ∈ (Finset.range (0 + 1)).erase i, f j = ∏ i ∈ Finset.range (0 + 1), f i ^ ↑0
Tactic:
simp
Proof state after:
no goals
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
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    ∏ i ∈ Finset.range (n + 1 + 1), f i ^ ↑(n + 1)
Tactic:
have h1 : ∏ i ∈ Finset.range (Nat.succ n + 1), f i ^ ((Nat.succ n):ℝ) =
        (∏ i ∈ Finset.range (n + 1), f i ^ ((Nat.succ n):ℝ)) * f (n + 1) ^ ((Nat.succ n):ℝ) :=
 by rw [Finset.prod_range_succ]
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
h1 : ∏ i ∈ Finset.range (n.succ + 1), f i ^ ↑n.succ = (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    ∏ i ∈ Finset.range (n + 1 + 1), f i ^ ↑(n + 1)
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
h1 : ∏ i ∈ Finset.range (n.succ + 1), f i ^ ↑n.succ = (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    ∏ i ∈ Finset.range (n + 1 + 1), f i ^ ↑(n + 1)
Tactic:
rw [h1]
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
h1 : ∏ i ∈ Finset.range (n.succ + 1), f i ^ ↑n.succ = (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * 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
h1 : ∏ i ∈ Finset.range (n.succ + 1), f i ^ ↑n.succ = (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ
Tactic:
clear h1
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
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * 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
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ
Tactic:
have h2 : ∏ i ∈ Finset.range (n + 1), f i ^ ((Nat.succ n):ℝ) =
          ∏ i ∈ Finset.range (n + 1), (f i ^ (n:ℝ) * f i) := by
   congr; funext x
   norm_cast
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
h2 : ∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n * f i
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * 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
h2 : ∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n * f i
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ
Tactic:
rw [h2]
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
h2 : ∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n * f i
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n * f i) * 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
h2 : ∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n * f i
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n * f i) * f (n + 1) ^ ↑n.succ
Tactic:
clear h2
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
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n * f i) * 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
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n * f i) * f (n + 1) ^ ↑n.succ
Tactic:
rw [Finset.prod_mul_distrib]
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
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    ((∏ 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
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    ((∏ x ∈ Finset.range (n + 1), f x ^ ↑n) * ∏ x ∈ Finset.range (n + 1), f x) * f (n + 1) ^ ↑n.succ
Tactic:
rw [Finset.prod_range_succ, lemma2']
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
⊢ (∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase x, f j) * ∏ 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
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)
⊢ (∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase x, f j) * ∏ 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 [h3]
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)
⊢ (∏ 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
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)
⊢ (∏ 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:
have h4 :
    ∏ x ∈ Finset.range (n + 1),
      ((∏ j ∈ Finset.erase (Finset.range (n + 1)) x, f j) * f (n + 1)) =
     (∏ x ∈ Finset.range (n + 1),
        ∏ j ∈ Finset.erase (Finset.range (n + 1)) x, f j) * f (n + 1) ^ (n+1) := by
  rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range]
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)
⊢ (∏ 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