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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h :
  ∀ p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊,
    Nat.Prime p →
      ∀ P ∈ (span {↑p}).primesOver (𝓞 K),
        p ^ P.inertiaDeg ℤ ≤
            ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ →
          Submodule.IsPrincipal P
x✝ : ↥(Ideal (𝓞 K))⁰
P : Ideal (𝓞 K)
HP : P ∈ (Ideal (𝓞 K))⁰
hP : (↑⟨P, HP⟩).IsPrime
hPN :
  ↑(absNorm ↑⟨P, HP⟩) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
p : ℤ
hp : under ℤ P = ℤ ∙ p
⊢ Submodule.IsPrincipal ↑⟨P, HP⟩

Tactic:
have hp0 : p ≠ 0 := fun h ↦ nonZeroDivisors.coe_ne_zero ⟨P, HP⟩ <|
    eq_bot_of_comap_eq_bot (R := ℤ) <| by simpa only [hp, submodule_span_eq, span_singleton_eq_bot]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h :
  ∀ p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊,
    Nat.Prime p →
      ∀ P ∈ (span {↑p}).primesOver (𝓞 K),
        p ^ P.inertiaDeg ℤ ≤
            ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ →
          Submodule.IsPrincipal P
x✝ : ↥(Ideal (𝓞 K))⁰
P : Ideal (𝓞 K)
HP : P ∈ (Ideal (𝓞 K))⁰
hP : (↑⟨P, HP⟩).IsPrime
hPN :
  ↑(absNorm ↑⟨P, HP⟩) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
p : ℤ
hp : under ℤ P = ℤ ∙ p
hp0 : p ≠ 0
⊢ Submodule.IsPrincipal ↑⟨P, HP⟩
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case refine_2.refine_2
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ max (↑(max B 1)) 1 ^ finrank ℚ ↥K * ↑((finrank ℚ ↥K).choose (finrank ℚ ↥K / 2)) ≤ ↑(max B 1 ^ D * ↑(D.choose (D / 2)))

Tactic:
rw [show max ↑(max (B : ℝ≥0) 1) (1 : ℝ) = max (B : ℝ) 1 by simp, val_eq_coe, NNReal.coe_mul,
          NNReal.coe_pow, NNReal.coe_max, NNReal.coe_one, NNReal.coe_natCast]

Goal state after:
case refine_2.refine_2
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ max (↑B) 1 ^ finrank ℚ ↥K * ↑((finrank ℚ ↥K).choose (finrank ℚ ↥K / 2)) ≤ max (↑B) 1 ^ D * ↑(D.choose (D / 2))
Module: Mathlib.NumberTheory.RamificationInertia.Unramified

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain R
inst✝³ : IsDomain S
inst✝² : FaithfulSMul R S
inst✝¹ : CharZero R
inst✝ : Algebra.IsIntegral R S
P : Ideal S
x✝ : P.IsPrime
hP : P.LiesOver ⊥
⊢ IsUnramifiedAt R P

Tactic:
simpa [Ideal.eq_bot_of_liesOver_bot R P] using isUnramifiedAt_bot

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: A : Type u_1
inst✝⁸ : CommRing A
B : Type u_2
inst✝⁷ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁶ : CommRing K
inst✝⁵ : Algebra A K
inst✝⁴ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝³ : CommRing L
inst✝² : Algebra B L
inst✝¹ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
inst✝ : IsDomain B
hf' : Function.Injective ⇑f
hI : I ≠ 0
hN : 0 ∉ N
x : K
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ ¬(IsLocalization.map L f hf) x = 0

Tactic:
exact (map_ne_zero_iff _ (IsLocalization.map_injective_of_injective' _ _ _ _ hN hf')).mpr hx₂

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: case refine_1
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ ↑I * ↑J
⊢ (IsLocalization.map L f hf) x ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

Tactic:
Submodule.mul_eq_span_mul_set

Goal state after:
case refine_1
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
⊢ (IsLocalization.map L f hf) x ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case h₂
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := ⋯
B : ℝ≥0 := ⋯
C : ℕ := ⋯
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsComplex}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLT'Factor ↥K) * ↑(boundOfDiscBdd N)
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < √(1 + ↑(boundOfDiscBdd N) ^ 2)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ ↑((finrank ℚ ↥K).choose (finrank ℚ ↥K / 2)) ≤ ↑↑(D.choose (D / 2))

Tactic:
rw [NNReal.coe_natCast, Nat.cast_le]
          exact (Nat.choose_le_choose _ (rank_le_rankOfDiscrBdd hK₂)).trans
            (Nat.choose_le_middle _ _)

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
⊢ P = span {x}

Tactic:
rw [← associated_iff_eq, associated_iff_normalizedFactors_eq_normalizedFactors hP0 hspan0]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
⊢ normalizedFactors P = normalizedFactors (span {x})
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: n x : ℕ
⊢ ↑x ∈ Ideal.span {↑↑n} ↔ n ∣ x

Tactic:
Ideal.mem_span_singleton,

Goal state after:
n x : ℕ
⊢ ↑↑n ∣ ↑x ↔ n ∣ x
Module: Mathlib.RingTheory.NormalClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
inst✝² : Module.IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : PerfectField K
⊢ IsGalois K (FractionRing T)

Tactic:
by
  refine IsGalois.of_equiv_equiv (F := K) («E» := E)
    (f := (FractionRing.algEquiv R K).symm.toRingEquiv)
    (g := (FractionRing.algEquiv T E).symm.toRingEquiv) ?_
  ext
  simpa using! IsFractionRing.algEquiv_commutes (FractionRing.algEquiv R K).symm
    (FractionRing.algEquiv T E).symm _

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsIntegrallyClosed S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : IsTorsionFree R S
I J : Ideal S
⊢ ↑I * ↑J ⊆ ↑(I * J)

Tactic:
rintro _ ⟨x, hxI, y, hyJ, rfl⟩

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsIntegrallyClosed S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : IsTorsionFree R S
I J : Ideal S
x : S
hxI : x ∈ ↑I
y : S
hyJ : y ∈ ↑J
⊢ (fun x1 x2 ↦ x1 * x2) x y ∈ ↑(I * J)
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg
R : Type u_1
inst✝²¹ : CommRing R
inst✝²⁰ : IsDomain R
S : Type u_3
inst✝¹⁹ : CommRing S
inst✝¹⁸ : IsDomain S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsIntegrallyClosed S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : Module.Finite R S
inst✝¹³ : IsTorsionFree R S
T : Type u_4
inst✝¹² : CommRing T
inst✝¹¹ : IsDomain T
inst✝¹⁰ : IsIntegrallyClosed T
inst✝⁹ : Algebra R T
inst✝⁸ : Algebra T S
inst✝⁷ : Module.Finite R T
inst✝⁶ : Module.Finite T S
inst✝⁵ : IsTorsionFree R T
inst✝⁴ : IsTorsionFree T S
inst✝³ : IsScalarTower R T S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain T
inst✝ : IsDedekindDomain S
I : Ideal S
P : Ideal R
hP✝ : P.IsMaximal
hP : ¬P = ⊥
Rₚ : Type u_1 := Localization.AtPrime P
Tₚ : Type u_4 := Localization (algebraMapSubmonoid T P.primeCompl)
Sₚ : Type u_3 := Localization (algebraMapSubmonoid S P.primeCompl)
this : NeZero P
h : algebraMapSubmonoid T P.primeCompl ≤ T⁰
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (spanNorm T I)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I)

Tactic:
← spanIntNorm_localization R (spanNorm T I) _ (primeCompl_le_nonZeroDivisors P) Tₚ,

Goal state after:
case neg
R : Type u_1
inst✝²¹ : CommRing R
inst✝²⁰ : IsDomain R
S : Type u_3
inst✝¹⁹ : CommRing S
inst✝¹⁸ : IsDomain S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsIntegrallyClosed S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : Module.Finite R S
inst✝¹³ : IsTorsionFree R S
T : Type u_4
inst✝¹² : CommRing T
inst✝¹¹ : IsDomain T
inst✝¹⁰ : IsIntegrallyClosed T
inst✝⁹ : Algebra R T
inst✝⁸ : Algebra T S
inst✝⁷ : Module.Finite R T
inst✝⁶ : Module.Finite T S
inst✝⁵ : IsTorsionFree R T
inst✝⁴ : IsTorsionFree T S
inst✝³ : IsScalarTower R T S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain T
inst✝ : IsDedekindDomain S
I : Ideal S
P : Ideal R
hP✝ : P.IsMaximal
hP : ¬P = ⊥
Rₚ : Type u_1 := Localization.AtPrime P
Tₚ : Type u_4 := Localization (algebraMapSubmonoid T P.primeCompl)
Sₚ : Type u_3 := Localization (algebraMapSubmonoid S P.primeCompl)
this : NeZero P
h : algebraMapSubmonoid T P.primeCompl ≤ T⁰
⊢ spanNorm (Localization.AtPrime P) (map (algebraMap T Tₚ) (spanNorm T I)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ ℤ ∙ ↑p
i : ℕ
hi : i < ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).natDegree
⊢ ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).coeff i ∈ span {↑p}

Tactic:
Ideal.mem_span_singleton,

Goal state after:
case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ ℤ ∙ ↑p
i : ℕ
hi : i < ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).natDegree
⊢ ↑p ∣ ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).coeff i
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ ℤ ∙ ↑p
i : ℕ
hi : i < ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).natDegree
⊢ ((cyclotomic (p ^ (n + 1) * p) (ZMod p)).comp (X + 1)).coeff i = 0

Tactic:
cyclotomic_mul_prime_dvd_eq_pow,

Goal state after:
case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ ℤ ∙ ↑p
i : ℕ
hi : i < ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).natDegree
⊢ ((cyclotomic (p ^ (n + 1)) (ZMod p) ^ p).comp (X + 1)).coeff i = 0

case refine_2.succ.hn
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ ℤ ∙ ↑p
i : ℕ
hi : i < ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).natDegree
⊢ p ∣ p ^ (n + 1)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n i k : ℕ
hi : p * k < p * (p ^ n * (p - 1))
hk : i = p * k
hn : ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + C 1)).coeff k ∈ span {↑p}
⊢ ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff k = 0

Tactic:
Ideal.mem_span_singleton,

Goal state after:
case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n i k : ℕ
hi : p * k < p * (p ^ n * (p - 1))
hk : i = p * k
hn : ↑p ∣ ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + C 1)).coeff k
⊢ ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff k = 0
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : IsIntegrallyClosed S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
⊢ span {↑(absNorm ((relNorm ℤ) I))} = span {↑(absNorm I)}

Tactic:
absNorm_relNorm

Goal state after:
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : IsIntegrallyClosed S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
⊢ span {↑(absNorm I)} = span {↑(absNorm I)}
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
inst✝¹³ : IsDomain R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : IsIntegrallyClosed R
inst✝⁹ : IsIntegrallyClosed S
inst✝⁸ : Algebra R S
inst✝⁷ : Module.Finite R S
inst✝⁶ : IsTorsionFree R S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : IsDedekindDomain S
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal R
inst✝ : Module.Finite ℤ R
⊢ absNorm ((relNorm ℤ) (I ^ finrank R S)) = absNorm I ^ finrank R S

Tactic:
absNorm_relNorm,

Goal state after:
R : Type u_1
inst✝¹⁴ : CommRing R
inst✝¹³ : IsDomain R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : IsIntegrallyClosed R
inst✝⁹ : IsIntegrallyClosed S
inst✝⁸ : Algebra R S
inst✝⁷ : Module.Finite R S
inst✝⁶ : IsTorsionFree R S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : IsDedekindDomain S
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
I : Ideal R
inst✝ : Module.Finite ℤ R
⊢ absNorm (I ^ finrank R S) = absNorm I ^ finrank R S
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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✝²³ : IsIntegrallyClosed A
inst✝²² : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst✝²¹ : CommRing C
inst✝²⁰ : IsDedekindDomain C
inst✝¹⁹ : Field M
inst✝¹⁸ : Algebra C M
inst✝¹⁷ : IsFractionRing C M
inst✝¹⁶ : Algebra A C
inst✝¹⁵ : Algebra B C
inst✝¹⁴ : Algebra A M
inst✝¹³ : Algebra B M
inst✝¹² : Algebra K M
inst✝¹¹ : Algebra L M
inst✝¹⁰ : IsScalarTower A C M
inst✝⁹ : IsScalarTower A K M
inst✝⁸ : IsScalarTower B C M
inst✝⁷ : IsScalarTower B L M
inst✝⁶ : IsScalarTower K L M
inst✝⁵ : IsIntegralClosure C A M
inst✝⁴ : FiniteDimensional K M
inst✝³ : FiniteDimensional L M
inst✝² : Algebra.IsSeparable K M
inst✝¹ : IsIntegralClosure C B M
inst✝ : Algebra.IsSeparable L M
x : L
y : M
hx : ∀ (a : B), ∃ x_1, (algebraMap A K) x_1 = (Algebra.trace K L) (a • x)
hy : ∀ (a : C), ∃ x, (algebraMap B L) x = (Algebra.trace L M) (a • y)
c : C
⊢ ∃ x_1, (algebraMap A K) x_1 = (Algebra.trace K M) (c • x • y)

Tactic:
obtain ⟨b, hb⟩ := hy c

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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✝²³ : IsIntegrallyClosed A
inst✝²² : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst✝²¹ : CommRing C
inst✝²⁰ : IsDedekindDomain C
inst✝¹⁹ : Field M
inst✝¹⁸ : Algebra C M
inst✝¹⁷ : IsFractionRing C M
inst✝¹⁶ : Algebra A C
inst✝¹⁵ : Algebra B C
inst✝¹⁴ : Algebra A M
inst✝¹³ : Algebra B M
inst✝¹² : Algebra K M
inst✝¹¹ : Algebra L M
inst✝¹⁰ : IsScalarTower A C M
inst✝⁹ : IsScalarTower A K M
inst✝⁸ : IsScalarTower B C M
inst✝⁷ : IsScalarTower B L M
inst✝⁶ : IsScalarTower K L M
inst✝⁵ : IsIntegralClosure C A M
inst✝⁴ : FiniteDimensional K M
inst✝³ : FiniteDimensional L M
inst✝² : Algebra.IsSeparable K M
inst✝¹ : IsIntegralClosure C B M
inst✝ : Algebra.IsSeparable L M
x : L
y : M
hx : ∀ (a : B), ∃ x_1, (algebraMap A K) x_1 = (Algebra.trace K L) (a • x)
hy : ∀ (a : C), ∃ x, (algebraMap B L) x = (Algebra.trace L M) (a • y)
c : C
b : B
hb : (algebraMap B L) b = (Algebra.trace L M) (c • y)
⊢ ∃ x_1, (algebraMap A K) x_1 = (Algebra.trace K M) (c • x • y)
Module: Mathlib.RingTheory.Fintype

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h : Fintype.card R ≤ 3
⊢ univ = {0, 1, -1}

Tactic:
by
  refine (eq_of_subset_of_card_le (subset_univ _) ?_).symm
  rcases lt_or_eq_of_le h with h | h
  · apply card_le_card
    rw [Finset.univ_of_card_le_two (Nat.lt_succ_iff.1 h)]
    simp
  · have : Nontrivial R := by
      refine Fintype.one_lt_card_iff_nontrivial.1 ?_
      rw [h]
      simp
    rw [card_univ, h, card_insert_of_notMem, card_insert_of_notMem, card_singleton]
    · rw [mem_singleton]
      intro H
      rw [← add_eq_zero_iff_eq_neg, one_add_one_eq_two] at H
      apply_fun (ringEquivOfPrime R Nat.prime_three h).symm at H
      simp only [map_ofNat, map_zero] at H
      replace H : ((2 : ℕ) : ZMod 3) = 0 := H
      rw [natCast_eq_zero_iff] at H
      norm_num at H
    · simp

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 : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
hu : Associated ↑(seq K w₁ hB n) ↑(seq K w₁ hB m)
w : InfinitePlace K
hw : w ≠ w₁
⊢ w ((algebraMap (𝓞 K) K) ↑(Exists.choose hu)) =
    w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB m) * ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB n))⁻¹)

Tactic:
by
        rw [← congr_arg (algebraMap (𝓞 K) K) hu.choose_spec, mul_comm, map_mul (algebraMap _ _),
          ← mul_assoc, inv_mul_cancel₀ (seq_ne_zero K w₁ hB n), one_mul]

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

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ↑a = 0
⊢ ↑0 = 0 ^ (p / 2)

Tactic:
zero_pow (Nat.div_pos (@Fact.out p.Prime).two_le (succ_pos 1)).ne'

Goal state after:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ↑a = 0
⊢ ↑0 = 0
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : (x * y⁻¹) ^ 2 - ↑a * (y * y⁻¹) ^ 2 = 0
⊢ legendreSym p a = 1

Tactic:
mul_inv_cancel₀ hy,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : (x * y⁻¹) ^ 2 - ↑a * 1 ^ 2 = 0
⊢ legendreSym p a = 1
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsSquare (-1) ↔ p % 4 ≠ 3

Tactic:
by
  rw [FiniteField.isSquare_neg_one_iff, card p]

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
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h✝ : ringChar F' ≠ ringChar F
χ : MulChar F F' := (quadraticChar F).ringHomComp (algebraMap ℤ F')
hχ₁ : χ ≠ 1
h : (χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2) = χ ↑(Fintype.card F')
⊢ (quadraticChar F) ↑(Fintype.card F') = (quadraticChar F') (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))

Tactic:
rw [← quadraticChar_eq_pow_of_char_ne_two' hF'] at h

Goal state after:
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : Fintype F
inst✝³ : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h✝ : ringChar F' ≠ ringChar F
χ : MulChar F F' := (quadraticChar F).ringHomComp (algebraMap ℤ F')
hχ₁ : χ ≠ 1
h : ↑((quadraticChar F') (χ (-1) * ↑(Fintype.card F))) = χ ↑(Fintype.card F')
⊢ (quadraticChar F) ↑(Fintype.card F') = (quadraticChar F') (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))
Module: Mathlib.NumberTheory.LucasPrimality

Goal state before:
pp: p : ℕ
hP : Nat.Prime p
this : Fact (Nat.Prime p)
g : (ZMod p)ˣ
hg : ∀ (x : (ZMod p)ˣ), x ∈ Subgroup.zpowers g
⊢ orderOf g = p - 1

Tactic:
orderOf_eq_card_of_forall_mem_zpowers hg,

Goal state after:
p : ℕ
hP : Nat.Prime p
this : Fact (Nat.Prime p)
g : (ZMod p)ˣ
hg : ∀ (x : (ZMod p)ˣ), x ∈ Subgroup.zpowers g
⊢ Nat.card (ZMod p)ˣ = p - 1
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
⊢ n.Coprime b

Tactic:
by
  by_cases h₃ : 2 ≤ n
  · -- To prove that `n` is coprime with `b`, we need to show that for all prime factors of `n`,
    -- we can derive a contradiction if `n` divides `b`.
    apply Nat.coprime_of_dvd
    -- If `k` is a prime number that divides both `n` and `b`, then we know that `n = m * k` and
    -- `b = j * k` for some natural numbers `m` and `j`. We substitute these into the hypothesis.
    rintro k hk ⟨m, rfl⟩ ⟨j, rfl⟩
    -- Because prime numbers do not divide 1, it suffices to show that `k ∣ 1` to prove a
    -- contradiction
    apply Nat.Prime.not_dvd_one hk
    -- Since `n` divides `b ^ (n - 1) - 1`, `k` also divides `b ^ (n - 1) - 1`
    replace h := dvd_of_mul_right_dvd h
    -- Because `k` divides `b ^ (n - 1) - 1`, if we can show that `k` also divides `b ^ (n - 1)`,
    -- then we know `k` divides 1.
    rw [Nat.dvd_add_iff_right h, Nat.sub_add_cancel (Nat.one_le_pow _ _ h₂)]
    -- Since `k` divides `b`, `k` also divides any power of `b` except `b ^ 0`. Therefore, it
    -- suffices to show that `n - 1` isn't zero. However, we know that `n - 1` isn't zero because we
    -- assumed `2 ≤ n` when doing `by_cases`.
    refine dvd_of_mul_right_dvd (dvd_pow_self (k * j) ?_)
    lia
  -- If `n = 1`, then it follows trivially that `n` is coprime with `b`.
  · rw [show n = 1 by lia]
    simp

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: n b : ℕ
h : 1 ≤ b
⊢ n.ProbablePrime b ↔ b ^ (n - 1) ≡ 1 [MOD n]

Tactic:
have : 1 ≤ b ^ (n - 1) := one_le_pow₀ h

Goal state after:
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ n.ProbablePrime b ↔ b ^ (n - 1) ≡ 1 [MOD n]