awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.GaussSum
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)
⊢ HPow.hPow (β := ℕ) (2 * (τ - HPow.hPow (β := ℕ) τ 3)) 2 = 8

Tactic:
linear_combination (4 * τ ^ 2 - 8) * τ_spec

Premises used: HMul.hMul, HSub.hSub, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.GaussSum
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)
⊢ HPow.hPow (β := ℕ) (gaussSum χ ψ₈char) 2 =
    HMul.hMul (α := FF) (β := FF) ((χ : (a : ZMod 8) → FF) (-1) : FF) ((↑(Fintype.card (ZMod 8)) : FF) : FF)

Tactic:
have hg : gaussSum χ ψ₈char ^ 2 = χ (-1) * Fintype.card (ZMod 8) := by
    rw [hχ, one_mul, ZMod.card, Nat.cast_ofNat, hg₁]
    linear_combination (4 * τ ^ 2 - 8) * τ_spec
-- Module: Mathlib.NumberTheory.GaussSum
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)
⊢ 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
-- Module: Mathlib.NumberTheory.GaussSum
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 (α := 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

Premises used: ringChar, Nat.cast_pow, one_mul, ZMod.card
-- Module: Mathlib.NumberTheory.GaussSum
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)
convert_2 : HPow.hPow (α := F) 8 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)
⊢ HPow.hPow (α := F) 2 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)

Tactic:
convert_to (8 : F) ^ (Fintype.card F / 2) = _

Premises used: Fintype.card, HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.NumberTheory.GaussSum
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)
⊢ 8 = HPow.hPow (α := F) (β := ℕ) 2 2 * 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.GaussSum
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)
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)
⊢ HPow.hPow (α := F) 8 (Fintype.card F / 2) = (↑((χ₈ : (a : ZMod 8) → ℤ) (↑(Fintype.card F) : ZMod 8)) : F)

Tactic:
apply (algebraMap F FF).injective

Premises used: Algebra.algebraMap, RingHom.injective
-- Module: Mathlib.NumberTheory.GaussSum
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)
⊢ 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:
simpa only [map_pow, map_ofNat, map_intCast, Nat.cast_ofNat] using h

Premises used: Nat.cast_ofNat, map_ofNat, map_intCast, map_pow
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
rw : Eq (α := ℚ) (∑ x ∈ Finset.Ico (HAdd.hAdd (α := ℕ) 0 1) (n + 1), (↑x : ℚ)⁻¹) (∑ i ∈ Finset.Icc 1 n, (↑i : ℚ)⁻¹)
⊢ harmonic n = ∑ i ∈ Finset.Icc 1 n, (↑i : ℚ)⁻¹

Tactic:
rw [harmonic, Finset.range_eq_Ico, Finset.sum_Ico_add' (fun (i : ℕ) ↦ (i : ℚ)⁻¹) 0 n (c := 1)]

Premises used: Nat.cast, Finset.sum_Ico_add', Inv.inv, Finset.range_eq_Ico, harmonic, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
⊢ Eq (α := ℚ) (∑ x ∈ Finset.Ico (HAdd.hAdd (α := ℕ) 0 1) (n + 1), (↑x : ℚ)⁻¹) (∑ i ∈ Finset.Icc 1 n, (↑i : ℚ)⁻¹)

Tactic:
simp only [Finset.Ico_add_one_right_eq_Icc]

Premises used: Finset.Ico_add_one_right_eq_Icc
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
⊢ Real.log (↑(n + 1) : ℝ) = ∫ (x : ℝ) in (↑1 : ℝ)..(↑(n + 1) : ℝ), x⁻¹

Tactic:
?_
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑1 : ℝ)..(↑(n + 1) : ℝ), x⁻¹) (∑ d ∈ Finset.Icc 1 n, (↑d : ℝ)⁻¹)

Tactic:
?_
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
⊢ Eq (α := ℝ) (∑ d ∈ Finset.Icc 1 n, (↑d : ℝ)⁻¹) (↑(harmonic n) : ℝ)

Tactic:
?_
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
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 : ℝ)⁻¹)
calc_3 : Eq (α := ℝ) (∑ d ∈ Finset.Icc 1 n, (↑d : ℝ)⁻¹) (↑(harmonic n) : ℝ)
⊢ Real.log (↑(n + 1) : ℝ) ≤ (↑(harmonic n) : ℝ)

Tactic:
calc _ = ∫ x in (1 : ℕ)..↑(n + 1), x⁻¹ := ?_
       _ ≤ ∑ d ∈ Finset.Icc 1 n, (d : ℝ)⁻¹ := ?_
       _ = harmonic n := ?_

Premises used: Finset.Icc, HAdd.hAdd, harmonic, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
⊢ ¬LE.le (α := ℝ) 1 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
⊢ 0 ∉ Set.uIcc 1 (↑(n + 1) : ℝ)

Tactic:
simp [(show ¬ (1 : ℝ) ≤ 0 by simp)]
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
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)
calc_1₂ calc_1₃ : Real.log (↑(n + 1) : ℝ) = Real.log (↑(n + 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]

Premises used: integral_inv, div_one, Nat.cast_one
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
⊢ LT.lt (α := ℝ) 0 (↑1 : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑1 : ℝ)..(↑(n + 1) : ℝ), x⁻¹) (∑ d ∈ Finset.Icc 1 n, (↑d : ℝ)⁻¹)

Tactic:
exact (inv_antitoneOn_Icc_right <| by simp).integral_le_sum_Ico (Nat.le_add_left 1 n)

Premises used: Nat.le_add_left, AntitoneOn.integral_le_sum_Ico, inv_antitoneOn_Icc_right, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
⊢ Eq (α := ℝ) (∑ d ∈ Finset.Icc 1 n, (↑d : ℝ)⁻¹) (↑(harmonic n) : ℝ)

Tactic:
simp only [harmonic_eq_sum_Icc, Rat.cast_sum, Rat.cast_inv, Rat.cast_natCast]

Premises used: Rat.cast_inv, Rat.cast_sum, Rat.cast_natCast, harmonic_eq_sum_Icc
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
pos : ∀ (hn0 : n = 0), (↑(harmonic n) : ℝ) ≤ 1 + Real.log (↑n : ℝ)
neg : ∀ (hn0 : ¬n = 0), (↑(harmonic n) : ℝ) ≤ 1 + Real.log (↑n : ℝ)
⊢ (↑(harmonic n) : ℝ) ≤ 1 + Real.log (↑n : ℝ)

Tactic:
by_cases hn0 : n = 0
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : n = 0
⊢ (↑(harmonic n) : ℝ) ≤ 1 + Real.log (↑n : ℝ)

Tactic:
simp [hn0]
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : ¬n = 0
⊢ 1 ≤ n

Tactic:
have hn : 1 ≤ n := Nat.one_le_iff_ne_zero.mpr hn0
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
neg : ∑ x ∈ Finset.Icc 1 n, (↑x : ℝ)⁻¹ ≤ 1 + Real.log (↑n : ℝ)
⊢ (↑(harmonic n) : ℝ) ≤ 1 + Real.log (↑n : ℝ)

Tactic:
simp_rw [harmonic_eq_sum_Icc, Rat.cast_sum, Rat.cast_inv, Rat.cast_natCast]

Premises used: Rat.cast_inv, Rat.cast_sum, Rat.cast_natCast, harmonic_eq_sum_Icc
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
neg : HAdd.hAdd (α := ℝ) 1 (∑ x ∈ (Finset.Icc 1 n).erase 1, (↑x : ℝ)⁻¹) ≤ 1 + Real.log (↑n : ℝ)
⊢ ∑ x ∈ Finset.Icc 1 n, (↑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]

Premises used: Iff.mpr, Finset.left_mem_Icc, inv_one, Finset.Icc, add_comm, Finset.sum_erase_add, OfNat.ofNat, Nat.cast_one
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
neg : ∑ x ∈ (Finset.Icc 1 n).erase 1, (↑x : ℝ)⁻¹ ≤ Real.log (↑n : ℝ)
⊢ HAdd.hAdd (α := ℝ) 1 (∑ x ∈ (Finset.Icc 1 n).erase 1, (↑x : ℝ)⁻¹) ≤ 1 + Real.log (↑n : ℝ)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
neg : ∑ x ∈ Finset.Ioc 1 n, (↑x : ℝ)⁻¹ ≤ Real.log (↑n : ℝ)
⊢ ∑ x ∈ (Finset.Icc 1 n).erase 1, (↑x : ℝ)⁻¹ ≤ Real.log (↑n : ℝ)

Tactic:
simp only [Finset.Icc_erase_left]

Premises used: Finset.Icc_erase_left
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
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)⁻¹)

Tactic:
?_
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ LE.le (α := ℝ) (∑ d ∈ Finset.Ico 2 (n + 1), (HSub.hSub (α := ℝ) (↑(d + 1) : ℝ) 1)⁻¹)
    (∫ (x : ℝ) in 2..(↑(n + 1) : ℝ), (x - 1)⁻¹)

Tactic:
?_
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 2..(↑(n + 1) : ℝ), (x - 1)⁻¹) (∫ (x : ℝ) in 1..(↑n : ℝ), x⁻¹)

Tactic:
?_
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∫ (x : ℝ) in 1..(↑n : ℝ), x⁻¹ = Real.log (↑n : ℝ)

Tactic:
?_
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
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⁻¹)
neg₃ : ∫ (x : ℝ) in 1..(↑n : ℝ), x⁻¹ = Real.log (↑n : ℝ)
⊢ ∑ x ∈ Finset.Ioc 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 := ?_

Premises used: HSub.hSub, Nat.cast, Real.log, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
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)⁻¹)
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)⁻¹)

Tactic:
simp_rw [Nat.cast_add, Nat.cast_one, add_sub_cancel_right]

Premises used: Nat.cast_add, add_sub_cancel_right, Nat.cast_one
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
linarith : n + 1 < 2 → -1 + HSub.hSub (α := ℤ) 1 (↑n : ℤ) + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 - 2) = 0
⊢ 2 ≤ n + 1

Tactic:
linarith [hn]
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ LT.lt (α := ℝ) 1 (↑2 : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ LE.le (α := ℝ) (∑ d ∈ Finset.Ico 2 (n + 1), (HSub.hSub (α := ℝ) (↑(d + 1) : ℝ) 1)⁻¹)
    (∫ (x : ℝ) in 2..(↑(n + 1) : ℝ), (x - 1)⁻¹)

Tactic:
exact @AntitoneOn.sum_le_integral_Ico 2 (n + 1) (fun x : ℝ ↦ (x - 1)⁻¹) (by linarith [hn]) <|
      sub_inv_antitoneOn_Icc_right (by simp)

Premises used: AntitoneOn.sum_le_integral_Ico, sub_inv_antitoneOn_Icc_right
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 2..(↑(n + 1) : ℝ), (x - 1)⁻¹)
    (∫ (x : ℝ) in HSub.hSub (α := ℝ) 2 1..HSub.hSub (α := ℝ) (↑(n + 1) : ℝ) 1, x⁻¹)

Tactic:
intervalIntegral.integral_comp_sub_right _ 1

Premises used: intervalIntegral.integral_comp_sub_right, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
h : 1 = HSub.hSub (α := ℝ) 2 1
h₁ : (↑n : ℝ) = HSub.hSub (α := ℝ) (↑(n + 1) : ℝ) 1
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 2..(↑(n + 1) : ℝ), (x - 1)⁻¹) (∫ (x : ℝ) in 1..(↑n : ℝ), x⁻¹)

Tactic:
convert! intervalIntegral.integral_comp_sub_right _ 1

Premises used: intervalIntegral.integral_comp_sub_right, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ 1 = HSub.hSub (α := ℝ) 2 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ (↑n : ℝ) = HSub.hSub (α := ℝ) (↑(n + 1) : ℝ) 1

Tactic:
simp only [Nat.cast_add, Nat.cast_one, add_sub_cancel_right]

Premises used: Nat.cast_add, add_sub_cancel_right, Nat.cast_one
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∫ (x : ℝ) in 1..(↑n : ℝ), x⁻¹ = Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) 1)

Tactic:
integral_inv _

Premises used: integral_inv
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
h : (↑n : ℝ) = HDiv.hDiv (α := ℝ) (↑n : ℝ) 1
neg : 0 ∉ Set.uIcc 1 (↑n : ℝ)
⊢ ∫ (x : ℝ) in 1..(↑n : ℝ), x⁻¹ = Real.log (↑n : ℝ)

Tactic:
convert! integral_inv _

Premises used: integral_inv
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
h h₁ : Eq (α := ℝ) (↑n : ℝ) (↑n : ℝ)
⊢ (↑n : ℝ) = HDiv.hDiv (α := ℝ) (↑n : ℝ) 1

Tactic:
rw [div_one]

Premises used: div_one
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ 0 ∉ Set.uIcc 1 (↑n : ℝ)

Tactic:
simp only [Nat.one_le_cast, hn, Set.uIcc_of_le, Set.mem_Icc, Nat.cast_nonneg,
        and_true, not_le, zero_lt_one]

Premises used: not_le, and_true, Nat.cast_nonneg, Set.uIcc_of_le, Nat.one_le_cast, zero_lt_one, Set.mem_Icc
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
y : ℝ
hy : 0 ≤ y
pos : ∀ (h0 : y = 0), Real.log y ≤ (↑(harmonic ⌊y⌋₊) : ℝ)
neg : ∀ (h0 : ¬y = 0), Real.log y ≤ (↑(harmonic ⌊y⌋₊) : ℝ)
⊢ Real.log y ≤ (↑(harmonic ⌊y⌋₊) : ℝ)

Tactic:
by_cases h0 : y = 0
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
y : ℝ
hy : 0 ≤ y
h0 : y = 0
⊢ Real.log y ≤ (↑(harmonic ⌊y⌋₊) : ℝ)

Tactic:
simp [h0]
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ Real.log y ≤ Real.log (↑(⌊y⌋₊ + 1) : ℝ)

Tactic:
?_
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ Real.log (↑(⌊y⌋₊ + 1) : ℝ) ≤ (↑(harmonic ⌊y⌋₊) : ℝ)

Tactic:
log_add_one_le_harmonic _

Premises used: log_add_one_le_harmonic
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
neg : Real.log y ≤ Real.log (↑(⌊y⌋₊ + 1) : ℝ)
⊢ Real.log y ≤ (↑(harmonic ⌊y⌋₊) : ℝ)

Tactic:
calc
      _ ≤ Real.log ↑(Nat.floor y + 1) := ?_
      _ ≤ _ := log_add_one_le_harmonic _

Premises used: log_add_one_le_harmonic, Nat.cast, Real.log, HAdd.hAdd, Nat.floor, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Harmonic.Bounds
Goal:
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
neg : y ≤ (↑(⌊y⌋₊ + 1) : ℝ)
⊢ Real.log y ≤ Real.log (↑(⌊y⌋₊ + 1) : ℝ)

Tactic:
gcongr