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
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
i✝ j✝ : ι
⊢ (algebraMap ℤ ℚ).mapMatrix (b.toMatrix (Subtype.val ∘ ⇑(bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))))) i✝ j✝ =
    b₀.toMatrix ((algebraMap R K) ↑I.den • Subtype.val ∘ ⇑bI) i✝ j✝

Tactic:
RingHom.mapMatrix_apply,

Goal state after:
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
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
i✝ j✝ : ι
⊢ (b.toMatrix (Subtype.val ∘ ⇑(bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))))).map (⇑(algebraMap ℤ ℚ)) i✝ j✝ =
    b₀.toMatrix ((algebraMap R K) ↑I.den • Subtype.val ∘ ⇑bI) i✝ j✝
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inl.right.inl.left
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos✝ : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_pos : z = m ^ 2 + n ^ 2
⊢ (-m).gcd (-n) = 1

Tactic:
delta Int.gcd
          rw [Int.natAbs_neg, Int.natAbs_neg]
          exact ht3

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

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
⊢ FermatLastTheoremWith' k[X] n

Tactic:
by
  classical
  rw [FermatLastTheoremWith']
  intro a b c ha hb hc heq
  obtain ⟨a', eq_a⟩ := gcd_dvd_left a b
  obtain ⟨b', eq_b⟩ := gcd_dvd_right a b
  set d := gcd a b
  have hd : d ≠ 0 := gcd_ne_zero_of_left ha
  rw [eq_a, eq_b, mul_pow, mul_pow, ← mul_add] at heq
  obtain ⟨c', eq_c⟩ : ∃ c', c = d * c' :=
    (IsIntegrallyClosed.pow_dvd_pow_iff (by lia)).mp ⟨_, heq.symm⟩
  rw [eq_a, mul_ne_zero_iff] at ha
  rw [eq_b, mul_ne_zero_iff] at hb
  rw [eq_c, mul_ne_zero_iff] at hc
  rw [mul_comm] at eq_a eq_b eq_c
  refine ⟨d, a', b', c', ⟨eq_a, eq_b, eq_c⟩, ?_⟩
  rw [eq_c, mul_pow, mul_comm, mul_left_inj' (pow_ne_zero n hd)] at heq
  suffices goal : a'.natDegree = 0 ∧ b'.natDegree = 0 ∧ c'.natDegree = 0 by
    simp only [natDegree_eq_zero] at goal
    obtain ⟨⟨ca', ha'⟩, ⟨cb', hb'⟩, ⟨cc', hc'⟩⟩ := goal
    rw [← ha', ← hb', ← hc']
    rw [← ha', C_ne_zero] at ha
    rw [← hb', C_ne_zero] at hb
    rw [← hc', C_ne_zero] at hc
    exact ⟨ha.right.isUnit_C, hb.right.isUnit_C, hc.right.isUnit_C⟩
  apply flt hn chn ha.right hb.right hc.right _ heq
  convert! isCoprime_div_gcd_div_gcd _
  · exact EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_a.symm
  · exact EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_b.symm
  · rw [eq_b]
    exact mul_ne_zero hb.right hb.left

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
a✝ b✝ : K
hx : a✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
hy : b✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
x✝ : K →+* ℂ
⊢ x✝ a✝ + star (x✝ b✝) = x✝ a✝ + x✝ b✝

Tactic:
hy

Goal state after:
F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
a✝ b✝ : K
hx : a✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
hy : b✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
x✝ : K →+* ℂ
⊢ x✝ a✝ + x✝ b✝ = x✝ a✝ + x✝ b✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case refine_3
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝³ x✝² : (K →+* ℂ) → ℂ
x✝¹ : x✝³ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝ : x✝² ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝³ φ) = x✝³ (ComplexEmbedding.conjugate φ)
hy : (starRingEnd ℂ) (x✝² φ) = x✝² (ComplexEmbedding.conjugate φ)
⊢ x✝³ (ComplexEmbedding.conjugate φ) + (starRingEnd ℂ) (x✝² φ) =
    x✝³ (ComplexEmbedding.conjugate φ) + x✝² (ComplexEmbedding.conjugate φ)

Tactic:
hy

Goal state after:
case refine_3
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝³ x✝² : (K →+* ℂ) → ℂ
x✝¹ : x✝³ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝ : x✝² ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝³ φ) = x✝³ (ComplexEmbedding.conjugate φ)
hy : (starRingEnd ℂ) (x✝² φ) = x✝² (ComplexEmbedding.conjugate φ)
⊢ x✝³ (ComplexEmbedding.conjugate φ) + x✝² (ComplexEmbedding.conjugate φ) =
    x✝³ (ComplexEmbedding.conjugate φ) + x✝² (ComplexEmbedding.conjugate φ)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ∏ i, volume (if i = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑i) ^ 2} else ball 0 ↑(f ↑i)) =
    (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi) * (4 * ↑(f ↑w₀) ^ 2))

Tactic:
rw [← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)]

Goal state after:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀,
          volume (if x = w₀ then {x_1 | |x_1.re| < 1 ∧ |x_1.im| < ↑(f ↑x) ^ 2} else ball 0 ↑(f ↑x))) *
        volume (if w₀ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑w₀) ^ 2} else ball 0 ↑(f ↑w₀))) =
    (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi) * (4 * ↑(f ↑w₀) ^ 2))
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ((starRingEnd ℂ).mapMatrix (basisMatrix K)).det = (basisMatrix K).det ↔ Even (nrComplexPlaces K)

Tactic:
RingHom.mapMatrix_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ((basisMatrix K).map ⇑(starRingEnd ℂ)).det = (basisMatrix K).det ↔ Even (nrComplexPlaces K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : Field K
x : mixedSpace K
h : x = 0
⊢ ∀ (w : InfinitePlace K), True

Tactic:
implies_true

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) (RingHom.equivRatAlgHom K ℂ)
this : M.map ⇑ofRealHom = matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ
⊢ ↑‖(ofRealHom.mapMatrix ((mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm))).det‖₊ =
    ↑‖(matrixToStdBasis K).det * N.det‖₊

Tactic:
RingHom.mapMatrix_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) (RingHom.equivRatAlgHom K ℂ)
this : M.map ⇑ofRealHom = matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ
⊢ ↑‖(((mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)).map ⇑ofRealHom).det‖₊ =
    ↑‖(matrixToStdBasis K).det * N.det‖₊
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 : Nat.card ↥(Stab (mk φ)) = 2
⊢ ∃ σ, ComplexEmbedding.IsConj φ σ

Tactic:
Nat.card_eq_two_iff

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 : ∃ x y, x ≠ y ∧ {x, y} = Set.univ
⊢ ∃ σ, ComplexEmbedding.IsConj φ σ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: 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
⊢ ∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < √(1 + ↑B ^ 2)

Tactic:
have : minkowskiBound K ↑1 <
      volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩) := by
    rw [convexBodyLT'_volume, ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)]
    simp_rw [ite_pow, one_pow]
    rw [Finset.prod_ite_eq']
    simp_rw [Finset.notMem_erase, ite_false, mult, not_isReal_iff_isComplex.mpr hw₀,
      ite_true, ite_false, one_mul, NNReal.sq_sqrt]
    exact hB

Goal state after:
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, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), 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
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I
i j : ChooseBasisIndex ℤ (𝓞 K)
⊢ (latticeBasis K).toMatrix (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e) i j =
    (algebraMap ℚ ℝ).mapMatrix ((integralBasis K).toMatrix (⇑(basisOfFractionalIdeal K I) ∘ ⇑e)) i j

Tactic:
RingHom.mapMatrix_apply,

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ MeasureTheory.IsAddFundamentalDomain (↥(idealLattice K I)) (ZSpan.fundamentalDomain (fractionalIdealLatticeBasis K I))
    MeasureTheory.volume

Tactic:
rw [← span_idealLatticeBasis]
  exact ZSpan.isAddFundamentalDomain (fractionalIdealLatticeBasis K I) _

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

Goal state before:
pp: case inr
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : InfinitePlace K
hw : w.IsComplex
⊢ (normAtPlace w) ((negAt s) x) = (normAtPlace w) x

Tactic:
· simp_rw [normAtPlace_apply_of_isComplex hw, negAt_apply_isComplex]

Goal state after:
Module: Mathlib.RingTheory.Invariant.Galois

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : IsFractionRing A K
inst✝⁸ : IsFractionRing 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✝² : IsIntegrallyClosed A
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
h✝ : IsGalois K L
h : IntermediateField.fixedField ⊤ = ⊥
this : MulSemiringAction Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
k : K
hk : (algebraMap K L) k = (algebraMap B L) b
⊢ ∃ a, (algebraMap A B) a = b

Tactic:
have hb : IsIntegral A b := IsIntegralClosure.isIntegral A L b

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : IsFractionRing A K
inst✝⁸ : IsFractionRing 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✝² : IsIntegrallyClosed A
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
h✝ : IsGalois K L
h : IntermediateField.fixedField ⊤ = ⊥
this : MulSemiringAction Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
k : K
hk : (algebraMap K L) k = (algebraMap B L) b
hb : IsIntegral A b
⊢ ∃ a, (algebraMap A B) a = b
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case refine_2
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
x : mixedSpace K
h : x ∈ A
⊢ (∃ i, x ∈ ⇑(negAt i) '' plusPart A) ∨ x ∈ A ∧ ∃ i, x ∈ {x | x.1 i = 0}

Tactic:
· obtain hx | hx := exists_or_forall_not (fun w ↦ x.1 w = 0)
    · exact Or.inr ⟨h, hx⟩
    · refine Or.inl ⟨signSet x,
        (mem_negAt_plusPart_of_mem A hA h hx).mpr ⟨fun w hw ↦ ?_, fun w hw ↦ ?_⟩⟩
      · exact lt_of_le_of_ne hw (hx w)
      · exact lt_of_le_of_ne (lt_of_not_ge hw).le (Ne.symm (hx w))

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

Goal state before:
pp: case e'_2
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⟯
x✝¹ x✝ : ↑S
h_eq :
  (fun x ↦
        match x with
        | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩)
      x✝¹ =
    (fun x ↦
        match x with
        | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩)
      x✝
⊢ ↑↑x✝¹ = ℚ⟮⋯.choose⟯

Tactic:
exact (h _ (Subtype.mem _)).choose_spec.2

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

Goal state before:
pp: case e'_3
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⟯
x✝¹ x✝ : ↑S
h_eq :
  (fun x ↦
        match x with
        | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩)
      x✝¹ =
    (fun x ↦
        match x with
        | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩)
      x✝
⊢ ↑↑x✝ = ℚ⟮⋯.choose⟯

Tactic:
exact (h _ (Subtype.mem _)).choose_spec.2

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
B : Type u_6
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain B
inst✝³ : IsIntegrallyClosed B
inst✝² : Module.Finite A B
inst✝¹ : IsTorsionFree A B
inst✝ : IsGalois (FractionRing A) (FractionRing B)
x : B
this : FiniteDimensional (FractionRing A) (FractionRing B)
⊢ (algebraMap A B) ((intNorm A B) x) = ∏ σ, σ x

Tactic:
rw [← (galRestrict A (FractionRing A) (FractionRing B) B).toEquiv.prod_comp]

Goal state after:
A : Type u_1
B : Type u_6
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain B
inst✝³ : IsIntegrallyClosed B
inst✝² : Module.Finite A B
inst✝¹ : IsTorsionFree A B
inst✝ : IsGalois (FractionRing A) (FractionRing B)
x : B
this : FiniteDimensional (FractionRing A) (FractionRing B)
⊢ (algebraMap A B) ((intNorm A B) x) = ∏ i, ((galRestrict A (FractionRing A) (FractionRing B) B).toEquiv i) x
Module: Mathlib.NumberTheory.NumberField.ClassNumber

Goal state before:
pp: case refine_1
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.natAbs ∈
    Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊

Tactic:
suffices 0 < P.inertiaDeg ℤ by
      exact Finset.mem_Icc.mpr ⟨hpabsprime.one_le, le_trans (le_pow this) hple⟩

Goal state after:
case refine_1
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
⊢ 0 < P.inertiaDeg ℤ
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✝³ : IsDedekindDomain S
inst✝² : Module.IsTorsionFree R S
inst✝¹ : CharZero R
inst✝ : Algebra.IsIntegral R S
p : Ideal R
h : ∀ (P : Ideal S) (x : P.IsMaximal), P.LiesOver p → IsUnramifiedAt R P
P : Ideal S
hP : P.IsPrime
hlo : P.LiesOver p
⊢ IsUnramifiedAt R P

Tactic:
rcases eq_or_ne P ⊥ with rfl | hPbot

Goal state after:
case inl
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.IsTorsionFree R S
inst✝¹ : CharZero R
inst✝ : Algebra.IsIntegral R S
p : Ideal R
h : ∀ (P : Ideal S) (x : P.IsMaximal), P.LiesOver p → IsUnramifiedAt R P
hP : ⊥.IsPrime
hlo : ⊥.LiesOver p
⊢ IsUnramifiedAt R ⊥

case inr
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.IsTorsionFree R S
inst✝¹ : CharZero R
inst✝ : Algebra.IsIntegral R S
p : Ideal R
h : ∀ (P : Ideal S) (x : P.IsMaximal), P.LiesOver p → IsUnramifiedAt R P
P : Ideal S
hP : P.IsPrime
hlo : P.LiesOver p
hPbot : P ≠ ⊥
⊢ IsUnramifiedAt R P
Module: Mathlib.RingTheory.Ideal.Quotient.Index

Goal state before:
pp: case intro
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
N : Submodule R M
inst✝ : Finite (R ⧸ I)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
⊢ (I • N).toAddSubgroup.index ≤ (toAddSubgroup I).index ^ s.card * N.toAddSubgroup.index

Tactic:
← AddSubgroup.relIndex_mul_index
    (H := (I • N).toAddSubgroup) (K := N.toAddSubgroup) Submodule.smul_le_right

Goal state after:
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
N : Submodule R M
inst✝ : Finite (R ⧸ I)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
⊢ (I • N).toAddSubgroup.relIndex N.toAddSubgroup * N.toAddSubgroup.index ≤
    (toAddSubgroup I).index ^ s.card * N.toAddSubgroup.index
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
I : FractionalIdeal M K
⊢ ↑(extended L hf I) = span B (⇑(IsLocalization.map L f hf) '' ↑I)

Tactic:
by
  ext; simp [mem_coe, mem_extended_iff]

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

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

Tactic:
subst hP0
    rwa [eq_comm, span_singleton_eq_bot, ← mem_bot]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: n x : ℕ
⊢ (Ideal.Quotient.mk (Ideal.span {↑n})) ↑x = 0 ↔ n ∣ x

Tactic:
Ideal.Quotient.eq_zero_iff_mem,

Goal state after:
n x : ℕ
⊢ ↑x ∈ Ideal.span {↑n} ↔ n ∣ x
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I✝ I : Ideal R
⊢ I.LiesOver (span {↑(absNorm (under ℤ I))})

Tactic:
by
  rw [liesOver_iff, under_def, Int.ideal_span_absNorm_eq_self]

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

Goal state before:
pp: case neg.refine_1
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
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : PerfectField (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
a✝ b✝ : Ideal S
hx : absNorm ((relNorm R) a✝) = absNorm a✝
⊢ absNorm ((relNorm R) b✝) = absNorm b✝ → absNorm ((relNorm R) (a✝ * b✝)) = absNorm (a✝ * b✝)

Tactic:
hy

Goal state after:
case neg.refine_1
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
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : PerfectField (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
a✝ b✝ : Ideal S
hx : absNorm ((relNorm R) a✝) = absNorm a✝
hy : absNorm ((relNorm R) b✝) = absNorm b✝
⊢ absNorm ((relNorm R) (a✝ * b✝)) = absNorm (a✝ * b✝)