awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
hx : Finset.gcd Finset.univ x = 1
⊢ Ne (α := ι → ℚ) (Int.cast ∘ x) 0
have contrapose! : ∀ (hx : Eq (α := ι → ℚ) (Int.cast ∘ x) 0), Finset.gcd Finset.univ x ≠ 1
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
hx : Eq (α := ι → ℚ) (Int.cast ∘ x) 0
⊢ Finset.gcd Finset.univ x ≠ 1
have hx₁ : x = 0
Tactic: rw [Function.comp_eq_zero_iff x intCast_injective Rat.intCast_zero] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
hx : x = 0
⊢ Finset.gcd Finset.univ x ≠ 1
have rw : Ne (α := ℤ) 0 1
Tactic: rw [hx, Finset.gcd_eq_zero_iff.mpr (by simp)]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
hx : Finset.gcd Finset.univ x = 1
⊢ mulHeight (K := ℚ) (Int.cast ∘ x) = (↑(⨆ (i : ι), |x i|) : ℝ)
have hx₀ : Ne (α := ι → ℚ) (Int.cast ∘ x) 0
Tactic: have hx₀ : Int.cast ∘ x ≠ (0 : ι → ℚ) := by
    contrapose! hx
    rw [Function.comp_eq_zero_iff x intCast_injective Rat.intCast_zero] at hx
    rw [hx, Finset.gcd_eq_zero_iff.mpr (by simp)]
    exact zero_ne_one
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
hx : Finset.gcd Finset.univ x = 1
hx₀ : Ne (α := ι → ℚ) (Int.cast ∘ x) 0
⊢ mulHeight (K := ℚ) (Int.cast ∘ x) = (↑(⨆ (i : ι), |x i|) : ℝ)
have simp_rw : HMul.hMul (α := ℝ) (∏ x_1 : InfinitePlace ℚ, HPow.hPow (α := ℝ) (⨆ (i : ι), (↑|(Int.cast ∘ x) i| : ℝ)) x_1.mult)
    (∏ᶠ (v : FinitePlace ℚ), ⨆ (i : ι), (v : (a : ℚ) → ℝ) ((Int.cast ∘ x) i)) =
  ⨆ (i : ι), (↑|x i| : ℝ)
Tactic: simp_rw [Finite.map_iSup_of_monotone _ Int.cast_mono, NumberField.mulHeight_eq hx₀,
    infinitePlace_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
hx : Finset.gcd Finset.univ x = 1
⊢ logHeight (K := ℚ) (Int.cast ∘ x) = log (↑(⨆ (i : ι), |x i|) : ℝ)
have rw : log (mulHeight (K := ℚ) (Int.cast ∘ x)) = log (↑(⨆ (i : ι), |x i|) : ℝ)
Tactic: rw [logHeight_eq_log_mulHeight, mulHeight_eq_max_abs_of_gcd_eq_one hx]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
hx : Finset.gcd Finset.univ x = 1
rw : log (mulHeight (K := ℚ) (Int.cast ∘ x)) = log (↑(⨆ (i : ι), |x i|) : ℝ)
⊢ logHeight (K := ℚ) (Int.cast ∘ x) = log (↑(⨆ (i : ι), |x i|) : ℝ)
have rw₁ : log (↑(⨆ (i : ι), |x i|) : ℝ) = log (↑(⨆ (i : ι), |x i|) : ℝ)
Tactic: rw [logHeight_eq_log_mulHeight, mulHeight_eq_max_abs_of_gcd_eq_one hx]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (hypothesis)
Goal:
q : ℚ
⊢ mulHeight ![q, 1] = mulHeight (K := ℚ) ![(↑q.num : ℚ), (↑q.den : ℚ)]
have hq₀ : Ne (α := ℚ) (↑q.den : ℚ) 0
Tactic: have hq₀ : (q.den : ℚ) ≠ 0 := mod_cast q.den_nz
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
q : ℚ
hq₀ : Ne (α := ℚ) (↑q.den : ℚ) 0
⊢ mulHeight ![q, 1] = mulHeight (K := ℚ) ![(↑q.num : ℚ), (↑q.den : ℚ)]
have rw : mulHeight (HSMul.hSMul (α := ℚ) (↑q.den : ℚ) ![q, 1]) = mulHeight (K := ℚ) ![(↑q.num : ℚ), (↑q.den : ℚ)]
Tactic: rw [← mulHeight_smul_eq_mulHeight _ hq₀]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
q : ℚ
⊢ mulHeight₁ q = (↑(max q.num.natAbs q.den) : ℝ)
have rw : mulHeight (K := ℚ) ![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] = (↑(max q.num.natAbs q.den) : ℝ)
Tactic: rw [mulHeight₁_eq_mulHeight, mulHeight_self_one_eq_mulHeight_num_den, ← intCast_natCast q.den]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (hypothesis)
Goal:
q : ℚ
⊢ mulHeight (K := ℚ) ![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] = (↑(max q.num.natAbs q.den) : ℝ)
have this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
Tactic: have : (.univ : Finset (Fin 2)).gcd ![q.num, q.den] = 1 := by
    simpa [Finset.univ_fin2, Int.normalize_coe_nat, ← Int.coe_gcd q.num q.den] using
      Int.isCoprime_iff_gcd_eq_one.mp <| isCoprime_num_den q
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
⊢ mulHeight (K := ℚ) ![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] = (↑(max q.num.natAbs q.den) : ℝ)
have h : Eq (α := Fin (Nat.succ 0).succ → ℚ) ![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] (Int.cast ∘ ![q.num, (↑q.den : ℤ)])
Tactic: convert! mulHeight_eq_max_abs_of_gcd_eq_one this
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
h : Eq (α := Fin (Nat.succ 0).succ → ℚ) ![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] (Int.cast ∘ ![q.num, (↑q.den : ℤ)])
⊢ mulHeight (K := ℚ) ![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] = (↑(max q.num.natAbs q.den) : ℝ)
have h₁ : Eq (α := ℝ) (↑(max q.num.natAbs q.den) : ℝ) (↑(⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|) : ℝ)
Tactic: convert! mulHeight_eq_max_abs_of_gcd_eq_one this
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
⊢ Eq (α := Fin (Nat.succ 0).succ → ℚ) ![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] (Int.cast ∘ ![q.num, (↑q.den : ℤ)])
have h : ∀ (i : Fin (Nat.succ 0).succ),
  Eq (α := ℚ) (![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] i) ((Int.cast ∘ ![q.num, (↑q.den : ℤ)]) i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
i : Fin (Nat.succ 0).succ
⊢ Eq (α := ℚ) (![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] i) ((Int.cast ∘ ![q.num, (↑q.den : ℤ)]) i)
have h : Eq (α := ℚ) (![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩))
  ((Int.cast ∘ ![q.num, (↑q.den : ℤ)]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
i : Fin (Nat.succ 0).succ
h :
  Eq (α := ℚ) (![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩))
    ((Int.cast ∘ ![q.num, (↑q.den : ℤ)]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩))
⊢ Eq (α := ℚ) (![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] i) ((Int.cast ∘ ![q.num, (↑q.den : ℤ)]) i)
have h₁ : Eq (α := ℚ) (![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩))
  ((Int.cast ∘ ![q.num, (↑q.den : ℤ)]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
⊢ Eq (α := ℝ) (↑(max q.num.natAbs q.den) : ℝ) (↑(⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|) : ℝ)
have h : Eq (α := ℤ) (↑(max q.num.natAbs q.den) : ℤ) (⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|)
Tactic: rw [← Int.cast_natCast, Int.cast_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
⊢ Eq (α := ℤ) (↑(max q.num.natAbs q.den) : ℤ) (⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|)
have h : max |q.num| (↑q.den : ℤ) = ⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
⊢ max |q.num| (↑q.den : ℤ) = ⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|
have h : |q.num| ≤ ⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|
Tactic: refine le_antisymm (max_le ?_ ?_) <| ciSup_le fun i ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
h : |q.num| ≤ ⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|
⊢ max |q.num| (↑q.den : ℤ) = ⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|
have h₁ : LE.le (α := ℤ) (↑q.den : ℤ) (⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|)
Tactic: refine le_antisymm (max_le ?_ ?_) <| ciSup_le fun i ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
h : |q.num| ≤ ⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|
h₁ : LE.le (α := ℤ) (↑q.den : ℤ) (⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|)
⊢ max |q.num| (↑q.den : ℤ) = ⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|
have h₂ : ∀ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i| ≤ max |q.num| (↑q.den : ℤ)
Tactic: refine le_antisymm (max_le ?_ ?_) <| ciSup_le fun i ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
i : Fin 2
⊢ |![q.num, (↑q.den : ℤ)] i| ≤ max |q.num| (↑q.den : ℤ)
have h : |![q.num, (↑q.den : ℤ)] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))| ≤ max |q.num| (↑q.den : ℤ)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
i : Fin 2
h : |![q.num, (↑q.den : ℤ)] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))| ≤ max |q.num| (↑q.den : ℤ)
⊢ |![q.num, (↑q.den : ℤ)] i| ≤ max |q.num| (↑q.den : ℤ)
have h₁ : |![q.num, (↑q.den : ℤ)] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))| ≤ max |q.num| (↑q.den : ℤ)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
q : ℚ
⊢ logHeight₁ q = log (↑(max q.num.natAbs q.den) : ℝ)
have rw : log (mulHeight₁ q) = log (↑(max q.num.natAbs q.den) : ℝ)
Tactic: rw [logHeight₁_eq_log_mulHeight₁, mulHeight₁_eq_max]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
q : ℚ
rw : log (mulHeight₁ q) = log (↑(max q.num.natAbs q.den) : ℝ)
⊢ logHeight₁ q = log (↑(max q.num.natAbs q.den) : ℝ)
have rw₁ : log (↑(max q.num.natAbs q.den) : ℝ) = log (↑(max q.num.natAbs q.den) : ℝ)
Tactic: rw [logHeight₁_eq_log_mulHeight₁, mulHeight₁_eq_max]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Projectivization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
a b : { v : ι → K // v ≠ 0 }
t : K
h : (↑a : ι → K) = t • (↑b : ι → K)
⊢ t ≠ 0
have contrapose! : ∀ (h : t = 0), (↑a : ι → K) ≠ t • (↑b : ι → K)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Projectivization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : Projectivization K (ι → K)
⊢ x.logHeight = log x.mulHeight
have rw : logHeight (mk K x.rep sorry) = log (mulHeight (mk K x.rep sorry))
Tactic: rw [← x.mk_rep, mulHeight_mk, logHeight_mk, Height.logHeight]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Projectivization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : Projectivization K (ι → K)
rw : logHeight (mk K x.rep ⋯) = log (mulHeight (mk K x.rep ⋯))
⊢ x.logHeight = log x.mulHeight
have rw₁ : logHeight (mk K x.rep sorry) = log (Height.mulHeight x.rep)
Tactic: rw [← x.mk_rep, mulHeight_mk, logHeight_mk, Height.logHeight]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Projectivization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : Projectivization K (ι → K)
rw : logHeight (mk K x.rep ⋯) = log (mulHeight (mk K x.rep ⋯))
rw₁ : logHeight (mk K x.rep ⋯) = log (Height.mulHeight x.rep)
⊢ x.logHeight = log x.mulHeight
have rw₂ : Height.logHeight x.rep = log (Height.mulHeight x.rep)
Tactic: rw [← x.mk_rep, mulHeight_mk, logHeight_mk, Height.logHeight]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Projectivization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : Projectivization K (ι → K)
rw : logHeight (mk K x.rep ⋯) = log (mulHeight (mk K x.rep ⋯))
rw₁ : logHeight (mk K x.rep ⋯) = log (Height.mulHeight x.rep)
rw₂ : Height.logHeight x.rep = log (Height.mulHeight x.rep)
⊢ x.logHeight = log x.mulHeight
have rw₃ : log (Height.mulHeight x.rep) = log (Height.mulHeight x.rep)
Tactic: rw [← x.mk_rep, mulHeight_mk, logHeight_mk, Height.logHeight]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Projectivization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : Projectivization K (ι → K)
⊢ 1 ≤ x.mulHeight
have rw : 1 ≤ Height.mulHeight x.rep
Tactic: rw [← x.mk_rep, mulHeight_mk]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Projectivization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : Projectivization K (ι → K)
⊢ 0 ≤ x.logHeight
have rw : 0 ≤ log x.mulHeight
Tactic: rw [logHeight_eq_log_mulHeight]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : Fintype R
inst_2 : CommRing R'
χ ψ : MulChar R R'
⊢ jacobiSum χ ψ = jacobiSum ψ χ
have simp : Eq.{u_2 + 1} (α := R')
  (∑ x : R, HMul.hMul (α := R') (β := R') ((ψ : (a : R) → R') (1 - x) : R') ((χ : (a : R) → R') x : R'))
  (∑ x : R, HMul.hMul (α := R') (β := R') ((ψ : (a : R) → R') x : R') ((χ : (a : R) → R') (1 - x) : R'))
Tactic: simp only [jacobiSum, mul_comm (χ _)]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : Fintype R
inst_2 : CommRing R'
χ ψ : MulChar R R'
⊢ Eq.{u_2 + 1} (α := R')
    (∑ x : R, HMul.hMul (α := R') (β := R') ((ψ : (a : R) → R') (1 - x) : R') ((χ : (a : R) → R') x : R'))
    (∑ x : R, HMul.hMul (α := R') (β := R') ((ψ : (a : R) → R') x : R') ((χ : (a : R) → R') (1 - x) : R'))
have rw : Eq.{u_2 + 1} (α := R')
  (∑ i : R,
    HMul.hMul (α := R') (β := R')
      ((ψ : (a : R) → R') (HSub.hSub (α := R) (β := R) (1 : R) ((Equiv.subLeft 1 : (a : R) → R) i : R)) : R')
      ((χ : (a : R) → R') ((Equiv.subLeft 1 : (a : R) → R) i : R) : R'))
  (∑ x : R, HMul.hMul (α := R') (β := R') ((ψ : (a : R) → R') x : R') ((χ : (a : R) → R') (1 - x) : R'))
Tactic: rw [← (Equiv.subLeft 1).sum_comp]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : Fintype F
inst_3 : DecidableEq F
inst_4 : CommRing R
χ ψ : MulChar F R
⊢ jacobiSum χ ψ =
    ∑ x ∈ univ \ {0, 1}, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((ψ : (a : F) → R) (1 - x) : R)
have simp : Eq.{u_2 + 1} (α := R)
  (∑ x ∈ {0, 1}, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((ψ : (a : F) → R) (1 + -x) : R)) 0
Tactic: simp only [jacobiSum, subset_univ, sum_sdiff_eq_sub, sub_eq_add_neg, left_eq_add,
    neg_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : Fintype F
inst_3 : DecidableEq F
inst_4 : CommRing R
χ ψ : MulChar F R
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x ∈ {0, 1}, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((ψ : (a : F) → R) (1 + -x) : R)) 0
have h : ∀ (x : F),
  Membership.mem (γ := Finset F) {0, 1} x →
    HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((ψ : (a : F) → R) (1 + -x) : R) = 0
Tactic: apply sum_eq_zero
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : Fintype F
inst_3 : DecidableEq F
inst_4 : CommRing R
χ ψ : MulChar F R
| ∑ x : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((ψ : (a : F) → R) (1 - x) : R) =
    HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
      ∑ x ∈ univ \ {0, 1},
        HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
          HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R)
have h : ∀ (x : F), HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((ψ : (a : F) → R) (1 - x) : R)
Tactic: enter [1, 2, x]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : Fintype F
inst_3 : DecidableEq F
inst_4 : CommRing R
χ ψ : MulChar F R
x : F
| HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((ψ : (a : F) → R) (1 - x) : R)
have h : HAdd.hAdd (α := R) (β := R) ((χ : (a : F) → R) x : R) ((ψ : (a : F) → R) (1 - x) : R) - 1 +
  HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
    HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R)
Tactic: rw [show ∀ x y : R, x * y = x + y - 1 + (x - 1) * (y - 1) by intros; ring]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : Fintype F
inst_3 : DecidableEq F
inst_4 : CommRing R
χ ψ : MulChar F R
| ∑ x : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((ψ : (a : F) → R) (1 - x) : R) =
    HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
      ∑ x ∈ univ \ {0, 1},
        HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
          HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R)
have h : ∀ (x : F),
  HAdd.hAdd (α := R) (β := R) ((χ : (a : F) → R) x : R) ((ψ : (a : F) → R) (1 - x) : R) - 1 +
    HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
      HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R)
Tactic: enter [1, 2, x]
    rw [show ∀ x y : R, x * y = x + y - 1 + (x - 1) * (y - 1) by intros; ring]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : Fintype F
inst_3 : DecidableEq F
inst_4 : CommRing R
χ ψ : MulChar F R
⊢ ∑ x : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((ψ : (a : F) → R) (1 - x) : R) =
    HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
      ∑ x ∈ univ \ {0, 1},
        HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
          HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R)
have conv : ∑ x : F,
    (HAdd.hAdd (α := R) (β := R) ((χ : (a : F) → R) x : R) ((ψ : (a : F) → R) (1 - x) : R) - 1 +
      HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
        HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R)) =
  HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
    ∑ x ∈ univ \ {0, 1},
      HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
        HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R)
Tactic: conv =>
    enter [1, 2, x]
    rw [show ∀ x y : R, x * y = x + y - 1 + (x - 1) * (y - 1) by intros; ring]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : Fintype F
inst_3 : DecidableEq F
inst_4 : CommRing R
χ ψ : MulChar F R
⊢ ∑ x : F,
      (HAdd.hAdd (α := R) (β := R) ((χ : (a : F) → R) x : R) ((ψ : (a : F) → R) (1 - x) : R) - 1 +
        HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
          HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R)) =
    HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
      ∑ x ∈ univ \ {0, 1},
        HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
          HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R)
have rw : HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) (1 - x)) - ∑ x : F, 1 +
    ∑ x : F,
      HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
        HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
  HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
    ∑ x ∈ univ \ {0, 1},
      HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
        HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R)
Tactic: rw [sum_add_distrib, sum_sub_distrib, sum_add_distrib]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : Fintype F
inst_3 : DecidableEq F
inst_4 : CommRing R
χ ψ : MulChar F R
| HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) (1 - x)) - ∑ x : F, 1 +
      ∑ x : F,
        HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
          HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
    HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
      ∑ x ∈ univ \ {0, 1},
        HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
          HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R)
have h : ∀ (x : F), ((ψ : (a : F) → R) (1 - x) : R)
Tactic: enter [1, 1, 1, 2, 2, x]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : Fintype F
inst_3 : DecidableEq F
inst_4 : CommRing R
χ ψ : MulChar F R
x : F
| ((ψ : (a : F) → R) (1 - x) : R)
have h : ((ψ : (a : F) → R) ((Equiv.subLeft 1 : (a : F) → F) x : F) : R)
Tactic: rw [← Equiv.subLeft_apply 1]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : Fintype F
inst_3 : DecidableEq F
inst_4 : CommRing R
χ ψ : MulChar F R
| HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) (1 - x)) - ∑ x : F, 1 +
      ∑ x : F,
        HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
          HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
    HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
      ∑ x ∈ univ \ {0, 1},
        HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
          HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R)
have h : ∀ (x : F), ((ψ : (a : F) → R) ((Equiv.subLeft 1 : (a : F) → F) x : F) : R)
Tactic: enter [1, 1, 1, 2, 2, x]; rw [← Equiv.subLeft_apply 1]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : Fintype F
inst_3 : DecidableEq F
inst_4 : CommRing R
χ ψ : MulChar F R
⊢ HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) (1 - x)) - ∑ x : F, 1 +
      ∑ x : F,
        HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
          HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
    HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
      ∑ x ∈ univ \ {0, 1},
        HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
          HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R)
have conv : HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) ((Equiv.subLeft 1 : (a : F) → F) x : F)) -
      ∑ x : F, 1 +
    ∑ x : F,
      HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
        HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
  HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
    ∑ x ∈ univ \ {0, 1},
      HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
        HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R)
Tactic: conv => enter [1, 1, 1, 2, 2, x]; rw [← Equiv.subLeft_apply 1]