mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
⊢ ∃ ca, ca ≠ 0 ∧ a = (expand k (ringChar k)) ca ∧ a.natDegree = ca.natDegree * ringChar k

Tactic:
have heq := (expand_contract (ringChar k) hda chn0).symm
  refine ⟨contract (ringChar k) a, ?_, heq, ?_⟩
  · intro h
    rw [h, map_zero] at heq
    exact ha heq
  · rw [← natDegree_expand, ← heq]

Goal state after:
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✝ : Module.Finite ℚ K
x : K
⊢ absNorm (spanSingleton R⁰ x) = |(Algebra.norm ℚ) x|

Tactic:
by
  have : IsDomain K := IsFractionRing.isDomain R
  obtain ⟨d, ⟨r, hr⟩⟩ := IsLocalization.exists_integer_multiple R⁰ x
  rw [absNorm_eq' d (Ideal.span {r})]
  · rw [Ideal.absNorm_span_singleton]
    simp_rw [Nat.cast_natAbs, Int.cast_abs, show ((Algebra.norm ℤ _) : ℚ) = algebraMap ℤ ℚ
      (Algebra.norm ℤ _) by rfl, ← Algebra.norm_localization ℤ ℤ⁰ (Sₘ := K) _]
    rw [hr, Algebra.smul_def, map_mul, abs_mul, mul_div_assoc, mul_div_cancel₀ _ (by
      rw [ne_eq, abs_eq_zero, Algebra.norm_eq_zero_iff, IsFractionRing.to_map_eq_zero_iff]
      exact nonZeroDivisors.coe_ne_zero _)]
  · ext
    simp_rw [Submodule.mem_smul_pointwise_iff_exists, mem_coe, mem_spanSingleton, Submodule.mem_map,
      Algebra.linearMap_apply, Submonoid.smul_def, Ideal.mem_span_singleton', exists_exists_eq_and,
      map_mul, hr, ← Algebra.smul_def, smul_comm (d : R)]

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inl.right.inl
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
⊢ z = m ^ 2 + n ^ 2 ∧ (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m

pp: case h.inl.right.inr
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_neg : z = -(m ^ 2 + n ^ 2)
⊢ z = m ^ 2 + n ^ 2 ∧ (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m

Tactic:
· apply And.intro h_pos
        constructor
        · delta Int.gcd
          rw [Int.natAbs_neg, Int.natAbs_neg]
          exact ht3
        · rw [Int.neg_emod_two, Int.neg_emod_two]
          apply And.intro ht4
          lia

Goal state after:
case h.inl.right.inr
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_neg : z = -(m ^ 2 + n ^ 2)
⊢ z = m ^ 2 + n ^ 2 ∧ (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
Module: Mathlib.NumberTheory.NumberField.EquivReindex

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

Tactic:
← finrank_eq_card_chooseBasisIndex,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℚ K = finrank ℤ (𝓞 K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ volume (convexBodyLT K f) = (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) * ∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi

Tactic:
volume_eq_prod,

Goal state after:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ (volume.prod volume) (convexBodyLT K f) = (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) * ∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi
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 →+* ℂ
⊢ star (x✝ a✝ + x✝ b✝) = x✝ a✝ + x✝ b✝

Tactic:
star_add,

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 →+* ℂ
⊢ star (x✝ a✝) + star (x✝ b✝) = x✝ a✝ + x✝ b✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ‖(canonicalEmbedding K) x‖₊ = Finset.univ.sup fun φ ↦ ‖φ x‖₊

Tactic:
simp_rw [Pi.nnnorm_def, apply_at]

Goal state after:
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
B : ℝ≥0
⊢ volume (Set.Ioo (-1) 1 ×ˢ Set.Ioo (-↑B ^ 2) (↑B ^ 2)) = 4 * ↑B ^ 2

Tactic:
volume_eq_prod,

Goal state after:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ (volume.prod volume) (Set.Ioo (-1) 1 ×ˢ Set.Ioo (-↑B ^ 2) (↑B ^ 2)) = 4 * ↑B ^ 2
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
⊢ volume (convexBodyLT' K f w₀) =
    (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi) * (4 * ↑(f ↑w₀) ^ 2))

Tactic:
volume_eq_prod,

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
⊢ (volume.prod volume) (convexBodyLT' K 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.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
h : IsUnramified k w
⊢ Stab w = ⊥

Tactic:
eq_bot_iff,

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
⊢ Stab w ≤ ⊥
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ volume
      ((Set.univ.pi fun x ↦ Set.Ico 0 1) ×ˢ
        Set.univ.pi fun x ↦ ⇑measurableEquivPi ⁻¹' Set.univ.pi fun x ↦ Set.Ico 0 1) =
    1

Tactic:
volume_eq_prod,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (volume.prod volume)
      ((Set.univ.pi fun x ↦ Set.Ico 0 1) ×ˢ
        Set.univ.pi fun x ↦ ⇑measurableEquivPi ⁻¹' Set.univ.pi fun x ↦ Set.Ico 0 1) =
    1
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 →+* ℂ
x : Gal(K/k)
hx : x ∈ Stab (mk φ)
y : Gal(K/k)
hy : y ∈ Stab (mk φ)
h₁ : ⟨x, hx⟩ ≠ ⟨y, hy⟩
⊢ ∃ σ, ComplexEmbedding.IsConj φ σ

Tactic:
rw [mem_stabilizer_mk_iff] at hx hy

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 →+* ℂ
x : Gal(K/k)
hx✝ : x ∈ Stab (mk φ)
hx : x = 1 ∨ ComplexEmbedding.IsConj φ x
y : Gal(K/k)
hy✝ : y ∈ Stab (mk φ)
hy : y = 1 ∨ ComplexEmbedding.IsConj φ y
h₁ : ⟨x, hx✝⟩ ≠ ⟨y, hy✝⟩
⊢ ∃ σ, ComplexEmbedding.IsConj φ σ
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 : IsRamified k (mk φ)
⊢ ∃ σ, ComplexEmbedding.IsConj φ σ

Tactic:
rw [isRamified_iff_card_stabilizer_eq_two, Nat.card_eq_two_iff] at h
  obtain ⟨⟨x, hx⟩, ⟨y, hy⟩, h₁, -⟩ := h
  rw [mem_stabilizer_mk_iff] at hx hy
  grind

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)ˣ
⊢ Fintype.card (Free.ChooseBasisIndex ℤ ↥↑↑I) = Fintype.card (Free.ChooseBasisIndex ℤ (𝓞 K))

Tactic:
← finrank_eq_card_chooseBasisIndex,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ finrank ℤ ↥↑↑I = Fintype.card (Free.ChooseBasisIndex ℤ (𝓞 K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ finrank ℤ ↥↑↑I = Fintype.card (Free.ChooseBasisIndex ℤ (𝓞 K))

Tactic:
← finrank_eq_card_chooseBasisIndex,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ finrank ℤ ↥↑↑I = finrank ℤ (𝓞 K)
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 ℂ)
⊢ volume (fundamentalDomain (latticeBasis K)) = 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊)

Tactic:
suffices M.map ofRealHom = matrixToStdBasis K *
      (Matrix.reindex (indexEquiv K).symm (indexEquiv K).symm N).transpose by
    calc volume (fundamentalDomain (latticeBasis K))
      _ = ‖((mixedEmbedding.stdBasis K).toMatrix ((latticeBasis K).reindex e.symm)).det‖₊ := by
        rw [← fundamentalDomain_reindex _ e.symm, ← norm_toNNReal, measure_fundamentalDomain
          ((latticeBasis K).reindex e.symm), volume_fundamentalDomain_stdBasis, mul_one]
        rfl
      _ = ‖(matrixToStdBasis K).det * N.det‖₊ := by
        rw [← nnnorm_real, ← ofRealHom_eq_coe, RingHom.map_det, RingHom.mapMatrix_apply, this,
          det_mul, det_transpose, det_reindex_self]
      _ = (2 : ℝ≥0∞)⁻¹ ^ Fintype.card {w : InfinitePlace K // IsComplex w} * sqrt ‖N.det ^ 2‖₊ := by
        have : ‖Complex.I‖₊ = 1 := by rw [← norm_toNNReal, norm_I, Real.toNNReal_one]
        rw [det_matrixToStdBasis, nnnorm_mul, nnnorm_pow, nnnorm_mul, this, mul_one, nnnorm_inv,
          coe_mul, ENNReal.coe_pow, ← norm_toNNReal, RCLike.norm_two, Real.toNNReal_ofNat,
          coe_inv two_ne_zero, coe_ofNat, nnnorm_pow, NNReal.sqrt_sq]
      _ = (2 : ℝ≥0∞)⁻¹ ^ Fintype.card { w // IsComplex w } * NNReal.sqrt ‖discr K‖₊ := by
        rw [← Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two, Algebra.discr_reindex,
          ← coe_discr, map_intCast, ← Complex.nnnorm_intCast]

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 ℂ)
⊢ M.map ⇑ofRealHom = matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : LinearIndependent ℝ (⇑(commMap K) ∘ ⇑(canonicalEmbedding.latticeBasis K))
⊢ Fintype.card (ChooseBasisIndex ℤ (𝓞 K)) = finrank ℝ (mixedSpace K)

Tactic:
← finrank_eq_card_chooseBasisIndex,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : LinearIndependent ℝ (⇑(commMap K) ∘ ⇑(canonicalEmbedding.latticeBasis K))
⊢ finrank ℤ (𝓞 K) = finrank ℝ (mixedSpace K)
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₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ ∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(max B 1)

Tactic:
have : minkowskiBound K ↑1 < volume (convexBodyLT K (fun w ↦ if w = w₀ then B else 1)) := 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, hw₀, ite_true, one_mul, pow_one]
    exact hB
  obtain ⟨a, h_nz, h_le⟩ := exists_ne_zero_mem_ringOfIntegers_lt K this
  refine ⟨a, ?_, fun w ↦ lt_of_lt_of_le (h_le w) ?_⟩
  · exact is_primitive_element_of_infinitePlace_lt h_nz
      (fun w h_ne ↦ by convert! (if_neg h_ne) ▸ h_le w) (Or.inl hw₀)
  · split_ifs <;> simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ Fintype.card (ChooseBasisIndex ℤ (𝓞 K)) = Fintype.card (ChooseBasisIndex ℤ ↥↑↑I)

Tactic:
← finrank_eq_card_chooseBasisIndex,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ finrank ℤ (𝓞 K) = Fintype.card (ChooseBasisIndex ℤ ↥↑↑I)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ finrank ℤ (𝓞 K) = Fintype.card (ChooseBasisIndex ℤ ↥↑↑I)

Tactic:
← finrank_eq_card_chooseBasisIndex,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ finrank ℤ (𝓞 K) = finrank ℤ ↥↑↑I
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
i : ChooseBasisIndex ℤ ↥↑↑I
⊢ (fractionalIdealLatticeBasis K I) i = (mixedEmbedding K) ((basisOfFractionalIdeal K I) i)

Tactic:
simp only [fractionalIdealLatticeBasis, Basis.coe_reindex, Basis.coe_mk, Function.comp_apply,
    Equiv.apply_symm_apply]

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : Algebra B L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsIntegralClosure B A L
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Algebra.IsIntegral A B
inst✝ : IsTorsionFree A B
x : B
this : IsFractionRing B L
⊢ (FractionRing.algEquiv A K).symm ((algebraMap A K) ((intNorm A B) x)) =
    (FractionRing.algEquiv A K).symm ((norm K) ((algebraMap B L) x))

Tactic:
rw [AlgEquiv.commutes, Algebra.intNorm, Algebra.map_intNormAux,
    ← AlgEquiv.commutes (FractionRing.algEquiv B L)]

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : Algebra B L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsIntegralClosure B A L
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Algebra.IsIntegral A B
inst✝ : IsTorsionFree A B
x : B
this : IsFractionRing B L
⊢ (norm (FractionRing A)) ((algebraMap B (FractionRing B)) x) =
    (FractionRing.algEquiv A K).symm ((norm K) ((FractionRing.algEquiv B L) ((algebraMap B (FractionRing B)) x)))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : Set (realSpace K)
hs : ∀ x ∈ s, ∀ (w : InfinitePlace K), 0 ≤ x w
⊢ s ⊆ Set.range normAtAllPlaces

Tactic:
rintro x hx

Goal state after:
K : Type u_1
inst✝ : Field K
s : Set (realSpace K)
hs : ∀ x ∈ s, ∀ (w : InfinitePlace K), 0 ≤ x w
x : realSpace K
hx : x ∈ s
⊢ x ∈ Set.range normAtAllPlaces
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✝² : Module.IsTorsionFree R S
inst✝¹ : CharZero R
inst✝ : Algebra.IsIntegral R S
⊢ IsUnramifiedAt R ⊥

Tactic:
by
  have : IsFractionRing S (Localization.AtPrime (⊥ : Ideal S)) := by
    simpa [Ideal.primeCompl_bot] using Localization.isLocalization (M := (⊥ : Ideal S).primeCompl)
  let : Field (Localization.AtPrime (⊥ : Ideal S)) := IsFractionRing.toField S
  have : FaithfulSMul R (Localization.AtPrime (⊥ : Ideal S)) := by
    rw [faithfulSMul_iff_algebraMap_injective,
      IsScalarTower.algebraMap_eq R S (Localization.AtPrime ⊥)]
    exact (IsFractionRing.injective S _).comp (FaithfulSMul.algebraMap_injective R S)
  let := FractionRing.liftAlgebra R (Localization.AtPrime (⊥ : Ideal S))
  have : Algebra.IsAlgebraic (FractionRing R) (Localization.AtPrime ⊥) :=
    isAlgebraic_of_isFractionRing R S (FractionRing R) (Localization.AtPrime (⊥ : Ideal S))
  have : FormallyUnramified (FractionRing R) (Localization.AtPrime (⊥ : Ideal S)) :=
    FormallyUnramified.of_isSeparable _ _
  exact FormallyUnramified.comp R (FractionRing R) (Localization.AtPrime ⊥)

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

Goal state before:
pp: 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
⊢ IsPrincipalIdealRing (𝓞 K)

Tactic:
refine isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime <|
    fun ⟨P, HP⟩ hP hPN ↦ ?_
  obtain ⟨p, hp⟩ := IsPrincipalIdealRing.principal <| under ℤ P
  have hp0 : p ≠ 0 := fun h ↦ nonZeroDivisors.coe_ne_zero ⟨P, HP⟩ <|
    eq_bot_of_comap_eq_bot (R := ℤ) <| by simpa only [hp, submodule_span_eq, span_singleton_eq_bot]
  have hpprime := (span_singleton_prime hp0).mp
  simp only [← submodule_span_eq, ← hp] at hpprime
  have hlies : P.LiesOver (span {p}) := by
    rcases abs_choice p with h | h <;>
    simpa [h, span_singleton_neg p, ← submodule_span_eq, ← hp] using over_under P
  have hspan : span {↑p.natAbs} = span {p} := by
    rcases abs_choice p with h | h <;> simp [h]
  have hple : p.natAbs ^ P.inertiaDeg ℤ ≤ ⌊(M K)⌋₊ := by
    refine le_floor ?_
    have : P.IsMaximal := hP.isMaximal (by simpa using HP.2)
    have : (span {p}).IsMaximal := (hpprime (.under ℤ P)).isMaximal_span_singleton
    simpa only [hspan, ← cast_pow, ← natAbs_pow_inertiaDeg p P] using hPN
  have hpabsprime := Int.prime_iff_natAbs_prime.mp (hpprime (hP.under _))
  refine h _ ?_ hpabsprime _ ⟨hP, ?_⟩ hple
  · suffices 0 < P.inertiaDeg ℤ by
      exact Finset.mem_Icc.mpr ⟨hpabsprime.one_le, le_trans (le_pow this) hple⟩
    have := (isPrime_of_prime (prime_span_singleton_iff.mpr <|
      hpprime (hP.under _))).isMaximal <| by simp [((hpprime (hP.under _))).ne_zero]
    exact inertiaDeg_pos ..
  · exact hspan ▸ hlies

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
I : FractionalIdeal M K
inst✝ : IsDomain B
hf' : Function.Injective ⇑f
hI : I ≠ 0
hN : 0 ∉ N
x : K
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ ∃ x, ∃ (_ : x ∈ I), ¬(IsLocalization.map L f hf) x = 0

Tactic:
refine ⟨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
I : FractionalIdeal M K
inst✝ : IsDomain B
hf' : Function.Injective ⇑f
hI : I ≠ 0
hN : 0 ∉ N
x : K
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ ¬(IsLocalization.map L f hf) x = 0
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 = ⊥
hspan0 : span {x} ≠ ⊥
Q : Ideal R
hQ : Q = P
⊢ Multiset.count Q (normalizedFactors (span {x})) = 1

Tactic:
subst hQ

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
hspan0 : span {x} ≠ ⊥
Q : Ideal R
hP : Q.IsPrime
x_mem : x ∈ Q
hxP2 : x ∉ Q ^ 2
hxQ : ∀ (Q_1 : Ideal R), Q_1.IsPrime → Q_1 ≠ Q → x ∉ Q_1
hP0 : ¬Q = ⊥
⊢ Multiset.count Q (normalizedFactors (span {x})) = 1