mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀
⊢ ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den| = ↑(Ideal.absNorm I₀) / ↑|(Algebra.norm ℤ) ↑a|

Tactic:
rw [div_eq_div_iff]
  · replace h := congr_arg (I.den • ·) h
    have h' := congr_arg (a • ·) (den_mul_self_eq_num I)
    rw [smul_comm] at h
    rw [h, Submonoid.smul_def, Submonoid.smul_def, ← Submodule.ideal_span_singleton_smul,
      ← Submodule.ideal_span_singleton_smul, ← Submodule.map_smul'', ← Submodule.map_smul'',
      (LinearMap.map_injective ?_).eq_iff, smul_eq_mul, smul_eq_mul] at h'
    · simp_rw [← Nat.cast_natAbs, ← Nat.cast_mul, ← Ideal.absNorm_span_singleton]
      rw [← map_mul, ← map_mul, mul_comm, ← h', mul_comm]
    · exact LinearMap.ker_eq_bot.mpr (IsFractionRing.injective R K)
  all_goals simp [Algebra.norm_eq_zero_iff]

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

Goal state before:
pp: case refine_3
K : Type u_1
inst✝ : Field K
w : { w // w.IsReal }
⊢ ∃ a, (fun φ ↦ ⟨mk ↑φ, ⋯⟩) a = w

Tactic:
· exact ⟨⟨embedding w, isReal_iff.mp w.prop⟩, by simp⟩

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

Goal state before:
pp: 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
d : ℕ
a b c : k[X]
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
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
heq : C u * (expand k ch) ca ^ p + C v * (expand k ch) cb ^ q + C w * (expand k ch) cc ^ r = 0
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
⊢ C u * ca ^ p + C v * cb ^ q + C w * cc ^ r = 0

Tactic:
← expand_C ch u,

Goal state after:
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
d : ℕ
a b c : k[X]
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
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
heq : (expand k ch) (C u) * (expand k ch) ca ^ p + C v * (expand k ch) cb ^ q + C w * (expand k ch) cc ^ r = 0
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
⊢ C u * ca ^ p + C v * cb ^ q + C w * cc ^ r = 0
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:
by
  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.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ((B * S⁻¹) ^ (↑w₁.mult)⁻¹) ^ w₁.mult *
      ∏ x ∈ Finset.univ.erase w₁, Function.update f w₁ ((B * S⁻¹) ^ (↑w₁.mult)⁻¹) x ^ x.mult =
    B

Tactic:
Finset.prod_congr rfl fun w hw => by rw [Function.update_of_ne (Finset.ne_of_mem_erase hw)],

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ((B * S⁻¹) ^ (↑w₁.mult)⁻¹) ^ w₁.mult * ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult = B
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hn' : 0 < n
hone : 1 = C 1
hneg_one : -1 = C (-1)
heq : C 1 * a ^ n + C 1 * b ^ n + C (-1) * c ^ n = 0
eq_lhs : n * n + n * n + n * n = 3 * n * n
⊢ n * n + n * n + n * n ≤ n * n * n

Tactic:
rw [eq_lhs, mul_assoc, mul_assoc]

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hn' : 0 < n
hone : 1 = C 1
hneg_one : -1 = C (-1)
heq : C 1 * a ^ n + C 1 * b ^ n + C (-1) * c ^ n = 0
eq_lhs : n * n + n * n + n * n = 3 * n * n
⊢ 3 * (n * n) ≤ n * (n * n)
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)
x✝ : i ∈ Finset.univ
⊢ (canonicalEmbedding K) ((integralBasis K) i) ∈ Set.range ⇑(latticeBasis K)

Tactic:
rw [← latticeBasis_apply]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i : Free.ChooseBasisIndex ℤ (𝓞 K)
x✝ : i ∈ Finset.univ
⊢ (latticeBasis K) i ∈ Set.range ⇑(latticeBasis K)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
⊢ IsUnramified k w ↔ w.IsReal ∨ (w.comap (algebraMap k K)).IsComplex

Tactic:
← not_iff_not,

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
⊢ ¬IsUnramified k w ↔ ¬(w.IsReal ∨ (w.comap (algebraMap k K)).IsComplex)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Gal(K/k)
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
⊢ IsUnramified k (mk φ) ↔ ComplexEmbedding.IsReal φ

Tactic:
← not_iff_not,

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Gal(K/k)
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
⊢ ¬IsUnramified k (mk φ) ↔ ¬ComplexEmbedding.IsReal φ
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
φ : K →+* ℂ
H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : ¬ComplexEmbedding.IsReal φ ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
⊢ False

Tactic:
← ComplexEmbedding.isConj_one_iff (k := k)

Goal state after:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
φ : K →+* ℂ
H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : ¬ComplexEmbedding.IsConj φ 1 ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
⊢ False
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∏ _k, (2⁻¹ • !![1, 1; -I, I]).det = ∏ _k, 2⁻¹ * I

Tactic:
by
      refine prod_congr (Eq.refl _) (fun _ _ => ?_)
      simp [field]; ring

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

Goal state before:
pp: k : Type u_1
inst✝⁶ : Field k
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : NumberField k
inst✝² : NumberField K
inst✝¹ : IsGalois k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
⊢ card (InfinitePlace K) = card (InfinitePlace k) * finrank k K

Tactic:
rw [InfinitePlace.card_eq_card_isUnramifiedIn (k := k) (K := K), Finset.filter_true_of_mem,
    Finset.card_univ, Finset.card_eq_zero.mpr, zero_mul, add_zero]
  · exact Finset.compl_univ
  simp only [Finset.mem_univ, forall_true_left]
  exact InfinitePlace.isUnramifiedIn K

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)
x✝ : i ∈ univ
⊢ (mixedEmbedding K) ((integralBasis K) i) ∈ Set.range ⇑(latticeBasis K)

Tactic:
rw [← latticeBasis_apply]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i : ChooseBasisIndex ℤ (𝓞 K)
x✝ : i ∈ univ
⊢ (latticeBasis K) i ∈ Set.range ⇑(latticeBasis K)
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
⊢ 2 * (ramifiedPlacesOver L v).ncard = (mixedEmbeddingsOver L v.embedding).ncard

Tactic:
rw [← (bijOn_sumElim_conjugate L v).ncard_eq, two_mul, Set.ncard_sumEquiv_symm_apply]

Goal state after:
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 : 0 ∉ M
⊢ (algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)

Tactic:
replace hM : M ≤ A⁰ := fun x hx ↦ mem_nonZeroDivisors_iff_ne_zero.mpr (fun e ↦ hM (e ▸ hx))

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⁰
⊢ (algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case refine_1.inl
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
s : Set { w // w.IsReal }
x : mixedSpace K
hx : x ∈ A
right✝ : x ∈ {x | ∀ (w : { w // w.IsReal }), 0 < x.1 w}
⊢ (fun w ↦ ‖((negAt s) x).1 w‖, ((negAt s) x).2) ∈ A

Tactic:
negAt_apply_norm_isReal,

Goal state after:
case refine_1.inl
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
s : Set { w // w.IsReal }
x : mixedSpace K
hx : x ∈ A
right✝ : x ∈ {x | ∀ (w : { w // w.IsReal }), 0 < x.1 w}
⊢ (fun w ↦ ‖x.1 w‖, ((negAt s) x).2) ∈ A
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F // p F }
T : Set A
hT : T.Finite
h : ∀ F ∈ S, ∃ x ∈ T, ↑F = ℚ⟮x⟯
⊢ S.Finite

Tactic:
← Set.finite_coe_iff

Goal state after:
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F // p F }
T : Set A
hT : Finite ↑T
h : ∀ F ∈ S, ∃ x ∈ T, ↑F = ℚ⟮x⟯
⊢ S.Finite
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 : 0 ∉ M
⊢ (algebraMap A Aₘ) ((intNorm A B) x) = (intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)

Tactic:
replace hM : M ≤ A⁰ := fun x hx ↦ mem_nonZeroDivisors_iff_ne_zero.mpr (fun e ↦ hM (e ▸ hx))

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⁰
⊢ (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
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
h : ∃ P, P.IsPrime ∧ P.LiesOver p
left✝ : h.choose.IsPrime
right✝ : h.choose.LiesOver p
⊢ h.choose.inertiaDeg A = P.inertiaDeg A

Tactic:
exact inertiaDeg_eq_of_isGaloisGroup p h.choose P G

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
Q : Ideal C
left✝ : Q.IsPrime
right✝ : Q.LiesOver P
this : Q.LiesOver p
⊢ P.inertiaDeg A * Q.inertiaDeg B = Q.inertiaDeg A

Tactic:
← inertiaDeg_tower P Q

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
Q : Ideal C
left✝ : Q.IsPrime
right✝ : Q.LiesOver P
this : Q.LiesOver p
⊢ Q.inertiaDeg A = Q.inertiaDeg A
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsDedekindDomain R
inst✝ : IsGalois K L
p : Ideal R
P₂ : Ideal S
hP₂ : P₂ ∈ p.primesOver S
this✝⁸ : IsDomain S
this✝⁷ : IsDedekindDomain S
this✝⁶ : Module.Finite R S
this✝⁵ : P₂.IsPrime
this✝⁴ : P₂.LiesOver p
this✝³ : IsFractionRing S L
this✝² : MulSemiringAction Gal(L/K) S := IsIntegralClosure.MulSemiringAction R K L S
this✝¹ : IsGaloisGroup Gal(L/K) R S
σ : Gal(L/K)
hP₁ : σ • P₂ ∈ p.primesOver S
this✝ : (σ • P₂).IsPrime
this : (σ • P₂).LiesOver p
⊢ ∃ σ_1, comap ((galRestrict R K L S) σ_1) (σ • P₂) = P₂

Tactic:
exact ⟨σ, comap_map_of_bijective _ ((galRestrict R K L S σ).bijective)⟩

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
B : ℕ
h✝ : Infinite R
s : Finset R
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : Nat.card (R ⧸ I) ≤ B ∧ I ∉ {⊥}
hs : (Finset.image (⇑(Ideal.Quotient.mk I)) s).card < s.card
x : R
hx : x ∈ s
y : R
hy : y ∈ s
hxy : x ≠ y
h : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
⊢ x - y ∉ {0}

Tactic:
Finset.notMem_singleton,

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
B : ℕ
h✝ : Infinite R
s : Finset R
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : Nat.card (R ⧸ I) ≤ B ∧ I ∉ {⊥}
hs : (Finset.image (⇑(Ideal.Quotient.mk I)) s).card < s.card
x : R
hx : x ∈ s
y : R
hy : y ∈ s
hxy : x ≠ y
h : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
⊢ x - y ≠ 0
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: case a.hv
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
⊢ span (R ⧸ p) (?a.hv.g✝ '' Set.range ?a.hv.f✝) = ⊤

pp: case a.hv.g
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 := ⋯
⊢ ?m.104 → S ⧸ pS

pp: case a.hv.f
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.ChooseBasisIndex R S → ?m.104

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 := ⋯
⊢ Type ?u.64

Tactic:
apply (quotient_span_eq_top_iff_span_eq_top _).mpr b.span_eq

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 ℤ 𝒪
L : Type u_3
𝒪' : Type u_4
inst✝¹⁵ : Field L
inst✝¹⁴ : NumberField L
inst✝¹³ : CommRing 𝒪'
inst✝¹² : Algebra 𝒪' L
inst✝¹¹ : IsFractionRing 𝒪' L
inst✝¹⁰ : IsDedekindDomain 𝒪'
inst✝⁹ : CharZero 𝒪'
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra 𝒪 𝒪'
inst✝⁶ : Algebra 𝒪 L
inst✝⁵ : IsScalarTower 𝒪 K L
inst✝⁴ : IsScalarTower 𝒪 𝒪' L
inst✝³ : IsTorsionFree 𝒪 𝒪'
inst✝² : Free ℤ 𝒪'
inst✝¹ : Module.Finite ℤ 𝒪'
inst✝ : Module.Finite 𝒪 𝒪'
this :
  (discr L).natAbs =
    Ideal.absNorm (differentIdeal 𝒪 𝒪') * Ideal.absNorm (Ideal.map (algebraMap 𝒪 𝒪') (differentIdeal ℤ 𝒪))
⊢ (discr L).natAbs = Ideal.absNorm (differentIdeal 𝒪 𝒪') * (discr K).natAbs ^ finrank K L

Tactic:
Ideal.absNorm_algebraMap,

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 ℤ 𝒪
L : Type u_3
𝒪' : Type u_4
inst✝¹⁵ : Field L
inst✝¹⁴ : NumberField L
inst✝¹³ : CommRing 𝒪'
inst✝¹² : Algebra 𝒪' L
inst✝¹¹ : IsFractionRing 𝒪' L
inst✝¹⁰ : IsDedekindDomain 𝒪'
inst✝⁹ : CharZero 𝒪'
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra 𝒪 𝒪'
inst✝⁶ : Algebra 𝒪 L
inst✝⁵ : IsScalarTower 𝒪 K L
inst✝⁴ : IsScalarTower 𝒪 𝒪' L
inst✝³ : IsTorsionFree 𝒪 𝒪'
inst✝² : Free ℤ 𝒪'
inst✝¹ : Module.Finite ℤ 𝒪'
inst✝ : Module.Finite 𝒪 𝒪'
this : (discr L).natAbs = Ideal.absNorm (differentIdeal 𝒪 𝒪') * Ideal.absNorm (differentIdeal ℤ 𝒪) ^ finrank 𝒪 𝒪'
⊢ (discr L).natAbs = Ideal.absNorm (differentIdeal 𝒪 𝒪') * (discr K).natAbs ^ finrank K L
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: L : Type u_3
inst✝¹ : Field L
inst✝ : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
⊢ (discr L).natAbs = (discr ↥K₁).natAbs ^ finrank ℚ ↥K₂ * (discr ↥K₂).natAbs ^ finrank ℚ ↥K₁

Tactic:
let _ : Algebra (FractionRing (𝓞 K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra _ _

Goal state after:
L : Type u_3
inst✝¹ : Field L
inst✝ : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x✝ : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
⊢ (discr L).natAbs = (discr ↥K₁).natAbs ^ finrank ℚ ↥K₂ * (discr ↥K₂).natAbs ^ finrank ℚ ↥K₁
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: L : Type u_3
inst✝¹ : Field L
inst✝ : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x✝ : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main :
  (discr L).natAbs =
    Ideal.absNorm (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁))) *
      (discr ↥K₂).natAbs ^ finrank (↥K₂) L
⊢ (discr L).natAbs = (discr ↥K₁).natAbs ^ finrank ℚ ↥K₂ * (discr ↥K₂).natAbs ^ finrank ℚ ↥K₁

Tactic:
Ideal.absNorm_algebraMap,

Goal state after:
L : Type u_3
inst✝¹ : Field L
inst✝ : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x✝ : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main :
  (discr L).natAbs =
    Ideal.absNorm (differentIdeal ℤ (𝓞 ↥K₁)) ^ finrank (𝓞 ↥K₁) (𝓞 L) * (discr ↥K₂).natAbs ^ finrank (↥K₂) L
⊢ (discr L).natAbs = (discr ↥K₁).natAbs ^ finrank ℚ ↥K₂ * (discr ↥K₂).natAbs ^ finrank ℚ ↥K₁