mathlib-initiative/mathlib-tactics huggingface dataset:
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
hp : ¬p = ⊥
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) L
this : FiniteDimensional K L
H : ↑Q ≤ FractionalIdeal.dual A K 1 * ↑(Ideal.map (algebraMap A B) p)
hne : 1 ≠ 0
y✝ : B
x : L
hx : x ∈ FractionalIdeal.dual A K 1
y : A
hy : y ∈ ↑p
⊢ 1 ≠ 0

Tactic:
simp

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

Goal state before:
pp: case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
hy : y ≠ 0
⊢ ↑(Units.mk0 y hy) * ↑(Units.mk0 y hy) = y * y

Tactic:
simp

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

Goal state before:
pp: case inl.«1»
inst✝ : Fact (Nat.Prime 2)
⊢ (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0 → (fun i ↦ i) ⟨1, ⋯⟩ ^ (2 / 2) = 1 ∨ (fun i ↦ i) ⟨1, ⋯⟩ ^ (2 / 2) = -1

Tactic:
simp

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

Goal state before:
pp: case neg.«_@».Mathlib.NumberTheory.LegendreSymbol.Basic.2777296637._hygCtx._hyg.53.«1»
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬(fun i ↦ i) ⟨1, ⋯⟩ = 0 → 1 = (fun i ↦ i) ⟨1, ⋯⟩ ^ 1

Tactic:
simp

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 : F
ha : a = 0
⊢ (quadraticChar F) 0 = 0

Tactic:
exact quadraticChar_zero

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

Goal state before:
pp: case neg.refine_1.zero
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
hp : ¬p = ⊥
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) L
this : FiniteDimensional K L
H : ↑Q ≤ FractionalIdeal.dual A K 1 * ↑(Ideal.map (algebraMap A B) p)
hne : 1 ≠ 0
y : B
x : L
hx : x ∈ FractionalIdeal.dual A K 1
⊢ (Algebra.trace K L) (x * (Algebra.linearMap B L) 0) ∈ ↑p

Tactic:
simp

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ -2 = -1 * 2

Tactic:
simp

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

Goal state before:
pp: H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : (-c) ^ 3 + a ^ 3 + b ^ 3 = 0
h3c : 3 ∣ c
⊢ 3 ∣ -c

Tactic:
by simp [h3c]

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: case neg
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ Coprime 1 b

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: n : ℕ
h₁ : 1 < n
h₂ : ¬Prime n
⊢ 0 = 1 ^ (n - 1) - 1

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

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

Tactic:
simp

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
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = λ ^ 4 * y
⊢ ↑S'.u⁻¹ * (↑S'.u * S'.c ^ 3) = S'.c ^ 3

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: k n : ℕ
hn : 1 < n + succ 1
hp : Prime (k * 2 ^ (n + succ 1 + 1) + 1)
hpdvd : k * 2 ^ (n + succ 1 + 1) + 1 ∣ (n + succ 1).fermatNumber
this : Fact (Prime (k * 2 ^ (n + succ 1 + 1) + 1))
hp2 : k * 2 ^ (n + succ 1 + 1) + 1 ≠ 2
⊢ (k * 2 ^ n % 8 * (2 ^ (succ 1 + 1) % 8) % 8 + 1) % 8 = 1

Tactic:
simp

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
x : 𝓞 K
hx : S'.a ^ 3 + 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = λ ^ 4 * y
⊢ ↑S'.u⁻¹ * (↑S'.u * S'.c ^ 3) = S'.c ^ 3

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: n : ℕ
⊢ n ∈ maximalIdeal ℕ ↔ n ≠ 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: x✝ : ℕ
⊢ x✝ ∈ ↑(maximalIdeal ℕ) ↔ x✝ ∈ {1}ᶜ

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: ⊢ 2 ∈ ↑(maximalIdeal ℕ)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: ⊢ 3 ∈ ↑(maximalIdeal ℕ)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: n : ℕ
h : n ∈ maximalIdeal ℕ
lt : 1 < n
⊢ gcd 2 3 ∣ n

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: ⊢ {2} ⊆ {2, 3}

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: ⊢ 3 ∈ {2, 3}

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: ⊢ ¬2 ∣ 3

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: case refine_2.«1»
⊢ (![⊥, { asIdeal := span {2}, isPrime := ⋯ }, { asIdeal := span {2, 3}, isPrime := ⋯ }] ⟨1, ⋯⟩.castSucc,
      ![⊥, { asIdeal := span {2}, isPrime := ⋯ }, { asIdeal := span {2, 3}, isPrime := ⋯ }] ⟨1, ⋯⟩.succ) ∈
    {x | x.1 < x.2}

Tactic:
exact SetLike.lt_iff_le_and_exists.mpr ⟨Ideal.span_mono (by simp),
        3, Ideal.subset_span (by simp), Ideal.mem_span_singleton.not.mpr <| by simp⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: case refine_2.«1»
⊢ (![⊥, { asIdeal := span {2}, isPrime := ⋯ }, { asIdeal := maximalIdeal ℕ, isPrime := ⋯ }]
        ((fun i ↦ i) ⟨1, ⋯⟩).castSucc,
      ![⊥, { asIdeal := span {2}, isPrime := ⋯ }, { asIdeal := maximalIdeal ℕ, isPrime := ⋯ }]
        ((fun i ↦ i) ⟨1, ⋯⟩).succ) ∈
    {(a, b) | a < b}

Tactic:
· simp_rw [Nat.maximalIdeal_eq_span_two_three]
      exact SetLike.lt_iff_le_and_exists.mpr ⟨Ideal.span_mono (by simp),
        3, Ideal.subset_span (by simp), Ideal.mem_span_singleton.not.mpr <| by simp⟩

Goal state after:
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
h0 : setGcd s = 0
⊢ ↑∅ ⊆ s

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: 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
rx : ℕ
hrx : r = setGcd s * rx
⊢ ↑(setGcd s * rx + n) = ↑(∑ c, (if 0 ≤ a c then rx else x / setGcd s - rx) * (a c).natAbs * ↑c)

Tactic:
n,

Goal state after:
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
rx : ℕ
hrx : r = setGcd s * rx
⊢ ↑(setGcd s * rx + x / setGcd s * ∑ i, (-a i).toNat * ↑i) =
    ↑(∑ c, (if 0 ≤ a c then rx else x / setGcd s - rx) * (a c).natAbs * ↑c)
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: m✝ n✝¹ : ℕ
s✝ t✝ : Set ℕ
n✝ : ℕ
s : Submodule ℕ ℕ
t : Finset ℕ
n : ℕ
hts : ↑t ⊆ ↑s
hn : ∀ m ≥ n, setGcd ↑s ∣ m → m ∈ Ideal.span ↑t
m : ℕ
hm : m ∈ s
le : n ≤ m
⊢ ↑t ⊆ ↑(t ∪ {m ∈ Finset.range n | m ∈ s})

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ ¬1 ≤ 0

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ 0 < ↑1

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
⊢ 1 < 4

Tactic:
simp

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

Goal state before:
pp: n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ 1 < ↑2

Tactic:
simp

Goal state after:
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 B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) P) ≤ P ^ (1 + 1)
⊢ 1 = 2 - 1

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ padicValRat 2 (harmonic 0) = -↑(Nat.log 2 0)

Tactic:
simp

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

Goal state before:
pp: case succ.inl
ih : padicValRat 2 (harmonic 0) = -↑(Nat.log 2 0)
⊢ padicValRat 2 (harmonic (0 + 1)) = -↑(Nat.log 2 (0 + 1))

Tactic:
simp

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
k k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
hk : (S.b * (↑η + 1) + λ * k') * -↑η = λ * k * -↑η
⊢ S.b = λ * ((k - k') * -↑η)

Tactic:
show (S.b * (η + 1) + λ * k') * -η = (-S.b) * (η ^ 2 + η + 1 - 1) - η * λ * k' by ring,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
hk : -S.b * (↑η ^ 2 + ↑η + 1 - 1) - ↑η * λ * k' = λ * k * -↑η
⊢ S.b = λ * ((k - k') * -↑η)
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 : λ ∣ S.z
⊢ False

Tactic:
replace h := mul_dvd_mul_left ((η : 𝓞 K) - 1) h
  rw [coe_eta, ← z_spec, ← pow_two] at h
  exact lambda_sq_not_dvd_a_add_eta_sq_mul_b _ h

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
hι : Nonempty ι
⊢ 1 ≠ 0

Tactic:
simp

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

Goal state before:
pp: case refine_3
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ ↑S.u₄ * S.Z ^ 3 * (λ * ↑S.u₂ * ↑η) = S.Z ^ 3 * ↑S.u₃ * λ * ↑η ^ 2

Tactic:
· simp only [u₄_def, inv_eq_one_div, mul_div_assoc', mul_one, val_div_eq_divp, Units.val_mul,
      IsUnit.unit_spec, divp_mul_eq_mul_divp, divp_eq_iff_mul_eq]
    ring

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

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
e : ι ≃ ι'
H : ∀ (v : AbsoluteValue K ℝ), ⨆ i, v (0 (e i)) = ⨆ i, v (0 i)
⊢ mulHeight (0 ∘ ⇑e) = mulHeight 0

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
⊢ HasFiniteMulSupport fun v ↦ max (↑v x) 1

Tactic:
by
  rcases eq_or_ne x 0 with rfl | hx
  · simp [HasFiniteMulSupport]
  fun_prop

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

Goal state before:
pp: n : ℕ
s : ℝ
⊢ ↑n ≤ ↑n + 1

Tactic:
simp

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

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
⊢ 1 ≤ mulHeight 0

Tactic:
simp

Goal state after:
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 B
inst✝ : P.IsPrime
⊢ ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P

Tactic:
by
  rcases eq_or_ne P ⊥ with rfl | hPbot
  · simp_rw [← Ideal.zero_eq_bot, zero_dvd_iff]
    simp only [Submodule.zero_eq_bot, differentIdeal_ne_bot, not_false_eq_true, true_iff]
    let K := FractionRing A
    let L := FractionRing B
    have : IsLocalization B⁰ (Localization.AtPrime (⊥ : Ideal B)) := by
      convert!
        (inferInstance :
          IsLocalization (⊥ : Ideal B).primeCompl (Localization.AtPrime (⊥ : Ideal B)))
      ext; simp [Ideal.primeCompl]
    refine (Algebra.FormallyUnramified.iff_of_equiv (A := L)
      ((IsLocalization.algEquiv B⁰ _ _).restrictScalars A)).mp ?_
    have : Algebra.FormallyUnramified K L := by
      rwa [Algebra.FormallyUnramified.iff_isSeparable]
    refine .comp A K L
  have hp : P.under A ≠ ⊥ := mt Ideal.eq_bot_of_comap_eq_bot hPbot
  have hp' := (Ideal.map_eq_bot_iff_of_injective
    (FaithfulSMul.algebraMap_injective A B)).not.mpr hp
  have := Ideal.IsPrime.isMaximal inferInstance hPbot
  let := Localization.AtPrime.algebraOfLiesOver (P.under A) P
  constructor
  · intro H
    · rw [Algebra.isUnramifiedAt_iff_map_eq (p := P.under A)]
      constructor
      · suffices Algebra.IsSeparable (A ⧸ P.under A) (B ⧸ P) by infer_instance
        contrapose H
        exact dvd_differentIdeal_of_not_isSeparable A hp P H
      · rw [← Ideal.IsDedekindDomain.ramificationIdx'_eq_one_iff hPbot Ideal.map_comap_le]
        apply Ideal.ramificationIdx'_spec
        · simp [Ideal.map_le_iff_le_comap]
        · contrapose H
          rw [← pow_one P, show 1 = 2 - 1 by simp]
          apply pow_sub_one_dvd_differentIdeal _ _ _ hp
          simpa [Ideal.dvd_iff_le] using H
  · intro H
    obtain ⟨Q, h₁, h₂⟩ := Ideal.eq_prime_pow_mul_coprime hp' P
    rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count _ _ hp',
      Ideal.ramificationIdx_eq_one_of_isUnramifiedAt, pow_one] at h₂
    obtain ⟨h₃, h₄⟩ := (Algebra.isUnramifiedAt_iff_map_eq (p := P.under A) _ _).mp H
    exact not_dvd_differentIdeal_of_isCoprime_of_isSeparable
      A P Q (Ideal.isCoprime_iff_sup_eq.mpr h₁) h₂.symm

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

Goal state before:
pp: case empty
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : AddCommMonoid β
inst✝² : FunLike F β ℝ
inst✝¹ : NonnegHomClass F β ℝ
inst✝ : ZeroHomClass F β ℝ
v : F
l : α → β
hv : IsNonarchimedean ⇑v
⊢ v (∑ i ∈ ∅, l i) ≤ ⨆ i, v (l ↑i)

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ (∫ (x : ℝ) in ↑n..↑n + 1, 1 / x) - ∫ (x : ℝ) in ↑n..↑n + 1, ↑n * (1 / x ^ 2) =
    (∫ (x : ℝ) in ↑n..↑n + 1, 1 / x) - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x ^ 2

pp: case hf
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (HDiv.hDiv 1) volume (↑n) (↑n + 1)

pp: case hg
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (fun x ↦ ↑n * (1 / x ^ 2)) volume (↑n) (↑n + 1)

Tactic:
· simp_rw [intervalIntegral.integral_const_mul]

Goal state after:
case hf
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (HDiv.hDiv 1) volume (↑n) (↑n + 1)

case hg
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (fun x ↦ ↑n * (1 / x ^ 2)) volume (↑n) (↑n + 1)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁴ : AddCommMonoid β
inst✝³ : FunLike F β ℝ
inst✝² : NonnegHomClass F β ℝ
inst✝¹ : ZeroHomClass F β ℝ
v : F
l : α → β
inst✝ : Fintype α
hv : IsNonarchimedean ⇑v
⊢ ⨆ i, ⨆ (h : i ∈ Finset.univ), v (l ↑⟨i, h⟩) ≤ ⨆ i, v (l i)

Tactic:
simp

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

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
⊢ mulHeight (Sum.elim 0 0) = mulHeight 0

Tactic:
simp

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

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : IsEmpty ι'
⊢ ⨆ j, v (∑ i, A (j, i) * x i) ≤ (↑(Nat.card ι) * ⨆ ji, v (A ji)) * ⨆ i, v (x i)

Tactic:
simp

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

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝ : IsEmpty ι
⊢ ⨆ j, v (∑ i, A (j, i) * x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ -2 ≠ -1

Tactic:
simp

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

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝¹ : Nonempty ι
h✝ : IsEmpty ι'
⊢ ⨆ j, v (∑ i, A (j, i) * x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)

Tactic:
simp

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

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_5
inst✝ : Subsingleton ι
⊢ mulHeight 0 = 1

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
a : K
x : Fin n → K
⊢ mulHeight (vecCons a (vecCons 0 x) ∘ ⇑(Equiv.swap 0 1)) = mulHeight (vecCons a x)

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
a b : K
x : Fin n → K
⊢ mulHeight (vecCons a (vecCons b (vecCons 0 x) ∘ ⇑(Equiv.swap 0 1))) = mulHeight (vecCons a (vecCons b x))

Tactic:
simp

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

Goal state before:
pp: case «0»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x✝ : K
v : AbsoluteValue K ℝ
x : K
⊢ v (![x, 1] ((fun i ↦ i) ⟨0, ⋯⟩)) = ![v x, 1] ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp

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

Goal state before:
pp: case «1»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x✝ : K
v : AbsoluteValue K ℝ
x : K
⊢ v (![x, 1] ((fun i ↦ i) ⟨1, ⋯⟩)) = ![v x, 1] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : ∀ (v : AbsoluteValue K ℝ) (x : K), max (v x) 1 = ⨆ i, v (![x, 1] i)
⊢ ![x, 1] ≠ 0

Tactic:
simp

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

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
⊢ mulHeight₁ (x / 0) = mulHeight ![x, 0]

Tactic:
simp

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

Goal state before:
pp: case inl.zero
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
⊢ mulHeight (0 ^ 0) = mulHeight 0 ^ 0

Tactic:
simp

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

Goal state before:
pp: case inl.succ
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
n✝ : ℕ
⊢ mulHeight (0 ^ (n✝ + 1)) = mulHeight 0 ^ (n✝ + 1)

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ 0 ≤ ↑(Nat.card ι) ^ totalWeight K

Tactic:
simp

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

Goal state before:
pp: case «0»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℕ
⊢ ![x ^ n, 1] ((fun i ↦ i) ⟨0, ⋯⟩) = (![x, 1] ^ n) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp

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

Goal state before:
pp: case «1»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℕ
⊢ ![x ^ n, 1] ((fun i ↦ i) ⟨1, ⋯⟩) = (![x, 1] ^ n) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp

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ζ
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : S.multiplicity - 1 = 0
⊢ 1 ≤ 2

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
ι : Type u_2
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : IsEmpty ι
this : 0 ≤ logHeight A + logHeight x
⊢ (logHeight fun j ↦ ∑ i, A (j, i) * x i) ≤ ↑(totalWeight K) * log ↑(Nat.card ι) + logHeight A + logHeight x

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
ι : Type u_2
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : Nonempty ι
⊢ ↑(Nat.card ι) ^ totalWeight K ≠ 0

Tactic:
simp

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

Goal state before:
pp: N : ℕ
s : ℝ
hs : 1 < s
n : ℕ
⊢ 0 < n + 1

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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
h_fin₂ : t₂.Finite
⊢ ∀ (x : Ideal (𝓞 K)), ((↑(Nat.castRingHom ℝ)).comp ↑absNorm) x = 1 → x = 1

Tactic:
simp

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

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
⊢ mulHeight (-0) = mulHeight 0

Tactic:
simp

Goal state after: