mathlib-initiative/mathlib-tactics huggingface dataset:
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
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 := ⋯
f : Rₘ →+* K := ⋯
L : Type u_3 := ⋯
g : Sₘ →+* L := ⋯
algInst✝² : Algebra Rₘ K := ⋯
algInst✝¹ : Algebra Sₘ L := ⋯
algInst✝ : Algebra Rₘ L := ⋯
scalarTowerInst✝ : IsScalarTower Rₘ K L := ⋯
this✝ : IsScalarTower R Rₘ K
x✝ : IsFractionRing Rₘ K := ⋯
this : IsScalarTower S Sₘ L
⊢ (algebraMap Rₘ L).comp (algebraMap R Rₘ) = ((algebraMap Sₘ L).comp (algebraMap Rₘ Sₘ)).comp (algebraMap R Rₘ)

Tactic:
RingHom.algebraMap_toAlgebra,

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
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
⊢ ((algebraMap K L).comp f).comp (algebraMap R Rₘ) = ((algebraMap Sₘ L).comp (algebraMap Rₘ Sₘ)).comp (algebraMap R Rₘ)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree
⊢ ((∑ i ∈ range p, X ^ i).comp (X + 1)).coeff i ∈ ℤ ∙ ↑p

Tactic:
geom_sum_X_comp_X_add_one_eq_sum,

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree
⊢ (∑ i ∈ range p, ↑(p.choose (i + 1)) * X ^ i).coeff i ∈ ℤ ∙ ↑p
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ ∃ u n, Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑p ^ n

Tactic:
hζ.discr_zeta_eq_discr_zeta_sub_one.symm

Goal state after:
p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ ∃ u n, Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = ↑↑u * ↑p ^ n
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case refine_1
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
x : K
h : IsIntegral ℤ x
⊢ x ∈ ℤ[ζ]

pp: case refine_2
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
x : K
⊢ (∃ y, (algebraMap (↥ℤ[ζ]) K) y = x) → IsIntegral ℤ x

Tactic:
swap

Goal state after:
case refine_2
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
x : K
⊢ (∃ y, (algebraMap (↥ℤ[ζ]) K) y = x) → IsIntegral ℤ x

case refine_1
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
x : K
h : IsIntegral ℤ x
⊢ x ∈ ℤ[ζ]
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case refine_2
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
x : K
⊢ (∃ y, (algebraMap (↥ℤ[ζ]) K) y = x) → IsIntegral ℤ x

Tactic:
rintro ⟨y, rfl⟩

Goal state after:
case refine_2
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
y : ↥ℤ[ζ]
⊢ IsIntegral ℤ ((algebraMap (↥ℤ[ζ]) K) y)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case refine_2
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
x : CyclotomicField (p ^ k) ℚ
⊢ (∃ y, (algebraMap (CyclotomicRing (p ^ k) ℤ ℚ) (CyclotomicField (p ^ k) ℚ)) y = x) → IsIntegral ℤ x

Tactic:
rintro ⟨y, rfl⟩

Goal state after:
case refine_2
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
y : CyclotomicRing (p ^ k) ℤ ℚ
⊢ IsIntegral ℤ ((algebraMap (CyclotomicRing (p ^ k) ℤ ℚ) (CyclotomicField (p ^ k) ℚ)) y)
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
hcycl : IsCyclotomicExtension {p} ℚ K
hζ✝ : IsPrimitiveRoot ζ p
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (0 + 1))
⊢ Prime ((Algebra.norm ℤ) (hζ✝.toInteger - 1))

Tactic:
exact hζ.prime_norm_toInteger_sub_one_of_prime_ne_two hodd

Goal state after:
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
hcycl : IsCyclotomicExtension {p} ℚ K
hζ✝ : IsPrimitiveRoot ζ p
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (0 + 1))
⊢ ¬∃ n, ↑p ∣ hζ✝.toInteger - ↑n

Tactic:
exact not_exists_int_prime_dvd_sub_of_prime_ne_two hζ hodd

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✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
y : FractionRing B
hy : y ∈ I
⊢ (∃ y_1,
      (algebraMap A (FractionRing A)) y_1 =
        (FractionRing.algEquiv A K).toRingEquiv.symm
          ((Algebra.trace K L) ((FractionRing.algEquiv B L).toRingEquiv ((FractionRing.algEquiv B L).symm x * y)))) ↔
    ∃ y_1, (algebraMap A K) y_1 = (Algebra.trace K L) (x * (FractionRing.algEquiv B L) y)

pp: case he
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✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
y : FractionRing B
hy : y ∈ I
⊢ (algebraMap K L).comp ↑(FractionRing.algEquiv A K).toRingEquiv =
    (↑(FractionRing.algEquiv B L).toRingEquiv).comp (algebraMap (FractionRing A) (FractionRing B))

Tactic:
swap

Goal state after:
case he
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✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
y : FractionRing B
hy : y ∈ I
⊢ (algebraMap K L).comp ↑(FractionRing.algEquiv A K).toRingEquiv =
    (↑(FractionRing.algEquiv B L).toRingEquiv).comp (algebraMap (FractionRing A) (FractionRing B))

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✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
y : FractionRing B
hy : y ∈ I
⊢ (∃ y_1,
      (algebraMap A (FractionRing A)) y_1 =
        (FractionRing.algEquiv A K).toRingEquiv.symm
          ((Algebra.trace K L) ((FractionRing.algEquiv B L).toRingEquiv ((FractionRing.algEquiv B L).symm x * y)))) ↔
    ∃ y_1, (algebraMap A K) y_1 = (Algebra.trace K L) (x * (FractionRing.algEquiv B L) y)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
h : hζ.toInteger - 1 ∣ 2
this : NumberField K
⊢ hζ.toInteger - 1 ∣ ↑2

Tactic:
simp [h]

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

Goal state before:
pp: case h
R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : ℕ → R
hg : ∀ k ∈ range (j + 1), Q.coeff k • B.gen ^ k = (algebraMap R L) p * g k • B.gen ^ k
f : ℕ → L
hf :
  ∀ (i : ℕ),
    (Polynomial.map (algebraMap R L) (minpoly R B.gen)).natDegree ≤ i →
      f i ∈ R[B.gen] ∧ (algebraMap R L) p * f i = B.gen ^ i
k : ℕ
hk : 0 ∈ (range (Q.natDegree - j)).erase 0
h : k = 0
⊢ False

Tactic:
simp at hk

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

Goal state before:
pp: case refine_1
A : Type u_1
K : Type u_2
L : Type u
B : Type ?u.10
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
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : Nontrivial B
inst✝ : NoZeroDivisors B
I : FractionalIdeal B⁰ L
hI : ¬I = 0
s : Finset L
b : Basis (↥s) K L
hb : ∀ (x : ↥s), IsIntegral A (b x)
x : B
hx : x ≠ 0
hx' : (algebraMap B L) x ∈ I
y : B
hy : (algebraMap B L) y = (algebraMap K L) (discr K ⇑b)
⊢ y ≠ 0

Tactic:
rw [← (IsIntegralClosure.algebraMap_injective B A L).ne_iff, hy, map_zero,
        ← (algebraMap K L).map_zero, (algebraMap K L).injective.ne_iff]

Goal state after:
case refine_1
A : Type u_1
K : Type u_2
L : Type u
B : Type ?u.10
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
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : Nontrivial B
inst✝ : NoZeroDivisors B
I : FractionalIdeal B⁰ L
hI : ¬I = 0
s : Finset L
b : Basis (↥s) K L
hb : ∀ (x : ↥s), IsIntegral A (b x)
x : B
hx : x ≠ 0
hx' : (algebraMap B L) x ∈ I
y : B
hy : (algebraMap B L) y = (algebraMap K L) (discr K ⇑b)
⊢ discr K ⇑b ≠ 0
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case e_a.prime_pow
p k : ℕ
hp : Nat.Prime p
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (p ^ k)
hK : IsCyclotomicExtension {p ^ k} ℚ K
this✝ : NumberField K
this : Fact (Nat.Prime p)
⊢ (NumberField.discr K).natAbs = (p ^ k) ^ φ (p ^ k) / ∏ p_1 ∈ (p ^ k).primeFactors, p_1 ^ (φ (p ^ k) / (p_1 - 1))

Tactic:
rw [discr_prime_pow p k K]

Goal state after:
case e_a.prime_pow
p k : ℕ
hp : Nat.Prime p
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (p ^ k)
hK : IsCyclotomicExtension {p ^ k} ℚ K
this✝ : NumberField K
this : Fact (Nat.Prime p)
⊢ ((-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))).natAbs =
    (p ^ k) ^ φ (p ^ k) / ∏ p_1 ∈ (p ^ k).primeFactors, p_1 ^ (φ (p ^ k) / (p_1 - 1))
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
inst✝ : IsTorsionFree B C
this : IsLocalization (algebraMapSubmonoid C B⁰) M
h : B⁰ ≤ Submonoid.comap (algebraMap B C) C⁰
h_alg : ∀ {x : L}, (algebraMap L M) x = (IsLocalization.map M (algebraMap B C) h) x
x : M
hx : x ∈ dual A K 1
⊢ (extendedHom M C) (dual A K 1) ≠ ⊥

Tactic:
by simp [-extendedHom'_apply]

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

Goal state before:
pp: case h
R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : ℕ → R
hg : ∀ k ∈ range (j + 1), Q.coeff k • B.gen ^ k = (algebraMap R L) p * g k • B.gen ^ k
f : ℕ → L
hf :
  ∀ (i : ℕ),
    (Polynomial.map (algebraMap R L) (minpoly R B.gen)).natDegree ≤ i →
      f i ∈ R[B.gen] ∧ (algebraMap R L) p * f i = B.gen ^ i
hf₁ :
  ∀ k ∈ (range (Q.natDegree - j)).erase 0,
    Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
      (algebraMap R L) p * Q.coeff (j + 1 + k) • f (k + P.natDegree - 1)
hQ :
  (Algebra.norm K) ((algebraMap R L) (Q.coeff (j + 1)) * B.gen ^ (j + 1 + (P.natDegree - (j + 2)))) =
    (Algebra.norm K)
      (p • z * B.gen ^ (P.natDegree - (j + 2)) -
        (algebraMap R L) p *
          (∑ i ∈ (range (Q.natDegree - j)).erase 0, Q.coeff (j + 1 + i) • f (i + P.natDegree - 1) +
            ∑ i ∈ range (j + 1), g i • B.gen ^ i * B.gen ^ (P.natDegree - (j + 2))))
k : ℕ
hk : 0 ∈ (range (Q.natDegree - j)).erase 0
h : k = 0
⊢ False

Tactic:
simp at hk

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✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsIntegrallyClosed A
inst✝¹ : IsDedekindDomain B
inst✝ : IsTorsionFree A B
x : B
hx : K[(algebraMap B L) x] = ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
⊢ ↑(conductor A x) =
    FractionalIdeal.spanSingleton B⁰ ((algebraMap B L) ((aeval x) (derivative (minpoly A x)))) *
      FractionalIdeal.dual A K 1

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✝² : IsIntegrallyClosed A
inst✝¹ : IsDedekindDomain B
inst✝ : IsTorsionFree A B
x : B
hx : K[(algebraMap B L) x] = ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
⊢ FractionalIdeal.dual A K 1 ≠ 0

Tactic:
swap

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✝² : IsIntegrallyClosed A
inst✝¹ : IsDedekindDomain B
inst✝ : IsTorsionFree A B
x : B
hx : K[(algebraMap B L) x] = ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
⊢ FractionalIdeal.dual A K 1 ≠ 0

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✝² : IsIntegrallyClosed A
inst✝¹ : IsDedekindDomain B
inst✝ : IsTorsionFree A B
x : B
hx : K[(algebraMap B L) x] = ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
⊢ ↑(conductor A x) =
    FractionalIdeal.spanSingleton B⁰ ((algebraMap B L) ((aeval x) (derivative (minpoly A x)))) *
      FractionalIdeal.dual A K 1
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
n : ℕ
z : L
hzint : IsIntegral R z
hz : p ^ n • z ∈ R[B.gen]
hei : (minpoly R B.gen).IsEisensteinAt (R ∙ p)
⊢ z ∈ R[B.gen]

Tactic:
by
  induction n with
  | zero => simpa using hz
  | succ n hn =>
    rw [_root_.pow_succ', mul_smul] at hz
    exact
      hn (mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt hp hBint (hzint.smul _) hz hei)

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

Goal state before:
pp: case refine_2
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (zeta n ℚ (CyclotomicField n ℚ)) n
x : CyclotomicField n ℚ
⊢ (∃ y, (algebraMap (CyclotomicRing n ℤ ℚ) (CyclotomicField n ℚ)) y = x) → IsIntegral ℤ x

Tactic:
rintro ⟨y, rfl⟩

Goal state after:
case refine_2
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (zeta n ℚ (CyclotomicField n ℚ)) n
y : CyclotomicRing n ℤ ℚ
⊢ IsIntegral ℤ ((algebraMap (CyclotomicRing n ℤ ℚ) (CyclotomicField n ℚ)) y)
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) x‖ ≤ r
w : { w // w ≠ w₀ }
⊢ |(logEmbedding K) (Additive.ofMul x) w| ≤ r

Tactic:
lift r to NNReal using hr

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
w : { w // w ≠ w₀ }
r : NNReal
h : ‖(logEmbedding K) x‖ ≤ ↑r
⊢ |(logEmbedding K) (Additive.ofMul x) w| ≤ ↑r
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✝² : IsIntegrallyClosed A
inst✝¹ : IsDedekindDomain B
inst✝ : IsTorsionFree A B
x : B
hx : K[(algebraMap B L) x] = ⊤
hAx : IsIntegral A x
this✝¹ : IsFractionRing B L
y : L
hne₁ : (aeval ((algebraMap B L) x)) (derivative (minpoly K ((algebraMap B L) x))) ≠ 0
this✝ : (algebraMap B L) ((aeval x) (derivative (minpoly A x))) ≠ 0
hne₂ : ((aeval ((algebraMap B L) x)) (derivative (minpoly K ((algebraMap B L) x))))⁻¹ ≠ 0
this : IsIntegral A ((algebraMap B L) x)
⊢ (∀ (z a : B),
      a ∈ A[x] →
        (Algebra.trace K L)
            (((algebraMap B L) ((aeval x) (derivative (minpoly A x))))⁻¹ * (y * (algebraMap B L) (z * a))) ∈
          (Algebra.linearMap A K).range) ↔
    ∀ (a : B),
      (Algebra.trace K L) (((algebraMap B L) ((aeval x) (derivative (minpoly A x))))⁻¹ * (y * (algebraMap B L) a)) ∈
        (algebraMap A K).range

Tactic:
exact ⟨fun H b ↦ (mul_one b) ▸ H b 1 (one_mem _), fun H _ _ _ ↦ H _⟩

Goal state after: