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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)

Tactic:
by
  let Rₚ := Localization.AtPrime p
  let Sₚ := Localization (Algebra.algebraMapSubmonoid S p.primeCompl)
  let : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
  have : IsScalarTower R Rₚ Sₚ := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq])
  have : IsLocalization (Submonoid.map (algebraMap R S) (Ideal.primeCompl p)) Sₚ :=
    inferInstanceAs (IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ)
  have e : Algebra.algebraMapSubmonoid S p.primeCompl ≤ S⁰ :=
    Submonoid.map_le_of_le_comap _ <| p.primeCompl_le_nonZeroDivisors.trans
      (nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _
        (FaithfulSMul.algebraMap_injective _ _))
  have : IsDomain Sₚ := IsLocalization.isDomain_of_le_nonZeroDivisors _ e
  have : IsTorsionFree Rₚ Sₚ := by
    rw [isTorsionFree_iff_algebraMap_injective, RingHom.injective_iff_ker_eq_bot,
      RingHom.ker_eq_bot_iff_eq_zero]
    simp
  have : Module.Finite Rₚ Sₚ := .of_isLocalization R S p.primeCompl
  have : IsIntegrallyClosed Sₚ := isIntegrallyClosed_of_isLocalization _ _ e
  have : IsPrincipalIdealRing Rₚ := by
    by_cases hp : p = ⊥
    · infer_instance
    · have := (IsDedekindDomain.isDedekindDomainDvr R).2 p hp inferInstance
      infer_instance
  have : Module.Free Rₚ Sₚ := Module.free_of_finite_type_torsion_free'
  apply (equivQuotMaximalIdeal p Rₚ).injective
  rw [trace_quotient_eq_trace_localization_quotient S p Rₚ Sₚ, IsScalarTower.algebraMap_eq S Sₚ,
    RingHom.comp_apply, Ideal.Quotient.algebraMap_eq, Algebra.trace_quotient_mk,
    RingEquiv.apply_symm_apply, ← Algebra.intTrace_eq_trace,
    ← Algebra.intTrace_eq_of_isLocalization R S p.primeCompl (Aₘ := Rₚ) (Bₘ := Sₚ) x,
    ← Ideal.Quotient.algebraMap_eq, ← IsScalarTower.algebraMap_apply]
  simp only [equivQuotMaximalIdeal, RingHom.quotientKerEquivOfSurjective, RingEquiv.coe_trans,
    Function.comp_apply, Ideal.quotEquivOfEq_mk, RingHom.quotientKerEquivOfRightInverse.apply,
    RingHom.kerLift_mk]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case pos.eq_bot_or_top
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
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I✝ J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
hP : ⊥.IsMaximal
I : Ideal R
⊢ I = ⊥ ∨ I = ⊤

Tactic:
exact or_iff_not_imp_right.mpr fun hI ↦ (hP.eq_of_le hI bot_le).symm

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
inst✝¹ : IsDedekindDomain R
inst✝ : IsDedekindDomain S
I P : Ideal R
hPd : P.IsMaximal
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
K : Type u_1 := FractionRing R
⊢ (Algebra.norm K)
      ((algebraMap K (FractionRing S)) ((algebraMap Rₚ K) (IsPrincipal.generator (map (algebraMap R Rₚ) I)))) =
    (algebraMap Rₚ K) (IsPrincipal.generator (map (algebraMap R Rₚ) I) ^ finrank R S)

Tactic:
Algebra.norm_algebraMap,

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
inst✝¹ : IsDedekindDomain R
inst✝ : IsDedekindDomain S
I P : Ideal R
hPd : P.IsMaximal
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
K : Type u_1 := FractionRing R
⊢ (algebraMap Rₚ K) (IsPrincipal.generator (map (algebraMap R Rₚ) I)) ^ finrank K (FractionRing S) =
    (algebraMap Rₚ K) (IsPrincipal.generator (map (algebraMap R Rₚ) I) ^ finrank R S)
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
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : IsDedekindDomain S
R' : Type u_4
inst✝³ : CommRing R'
I : Ideal R'
inst✝² : Algebra R' R
inst✝¹ : Algebra R' S
inst✝ : IsScalarTower R' R S
⊢ (relNorm R) (map (algebraMap R' S) I) = map (algebraMap R' R) I ^ finrank R S

Tactic:
← relNorm_algebraMap,

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
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : IsDedekindDomain S
R' : Type u_4
inst✝³ : CommRing R'
I : Ideal R'
inst✝² : Algebra R' R
inst✝¹ : Algebra R' S
inst✝ : IsScalarTower R' R S
⊢ (relNorm R) (map (algebraMap R' S) I) = (relNorm R) (map (algebraMap R S) (map (algebraMap R' R) I))
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case h.calc_3
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
Q : R[X]
hQ : (aeval B.gen) Q = p • z
hzint : IsIntegral R z
hei : (minpoly R B.gen).IsEisensteinAt (R ∙ p)
this : Module.Finite K L := finite B
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : (minpoly K B.gen).natDegree = B.dim
deg_R_P : P.natDegree = B.dim
f : ℕ → L
hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ R[B.gen] ∧ (algebraMap R L) p * f i = B.gen ^ i
aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n
hintsum : IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))
r : R
hr :
  (algebraMap R K) r = (Algebra.norm K) (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))
⊢ (Algebra.norm K) ((algebraMap K L) ((algebraMap R K) p)) *
      (Algebra.norm K) (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n)) =
    (algebraMap R K) p ^ n.succ * (algebraMap R K) r

Tactic:
Algebra.norm_algebraMap,

Goal state after:
case h.calc_3
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
Q : R[X]
hQ : (aeval B.gen) Q = p • z
hzint : IsIntegral R z
hei : (minpoly R B.gen).IsEisensteinAt (R ∙ p)
this : Module.Finite K L := finite B
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : (minpoly K B.gen).natDegree = B.dim
deg_R_P : P.natDegree = B.dim
f : ℕ → L
hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ R[B.gen] ∧ (algebraMap R L) p * f i = B.gen ^ i
aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n
hintsum : IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))
r : R
hr :
  (algebraMap R K) r = (Algebra.norm K) (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))
⊢ (algebraMap R K) p ^ Module.finrank K L *
      (Algebra.norm K) (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n)) =
    (algebraMap R K) p ^ n.succ * (algebraMap R K) r
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
h : p ≠ 2
⊢ (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑p

Tactic:
have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by simpa using hcycl
  replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ
  exact hζ.norm_toInteger_sub_one_of_prime_ne_two h

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
I J : Submodule B L
⊢ I ≤ Jᵛ ↔ map (↑A (Algebra.trace K L)) (restrictScalars A (I * J)) ≤ 1

Tactic:
rw [Submodule.map_le_iff_le_comap, Submodule.restrictScalars_mul, Submodule.mul_le]
  simp [SetLike.le_def, mem_traceDual]

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

Goal state before:
pp: case neg
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
b : L
hb : ∀ (x : A), ¬(algebraMap A K) x = (Algebra.trace K L) b
⊢ ⊤ᵛ ≤ ⊥

Tactic:
SetLike.le_def,

Goal state after:
case neg
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
b : L
hb : ∀ (x : A), ¬(algebraMap A K) x = (Algebra.trace K L) b
⊢ ∀ ⦃x : L⦄, x ∈ ⊤ᵛ → 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ hζ.toInteger - 1 ∣ ↑p

Tactic:
by
  by_cases htwo : p ^ (k + 1) = 2
  · have ⟨hp2, hk⟩ := (Nat.Prime.pow_eq_iff Nat.prime_two).1 htwo
    simp only [add_eq_right] at hk
    have hζ' : ζ = -1 := by
      refine IsPrimitiveRoot.eq_neg_one_of_two_right ?_
      rwa [hk, zero_add, pow_one, hp2] at hζ
    replace hζ' : hζ.toInteger = -1 := by
      ext
      exact hζ'
    rw [hζ', hp2]
    exact ⟨-1, by ring⟩
  suffices (hζ.toInteger - 1) ∣ (p : ℤ) by simpa
  have := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K
  have H := hζ.norm_toInteger_pow_sub_one_of_prime_pow_ne_two zero_le htwo
  rw [pow_zero, pow_one] at H
  rw [← Ideal.norm_dvd_iff, H]
  · simp
  · exact prime_norm_toInteger_sub_one_of_prime_pow_ne_two hζ htwo

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

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

Tactic:
Algebra.norm_algebraMap,

Goal state after:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
hp : ↑p ∣ (Algebra.norm ℤ) (hζ.toInteger - 1)
this✝ : NeZero n
this : NumberField ↥ℚ⟮ζ⟯
⊢ (Algebra.norm ℚ) ((AdjoinSimple.gen ℚ ζ - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K) =
    (algebraMap ℤ ℚ) ((Algebra.norm ℤ) (⋯.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K)
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 : B),
      ((aeval ((algebraMap B L) x)) (derivative (minpoly K ((algebraMap B L) x))))⁻¹ * (y * (algebraMap B L) z) ∈
        ((aeval ((algebraMap B L) x)) (derivative (minpoly K ((algebraMap B L) x))))⁻¹ •
          Subalgebra.toSubmodule A[(algebraMap B L) x]) ↔
    ∀ a ∈ 1,
      ((traceForm K L) (((algebraMap B L) ((aeval x) (derivative (minpoly A x))))⁻¹ * y)) a ∈ (algebraMap A K).range

Tactic:
rw [← traceForm_dualSubmodule_adjoin A K hx this]

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₁ : (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 : B),
      ((aeval ((algebraMap B L) x)) (derivative (minpoly K ((algebraMap B L) x))))⁻¹ * (y * (algebraMap B L) z) ∈
        (traceForm K L).dualSubmodule (Subalgebra.toSubmodule A[(algebraMap B L) x])) ↔
    ∀ a ∈ 1,
      ((traceForm K L) (((algebraMap B L) ((aeval x) (derivative (minpoly A x))))⁻¹ * y)) a ∈ (algebraMap A K).range
Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint

Goal state before:
pp: 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₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
h₃ : IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))
s : Set R₁
t : Set R₂
hs : Algebra.adjoin A s = ⊤
ht : Algebra.adjoin A t = ⊤
⊢ Algebra.adjoin A (⇑(algebraMap R₁ B) '' s ∪ ⇑(algebraMap R₂ B) '' t) = ⊤

Tactic:
by
  rw [Algebra.adjoin_union, ← IsScalarTower.coe_toAlgHom' A R₁, ← IsScalarTower.coe_toAlgHom' A R₂,
    ← AlgHom.map_adjoin, hs, ← AlgHom.map_adjoin, ht, Algebra.map_top, Algebra.map_top]
  exact range_sup_range_eq_top_of_isCoprime_differentIdeal A B R₁ R₂ h₁ h₂ h₃

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ x ^ 3 - 1 = (x - 1) * (x - 1 - λ) * (x - 1 - λ * (↑η + 1))

Tactic:
simp only [coe_eta, cube_sub_one_eq_mul hζ x]

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ (x - 1) * (x - hζ.toInteger) * (x - hζ.toInteger ^ 2) = (x - 1) * (x - 1 - λ) * (x - 1 - λ * (hζ.toInteger + 1))
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case pos
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : a ^ 3 + b ^ 3 = c ^ 3
h1 : 3 ∣ a * b * c
⊢ False

Tactic:
prime_three.dvd_mul,

Goal state after:
case pos
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : a ^ 3 + b ^ 3 = c ^ 3
h1 : 3 ∣ a * b ∨ 3 ∣ c
⊢ False
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Tactic:
simp only [FiniteField.isSquare_of_char_two hF, true_iff]

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7

Tactic:
simp only [FiniteField.isSquare_of_char_two hF, true_iff]

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
h : Fintype.card F % 2 = 0
⊢ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case inr.mp.right.hle
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 B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) := ⋯
H : ¬P ∣ differentIdeal A B
⊢ Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) P) ≤ P ^ 1

Tactic:
simp [Ideal.map_le_iff_le_comap]

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
v : AbsoluteValue K ℝ
j : ι ⊕ ι'
⊢ v (Sum.elim x 0 j) ≤ ⨆ i, v (x i)

Tactic:
cases j with

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log (↑n + 1) - log ↑n - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, x ^ (-2) = log (↑n + 1) - log ↑n - ↑n * (1 / ↑n - 1 / (↑n + 1))

Tactic:
by
      rw [integral_rpow]
      · simp_rw [sub_div, (by norm_num : (-2 : ℝ) + 1 = -1), div_neg, div_one, neg_sub_neg,
          rpow_neg_one, ← one_div]
      · refine Or.inr ⟨by simp, notMem_uIcc_of_lt ?_ ?_⟩
        all_goals positivity

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ (Multiset.map (fun v ↦ max (v (∑ a ∈ s, x a)) 1) archAbsVal).prod *
      ∏ᶠ (v : ↑nonarchAbsVal), max (↑v (∑ a ∈ s, x a)) 1 ≤
    (Multiset.map (Function.const (AbsoluteValue K ℝ) ↑(#s)) archAbsVal).prod *
      ((∏ x_1 ∈ s, (Multiset.map (fun v ↦ max (v (x x_1)) 1) archAbsVal).prod) *
        ∏ᶠ (a : ↑nonarchAbsVal), ∏ b ∈ s, max (↑a (x b)) 1)

Tactic:
← prod_map_prod,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ (Multiset.map (fun v ↦ max (v (∑ a ∈ s, x a)) 1) archAbsVal).prod *
      ∏ᶠ (v : ↑nonarchAbsVal), max (↑v (∑ a ∈ s, x a)) 1 ≤
    (Multiset.map (Function.const (AbsoluteValue K ℝ) ↑(#s)) archAbsVal).prod *
      ((Multiset.map (fun i ↦ ∏ a ∈ s, max (i (x a)) 1) archAbsVal).prod *
        ∏ᶠ (a : ↑nonarchAbsVal), ∏ b ∈ s, max (↑a (x b)) 1)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case h₂
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ ∏ᶠ (v : ↑nonarchAbsVal), max (↑v (∑ a ∈ s, x a)) 1 ≤ ∏ᶠ (a : ↑nonarchAbsVal), ∏ b ∈ s, max (↑a (x b)) 1

Tactic:
· exact finprod_le_finprod (by fun_prop) (fun _ ↦ by grind) (by fun_prop) <|
      fun v ↦ max_abv_sum_one_le_of_isNonarchimedean (isNonarchimedean _ v.prop) _ x

Goal state after:
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
m n : ℕ
hn : n ≠ 0
a : 𝓞 K
⊢ (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, a})) =
    (Submodule.toAddSubgroup (span {↑n * ↑m})).relIndex (Submodule.toAddSubgroup (span {↑(n * m), ↑n * a}))

Tactic:
let f : 𝓞 K →ₗ[𝓞 K] 𝓞 K := .mulLeft _ n
  have hf : Function.Injective (f : 𝓞 K →+ 𝓞 K) :=
    (injective_iff_map_eq_zero f).mpr fun _ _ ↦ by simp_all [f]
  have H₁ : span {(n * m : 𝓞 K)} = Submodule.map f (span {↑m}) := by
    simp [LinearMap.map_span, f]
  have H₂ : span {↑(n * m), n * a} = Submodule.map f (span {↑m, a}) := by
    simp [LinearMap.map_span, f, Set.image_pair]
  rw [H₁, H₂]
  exact AddSubgroup.relIndex_map_map_of_injective _ _ hf |>.symm

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case pos
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
⊢ 1 ≤ max C 1 * mulHeight ![c, d]

Tactic:
← one_le_mulHeight

Goal state after:
case pos
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
⊢ 1 ≤ max C 1 * 1