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

Goal state before:
pp: L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : 𝓞 L
hint : IsIntegral ℤ (∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x)
⊢ ↑((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x)) = ↑(x * ⟨∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x, hint⟩)

Tactic:
rw [coe_algebraMap_norm K x, norm_eq_prod_automorphisms]

Goal state after:
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : 𝓞 L
hint : IsIntegral ℤ (∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x)
⊢ ∏ σ, σ ↑x = ↑(x * ⟨∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x, hint⟩)
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ ofReal '' univ

Tactic:
simp only [image_univ]

Goal state after:
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ range ofReal
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : z ≤ 0
⊢ PythagoreanTriple x y (-z)

Tactic:
simpa [PythagoreanTriple, neg_mul_neg] using h.eq

Goal state after:
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ := ⋯
this : IsTopologicalRing ↥K.topologicalClosure := ⋯
ι : ↥K → ↥K.topologicalClosure := ⋯
ui : IsUniformInducing ι
di : IsDenseInducing ι := ⋯
extψ : ↥K.topologicalClosure →+* ℂ := ⋯
hψ : Continuous (⋯.extend ⇑ψ)
h : K.topologicalClosure = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := ⋯
ψ₁ : ℝ →+* ℂ := ⋯
hψ₁ : Continuous ⇑ψ₁
x : ↥K
⊢ ∃ r, ofRealHom.rangeRestrictField r = j (ι x)

Tactic:
obtain ⟨r, hr⟩ := SetLike.coe_mem (j (ι x))

Goal state after:
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 = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrictField)
hψ₁ : Continuous ⇑ψ₁
x : ↥K
r : ℝ
hr : ofRealHom r = ↑(j (ι x))
⊢ ∃ r, ofRealHom.rangeRestrictField r = j (ι x)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
⊢ LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)

Tactic:
change LipschitzWith 1 (ψ ∘ ι.symm)

Goal state after:
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
⊢ LipschitzWith 1 (⇑ψ ∘ ⇑ι.symm)
Module: Mathlib.NumberTheory.PythagoreanTriples

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

Tactic:
neg_sq m

Goal state after:
case h.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 : ℤ
ht2 : z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)
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
⊢ x = m ^ 2 - (-n) ^ 2 ∧
    y = 2 * -m * -n ∧
      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.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
hw : w.IsReal
x : K
⊢ ‖(embedding_of_isReal hw) x‖ = ‖w.embedding x‖

Tactic:
← embedding_of_isReal_apply hw,

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
hw : w.IsReal
x : K
⊢ ‖(embedding_of_isReal hw) x‖ = ‖↑((embedding_of_isReal hw) x)‖
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
this : w ↑a < 1
z : InfinitePlace K
x✝ : z ∈ Finset.univ
⊢ z ↑a ^ z.mult < 1

Tactic:
refine pow_lt_one₀ (apply_nonneg _ _) ?_ (by rw [mult]; split_ifs <;> norm_num)

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
this : w ↑a < 1
z : InfinitePlace K
x✝ : z ∈ Finset.univ
⊢ z ↑a < 1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
⊢ ∀ (ψ : K →ₐ[ℚ] ℂ), w.embedding.toRatAlgHom ↑x = ψ ↑x → w.embedding.toRatAlgHom = ψ

Tactic:
intro ψ

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
ψ : K →ₐ[ℚ] ℂ
⊢ w.embedding.toRatAlgHom ↑x = ψ ↑x → w.embedding.toRatAlgHom = ψ
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
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
heq : (expand k ch) (C u * ca ^ p + C v * cb ^ q + C w * cc ^ r) = 0
⊢ C u * ca ^ p + C v * cb ^ q + C w * cc ^ r = 0

Tactic:
Polynomial.expand_eq_zero (zero_lt_iff.mpr chn0)

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
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
heq : C u * ca ^ p + C v * cb ^ q + C w * cc ^ r = 0
⊢ C u * ca ^ p + C v * cb ^ q + C w * cc ^ r = 0
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
heq : 1 * a ^ n + 1 * b ^ n + -(1 * c ^ n) = 0
hn' : 0 < n
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0

Tactic:
← neg_mul

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
heq : 1 * a ^ n + 1 * b ^ n + -1 * c ^ n = 0
hn' : 0 < n
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

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

Tactic:
ComplexEmbedding.isReal_iff.mp hφ

Goal state after:
case pos.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ x φ = x φ
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case neg
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 ∨ ((mk φ).comap (algebraMap k K)).IsComplex

Tactic:
· exact .inr <| by simpa using (isReal_mk_iff.not.2 hv)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
⊢ mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) = 1

Tactic:
norm_eq_norm,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
⊢ ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) ↑u)| = 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
⊢ mixedEmbedding.norm ((mixedEmbedding K) a) = 0 ↔ (mixedEmbedding K) a = 0

Tactic:
norm_eq_norm,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
⊢ ↑|(Algebra.norm ℚ) a| = 0 ↔ (mixedEmbedding K) a = 0
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case pos.intro
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
hw : ¬IsUnramified k w
H : Finite Gal(K/k)
val✝ : Fintype Gal(K/k)
⊢ Nat.card ↥(Stab w) ∣ Nat.card Gal(K/k)

Tactic:
exact Subgroup.card_subgroup_dvd_card (Stab w)

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
w : InfinitePlace K
hw : IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
w' : InfinitePlace K
⊢ w' ∈ {w | IsUnramified k w} ∧ w'.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w ↔
    w' ∈ (MulAction.orbit Gal(K/k) w).toFinset

Tactic:
mem_filter_univ,

Goal state after:
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
w : InfinitePlace K
hw : IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
w' : InfinitePlace K
⊢ IsUnramified k w' ∧ w'.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w ↔
    w' ∈ (MulAction.orbit Gal(K/k) w).toFinset
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ ↥↑↑I ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
⊢ ENNReal.ofReal |(Basis.det ?b₀) (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e.symm)| *
      volume (fundamentalDomain ?b₀) =
    ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * volume (fundamentalDomain (latticeBasis K))

Tactic:
rw [mixedEmbedding.det_basisOfFractionalIdeal_eq_norm]

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)ˣ
⊢ minkowskiBound K I < ∞

Tactic:
by
  classical
  -- FIXME: Make `finiteness` work here
  exact ENNReal.mul_lt_top (fundamentalDomain_isBounded _).measure_lt_top <|
    ENNReal.pow_lt_top ENNReal.ofNat_lt_top

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
w : InfinitePlace K
hw : ¬IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
w' : InfinitePlace K
⊢ w' ∈ {x | ¬IsUnramified k x} ∧ w'.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w ↔
    w' ∈ (MulAction.orbit Gal(K/k) w).toFinset

Tactic:
mem_filter_univ,

Goal state after:
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
w : InfinitePlace K
hw : ¬IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
w' : InfinitePlace K
⊢ ¬IsUnramified k w' ∧ w'.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w ↔
    w' ∈ (MulAction.orbit Gal(K/k) w).toFinset
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inr.«0»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsComplex }
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) (Sum.inr (w, (fun i ↦ i) ⟨0, ⋯⟩))) =
    ∑ x_1,
        fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
            (Sum.inr (w, (fun i ↦ i) ⟨0, ⋯⟩)) (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1,
        (fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inr (w, (fun i ↦ i) ⟨0, ⋯⟩)) (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inr (w, (fun i ↦ i) ⟨0, ⋯⟩)) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))

Tactic:
simp only [Fin.zero_eta, Fin.isValue, stdBasis_apply_isComplex_fst, re_eq_add_conj,
        mul_neg, fromBlocks_apply₂₁, Matrix.zero_apply, zero_mul, sum_const_zero,
        fromBlocks_apply₂₂, submatrix_apply, Prod.swap_prod_mk, blockDiagonal_apply, of_apply,
        cons_val', cons_val_zero, empty_val', cons_val_fin_one, ite_mul, cons_val_one,
        sum_add_distrib, sum_ite_eq, mem_univ, ↓reduceIte, ← hx (embedding w), zero_add]

Goal state after:
case inr.«0»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsComplex }
⊢ (x (↑w).embedding + (starRingEnd ℂ) (x (↑w).embedding)) / 2 =
    2⁻¹ * x (↑w).embedding + 2⁻¹ * (starRingEnd ℂ) (x (↑w).embedding)
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
⊢ (ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I)).toReal *
      (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:
rw [ENNReal.toReal_ofReal (Rat.cast_nonneg.mpr (FractionalIdeal.absNorm_nonneg I.1))]

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 * (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)⁻¹)))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case pos
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 : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ : |(w₀.embedding ↑a).re| < 1 ∧ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ ‖w₀.embedding ↑a‖ ^ 2 < 1 + ↑B ^ 2

Tactic:
← Complex.re_add_im
        (embedding w₀ _),

Goal state after:
case pos
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 : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ : |(w₀.embedding ↑a).re| < 1 ∧ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ ‖↑(w₀.embedding ↑a).re + ↑(w₀.embedding ↑a).im * Complex.I‖ ^ 2 < 1 + ↑B ^ 2
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✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : IsTorsionFree A B
x : B
this✝² : IsIntegralClosure B A (FractionRing B)
this✝¹ : Algebra.IsAlgebraic (FractionRing A) (FractionRing B)
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
⊢ (algebraMap A K) ((intTrace A B) x) = (trace K L) ((algebraMap B L) x)

Tactic:
have := IsIntegralClosure.isFractionRing_of_finite_extension A K L B

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✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : IsTorsionFree A B
x : B
this✝³ : IsIntegralClosure B A (FractionRing B)
this✝² : Algebra.IsAlgebraic (FractionRing A) (FractionRing B)
this✝¹ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this✝ : FiniteDimensional (FractionRing A) (FractionRing B)
this : IsFractionRing B L
⊢ (algebraMap A K) ((intTrace A B) x) = (trace K L) ((algebraMap B L) x)
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
⊢ (algebraMap A K) ((intNorm A B) x) = (norm K) ((algebraMap B L) x)

Tactic:
have := IsIntegralClosure.isFractionRing_of_finite_extension A K L B

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
⊢ (algebraMap A K) ((intNorm A B) x) = (norm K) ((algebraMap B L) x)
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
x : B
this : FiniteDimensional (FractionRing A) (FractionRing B)
hx : x = 0
⊢ (algebraMap A B) ((intNorm A B) x) = x * 1

Tactic:
simp [hx]

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: case mpr
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : FaithfulSMul A B
p : Ideal A
P : Ideal B
inst✝¹⁵ : P.IsPrime
inst✝¹⁴ : 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✝⁸ : IsDomain C
inst✝⁷ : Algebra A C
inst✝⁶ : Algebra B C
inst✝⁵ : FaithfulSMul B 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
this✝¹ : Algebra.IsIntegral A C
this✝ : Algebra.IsIntegral B C
f : GAC →* G := restrictHom GAC G A B C
H : Subgroup GAC := Subgroup.comap f (stabilizer G P)
key : ∀ (Q Q' : Ideal C) [Q.LiesOver P] [Q'.LiesOver P] (g : GAC), g • Q = Q' → g ∈ H
Q : Ideal C
left✝¹ : Q.IsPrime
right✝¹ : Q.LiesOver P
this : Q.LiesOver p
Q' : Ideal C
left✝ : Q'.IsPrime
right✝ : Q'.LiesOver P
⊢ Q' ∈ orbit (↥H) Q

Tactic:
have : Q'.LiesOver p := .trans Q' P p

Goal state after:
case mpr
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : FaithfulSMul A B
p : Ideal A
P : Ideal B
inst✝¹⁵ : P.IsPrime
inst✝¹⁴ : 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✝⁸ : IsDomain C
inst✝⁷ : Algebra A C
inst✝⁶ : Algebra B C
inst✝⁵ : FaithfulSMul B 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
this✝² : Algebra.IsIntegral A C
this✝¹ : Algebra.IsIntegral B C
f : GAC →* G := restrictHom GAC G A B C
H : Subgroup GAC := Subgroup.comap f (stabilizer G P)
key : ∀ (Q Q' : Ideal C) [Q.LiesOver P] [Q'.LiesOver P] (g : GAC), g • Q = Q' → g ∈ H
Q : Ideal C
left✝¹ : Q.IsPrime
right✝¹ : Q.LiesOver P
this✝ : Q.LiesOver p
Q' : Ideal C
left✝ : Q'.IsPrime
right✝ : Q'.LiesOver P
this : Q'.LiesOver p
⊢ Q' ∈ orbit (↥H) Q