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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
w₀ : { w // w.IsComplex }
h : minkowskiBound K I < volume (convexBodyLT' K f w₀)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
x : mixedSpace K
hx : x ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨x, hx⟩ ≠ 0
h_mem : ↑⟨x, hx⟩ ∈ convexBodyLT' K f w₀
⊢ ∃ a ∈ ↑I,
    a ≠ 0 ∧
      (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w a < ↑(f w)) ∧
        |((↑w₀).embedding a).re| < 1 ∧ |((↑w₀).embedding a).im| < ↑(f ↑w₀) ^ 2

Tactic:
rw [mem_toAddSubgroup, mem_span_fractionalIdealLatticeBasis] at hx

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
w₀ : { w // w.IsComplex }
h : minkowskiBound K I < volume (convexBodyLT' K f w₀)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
x : mixedSpace K
hx✝ : x ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
hx : x ∈ ⇑(mixedEmbedding K) '' ↑↑I
h_nz : ⟨x, hx✝⟩ ≠ 0
h_mem : ↑⟨x, hx✝⟩ ∈ convexBodyLT' K f w₀
⊢ ∃ a ∈ ↑I,
    a ≠ 0 ∧
      (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w a < ↑(f w)) ∧
        |((↑w₀).embedding a).re| < 1 ∧ |((↑w₀).embedding a).im| < ↑(f ↑w₀) ^ 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ (∃ a, (mixedEmbedding K).toIntAlgHom.toLinearMap ((algebraMap (𝓞 K) K) a) = x) ↔ x ∈ mixedEmbedding.integerLattice K

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
⊢ {a | a.LiesOver v ∧ IsRamified K a ∨ a.LiesOver v ∧ IsUnramified K a} = {w | w.LiesOver v}

Tactic:
grind

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i✝ : ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) :=
  LinearMap.codRestrict (Submodule.span ℚ (Set.range ⇑(latticeBasis K))) (mixedEmbedding K).toRatAlgHom.toLinearMap ⋯
i : ChooseBasisIndex ℤ (𝓞 K)
⊢ (mixedEmbedding K).toRatAlgHom ((integralBasis K) i) = (mixedEmbedding K) ((integralBasis K) i)

Tactic:
rfl

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ x ∈ ⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' ↑↑I ↔ x ∈ ⇑(mixedEmbedding K) '' ↑↑I

Tactic:
rfl

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

Goal state before:
pp: case fst
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i✝ : index K
x✝ : { w // w.IsReal }
⊢ (((stdOrthonormalBasis K).toBasis.map ↑(toMixed K)) i✝).1 x✝ = ((stdBasis K) i✝).1 x✝

Tactic:
rfl

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

Goal state before:
pp: case snd
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i✝ : index K
x✝ : { w // w.IsComplex }
⊢ (((stdOrthonormalBasis K).toBasis.map ↑(toMixed K)) i✝).2 x✝ = ((stdBasis K) i✝).2 x✝

Tactic:
rfl

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)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
x : mixedSpace K
hx : x ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨x, hx⟩ ≠ 0
h_mem : ↑⟨x, hx⟩ ∈ convexBodySum K B
⊢ ∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K

Tactic:
rw [mem_toAddSubgroup, mem_span_fractionalIdealLatticeBasis] at hx

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
x : mixedSpace K
hx✝ : x ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
hx : x ∈ ⇑(mixedEmbedding K) '' ↑↑I
h_nz : ⟨x, hx✝⟩ ≠ 0
h_mem : ↑⟨x, hx✝⟩ ∈ convexBodySum K B
⊢ ∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case snd
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsComplex }
⊢ ((negAt s).symm x).2 w = ((negAt s) x).2 w

Tactic:
rfl

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

Goal state before:
pp: case snd
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
x : mixedSpace K
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hx₁ : x ∈ A
hx₂ : ∀ (w : { w // w.IsReal }), x.1 w ≠ 0
x✝ : (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0
h₁ : ∀ w ∈ s, x.1 w < 0
h₂ : ∀ w ∉ s, x.1 w > 0
w : { w // w.IsComplex }
⊢ ((negAt s) (fun w ↦ ‖x.1 w‖, x.2)).2 w = x.2 w

Tactic:
rfl

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

Goal state before:
pp: case _a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ ↑|discr K| ≤ ↑N

Tactic:
← Int.cast_natCast,

Goal state after:
case _a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ ↑|discr K| ≤ ↑↑N
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
B : ℕ
h✝ : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
this : {I | I.cardQuot ≤ B} \ {⊥} ⊆ ⋃ x ∈ t, {I | x ∈ I}
x : R
hx : x ∈ ↑t
⊢ x ≠ 0

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
B : ℕ
h✝ : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : Nat.card (R ⧸ I) ≤ B ∧ I ∉ {⊥}
this✝ : Finite (R ⧸ I)
this : Fintype (R ⧸ I)
⊢ Nat.card (R ⧸ I) < s.card

Tactic:
hI.1,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
B : ℕ
h✝ : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : Nat.card (R ⧸ I) ≤ B ∧ I ∉ {⊥}
this✝ : Finite (R ⧸ I)
this : Fintype (R ⧸ I)
⊢ B < s.card
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
x : L
⊢ x ∈ extended L hf I ↔ x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)

Tactic:
by
  constructor <;> { intro hx; simpa }

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₀ : Ideal A
⊢ extended L hf ↑I₀ = ↑(Ideal.map f I₀)

Tactic:
Ideal.map,

Goal state after:
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₀ : Ideal A
⊢ extended L hf ↑I₀ = ↑(Ideal.span (⇑f '' ↑I₀))
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
⊢ span B (⇑(IsLocalization.map L (algebraMap A B) ⋯) '' ↑I) = span B (⇑(IsLocalization.map L (algebraMap A B) ⋯) '' ↑I)

Tactic:
rfl

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

Goal state before:
pp: case pos
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
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal A⁰ K
h : (extendedHom L B) I = (extendedHom L B) J
hI : ¬I = 0
hJ : J = 0
⊢ I = J

Tactic:
rwa [hJ, map_zero, extendedHom_eq_zero_iff L B, ← hJ] at h

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

Goal state before:
pp: case a
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
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
hmem : u M • (a M * b M) + ∑ x ∈ s.erase M, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M
M' : Ideal R
hu : u M' ∈ ⨅ M'_1 ∈ s.erase M', M'_1
hM' : M' ≠ M ∧ M' ∈ s
c : R
hc : (algebraMap R A) c = a M * b M'
⊢ (algebraMap R A) (u M' * c) ∈ IsLocalization.coeSubmodule A M

Tactic:
Ideal.mem_iInf,

Goal state after:
case a
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
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
hmem : u M • (a M * b M) + ∑ x ∈ s.erase M, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M
M' : Ideal R
hM' : M' ≠ M ∧ M' ∈ s
c : R
hc : (algebraMap R A) c = a M * b M'
hu : ∀ i ∈ s.erase M', u M' ∈ i
⊢ (algebraMap R A) (u M' * c) ∈ IsLocalization.coeSubmodule A M
Module: Mathlib.RingTheory.Ideal.Int

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

Tactic:
← Int.cast_natCast,

Goal state after:
n x : ℕ
⊢ ↑x ∈ Ideal.span {↑↑n} ↔ n ∣ x
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
I : Ideal S
x : ℕ
⊢ ↑x ∈ I ↔ absNorm (under ℤ I) ∣ x

Tactic:
← Int.cast_natCast,

Goal state after:
S : Type u_2
inst✝ : CommRing S
I : Ideal S
x : ℕ
⊢ ↑↑x ∈ I ↔ absNorm (under ℤ I) ∣ x
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
⊢ instAlgebraLocalizationAtPrime P = instAlgebraAtPrimeFractionRing R

Tactic:
rfl

Goal state after:
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
⊢ (↑a₂ • Localization.mk (a₁, a₂).1 (a₁, a₂).2 • b) • c = ↑a₂ • Localization.mk (a₁, a₂).1 (a₁, a₂).2 • b • c

Tactic:
← _root_.smul_assoc (M := R)
    (α := Sₚ),

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
⊢ ((↑a₂ • Localization.mk (a₁, a₂).1 (a₁, a₂).2) • b) • c = ↑a₂ • Localization.mk (a₁, a₂).1 (a₁, a₂).2 • b • c
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: case inl
K : Type u_1
𝒪 : Type u_2
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : CommRing 𝒪
inst✝⁴ : Algebra 𝒪 K
inst✝³ : IsFractionRing 𝒪 K
inst✝² : IsDedekindDomain 𝒪
inst✝¹ : CharZero 𝒪
inst✝ : Module.Finite ℤ 𝒪
this : ↑(discr K).natAbs ∈ differentIdeal ℤ 𝒪
h : discr K = ↑(discr K).natAbs
⊢ ↑(discr K) ∈ differentIdeal ℤ 𝒪

Tactic:
← Int.cast_natCast,

Goal state after:
case inl
K : Type u_1
𝒪 : Type u_2
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : CommRing 𝒪
inst✝⁴ : Algebra 𝒪 K
inst✝³ : IsFractionRing 𝒪 K
inst✝² : IsDedekindDomain 𝒪
inst✝¹ : CharZero 𝒪
inst✝ : Module.Finite ℤ 𝒪
this : ↑↑(discr K).natAbs ∈ differentIdeal ℤ 𝒪
h : discr K = ↑(discr K).natAbs
⊢ ↑(discr K) ∈ differentIdeal ℤ 𝒪
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: case inr
K : Type u_1
𝒪 : Type u_2
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : CommRing 𝒪
inst✝⁴ : Algebra 𝒪 K
inst✝³ : IsFractionRing 𝒪 K
inst✝² : IsDedekindDomain 𝒪
inst✝¹ : CharZero 𝒪
inst✝ : Module.Finite ℤ 𝒪
this : ↑(discr K).natAbs ∈ differentIdeal ℤ 𝒪
h : discr K = -↑(discr K).natAbs
⊢ ↑(discr K) ∈ differentIdeal ℤ 𝒪

Tactic:
← Int.cast_natCast,

Goal state after:
case inr
K : Type u_1
𝒪 : Type u_2
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : CommRing 𝒪
inst✝⁴ : Algebra 𝒪 K
inst✝³ : IsFractionRing 𝒪 K
inst✝² : IsDedekindDomain 𝒪
inst✝¹ : CharZero 𝒪
inst✝ : Module.Finite ℤ 𝒪
this : ↑↑(discr K).natAbs ∈ differentIdeal ℤ 𝒪
h : discr K = -↑(discr K).natAbs
⊢ ↑(discr K) ∈ differentIdeal ℤ 𝒪
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case refine_1
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 : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹⁵ : CommRing Rₘ
inst✝¹⁴ : Algebra R Rₘ
inst✝¹³ : CommRing Sₘ
inst✝¹² : Algebra S Sₘ
inst✝¹¹ : Algebra Rₘ Sₘ
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : IsScalarTower R Rₘ Sₘ
inst✝⁸ : IsScalarTower R S Sₘ
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁵ : IsIntegrallyClosed Rₘ
inst✝⁴ : IsDomain Rₘ
inst✝³ : IsDomain Sₘ
inst✝² : IsTorsionFree Rₘ Sₘ
inst✝¹ : Module.Finite Rₘ Sₘ
inst✝ : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
algInst✝² : Algebra Rₘ K := f.toAlgebra
algInst✝¹ : Algebra Sₘ L := g.toAlgebra
algInst✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower Rₘ K L := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Rₘ L))
this✝¹ : IsScalarTower R Rₘ K
x✝¹ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
this✝ : IsScalarTower S Sₘ L
this : IsScalarTower Rₘ Sₘ L
x✝ : IsFractionRing Sₘ L :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization (Algebra.algebraMapSubmonoid S M) Sₘ L
⊢ ↑(map (algebraMap S Sₘ) I) ⊆
    ⇑(Algebra.intNorm Rₘ Sₘ) ⁻¹' ↑(Submodule.span Rₘ (⇑(algebraMap R Rₘ) ∘ ⇑(Algebra.intNorm R S) '' ↑I))

Tactic:
intro a' ha'
    simp only [Set.mem_preimage, submodule_span_eq, ← map_spanIntNorm, SetLike.mem_coe,
      IsLocalization.mem_map_algebraMap_iff (Algebra.algebraMapSubmonoid S M) Sₘ,
      IsLocalization.mem_map_algebraMap_iff M Rₘ, Prod.exists] at ha' ⊢
    obtain ⟨⟨a, ha⟩, ⟨_, ⟨s, hs, rfl⟩⟩, has⟩ := ha'
    refine ⟨⟨Algebra.intNorm R S a, intNorm_mem_spanNorm _ ha⟩,
      ⟨s ^ Module.finrank K L, pow_mem hs _⟩, ?_⟩
    simp only [map_pow] at has ⊢
    apply_fun algebraMap _ L at has
    apply_fun Algebra.norm K at has
    simp only [map_mul] at has
    rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
      ← IsScalarTower.algebraMap_apply,
      IsScalarTower.algebraMap_apply R K L,
      Algebra.norm_algebraMap] at has
    apply IsFractionRing.injective Rₘ K
    simp only [map_mul, map_pow]
    rwa [Algebra.algebraMap_intNorm (L := L), ← IsScalarTower.algebraMap_apply,
      ← IsScalarTower.algebraMap_apply, Algebra.algebraMap_intNorm (L := L)]

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

Goal state before:
pp: L : Type u_3
inst✝² : Field L
inst✝¹ : NumberField L
K₁ K₂ : IntermediateField ℚ L
inst✝ : IsGalois ℚ ↥K₁
h : IsCoprime (discr ↥K₁) (discr ↥K₂)
this✝ : K₁ ⊓ K₂ ≠ ⊥
this : 1 < finrank ℚ ↥(K₁ ⊓ K₂)
⊢ ¬|discr ↥(K₁ ⊓ K₂)| = 1

Tactic:
by linarith [abs_discr_gt_two this]

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 : Ideal S
⊢ map (Algebra.intNorm R S) I ≤ comap (algebraMap R S) I

Tactic:
Ideal.map,

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 : Ideal S
⊢ span (⇑(Algebra.intNorm R S) '' ↑I) ≤ comap (algebraMap R S) I
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⁰
⊢ span {(intNorm (Localization.AtPrime P) Tₚ) ((intNorm Tₚ Sₚ) (IsPrincipal.generator (map (algebraMap S Sₚ) I)))} =
    spanNorm Rₚ (span {IsPrincipal.generator (map (algebraMap S Sₚ) I)})

Tactic:
intNorm_intNorm,

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⁰
⊢ span {(intNorm (Localization.AtPrime P) Sₚ) (IsPrincipal.generator (map (algebraMap S Sₚ) I))} =
    spanNorm Rₚ (span {IsPrincipal.generator (map (algebraMap S Sₚ) I)})
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_3.zero
p : ℕ
hp : Fact (Nat.Prime p)
h : ↑p ^ 2 ∣ ↑p
this✝ : 2 ≤ p
this : p < p ^ 2
hk : p = p ^ 2 * 0
⊢ False

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_3.succ
p : ℕ
hp : Fact (Nat.Prime p)
h : ↑p ^ 2 ∣ ↑p
this✝ : 2 ≤ p
this : p < p ^ 2
n✝ : ℕ
hk : p = p ^ 2 * (n✝ + 1)
⊢ False

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

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

Tactic:
intro i hi
      rw [Nat.zero_add, pow_one] at hi ⊢
      exact (cyclotomic_comp_X_add_one_isEisensteinAt p).mem hi

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: 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) = (Int.castRingHom (ZMod p)) ?m.170

Tactic:
rfl

Goal state after: