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

Goal state before:
pp: case neg.refine_2
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 (c * a * b) ∣ w
hw : ¬w = 0
⊢ b.natDegree + 1 ≤ (radical (c * a * b)).natDegree

Tactic:
apply abc_subcall wca

Goal state after:
case neg.refine_2.ha
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] := ⋯
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 (c * a * b) ∣ w
hw : ¬w = 0
⊢ c ≠ 0

case neg.refine_2.hb
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] := ⋯
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 (c * a * b) ∣ w
hw : ¬w = 0
⊢ a ≠ 0

case neg.refine_2.hc
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] := ⋯
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 (c * a * b) ∣ w
hw : ¬w = 0
⊢ b ≠ 0

case neg.refine_2.abc_dr_dvd_w
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] := ⋯
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 (c * a * b) ∣ w
hw : ¬w = 0
⊢ divRadical (c * a * b) ∣ w

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] := ⋯
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 (c * a * b) ∣ w
hw : ¬w = 0
⊢ w ≠ 0
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: 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 ⋯)
⊢ Filter.comap (fun x ↦ (ι x.1, ι x.2)) (uniformity ↥K.topologicalClosure) = uniformity ↥K

Tactic:
by
      rw [uniformity_subtype, uniformity_subtype, Filter.comap_comap]
      congr

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✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
⊢ |(Basis.localizationLocalization ℚ ℤ⁰ K b).det (Subtype.val ∘ ⇑bI)| = absNorm I

Tactic:
have := IsFractionRing.nontrivial R K

Goal state after:
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
⊢ |(Basis.localizationLocalization ℚ ℤ⁰ K b).det (Subtype.val ∘ ⇑bI)| = absNorm I
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φ
x y : ↥φ.range
this : ‖φ (ι.symm (x - y))‖ = ‖ψ (ι.symm (x - y))‖
⊢ ‖ψ (ι.symm (x - y))‖ = dist x y

Tactic:
rw [← this, ← RingEquiv.ofLeftInverse_apply hiφ _, RingEquiv.apply_symm_apply ι _,
          dist_eq_norm]

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φ
x y : ↥φ.range
this : ‖φ (ι.symm (x - y))‖ = ‖ψ (ι.symm (x - y))‖
⊢ ‖↑(x - y)‖ = ‖x - y‖
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
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
x✝ : K
⊢ x✝ ∈ d • ↑(spanSingleton R⁰ x) ↔ x✝ ∈ Submodule.map (Algebra.linearMap R K) (Ideal.span {r})

Tactic:
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 mpr
x y z : ℤ
⊢ (∃ 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))) →
    PythagoreanTriple x y z

Tactic:
rintro ⟨k, m, n, ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, rfl | rfl⟩

Goal state after:
case mpr.inl.inl
k m n : ℤ
⊢ PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) (k * (m ^ 2 + n ^ 2))

case mpr.inl.inr
k m n : ℤ
⊢ PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) (-k * (m ^ 2 + n ^ 2))

case mpr.inr.inl
k m n : ℤ
⊢ PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) (k * (m ^ 2 + n ^ 2))

case mpr.inr.inr
k m n : ℤ
⊢ PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) (-k * (m ^ 2 + n ^ 2))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v w : InfinitePlace K
h✝ : (↑w).IsEquiv ↑v
t : ℝ
left✝ : 0 < t
h : (fun x ↦ ↑w x ^ t) = ⇑↑v
k : K
⊢ w k = v k

Tactic:
by simpa [eq_one_of_rpow_eq h, ext, coe_apply] using funext_iff.1 h k

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
⊢ (↑v).IsNontrivial

Tactic:
obtain ⟨n, hn⟩ := exists_gt (1 : ℕ)
  exact ⟨n, v.pos_iff.1 <| zero_lt_one.trans (by simpa), by simp [← coe_apply]; grind⟩

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

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
hb : b ≠ 0
hc : c ≠ 0
a' b' : k[X]
d : k[X] := gcd a b
ha : d * a' ≠ 0
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
c' : k[X]
eq_c : c = d * c'
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
mul_ne_zero_iff

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
hb : b ≠ 0
hc : c ≠ 0
a' b' : k[X]
d : k[X] := gcd a b
ha : d ≠ 0 ∧ a' ≠ 0
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
c' : k[X]
eq_c : c = d * c'
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ 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
a b c : k[X]
hc : c ≠ 0
a' b' : k[X]
d : k[X] := gcd a b
hb : d * b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
c' : k[X]
eq_c : c = d * c'
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
mul_ne_zero_iff

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
hc : c ≠ 0
a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
c' : k[X]
eq_c : c = d * c'
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ 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
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
c' : k[X]
hc : d * c' ≠ 0
eq_c : c = d * c'
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
mul_ne_zero_iff

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
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
c' : k[X]
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = d * c'
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
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 : IsRamified k w
⊢ (w.comap (algebraMap k K)).embedding = (conjugate w.embedding).comp (algebraMap k K)

Tactic:
rw [← ComplexEmbedding.isReal_iff.1 <| isReal_iff.1 ((isRamified_iff.1 h).2)]

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 : IsRamified k w
⊢ conjugate (w.comap (algebraMap k K)).embedding = (conjugate w.embedding).comp (algebraMap k K)
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 : IsRamified k w
⊢ (w.comap (algebraMap k K)).embedding = (conjugate w.embedding).comp (algebraMap k K)

Tactic:
rw [← ComplexEmbedding.isReal_iff.1 <| isReal_iff.1 ((isRamified_iff.1 h).2)]
  simp [conjugate_comp, comap_embedding_of_isReal _ ((isRamified_iff.1 h).2)]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (matrixToStdBasis K).det = ∏ _k, (2⁻¹ • !![1, 1; -I, I]).det

Tactic:
rw [matrixToStdBasis, det_fromBlocks_zero₂₁, det_diagonal, prod_const_one, one_mul,
          det_reindex_self, det_blockDiagonal]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ZLattice.covolume (mixedEmbedding.integerLattice K) volume = 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|

Tactic:
ZLattice.covolume_eq_measure_fundamentalDomain _ _ (fundamentalDomain_integerLattice K),

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ volume.real (fundamentalDomain (latticeBasis K)) = 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)

Tactic:
have := LinearIndependent.map (LinearIndependent.restrict_scalars
      (by { simpa only [Complex.real_smul, mul_one] using Complex.ofReal_injective })
      (canonicalEmbedding.latticeBasis K).linearIndependent)
      (disjoint_span_commMap_ker K)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : LinearIndependent ℝ (⇑(commMap K) ∘ ⇑(canonicalEmbedding.latticeBasis K))
⊢ Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
⊢ Disjoint (ramifiedPlacesOver L v) (unramifiedPlacesOver L v)

Tactic:
grind [ramifiedPlacesOver, unramifiedPlacesOver]

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

Goal state before:
pp: case intro
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Finite G
inst✝¹⁵ : Group G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝¹² : Q.LiesOver P
inst✝¹¹ : P.IsPrime
inst✝¹⁰ : Q.IsPrime
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra (A ⧸ P) K
inst✝⁵ : IsFractionRing (A ⧸ P) K
inst✝⁴ : Algebra (B ⧸ Q) L
inst✝³ : IsFractionRing (B ⧸ Q) L
inst✝² : Algebra (A ⧸ P) L
inst✝¹ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝ : IsScalarTower (A ⧸ P) K L
this✝ : Algebra.IsIntegral A B
this : Algebra.IsAlgebraic K L
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
a : A
ha : (algebraMap A (A ⧸ P)) a ≠ 0
b : B
h : (algebraMap A (A ⧸ P)) a • x = y * (algebraMap B (B ⧸ Q)) b
val✝ : Fintype G
p : A[X]
hp : Polynomial.map (algebraMap A B) p = MulSemiringAction.charpoly G b
h_monic : p.Monic
h_eval : (aeval b) p = 0
q : A[X] := p.comp (C a * X)
⊢ (Polynomial.map (algebraMap K L) (minpoly K ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y))).Splits

Tactic:
let d := (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y

Goal state after:
case intro
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Finite G
inst✝¹⁵ : Group G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝¹² : Q.LiesOver P
inst✝¹¹ : P.IsPrime
inst✝¹⁰ : Q.IsPrime
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra (A ⧸ P) K
inst✝⁵ : IsFractionRing (A ⧸ P) K
inst✝⁴ : Algebra (B ⧸ Q) L
inst✝³ : IsFractionRing (B ⧸ Q) L
inst✝² : Algebra (A ⧸ P) L
inst✝¹ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝ : IsScalarTower (A ⧸ P) K L
this✝ : Algebra.IsIntegral A B
this : Algebra.IsAlgebraic K L
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
a : A
ha : (algebraMap A (A ⧸ P)) a ≠ 0
b : B
h : (algebraMap A (A ⧸ P)) a • x = y * (algebraMap B (B ⧸ Q)) b
val✝ : Fintype G
p : A[X]
hp : Polynomial.map (algebraMap A B) p = MulSemiringAction.charpoly G b
h_monic : p.Monic
h_eval : (aeval b) p = 0
q : A[X] := p.comp (C a * X)
d : L := (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
⊢ (Polynomial.map (algebraMap K L) (minpoly K ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y))).Splits
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ := fun n ↦ ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n m : ℕ
hmn✝ : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + 1 / ↑m) ^ (2 * m)
⊢ 4 / 9 * (3 * π / 4) ^ (m + 1) ≤ a (m + 1)

Tactic:
convert_to _ ≤ (a m) * (1 + 1 / m : ℝ) ^ (2 * m) / (4 / π)
        · simp_rw [a, add_mul, one_mul, pow_succ, Nat.factorial_succ]
          field_simp
          simp [field, div_pow]
          ring
        · rw [_root_.le_div_iff₀ (by positivity), pow_succ]
          convert! (mul_le_mul h_m this (by positivity) (by positivity)) using 1
          field

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
⊢ minkowskiBound K 1 < ↑(boundOfDiscBdd N)

Tactic:
have : boundOfDiscBdd N - 1 < boundOfDiscBdd N := by
    simp_rw [boundOfDiscBdd, add_tsub_cancel_right, lt_add_iff_pos_right, zero_lt_one]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ minkowskiBound K 1 < ↑(boundOfDiscBdd N)
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✝² : FaithfulSMul R S
inst✝¹ : CharZero R
inst✝ : Algebra.IsIntegral R S
P : Ideal S
⊢ ∀ (x : P.IsPrime), P.LiesOver ⊥ → IsUnramifiedAt R P

Tactic:
_

Goal state after:
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✝² : FaithfulSMul R S
inst✝¹ : CharZero R
inst✝ : Algebra.IsIntegral R S
P : Ideal S
x✝ : P.IsPrime
⊢ P.LiesOver ⊥ → IsUnramifiedAt R P
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
I J : FractionalIdeal M K
x✝ : L
h : x✝ ∈ ⇑(IsLocalization.map L f hf) '' ↑(I * J)
⊢ x✝ ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

Tactic:
rcases h with ⟨x, hx, 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
I J : FractionalIdeal M K
x : K
hx : x ∈ ↑(I * J)
⊢ (IsLocalization.map L f hf) x ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg.refine_1
R : Type u_1
inst✝¹⁴ : CommRing R
inst✝¹³ : IsDomain R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : IsIntegrallyClosed R
inst✝⁹ : IsIntegrallyClosed S
inst✝⁸ : Algebra R S
inst✝⁷ : Module.Finite R S
inst✝⁶ : IsTorsionFree R S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : IsDedekindDomain S
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : PerfectField (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
a✝ : Ideal S
⊢ ∀ (b : Ideal S),
    absNorm ((relNorm R) a✝) = absNorm a✝ →
      absNorm ((relNorm R) b) = absNorm b → absNorm ((relNorm R) (a✝ * b)) = absNorm (a✝ * b)

Tactic:
_

Goal state after:
case neg.refine_1
R : Type u_1
inst✝¹⁴ : CommRing R
inst✝¹³ : IsDomain R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : IsIntegrallyClosed R
inst✝⁹ : IsIntegrallyClosed S
inst✝⁸ : Algebra R S
inst✝⁷ : Module.Finite R S
inst✝⁶ : IsTorsionFree R S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : IsDedekindDomain S
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : PerfectField (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
a✝ b✝ : Ideal S
⊢ absNorm ((relNorm R) a✝) = absNorm a✝ →
    absNorm ((relNorm R) b✝) = absNorm b✝ → absNorm ((relNorm R) (a✝ * b✝)) = absNorm (a✝ * b✝)
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Field L
inst✝¹³ : Algebra A K
inst✝¹² : Algebra B L
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : IsScalarTower A B L
inst✝⁶ : IsFractionRing A K
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsIntegralClosure B A L
inst✝² : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral A (b i)
a x : L
ha : a ∈ I
hx : x ∈ Iᵛ
hinv : IsUnit (traceMatrix K ⇑b).det
H : ((traceMatrix K ⇑b).cramer fun i ↦ (Algebra.trace K L) (x * a * b i)) = (traceMatrix K ⇑b).det • b.equivFun (x * a)
this : Function.Injective (traceMatrix K ⇑b).mulVec
i : ι
⊢ i ∈ Finset.univ → IsIntegral A (b.equivFun (discr K ⇑b • a * x) i • b i)

Tactic:
_

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Field L
inst✝¹³ : Algebra A K
inst✝¹² : Algebra B L
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : IsScalarTower A B L
inst✝⁶ : IsFractionRing A K
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsIntegralClosure B A L
inst✝² : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral A (b i)
a x : L
ha : a ∈ I
hx : x ∈ Iᵛ
hinv : IsUnit (traceMatrix K ⇑b).det
H : ((traceMatrix K ⇑b).cramer fun i ↦ (Algebra.trace K L) (x * a * b i)) = (traceMatrix K ⇑b).det • b.equivFun (x * a)
this : Function.Injective (traceMatrix K ⇑b).mulVec
i : ι
a✝ : i ∈ Finset.univ
⊢ IsIntegral A (b.equivFun (discr K ⇑b • a * x) i • b i)