mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
n : ℕ
⊢ hurwitzZetaEven a (-2 * (↑n + 1)) = 0

Tactic:
by
  have : (-2 : ℂ) * (n + 1) ≠ 0 :=
    mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (Nat.cast_add_one_ne_zero n)
  rw [hurwitzZetaEven, Function.update_of_ne this, Gammaℝ_eq_zero_iff.mpr ⟨n + 1, by simp⟩,
    div_zero]

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

Goal state before:
pp: n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
⊢ False

Tactic:
← Rat.num_ne_zero

Goal state after:
n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a.num ≠ 0
hb : b.num ≠ 0
hc : c.num ≠ 0
habc : a ^ n + b ^ n = c ^ n
⊢ False
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ hurwitzZetaEven a (1 - s) = 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.cos (↑π * s / 2) * cosZeta a s

Tactic:
by
  have : hurwitzZetaEven a (1 - s) = completedHurwitzZetaEven a (1 - s) * (Gammaℝ (1 - s))⁻¹ := by
    rw [hurwitzZetaEven_def_of_ne_or_ne, div_eq_mul_inv]
    simpa [sub_eq_zero, eq_comm (a := s)] using hs'
  rw [this, completedHurwitzZetaEven_one_sub, inv_Gammaℝ_one_sub hs, cosZeta,
    Function.update_of_ne (by simpa using hs 0), ← Gammaℂ]
  generalize Gammaℂ s * cos (π * s / 2) = A -- speeds up ring_nf call
  ring_nf

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ s ≠ 0

Tactic:
simpa using hs 1

Goal state after:
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Fermat42 a b c
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

Tactic:
by
  obtain ⟨a0, b0, c0, hf, hc⟩ := exists_odd_minimal h
  rcases lt_trichotomy 0 c0 with (h1 | h1 | h1)
  · use a0, b0, c0
  · exfalso
    exact ne_zero hf.1 h1.symm
  · use a0, b0, -c0, neg_of_minimal hf, hc
    exact neg_pos.mpr h1

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case left
K : Type u_1
inst✝ : Field K
hk : ∀ (x : K), 1 + x ^ 2 ≠ 0
x✝ : { p // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : x ^ 2 + y ^ 2 = 1
h2 : y + 1 ≠ 0
h3 : (y + 1) ^ 2 + x ^ 2 = 2 * (y + 1)
h4 : 2 ≠ 0
⊢ 2 * (x / (y + 1)) / (1 + (x / (y + 1)) ^ 2) = x

Tactic:
simp [field, h3]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hda : derivative a = 0
hdb : derivative b = 0
⊢ a * derivative b - derivative a * b = 0

Tactic:
rw [hda, hdb]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hda : derivative a = 0
hdb : derivative b = 0
⊢ a * 0 - 0 * b = 0
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hda : derivative a = 0
hdb : derivative b = 0
⊢ a * 0 - 0 * b = 0

Tactic:
simp only [mul_zero, zero_mul, sub_self]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: case neg
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a : k[X]
ha : ¬a = 0
⊢ (radical a).natDegree ≤ a.natDegree

Tactic:
· exact natDegree_le_of_dvd radical_dvd_self ha

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
x✝ : a = 0 ∨ IsUnit a
⊢ a = 0 → radical a = 1

Tactic:
simp +contextual

Goal state after:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case inr.hi
k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
chn0 : ringChar k ≠ 0
d : ℕ
ih_d :
  ∀ m ≤ d,
    ∀ {a b c : k[X]},
      C u * a ^ p + C v * b ^ q + C w * c ^ r = 0 → a ≠ 0 → b ≠ 0 → c ≠ 0 → IsCoprime a b → a.natDegree = m → m = 0
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
⊢ d + 1 = 0

Tactic:
obtain ⟨ca, ca_nz, eq_a, eq_deg_a⟩ := find_contract ha ad chn0

Goal state after:
case inr.hi
k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
chn0 : ringChar k ≠ 0
d : ℕ
ih_d :
  ∀ m ≤ d,
    ∀ {a b c : k[X]},
      C u * a ^ p + C v * b ^ q + C w * c ^ r = 0 → a ≠ 0 → b ≠ 0 → c ≠ 0 → IsCoprime a b → a.natDegree = m → m = 0
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
ca : k[X]
ca_nz : ca ≠ 0
eq_a : a = (expand k (ringChar k)) ca
eq_deg_a : a.natDegree = ca.natDegree * ringChar k
⊢ d + 1 = 0
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case mpr.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h : ComplexEmbedding.conjugate φ = ψ
⊢ mk φ = mk ψ

Tactic:
← mk_conjugate_eq

Goal state after:
case mpr.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h : ComplexEmbedding.conjugate φ = ψ
⊢ mk (ComplexEmbedding.conjugate φ) = mk ψ
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ : InfinitePlace K
x✝ : x✝¹ ∈ Finset.univ
⊢ x✝¹.mult = #{i | mk i = x✝¹}

Tactic:
card_filter_mk_eq

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ : InfinitePlace K
x✝ : x✝¹ ∈ Finset.univ
⊢ x✝¹.mult = x✝¹.mult
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
this : ∀ (w : InfinitePlace K), ∀ φ ∈ {φ | mk φ = w}, ‖φ x‖ = w x
⊢ ∏ w, w x ^ w.mult = ∏ x_1, x_1 x ^ #{i | mk i = x_1}

Tactic:
card_filter_mk_eq

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

Goal state before:
pp: case neg.«2»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf ↑↑x = 2
hc : 2 ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1

Tactic:
CharP.orderOf_eq_two_iff 0 (by decide)

Goal state after:
case neg.«2»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : ↑↑x = -1
hc : 2 ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : finrank ℚ K = 1
⊢ nrRealPlaces K = 1

Tactic:
have := card_add_two_mul_card_eq_rank K
  rwa [nrComplexPlaces_eq_zero_of_finrank_eq_one h, h, mul_zero, add_zero] at this

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℚ K = finrank ℤ (𝓞 K)

Tactic:
RingOfIntegers.rank

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℚ K = finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

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

Tactic:
simp_rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, this, Basis.repr_self]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
⊢ x φ = 0 φ

Tactic:
rw [Pi.zero_apply]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
⊢ x φ = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ‖x‖₊ = univ.sup fun w ↦ NNReal.mk ((normAtPlace w) x) ⋯

Tactic:
by
  have :
      (univ : Finset (InfinitePlace K)) =
      (univ.image (fun w : {w : InfinitePlace K // IsReal w} ↦ w.1)) ∪
      (univ.image (fun w : {w : InfinitePlace K // IsComplex w} ↦ w.1)) := by
    ext; simp [isReal_or_isComplex]
  rw [this, sup_union, univ.sup_image, univ.sup_image,
    Prod.nnnorm_def, Pi.nnnorm_def, Pi.nnnorm_def]
  congr
  · ext w
    simp [normAtPlace_apply_of_isReal w.prop]
  · ext w
    simp [normAtPlace_apply_of_isComplex w.prop]

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

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : B ≤ 0
⊢ volume (convexBodySum K B) = ↑(convexBodySumFactor K) * ENNReal.ofReal B ^ finrank ℚ K

Tactic:
rw [convexBodySum_volume_eq_zero_of_le_zero K hB, ofReal_eq_zero.mpr hB, zero_pow, mul_zero]
    exact finrank_pos.ne'

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

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
hw : ¬(InfinitePlace.mk φ).embedding = φ
⊢ ∃ a,
    (fun c ↦
          Sum.casesOn (motive := fun t ↦ c = t → K →+* ℂ) c (fun w h ↦ (↑w).embedding)
            (fun wj h ↦
              Prod.casesOn wj fun w j ↦ if j = 0 then (↑w).embedding else ComplexEmbedding.conjugate (↑w).embedding)
            ⋯)
        a =
      φ

Tactic:
exact ⟨Sum.inr ⟨InfinitePlace.mkComplex ⟨φ, hφ⟩, 1⟩,
          by simp [(embedding_mk_eq φ).resolve_left hw]⟩

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

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : ψ ∈ unmixedEmbeddingsOver L v.embedding
hψ : (mk ψ).embedding = conjugate ψ
x✝ : ComplexEmbedding.LiesOver (conjugate ψ) v.embedding
over✝ : (conjugate ψ).comp (algebraMap K L) = v.embedding
⊢ ComplexEmbedding.IsReal (ψ.comp (algebraMap K L))

Tactic:
by have := h.1.over; aesop

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

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

Tactic:
simp_rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, this, Basis.repr_self]

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

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

Tactic:
le_div_iff₀' (Nat.cast_pos.mpr finrank_pos)

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

Goal state before:
pp: case neg
A : Type u_1
B : Type u_6
inst✝²⁴ : CommRing A
inst✝²³ : CommRing B
inst✝²² : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst✝²¹ : CommRing Aₘ
inst✝²⁰ : CommRing Bₘ
inst✝¹⁹ : Algebra Aₘ Bₘ
inst✝¹⁸ : Algebra A Aₘ
inst✝¹⁷ : Algebra B Bₘ
inst✝¹⁶ : Algebra A Bₘ
inst✝¹⁵ : IsScalarTower A Aₘ Bₘ
inst✝¹⁴ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹³ : IsLocalization M Aₘ
inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDomain B
inst✝⁸ : IsIntegrallyClosed B
inst✝⁷ : Module.Finite A B
inst✝⁶ : IsTorsionFree A B
inst✝⁵ : IsDomain Aₘ
inst✝⁴ : IsIntegrallyClosed Aₘ
inst✝³ : IsDomain Bₘ
inst✝² : IsIntegrallyClosed Bₘ
inst✝¹ : IsTorsionFree Aₘ Bₘ
inst✝ : Module.Finite Aₘ Bₘ
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
this✝⁶ : IsIntegralClosure B A L
this✝⁵ : Algebra.IsAlgebraic (FractionRing A) (FractionRing B)
this✝⁴ : IsLocalization (algebraMapSubmonoid B A⁰) L
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝³ : Algebra Aₘ K := f.toAlgebra
this✝² : IsScalarTower A Aₘ K
this✝¹ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K
g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯
this✝ : Algebra Bₘ L := g.toAlgebra
this : IsScalarTower B Bₘ L
⊢ (algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)

Tactic:
let := ((algebraMap K L).comp f).toAlgebra

Goal state after:
case neg
A : Type u_1
B : Type u_6
inst✝²⁴ : CommRing A
inst✝²³ : CommRing B
inst✝²² : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst✝²¹ : CommRing Aₘ
inst✝²⁰ : CommRing Bₘ
inst✝¹⁹ : Algebra Aₘ Bₘ
inst✝¹⁸ : Algebra A Aₘ
inst✝¹⁷ : Algebra B Bₘ
inst✝¹⁶ : Algebra A Bₘ
inst✝¹⁵ : IsScalarTower A Aₘ Bₘ
inst✝¹⁴ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹³ : IsLocalization M Aₘ
inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDomain B
inst✝⁸ : IsIntegrallyClosed B
inst✝⁷ : Module.Finite A B
inst✝⁶ : IsTorsionFree A B
inst✝⁵ : IsDomain Aₘ
inst✝⁴ : IsIntegrallyClosed Aₘ
inst✝³ : IsDomain Bₘ
inst✝² : IsIntegrallyClosed Bₘ
inst✝¹ : IsTorsionFree Aₘ Bₘ
inst✝ : Module.Finite Aₘ Bₘ
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
this✝⁷ : IsIntegralClosure B A L
this✝⁶ : Algebra.IsAlgebraic (FractionRing A) (FractionRing B)
this✝⁵ : IsLocalization (algebraMapSubmonoid B A⁰) L
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝⁴ : Algebra Aₘ K := f.toAlgebra
this✝³ : IsScalarTower A Aₘ K
this✝² : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K
g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯
this✝¹ : Algebra Bₘ L := g.toAlgebra
this✝ : IsScalarTower B Bₘ L
this : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra
⊢ (algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: case neg
A : Type u_1
B : Type u_6
inst✝²⁵ : CommRing A
inst✝²⁴ : CommRing B
inst✝²³ : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst✝²² : CommRing Aₘ
inst✝²¹ : CommRing Bₘ
inst✝²⁰ : Algebra Aₘ Bₘ
inst✝¹⁹ : Algebra A Aₘ
inst✝¹⁸ : Algebra B Bₘ
inst✝¹⁷ : Algebra A Bₘ
inst✝¹⁶ : IsScalarTower A Aₘ Bₘ
inst✝¹⁵ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹⁴ : IsLocalization M Aₘ
inst✝¹³ : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝¹² : IsIntegrallyClosed A
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsDomain B
inst✝⁹ : IsIntegrallyClosed B
inst✝⁸ : Algebra.IsIntegral A B
inst✝⁷ : IsTorsionFree A B
inst✝⁶ : IsDomain Aₘ
inst✝⁵ : IsIntegrallyClosed Aₘ
inst✝⁴ : IsDomain Bₘ
inst✝³ : IsIntegrallyClosed Bₘ
inst✝² : IsTorsionFree Aₘ Bₘ
inst✝¹ : Algebra.IsIntegral Aₘ Bₘ
inst✝ : FiniteDimensional (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝³ : Algebra Aₘ K := f.toAlgebra
this✝² : IsScalarTower A Aₘ K
this✝¹ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K
g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯
this✝ : Algebra Bₘ L := g.toAlgebra
this : IsScalarTower B Bₘ L
⊢ (algebraMap A Aₘ) ((intNorm A B) x) = (intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)

Tactic:
let := ((algebraMap K L).comp f).toAlgebra

Goal state after:
case neg
A : Type u_1
B : Type u_6
inst✝²⁵ : CommRing A
inst✝²⁴ : CommRing B
inst✝²³ : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst✝²² : CommRing Aₘ
inst✝²¹ : CommRing Bₘ
inst✝²⁰ : Algebra Aₘ Bₘ
inst✝¹⁹ : Algebra A Aₘ
inst✝¹⁸ : Algebra B Bₘ
inst✝¹⁷ : Algebra A Bₘ
inst✝¹⁶ : IsScalarTower A Aₘ Bₘ
inst✝¹⁵ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹⁴ : IsLocalization M Aₘ
inst✝¹³ : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝¹² : IsIntegrallyClosed A
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsDomain B
inst✝⁹ : IsIntegrallyClosed B
inst✝⁸ : Algebra.IsIntegral A B
inst✝⁷ : IsTorsionFree A B
inst✝⁶ : IsDomain Aₘ
inst✝⁵ : IsIntegrallyClosed Aₘ
inst✝⁴ : IsDomain Bₘ
inst✝³ : IsIntegrallyClosed Bₘ
inst✝² : IsTorsionFree Aₘ Bₘ
inst✝¹ : Algebra.IsIntegral Aₘ Bₘ
inst✝ : FiniteDimensional (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝⁴ : Algebra Aₘ K := f.toAlgebra
this✝³ : IsScalarTower A Aₘ K
this✝² : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K
g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯
this✝¹ : Algebra Bₘ L := g.toAlgebra
this✝ : IsScalarTower B Bₘ L
this : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra
⊢ (algebraMap A Aₘ) ((intNorm A B) x) = (intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)
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
⊢ (p.primesOver B).ncard * (p.ramificationIdxIn B * p.inertiaDegIn B) = Nat.card G

Tactic:
by
  have : Fintype (primesOver p B) := (QuasiFinite.finite_primesOver p).fintype
  rw [← smul_eq_mul, ← Set.fintypeCard_eq_ncard, ← Finset.card_univ, ← Finset.sum_const,
    ← sum_ramification_inertia_eq_card p B]
  apply Finset.sum_congr rfl
  intro P hp
  rw [ramificationIdxIn_eq_ramificationIdx p P G, inertiaDegIn_eq_inertiaDeg p P G]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
a : 𝓞 K
ha : a ∈ ↑↑J
h_nz : (Algebra.linearMap (𝓞 K) K) a ≠ 0
h_nm :
  ↑|(Algebra.norm ℚ) ((Algebra.linearMap (𝓞 K) K) a)| ≤
    ↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K)! /
        ↑(finrank ℚ K) ^ finrank ℚ K *
      √|↑(discr K)|
I₀ : Ideal (𝓞 K)
hI : span {a} = ↑J * I₀
this✝ : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ := ⟨I₀, ⋯⟩
this : ClassGroup.mk0 I = (ClassGroup.mk0 J)⁻¹
⊢ (ClassGroup.mk0 J)⁻¹ = C

Tactic:
hJ,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
a : 𝓞 K
ha : a ∈ ↑↑J
h_nz : (Algebra.linearMap (𝓞 K) K) a ≠ 0
h_nm :
  ↑|(Algebra.norm ℚ) ((Algebra.linearMap (𝓞 K) K) a)| ≤
    ↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K)! /
        ↑(finrank ℚ K) ^ finrank ℚ K *
      √|↑(discr K)|
I₀ : Ideal (𝓞 K)
hI : span {a} = ↑J * I₀
this✝ : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ := ⟨I₀, ⋯⟩
this : ClassGroup.mk0 I = (ClassGroup.mk0 J)⁻¹
⊢ C⁻¹⁻¹ = C
Module: Mathlib.NumberTheory.RamificationInertia.Unramified

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain R
inst✝³ : IsDomain S
inst✝² : FaithfulSMul R S
inst✝¹ : CharZero R
inst✝ : Algebra.IsIntegral R S
⊢ IsUnramifiedIn S ⊥

Tactic:
intro P _ hP
  simpa [Ideal.eq_bot_of_liesOver_bot R P] using isUnramifiedAt_bot

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

Goal state before:
pp: A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
J : Ideal A
hI : ↑J ≤ 1
⊢ extended L hf ↑J ≤ 1

Tactic:
intro x hx

Goal state after:
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
J : Ideal A
hI : ↑J ≤ 1
x : L
hx : x ∈ extended L hf ↑J
⊢ x ∈ 1
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: 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
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
| finrank R S

Tactic:
finrank_eq_card_chooseBasisIndex

Goal state after:
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
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
| Fintype.card (Free.ChooseBasisIndex R S)
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: 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
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)) (R ⧸ p) (S ⧸ pS) := Free.chooseBasis (R ⧸ p) (S ⧸ pS)
b' : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS) → S
hb' : ∀ (i : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)), (Ideal.Quotient.mk pS) (b' i) = b i
| finrank (R ⧸ p) (S ⧸ pS)

Tactic:
finrank_eq_card_chooseBasisIndex

Goal state after:
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
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)) (R ⧸ p) (S ⧸ pS) := Free.chooseBasis (R ⧸ p) (S ⧸ pS)
b' : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS) → S
hb' : ∀ (i : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)), (Ideal.Quotient.mk pS) (b' i) = b i
| Fintype.card (Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS))