mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this✝ : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : Ideal R → A
ha : ∀ M ∈ s, a M ∈ I
b : Ideal R → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b
c : R
hmem : (algebraMap R A) (u M * c) ∈ IsLocalization.coeSubmodule A M
hc : (algebraMap R A) c = a M * b M
⊢ (algebraMap R A) c ∈ IsLocalization.coeSubmodule A M

Tactic:
obtain ⟨d, hdM, he⟩ := hmem

Goal state after:
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this✝ : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : Ideal R → A
ha : ∀ M ∈ s, a M ∈ I
b : Ideal R → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b
c : R
hc : (algebraMap R A) c = a M * b M
d : R
hdM : d ∈ ↑M
he : (Algebra.linearMap R A) d = (algebraMap R A) (u M * c)
⊢ (algebraMap R A) c ∈ IsLocalization.coeSubmodule A M
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: case refine_1
L : Type u_3
inst✝⁶ : Field L
K₁ : Type u_4
K₂ : Type u_5
inst✝⁵ : Field K₁
inst✝⁴ : NumberField K₁
inst✝³ : Field K₂
inst✝² : NumberField K₂
inst✝¹ : Algebra K₁ L
inst✝ : Algebra K₂ L
u v : ℤ
h : u * discr K₁ + v * discr K₂ = 1
⊢ ↑u * ↑(discr K₁) ∈ Ideal.map (algebraMap (𝓞 K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 K₁))

pp: case refine_2
L : Type u_3
inst✝⁶ : Field L
K₁ : Type u_4
K₂ : Type u_5
inst✝⁵ : Field K₁
inst✝⁴ : NumberField K₁
inst✝³ : Field K₂
inst✝² : NumberField K₂
inst✝¹ : Algebra K₁ L
inst✝ : Algebra K₂ L
u v : ℤ
h : u * discr K₁ + v * discr K₂ = 1
⊢ ↑v * ↑(discr K₂) ∈ Ideal.map (algebraMap (𝓞 K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 K₂))

pp: case refine_3
L : Type u_3
inst✝⁶ : Field L
K₁ : Type u_4
K₂ : Type u_5
inst✝⁵ : Field K₁
inst✝⁴ : NumberField K₁
inst✝³ : Field K₂
inst✝² : NumberField K₂
inst✝¹ : Algebra K₁ L
inst✝ : Algebra K₂ L
u v : ℤ
h : u * discr K₁ + v * discr K₂ = 1
⊢ ↑u * ↑(discr K₁) + ↑v * ↑(discr K₂) = 1

Tactic:
· apply Ideal.mul_mem_left
    rw [← map_intCast (algebraMap (𝓞 K₁) (𝓞 L))]
    exact Ideal.mem_map_of_mem (algebraMap (𝓞 K₁) (𝓞 L)) <| discr_mem_differentIdeal _ _

Goal state after:
case refine_2
L : Type u_3
inst✝⁶ : Field L
K₁ : Type u_4
K₂ : Type u_5
inst✝⁵ : Field K₁
inst✝⁴ : NumberField K₁
inst✝³ : Field K₂
inst✝² : NumberField K₂
inst✝¹ : Algebra K₁ L
inst✝ : Algebra K₂ L
u v : ℤ
h : u * discr K₁ + v * discr K₂ = 1
⊢ ↑v * ↑(discr K₂) ∈ Ideal.map (algebraMap (𝓞 K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 K₂))

case refine_3
L : Type u_3
inst✝⁶ : Field L
K₁ : Type u_4
K₂ : Type u_5
inst✝⁵ : Field K₁
inst✝⁴ : NumberField K₁
inst✝³ : Field K₂
inst✝² : NumberField K₂
inst✝¹ : Algebra K₁ L
inst✝ : Algebra K₂ L
u v : ℤ
h : u * discr K₁ + v * discr K₂ = 1
⊢ ↑u * ↑(discr K₁) + ↑v * ↑(discr K₂) = 1
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: L : Type u_3
inst✝¹ : Field L
inst✝ : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x✝ : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main : (discr L).natAbs = (discr ↥K₁).natAbs ^ finrank (𝓞 ↥K₁) (𝓞 L) * (discr ↥K₂).natAbs ^ finrank ℚ ↥K₁
⊢ (discr L).natAbs = (discr ↥K₁).natAbs ^ finrank ℚ ↥K₂ * (discr ↥K₂).natAbs ^ finrank ℚ ↥K₁

Tactic:
← IsFractionRing.finrank_eq (𝓞 K₁) K₁ (𝓞 L) L,

Goal state after:
L : Type u_3
inst✝¹ : Field L
inst✝ : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x✝ : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main : (discr L).natAbs = (discr ↥K₁).natAbs ^ finrank (↥K₁) L * (discr ↥K₂).natAbs ^ finrank ℚ ↥K₁
⊢ (discr L).natAbs = (discr ↥K₁).natAbs ^ finrank ℚ ↥K₂ * (discr ↥K₂).natAbs ^ finrank ℚ ↥K₁
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
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
⊢ spanNorm R ⊤ = 1

Tactic:
spanNorm_top R,

Goal state after:
R : Type u_1
S✝ : Type u_2
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
⊢ ⊤ = 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case refine_1.zero
p : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ 0} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ 0)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝¹ : FiniteDimensional ℚ K := finiteDimensional {p ^ 0} ℚ K
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑p ^ n
this✝ : IsCyclotomicExtension {1} ℚ K
y : ℚ
H : (algebraMap ℚ K) ↑p ^ n * (algebraMap ℚ K) y ∈ ℤ[B.gen]
this : (algebraMap ℚ K) y ∈ ⊥
h : IsIntegral ℤ y
z : ℤ
hz : (algebraMap ℤ ℚ) z = y
⊢ (algebraMap ℚ K) y ∈ ℤ[ζ]

Tactic:
← hz,

Goal state after:
case refine_1.zero
p : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ 0} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ 0)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝¹ : FiniteDimensional ℚ K := finiteDimensional {p ^ 0} ℚ K
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑p ^ n
this✝ : IsCyclotomicExtension {1} ℚ K
y : ℚ
H : (algebraMap ℚ K) ↑p ^ n * (algebraMap ℚ K) y ∈ ℤ[B.gen]
this : (algebraMap ℚ K) y ∈ ⊥
h : IsIntegral ℤ y
z : ℤ
hz : (algebraMap ℤ ℚ) z = y
⊢ (algebraMap ℚ K) ((algebraMap ℤ ℚ) z) ∈ ℤ[ζ]
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ (n✝ + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n✝ + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ (n✝ + 1)} ℚ K
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑p ^ n
H : (algebraMap ℚ K) ↑p ^ n * x ∈ ℤ[B.gen]
h₁ : minpoly ℚ B.gen = map (algebraMap ℤ ℚ) (minpoly ℤ B.gen)
h₂ : minpoly ℚ (ζ - 1) = (cyclotomic (p ^ (n✝ + 1)) ℚ).comp (X + 1)
⊢ (minpoly ℤ B.gen).IsEisensteinAt (ℤ ∙ ↑p)

Tactic:
rw [IsPrimitiveRoot.subOnePowerBasis_gen] at h₁

Goal state after:
p : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ (n✝ + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n✝ + 1))
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ (n✝ + 1)} ℚ K
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑p ^ n
H : (algebraMap ℚ K) ↑p ^ n * x ∈ ℤ[B.gen]
h₁ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
h₂ : minpoly ℚ (ζ - 1) = (cyclotomic (p ^ (n✝ + 1)) ℚ).comp (X + 1)
⊢ (minpoly ℤ B.gen).IsEisensteinAt (ℤ ∙ ↑p)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: k : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
⊢ Prime (hζ.toInteger - 1)

Tactic:
have := IsCyclotomicExtension.numberField {2 ^ (k + 1)} ℚ K
  refine Ideal.prime_of_irreducible_absNorm_span (fun h ↦ ?_) ?_
  · apply hζ.pow_ne_one_of_pos_of_lt one_ne_zero (one_lt_pow₀ (by decide) (by simp))
    rw [sub_eq_zero] at h
    simpa using! congrArg (algebraMap _ K) h
  rw [Nat.irreducible_iff_prime, Ideal.absNorm_span_singleton, ← Nat.prime_iff,
    ← Int.prime_iff_natAbs_prime]
  cases k
  · convert! Prime.neg Int.prime_two
    apply RingHom.injective_int (algebraMap ℤ ℚ)
    rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ)]
    simp only [algebraMap_int_eq, map_neg, map_ofNat]
    simpa only [zero_add, pow_one, AddSubgroupClass.coe_sub, OneMemClass.coe_one,
        pow_zero]
      using! hζ.norm_pow_sub_one_two (cyclotomic.irreducible_rat
        (by simp only [zero_add, pow_one, Nat.ofNat_pos]))
  convert! Int.prime_two
  apply RingHom.injective_int (algebraMap ℤ ℚ)
  rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ), algebraMap_int_eq]
  exact hζ.norm_sub_one_two Nat.AtLeastTwo.prop (cyclotomic.irreducible_rat (by simp))

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : K[x] = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L
pbgen : pb.gen = x
hnondeg : (traceForm K L).Nondegenerate
hpb :
  ⇑((traceForm K L).dualBasis hnondeg pb.basis) = fun x ↦
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
this : Subalgebra.toSubmodule A[x] = span A (Set.range ⇑pb.basis)
⊢ span A (Set.range fun x_1 ↦ ((aeval x) (derivative (minpoly K x)))⁻¹ * (minpolyDiv K x).coeff ↑x_1) =
    span A (Set.range ((fun a ↦ ((aeval x) (derivative (minpoly K x)))⁻¹ * a) ∘ (minpolyDiv K x).coeff))

Tactic:
apply le_antisymm <;> rw [Submodule.span_le]

Goal state after:
case a
A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : K[x] = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L
pbgen : pb.gen = x
hnondeg : (traceForm K L).Nondegenerate
hpb :
  ⇑((traceForm K L).dualBasis hnondeg pb.basis) = fun x ↦
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
this : Subalgebra.toSubmodule A[x] = span A (Set.range ⇑pb.basis)
⊢ (Set.range fun x_1 ↦ ((aeval x) (derivative (minpoly K x)))⁻¹ * (minpolyDiv K x).coeff ↑x_1) ⊆
    ↑(span A (Set.range ((fun a ↦ ((aeval x) (derivative (minpoly K x)))⁻¹ * a) ∘ (minpolyDiv K x).coeff)))

case a
A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : K[x] = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L
pbgen : pb.gen = x
hnondeg : (traceForm K L).Nondegenerate
hpb :
  ⇑((traceForm K L).dualBasis hnondeg pb.basis) = fun x ↦
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
this : Subalgebra.toSubmodule A[x] = span A (Set.range ⇑pb.basis)
⊢ Set.range ((fun a ↦ ((aeval x) (derivative (minpoly K x)))⁻¹ * a) ∘ (minpolyDiv K x).coeff) ⊆
    ↑(span A (Set.range fun x_1 ↦ ((aeval x) (derivative (minpoly K x)))⁻¹ * (minpolyDiv K x).coeff ↑x_1))
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p k n : ℕ
K : Type u
inst✝³ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝² : NeZero n
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ ℤ[⟨ζ - 1, ⋯⟩] = ⊤

Tactic:
refine hζ.integralPowerBasis.adjoin_eq_top_of_gen_mem_adjoin ?_

Goal state after:
p k n : ℕ
K : Type u
inst✝³ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝² : NeZero n
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ hζ.integralPowerBasis.gen ∈ ℤ[⟨ζ - 1, ⋯⟩]
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
⊢ P ^ (e - 1) ∣ differentIdeal A B

