awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (hypothesis)
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
τ_spec : HPow.hPow (β := ℕ) τ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : Eq (α := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) (1 : FF)
hq : χ.IsQuadratic
h₁ :
  Eq.{u_1 + 1} (α := (a : Fin 8) → FF) (fun (a : Fin 8) ↦ (↑((χ₈ : (a : ZMod 8) → ℤ) a) : FF) * τ ^ (↑a : ℕ))
    fun (a : ZMod 8) ↦
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) a : FF) ((ψ₈char : (a : ZMod 8) → FF) a : FF)
hg₁ : gaussSum χ ψ₈char = 2 * (τ - HPow.hPow (β := ℕ) τ 3)
hg :
  HPow.hPow (β := ℕ) (gaussSum χ ψ₈char) 2 =
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) ((↑(Fintype.card (ZMod 8)) : FF) : FF)
⊢ HPow.hPow (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
have h : HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) ((↑(Fintype.card (ZMod 8)) : FF) : FF) ^
    (ringChar FF ^ (↑n : ℕ) / 2) =
  (χ : (a : ZMod 8) → FF) (HPow.hPow (α := ZMod 8) (↑(ringChar FF) : ZMod 8) (↑n : ℕ))
Tactic: have h := Char.card_pow_char_pow (R := ZMod 8) hq ψ₈char (ringChar FF) n hu hFF hg
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (hypothesis)
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
τ_spec : HPow.hPow (β := ℕ) τ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : Eq (α := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) (1 : FF)
hq : χ.IsQuadratic
h₁ :
  Eq.{u_1 + 1} (α := (a : Fin 8) → FF) (fun (a : Fin 8) ↦ (↑((χ₈ : (a : ZMod 8) → ℤ) a) : FF) * τ ^ (↑a : ℕ))
    fun (a : ZMod 8) ↦
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) a : FF) ((ψ₈char : (a : ZMod 8) → FF) a : FF)
hg₁ : gaussSum χ ψ₈char = 2 * (τ - HPow.hPow (β := ℕ) τ 3)
hg :
  HPow.hPow (β := ℕ) (gaussSum χ ψ₈char) 2 =
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) ((↑(Fintype.card (ZMod 8)) : FF) : FF)
h :
  HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) ((↑(Fintype.card (ZMod 8)) : FF) : FF) ^
      (ringChar FF ^ (↑n : ℕ) / 2) =
    (χ : (a : ZMod 8) → FF) (HPow.hPow (α := ZMod 8) (↑(ringChar FF) : ZMod 8) (↑n : ℕ))
⊢ HPow.hPow (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
have h₂ : HPow.hPow (α := FF) (↑8 : FF) (Fintype.card F / 2) = (χ : (a : ZMod 8) → FF) (↑(Fintype.card F) : ZMod 8)
Tactic: rw [ZMod.card, ← hchar, hχ, one_mul, ← hc, ← Nat.cast_pow (ringChar F), ← hc] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
τ_spec : HPow.hPow (β := ℕ) τ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : Eq (α := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) (1 : FF)
hq : χ.IsQuadratic
h₁ :
  Eq.{u_1 + 1} (α := (a : Fin 8) → FF) (fun (a : Fin 8) ↦ (↑((χ₈ : (a : ZMod 8) → ℤ) a) : FF) * τ ^ (↑a : ℕ))
    fun (a : ZMod 8) ↦
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) a : FF) ((ψ₈char : (a : ZMod 8) → FF) a : FF)
hg₁ : gaussSum χ ψ₈char = 2 * (τ - HPow.hPow (β := ℕ) τ 3)
hg :
  HPow.hPow (β := ℕ) (gaussSum χ ψ₈char) 2 =
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) ((↑(Fintype.card (ZMod 8)) : FF) : FF)
h : HPow.hPow (α := FF) (↑8 : FF) (Fintype.card F / 2) = (χ : (a : ZMod 8) → FF) (↑(Fintype.card F) : ZMod 8)
⊢ HPow.hPow (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
have h₂ : HPow.hPow (α := F) 2 (Fintype.card F / 2) = HPow.hPow (α := F) 8 (Fintype.card F / 2)
Tactic: convert_to (8 : F) ^ (Fintype.card F / 2) = _
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
τ_spec : HPow.hPow (β := ℕ) τ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : Eq (α := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) (1 : FF)
hq : χ.IsQuadratic
h₁ :
  Eq.{u_1 + 1} (α := (a : Fin 8) → FF) (fun (a : Fin 8) ↦ (↑((χ₈ : (a : ZMod 8) → ℤ) a) : FF) * τ ^ (↑a : ℕ))
    fun (a : ZMod 8) ↦
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) a : FF) ((ψ₈char : (a : ZMod 8) → FF) a : FF)
hg₁ : gaussSum χ ψ₈char = 2 * (τ - HPow.hPow (β := ℕ) τ 3)
hg :
  HPow.hPow (β := ℕ) (gaussSum χ ψ₈char) 2 =
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) ((↑(Fintype.card (ZMod 8)) : FF) : FF)
h : HPow.hPow (α := FF) (↑8 : FF) (Fintype.card F / 2) = (χ : (a : ZMod 8) → FF) (↑(Fintype.card F) : ZMod 8)
h₂ : HPow.hPow (α := F) 2 (Fintype.card F / 2) = HPow.hPow (α := F) 8 (Fintype.card F / 2)
⊢ HPow.hPow (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
have convert_2 : HPow.hPow (α := F) 8 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
Tactic: convert_to (8 : F) ^ (Fintype.card F / 2) = _
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
F : Type u_1
inst : Fintype F
inst_1 : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), HPow.hPow (α := F) 2 n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit (M := ZMod 8) (↑(ringChar FF) : ZMod 8)
ψ₈ : PrimitiveAddChar (ZMod (↑8 : ℕ)) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := (ψ₈char : (a : ZMod 8) → FF) 1
τ_spec : HPow.hPow (β := ℕ) τ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : Eq (α := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) (1 : FF)
hq : χ.IsQuadratic
h₁ :
  Eq.{u_1 + 1} (α := (a : Fin 8) → FF) (fun (a : Fin 8) ↦ (↑((χ₈ : (a : ZMod 8) → ℤ) a) : FF) * τ ^ (↑a : ℕ))
    fun (a : ZMod 8) ↦
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) a : FF) ((ψ₈char : (a : ZMod 8) → FF) a : FF)
hg₁ : gaussSum χ ψ₈char = 2 * (τ - HPow.hPow (β := ℕ) τ 3)
hg :
  HPow.hPow (β := ℕ) (gaussSum χ ψ₈char) 2 =
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) ((↑(Fintype.card (ZMod 8)) : FF) : FF)
h : HPow.hPow (α := FF) (↑8 : FF) (Fintype.card F / 2) = (χ : (a : ZMod 8) → FF) (↑(Fintype.card F) : ZMod 8)
⊢ HPow.hPow (α := F) 8 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
have convert_2 : Eq (α := FF) (((algebraMap F FF : F →+* FF) : (a : F) → FF) (HPow.hPow (α := F) 8 (Fintype.card F / 2)) : FF)
  (((algebraMap F FF : F →+* FF) : (a : F) → FF) (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F) : FF)
