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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I
⊢ (latticeBasis K).det (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e) =
    (algebraMap ℚ ℝ) ((integralBasis K).det (⇑(basisOfFractionalIdeal K I) ∘ ⇑e))

Tactic:
Basis.det_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I
⊢ ((latticeBasis K).toMatrix (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e)).det =
    (algebraMap ℚ ℝ) ((integralBasis K).det (⇑(basisOfFractionalIdeal K I) ∘ ⇑e))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I
⊢ ((latticeBasis K).toMatrix (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e)).det =
    (algebraMap ℚ ℝ) ((integralBasis K).det (⇑(basisOfFractionalIdeal K I) ∘ ⇑e))

Tactic:
Basis.det_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I
⊢ ((latticeBasis K).toMatrix (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e)).det =
    (algebraMap ℚ ℝ) ((integralBasis K).toMatrix (⇑(basisOfFractionalIdeal K I) ∘ ⇑e)).det
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ :
  |((↑⟨w₀, hw₀⟩).embedding ↑a).re| < 1 ∧
    |((↑⟨w₀, hw₀⟩).embedding ↑a).im| < ↑(if ↑⟨w₀, hw₀⟩ = w₀ then NNReal.sqrt B else 1) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ w ↑a < √(1 + ↑B ^ 2)

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ :
  |((↑⟨w₀, hw₀⟩).embedding ↑a).re| < 1 ∧
    |((↑⟨w₀, hw₀⟩).embedding ↑a).im| < ↑(if ↑⟨w₀, hw₀⟩ = w₀ then NNReal.sqrt B else 1) ^ 2
w : InfinitePlace K
h_eq : ¬w = w₀
⊢ w ↑a < √(1 + ↑B ^ 2)

Tactic:
· rw [if_pos rfl] at h_le₀
      dsimp only at h_le₀
      rw [h_eq, ← norm_embedding_eq, Real.lt_sqrt (norm_nonneg _), ← Complex.re_add_im
        (embedding w₀ _), Complex.norm_add_mul_I, Real.sq_sqrt (by positivity)]
      refine add_lt_add ?_ ?_
      · rw [← sq_abs, sq_lt_one_iff₀ (abs_nonneg _)]
        exact h_le₀.1
      · rw [sq_lt_sq, NNReal.abs_eq, ← NNReal.sq_sqrt B]
        exact h_le₀.2

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ :
  |((↑⟨w₀, hw₀⟩).embedding ↑a).re| < 1 ∧
    |((↑⟨w₀, hw₀⟩).embedding ↑a).im| < ↑(if ↑⟨w₀, hw₀⟩ = w₀ then NNReal.sqrt B else 1) ^ 2
w : InfinitePlace K
h_eq : ¬w = w₀
⊢ w ↑a < √(1 + ↑B ^ 2)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measure.map (⇑(toMixed K)) volume = volume

Tactic:
by
    rw [← (OrthonormalBasis.addHaar_eq_volume (euclidean.stdOrthonormalBasis K)), Basis.map_addHaar,
      stdOrthonormalBasis_map_eq, Basis.addHaar_eq_iff, Basis.coe_parallelepiped,
      ← measure_congr (ZSpan.fundamentalDomain_ae_parallelepiped (stdBasis K) volume),
      volume_fundamentalDomain_stdBasis K]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ↑(finrank ℚ K) ^ (2 * finrank ℚ K) / ((4 / π) ^ (2 * nrComplexPlaces K) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|

Tactic:
obtain ⟨x, h_nz, h_bd⟩ := exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr K
  have h_nm : (1 : ℝ) ≤ |Algebra.norm ℚ (x : K)| := by
    rw [← Algebra.coe_norm_int, ← Int.cast_one, ← Int.cast_abs, Rat.cast_intCast, Int.cast_le]
    exact Int.one_le_abs (Algebra.norm_ne_zero_iff.mpr h_nz)
  replace h_bd := le_trans h_nm h_bd
  rwa [← inv_mul_le_iff₀, inv_div, mul_one, Real.le_sqrt (by positivity) (by positivity),
    ← Int.cast_abs, div_pow, mul_pow, ← pow_mul, mul_comm _ 2, ← pow_mul, mul_comm _ 2] at h_bd
  exact div_pos (by positivity) <| pow_pos (Nat.cast_pos.mpr finrank_pos) (finrank ℚ K)

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝²⁰ : CommRing A
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst✝¹⁷ : Group G
inst✝¹⁶ : Finite G
inst✝¹⁵ : MulSemiringAction G B
inst✝¹⁴ : IsGaloisGroup G A B
C : Type u_4
inst✝¹³ : CommRing C
inst✝¹² : Algebra A C
inst✝¹¹ : Algebra B C
inst✝¹⁰ : Nonempty ↑(P.primesOver C)
inst✝⁹ : IsScalarTower A B C
GAC : Type u_5
inst✝⁸ : Group GAC
inst✝⁷ : Finite GAC
inst✝⁶ : MulSemiringAction GAC C
inst✝⁵ : IsGaloisGroup GAC A C
GBC : Type u_6
inst✝⁴ : Group GBC
inst✝³ : Finite GBC
inst✝² : MulSemiringAction GBC C
inst✝¹ : IsGaloisGroup GBC B C
inst✝ : Flat B C
Q : Ideal C
left✝ : Q.IsPrime
hQ : Q.LiesOver P
this : Q.LiesOver p
⊢ P.ramificationIdx A * P.ramificationIdxIn C = p.ramificationIdxIn C

Tactic:
ramificationIdxIn_eq_ramificationIdx p Q GAC,

Goal state after:
A : Type u_1
B : Type u_2
inst✝²⁰ : CommRing A
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst✝¹⁷ : Group G
inst✝¹⁶ : Finite G
inst✝¹⁵ : MulSemiringAction G B
inst✝¹⁴ : IsGaloisGroup G A B
C : Type u_4
inst✝¹³ : CommRing C
inst✝¹² : Algebra A C
inst✝¹¹ : Algebra B C
inst✝¹⁰ : Nonempty ↑(P.primesOver C)
inst✝⁹ : IsScalarTower A B C
GAC : Type u_5
inst✝⁸ : Group GAC
inst✝⁷ : Finite GAC
inst✝⁶ : MulSemiringAction GAC C
inst✝⁵ : IsGaloisGroup GAC A C
GBC : Type u_6
inst✝⁴ : Group GBC
inst✝³ : Finite GBC
inst✝² : MulSemiringAction GBC C
inst✝¹ : IsGaloisGroup GBC B C
inst✝ : Flat B C
Q : Ideal C
left✝ : Q.IsPrime
hQ : Q.LiesOver P
this : Q.LiesOver p
⊢ P.ramificationIdx A * P.ramificationIdxIn C = Q.ramificationIdx A
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: A : Type u_1
inst✝¹¹ : CommRing A
inst✝¹⁰ : IsDomain A
p : Ideal A
inst✝⁹ : p.IsPrime
B : Type u_2
inst✝⁸ : CommRing B
inst✝⁷ : IsDomain B
inst✝⁶ : Algebra A B
inst✝⁵ : Module.Finite A B
inst✝⁴ : Flat A B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G A B
this : Fintype ↑(p.primesOver B)
⊢ (p.primesOver B).ncard * (p.ramificationIdxIn B * p.inertiaDegIn B) = Nat.card G

Tactic:
rw [← smul_eq_mul, ← Set.fintypeCard_eq_ncard, ← Finset.card_univ, ← Finset.sum_const,
    ← sum_ramification_inertia_eq_card p B]

Goal state after:
A : Type u_1
inst✝¹¹ : CommRing A
inst✝¹⁰ : IsDomain A
p : Ideal A
inst✝⁹ : p.IsPrime
B : Type u_2
inst✝⁸ : CommRing B
inst✝⁷ : IsDomain B
inst✝⁶ : Algebra A B
inst✝⁵ : Module.Finite A B
inst✝⁴ : Flat A B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G A B
this : Fintype ↑(p.primesOver B)
⊢ ∑ _x, p.ramificationIdxIn B * p.inertiaDegIn B = ∑ q, (↑q).ramificationIdx A * (↑q).inertiaDeg A
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

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

Tactic:
simpa using hI

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h :
  ∀ p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊,
    Nat.Prime p →
      ∀ P ∈ (span {↑p}).primesOver (𝓞 K),
        p ^ P.inertiaDeg ℤ ≤
            ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ →
          Submodule.IsPrincipal P
x✝ : ↥(Ideal (𝓞 K))⁰
P : Ideal (𝓞 K)
HP : P ∈ (Ideal (𝓞 K))⁰
hP : (↑⟨P, HP⟩).IsPrime
hPN :
  ↑(absNorm ↑⟨P, HP⟩) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
p : ℤ
hp : under ℤ P = ℤ ∙ p
hp0 : p ≠ 0
hpprime : (under ℤ P).IsPrime → _root_.Prime p
hlies : P.LiesOver (span {p})
hspan : span {↑p.natAbs} = span {p}
hple :
  p.natAbs ^ P.inertiaDeg ℤ ≤
    ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊
hpabsprime : Nat.Prime p.natAbs
⊢ (↑⟨P, HP⟩).LiesOver (span {↑p.natAbs})

Tactic:
exact hspan ▸ hlies

Goal state after:
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
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : IsLocalization.AtPrime Rₚ p
inst✝⁶ : IsLocalRing Rₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
⊢ (Algebra.trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) =
    (equivQuotMaximalIdeal p Rₚ).symm ((Algebra.trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)) ((algebraMap S (Sₚ ⧸ pSₚ)) x))

Tactic:
rw [Algebra.trace_eq_of_equiv_equiv (equivQuotMaximalIdeal p Rₚ)
    (equivQuotientMapMaximalIdeal S p Rₚ Sₚ)]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
inst✝¹¹ : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : IsLocalization.AtPrime Rₚ p
inst✝⁶ : IsLocalRing Rₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
⊢ (equivQuotMaximalIdeal p Rₚ).symm
      ((Algebra.trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ))
        ((equivQuotientMapMaximalIdeal S p Rₚ Sₚ) ((Ideal.Quotient.mk pS) x))) =
    (equivQuotMaximalIdeal p Rₚ).symm ((Algebra.trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)) ((algebraMap S (Sₚ ⧸ pSₚ)) x))

case he
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
inst✝¹¹ : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : IsLocalization.AtPrime Rₚ p
inst✝⁶ : IsLocalRing Rₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
⊢ (algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)).comp ↑(equivQuotMaximalIdeal p Rₚ) =
    (↑(equivQuotientMapMaximalIdeal S p Rₚ Sₚ)).comp (algebraMap (R ⧸ p) (S ⧸ pS))
Module: Mathlib.RingTheory.Trace.Quotient

Goal state before:
pp: case neg
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
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
this✝³ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : IsTorsionFree Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
hp : ¬p = ⊥
⊢ IsPrincipalIdealRing Rₚ

Tactic:
have := (IsDedekindDomain.isDedekindDomainDvr R).2 p hp inferInstance
      infer_instance

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : IsDomain R
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹³ : CommRing Rₘ
inst✝¹² : CommRing Sₘ
inst✝¹¹ : Algebra R Rₘ
inst✝¹⁰ : IsTorsionFree R S
inst✝⁹ : Algebra.IsSeparable K L
M : Submonoid R
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : Algebra Rₘ Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra (FractionRing Rₘ) (FractionRing Sₘ)
inst✝ : IsScalarTower Rₘ (FractionRing Rₘ) (FractionRing Sₘ)
hM : M ≤ R⁰
⊢ Algebra.IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)

Tactic:
by
  let M' := algebraMapSubmonoid S M
  have hM' : algebraMapSubmonoid S M ≤ S⁰ := algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul
    _ hM
  let f₁ : Rₘ →+* K := map _ (T := R⁰) (RingHom.id R) hM
  let f₂ : Sₘ →+* L := map _ (T := S⁰) (RingHom.id S) hM'
  algebraize [f₁, f₂]
  have := localization_isScalarTower_of_submonoid_le Rₘ K _ _ hM
  have := localization_isScalarTower_of_submonoid_le Sₘ L _ _ hM'
  have := isFractionRing_of_isDomain_of_isLocalization M Rₘ K
  have := isFractionRing_of_isDomain_of_isLocalization M' Sₘ L
  have : IsDomain Rₘ := isDomain_of_le_nonZeroDivisors _ hM
  apply Algebra.IsSeparable.of_equiv_equiv (FractionRing.algEquiv Rₘ K).symm.toRingEquiv
    (FractionRing.algEquiv Sₘ L).symm.toRingEquiv
  apply ringHom_ext R⁰
  ext
  simp only [RingHom.coe_comp,
      RingHom.coe_coe, Function.comp_apply, ← algebraMap_apply]
  rw [algebraMap_apply R Rₘ (FractionRing R), AlgEquiv.coe_ringEquiv, AlgEquiv.commutes,
    algebraMap_apply R S L, algebraMap_apply S Sₘ L, AlgEquiv.coe_ringEquiv, AlgEquiv.commutes]
  simp only [← algebraMap_apply]
  rw [algebraMap_apply R Rₘ (FractionRing Rₘ), ← algebraMap_apply Rₘ, ← algebraMap_apply]

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
⊢ algebraMap R Tₚ = (algebraMap Sₚ Tₚ).comp (algebraMap R Sₚ)

Tactic:
by rw [IsScalarTower.algebraMap_eq R S Sₚ, ← RingHom.comp_assoc,
      ← IsScalarTower.algebraMap_eq S, ← IsScalarTower.algebraMap_eq]

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
⊢ spanNorm R I ≤ comap (algebraMap R S) I

Tactic:
rw [spanNorm, Ideal.map, Ideal.span_le, ← Submodule.span_le]

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
⊢ Submodule.span R (⇑(Algebra.intNorm R S) '' ↑I) ≤ comap (algebraMap R S) 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
⊢ ⊤ᵛ = if restrictScalars A (Algebra.trace K L).range ≤ 1 then ⊤ else ⊥

Tactic:
by
  split_ifs with h
  · rw [_root_.eq_top_iff]
    exact fun _ _ _ _ ↦ h ⟨_, rfl⟩
  · simp only [SetLike.le_def, restrictScalars_mem, LinearMap.mem_range, mem_one,
      forall_exists_index, forall_apply_eq_imp_iff, not_forall, not_exists] at h
    obtain ⟨b, hb⟩ := h
    simp_rw [eq_bot_iff, SetLike.le_def, mem_bot, mem_traceDual, mem_top, true_implies,
      traceForm_apply, RingHom.mem_range]
    contrapose! hb with hx'
    obtain ⟨c, hc, hc0⟩ := hx'
    simpa [hc0] using hc (c⁻¹ * b)

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

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

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
⊢ ∑ w, (logEmbedding K) (Additive.ofMul x) w = -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))

Tactic:
have h := sum_mult_mul_log x
  rw [Fintype.sum_eq_add_sum_subtype_ne _ w₀, add_comm, add_eq_zero_iff_eq_neg, ← neg_mul] at h
  simpa [logEmbedding_component] using 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
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✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : Ideal.map (algebraMap A B) p ∣ a ^ e
x : B
hx : x ∈ a
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x ^ e = 0

Tactic:
rw [← map_pow, Ideal.Quotient.eq_zero_iff_mem]

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✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : Ideal.map (algebraMap A B) p ∣ a ^ e
x : B
hx : x ∈ a
⊢ x ^ e ∈ Ideal.map (algebraMap A B) p
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: case inr
n m : ℕ
h : Prime n
h✝ : m > 0
⊢ (n ^ m).Deficient

Tactic:
rw [Deficient, properDivisors_prime_pow h]
    calc
      ∑ x ∈ Finset.map ⟨(n ^ ·), Nat.pow_right_injective h.two_le⟩ (range m), x
        = ∑ i ∈ range m, n ^ i := by simp
      _ = (n ^ m - 1) / (n - 1) := (Nat.geomSum_eq (Prime.two_le h) _)
      _ ≤ (n ^ m - 1) := Nat.div_le_self (n ^ m - 1) (n - 1)
      _ < n ^ m := sub_lt (pow_pos (Prime.pos h) m) (Nat.one_pos)

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
⊢ quadraticCharFun F (a * b) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1

Tactic:
quadraticCharFun_eq_pow_of_char_ne_two hF hab,

Goal state after:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
⊢ (if (a * b) ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ¬↑a = 0
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

Tactic:
· have := (ringChar_zmod_n p).symm.trans hc
      -- p = 2
      subst p
      rw [legendreSym, quadraticChar_eq_one_of_char_two hc ha]
      revert ha
      push_cast
      generalize (a : ZMod 2) = b; fin_cases b
      · tauto
      · simp

Goal state after: