mathlib-initiative/mathlib-tactics huggingface dataset:
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) ∣ differentIdeal A B

Tactic:
have hP : ((P ^ (e - 1) :)⁻¹ : FractionalIdeal B⁰ L) = a / p.map (algebraMap A B) := by
      apply inv_involutive.injective
      simp only [inv_inv, ha, FractionalIdeal.coeIdeal_mul, inv_div,
          mul_div_assoc]
      rw [div_self (by simpa), mul_one]
    rw [Ideal.dvd_iff_le, differentialIdeal_le_iff (K := K) (L := L) (pow_ne_zero _ hPbot), hP,
      Submodule.map_le_iff_le_comap]
    intro x hx
    rw [Submodule.restrictScalars_mem, FractionalIdeal.mem_coe,
      FractionalIdeal.mem_div_iff_of_ne_zero (by simpa using hp')] at hx
    rw [Submodule.mem_comap, LinearMap.coe_restrictScalars, ← FractionalIdeal.coe_one,
      ← div_self (G₀ := FractionalIdeal A⁰ K) (a := p) (by simpa using hp),
      FractionalIdeal.mem_coe, FractionalIdeal.mem_div_iff_of_ne_zero (by simpa using hp)]
    simp only [FractionalIdeal.mem_coeIdeal, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂] at hx
    intro y hy'
    obtain ⟨y, hy, rfl : algebraMap A K _ = _⟩ := (FractionalIdeal.mem_coeIdeal _).mp hy'
    obtain ⟨z, hz, hz'⟩ := hx _ (Ideal.mem_map_of_mem _ hy)
    have : trace K L (algebraMap B L z) ∈ (p : FractionalIdeal A⁰ K) := by
      rw [← algebraMap_intTrace (A := A)]
      exact ⟨intTrace A B z, this z hz, rfl⟩
    rwa [mul_comm, ← smul_eq_mul, ← map_smul, Algebra.smul_def, mul_comm,
      ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply A B L, ← hz']

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case «5»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit ^ 2) - ↑n
⊢ False

Tactic:
apply (hζ.pow_of_coprime 2 (by decide)).not_exists_int_prime_dvd_sub_of_prime_ne_two'
      (by decide)

Goal state after:
case «5»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit ^ 2) - ↑n
⊢ ∃ n, ↑3 ∣ ⋯.toInteger - ↑n
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
⊢ (intTrace A B) x ∈ p

Tactic:
← Ideal.Quotient.eq_zero_iff_mem,

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 p) ((intTrace A B) x) = 0
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ x✝ : Additive ((𝓞 K)ˣ ⧸ torsion K)
⊢ ((logEmbeddingQuot K).codRestrict (unitLattice K) ⋯).toIntLinearMap x✝¹ =
      ((logEmbeddingQuot K).codRestrict (unitLattice K) ⋯).toIntLinearMap x✝ →
    x✝¹ = x✝

Tactic:
rw [AddMonoidHom.coe_toIntLinearMap, AddMonoidHom.codRestrict_apply,
        AddMonoidHom.codRestrict_apply, Subtype.mk.injEq]
      apply logEmbeddingQuot_injective K

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i, fundSystem K i ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i)⁻¹
⊢ Additive.ofMul ↑x + -∑ i, Additive.ofMul (↑(fundSystem K i) ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i) = 0

Tactic:
ofMul_zpow,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i, fundSystem K i ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i)⁻¹
⊢ Additive.ofMul ↑x + -∑ x_1, ((basisModTorsion K).repr (Additive.ofMul ↑x)) x_1 • Additive.ofMul ↑(fundSystem K x_1) =
    0
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
rcases cube_of_not_dvd hdvd.1.1 with ha | ha <;>
  rcases cube_of_not_dvd hdvd.1.2 with hb | hb <;>
  rcases cube_of_not_dvd hdvd.2 with hc | hc

Goal state after:
case inl.inl.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 1
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

case inl.inl.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 8
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

case inl.inr.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 1
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

case inl.inr.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 8
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

case inr.inl.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 1
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

case inr.inl.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 8
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

case inr.inr.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 1
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

case inr.inr.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 8
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: p k : ℕ
hp : _root_.Prime p
⊢ (p ^ k).Deficient

Tactic:
exact hp.nat_prime.deficient_pow

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

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

Tactic:
← add_assoc

Goal state after:
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : b ^ 3 + c ^ 3 + a ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
⊢ IsCoprime b c
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case pos
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + (c ^ 3 + b ^ 3) = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : 3 ∣ c
⊢ 3 ∣ b

Tactic:
← add_assoc

Goal state after:
case pos
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + c ^ 3 + b ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : 3 ∣ c
⊢ 3 ∣ b
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n m : ℕ
h : m.Abundant
hd : m ∣ n
hn : n ≠ 0
⊢ n.Abundant

Tactic:
have := abundancyIndex_le_of_dvd hn hd

Goal state after:
n m : ℕ
h : m.Abundant
hd : m ∣ n
hn : n ≠ 0
this : m.abundancyIndex ≤ n.abundancyIndex
⊢ n.Abundant
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case neg.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = -1
h : -1 ≠ 1
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1

Tactic:
simp only [hb', mul_neg, mul_one, h, if_false]

Goal state after:
case neg.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = -1
h : -1 ≠ 1
⊢ (if -a ^ (Fintype.card F / 2) = 1 then 1 else -1) = -if a ^ (Fintype.card F / 2) = 1 then 1 else -1
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case neg.refine_1.add
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✝ y z : B
hx✝ : y ∈ span B (⇑(algebraMap A B) '' ↑p)
hy✝ : z ∈ span B (⇑(algebraMap A B) '' ↑p)
hy : ∀ x ∈ FractionalIdeal.dual A K 1, (Algebra.trace K L) (x * (Algebra.linearMap B L) y) ∈ ↑p
hz : ∀ x ∈ FractionalIdeal.dual A K 1, (Algebra.trace K L) (x * (Algebra.linearMap B L) z) ∈ ↑p
x : L
hx : x ∈ FractionalIdeal.dual A K 1
⊢ (Algebra.trace K L) (x * (Algebra.linearMap B L) y) + (Algebra.trace K L) (x * (Algebra.linearMap B L) z) ∈ ↑p

Tactic:
exact Submodule.add_mem _ (hy x hx) (hz x hx)

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

Goal state before:
pp: case pos.inr
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
⊢ False

Tactic:
← add_assoc

Goal state after:
case pos.inr
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
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case neg.refine_1.add
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✝ y z : B
hx✝ : y ∈ span B (⇑(algebraMap A B) '' ↑p)
hy✝ : z ∈ span B (⇑(algebraMap A B) '' ↑p)
hy : ∀ x ∈ FractionalIdeal.dual A K 1, (Algebra.trace K L) (x * (Algebra.linearMap B L) y) ∈ ↑p
hz : ∀ x ∈ FractionalIdeal.dual A K 1, (Algebra.trace K L) (x * (Algebra.linearMap B L) z) ∈ ↑p
x : L
hx : x ∈ FractionalIdeal.dual A K 1
⊢ (Algebra.trace K L) (x * (Algebra.linearMap B L) (y + z)) ∈ ↑p

Tactic:
| add y z _ _ hy hz =>

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
a : F
s : Finset F := {x | x ^ 2 = a}.toFinset
b : F
h₀ : ¬b = 0
h : a = b ^ 2
a✝ : F
⊢ a✝ ∈ s ↔ a✝ ∈ [b, -b].toFinset

Tactic:
simp_rw [s, Set.toFinset_ofPred, mem_filter_univ, h, List.toFinset_cons, List.toFinset_nil,
          insert_empty_eq, mem_insert, mem_singleton]

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := {x | x ^ 2 = a}.toFinset
b : F
h₀ : ¬b = 0
h : a = b ^ 2
a✝ : F
⊢ a✝ ^ 2 = b ^ 2 ↔ a✝ = b ∨ a✝ = -b
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
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
P Q : Ideal B
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
inst✝ : Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this✝ : IsScalarTower A (A ⧸ p) (B ⧸ Q)
this : Module.Finite (A ⧸ p) (B ⧸ Q)
e : (B ⧸ Ideal.map (algebraMap A B) p) ≃ₐ[A ⧸ p] (B ⧸ P) × B ⧸ Q :=
  let __spread.0 := (Ideal.quotEquivOfEq ⋯).trans (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
x : B ⧸ P
hx : (Algebra.trace (A ⧸ p) (B ⧸ P)) x ≠ 0
y : B
hy : (Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) y = e.symm (x, 0)
⊢ (intTrace A B) y ∉ p

Tactic:
← Ideal.Quotient.eq_zero_iff_mem,

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
P Q : Ideal B
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
inst✝ : Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this✝ : IsScalarTower A (A ⧸ p) (B ⧸ Q)
this : Module.Finite (A ⧸ p) (B ⧸ Q)
e : (B ⧸ Ideal.map (algebraMap A B) p) ≃ₐ[A ⧸ p] (B ⧸ P) × B ⧸ Q :=
  let __spread.0 := (Ideal.quotEquivOfEq ⋯).trans (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
x : B ⧸ P
hx : (Algebra.trace (A ⧸ p) (B ⧸ P)) x ≠ 0
y : B
hy : (Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) y = e.symm (x, 0)
⊢ ¬(Ideal.Quotient.mk p) ((intTrace A B) y) = 0
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case succ
n : ℕ
hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
⊢ (2 ^ 2 ^ n + 1) * (2 ^ 2 ^ n + 1 - 2) = 2 ^ 2 ^ (n + 1) + 1 - 2

Tactic:
(show 2 ^ 2 ^ n + 1 - 2 = 2 ^ 2 ^ n - 1 by lia),

Goal state after:
case succ
n : ℕ
hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
⊢ (2 ^ 2 ^ n + 1) * (2 ^ 2 ^ n - 1) = 2 ^ 2 ^ (n + 1) + 1 - 2
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case neg
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
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
x : B
hx : x ∈ a
⊢ (intTrace A B) x ∈ p

Tactic:
← Ideal.Quotient.eq_zero_iff_mem,

Goal state after:
case neg
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
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
x : B
hx : x ∈ a
⊢ (Ideal.Quotient.mk p) ((intTrace A B) x) = 0
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
⊢ ↑rx * ↑(setGcd s) + ∑ x_1, ↑(x / setGcd s) * (↑(-a x_1).toNat * ↑↑x_1) =
    ∑ x_1, ↑(if 0 ≤ a x_1 then rx else x / setGcd s - rx) * ↑(a x_1).natAbs * ↑↑x_1

Tactic:
← eq,

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

Goal state before:
pp: case a
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
i : ↥t
a✝ : i ∈ Finset.univ
⊢ ↑rx * a i + ↑(x / setGcd s) * ↑(-a i).toNat = ↑(if 0 ≤ a i then rx else x / setGcd s - rx) * ↑(a i).natAbs

Tactic:
split_ifs with hai

Goal state after:
case pos
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
i : ↥t
a✝ : i ∈ Finset.univ
hai : 0 ≤ a i
⊢ ↑rx * a i + ↑(x / setGcd s) * ↑(-a i).toNat = ↑rx * ↑(a i).natAbs

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
rx : ℕ
hrx : r = setGcd s * rx
i : ↥t
a✝ : i ∈ Finset.univ
hai : ¬0 ≤ a i
⊢ ↑rx * a i + ↑(x / setGcd s) * ↑(-a i).toNat = ↑(x / setGcd s - rx) * ↑(a i).natAbs
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
rx : ℕ
hrx : r = setGcd s * rx
i : ↥t
a✝ : i ∈ Finset.univ
hai : ¬0 ≤ a i
⊢ rx ≤ x / setGcd s

Tactic:
← Nat.mul_le_mul_left_iff (pos_of_ne_zero h0),

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
rx : ℕ
hrx : r = setGcd s * rx
i : ↥t
a✝ : i ∈ Finset.univ
hai : ¬0 ≤ a i
⊢ setGcd s * rx ≤ setGcd s * (x / setGcd s)
Module: Mathlib.NumberTheory.Harmonic.Bounds

Goal state before:
pp: case h₂.calc_4
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∫ (x : ℝ) in 1..↑n, x⁻¹ = Real.log ↑n

Tactic:
convert! integral_inv _
    · rw [div_one]
    · simp only [Nat.one_le_cast, hn, Set.uIcc_of_le, Set.mem_Icc, Nat.cast_nonneg,
        and_true, not_le, zero_lt_one]

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
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
this : Nonempty { j // x j ≠ 0 }
⊢ HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)

Tactic:
suffices (fun v : nonarchAbsVal ↦ ⨆ i : {j // x j ≠ 0}, v.val (x i)).HasFiniteMulSupport by
    convert! this with v
    obtain ⟨i, hi⟩ : ∃ j, x j ≠ 0 := Function.ne_iff.mp hx
    have : Nonempty ι := .intro i
    refine le_antisymm (ciSup_le fun j ↦ ?_) (ciSup_le fun ⟨j, hj⟩ ↦ Finite.le_ciSup_of_le j le_rfl)
    rcases eq_or_ne (x j) 0 with h | h
    · rw [h, v.val.map_zero]
      exact Real.iSup_nonneg' ⟨⟨i, hi⟩, v.val.nonneg ..⟩
    · exact Finite.le_ciSup_of_le ⟨j, h⟩ le_rfl

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
this : Nonempty { j // x j ≠ 0 }
⊢ HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x ↑i)
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 ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f = 0
⊢ mulHeight (x ∘ f) ≤ mulHeight x

pp: case 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
⊢ mulHeight (x ∘ f) ≤ mulHeight x

Tactic:
· simpa [h₀] using one_le_mulHeight _

Goal state after:
case 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
⊢ mulHeight (x ∘ f) ≤ mulHeight x
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
rw [integral_one_div_of_pos, log_div]

Goal state after:
case e_a.hx
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ↑n + 1 ≠ 0

case e_a.hy
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ↑n ≠ 0

case e_a.ha
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n

case e_a.hb
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n + 1