mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
h : radical a = radical b
⊢ primeFactors a = primeFactors b

Tactic:
rw [← primeFactors_radical, h]

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
h : radical a = radical b
⊢ primeFactors (radical b) = primeFactors b
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
h : normalizedFactors a ≤ normalizedFactors b
hb₀ : b ≠ 0
ha₀ : a ≠ 0
⊢ radical a ∣ radical b

Tactic:
rw [radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors]

Goal state after:
case inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
h : normalizedFactors a ≤ normalizedFactors b
hb₀ : b ≠ 0
ha₀ : a ≠ 0
⊢ normalizedFactors a ⊆ normalizedFactors b
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: case neg
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
left
    -- use `abc_subcall` three times, using the symmetry in `a, b, c`
    refine ⟨?_, ?_, ?_⟩
    · rw [mul_rotate] at abc_dr_dvd_w ⊢
      apply abc_subcall wbc <;> assumption
    · rw [← mul_rotate] at abc_dr_dvd_w ⊢
      apply abc_subcall wca <;> assumption
    · apply abc_subcall wab <;> assumption

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

Goal state before:
pp: 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
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
have hCu := C_ne_zero.mpr hu

Goal state after:
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
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))

Tactic:
nth_rw 1 [range_comp]

Goal state after:
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ closure (ofReal '' range Rat.cast)
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 J : FractionalIdeal R⁰ K
⊢ ↑(Ideal.absNorm I.num * Ideal.absNorm J.num) / ↑|(Algebra.norm ℤ) ↑I.den * (Algebra.norm ℤ) ↑J.den| =
    ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den| * (↑(Ideal.absNorm J.num) / ↑|(Algebra.norm ℤ) ↑J.den|)

Tactic:
Nat.cast_mul,

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 J : FractionalIdeal R⁰ K
⊢ ↑(Ideal.absNorm I.num) * ↑(Ideal.absNorm J.num) / ↑|(Algebra.norm ℤ) ↑I.den * (Algebra.norm ℤ) ↑J.den| =
    ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den| * (↑(Ideal.absNorm J.num) / ↑|(Algebra.norm ℤ) ↑J.den|)
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: 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
⊢ a.natDegree = 0

Tactic:
rcases eq_or_ne (ringChar k) 0 with ch0 | chn0

Goal state after:
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
⊢ a.natDegree = 0

case inr
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
chn0 : ringChar k ≠ 0
⊢ a.natDegree = 0
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

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