Tactic:
obtain ⟨a, ha⟩ := (pow_dvd_pow _ (Nat.sub_le e 1)).trans hP

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
⊢ P ^ (e - 1) ∣ differentIdeal A B
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this✝ : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
this : (Ideal.Quotient.mk (Ideal.span {λ})) x ∈ Finset.univ
⊢ (↑3).natAbs = 3

Tactic:
simp only [Nat.cast_ofNat, Int.reduceAbs]

Goal state after:
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
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
⊢ (Algebra.trace K L) ((algebraMap B L) x) ∈ ↑p

Tactic:
refine FractionalIdeal.mul_induction_on (H ⟨_, hxQ, rfl⟩) ?_ ?_

Goal state after:
case neg.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
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
⊢ ∀ i ∈ FractionalIdeal.dual A K 1, ∀ j ∈ ↑(Ideal.map (algebraMap A B) p), (Algebra.trace K L) (i * j) ∈ ↑p

case neg.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
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
⊢ ∀ (x y : L), (Algebra.trace K L) x ∈ ↑p → (Algebra.trace K L) y ∈ ↑p → (Algebra.trace K L) (x + y) ∈ ↑p
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case neg.refine_1.mem
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
z : A
hz : (algebraMap A K) z = (Algebra.trace K L) x
⊢ (algebraMap A K) (z * y) = y • (Algebra.trace K L) x

Tactic:
← hz,

Goal state after:
case neg.refine_1.mem
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
z : A
hz : (algebraMap A K) z = (Algebra.trace K L) x
⊢ (algebraMap A K) (z * y) = y • (algebraMap A K) z
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ¬a = 0
ha' : ¬a ^ (Fintype.card F / 2) = 1
ha'' : a ^ (Fintype.card F / 2) = -1
⊢ -1 = 1 → 1 = -1

Tactic:
exact Eq.symm

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
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (3 ^ 1)
⊢ ↑S'.u * ((hζ✝.toInteger - 1) * z) ^ 3 - (S'.a ^ 3 - 1) - (S'.b ^ 3 - 1) =
    S'.a ^ 3 + S'.b ^ 3 - (S'.a ^ 3 - 1) - (S'.b ^ 3 - 1)

Tactic:
← hz,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ 3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (3 ^ 1)
⊢ ↑S'.u * S'.c ^ 3 - (S'.a ^ 3 - 1) - (S'.b ^ 3 - 1) = S'.a ^ 3 + S'.b ^ 3 - (S'.a ^ 3 - 1) - (S'.b ^ 3 - 1)
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
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (3 ^ 1)
⊢ S'.a ^ 3 + 1 + (S'.b ^ 3 + 1) - ↑S'.u * ((hζ✝.toInteger - 1) * z) ^ 3 =
    S'.a ^ 3 + 1 + (S'.b ^ 3 + 1) - (S'.a ^ 3 + S'.b ^ 3)

Tactic:
← hz,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ 3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (3 ^ 1)
⊢ S'.a ^ 3 + 1 + (S'.b ^ 3 + 1) - ↑S'.u * S'.c ^ 3 = S'.a ^ 3 + 1 + (S'.b ^ 3 + 1) - (S'.a ^ 3 + S'.b ^ 3)
Module: Mathlib.NumberTheory.Fermat

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

Tactic:
apply pepin_primality
  rw [← h]
  congr
  rw [fermatNumber, add_tsub_cancel_right, Nat.pow_div Nat.one_le_two_pow Nat.zero_lt_two]

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

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

Tactic:
mul_dvd_mul_iff_left _

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ S.w ^ 3
this : 2 ≤ S.multiplicity
⊢ False

K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ (3 * S.multiplicity) * λ ∣ λ ^ (3 * S.multiplicity) * S.w ^ 3
this : 2 ≤ S.multiplicity
⊢ λ ^ (3 * S.multiplicity) ≠ 0