mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ n ^ φ n / (↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1)))).natAbs = n ^ φ n / ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))

pp: n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ ↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))) ∣ ↑n ^ φ n

Tactic:
Int.natAbs_natCast

Goal state after:
n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ n ^ φ n / ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1)) = n ^ φ n / ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))

n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ ↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))) ∣ ↑n ^ φ n
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case coprime
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
hK₂ :
  ∀ {K : Type u} [inst : Field K] [inst_1 : CharZero K] [hn : NeZero n₂] [hK : IsCyclotomicExtension {n₂} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₂), NumberField K → ℤ[hζ.toInteger] = ⊤
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this✝³ : NumberField K
this✝² : NeZero n₁
this✝¹ : NeZero n₂
this✝ : IsCyclotomicExtension {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : ℤ[hζ₁.toInteger] = ⊤
hζ₂ : IsPrimitiveRoot (ζ ^ n₁) n₂
this : IsCyclotomicExtension {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯
⊢ ℤ[hζ.toInteger] = ⊤

Tactic:
replace hζ₂ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂ :=
      IsPrimitiveRoot.coe_submonoidClass_iff.mp hζ₂

Goal state after:
case coprime
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
hK₂ :
  ∀ {K : Type u} [inst : Field K] [inst_1 : CharZero K] [hn : NeZero n₂] [hK : IsCyclotomicExtension {n₂} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₂), NumberField K → ℤ[hζ.toInteger] = ⊤
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this✝³ : NumberField K
this✝² : NeZero n₁
this✝¹ : NeZero n₂
this✝ : IsCyclotomicExtension {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : ℤ[hζ₁.toInteger] = ⊤
this : IsCyclotomicExtension {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯
hζ₂ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
⊢ ℤ[hζ.toInteger] = ⊤
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ w ((algebraMap (𝓞 K) K) ↑x) = 1 ∨ w ((algebraMap (𝓞 K) K) ↑x) = -1 ↔ w ((algebraMap (𝓞 K) K) ↑x) = 1

pp: K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ¬w ((algebraMap (𝓞 K) K) ↑x) = 0

pp: K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ¬↑w.mult = 0

Tactic:
or_iff_left

Goal state after:
K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ w ((algebraMap (𝓞 K) K) ↑x) = 1 ↔ w ((algebraMap (𝓞 K) K) ↑x) = 1

K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ¬w ((algebraMap (𝓞 K) K) ↑x) = -1

K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ¬w ((algebraMap (𝓞 K) K) ↑x) = 0

K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ¬↑w.mult = 0
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case inl
n : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : NeZero n
inst✝ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot ((algebraMap (𝓞 K) K) ↑↑μ) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      (algebraMap (𝓞 K) K) ↑↑μ ^ (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this✝ : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Even n
⊢ torsionOrder K = n

Tactic:
apply dvd_antisymm

Goal state after:
case inl.a
n : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : NeZero n
inst✝ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot ((algebraMap (𝓞 K) K) ↑↑μ) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      (algebraMap (𝓞 K) K) ↑↑μ ^ (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this✝ : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Even n
⊢ torsionOrder K ∣ n

case a
n : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : NeZero n
inst✝ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot ((algebraMap (𝓞 K) K) ↑↑μ) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      (algebraMap (𝓞 K) K) ↑↑μ ^ (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this✝ : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Even n
⊢ n ∣ torsionOrder K
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝²¹ : CommRing A
inst✝²⁰ : Field K
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Field L
inst✝¹⁷ : Algebra A K
inst✝¹⁶ : Algebra B L
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Algebra K L
inst✝¹³ : Algebra A L
inst✝¹² : IsScalarTower A K L
inst✝¹¹ : IsScalarTower A B L
inst✝¹⁰ : IsDomain A
inst✝⁹ : IsFractionRing A K
inst✝⁸ : FiniteDimensional K L
inst✝⁷ : Algebra.IsSeparable K L
inst✝⁶ : IsIntegralClosure B A L
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this✝ : Ideal.map (algebraMap A B) p ∣ a ^ e
this : ∀ x ∈ a, (intTrace A B) x ∈ p
⊢ ↑(P ^ (e - 1)) = ↑(P ^ (e - 1)) * (↑a / ↑a)

Tactic:
rw [div_self (by simpa), mul_one]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝²¹ : CommRing A
inst✝²⁰ : Field K
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Field L
inst✝¹⁷ : Algebra A K
inst✝¹⁶ : Algebra B L
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Algebra K L
inst✝¹³ : Algebra A L
inst✝¹² : IsScalarTower A K L
inst✝¹¹ : IsScalarTower A B L
inst✝¹⁰ : IsDomain A
inst✝⁹ : IsFractionRing A K
inst✝⁸ : FiniteDimensional K L
inst✝⁷ : Algebra.IsSeparable K L
inst✝⁶ : IsIntegralClosure B A L
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : Ideal.map (algebraMap A B) p ∣ a ^ e
x : B
hx : x ∈ a
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x ^ e = 0

Tactic:
← map_pow,

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝²¹ : CommRing A
inst✝²⁰ : Field K
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Field L
inst✝¹⁷ : Algebra A K
inst✝¹⁶ : Algebra B L
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Algebra K L
inst✝¹³ : Algebra A L
inst✝¹² : IsScalarTower A K L
inst✝¹¹ : IsScalarTower A B L
inst✝¹⁰ : IsDomain A
inst✝⁹ : IsFractionRing A K
inst✝⁸ : FiniteDimensional K L
inst✝⁷ : Algebra.IsSeparable K L
inst✝⁶ : IsIntegralClosure B A L
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : Ideal.map (algebraMap A B) p ∣ a ^ e
x : B
hx : x ∈ a
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) (x ^ e) = 0
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ x ^ 3 - 1 = λ ^ 3 * (y * (y - 1) * (y - (↑η + 1)))

Tactic:
calc _ = (x - 1) * (x - 1 - λ) * (x - 1 - λ * (η + 1)) := by
          simp only [coe_eta, cube_sub_one_eq_mul hζ x]; ring
    _ = _ := by rw [hy]; ring

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ {n | n.Deficient}.Infinite

Tactic:
Set.infinite_iff_exists_gt

Goal state after:
⊢ ∀ (a : ℕ), ∃ b ∈ {n | n.Deficient}, a < b
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ {n | Even n ∧ n.Deficient}.Infinite

Tactic:
Set.infinite_iff_exists_gt

Goal state after:
⊢ ∀ (a : ℕ), ∃ b ∈ {n | Even n ∧ n.Deficient}, a < b
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ {n | Odd n ∧ n.Deficient}.Infinite

Tactic:
Set.infinite_iff_exists_gt

Goal state after:
⊢ ∀ (a : ℕ), ∃ b ∈ {n | Odd n ∧ n.Deficient}, a < b
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ {n | Even n ∧ n.Abundant}.Infinite

Tactic:
Set.infinite_iff_exists_gt

Goal state after:
⊢ ∀ (a : ℕ), ∃ b ∈ {n | Even n ∧ n.Abundant}, a < b
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ {n | Odd n ∧ n.Abundant}.Infinite

Tactic:
Set.infinite_iff_exists_gt

Goal state after:
⊢ ∀ (a : ℕ), ∃ b ∈ {n | Odd n ∧ n.Abundant}, a < b
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case pos
inst✝ : Fact (Nat.Prime 2)
x : (ZMod 2)ˣ
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (2 / 2) = 1

Tactic:
simp only [eq_iff_true_of_subsingleton, exists_const]

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

Goal state before:
pp: case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : b = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Tactic:
rw [hb, mul_zero, quadraticCharFun_zero, mul_zero]

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

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ χ₈ ↑(Fintype.card F) = 1 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Tactic:
χ₈_nat_eq_if_mod_eight

Goal state after:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ (if Fintype.card F % 2 = 0 then 0 else if Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 7 then 1 else -1) = 1 ↔
    Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
P Q : Ideal B
hP : P * Q = Ideal.map (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : (intTrace A B) x ∉ p
⊢ ¬P ∣ differentIdeal A B

Tactic:
by_cases hp : p = ⊥
  · subst hp
    simp only [Ideal.map_bot, Ideal.mul_eq_bot] at hP
    obtain (rfl | rfl) := hP
    · rw [← Ideal.zero_eq_bot, zero_dvd_iff]
      exact differentIdeal_ne_bot
    · obtain rfl := hxQ
      simp at hx
  let : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap (by
      rw [← Ideal.map_le_iff_le_comap, ← hP]
      exact Ideal.mul_le_right)
  let K := FractionRing A
  let L := FractionRing B
  have : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L :=
    IsIntegralClosure.isLocalization _ K _ _
  have : FiniteDimensional K L := .of_isLocalization A B A⁰
  rw [Ideal.dvd_iff_le]
  intro H
  replace H := (mul_le_mul_left H Q).trans_eq hP
  replace H := (FractionalIdeal.coeIdeal_le_coeIdeal' _ (P := L) le_rfl).mpr H
  rw [FractionalIdeal.coeIdeal_mul, coeIdeal_differentIdeal A K] at H
  replace H := mul_le_mul_right H (FractionalIdeal.dual A K 1)
  have hne : (1 : FractionalIdeal B⁰ L) ≠ 0 := one_ne_zero
  rw [mul_inv_cancel_left₀ (FractionalIdeal.dual_ne_zero A K hne)] at H
  apply hx
  suffices Algebra.trace K L (algebraMap B L x) ∈ (p : FractionalIdeal A⁰ K) by
    obtain ⟨y, hy, e⟩ := this
    rw [← Algebra.algebraMap_intTrace (A := A), Algebra.linearMap_apply,
      (IsLocalization.injective _ le_rfl).eq_iff] at e
    exact e ▸ hy
  refine FractionalIdeal.mul_induction_on (H ⟨_, hxQ, rfl⟩) ?_ ?_
  · rintro x hx _ ⟨y, hy, rfl⟩
    induction hy using Submodule.span_induction generalizing x with
    | mem y h =>
      obtain ⟨y, hy, rfl⟩ := h
      obtain ⟨z, hz⟩ :=
        (FractionalIdeal.mem_dual (by simp)).mp hx 1 ⟨1, trivial, (algebraMap B L).map_one⟩
      simp only [Algebra.traceForm_apply, mul_one] at hz
      refine ⟨z * y, Ideal.mul_mem_left _ _ hy, ?_⟩
      rw [Algebra.linearMap_apply, Algebra.linearMap_apply, mul_comm x,
        ← IsScalarTower.algebraMap_apply,
        ← Algebra.smul_def, LinearMap.map_smul_of_tower, ← hz,
        Algebra.smul_def, map_mul, mul_comm]
    | zero => simp
    | add y z _ _ hy hz =>
      simp only [map_add, mul_add]
      exact Submodule.add_mem _ (hy x hx) (hz x hx)
    | smul y z hz IH =>
      simpa [Algebra.smul_def, mul_assoc, -FractionalIdeal.mem_coeIdeal, mul_left_comm x] using
        IH _ (Submodule.smul_mem _ y hx)
  · simp only [map_add]
    exact fun _ _ h₁ h₂ ↦ Submodule.add_mem _ h₁ h₂

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
inst✝¹ : Finite (A ⧸ p)
P Q : Ideal B
inst✝ : P.IsMaximal
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
⊢ Ideal.under A P ≠ ⊤

pp: case refine_2
A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
inst✝¹ : Finite (A ⧸ p)
P Q : Ideal B
inst✝ : P.IsMaximal
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
⊢ p ≤ Ideal.under A P

Tactic:
· simpa using ‹P.IsMaximal›.ne_top

Goal state after:
case refine_2
A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
inst✝¹ : Finite (A ⧸ p)
P Q : Ideal B
inst✝ : P.IsMaximal
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
⊢ p ≤ Ideal.under A P
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: case neg
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : ↑t ⊆ s
a : ↥t → ℤ
eq : ∑ i, a i • ↑↑i = ↑(setGcd s)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i, (-a i).toNat * ↑i
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
⊢ q * x + r + n ∈ span ↑(insert x t)

Tactic:
add_assoc

Goal state after:
case neg
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : ↑t ⊆ s
a : ↥t → ℤ
eq : ∑ i, a i • ↑↑i = ↑(setGcd s)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i, (-a i).toNat * ↑i
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
⊢ q * x + (r + n) ∈ span ↑(insert x t)
Module: Mathlib.NumberTheory.HeckeRing.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
Δ : Submonoid G
H₁ H₂ : Subgroup G
h : IsHeckeTriple Δ H₁ H₂
⊢ Δ ≤ (commensurator H₁).toSubmonoid

Tactic:
rw [h.commensurable.eq]
  exact h.le_commensurator_right

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

Goal state before:
pp: ⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, term (i + 1) 1) atTop (𝓝 (1 - γ))

Tactic:
change Tendsto (fun N ↦ termSum 1 N) atTop _

Goal state after:
⊢ Tendsto (fun N ↦ termSum 1 N) atTop (𝓝 (1 - γ))
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℕ
⊢ mulHeight₁ x ^ n = mulHeight₁ x ^ (↑n).natAbs

Tactic:
Int.natAbs_natCast

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℕ
⊢ mulHeight₁ x ^ n = mulHeight₁ x ^ n
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: ⊢ FermatLastTheoremFor 3

Tactic:
let K := CyclotomicField 3 ℚ

Goal state after:
K : Type := CyclotomicField 3 ℚ
⊢ FermatLastTheoremFor 3
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
α : Type u
inst✝¹ : Fintype α
ι : α → Type v
inst✝ : ∀ (a : α), Finite (ι a)
x : (a : α) → ι a → K
f : (a : α) → ι a
hf : ∀ (a : α), x a (f a) ≠ 0
⊢ ∃ a, ∏ a_1, x a_1 (a a_1) ≠ 0

Tactic:
exact ⟨f, prod_ne_zero_iff.mpr fun a _ ↦ hf a⟩

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

Goal state before:
pp: case e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N, 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1))

pp: case e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N, ↑(x + 1) / s * (1 / ↑(x + 1) ^ s - 1 / (↑(x + 1) + 1) ^ s) =
    1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)

Tactic:
· induction N with
    | zero => simp
    | succ N hN =>
      rw [Finset.sum_range_succ, hN, Nat.cast_add_one]
      ring_nf

Goal state after:
case e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N, ↑(x + 1) / s * (1 / ↑(x + 1) ^ s - 1 / (↑(x + 1) + 1) ^ s) =
    1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)
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
⊢ ∏ᶠ (w : FinitePlace K), w ((algebraMap (𝓞 K) K) a) / w ((algebraMap (𝓞 K) K) b) =
    (↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b)|)⁻¹

Tactic:
Rat.cast_abs,

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
⊢ ∏ᶠ (w : FinitePlace K), w ((algebraMap (𝓞 K) K) a) / w ((algebraMap (𝓞 K) K) b) =
    |↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b))|⁻¹
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e_a.e_a.succ
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ i ∈ Finset.range N, (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1) =
    ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s
⊢ ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s + -(↑N / (↑N + 1) ^ s) +
      (1 / (↑N + 1) ^ s + -(1 / (↑N + 1 + 1) ^ s)) * (↑N + 1) =
    ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s + 1 / (↑N + 1) ^ s + -((↑N + 1) / (↑N + 1 + 1) ^ s)

Tactic:
add_assoc

Goal state after:
case e_a.e_a.succ
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ i ∈ Finset.range N, (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1) =
    ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s
⊢ ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s +
      (-(↑N / (↑N + 1) ^ s) + (1 / (↑N + 1) ^ s + -(1 / (↑N + (1 + 1)) ^ s)) * (↑N + 1)) =
    ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s + (1 / (↑N + 1) ^ s + -((↑N + 1) / (↑N + (1 + 1)) ^ s))
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ logHeight₁ (x - y) ≤ ↑(totalWeight K) * log 2 + logHeight₁ x + logHeight₁ y

Tactic:
by
  rw [sub_eq_add_neg, ← logHeight₁_neg y]
  exact logHeight₁_add_le x (-y)

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Finite ι
x : ι → 𝓞 K
inst✝ : Nonempty ι
hx : ∀ (i : ι), x i ≠ 0
H : ∀ (j : ι), span {x j} ≠ ⊥
⊢ ↑(absNorm (span (Set.range x))) * ∏ᶠ (v : FinitePlace K), ⨆ i, v ↑(x i) = 1

Tactic:
have hx' : ⨆ i, span {x i} ≠ ⊥ :=
    iSup_eq_bot.not.mpr <| not_forall.mpr ⟨Classical.ofNonempty, H _⟩

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Finite ι
x : ι → 𝓞 K
inst✝ : Nonempty ι
hx : ∀ (i : ι), x i ≠ 0
H : ∀ (j : ι), span {x j} ≠ ⊥
hx' : ⨆ i, span {x i} ≠ ⊥
⊢ ↑(absNorm (span (Set.range x))) * ∏ᶠ (v : FinitePlace K), ⨆ i, v ↑(x i) = 1
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
h✝ : Nonempty ι'
q' : ι × ι' → K := fun a ↦ (eval x) (q a)
this : x ^ (M + N) = fun k ↦ ∑ j, (eval x) (q (k, j)) * (eval x) (p j)
⊢ mulHeight (x ^ (M + N)) ≤ ↑(Nat.card ι') ^ totalWeight K * mulHeight q' * mulHeight fun j ↦ (eval x) (p j)

Tactic:
simpa [this] using mulHeight_linearMap_apply_le q' _

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (totalWeight K - 1)
hv : ∀ (i : Fin 2), ↑(![a, ↑n] i) = ![↑a, ↑n] i
⊢ ↑n ^ (totalWeight K - 1) * ∏ᶠ (v : FinitePlace K), ⨆ i, v (![↑a, ↑n] i) = 1

Tactic:
simpa [ha₂, hv] using absNorm_mul_finprod_finitePlace_eq_one (show ![a, n] ≠ 0 by simp [hn])

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

Goal state before:
pp: case neg
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ C * mulHeight ![a * c, a * d, b * c, b * d]

Tactic:
convert! hC _ with i

Goal state after:
case e'_3
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
i : Fin (Nat.succ 0).succ.succ
⊢ ![a * c, a * d + b * c, b * d] i = (eval ![a * c, a * d, b * c, b * d]) (p i)
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
n : ℕ
hdeg : n < f.natDegree
a✝ : Nontrivial R
⊢ h.modByMonicHom (h.map X ^ n) = X ^ n

Tactic:
← map_pow,

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
n : ℕ
hdeg : n < f.natDegree
a✝ : Nontrivial R
⊢ h.modByMonicHom (h.map (X ^ n)) = X ^ n