awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
h :
  ∀ (i : Fin (Nat.succ 0).succ),
    Eq (α := ℚ) (![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] i) ((Int.cast ∘ ![q.num, (↑q.den : ℤ)]) i)
⊢ Eq (α := Fin (Nat.succ 0).succ → ℚ) ![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] (Int.cast ∘ ![q.num, (↑q.den : ℤ)])

Tactic:
ext i
-- Module: Mathlib.NumberTheory.Height.NumberField
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, ⋯⟩))
h₁ :
  Eq (α := ℚ) (![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩))
    ((Int.cast ∘ ![q.num, (↑q.den : ℤ)]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩))
⊢ Eq (α := ℚ) (![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] i) ((Int.cast ∘ ![q.num, (↑q.den : ℤ)]) i)

Tactic:
fin_cases i
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
⊢ 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, ⋯⟩))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
⊢ Eq (α := ℚ) (![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩))
    ((Int.cast ∘ ![q.num, (↑q.den : ℤ)]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
h : Eq (α := ℤ) (↑(max q.num.natAbs q.den) : ℤ) (⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|)
⊢ Eq (α := ℝ) (↑(max q.num.natAbs q.den) : ℝ) (↑(⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|) : ℝ)

Tactic:
rw [← Int.cast_natCast, Int.cast_inj]

Premises used: Int.cast_natCast, Int.cast_inj
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
h : max |q.num| (↑q.den : ℤ) = ⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|
⊢ Eq (α := ℤ) (↑(max q.num.natAbs q.den) : ℤ) (⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.Height.NumberField
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|

Tactic:
le_antisymm (max_le ?_ ?_) <| ciSup_le fun i ↦ ?_

Premises used: le_antisymm, max_le, ciSup_le
-- Module: Mathlib.NumberTheory.Height.NumberField
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|)
h₂ : ∀ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i| ≤ max |q.num| (↑q.den : ℤ)
⊢ max |q.num| (↑q.den : ℤ) = ⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|

Tactic:
refine le_antisymm (max_le ?_ ?_) <| ciSup_le fun i ↦ ?_

Premises used: le_antisymm, max_le, ciSup_le
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
⊢ |q.num| ≤ |![q.num, (↑q.den : ℤ)] 0|

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
⊢ |q.num| ≤ ⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|

Tactic:
exact Finite.le_ciSup_of_le 0 <| by simp

Premises used: Finite.le_ciSup_of_le, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
⊢ (↑q.den : ℤ) ≤ |![q.num, (↑q.den : ℤ)] 1|

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
⊢ LE.le (α := ℤ) (↑q.den : ℤ) (⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|)

Tactic:
exact Finite.le_ciSup_of_le 1 <| by simp

Premises used: Finite.le_ciSup_of_le, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Height.NumberField
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 : ℤ)
h₁ : |![q.num, (↑q.den : ℤ)] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))| ≤ max |q.num| (↑q.den : ℤ)
⊢ |![q.num, (↑q.den : ℤ)] i| ≤ max |q.num| (↑q.den : ℤ)

Tactic:
fin_cases i
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
⊢ |![q.num, (↑q.den : ℤ)] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))| ≤ max |q.num| (↑q.den : ℤ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
⊢ |![q.num, (↑q.den : ℤ)] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))| ≤ max |q.num| (↑q.den : ℤ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
rw : log (mulHeight₁ q) = log (↑(max q.num.natAbs q.den) : ℝ)
rw₁ rw₂ : log (↑(max q.num.natAbs q.den) : ℝ) = log (↑(max q.num.natAbs q.den) : ℝ)
⊢ logHeight₁ q = log (↑(max q.num.natAbs q.den) : ℝ)

Tactic:
rw [logHeight₁_eq_log_mulHeight₁, mulHeight₁_eq_max]

Premises used: Rat.mulHeight₁_eq_max, Height.logHeight₁_eq_log_mulHeight₁
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
n : ℕ
inst : NeZero n
⊢ 1 ≤ n

Tactic:
grind [NeZero.ne n]

Premises used: NeZero.ne
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
n : ℕ
inst : NeZero n
⊢ mulHeight₁ (K := ℚ) (↑n : ℚ) = (↑n : ℝ)

Tactic:
simp [mulHeight₁_eq_max, show 1 ≤ n by grind [NeZero.ne n]]

Premises used: Rat.mulHeight₁_eq_max
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
n : ℕ
inst : NeZero n
⊢ logHeight₁ (K := ℚ) (↑n : ℚ) = Real.log (↑n : ℝ)

Tactic:
simp [logHeight₁_eq_log_mulHeight₁, mulHeight₁_natCast n]

Premises used: Rat.mulHeight₁_natCast, Height.logHeight₁_eq_log_mulHeight₁
-- Module: Mathlib.NumberTheory.Height.Projectivization
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)
contrapose! : ∀ (h : t = 0), (↑a : ι → K) ≠ t • (↑b : ι → K)
⊢ t ≠ 0

Tactic:
contrapose! h
-- Module: Mathlib.NumberTheory.Height.Projectivization
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 : t = 0
⊢ (↑a : ι → K) ≠ t • (↑b : ι → K)

Tactic:
simpa [h] using a.prop

Premises used: Subtype.prop
-- Module: Mathlib.NumberTheory.Height.Projectivization
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)
⊢ logHeight (↑a : ι → K) = logHeight (↑b : ι → K)

Tactic:
congrArg log <| mod_cast mulHeight_aux a b t h

Premises used: congrArg, _private.0.Projectivization.mulHeight_aux, cast, Real.log, Height.logHeight, Eq.refl, Subtype.val, Eq, Height.mulHeight
-- Module: Mathlib.NumberTheory.Height.Projectivization
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : ι → K
hx : x ≠ 0
⊢ mulHeight (mk K x hx) = Height.mulHeight x

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Height.Projectivization
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : ι → K
hx : x ≠ 0
⊢ logHeight (mk K x hx) = Height.logHeight x

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Height.Projectivization
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)
rw₃ rw₄ : log (Height.mulHeight x.rep) = log (Height.mulHeight x.rep)
⊢ x.logHeight = log x.mulHeight

Tactic:
rw [← x.mk_rep, mulHeight_mk, logHeight_mk, Height.logHeight]

Premises used: Projectivization.mulHeight_mk, Height.logHeight, Projectivization.mk_rep, Projectivization.logHeight_mk
-- Module: Mathlib.NumberTheory.Height.Projectivization
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : Projectivization K (ι → K)
rw : 1 ≤ Height.mulHeight x.rep
⊢ 1 ≤ x.mulHeight

Tactic:
rw [← x.mk_rep, mulHeight_mk]

Premises used: Projectivization.mulHeight_mk, Projectivization.mk_rep
-- Module: Mathlib.NumberTheory.Height.Projectivization
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : Projectivization K (ι → K)
⊢ 1 ≤ Height.mulHeight x.rep

Tactic:
Height.one_le_mulHeight _

Premises used: Height.one_le_mulHeight
-- Module: Mathlib.NumberTheory.Height.Projectivization
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : Projectivization K (ι → K)
⊢ 1 ≤ Height.mulHeight x.rep

Tactic:
exact Height.one_le_mulHeight _

Premises used: Height.one_le_mulHeight
-- Module: Mathlib.NumberTheory.Height.Projectivization
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : Projectivization K (ι → K)
⊢ 0 < x.mulHeight

Tactic:
zero_lt_one.trans_le <| one_le_mulHeight x

Premises used: Projectivization.one_le_mulHeight, zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.Height.Projectivization
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : Projectivization K (ι → K)
⊢ x.mulHeight ≠ 0

Tactic:
(mulHeight_pos x).ne'

Premises used: Projectivization.mulHeight_pos, LT.lt.ne'
-- Module: Mathlib.NumberTheory.Height.Projectivization
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : Projectivization K (ι → K)
rw : 0 ≤ log x.mulHeight
⊢ 0 ≤ x.logHeight

Tactic:
rw [logHeight_eq_log_mulHeight]

Premises used: Projectivization.logHeight_eq_log_mulHeight
-- Module: Mathlib.NumberTheory.Height.Projectivization
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : Projectivization K (ι → K)
⊢ 0 ≤ log x.mulHeight

Tactic:
log_nonneg <| x.one_le_mulHeight

Premises used: Projectivization.one_le_mulHeight, Real.log_nonneg
-- Module: Mathlib.NumberTheory.Height.Projectivization
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : Projectivization K (ι → K)
⊢ 0 ≤ log x.mulHeight

Tactic:
exact log_nonneg <| x.one_le_mulHeight

Premises used: Projectivization.one_le_mulHeight, Real.log_nonneg
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : Fintype R
inst_2 : CommRing R'
χ ψ : MulChar R R'
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'))
⊢ jacobiSum χ ψ = jacobiSum ψ χ

Tactic:
simp only [jacobiSum, mul_comm (χ _)]

Premises used: jacobiSum, mul_comm, DFunLike.coe
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : Fintype R
inst_2 : CommRing R'
χ ψ : MulChar R R'
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'))
⊢ 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:
rw [← (Equiv.subLeft 1).sum_comp]

Premises used: Equiv.subLeft, Equiv.sum_comp, OfNat.ofNat
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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')
    (∑ 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:
simp only [Equiv.subLeft_apply, sub_sub_cancel]

Premises used: sub_sub_cancel, Equiv.subLeft_apply
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : Fintype R
inst_2 : CommRing R'
R'' : Type u_3
inst_3 : CommRing R''
χ ψ : MulChar R R'
f : R' →+* R''
⊢ jacobiSum (χ.ringHomComp f) (ψ.ringHomComp f) = (f : (a : R') → R'') (jacobiSum χ ψ)

Tactic:
simp only [jacobiSum, MulChar.ringHomComp, MulChar.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    map_sum, map_mul]

Premises used: OneHom.coe_mk, MulChar.coe_mk, jacobiSum, map_sum, map_mul, MonoidHom.coe_mk, MulChar.ringHomComp
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
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
⊢ jacobiSum χ ψ =
    ∑ x ∈ univ \ {0, 1}, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((ψ : (a : F) → R) (1 - x) : R)

Tactic:
simp only [jacobiSum, subset_univ, sum_sdiff_eq_sub, sub_eq_add_neg, left_eq_add,
    neg_eq_zero]

Premises used: left_eq_add, Finset.sum_sdiff_eq_sub, sub_eq_add_neg, neg_eq_zero, jacobiSum, Finset.subset_univ
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
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
⊢ 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:
apply sum_eq_zero

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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),
    Membership.mem (γ := Finset F) {0, 1} x →
      HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((ψ : (a : F) → R) (1 + -x) : R) = 0

Tactic:
simp only [mem_insert, mem_singleton, forall_eq_or_imp, χ.map_zero, neg_zero, add_zero, map_one,
    mul_one, forall_eq, add_neg_cancel, ψ.map_zero, mul_zero, and_self]

Premises used: add_neg_cancel, Finset.mem_singleton, and_self, forall_eq, Finset.mem_insert, forall_eq_or_imp, MulZeroClass.mul_zero, map_one, mul_one, add_zero, neg_zero, MulChar.map_zero
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
h : ∀ (x : F), HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((ψ : (a : F) → R) (1 - x) : 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)

Tactic:
enter [1, 2, x]
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
x_1 y : R
⊢ x_1 * y = x_1 + y - 1 + (x_1 - 1) * (y - 1)

Tactic:
ring
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
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)
| HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((ψ : (a : F) → R) (1 - x) : R)

Tactic:
rw [show ∀ x y : R, x * y = x + y - 1 + (x - 1) * (y - 1) by intros; ring]
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
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)
| ∑ 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)

Tactic:
enter [1, 2, x]
    rw [show ∀ x y : R, x * y = x + y - 1 + (x - 1) * (y - 1) by intros; ring]
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
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)
⊢ ∑ 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)

Tactic:
conv =>
    enter [1, 2, x]
    rw [show ∀ x y : R, x * y = x + y - 1 + (x - 1) * (y - 1) by intros; ring]
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
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)
⊢ ∑ 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:
rw [sum_add_distrib, sum_sub_distrib, sum_add_distrib]

Premises used: Finset.sum_add_distrib, Finset.sum_sub_distrib
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
h : ∀ (x : F), ((ψ : (a : F) → R) (1 - x) : 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)

Tactic:
enter [1, 1, 1, 2, 2, x]
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
h : ((ψ : (a : F) → R) ((Equiv.subLeft 1 : (a : F) → F) x : F) : R)
| ((ψ : (a : F) → R) (1 - x) : R)

Tactic:
rw [← Equiv.subLeft_apply 1]

Premises used: Equiv.subLeft_apply, OfNat.ofNat
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
h : ∀ (x : F), ((ψ : (a : F) → R) ((Equiv.subLeft 1 : (a : F) → F) x : 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)

Tactic:
enter [1, 1, 1, 2, 2, x]; rw [← Equiv.subLeft_apply 1]

Premises used: Equiv.subLeft_apply, OfNat.ofNat
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
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
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)
⊢ 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:
conv => enter [1, 1, 1, 2, 2, x]; rw [← Equiv.subLeft_apply 1]

Premises used: Equiv.subLeft_apply, OfNat.ofNat