Tactic:
Finset.card_eq_sum_ones,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∑ w, w.mult = ∑ x, 1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mp
x y z : ℤ
h : PythagoreanTriple x y z
k m n : ℤ
H : (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧ m.gcd n = 1
⊢ ∃ k m n,
    (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
      (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Tactic:
use k, m, n

Goal state after:
case h
x y z : ℤ
h : PythagoreanTriple x y z
k m n : ℤ
H : (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧ m.gcd n = 1
⊢ (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
    (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : ∀ (w : { w // w.IsComplex }), #{φ | mkComplex φ = w} = 2
⊢ #Finset.univ = 2 * nrComplexPlaces K

Tactic:
Finset.card_eq_sum_ones,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : ∀ (w : { w // w.IsComplex }), #{φ | mkComplex φ = w} = 2
⊢ ∑ x, 1 = 2 * nrComplexPlaces K
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : ∀ (w : { w // w.IsComplex }), #{φ | mkComplex φ = w} = 2
⊢ ∑ x, 2 = 2 * #Finset.univ

Tactic:
Finset.card_eq_sum_ones,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : ∀ (w : { w // w.IsComplex }), #{φ | mkComplex φ = w} = 2
⊢ ∑ x, 2 = 2 * ∑ x, 1
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 a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : (a' ^ n + b' ^ n) * d ^ n = c' ^ n * d ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
mul_left_inj' (pow_ne_zero n hd)

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
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:
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: case inr
F : Type u_1
inst✝⁴ : Field F
K : Type u_2
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst✝ : ∀ (i : ι), IsTotallyReal ↥(k i)
i : ι
⊢ IsTotallyReal ↥(⨆ i, k i)

Tactic:
rw [isTotallyReal_iff_le_maximalRealSubfield, iSup_le_iff]
    exact fun i ↦ IsTotallyReal.le_maximalRealSubfield (k i)

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

Goal state before:
pp: case inr
F : Type u_1
inst✝⁴ : Field F
K : Type u_2
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst✝ : ∀ (i : ι), IsTotallyReal ↥(k i)
i : ι
⊢ IsTotallyReal ↥(⨆ i, k i)

Tactic:
· rw [isTotallyReal_iff_le_maximalRealSubfield, iSup_le_iff]
    exact fun i ↦ IsTotallyReal.le_maximalRealSubfield (k i)

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
f : k →+* K
w : InfinitePlace K
hφ : w.IsReal
⊢ ComplexEmbedding.IsReal (w.embedding.comp f)

Tactic:
rw [← mk_embedding w, isReal_mk_iff] at hφ

Goal state after:
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
hφ : ComplexEmbedding.IsReal w.embedding
⊢ ComplexEmbedding.IsReal (w.embedding.comp f)
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 φ).re = Complex.re 0

Tactic:
rw [← embedding_mk_eq_of_isReal hφ, ← commMap_apply_of_isReal K x ⟨φ, hφ, rfl⟩]

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 φ
⊢ ((commMap K) x).1 ⟨InfinitePlace.mk φ, ⋯⟩ = Complex.re 0
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
hw : ComplexEmbedding.IsReal ((conjugate w.embedding).comp (algebraMap k K))
⊢ ComplexEmbedding.IsReal (conjugate w.embedding)

Tactic:
conjugate_comp,

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
hw : ComplexEmbedding.IsReal (conjugate (w.embedding.comp (algebraMap k K)))
⊢ ComplexEmbedding.IsReal (conjugate w.embedding)
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)
⊢ #({a ∉ {w | IsUnramified k w} | a.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w}) =
    #(MulAction.orbit Gal(K/k) w).toFinset

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)
⊢ #(MulAction.orbit Gal(K/k) w).toFinset = Nat.card Gal(K/k) / 2

Tactic:
· congr; ext w'
      rw [mem_filter, compl_filter, mem_filter_univ, @eq_comm _ (comap w' _), Set.mem_toFinset,
        mem_orbit_iff, and_iff_right_iff_imp]
      intro e; rwa [← isUnramifiedIn_comap, ← e]

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)
⊢ #(MulAction.orbit Gal(K/k) w).toFinset = Nat.card Gal(K/k) / 2
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₀, hw₀⟩).embedding ↑a).re| < 1 ∧
    |((↑⟨w₀, hw₀⟩).embedding ↑a).im| < ↑(if ↑⟨w₀, hw₀⟩ = w₀ then NNReal.sqrt B else 1) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ w ↑a < √(1 + ↑B ^ 2)

Tactic:
rw [if_pos rfl] at h_le₀
      dsimp only at h_le₀
      rw [h_eq, ← norm_embedding_eq, Real.lt_sqrt (norm_nonneg _), ← Complex.re_add_im
        (embedding w₀ _), Complex.norm_add_mul_I, Real.sq_sqrt (by positivity)]
      refine add_lt_add ?_ ?_
      · rw [← sq_abs, sq_lt_one_iff₀ (abs_nonneg _)]
        exact h_le₀.1
      · rw [sq_lt_sq, NNReal.abs_eq, ← NNReal.sq_sqrt B]
        exact h_le₀.2

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

Goal state before:
pp: case e_a.e_a.e_a.e_a.e_a
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
⊢ ↑(nrRealPlaces K) + ↑(2 * nrComplexPlaces K) - ↑(nrComplexPlaces K) - ↑(nrRealPlaces K) + ↑(nrComplexPlaces K) =
    2 * ↑(nrComplexPlaces K)

Tactic:
Nat.cast_mul,

Goal state after:
case e_a.e_a.e_a.e_a.e_a
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
⊢ ↑(nrRealPlaces K) + ↑2 * ↑(nrComplexPlaces K) - ↑(nrComplexPlaces K) - ↑(nrRealPlaces K) + ↑(nrComplexPlaces K) =
    2 * ↑(nrComplexPlaces 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)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B
⊢ ↑(finrank ℚ K) * ↑|(Algebra.norm ℚ) a| ^ (↑(finrank ℚ K))⁻¹ ≤ B

Tactic:
refine le_trans ?_ ((convexBodySum_mem K B).mp h_mem)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B
⊢ ↑(finrank ℚ K) * ↑|(Algebra.norm ℚ) a| ^ (↑(finrank ℚ K))⁻¹ ≤ ∑ w, ↑w.mult * ↑w a
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: case neg
A : Type u_1
B : Type u_6
inst✝²⁴ : CommRing A
inst✝²³ : CommRing B
inst✝²² : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst✝²¹ : CommRing Aₘ
inst✝²⁰ : CommRing Bₘ
inst✝¹⁹ : Algebra Aₘ Bₘ
inst✝¹⁸ : Algebra A Aₘ
inst✝¹⁷ : Algebra B Bₘ
inst✝¹⁶ : Algebra A Bₘ
inst✝¹⁵ : IsScalarTower A Aₘ Bₘ
inst✝¹⁴ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹³ : IsLocalization M Aₘ
inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDomain B
inst✝⁸ : IsIntegrallyClosed B
inst✝⁷ : Module.Finite A B
inst✝⁶ : IsTorsionFree A B
inst✝⁵ : IsDomain Aₘ
inst✝⁴ : IsIntegrallyClosed Aₘ
inst✝³ : IsDomain Bₘ
inst✝² : IsIntegrallyClosed Bₘ
inst✝¹ : IsTorsionFree Aₘ Bₘ
inst✝ : Module.Finite Aₘ Bₘ
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
this✝³ : IsIntegralClosure B A L
this✝² : Algebra.IsAlgebraic (FractionRing A) (FractionRing B)
this✝¹ : IsLocalization (algebraMapSubmonoid B A⁰) L
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝ : Algebra Aₘ K := f.toAlgebra
this : IsScalarTower A Aₘ K
⊢ (algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)

Tactic:
let := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K

Goal state after:
case neg
A : Type u_1
B : Type u_6
inst✝²⁴ : CommRing A
inst✝²³ : CommRing B
inst✝²² : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst✝²¹ : CommRing Aₘ
inst✝²⁰ : CommRing Bₘ
inst✝¹⁹ : Algebra Aₘ Bₘ
inst✝¹⁸ : Algebra A Aₘ
inst✝¹⁷ : Algebra B Bₘ
inst✝¹⁶ : Algebra A Bₘ
inst✝¹⁵ : IsScalarTower A Aₘ Bₘ
inst✝¹⁴ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹³ : IsLocalization M Aₘ
inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDomain B
inst✝⁸ : IsIntegrallyClosed B
inst✝⁷ : Module.Finite A B
inst✝⁶ : IsTorsionFree A B
inst✝⁵ : IsDomain Aₘ
inst✝⁴ : IsIntegrallyClosed Aₘ
inst✝³ : IsDomain Bₘ
inst✝² : IsIntegrallyClosed Bₘ
inst✝¹ : IsTorsionFree Aₘ Bₘ
inst✝ : Module.Finite Aₘ Bₘ
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
this✝⁴ : IsIntegralClosure B A L
this✝³ : Algebra.IsAlgebraic (FractionRing A) (FractionRing B)
this✝² : IsLocalization (algebraMapSubmonoid B A⁰) L
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝¹ : Algebra Aₘ K := f.toAlgebra
this✝ : IsScalarTower A Aₘ K
this : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K
⊢ (algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

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

Tactic:
simp_rw +singlePass [hA, negAt_apply_norm_isReal, negAt_apply_snd]
      rwa [← hA]

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

Goal state before:
pp: case neg
A : Type u_1
B : Type u_6
inst✝²⁵ : CommRing A
inst✝²⁴ : CommRing B
inst✝²³ : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst✝²² : CommRing Aₘ
inst✝²¹ : CommRing Bₘ
inst✝²⁰ : Algebra Aₘ Bₘ
inst✝¹⁹ : Algebra A Aₘ
inst✝¹⁸ : Algebra B Bₘ
inst✝¹⁷ : Algebra A Bₘ
inst✝¹⁶ : IsScalarTower A Aₘ Bₘ
inst✝¹⁵ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹⁴ : IsLocalization M Aₘ
inst✝¹³ : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝¹² : IsIntegrallyClosed A
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsDomain B
inst✝⁹ : IsIntegrallyClosed B
inst✝⁸ : Algebra.IsIntegral A B
inst✝⁷ : IsTorsionFree A B
inst✝⁶ : IsDomain Aₘ
inst✝⁵ : IsIntegrallyClosed Aₘ
inst✝⁴ : IsDomain Bₘ
inst✝³ : IsIntegrallyClosed Bₘ
inst✝² : IsTorsionFree Aₘ Bₘ
inst✝¹ : Algebra.IsIntegral Aₘ Bₘ
inst✝ : FiniteDimensional (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝ : Algebra Aₘ K := f.toAlgebra
this : IsScalarTower A Aₘ K
⊢ (algebraMap A Aₘ) ((intNorm A B) x) = (intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)

Tactic:
let := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K

Goal state after:
case neg
A : Type u_1
B : Type u_6
inst✝²⁵ : CommRing A
inst✝²⁴ : CommRing B
inst✝²³ : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst✝²² : CommRing Aₘ
inst✝²¹ : CommRing Bₘ
inst✝²⁰ : Algebra Aₘ Bₘ
inst✝¹⁹ : Algebra A Aₘ
inst✝¹⁸ : Algebra B Bₘ
inst✝¹⁷ : Algebra A Bₘ
inst✝¹⁶ : IsScalarTower A Aₘ Bₘ
inst✝¹⁵ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹⁴ : IsLocalization M Aₘ
inst✝¹³ : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝¹² : IsIntegrallyClosed A
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsDomain B
inst✝⁹ : IsIntegrallyClosed B
inst✝⁸ : Algebra.IsIntegral A B
inst✝⁷ : IsTorsionFree A B
inst✝⁶ : IsDomain Aₘ
inst✝⁵ : IsIntegrallyClosed Aₘ
inst✝⁴ : IsDomain Bₘ
inst✝³ : IsIntegrallyClosed Bₘ
inst✝² : IsTorsionFree Aₘ Bₘ
inst✝¹ : Algebra.IsIntegral Aₘ Bₘ
inst✝ : FiniteDimensional (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝¹ : Algebra Aₘ K := f.toAlgebra
this✝ : IsScalarTower A Aₘ K
this : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K
⊢ (algebraMap A Aₘ) ((intNorm A B) x) = (intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Algebra A B
p : Ideal A
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : MulSemiringAction G B
inst✝¹¹ : SMulCommClass G A B
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : IsFractionRing A K
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
Q : ↑(p.primesOver B)
⊢ ↑(1 • Q) = ↑Q

Tactic:
change map _ Q.1 = Q.1

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Algebra A B
p : Ideal A
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : MulSemiringAction G B
inst✝¹¹ : SMulCommClass G A B
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : IsFractionRing A K
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
Q : ↑(p.primesOver B)
⊢ map ((galRestrict A K L B) 1) ↑Q = ↑Q