Tactic: apply (algebraMap F FF).injective
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
⊢ harmonic n = ∑ i ∈ Finset.Icc 1 n, (↑i : ℚ)⁻¹
have rw : Eq (α := ℚ) (∑ x ∈ Finset.Ico (HAdd.hAdd (α := ℕ) 0 1) (n + 1), (↑x : ℚ)⁻¹) (∑ i ∈ Finset.Icc 1 n, (↑i : ℚ)⁻¹)
Tactic: rw [harmonic, Finset.range_eq_Ico, Finset.sum_Ico_add' (fun (i : ℕ) ↦ (i : ℚ)⁻¹) 0 n (c := 1)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
⊢ Real.log (↑(n + 1) : ℝ) ≤ (↑(harmonic n) : ℝ)
have calc_1 : Real.log (↑(n + 1) : ℝ) = ∫ (x : ℝ) in (↑1 : ℝ)..(↑(n + 1) : ℝ), x⁻¹
Tactic: calc _ = ∫ x in (1 : ℕ)..↑(n + 1), x⁻¹ := ?_
       _ ≤ ∑ d ∈ Finset.Icc 1 n, (d : ℝ)⁻¹ := ?_
       _ = harmonic n := ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
calc_1 : Real.log (↑(n + 1) : ℝ) = ∫ (x : ℝ) in (↑1 : ℝ)..(↑(n + 1) : ℝ), x⁻¹
⊢ Real.log (↑(n + 1) : ℝ) ≤ (↑(harmonic n) : ℝ)
have calc_2 : LE.le (α := ℝ) (∫ (x : ℝ) in (↑1 : ℝ)..(↑(n + 1) : ℝ), x⁻¹) (∑ d ∈ Finset.Icc 1 n, (↑d : ℝ)⁻¹)
Tactic: calc _ = ∫ x in (1 : ℕ)..↑(n + 1), x⁻¹ := ?_
       _ ≤ ∑ d ∈ Finset.Icc 1 n, (d : ℝ)⁻¹ := ?_
       _ = harmonic n := ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
calc_1 : Real.log (↑(n + 1) : ℝ) = ∫ (x : ℝ) in (↑1 : ℝ)..(↑(n + 1) : ℝ), x⁻¹
calc_2 : LE.le (α := ℝ) (∫ (x : ℝ) in (↑1 : ℝ)..(↑(n + 1) : ℝ), x⁻¹) (∑ d ∈ Finset.Icc 1 n, (↑d : ℝ)⁻¹)
⊢ Real.log (↑(n + 1) : ℝ) ≤ (↑(harmonic n) : ℝ)
have calc_3 : Eq (α := ℝ) (∑ d ∈ Finset.Icc 1 n, (↑d : ℝ)⁻¹) (↑(harmonic n) : ℝ)
Tactic: calc _ = ∫ x in (1 : ℕ)..↑(n + 1), x⁻¹ := ?_
       _ ≤ ∑ d ∈ Finset.Icc 1 n, (d : ℝ)⁻¹ := ?_
       _ = harmonic n := ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
⊢ Real.log (↑(n + 1) : ℝ) = ∫ (x : ℝ) in (↑1 : ℝ)..(↑(n + 1) : ℝ), x⁻¹
have calc_1 : Real.log (↑(n + 1) : ℝ) = ∫ (x : ℝ) in 1..(↑(n + 1) : ℝ), x⁻¹
Tactic: rw [Nat.cast_one, integral_inv (by simp [(show ¬ (1 : ℝ) ≤ 0 by simp)]), div_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
calc_1 : Real.log (↑(n + 1) : ℝ) = ∫ (x : ℝ) in 1..(↑(n + 1) : ℝ), x⁻¹
⊢ Real.log (↑(n + 1) : ℝ) = ∫ (x : ℝ) in (↑1 : ℝ)..(↑(n + 1) : ℝ), x⁻¹
have calc_1₁ : Real.log (↑(n + 1) : ℝ) = Real.log (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) 1)
Tactic: rw [Nat.cast_one, integral_inv (by simp [(show ¬ (1 : ℝ) ≤ 0 by simp)]), div_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
calc_1 : Real.log (↑(n + 1) : ℝ) = ∫ (x : ℝ) in 1..(↑(n + 1) : ℝ), x⁻¹
calc_1₁ : Real.log (↑(n + 1) : ℝ) = Real.log (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) 1)
⊢ Real.log (↑(n + 1) : ℝ) = ∫ (x : ℝ) in (↑1 : ℝ)..(↑(n + 1) : ℝ), x⁻¹
have calc_1₂ : Real.log (↑(n + 1) : ℝ) = Real.log (↑(n + 1) : ℝ)
Tactic: rw [Nat.cast_one, integral_inv (by simp [(show ¬ (1 : ℝ) ≤ 0 by simp)]), div_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
⊢ (↑(harmonic n) : ℝ) ≤ 1 + Real.log (↑n : ℝ)
have pos : ∀ (hn0 : n = 0), (↑(harmonic n) : ℝ) ≤ 1 + Real.log (↑n : ℝ)
Tactic: by_cases hn0 : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
pos : ∀ (hn0 : n = 0), (↑(harmonic n) : ℝ) ≤ 1 + Real.log (↑n : ℝ)
⊢ (↑(harmonic n) : ℝ) ≤ 1 + Real.log (↑n : ℝ)
have neg : ∀ (hn0 : ¬n = 0), (↑(harmonic n) : ℝ) ≤ 1 + Real.log (↑n : ℝ)
Tactic: by_cases hn0 : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (hypothesis)
Goal:
n : ℕ
hn0 : ¬n = 0
⊢ (↑(harmonic n) : ℝ) ≤ 1 + Real.log (↑n : ℝ)
have hn : 1 ≤ n
Tactic: have hn : 1 ≤ n := Nat.one_le_iff_ne_zero.mpr hn0
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ (↑(harmonic n) : ℝ) ≤ 1 + Real.log (↑n : ℝ)
have neg : ∑ x ∈ Finset.Icc 1 n, (↑x : ℝ)⁻¹ ≤ 1 + Real.log (↑n : ℝ)
Tactic: simp_rw [harmonic_eq_sum_Icc, Rat.cast_sum, Rat.cast_inv, Rat.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ x ∈ Finset.Icc 1 n, (↑x : ℝ)⁻¹ ≤ 1 + Real.log (↑n : ℝ)
have neg : HAdd.hAdd (α := ℝ) 1 (∑ x ∈ (Finset.Icc 1 n).erase 1, (↑x : ℝ)⁻¹) ≤ 1 + Real.log (↑n : ℝ)
Tactic: rw [← Finset.sum_erase_add (Finset.Icc 1 n) _ (Finset.left_mem_Icc.mpr hn), add_comm,
    Nat.cast_one, inv_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ HAdd.hAdd (α := ℝ) 1 (∑ x ∈ (Finset.Icc 1 n).erase 1, (↑x : ℝ)⁻¹) ≤ 1 + Real.log (↑n : ℝ)
have neg : ∑ x ∈ (Finset.Icc 1 n).erase 1, (↑x : ℝ)⁻¹ ≤ Real.log (↑n : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ x ∈ (Finset.Icc 1 n).erase 1, (↑x : ℝ)⁻¹ ≤ Real.log (↑n : ℝ)
have neg : ∑ x ∈ Finset.Ioc 1 n, (↑x : ℝ)⁻¹ ≤ Real.log (↑n : ℝ)
Tactic: simp only [Finset.Icc_erase_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ x ∈ Finset.Ioc 1 n, (↑x : ℝ)⁻¹ ≤ Real.log (↑n : ℝ)
have neg : Eq (α := ℝ) (∑ d ∈ Finset.Ico 2 (n + 1), (↑d : ℝ)⁻¹)
  (∑ d ∈ Finset.Ico 2 (n + 1), (HSub.hSub (α := ℝ) (↑(d + 1) : ℝ) 1)⁻¹)
Tactic: calc ∑ d ∈ .Ico 2 (n + 1), (d : ℝ)⁻¹
    _ = ∑ d ∈ .Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹ := ?_
    _ ≤ ∫ x in 2..↑(n + 1), (x - 1)⁻¹ := ?_
    _ = ∫ x in 1..n, x⁻¹ := ?_
    _ = Real.log ↑n := ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
neg :
  Eq (α := ℝ) (∑ d ∈ Finset.Ico 2 (n + 1), (↑d : ℝ)⁻¹)
    (∑ d ∈ Finset.Ico 2 (n + 1), (HSub.hSub (α := ℝ) (↑(d + 1) : ℝ) 1)⁻¹)
⊢ ∑ x ∈ Finset.Ioc 1 n, (↑x : ℝ)⁻¹ ≤ Real.log (↑n : ℝ)
have neg₁ : LE.le (α := ℝ) (∑ d ∈ Finset.Ico 2 (n + 1), (HSub.hSub (α := ℝ) (↑(d + 1) : ℝ) 1)⁻¹)
  (∫ (x : ℝ) in 2..(↑(n + 1) : ℝ), (x - 1)⁻¹)
Tactic: calc ∑ d ∈ .Ico 2 (n + 1), (d : ℝ)⁻¹
    _ = ∑ d ∈ .Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹ := ?_
    _ ≤ ∫ x in 2..↑(n + 1), (x - 1)⁻¹ := ?_
    _ = ∫ x in 1..n, x⁻¹ := ?_
    _ = Real.log ↑n := ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
neg :
  Eq (α := ℝ) (∑ d ∈ Finset.Ico 2 (n + 1), (↑d : ℝ)⁻¹)
    (∑ d ∈ Finset.Ico 2 (n + 1), (HSub.hSub (α := ℝ) (↑(d + 1) : ℝ) 1)⁻¹)
neg₁ :
  LE.le (α := ℝ) (∑ d ∈ Finset.Ico 2 (n + 1), (HSub.hSub (α := ℝ) (↑(d + 1) : ℝ) 1)⁻¹)
    (∫ (x : ℝ) in 2..(↑(n + 1) : ℝ), (x - 1)⁻¹)
⊢ ∑ x ∈ Finset.Ioc 1 n, (↑x : ℝ)⁻¹ ≤ Real.log (↑n : ℝ)
have neg₂ : Eq (α := ℝ) (∫ (x : ℝ) in 2..(↑(n + 1) : ℝ), (x - 1)⁻¹) (∫ (x : ℝ) in 1..(↑n : ℝ), x⁻¹)
Tactic: calc ∑ d ∈ .Ico 2 (n + 1), (d : ℝ)⁻¹
    _ = ∑ d ∈ .Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹ := ?_
    _ ≤ ∫ x in 2..↑(n + 1), (x - 1)⁻¹ := ?_
    _ = ∫ x in 1..n, x⁻¹ := ?_
    _ = Real.log ↑n := ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
neg :
  Eq (α := ℝ) (∑ d ∈ Finset.Ico 2 (n + 1), (↑d : ℝ)⁻¹)
    (∑ d ∈ Finset.Ico 2 (n + 1), (HSub.hSub (α := ℝ) (↑(d + 1) : ℝ) 1)⁻¹)
neg₁ :
  LE.le (α := ℝ) (∑ d ∈ Finset.Ico 2 (n + 1), (HSub.hSub (α := ℝ) (↑(d + 1) : ℝ) 1)⁻¹)
    (∫ (x : ℝ) in 2..(↑(n + 1) : ℝ), (x - 1)⁻¹)
neg₂ : Eq (α := ℝ) (∫ (x : ℝ) in 2..(↑(n + 1) : ℝ), (x - 1)⁻¹) (∫ (x : ℝ) in 1..(↑n : ℝ), x⁻¹)
⊢ ∑ x ∈ Finset.Ioc 1 n, (↑x : ℝ)⁻¹ ≤ Real.log (↑n : ℝ)
have neg₃ : ∫ (x : ℝ) in 1..(↑n : ℝ), x⁻¹ = Real.log (↑n : ℝ)
Tactic: calc ∑ d ∈ .Ico 2 (n + 1), (d : ℝ)⁻¹
    _ = ∑ d ∈ .Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹ := ?_
    _ ≤ ∫ x in 2..↑(n + 1), (x - 1)⁻¹ := ?_
    _ = ∫ x in 1..n, x⁻¹ := ?_
    _ = Real.log ↑n := ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ Eq (α := ℝ) (∑ d ∈ Finset.Ico 2 (n + 1), (↑d : ℝ)⁻¹)
    (∑ d ∈ Finset.Ico 2 (n + 1), (HSub.hSub (α := ℝ) (↑(d + 1) : ℝ) 1)⁻¹)
have neg : Eq (α := ℝ) (∑ d ∈ Finset.Ico 2 (n + 1), (↑d : ℝ)⁻¹)
  (∑ x ∈ Finset.Ico 2 (n + 1), (HAdd.hAdd (α := ℝ) (↑x : ℝ) (↑1 : ℝ) - 1)⁻¹)
Tactic: simp_rw [Nat.cast_add, Nat.cast_one, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
neg :
  Eq (α := ℝ) (∑ d ∈ Finset.Ico 2 (n + 1), (↑d : ℝ)⁻¹)
    (∑ x ∈ Finset.Ico 2 (n + 1), (HAdd.hAdd (α := ℝ) (↑x : ℝ) (↑1 : ℝ) - 1)⁻¹)
⊢ Eq (α := ℝ) (∑ d ∈ Finset.Ico 2 (n + 1), (↑d : ℝ)⁻¹)
    (∑ d ∈ Finset.Ico 2 (n + 1), (HSub.hSub (α := ℝ) (↑(d + 1) : ℝ) 1)⁻¹)
have neg₁ : Eq (α := ℝ) (∑ d ∈ Finset.Ico 2 (n + 1), (↑d : ℝ)⁻¹) (∑ x ∈ Finset.Ico 2 (n + 1), (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 - 1)⁻¹)
Tactic: simp_rw [Nat.cast_add, Nat.cast_one, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ 2 ≤ n + 1
have linarith : n + 1 < 2 → -1 + HSub.hSub (α := ℤ) 1 (↑n : ℤ) + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 - 2) = 0
Tactic: linarith [hn]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 2..(↑(n + 1) : ℝ), (x - 1)⁻¹) (∫ (x : ℝ) in 1..(↑n : ℝ), x⁻¹)
have h : 1 = HSub.hSub (α := ℝ) 2 1
Tactic: convert! intervalIntegral.integral_comp_sub_right _ 1
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
h : 1 = HSub.hSub (α := ℝ) 2 1
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 2..(↑(n + 1) : ℝ), (x - 1)⁻¹) (∫ (x : ℝ) in 1..(↑n : ℝ), x⁻¹)
have h₁ : (↑n : ℝ) = HSub.hSub (α := ℝ) (↑(n + 1) : ℝ) 1
Tactic: convert! intervalIntegral.integral_comp_sub_right _ 1
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∫ (x : ℝ) in 1..(↑n : ℝ), x⁻¹ = Real.log (↑n : ℝ)
have h : (↑n : ℝ) = HDiv.hDiv (α := ℝ) (↑n : ℝ) 1
Tactic: convert! integral_inv _
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
h : (↑n : ℝ) = HDiv.hDiv (α := ℝ) (↑n : ℝ) 1
⊢ ∫ (x : ℝ) in 1..(↑n : ℝ), x⁻¹ = Real.log (↑n : ℝ)
have neg : 0 ∉ Set.uIcc 1 (↑n : ℝ)
Tactic: convert! integral_inv _
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ (↑n : ℝ) = HDiv.hDiv (α := ℝ) (↑n : ℝ) 1
have h : Eq (α := ℝ) (↑n : ℝ) (↑n : ℝ)
Tactic: rw [div_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
y : ℝ
hy : 0 ≤ y
⊢ Real.log y ≤ (↑(harmonic ⌊y⌋₊) : ℝ)
have pos : ∀ (h0 : y = 0), Real.log y ≤ (↑(harmonic ⌊y⌋₊) : ℝ)
Tactic: by_cases h0 : y = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
y : ℝ
hy : 0 ≤ y
pos : ∀ (h0 : y = 0), Real.log y ≤ (↑(harmonic ⌊y⌋₊) : ℝ)
⊢ Real.log y ≤ (↑(harmonic ⌊y⌋₊) : ℝ)
have neg : ∀ (h0 : ¬y = 0), Real.log y ≤ (↑(harmonic ⌊y⌋₊) : ℝ)
Tactic: by_cases h0 : y = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ Real.log y ≤ (↑(harmonic ⌊y⌋₊) : ℝ)
have neg : Real.log y ≤ Real.log (↑(⌊y⌋₊ + 1) : ℝ)
Tactic: calc
      _ ≤ Real.log ↑(Nat.floor y + 1) := ?_
      _ ≤ _ := log_add_one_le_harmonic _
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ Real.log y ≤ Real.log (↑(⌊y⌋₊ + 1) : ℝ)
have neg : y ≤ (↑(⌊y⌋₊ + 1) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ y ≤ (↑(⌊y⌋₊ + 1) : ℝ)
have neg : LE.le (α := ℝ) (↑⌈y⌉₊ : ℝ) (↑(⌊y⌋₊ + 1) : ℝ)
Tactic: apply (Nat.le_ceil y).trans
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ LE.le (α := ℝ) (↑⌈y⌉₊ : ℝ) (↑(⌊y⌋₊ + 1) : ℝ)
have neg : ⌈y⌉₊ ≤ ⌊y⌋₊ + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
y : ℝ
hy : 1 ≤ y
⊢ (↑(harmonic ⌊y⌋₊) : ℝ) ≤ 1 + Real.log y
have refine : 1 + Real.log (↑⌊y⌋₊ : ℝ) ≤ 1 + Real.log y
Tactic: refine (harmonic_le_one_add_log _).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
y : ℝ
hy : 1 ≤ y
⊢ 1 + Real.log (↑⌊y⌋₊ : ℝ) ≤ 1 + Real.log y
have bc : LT.lt (α := ℝ) 0 (↑⌊y⌋₊ : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Bounds (goal)
Goal:
y : ℝ
hy : 1 ≤ y
bc : LT.lt (α := ℝ) 0 (↑⌊y⌋₊ : ℝ)
⊢ 1 + Real.log (↑⌊y⌋₊ : ℝ) ≤ 1 + Real.log y
have bc₁ : (↑⌊y⌋₊ : ℝ) ≤ y
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
⊢ StrictMono eulerMascheroniSeq
have refine : ∀ (n : ℕ), eulerMascheroniSeq n < eulerMascheroniSeq (n + 1)
Tactic: refine strictMono_nat_of_lt_succ (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
n : ℕ
⊢ eulerMascheroniSeq n < eulerMascheroniSeq (n + 1)
have rw : log (1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹) < (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
Tactic: rw [eulerMascheroniSeq, eulerMascheroniSeq, ← sub_pos, sub_sub_sub_comm,
    harmonic_succ, add_comm, Rat.cast_add, add_sub_cancel_right,
    ← log_div (by positivity) (by positivity), add_div, Nat.cast_add_one,
    Nat.cast_add_one, div_self (by positivity), sub_pos, one_div, Rat.cast_inv, Rat.cast_add,
    Rat.cast_one, Rat.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
n : ℕ
⊢ log (1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹) < (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
have refine_1 : 0 < 1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
Tactic: refine (log_lt_sub_one_of_pos ?_ (ne_of_gt <| lt_add_of_pos_right _ ?_)).trans_le (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
n : ℕ
refine_1 : 0 < 1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
⊢ log (1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹) < (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
have refine_2 : 0 < (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
Tactic: refine (log_lt_sub_one_of_pos ?_ (ne_of_gt <| lt_add_of_pos_right _ ?_)).trans_le (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
n : ℕ
refine_1 : 0 < 1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
refine_2 : 0 < (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
⊢ log (1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹) < (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
have refine_3 : 1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ - 1 = (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹
Tactic: refine (log_lt_sub_one_of_pos ?_ (ne_of_gt <| lt_add_of_pos_right _ ?_)).trans_le (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (hypothesis)
Goal:
⊢ 1 / 2 < eulerMascheroniSeq 6
have this : eulerMascheroniSeq 6 = 49 / 20 - log 7
Tactic: have : eulerMascheroniSeq 6 = 49 / 20 - log 7 := by
    rw [eulerMascheroniSeq]
    norm_num
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 1 / 2 < eulerMascheroniSeq 6
have rw : 7 < rexp (49 / 20 - 1 / 2)
Tactic: rw [this, lt_sub_iff_add_lt, ← lt_sub_iff_add_lt', log_lt_iff_lt_exp (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.EulerMascheroni (goal)
Goal:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 7 < rexp (49 / 20 - 1 / 2)
have refine : LT.lt (α := ℝ) 7 (∑ i ∈ Finset.range 7, (49 / 20 - 1 / 2) ^ i / (↑i.factorial : ℝ))
Tactic: refine lt_of_lt_of_le ?_ (Real.sum_le_exp_of_nonneg (by norm_num) 7)