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

Goal state before:
pp: case refine_2.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
x : mixedSpace K
h : x ∈ A
hx : ∃ a, x.1 a = 0
⊢ (∃ i, x ∈ ⇑(negAt i) '' plusPart A) ∨ x ∈ A ∧ ∃ i, x ∈ {x | x.1 i = 0}

pp: case refine_2.inr
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
x : mixedSpace K
h : x ∈ A
hx : ∀ (a : { w // w.IsReal }), ¬x.1 a = 0
⊢ (∃ i, x ∈ ⇑(negAt i) '' plusPart A) ∨ x ∈ A ∧ ∃ i, x ∈ {x | x.1 i = 0}

Tactic:
· exact Or.inr ⟨h, hx⟩

Goal state after:
case refine_2.inr
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
x : mixedSpace K
h : x ∈ A
hx : ∀ (a : { w // w.IsReal }), ¬x.1 a = 0
⊢ (∃ i, x ∈ ⇑(negAt i) '' plusPart A) ∨ x ∈ A ∧ ∃ i, x ∈ {x | x.1 i = 0}
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
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

Tactic:
by
  have h_nz : N ≠ 0 := by
    refine fun h ↦ discr_ne_zero K ?_
    rwa [h, Nat.cast_zero, abs_nonpos_iff] at hK
  have h₂ : 1 < 3 * π / 4 := by
    rw [_root_.lt_div_iff₀ (by positivity), ← _root_.div_lt_iff₀' (by positivity), one_mul]
    linarith [Real.pi_gt_three]
  obtain h | h := lt_or_ge 1 (finrank ℚ K)
  · apply le_max_of_le_right
    rw [Nat.le_floor_iff]
    · have h := le_trans (abs_discr_ge h) (Int.cast_le.mpr hK)
      contrapose! h
      rw [← Real.rpow_natCast]
      rw [Real.log_div_log] at h
      refine lt_of_le_of_lt ?_ (mul_lt_mul_of_pos_left
        (Real.rpow_lt_rpow_of_exponent_lt h₂ h) (by positivity : (0 : ℝ) < 4 / 9))
      rw [Real.rpow_logb (lt_trans zero_lt_one h₂) (ne_of_gt h₂) (by positivity), ← mul_assoc,
            ← inv_div, inv_mul_cancel₀ (by simp), one_mul, Int.cast_natCast]
    · refine div_nonneg (Real.log_nonneg ?_) (Real.log_nonneg (le_of_lt h₂))
      rw [mul_comm, ← mul_div_assoc, _root_.le_div_iff₀ (by positivity), one_mul,
        ← _root_.div_le_iff₀ (by positivity)]
      exact le_trans (by norm_num) (Nat.one_le_cast.mpr (Nat.one_le_iff_ne_zero.mpr h_nz))
  · exact le_max_of_le_left h

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

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : Group G
inst✝⁶ : MulSemiringAction G S
inst✝⁵ : IsGaloisGroup G R S
inst✝⁴ : Finite G
p : Ideal R
inst✝³ : p.IsPrime
P : Ideal S
inst✝² : P.LiesOver p
inst✝¹ : P.IsPrime
inst✝ : PerfectField p.ResidueField
⊢ (MulAction.orbit G P).ncard * Nat.card ↥(MulAction.stabilizer G P) = Nat.card G

Tactic:
simpa using Nat.card_congr (MulAction.orbitProdStabilizerEquivGroup G P)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
B : ℕ
h✝ : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : Nat.card (R ⧸ I) ≤ B ∧ I ∉ {⊥}
this✝ : Finite (R ⧸ I)
this : Fintype (R ⧸ I)
⊢ (Finset.image (⇑(Ideal.Quotient.mk I)) s).card < s.card

Tactic:
Finset.card_le_univ,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
B : ℕ
h✝ : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : Nat.card (R ⧸ I) ≤ B ∧ I ∉ {⊥}
this✝ : Finite (R ⧸ I)
this : Fintype (R ⧸ I)
⊢ Fintype.card (R ⧸ I) < s.card
Module: Mathlib.NumberTheory.RamificationInertia.Unramified

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing T
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S T
inst✝⁸ : Algebra R T
inst✝⁷ : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst✝⁶ : P.LiesOver p
inst✝⁵ : p.IsPrime
inst✝⁴ : P.IsPrime
inst✝³ : IsUnramifiedAt R P
inst✝² : EssFiniteType R S
inst✝¹ : EssFiniteType R T
inst✝ : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this✝⁴ : P.LiesOver p₀
this✝³ : Algebra (Localization.AtPrime p₀) (Localization.AtPrime p) := Localization.AtPrime.algebraOfLiesOver p₀ p
this✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
this✝¹ : Algebra (Localization.AtPrime p₀) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this✝ : EssFiniteType S T
this : IsNoetherianRing T
h₁ : Algebra.IsSeparable p₀.ResidueField P.ResidueField
h₂ : Ideal.map (algebraMap R (Localization.AtPrime P)) p₀ = maximalIdeal (Localization.AtPrime P)
hp : p = ⊥
⊢ Ideal.map (algebraMap R (Localization.AtPrime p)) p₀ = maximalIdeal (Localization.AtPrime p)

Tactic:
have : p₀.map (algebraMap R S) = p := by
      subst hp
      exact le_bot_iff.mp (Ideal.map_comap_le)

Goal state after:
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing T
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S T
inst✝⁸ : Algebra R T
inst✝⁷ : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst✝⁶ : P.LiesOver p
inst✝⁵ : p.IsPrime
inst✝⁴ : P.IsPrime
inst✝³ : IsUnramifiedAt R P
inst✝² : EssFiniteType R S
inst✝¹ : EssFiniteType R T
inst✝ : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this✝⁵ : P.LiesOver p₀
this✝⁴ : Algebra (Localization.AtPrime p₀) (Localization.AtPrime p) := Localization.AtPrime.algebraOfLiesOver p₀ p
this✝³ : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
this✝² : Algebra (Localization.AtPrime p₀) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this✝¹ : EssFiniteType S T
this✝ : IsNoetherianRing T
h₁ : Algebra.IsSeparable p₀.ResidueField P.ResidueField
h₂ : Ideal.map (algebraMap R (Localization.AtPrime P)) p₀ = maximalIdeal (Localization.AtPrime P)
hp : p = ⊥
this : Ideal.map (algebraMap R S) p₀ = p
⊢ Ideal.map (algebraMap R (Localization.AtPrime p)) p₀ = maximalIdeal (Localization.AtPrime p)
Module: Mathlib.RingTheory.Trace.Quotient

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Free R S
inst✝¹ : Module.Finite R S
inst✝ : IsLocalRing R
x : S
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((trace R S) x)

Tactic:
let ι := Module.Free.ChooseBasisIndex R S
  let b : Module.Basis ι R S := Module.Free.chooseBasis R S
  rw [trace_eq_matrix_trace b, trace_eq_matrix_trace (basisQuotient b), AddMonoidHom.map_trace]
  congr 1
  ext i j
  simp only [leftMulMatrix_apply, coe_lmul_eq_mul, LinearMap.toMatrix_apply,
    basisQuotient_apply, LinearMap.mul_apply', Matrix.map_apply, ← map_mul,
    basisQuotient_repr]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
inst✝ : Finite (ResidueField R)
I : Ideal R
n : ℕ
hn : p ^ n ≤ I
⊢ Finite (R ⧸ I)

Tactic:
have : Finite (R ⧸ maximalIdeal R) := ‹_›

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
inst✝ : Finite (ResidueField R)
I : Ideal R
n : ℕ
hn : p ^ n ≤ I
this : Finite (R ⧸ p)
⊢ Finite (R ⧸ I)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).Monic

Tactic:
rw [show (X + 1 : ℤ[X]) = X + C 1 by simp]
    refine (cyclotomic.monic _ ℤ).comp (monic_X_add_C 1) fun h => ?_
    rw [natDegree_X_add_C] at h
    exact zero_ne_one h.symm

Goal state after:
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
x : B
⊢ IsIntegral A ((Algebra.linearMap B L) x)

Tactic:
rw [IsIntegralClosure.isIntegral_iff (A := B)]

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
x : B
⊢ ∃ y, (algebraMap B L) y = (Algebra.linearMap B L) x
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case h
R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : ℕ → R
hg : ∀ k ∈ range (j + 1), Q.coeff k • B.gen ^ k = (algebraMap R L) p * g k • B.gen ^ k
f : ℕ → L
hf :
  ∀ (i : ℕ),
    (Polynomial.map (algebraMap R L) (minpoly R B.gen)).natDegree ≤ i →
      f i ∈ R[B.gen] ∧ (algebraMap R L) p * f i = B.gen ^ i
k : ℕ
hk : k ∈ (range (Q.natDegree - j)).erase 0
⊢ 1 ≤ k

Tactic:
· refine one_le_iff_ne_zero.2 fun h => ?_
        rw [h] at hk
        simp at hk

Goal state after:
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✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : y ∈ Submodule.restrictScalars A ↑I
⊢ IsIntegral A (((lmul K L).toLinearMap x) y)

Tactic:
rw [IsIntegralClosure.isIntegral_iff (A := B)]

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✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : y ∈ Submodule.restrictScalars A ↑I
⊢ ∃ y_1, (algebraMap B L) y_1 = ((lmul K L).toLinearMap x) y
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✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : ¬I = 0
⊢ 0 < dual A K I

Tactic:
by simpa [pos_iff_ne_zero]

Goal state after:
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✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : ¬I = 0
⊢ 0 < I

Tactic:
by simpa [pos_iff_ne_zero]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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✝²⁷ : IsDomain A
inst✝²⁶ : IsFractionRing A K
inst✝²⁵ : FiniteDimensional K L
inst✝²⁴ : Algebra.IsSeparable K L
inst✝²³ : IsIntegralClosure B A L
inst✝²² : IsFractionRing B L
inst✝²¹ : IsIntegrallyClosed A
inst✝²⁰ : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst✝¹⁹ : CommRing C
inst✝¹⁸ : IsDedekindDomain C
inst✝¹⁷ : Field M
inst✝¹⁶ : Algebra C M
inst✝¹⁵ : IsFractionRing C M
inst✝¹⁴ : Algebra A C
inst✝¹³ : Algebra B C
inst✝¹² : Algebra A M
inst✝¹¹ : Algebra B M
inst✝¹⁰ : Algebra K M
inst✝⁹ : Algebra L M
inst✝⁸ : IsScalarTower A C M
inst✝⁷ : IsScalarTower A K M
inst✝⁶ : IsScalarTower B C M
inst✝⁵ : IsScalarTower B L M
inst✝⁴ : IsScalarTower K L M
inst✝³ : IsIntegralClosure C A M
inst✝² : FiniteDimensional K M
inst✝¹ : FiniteDimensional L M
inst✝ : Algebra.IsSeparable K M
x : M
hx : x ∈ dual A K 1
⊢ (Algebra.trace L M) x ∈ dual A K 1

Tactic:
simp only [ne_eq, one_ne_zero, not_false_eq_true, mem_dual, mem_one_iff, traceForm_apply,
    RingHom.mem_range, forall_exists_index, forall_apply_eq_imp_iff,
    mul_comm _ (algebraMap _ _ _), ← Algebra.smul_def, ← LinearMap.map_smul_of_tower,
    Algebra.trace_trace] at hx ⊢

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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✝²⁷ : IsDomain A
inst✝²⁶ : IsFractionRing A K
inst✝²⁵ : FiniteDimensional K L
inst✝²⁴ : Algebra.IsSeparable K L
inst✝²³ : IsIntegralClosure B A L
inst✝²² : IsFractionRing B L
inst✝²¹ : IsIntegrallyClosed A
inst✝²⁰ : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst✝¹⁹ : CommRing C
inst✝¹⁸ : IsDedekindDomain C
inst✝¹⁷ : Field M
inst✝¹⁶ : Algebra C M
inst✝¹⁵ : IsFractionRing C M
inst✝¹⁴ : Algebra A C
inst✝¹³ : Algebra B C
inst✝¹² : Algebra A M
inst✝¹¹ : Algebra B M
inst✝¹⁰ : Algebra K M
inst✝⁹ : Algebra L M
inst✝⁸ : IsScalarTower A C M
inst✝⁷ : IsScalarTower A K M
inst✝⁶ : IsScalarTower B C M
inst✝⁵ : IsScalarTower B L M
inst✝⁴ : IsScalarTower K L M
inst✝³ : IsIntegralClosure C A M
inst✝² : FiniteDimensional K M
inst✝¹ : FiniteDimensional L M
inst✝ : Algebra.IsSeparable K M
x : M
hx : ∀ (a : C), ∃ x_1, (algebraMap A K) x_1 = (Algebra.trace K M) (a • x)
⊢ ∀ (a : B), ∃ x_1, (algebraMap A K) x_1 = (Algebra.trace K M) (a • x)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case h
R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : ℕ → R
hg : ∀ k ∈ range (j + 1), Q.coeff k • B.gen ^ k = (algebraMap R L) p * g k • B.gen ^ k
f : ℕ → L
hf :
  ∀ (i : ℕ),
    (Polynomial.map (algebraMap R L) (minpoly R B.gen)).natDegree ≤ i →
      f i ∈ R[B.gen] ∧ (algebraMap R L) p * f i = B.gen ^ i
hf₁ :
  ∀ k ∈ (range (Q.natDegree - j)).erase 0,
    Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
      (algebraMap R L) p * Q.coeff (j + 1 + k) • f (k + P.natDegree - 1)
hQ :
  (Algebra.norm K) ((algebraMap R L) (Q.coeff (j + 1)) * B.gen ^ (j + 1 + (P.natDegree - (j + 2)))) =
    (Algebra.norm K)
      (p • z * B.gen ^ (P.natDegree - (j + 2)) -
        (algebraMap R L) p *
          (∑ i ∈ (range (Q.natDegree - j)).erase 0, Q.coeff (j + 1 + i) • f (i + P.natDegree - 1) +
            ∑ i ∈ range (j + 1), g i • B.gen ^ i * B.gen ^ (P.natDegree - (j + 2))))
k : ℕ
hk : k ∈ (range (Q.natDegree - j)).erase 0
⊢ 1 ≤ k

Tactic:
· refine one_le_iff_ne_zero.2 fun h => ?_
        rw [h] at hk
        simp at hk

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
x : 𝓞 K
hx : x ≠ 0
hx' : (algebraMap (𝓞 K) K) x ≠ 0
f : InfinitePlace K → ℝ≥0 := fun w ↦ ⟨w ↑x / 2, ⋯⟩
w✝ : InfinitePlace K
a✝ : w✝ ≠ w₁
⊢ f w✝ ≠ 0

Tactic:
rw [ne_eq, Nonneg.mk_eq_zero, div_eq_zero_iff, map_eq_zero, not_or]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
x : 𝓞 K
hx : x ≠ 0
hx' : (algebraMap (𝓞 K) K) x ≠ 0
f : InfinitePlace K → ℝ≥0 := fun w ↦ ⟨w ↑x / 2, ⋯⟩
w✝ : InfinitePlace K
a✝ : w✝ ≠ w₁
⊢ ¬↑x = 0 ∧ ¬2 = 0
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
ha : ¬↑a = 0
⊢ ↑1 = ↑a ^ (2 / 2)

Tactic:
revert ha

Goal state after:
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬↑a = 0 → ↑1 = ↑a ^ (2 / 2)
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case pos.inr
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : a ^ 3 + b ^ 3 + (-c) ^ 3 = 0
h3c : 3 ∣ c
⊢ False

Tactic:
rw [add_comm _ ((-c) ^ 3), ← add_assoc] at hF

Goal state after:
case pos.inr
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : (-c) ^ 3 + a ^ 3 + b ^ 3 = 0
h3c : 3 ∣ c
⊢ False
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: n : ℕ
h₁ : 1 < n
h₂ : ¬Prime n
⊢ n ∣ 1 ^ (n - 1) - 1

Tactic:
exact show 0 = 1 ^ (n - 1) - 1 by simp ▸ dvd_zero n

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (2 ^ n - 1)
han1 : 1 < 2 ^ n
ha1 : 1 < 2
ha0 : 0 < 2
d : ℕ
hdn : d ∣ n
⊢ d = 1 ∨ d = n

Tactic:
have hinj : ∀ x y, 2 ^ x - 1 = 2 ^ y - 1 → x = y :=
    fun x y h ↦ Nat.pow_right_injective le_rfl (sub_one_cancel (pow_pos ha0 x) (pow_pos ha0 y) h)

Goal state after:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (2 ^ n - 1)
han1 : 1 < 2 ^ n
ha1 : 1 < 2
ha0 : 0 < 2
d : ℕ
hdn : d ∣ n
hinj : ∀ (x y : ℕ), 2 ^ x - 1 = 2 ^ y - 1 → x = y
⊢ d = 1 ∨ d = n
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: case inl
n : ℕ
h : n ∈ maximalIdeal ℕ
lt : n < 1
⊢ n ∈ span {2, 3}

Tactic:
obtain rfl := lt_one_iff.mp lt

Goal state after:
case inl
h : 0 ∈ maximalIdeal ℕ
lt : 0 < 1
⊢ 0 ∈ span {2, 3}
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: ⊢ ringKrullDim ℕ = 2

Tactic:
refine le_antisymm (iSup_le fun s ↦ le_of_not_gt fun hs ↦ ?_) ?_
  · replace hs : 2 < s.length := ENat.natCast_lt_natCast.mp (WithBot.coe_lt_coe.mp hs)
    let s := s.take ⟨3, by lia⟩
    have : NeZero s.length := ⟨three_ne_zero⟩
    have h1 : ⊥ < (s 1).asIdeal := bot_le.trans_lt (s.step 0)
    obtain hmax | ⟨p, hp, hsp⟩ := (Ideal.isPrime_nat_iff.mp (s 1).2).resolve_left h1.ne'
    · exact (le_maximalIdeal_of_isPrime (s 2).asIdeal).not_gt (hmax.symm.trans_lt (s.step 1))
    obtain hmax | ⟨q, hq, hsq⟩ :=
      (Ideal.isPrime_nat_iff.mp (s 2).2).resolve_left (h1.trans (s.step 1)).ne'
    · exact (le_maximalIdeal_of_isPrime (s 3).asIdeal).not_gt (hmax.symm.trans_lt (s.step 2))
    · exact hq.not_isUnit <| (Ideal.span_singleton_lt_span_singleton.mp
        ((hsp.symm.trans_lt (s.step 1)).trans_eq hsq)).isUnit_of_irreducible_right hp
  · refine le_iSup_of_le ⟨2, ![⊥, ⟨_, (span_singleton_prime two_ne_zero).mpr <| Nat.prime_iff.mp
      Nat.prime_two⟩, ⟨_, (maximalIdeal.isMaximal ℕ).isPrime⟩], fun i ↦ ?_⟩ le_rfl
    fin_cases i
    · exact bot_lt_iff_ne_bot.mpr (Ideal.span_singleton_eq_bot.not.mpr two_ne_zero)
    · simp_rw [Nat.maximalIdeal_eq_span_two_three]
      exact SetLike.lt_iff_le_and_exists.mpr ⟨Ideal.span_mono (by simp),
        3, Ideal.subset_span (by simp), Ideal.mem_span_singleton.not.mpr <| by simp⟩

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case neg
A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
x : B
hx : x ∈ a
this✝² : Algebra (A ⧸ p) (B ⧸ a) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this✝¹ : IsScalarTower A (A ⧸ p) (B ⧸ a)
this✝ : Module.Finite (A ⧸ p) (B ⧸ a)
this : Prime P
⊢ (Algebra.trace (A ⧸ p) (B ⧸ Ideal.map (algebraMap A B) p)) ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x) = 0

Tactic:
← this.irreducible.gcd_eq_one_iff,

Goal state after:
case neg
A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : gcd P a = 1
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
x : B
hx : x ∈ a
this✝² : Algebra (A ⧸ p) (B ⧸ a) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this✝¹ : IsScalarTower A (A ⧸ p) (B ⧸ a)
this✝ : Module.Finite (A ⧸ p) (B ⧸ a)
this : Prime P
⊢ (Algebra.trace (A ⧸ p) (B ⧸ Ideal.map (algebraMap A B) p)) ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x) = 0
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ S.y
⊢ False

Tactic:
by
  replace h := mul_dvd_mul_left ((η : 𝓞 K) - 1) h
  rw [coe_eta, ← y_spec, ← pow_two] at h
  exact lambda_sq_not_dvd_a_add_eta_mul_b _ h

Goal state after: