mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: case inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : HasFiniteQuotients R
S : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
I : Ideal S
hI : I ≠ ⊥
hR : Subsingleton R
this : Finite S
⊢ Finite (S ⧸ I)

Tactic:
exact Quotient.finite _

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
hI : ℤ ∙ n ≠ ⊥
⊢ n ≠ 0

Tactic:
by simpa using hI

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: case hIJ
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    map (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
⊢ ?mp.I ≤ ⊥.jacobson

Tactic:
exact (jacobson_eq_maximalIdeal ⊥ bot_ne_top).ge

Goal state after:
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 + (IsLocalization.map W g hg) z ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))

Tactic:
exact add_mem hy hz

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

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

Tactic:
exact Multiset.count_eq_zero.mpr fun hQi ↦
    hQp <| isPrime_of_prime <| irreducible_iff_prime.mp <| irreducible_of_normalized_factor _ hQi

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

Goal state before:
pp: 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✝ :
  (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) ≃ₗ[𝒪]
    ↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1
this :
  Nat.card (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) =
    Nat.card (↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1)
⊢ Nat.card (↥↑(FractionalIdeal.dual ℤ ℚ 1)⁻¹⁻¹ ⧸ Submodule.comap (↑(FractionalIdeal.dual ℤ ℚ 1)⁻¹⁻¹).subtype 1) =
    (discr K).natAbs

Tactic:
inv_inv

Goal state after:
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✝ :
  (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) ≃ₗ[𝒪]
    ↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1
this :
  Nat.card (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) =
    Nat.card (↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1)
⊢ Nat.card (↥↑(FractionalIdeal.dual ℤ ℚ 1) ⧸ Submodule.comap (↑(FractionalIdeal.dual ℤ ℚ 1)).subtype 1) =
    (discr K).natAbs
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

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

Tactic:
· exact ⟨p ^ n, by rw [pow_succ']⟩

Goal state after:
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
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K
H : Algebra.discr ℚ ⇑B.basis • x ∈ ℤ[B.gen]
u : ℤˣ
n : ℕ
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑p ^ n
⊢ x ∈ ℤ[ζ]

Tactic:
hun

Goal state after:
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
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K
u : ℤˣ
n : ℕ
H : (↑↑u * ↑p ^ n) • x ∈ ℤ[B.gen]
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑p ^ n
⊢ x ∈ ℤ[ζ]
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))
s : ℕ
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
⊢ (Algebra.norm ℤ) (hζ.toInteger ^ p ^ s - 1) = ↑p ^ p ^ s

Tactic:
have : NumberField K := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K
  rw [Algebra.norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl]
  simp [hζ.norm_pow_sub_one_of_prime_pow_ne_two (cyclotomic.irreducible_rat (NeZero.pos _)) hs htwo]

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

Goal state before:
pp: case a
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst✝⁵⁵ : CommRing A
inst✝⁵⁴ : Field K
inst✝⁵³ : Algebra A K
inst✝⁵² : IsFractionRing A K
inst✝⁵¹ : CommRing B
inst✝⁵⁰ : Field L
inst✝⁴⁹ : Algebra B L
inst✝⁴⁸ : Algebra A L
inst✝⁴⁷ : Algebra K L
inst✝⁴⁶ : FiniteDimensional K L
inst✝⁴⁵ : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst✝⁴⁴ : CommRing R₁
inst✝⁴³ : CommRing R₂
inst✝⁴² : IsDomain R₁
inst✝⁴¹ : Algebra A R₁
inst✝⁴⁰ : Algebra A R₂
inst✝³⁹ : Algebra R₁ B
inst✝³⁸ : Algebra R₂ B
inst✝³⁷ : Algebra R₁ L
inst✝³⁶ : Algebra R₂ L
inst✝³⁵ : IsScalarTower A R₁ L
inst✝³⁴ : IsScalarTower R₁ B L
inst✝³³ : IsScalarTower R₂ B L
inst✝³² : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst✝³¹ : Algebra R₁ ↥F₁
inst✝³⁰ : Algebra R₂ ↥F₂
inst✝²⁹ : IsTorsionFree R₁ ↥F₁
inst✝²⁸ : IsScalarTower A (↥F₂) L
inst✝²⁷ : IsScalarTower A R₂ ↥F₂
inst✝²⁶ : IsScalarTower R₁ (↥F₁) L
inst✝²⁵ : IsScalarTower R₂ (↥F₂) L
inst✝²⁴ : Algebra.IsSeparable K ↥F₂
inst✝²³ : Algebra.IsSeparable (↥F₁) L
inst✝²² : IsDomain A
inst✝²¹ : IsDedekindDomain B
inst✝²⁰ : IsDedekindDomain R₁
inst✝¹⁹ : IsDedekindDomain R₂
inst✝¹⁸ : IsFractionRing B L
inst✝¹⁷ : IsFractionRing R₁ ↥F₁
inst✝¹⁶ : IsFractionRing R₂ ↥F₂
inst✝¹⁵ : IsIntegrallyClosed A
inst✝¹⁴ : IsIntegralClosure B R₁ L
inst✝¹³ : IsTorsionFree R₁ B
inst✝¹² : IsTorsionFree R₂ B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Module.Finite A B
inst✝⁹ : IsTorsionFree A B
inst✝⁸ : IsTorsionFree A R₁
inst✝⁷ : IsTorsionFree A R₂
inst✝⁶ : Module.Finite A R₁
inst✝⁵ : Module.Finite R₂ B
inst✝⁴ : IsScalarTower A R₂ B
inst✝³ : Module.Finite R₁ B
inst✝² : Algebra.IsSeparable (FractionRing A) (FractionRing B)
inst✝¹ : IsScalarTower A R₁ B
inst✝ : Free A R₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
h₃ : IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))
⊢ differentIdeal R₁ B ∣ Ideal.map (algebraMap R₂ B) (differentIdeal A R₂)

Tactic:
exact differentIdeal_dvd_map_differentIdeal A B R₁ R₂ h₁ h₂

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]
      exact discr_not_zero_of_basis K b

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

Goal state before:
pp: case neg
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp : ↑p ∣ 1
h✝ : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 < n
h : ∀ (q : ℕ), Nat.Prime q → ∀ (t : ℕ), q ^ t ≠ n
⊢ ∃ q, Nat.Prime q ∧ ∃ t s, t ≠ 0 ∧ n = q ^ t ∧ ↑p ∣ ↑q ^ s

pp: case neg
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h✝ : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 < n
h : ∀ (q : ℕ), Nat.Prime q → ∀ (t : ℕ), q ^ t ≠ n
⊢ ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n

Tactic:
Int.natCast_dvd_ofNat,

Goal state after:
case neg
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp : p ∣ 1
h✝ : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 < n
h : ∀ (q : ℕ), Nat.Prime q → ∀ (t : ℕ), q ^ t ≠ n
⊢ ∃ q, Nat.Prime q ∧ ∃ t s, t ≠ 0 ∧ n = q ^ t ∧ ↑p ∣ ↑q ^ s

case neg
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h✝ : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 < n
h : ∀ (q : ℕ), Nat.Prime q → ∀ (t : ℕ), q ^ t ≠ n
⊢ ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case inr
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension {2} ℚ ↥ℚ⟮ζ⟯
hμ✝ : IsPrimitiveRoot μ n
hμ : IsPrimitiveRoot μ 2
hp : ↑p ∣ (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 = n
⊢ ↑p ∣ ↑2 ^ Module.finrank (↥ℚ⟮ζ⟯) K

Tactic:
rwa [hμ.norm_toInteger_sub_one_of_eq_two, neg_eq_neg_one_mul, mul_pow, IsUnit.dvd_mul_left
        ((isUnit_pow_iff Module.finrank_pos.ne').mpr isUnit_neg_one)] at hp

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

Goal state before:
pp: case neg.a
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✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : ¬I = 0
⊢ dual A K I * I ≤ dual A K 1

Tactic:
← le_dual_iff A K hI

Goal state after:
case neg.a
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✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : ¬I = 0
⊢ dual A K I ≤ dual A K I
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✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
⊢ dual A K 1 * I⁻¹⁻¹ = dual A K 1 * I

Tactic:
inv_inv

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✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
⊢ dual A K 1 * I = dual A K 1 * I
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
B : Type u_4
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : IsIntegrallyClosed A
inst✝¹³ : IsDedekindDomain B
inst✝¹² : IsTorsionFree A B
C : Type u_3
inst✝¹¹ : IsDomain B
inst✝¹⁰ : CommRing C
inst✝⁹ : Algebra B C
inst✝⁸ : Algebra A C
inst✝⁷ : IsDedekindDomain C
inst✝⁶ : Module.Finite A B
inst✝⁵ : Module.Finite A C
inst✝⁴ : Module.Finite B C
inst✝³ : IsTorsionFree A C
inst✝² : IsTorsionFree B C
inst✝¹ : IsScalarTower A B C
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing C)
this✝³ : Algebra.IsSeparable (FractionRing B) (FractionRing C)
this✝² : Algebra.IsSeparable (FractionRing A) (FractionRing B)
this✝¹ : FiniteDimensional (FractionRing A) (FractionRing B)
this✝ : FiniteDimensional (FractionRing A) (FractionRing C)
this : FiniteDimensional (FractionRing B) (FractionRing C)
⊢ (dual A (FractionRing A) 1)⁻¹⁻¹ =
    dual B (FractionRing B) 1 * (extendedHom (FractionRing C) C) (dual A (FractionRing A) 1)

Tactic:
inv_inv

Goal state after:
A : Type u_1
B : Type u_4
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : IsIntegrallyClosed A
inst✝¹³ : IsDedekindDomain B
inst✝¹² : IsTorsionFree A B
C : Type u_3
inst✝¹¹ : IsDomain B
inst✝¹⁰ : CommRing C
inst✝⁹ : Algebra B C
inst✝⁸ : Algebra A C
inst✝⁷ : IsDedekindDomain C
inst✝⁶ : Module.Finite A B
inst✝⁵ : Module.Finite A C
inst✝⁴ : Module.Finite B C
inst✝³ : IsTorsionFree A C
inst✝² : IsTorsionFree B C
inst✝¹ : IsScalarTower A B C
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing C)
this✝³ : Algebra.IsSeparable (FractionRing B) (FractionRing C)
this✝² : Algebra.IsSeparable (FractionRing A) (FractionRing B)
this✝¹ : FiniteDimensional (FractionRing A) (FractionRing B)
this✝ : FiniteDimensional (FractionRing A) (FractionRing C)
this : FiniteDimensional (FractionRing B) (FractionRing C)
⊢ dual A (FractionRing A) 1 = dual B (FractionRing B) 1 * (extendedHom (FractionRing C) C) (dual A (FractionRing A) 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✝² : 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 A x)) ≠ 0
⊢ (algebraMap B L) ((aeval x) (derivative (minpoly A x))) ≠ 0

Tactic:
aeval_algebraMap_apply

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
y : L
hne₁ : (algebraMap B L) ((aeval x) (derivative (minpoly A x))) ≠ 0
⊢ (algebraMap B L) ((aeval x) (derivative (minpoly A x))) ≠ 0
Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint

Goal state before:
pp: case e'_2
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst✝⁵⁴ : CommRing A
inst✝⁵³ : Field K
inst✝⁵² : Algebra A K
inst✝⁵¹ : IsFractionRing A K
inst✝⁵⁰ : CommRing B
inst✝⁴⁹ : Field L
inst✝⁴⁸ : Algebra B L
inst✝⁴⁷ : Algebra A L
inst✝⁴⁶ : Algebra K L
inst✝⁴⁵ : FiniteDimensional K L
inst✝⁴⁴ : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst✝⁴³ : CommRing R₁
inst✝⁴² : CommRing R₂
inst✝⁴¹ : IsDomain R₁
inst✝⁴⁰ : Algebra A R₁
inst✝³⁹ : Algebra A R₂
inst✝³⁸ : Algebra R₁ B
inst✝³⁷ : Algebra R₂ B
inst✝³⁶ : Algebra R₁ L
inst✝³⁵ : Algebra R₂ L
inst✝³⁴ : IsScalarTower A R₁ L
inst✝³³ : IsScalarTower R₁ B L
inst✝³² : IsScalarTower R₂ B L
inst✝³¹ : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst✝³⁰ : Algebra R₁ ↥F₁
inst✝²⁹ : Algebra R₂ ↥F₂
inst✝²⁸ : IsTorsionFree R₁ ↥F₁
inst✝²⁷ : IsScalarTower A (↥F₂) L
inst✝²⁶ : IsScalarTower A R₂ ↥F₂
inst✝²⁵ : IsScalarTower R₁ (↥F₁) L
inst✝²⁴ : IsScalarTower R₂ (↥F₂) L
inst✝²³ : Algebra.IsSeparable K ↥F₂
inst✝²² : Algebra.IsSeparable (↥F₁) L
inst✝²¹ : IsDomain A
inst✝²⁰ : IsDedekindDomain B
inst✝¹⁹ : IsDedekindDomain R₁
inst✝¹⁸ : IsDedekindDomain R₂
inst✝¹⁷ : IsFractionRing B L
inst✝¹⁶ : IsFractionRing R₁ ↥F₁
inst✝¹⁵ : IsFractionRing R₂ ↥F₂
inst✝¹⁴ : IsIntegrallyClosed A
inst✝¹³ : IsIntegralClosure B R₁ L
inst✝¹² : IsTorsionFree R₁ B
inst✝¹¹ : IsTorsionFree R₂ B
inst✝¹⁰ : Algebra A B
inst✝⁹ : Module.Finite A B
inst✝⁸ : IsTorsionFree A B
inst✝⁷ : IsTorsionFree A R₁
inst✝⁶ : IsTorsionFree A R₂
inst✝⁵ : Module.Finite A R₁
inst✝⁴ : Module.Finite R₂ B
inst✝³ : IsScalarTower A R₂ B
inst✝² : Module.Finite R₁ B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
inst✝ : IsScalarTower A R₁ B
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
h₃ : IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))
ι : Type u_7
b : Basis ι A R₂
this : Free A R₂
v : ι → B := fun i ↦ (algebraMap R₂ B) (b i)
b₂ : Basis ι K ↥F₂ := localizationLocalization K A⁰ (↥F₂) b
P₁ : LinearIndependent R₁ v
x✝ : ι
⊢ (⇑(IsScalarTower.toAlgHom R₁ B L).toLinearMap ∘ v) x✝ = (h₁.basisOfBasisRight h₂ b₂) x✝

Tactic:
simp [b₂, v, ← IsScalarTower.algebraMap_apply]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
⊢ v w x < 0

Tactic:
· refine mul_neg_of_pos_of_neg ?_ ((exists_unit K w).choose_spec x ?_)
    · rw [mult]; split_ifs <;> norm_num
    · exact Subtype.ext_iff.not.mp (ne_of_mem_erase hx)

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ ↑⋯.unit ^ 2 + ↑⋯.unit + 1 = 0

Tactic:
rw [eta_sq]

Goal state after:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ -↑⋯.unit - 1 + ↑⋯.unit + 1 = 0
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i, fundSystem K i ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i)⁻¹
⊢ Additive.ofMul ↑x +
      -∑ x_1,
          ((basisModTorsion K).repr (Additive.ofMul ↑x)) x_1 •
            Additive.ofMul ↑(Quotient.out (Additive.toMul ((basisModTorsion K) x_1))) =
    0

Tactic:
QuotientGroup.out_eq'

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i, fundSystem K i ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i)⁻¹
⊢ Additive.ofMul ↑x +
      -∑ x_1,
          ((basisModTorsion K).repr (Additive.ofMul ↑x)) x_1 •
            Additive.ofMul (Additive.toMul ((basisModTorsion K) x_1)) =
    0
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
⊢ ¬P ∣ differentIdeal A B

Tactic:
have : FiniteDimensional K L := .of_isLocalization A B A⁰

Goal state after:
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
⊢ ¬P ∣ differentIdeal A B
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ legendreSym p 0 = 0

Tactic:
rw [legendreSym, Int.cast_zero, MulChar.map_zero]

Goal state after: