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

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
⊢ 2 * q / (1 + q ^ 2) = 2 * (↑n / ↑m) / (1 + (↑n / ↑m) ^ 2)

Tactic:
hq2

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
⊢ 2 * (↑n / ↑m) / (1 + (↑n / ↑m) ^ 2) = 2 * (↑n / ↑m) / (1 + (↑n / ↑m) ^ 2)
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
⊢ m.gcd n = 1

Tactic:
Int.gcd_comm

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
⊢ n.gcd m = 1
Module: Mathlib.NumberTheory.NumberField.FractionalIdeal

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

Tactic:
RingOfIntegers.rank,

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

Goal state before:
pp: case inl
k : Type u_1
inst✝ : Field k
p q r : ℕ
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
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp : IsCoprime (C u * a ^ p) (C v * b ^ q)
hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r)
hcap : IsCoprime (C w * c ^ r) (C u * a ^ p)
habcp : IsCoprime (C u * a ^ p * (C v * b ^ q)) (C w * c ^ r)
nd_lt :
  0 + (a ^ p).natDegree + 1 ≤ (radical a * radical b * radical c).natDegree ∧
    0 + (b ^ q).natDegree + 1 ≤ (radical a * radical b * radical c).natDegree ∧
      0 + (c ^ r).natDegree + 1 ≤ (radical a * radical b * radical c).natDegree
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
natDegree_pow,

Goal state after:
case inl
k : Type u_1
inst✝ : Field k
p q r : ℕ
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
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp : IsCoprime (C u * a ^ p) (C v * b ^ q)
hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r)
hcap : IsCoprime (C w * c ^ r) (C u * a ^ p)
habcp : IsCoprime (C u * a ^ p * (C v * b ^ q)) (C w * c ^ r)
nd_lt :
  0 + p * a.natDegree + 1 ≤ (radical a * radical b * radical c).natDegree ∧
    0 + q * b.natDegree + 1 ≤ (radical a * radical b * radical c).natDegree ∧
      0 + r * c.natDegree + 1 ≤ (radical a * radical b * radical c).natDegree
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0
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₀
⊢ { toFun := fun I ↦ ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den|, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
      I =
    ↑(Ideal.absNorm I₀) / ↑|(Algebra.norm ℤ) ↑a|

Tactic:
← absNorm_div_norm_eq_absNorm_div_norm a I₀ h,

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
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀
⊢ { toFun := fun I ↦ ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den|, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
      I =
    ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den|
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
⊢ h.IsPrimitiveClassified

Tactic:
Int.gcd_comm

Goal state after:
case inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : y.gcd x = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
⊢ h.IsPrimitiveClassified
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: case refine_2.inr
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h : K.topologicalClosure = ⊤
⊢ (↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype

Tactic:
· -- ψ₁ is the continuous ring hom `ℂ →+* ℂ` constructed from `closure (K) ≃+* ℂ`
      -- and `extψ : closure (K) →+* ℂ`
      let ψ₁ :=
        RingHom.comp extψ
          (RingHom.comp (RingEquiv.subfieldCongr h).symm.toRingHom
            (@Subfield.topEquiv ℂ _).symm.toRingHom)
      -- Porting note: was `by continuity!` and was used inline
      have hψ₁ : Continuous ψ₁ := by
        simpa only [RingHom.coe_comp] using! hψ.comp (continuous_id.subtype_mk _)
      rcases ringHom_eq_id_or_conj_of_continuous hψ₁ with h | h
      · left
        ext1 z
        convert! RingHom.congr_fun h z using 1
        exact (IsDenseInducing.extend_eq di hc.continuous z).symm
      · right
        ext1 z
        convert! RingHom.congr_fun h z using 1
        exact (IsDenseInducing.extend_eq di hc.continuous z).symm

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr.inr.inl.right
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (2 * m * n).gcd (m ^ 2 - n ^ 2) = 1

Tactic:
Int.gcd_comm

Goal state after:
case mpr.inr.inl.right
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr.inr.inr.right
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (2 * m * n).gcd (m ^ 2 - n ^ 2) = 1

Tactic:
Int.gcd_comm

Goal state after:
case mpr.inr.inr.right
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case inl
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
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
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
ch0 : ringChar k = 0
da : derivative a = 0
czk : CharZero k
⊢ (C (a.coeff 0)).natDegree = 0

Tactic:
exact natDegree_C _

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∑ w, w.mult = ∑ x, 1

Tactic:
← Finset.univ.sum_fiberwise
    (fun φ => InfinitePlace.mk φ)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∑ w, w.mult = ∑ j, ∑ i with mk i = j, 1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∑ w, w.mult = finrank ℚ K

Tactic:
classical
  rw [← Embeddings.card K ℂ, Fintype.card, Finset.card_eq_sum_ones, ← Finset.univ.sum_fiberwise
    (fun φ => InfinitePlace.mk φ)]
  exact Finset.sum_congr rfl
    (fun _ _ => by rw [Finset.sum_const, smul_eq_mul, mul_one, card_filter_mk_eq])

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
x✝ : a ∈ (fun x ↦ (algebraMap (𝓞 K) K) ↑x) '' ↑(torsion K)
u : (𝓞 K)ˣ
h_tors : u ∈ ↑(torsion K)
h_ua : (fun x ↦ (algebraMap (𝓞 K) K) ↑x) u = a
⊢ IsIntegral ℤ a

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
x✝ : a ∈ (fun x ↦ (algebraMap (𝓞 K) K) ↑x) '' ↑(torsion K)
u : (𝓞 K)ˣ
h_tors : u ∈ ↑(torsion K)
h_ua : (fun x ↦ (algebraMap (𝓞 K) K) ↑x) u = a
φ : K →+* ℂ
⊢ ‖φ a‖ ≤ 1

Tactic:
· rw [← h_ua]
    exact u.val.prop

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
x✝ : a ∈ (fun x ↦ (algebraMap (𝓞 K) K) ↑x) '' ↑(torsion K)
u : (𝓞 K)ˣ
h_tors : u ∈ ↑(torsion K)
h_ua : (fun x ↦ (algebraMap (𝓞 K) K) ↑x) u = a
φ : K →+* ℂ
⊢ ‖φ a‖ ≤ 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∑ x_1, (canonicalEmbedding K) (((integralBasis K).repr x) x_1 • (integralBasis K) x_1) ∈
    Submodule.span ℚ (Set.range ⇑(latticeBasis K))

Tactic:
map_rat_smul

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∑ x_1, ((integralBasis K).repr x) x_1 • (canonicalEmbedding K) ((integralBasis K) x_1) ∈
    Submodule.span ℚ (Set.range ⇑(latticeBasis K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card { w // w.IsReal } + ∑ i, finrank ℝ ℂ = finrank ℚ K

Tactic:
Complex.finrank_real_complex,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card { w // w.IsReal } + ∑ i, 2 = finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
⊢ 0 ≤ (normAtPlace w) x

Tactic:
by
  rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]
  split_ifs <;> exact norm_nonneg _

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
φ : K →+* ℂ
h : IsUnmixed k φ
hv : ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
⊢ ComplexEmbedding.IsReal (mk φ).embedding

Tactic:
simp [embedding_mk_eq_of_isReal, h hv]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ rootDiscr K = ↑|discr K| ^ (↑(finrank ℚ K))⁻¹

Tactic:
rw [rootDiscr]

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)ᵀ
⊢ volume (fundamentalDomain ((latticeBasis K).reindex e.symm)) =
    ↑‖((mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)).det‖.toNNReal

Tactic:
measure_fundamentalDomain
          ((latticeBasis K).reindex e.symm),

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)ᵀ
⊢ ENNReal.ofReal |(Basis.det ?b₀) ⇑((latticeBasis K).reindex e.symm)| * volume (fundamentalDomain ?b₀) =
    ↑‖((mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)).det‖.toNNReal

case b₀
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) := ⋯
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := ⋯
M : Matrix (index K) (index K) ℝ := ⋯
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := ⋯
this : M.map ⇑ofRealHom = matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ
⊢ Basis (index K) ℝ (mixedSpace K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) c) =
    ∑ x_1,
        fromBlocks 1 0 0
            ((blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I]).submatrix ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm
              ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
            c (Sum.inl x_1) *
          x ((indexEquiv K) (Sum.inl x_1)) +
      ∑ x_1 ∈ univ ×ˢ univ,
        fromBlocks 1 0 0
            ((blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I]).submatrix ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm
              ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
            c (Sum.inr x_1) *
          x ((indexEquiv K) (Sum.inr x_1))

Tactic:
sum_product,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) c) =
    ∑ x_1,
        fromBlocks 1 0 0
            ((blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I]).submatrix ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm
              ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
            c (Sum.inl x_1) *
          x ((indexEquiv K) (Sum.inl x_1)) +
      ∑ x_1,
        ∑ y,
          fromBlocks 1 0 0
              ((blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I]).submatrix
                ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
              c (Sum.inr (x_1, y)) *
            x ((indexEquiv K) (Sum.inr (x_1, y)))
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))
⊢ finrank ℤ (𝓞 K) = finrank ℝ (mixedSpace K)

Tactic:
RingOfIntegers.rank,

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.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : LinearIndependent ℝ (⇑(commMap K) ∘ ⇑(canonicalEmbedding.latticeBasis K))
⊢ finrank ℚ K = Fintype.card { w // w.IsReal } + ∑ i, finrank ℝ ℂ

Tactic:
Complex.finrank_real_complex,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : LinearIndependent ℝ (⇑(commMap K) ∘ ⇑(canonicalEmbedding.latticeBasis K))
⊢ finrank ℚ K = Fintype.card { w // w.IsReal } + ∑ i, 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∑ x_1, (mixedEmbedding K) (((integralBasis K).repr x) x_1 • (integralBasis K) x_1) ∈
    Submodule.span ℚ (Set.range ⇑(latticeBasis K))

Tactic:
map_rat_smul

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∑ x_1, ((integralBasis K).repr x) x_1 • (mixedEmbedding K) ((integralBasis K) x_1) ∈
    Submodule.span ℚ (Set.range ⇑(latticeBasis K))
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ ↑(FractionalIdeal.absNorm ↑I) *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * (↑2 ^ nrRealPlaces K * (↑pi / ↑2) ^ nrComplexPlaces K / ↑↑(finrank ℚ K).factorial)⁻¹))) =
    ↑(FractionalIdeal.absNorm ↑I) *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹)))

Tactic:
coe_real_pi,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ ↑(FractionalIdeal.absNorm ↑I) *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * (↑2 ^ nrRealPlaces K * (π / ↑2) ^ nrComplexPlaces K / ↑↑(finrank ℚ K).factorial)⁻¹))) =
    ↑(FractionalIdeal.absNorm ↑I) *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹)))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (stdOrthonormalBasis K).toBasis.map ↑(toMixed K) = stdBasis K

Tactic:
ext <;> rfl

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : 𝓞 K
h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1
h_nz : (algebraMap (𝓞 K) K) a ≠ 0
h_nm :
  ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a)| ≤
    ↑(FractionalIdeal.absNorm ↑1) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial /
        ↑(finrank ℚ K) ^ finrank ℚ K *
      √|↑(discr K)|
⊢ ↑|(Algebra.norm ℚ) ↑a| ≤
    (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|

Tactic:
simp_rw [Units.val_one, FractionalIdeal.absNorm_one, Rat.cast_one, one_mul] at h_nm

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : 𝓞 K
h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1
h_nz : (algebraMap (𝓞 K) K) a ≠ 0
h_nm :
  ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a)| ≤
    (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|
⊢ ↑|(Algebra.norm ℚ) ↑a| ≤
    (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

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

Tactic:
Real.rpow_two

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsTotallyComplex K
h : 0 < ↑(finrank ℚ K)
⊢ ↑(finrank ℚ K) ^ (2 * finrank ℚ K) / ((4 / π) ^ finrank ℚ K * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
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✝⁷ : IsIntegrallyClosed A
inst✝⁶ : IsDomain A
inst✝⁵ : IsDomain B
inst✝⁴ : IsIntegrallyClosed B
inst✝³ : Algebra.IsIntegral A B
inst✝² : IsTorsionFree A B
inst✝¹ : Free A B
inst✝ : Module.Finite A B
x : B
this : IsIntegralClosure B A (FractionRing B)
⊢ (norm (FractionRing A)) ((algebraMap B (FractionRing B)) x) = (algebraMap A (FractionRing A)) ((norm A) x)

Tactic:
Algebra.norm_localization A A⁰

Goal state after:
A : Type u_1
B : Type u_6
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : IsIntegrallyClosed A
inst✝⁶ : IsDomain A
inst✝⁵ : IsDomain B
inst✝⁴ : IsIntegrallyClosed B
inst✝³ : Algebra.IsIntegral A B
inst✝² : IsTorsionFree A B
inst✝¹ : Free A B
inst✝ : Module.Finite A B
x : B
this : IsIntegralClosure B A (FractionRing B)
⊢ (algebraMap A (FractionRing A)) ((norm A) x) = (algebraMap A (FractionRing A)) ((norm A) x)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * ↑N) < ↑(finrank ℚ K)
⊢ ↑↑N ≤ ↑N

Tactic:
Int.cast_natCast

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * ↑N) < ↑(finrank ℚ K)
⊢ ↑N ≤ ↑N
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: case refine_1
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
x : L
⊢ x ∈ (fun I ↦ ↑I) 1 → x ∈ (fun I ↦ ↑I) (extended L hf 1)

Tactic:
rintro ⟨b, _, rfl⟩

Goal state after:
case refine_1
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
b : B
left✝ : b ∈ ↑⊤
⊢ (Algebra.linearMap B L) b ∈ (fun I ↦ ↑I) (extended L hf 1)