mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
h : n < m
w : InfinitePlace K
hw : w ≠ w₁
⊢ w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB m)) < w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB n))

Tactic:
induction m with
  | zero =>
      exfalso
      exact Nat.not_succ_le_zero n h
  | succ m m_ih =>
      cases eq_or_lt_of_le (Nat.le_of_lt_succ h) with
      | inl hr =>
          rw [hr]
          exact (seq_next K w₁ hB (seq K w₁ hB m).prop).choose_spec.2.1 w hw
      | inr hr =>
          refine lt_trans ?_ (m_ih hr)
          exact (seq_next K w₁ hB (seq K w₁ hB m).prop).choose_spec.2.1 w hw

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
| ∃ B, minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B

Tactic:
congr

Goal state after:
case p
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
| fun B ↦ minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
let _ := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝ : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a₁✝ a₂✝ : Additive ((𝓞 K)ˣ ⧸ torsion K)
h :
  Multiplicative.toAdd
      ((⇑(QuotientGroup.kerLift (AddMonoidHom.toMultiplicativeRight (logEmbedding K))) ∘
          ⇑(QuotientGroup.quotientMulEquivOfEq ⋯))
        (Additive.toMul a₁✝)) =
    Multiplicative.toAdd
      ((⇑(QuotientGroup.kerLift (AddMonoidHom.toMultiplicativeRight (logEmbedding K))) ∘
          ⇑(QuotientGroup.quotientMulEquivOfEq ⋯))
        (Additive.toMul a₂✝))
⊢ a₁✝ = a₂✝

Tactic:
Function.comp_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a₁✝ a₂✝ : Additive ((𝓞 K)ˣ ⧸ torsion K)
h :
  Multiplicative.toAdd
      ((QuotientGroup.kerLift (AddMonoidHom.toMultiplicativeRight (logEmbedding K)))
        ((QuotientGroup.quotientMulEquivOfEq ⋯) (Additive.toMul a₁✝))) =
    Multiplicative.toAdd
      ((QuotientGroup.kerLift (AddMonoidHom.toMultiplicativeRight (logEmbedding K)))
        ((QuotientGroup.quotientMulEquivOfEq ⋯) (Additive.toMul a₂✝)))
⊢ a₁✝ = a₂✝
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x ζ : (𝓞 K)ˣ
f : Fin (rank K) → ℤ
hζ : ζ ∈ torsion K
h : x = ζ * ∏ i, fundSystem K i ^ f i
this : Additive.ofMul ↑x = ∑ i, f i • (basisModTorsion K) i
⊢ f = ⇑((basisModTorsion K).repr (Additive.ofMul ↑x))

Tactic:
← (basisModTorsion K).repr_sum_self f,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x ζ : (𝓞 K)ˣ
f : Fin (rank K) → ℤ
hζ : ζ ∈ torsion K
h : x = ζ * ∏ i, fundSystem K i ^ f i
this : Additive.ofMul ↑x = ∑ i, f i • (basisModTorsion K) i
⊢ ⇑((basisModTorsion K).repr (∑ i, f i • (basisModTorsion K) i)) = ⇑((basisModTorsion K).repr (Additive.ofMul ↑x))
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n m : ℕ
hn : n ≠ 0
hd : m ∣ n
⊢ m.abundancyIndex ≤ n.abundancyIndex

Tactic:
obtain ⟨k, hk⟩ := hd
  have hk0 : k ≠ 0 := by grind
  rw [abundancyIndex, abundancyIndex, hk, cast_mul, div_mul_eq_div_div_swap]
  refine div_le_div_of_nonneg_right ?_ m.cast_nonneg
  rw [le_div_iff₀ (by grind [cast_pos]), ← cast_mul, cast_le, sum_mul]
  exact (sum_image (f := fun i ↦ i) (mul_left_injective₀ hk0).injOn).symm.trans_le
    (sum_le_sum_of_subset (by grind [mul_dvd_mul_iff_right hk0]))

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
h : (quadraticChar F) (-1) = if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1
⊢ (if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1) = χ₄ ↑(Fintype.card F)

Tactic:
χ₄_eq_neg_one_pow (FiniteField.odd_card_of_char_ne_two hF)

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
h : (quadraticChar F) (-1) = if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1
⊢ (if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1) = (-1) ^ (Fintype.card F / 2)
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h : (quadraticChar (ZMod p)) ↑q = (quadraticChar (ZMod q)) (↑(χ₄ ↑p) * ↑p)
nc : ∀ (n r : ℕ), ↑↑n = ↑n
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))

Tactic:
have nc' : (((-1) ^ (p / 2) : ℤ) : ZMod q) = (-1) ^ (p / 2) := by norm_cast

Goal state after:
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h : (quadraticChar (ZMod p)) ↑q = (quadraticChar (ZMod q)) (↑(χ₄ ↑p) * ↑p)
nc : ∀ (n r : ℕ), ↑↑n = ↑n
nc' : ↑((-1) ^ (p / 2)) = (-1) ^ (p / 2)
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p ≠ q
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q

Tactic:
have qr := congr_arg (· * legendreSym p q) (quadratic_reciprocity hp hq h)

Goal state after:
case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p ≠ q
qr : legendreSym q ↑p * legendreSym p ↑q * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n : ℕ
h : 3 ^ ((n.fermatNumber - 1) / 2) = -1
⊢ 3 ^ 2 ^ (2 ^ n - 1) = 3 ^ ((n.fermatNumber - 1) / 2)

Tactic:
congr

Goal state after:
case e_a
n : ℕ
h : 3 ^ ((n.fermatNumber - 1) / 2) = -1
⊢ 2 ^ (2 ^ n - 1) = (n.fermatNumber - 1) / 2
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ b < ∑ k ∈ Finset.range b, a ^ k

Tactic:
calc
    b = ∑ _ ∈ Finset.range b, (1 : ℕ) := by simp
    _ < _ := by
      refine Finset.sum_lt_sum (fun i hi => Nat.one_le_pow _ _ (by lia)) ?_
      exact ⟨1, Finset.mem_range.mpr (by lia), by simpa using! ha⟩

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpaηb : p ∣ 1 * S.a + ↑η * S.b
hpaηsqb : p ∣ 1 * S.a + ↑η ^ 2 * S.b
this : p ∣ ↑η ^ 2 - ↑η
⊢ (↑η ^ 2 - ↑η) * ↑η * ↑η = (-↑η - 1 - ↑η) * (-↑η - 1)

Tactic:
rw [eta_sq, mul_assoc, ← pow_two, eta_sq]

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ (3 * S.multiplicity) ∣ (S.a + S.b) * (λ * S.y) * (λ * S.z)
this : 2 ≤ S.multiplicity
⊢ λ ^ (3 * S.multiplicity - 2) ∣ S.y * (S.z * (S.a + S.b))

Tactic:
show 3 * multiplicity S = 3 * multiplicity S - 2 + 1 + 1 by lia,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ (3 * S.multiplicity - 2 + 1 + 1) ∣ (S.a + S.b) * (λ * S.y) * (λ * S.z)
this : 2 ≤ S.multiplicity
⊢ λ ^ (3 * S.multiplicity - 2) ∣ S.y * (S.z * (S.a + S.b))
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ * λ ^ (3 * S.multiplicity - 2) * λ * λ ∣ (S.a + S.b) * (S.a + ↑η * S.b) * (S.a + ↑η ^ 2 * S.b)
⊢ False

Tactic:
simp only [← a_cube_add_b_cube_eq_mul, S.H, w_spec, Units.isUnit, IsUnit.dvd_mul_left] at h

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ * λ ^ (3 * S.multiplicity - 2) * λ * λ ∣ (λ ^ S.multiplicity * S.w) ^ 3
⊢ False
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
⊢ mulHeight (x ∘ f) ≤ mulHeight x

Tactic:
rw [mulHeight_eq h₀, mulHeight_eq hx]

Goal state after:
case inr.inr
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
⊢ (Multiset.map (fun v ↦ ⨆ i, v ((x ∘ f) i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((x ∘ f) i) ≤
    (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case h₂
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H : ∀ (v : AbsoluteValue K ℝ), ⨆ i, v ((x ∘ f) i) ≤ ⨆ i, v (x i)
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((x ∘ f) i) ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)

Tactic:
· exact finprod_le_finprod (hasFiniteMulSupport_iSup_nonarchAbsVal h₀)
      (fun v ↦ Real.iSup_nonneg_of_nonnegHomClass v.val _)
      (hasFiniteMulSupport_iSup_nonarchAbsVal hx) fun v ↦ H v.val

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
H : ∀ (v : AbsoluteValue K ℝ), ⨆ j, v (Sum.elim x 0 j) = ⨆ i, v (x i)
⊢ (Multiset.map (fun v ↦ ⨆ i, v (Sum.elim x 0 i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (Sum.elim x 0 i) =
    (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)

Tactic:
congr

Goal state after:
case inr.e_a.e_f
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
H : ∀ (v : AbsoluteValue K ℝ), ⨆ j, v (Sum.elim x 0 j) = ⨆ i, v (x i)
⊢ (fun v ↦ ⨆ i, v (Sum.elim x 0 i)) = fun v ↦ ⨆ i, v (x i)

case inr.e_a
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
H : ∀ (v : AbsoluteValue K ℝ), ⨆ j, v (Sum.elim x 0 j) = ⨆ i, v (x i)
⊢ (fun v ↦ ⨆ i, ↑v (Sum.elim x 0 i)) = fun v ↦ ⨆ i, ↑v (x i)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: this : Tendsto (fun x ↦ -(eulerMascheroniSeq' ∘ fun a ↦ a + 1) x) atTop (𝓝 (-γ))
n : ℕ
⊢ -(eulerMascheroniSeq' ∘ fun a ↦ a + 1) n = -↑(harmonic (n + 1)) + log (↑n + 1)

Tactic:
Function.comp_apply,

Goal state after:
this : Tendsto (fun x ↦ -(eulerMascheroniSeq' ∘ fun a ↦ a + 1) x) atTop (𝓝 (-γ))
n : ℕ
⊢ -eulerMascheroniSeq' (n + 1) = -↑(harmonic (n + 1)) + log (↑n + 1)
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
Y : 𝓞 K
hY : S.Y ^ 3 + 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : S.Z ^ 3 - 1 = λ ^ 2 * Z
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

pp: case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
Y : 𝓞 K
hY : S.Y ^ 3 + 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : S.Z ^ 3 + 1 = λ ^ 2 * Z
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

Tactic:
· refine ⟨1, X - Y - S.u₄ * Z, ?_⟩
    rw [show λ ^ 2 * (X - Y - S.u₄ * Z) = λ ^ 2 * X - λ ^ 2 * Y - S.u₄ * (λ ^ 2 * Z) by ring,
      ← hX, ← hY, ← hZ, ← formula2]
    ring

Goal state after:
case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
Y : 𝓞 K
hY : S.Y ^ 3 + 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : S.Z ^ 3 + 1 = λ ^ 2 * Z
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n
Module: Mathlib.NumberTheory.NumberField.ProductFormula

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ‖(embedding v) ↑x‖
t₂ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ↑(absNorm (v.maxPowDividing (span {x})))
h_fin₁ : t₁.Finite
v : HeightOneSpectrum (𝓞 K)
hv :
  ↑(absNorm v.asIdeal) ^ (Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors ≠ ↑(absNorm v.asIdeal) ^ 0
h : (Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors = 0
⊢ ↑(absNorm v.asIdeal) ^ (Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors = ↑(absNorm v.asIdeal) ^ 0

Tactic:
congr

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
⊢ (Multiset.map (fun v ↦ ⨆ i, v (x i.1 * y i.2)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i.1 * y i.2) =
    (Multiset.map (fun i ↦ (⨆ i_1, i (x i_1)) * ⨆ i_1, i (y i_1)) archAbsVal).prod *
      ∏ᶠ (i : ↑nonarchAbsVal), (⨆ i_1, ↑i (x i_1)) * ⨆ i_1, ↑i (y i_1)

Tactic:
congr

Goal state after:
case e_a.e_f
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
⊢ (fun v ↦ ⨆ i, v (x i.1 * y i.2)) = fun i ↦ (⨆ i_1, i (x i_1)) * ⨆ i_1, i (y i_1)

case e_a
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
⊢ (fun v ↦ ⨆ i, ↑v (x i.1 * y i.2)) = fun i ↦ (⨆ i_1, ↑i (x i_1)) * ⨆ i_1, ↑i (y i_1)
Module: Mathlib.NumberTheory.NumberField.ProductFormula

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ |↑((Algebra.norm ℤ) a) / ↑((Algebra.norm ℤ) b)| =
    |↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b))|

Tactic:
congr

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ ↑((Algebra.norm ℤ) a) / ↑((Algebra.norm ℤ) b) = ↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b))
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ mulHeight₁ (∑ a ∈ s, x a) ≤ ↑(#s) ^ totalWeight K * ∏ a ∈ s, mulHeight₁ (x a)

Tactic:
by
  simp only [mulHeight₁_eq, totalWeight]
  rw [prod_mul_distrib, ← prod_replicate, ← map_const, ← finprod_prod_comm _ _ (by fun_prop),
    ← prod_map_prod, ← mul_assoc, ← prod_map_mul]
  simp only [Function.const_apply]
  gcongr
  · exact finprod_nonneg fun _ ↦ by positivity
  · exact prod_map_nonneg fun _ h ↦ by positivity
  · exact prod_map_le_prod_map₀ _ _ (fun _ _ ↦ by positivity) fun _ _ ↦ max_abv_sum_one_le _ hs x
  · exact finprod_le_finprod (by fun_prop) (fun _ ↦ by grind) (by fun_prop) <|
      fun v ↦ max_abv_sum_one_le_of_isNonarchimedean (isNonarchimedean _ v.prop) _ x

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case h_bound
n : ℕ
⊢ ∀ x ∈ Ici 1,
    ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)), ‖(a - ↑(n + 1)) / a ^ (x + 1)‖ ≤ (a - ↑(n + 1)) / a ^ 2

Tactic:
intro s (hs : 1 ≤ s)

Goal state after:
case h_bound
n : ℕ
s : ℝ
hs : 1 ≤ s
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)), ‖(a - ↑(n + 1)) / a ^ (s + 1)‖ ≤ (a - ↑(n + 1)) / a ^ 2
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: h : Tendsto (slope Gammaℝ 1) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
⊢ Tendsto (fun s ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))

Tactic:
slope_fun_def_field,

Goal state after:
h : Tendsto (fun b ↦ (b.Gammaℝ - Gammaℝ 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
⊢ Tendsto (fun s ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x, χ x + ∑ i, ψ i - ∑ x, 1 + (∑ x, (χ x - 1) * (ψ (1 - x) - 1) - 0) =
    ∑ x, χ x + ∑ x, ψ x - ∑ x, 1 + (∑ x, (χ x - 1) * (ψ (1 - x) - 1) - ∑ x ∈ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1))

Tactic:
congr

Goal state after:
case e_a.e_a
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ 0 = ∑ x ∈ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case h₂
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : ¬n = 0
a : 𝓞 K
Hw : 0 < absNorm (span {↑n})
⊢ ∏ᶠ (v : FinitePlace K), ⨆ i, v ↑(![a, ↑n] i) = ∏ᶠ (v : FinitePlace K), ⨆ i, v (![↑a, ↑n] i)

Tactic:
congr

Goal state after:
case h₂
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : ¬n = 0
a : 𝓞 K
Hw : 0 < absNorm (span {↑n})
⊢ (fun v ↦ ⨆ i, v ↑(![a, ↑n] i)) = fun v ↦ ⨆ i, v (![↑a, ↑n] i)
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case h₂
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : ¬n = 0
a : 𝓞 K
Hw : 0 < absNorm (span {↑n})
x✝ : FinitePlace K
⊢ ⨆ i, x✝ ↑(![a, ↑n] i) = ⨆ i, x✝ (![↑a, ↑n] i)

Tactic:
congr

Goal state after:
case h₂
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : ¬n = 0
a : 𝓞 K
Hw : 0 < absNorm (span {↑n})
x✝ : FinitePlace K
⊢ (fun i ↦ x✝ ↑(![a, ↑n] i)) = fun i ↦ x✝ (![↑a, ↑n] i)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ (fun s ↦ (riemannZeta s)⁻¹ - (s - 1)) =o[𝓝[≠] 1] fun x ↦ x - 1

Tactic:
apply inv_riemannZeta_sub_sub_isBigO.trans_isLittleO
  suffices (· - 1) =o[𝓝 1] (fun _ : ℂ ↦ (1 : ℂ)) by
    simpa [pow_two] using (this.mul_isBigO <| isBigO_refl ..).mono nhdsWithin_le_nhds
  exact ContinuousAt.isLittleO (by fun_prop)

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: case mk.mk
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
map✝¹ : R[X] →ₐ[R] S
map_surjective✝¹ : Function.Surjective ⇑map✝¹
ker_map✝¹ : RingHom.ker map✝¹ = Ideal.span {f}
map✝ : R[X] →ₐ[R] S
map_surjective✝ : Function.Surjective ⇑map✝
ker_map✝ : RingHom.ker map✝ = Ideal.span {f}
eq :
  ∀ (x : R[X]),
    { map := map✝¹, map_surjective := map_surjective✝¹, ker_map := ker_map✝¹ }.map x =
      { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝ }.map x
⊢ { map := map✝¹, map_surjective := map_surjective✝¹, ker_map := ker_map✝¹ } =
    { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝ }

Tactic:
congr

Goal state after:
case mk.mk
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
map✝¹ : R[X] →ₐ[R] S
map_surjective✝¹ : Function.Surjective ⇑map✝¹
ker_map✝¹ : RingHom.ker map✝¹ = Ideal.span {f}
map✝ : R[X] →ₐ[R] S
map_surjective✝ : Function.Surjective ⇑map✝
ker_map✝ : RingHom.ker map✝ = Ideal.span {f}
eq :
  ∀ (x : R[X]),
    { map := map✝¹, map_surjective := map_surjective✝¹, ker_map := ker_map✝¹ }.map x =
      { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝ }.map x
⊢ map✝¹ = map✝
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x y : S
| h.repr (h.map (h.repr x + h.repr y)) %ₘ f

Tactic:
h.modByMonic_repr_map,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x y : S
| (h.repr x + h.repr y) %ₘ f
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
c : R
x : S
⊢ h.repr (h.map (C c * h.repr x)) %ₘ f = c • (h.repr (h.map (h.repr x)) %ₘ f)

Tactic:
h.modByMonic_repr_map,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
c : R
x : S
⊢ C c * h.repr x %ₘ f = c • (h.repr (h.map (h.repr x)) %ₘ f)
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
⊢ h.coeff z i = if hi : i < f.natDegree then (h.basis.repr z) ⟨i, hi⟩ else 0

Tactic:
split_ifs with hi

Goal state after:
case pos
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
hi : i < f.natDegree
⊢ h.coeff z i = (h.basis.repr z) ⟨i, hi⟩

case neg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
hi : ¬i < f.natDegree
⊢ h.coeff z i = 0