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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ index K ≃ (K →+* ℂ)

Tactic:
by
  refine Equiv.ofBijective (fun c => ?_)
    ((Fintype.bijective_iff_surjective_and_card _).mpr ⟨?_, ?_⟩)
  · cases c with
    | inl w => exact w.val.embedding
    | inr wj => rcases wj with ⟨w, j⟩
                exact if j = 0 then w.val.embedding else ComplexEmbedding.conjugate w.val.embedding
  · intro φ
    by_cases hφ : ComplexEmbedding.IsReal φ
    · exact ⟨Sum.inl (InfinitePlace.mkReal ⟨φ, hφ⟩), by simp [embedding_mk_eq_of_isReal hφ]⟩
    · by_cases hw : (InfinitePlace.mk φ).embedding = φ
      · exact ⟨Sum.inr ⟨InfinitePlace.mkComplex ⟨φ, hφ⟩, 0⟩, by simp [hw]⟩
      · exact ⟨Sum.inr ⟨InfinitePlace.mkComplex ⟨φ, hφ⟩, 1⟩,
          by simp [(embedding_mk_eq φ).resolve_left hw]⟩
  · rw [Embeddings.card, ← mixedEmbedding.finrank K,
      ← Module.finrank_eq_card_basis (stdBasis K)]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ ↥↑↑I ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
⊢ ENNReal.ofReal |(Basis.det ?b₀) ⇑((fractionalIdealLatticeBasis K I).reindex e)| * volume (fundamentalDomain ?b₀) =
    ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * volume (fundamentalDomain (latticeBasis K))

Tactic:
show (fractionalIdealLatticeBasis K I).reindex e = (mixedEmbedding K) ∘
        (basisOfFractionalIdeal K I) ∘ e.symm by
      ext1; simp only [Basis.coe_reindex, Function.comp_apply, fractionalIdealLatticeBasis_apply]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ ↥↑↑I ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
⊢ ENNReal.ofReal |(Basis.det ?b₀) (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e.symm)| *
      volume (fundamentalDomain ?b₀) =
    ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * volume (fundamentalDomain (latticeBasis K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B

Tactic:
exact hB

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ DiscreteTopology ↥(mixedEmbedding.integerLattice K)

Tactic:
rw [← span_latticeBasis]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ DiscreteTopology ↥(Submodule.span ℤ (Set.range ⇑(latticeBasis K)))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ MeasureTheory.IsAddFundamentalDomain (↥(mixedEmbedding.integerLattice K)) (ZSpan.fundamentalDomain (latticeBasis K))
    MeasureTheory.volume

Tactic:
rw [← span_latticeBasis]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ MeasureTheory.IsAddFundamentalDomain (↥(Submodule.span ℤ (Set.range ⇑(latticeBasis K))))
    (ZSpan.fundamentalDomain (latticeBasis K)) MeasureTheory.volume
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
⊢ minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B

Tactic:
exact hB

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K *
      (↑(finrank ℚ K).factorial * ((2 ^ nrRealPlaces K)⁻¹ * ((π * 2⁻¹) ^ nrComplexPlaces K)⁻¹)) =
    ↑(FractionalIdeal.absNorm ↑I) *
            2 ^ (↑(finrank ℚ K) - ↑(nrComplexPlaces K) - ↑(nrRealPlaces K) + ↑(nrComplexPlaces K)) *
          √‖discr K‖ *
        ↑(finrank ℚ K).factorial *
      π⁻¹ ^ nrComplexPlaces K

Tactic:
← zpow_neg_one,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ ↑(FractionalIdeal.absNorm ↑I) * (2 ^ (-1)) ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K *
      (↑(finrank ℚ K).factorial * ((2 ^ nrRealPlaces K) ^ (-1) * ((π * 2 ^ (-1)) ^ nrComplexPlaces K) ^ (-1))) =
    ↑(FractionalIdeal.absNorm ↑I) *
            2 ^ (↑(finrank ℚ K) - ↑(nrComplexPlaces K) - ↑(nrRealPlaces K) + ↑(nrComplexPlaces K)) *
          √‖discr K‖ *
        ↑(finrank ℚ K).factorial *
      (π ^ (-1)) ^ nrComplexPlaces K
Module: Mathlib.RingTheory.Invariant.Galois

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Finite G
inst✝¹⁵ : Group G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝¹² : Q.LiesOver P
inst✝¹¹ : P.IsPrime
inst✝¹⁰ : Q.IsPrime
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra (A ⧸ P) K
inst✝⁵ : IsFractionRing (A ⧸ P) K
inst✝⁴ : Algebra (B ⧸ Q) L
inst✝³ : IsFractionRing (B ⧸ Q) L
inst✝² : Algebra (A ⧸ P) L
inst✝¹ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝ : IsScalarTower (A ⧸ P) K L
this✝ : Algebra.IsIntegral A B
this : Algebra.IsAlgebraic K L
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
a : A
ha : (algebraMap A (A ⧸ P)) a ≠ 0
b : B
h : (algebraMap A (A ⧸ P)) a • x = y * (algebraMap B (B ⧸ Q)) b
val✝ : Fintype G
p : A[X]
hp : Polynomial.map (algebraMap A B) p = MulSemiringAction.charpoly G b
h_monic : p.Monic
h_eval : (aeval b) p = 0
q : A[X] := p.comp (C a * X)
d : L := (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
comm₁ : (algebraMap K L).comp (algebraMap (A ⧸ P) K) = (algebraMap (B ⧸ Q) L).comp (algebraMap (A ⧸ P) (B ⧸ Q))
comm₂ : (algebraMap (A ⧸ P) (B ⧸ Q)).comp (algebraMap A (A ⧸ P)) = (algebraMap B (B ⧸ Q)).comp (algebraMap A B)
⊢ (aeval ((algebraMap K L) ((algebraMap (A ⧸ P) K) ((algebraMap A (A ⧸ P)) a)) * (aeval d) X))
      (Polynomial.map (algebraMap (A ⧸ P) K) (Polynomial.map (algebraMap A (A ⧸ P)) p)) =
    0

Tactic:
aeval_X,

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Finite G
inst✝¹⁵ : Group G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝¹² : Q.LiesOver P
inst✝¹¹ : P.IsPrime
inst✝¹⁰ : Q.IsPrime
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra (A ⧸ P) K
inst✝⁵ : IsFractionRing (A ⧸ P) K
inst✝⁴ : Algebra (B ⧸ Q) L
inst✝³ : IsFractionRing (B ⧸ Q) L
inst✝² : Algebra (A ⧸ P) L
inst✝¹ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝ : IsScalarTower (A ⧸ P) K L
this✝ : Algebra.IsIntegral A B
this : Algebra.IsAlgebraic K L
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
a : A
ha : (algebraMap A (A ⧸ P)) a ≠ 0
b : B
h : (algebraMap A (A ⧸ P)) a • x = y * (algebraMap B (B ⧸ Q)) b
val✝ : Fintype G
p : A[X]
hp : Polynomial.map (algebraMap A B) p = MulSemiringAction.charpoly G b
h_monic : p.Monic
h_eval : (aeval b) p = 0
q : A[X] := p.comp (C a * X)
d : L := (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
comm₁ : (algebraMap K L).comp (algebraMap (A ⧸ P) K) = (algebraMap (B ⧸ Q) L).comp (algebraMap (A ⧸ P) (B ⧸ Q))
comm₂ : (algebraMap (A ⧸ P) (B ⧸ Q)).comp (algebraMap A (A ⧸ P)) = (algebraMap B (B ⧸ Q)).comp (algebraMap A B)
⊢ (aeval ((algebraMap K L) ((algebraMap (A ⧸ P) K) ((algebraMap A (A ⧸ P)) a)) * d))
      (Polynomial.map (algebraMap (A ⧸ P) K) (Polynomial.map (algebraMap A (A ⧸ P)) p)) =
    0
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
B : Type u_6
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : IsIntegrallyClosed A
inst✝¹⁴ : IsDomain A
inst✝¹³ : IsDomain B
inst✝¹² : IsIntegrallyClosed B
inst✝¹¹ : Algebra.IsIntegral A B
inst✝¹⁰ : IsTorsionFree A B
C : Type u_9
inst✝⁹ : CommRing C
inst✝⁸ : IsDomain C
inst✝⁷ : IsIntegrallyClosed C
inst✝⁶ : Algebra A C
inst✝⁵ : Algebra B C
inst✝⁴ : IsScalarTower A B C
inst✝³ : Algebra.IsIntegral A C
inst✝² : Algebra.IsIntegral B C
inst✝¹ : IsTorsionFree A C
inst✝ : IsTorsionFree B C
x : C
⊢ (algebraMap A (FractionRing A)) ((intNorm A B) ((intNorm B C) x)) = (algebraMap A (FractionRing A)) ((intNorm A C) x)

Tactic:
rw [algebraMap_intNorm_fractionRing, algebraMap_intNorm_fractionRing,
    algebraMap_intNorm_fractionRing, Algebra.norm_norm]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : { w // w.IsComplex }
⊢ normAtComplexPlaces x ↑w = ‖x.2 w‖

Tactic:
rw [normAtComplexPlaces, dif_neg (not_isReal_iff_isComplex.mpr w.prop),
    normAtPlace_apply_of_isComplex]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
⊢ 4 / 9 * (3 * π / 4) ^ 2 ≤ 4 / 9 * (3 * π / 4) ^ finrank ℚ K

Tactic:
gcongr
      linarith [Real.pi_gt_three]

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G A B
h : ∃ P, P.IsPrime ∧ P.LiesOver p
left✝ : h.choose.IsPrime
right✝ : h.choose.LiesOver p
⊢ p.inertiaDegIn B = P.inertiaDeg A

Tactic:
inertiaDegIn,

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G A B
h : ∃ P, P.IsPrime ∧ P.LiesOver p
left✝ : h.choose.IsPrime
right✝ : h.choose.LiesOver p
⊢ (if h : ∃ P, P.IsPrime ∧ P.LiesOver p then h.choose.inertiaDeg A else 0) = P.inertiaDeg A
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: case refine_1.refine_2
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
C : Type u_5
W : Type u_6
inst✝³ : CommRing C
inst✝² : CommRing W
inst✝¹ : Algebra C W
P : Submonoid C
inst✝ : IsLocalization P W
g : B →+* C
hg : N ≤ Submonoid.comap g P
x : L
hx : x ∈ ↑(extended L hf I)
hx' : x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
y z : L
x✝¹ : y ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
x✝ : z ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
hy : (IsLocalization.map W g hg) y ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))
hz : (IsLocalization.map W g hg) z ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))
⊢ (IsLocalization.map W g hg) (y + z) ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))

pp: case refine_1.refine_3
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
C : Type u_5
W : Type u_6
inst✝³ : CommRing C
inst✝² : CommRing W
inst✝¹ : Algebra C W
P : Submonoid C
inst✝ : IsLocalization P W
g : B →+* C
hg : N ≤ Submonoid.comap g P
x : L
hx : x ∈ ↑(extended L hf I)
hx' : x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
b : B
y : L
x✝ : y ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
hy : (IsLocalization.map W g hg) y ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))
⊢ (IsLocalization.map W g hg) (b • y) ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))

Tactic:
· rw [map_add]
      exact add_mem hy hz

Goal state after:
case refine_1.refine_3
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
C : Type u_5
W : Type u_6
inst✝³ : CommRing C
inst✝² : CommRing W
inst✝¹ : Algebra C W
P : Submonoid C
inst✝ : IsLocalization P W
g : B →+* C
hg : N ≤ Submonoid.comap g P
x : L
hx : x ∈ ↑(extended L hf I)
hx' : x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
b : B
y : L
x✝ : y ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
hy : (IsLocalization.map W g hg) y ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))
⊢ (IsLocalization.map W g hg) (b • y) ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))
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
C : Type u_5
W : Type u_6
inst✝³ : CommRing C
inst✝² : CommRing W
inst✝¹ : Algebra C W
P : Submonoid C
inst✝ : IsLocalization P W
g : B →+* C
hg : N ≤ Submonoid.comap g P
⊢ (extendedHom' W hg).comp (extendedHom' L hf) = extendedHom' W ⋯

Tactic:
by
  apply RingHom.ext
  intro I
  exact extended_extended (A := A) (B := B) (f := f) (K := K) (M := M) (L := L)
    (N := N) (hf := hf) (I := I) (C := C) (W := W) (P := P) (g := g) hg

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra B L
inst✝⁶ : IsFractionRing A K
inst✝⁵ : IsFractionRing B L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A B L
inst✝¹ : IsScalarTower A K L
inst✝ : Algebra.IsIntegral A B
I : FractionalIdeal A⁰ K
⊢ ↑((extendedHom L B) I) = span B (⇑(algebraMap K L) '' ↑I)

Tactic:
extendedHom'_apply,

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra B L
inst✝⁶ : IsFractionRing A K
inst✝⁵ : IsFractionRing B L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A B L
inst✝¹ : IsScalarTower A K L
inst✝ : Algebra.IsIntegral A B
I : FractionalIdeal A⁰ K
⊢ ↑(extended L ⋯ I) = span B (⇑(algebraMap K L) '' ↑I)
Module: Mathlib.RingTheory.DedekindDomain.Instances

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : IsDomain R
inst✝⁸ : IsDomain S
inst✝⁷ : IsDomain T
inst✝⁶ : Algebra R S
P : Ideal R
inst✝⁵ : P.IsPrime
inst✝⁴ : FaithfulSMul R S
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : IsTorsionFree R T
a : Rₚ
b : Sₚ
c : Tₚ
x✝ : R × ↥P.primeCompl
a₁ : R
a₂ : ↥P.primeCompl
this : ↑a₂ ≠ 0
⊢ (mk' (Localization P.primeCompl) (↑a₂ * (a₁, a₂).1) (a₁, a₂).2 • b) • c =
    mk' (Localization P.primeCompl) (↑a₂ * (a₁, a₂).1) (a₁, a₂).2 • b • c

Tactic:
IsLocalization.mk'_mul_cancel_left,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : IsDomain R
inst✝⁸ : IsDomain S
inst✝⁷ : IsDomain T
inst✝⁶ : Algebra R S
P : Ideal R
inst✝⁵ : P.IsPrime
inst✝⁴ : FaithfulSMul R S
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : IsTorsionFree R T
a : Rₚ
b : Sₚ
c : Tₚ
x✝ : R × ↥P.primeCompl
a₁ : R
a₂ : ↥P.primeCompl
this : ↑a₂ ≠ 0
⊢ ((algebraMap R (Localization P.primeCompl)) (a₁, a₂).1 • b) • c =
    (algebraMap R (Localization P.primeCompl)) (a₁, a₂).1 • b • c
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ∉ span {↑p} ^ 2

Tactic:
Ideal.span_singleton_pow,

Goal state after:
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ∉ span {↑p ^ 2}
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✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
⊢ 1 ≤ 1ᵛ

Tactic:
by
  rw [le_traceDual_iff_map_le_one, mul_one, one_eq_range]
  rintro _ ⟨x, ⟨x, rfl⟩, rfl⟩
  rw [mem_one]
  apply IsIntegrallyClosed.isIntegral_iff.mp
  apply isIntegral_trace
  rw [IsIntegralClosure.isIntegral_iff (A := B)]
  exact ⟨_, rfl⟩

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Field L
inst✝¹³ : Algebra A K
inst✝¹² : Algebra B L
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : IsScalarTower A B L
inst✝⁶ : IsFractionRing A K
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsIntegralClosure B A L
inst✝² : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral A (b i)
a x : L
ha : a ∈ I
hx : x ∈ Iᵛ
hinv : IsUnit (traceMatrix K ⇑b).det
H : ((traceMatrix K ⇑b).cramer fun i ↦ (Algebra.trace K L) (x * a * b i)) = (traceMatrix K ⇑b).det • b.equivFun (x * a)
this : Function.Injective (traceMatrix K ⇑b).mulVec
i : ι
a✝ : i ∈ Finset.univ
⊢ IsIntegral A (b.equivFun (discr K ⇑b • (a * x)) i • b i)

Tactic:
b.equivFun.map_smul,

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✝⁶ : IsFractionRing A K
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsIntegralClosure B A L
inst✝² : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral A (b i)
a x : L
ha : a ∈ I
hx : x ∈ Iᵛ
hinv : IsUnit (traceMatrix K ⇑b).det
H : ((traceMatrix K ⇑b).cramer fun i ↦ (Algebra.trace K L) (x * a * b i)) = (traceMatrix K ⇑b).det • b.equivFun (x * a)
this : Function.Injective (traceMatrix K ⇑b).mulVec
i : ι
a✝ : i ∈ Finset.univ
⊢ IsIntegral A ((discr K ⇑b • b.equivFun (a * x)) i • b i)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case e'_2
p k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this✝ : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
this : pB₁.dim = (IsPrimitiveRoot.powerBasis ℚ hζ).dim
i : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ (algebraMap (𝓞 K) K) (pB₁.basis ((finCongr this).symm i)) = (IsPrimitiveRoot.powerBasis ℚ hζ).basis i

Tactic:
PowerBasis.coe_basis,

Goal state after:
case e'_2
p k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this✝ : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
this : pB₁.dim = (IsPrimitiveRoot.powerBasis ℚ hζ).dim
i : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ (algebraMap (𝓞 K) K) (pB₁.gen ^ ↑((finCongr this).symm i)) = (IsPrimitiveRoot.powerBasis ℚ hζ).basis i
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case e_a.coprime
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this✝⁴ : NumberField K
this✝³ : NeZero n₁
this✝² : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this✝¹ : IsCyclotomicExtension {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : (NumberField.discr ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hζ₂ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₁) n₂
this✝ : IsCyclotomicExtension {n₂} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₁⟯
hζ₂' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : (NumberField.discr ↥ℚ⟮ζ ^ n₁⟯).natAbs = n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))
this : IsGalois ℚ ↥ℚ⟮ζ ^ n₂⟯
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))

Tactic:
have h_top : ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯ = ⊤ := by
      have : IsCyclotomicExtension {n₁ * n₂} ℚ (⊤ : IntermediateField ℚ K) :=
          hK.equiv _ _ _ topEquiv.symm
      have : IsCyclotomicExtension {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) := by
        rw [← Nat.Coprime.lcm_eq_mul h]
        exact isCyclotomicExtension_lcm_sup ℚ K n₁ n₂ ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯
      exact isCyclotomicExtension_eq {n₁ * n₂} ℚ K _ _

Goal state after:
case e_a.coprime
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this✝⁴ : NumberField K
this✝³ : NeZero n₁
this✝² : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this✝¹ : IsCyclotomicExtension {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : (NumberField.discr ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hζ₂ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₁) n₂
this✝ : IsCyclotomicExtension {n₂} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₁⟯
hζ₂' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : (NumberField.discr ↥ℚ⟮ζ ^ n₁⟯).natAbs = n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))
this : IsGalois ℚ ↥ℚ⟮ζ ^ n₂⟯
h_top : ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯ = ⊤
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))