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

Goal state before:
pp: A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : IsInvariant A B G
inst✝¹ : Finite G
inst✝ : SMulCommClass G A B
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
val✝ : Fintype G
⊢ ∀ (P Q : Ideal B) [P.IsPrime] [Q.IsPrime], Ideal.under A P = Ideal.under A Q → ∃ g ∈ ⊤, Q ≤ g • P

Tactic:
intro P

Goal state after:
A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : IsInvariant A B G
inst✝¹ : Finite G
inst✝ : SMulCommClass G A B
P✝ Q : Ideal B
hP : P✝.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P✝ = Ideal.under A Q
val✝ : Fintype G
P : Ideal B
⊢ ∀ (Q : Ideal B) [P.IsPrime] [Q.IsPrime], Ideal.under A P = Ideal.under A Q → ∃ g ∈ ⊤, Q ≤ g • P
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ ((minpoly K (gen K x)).aroots F).sum = ((minpoly K x).aroots F).sum

Tactic:
← minpoly.algebraMap_eq injKxL

Goal state after:
case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ ((minpoly K ((algebraMap (↥K⟮x⟯) L) (gen K x))).aroots F).sum = ((minpoly K x).aroots F).sum
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (Polynomial.map (algebraMap K F) (minpoly K (gen K x))).Splits

Tactic:
← minpoly.algebraMap_eq injKxL

Goal state after:
case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (Polynomial.map (algebraMap K F) (minpoly K ((algebraMap (↥K⟮x⟯) L) (gen K x)))).Splits
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : IsInvariant A B G
inst✝¹ : Finite G
inst✝ : SMulCommClass G A B
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
⊢ ∃ g, Q = g • P

Tactic:
cases nonempty_fintype G
  have : ∀ (P Q : Ideal B) [P.IsPrime] [Q.IsPrime], P.under A = Q.under A →
      ∃ g ∈ (⊤ : Finset G), Q ≤ g • P := by
    intro P Q hP hQ hPQ
    rw [← Ideal.subset_union_prime 1 1 (fun _ _ _ _ ↦ hP.smul _)]
    intro b hb
    suffices h : ∃ g ∈ Finset.univ, g • b ∈ P by
      obtain ⟨g, -, hg⟩ := h
      apply Set.mem_biUnion (Finset.mem_univ g⁻¹) (Ideal.mem_inv_pointwise_smul_iff.mpr hg)
    obtain ⟨a, ha⟩ := isInvariant (A := A) (∏ g : G, g • b) (Finset.smul_prod_perm b)
    rw [← hP.prod_mem_iff, ← ha, ← P.mem_comap, ← P.under_def A,
      hPQ, Q.mem_comap, ha, hQ.prod_mem_iff]
    exact ⟨1, Finset.mem_univ 1, (one_smul G b).symm ▸ hb⟩
  obtain ⟨g, -, hg⟩ := this P Q hPQ
  obtain ⟨g', -, hg'⟩ := this Q (g • P) ((P.under_smul A g).trans hPQ).symm
  exact ⟨g, le_antisymm hg (smul_eq_of_le_smul (hg.trans hg') ▸ hg')⟩

Goal state after:
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A B
inst✝ : Algebra A C
e : B ≃ₐ[A] C
x : B
⊢ (trace A C) (e x) = (trace A B) x

Tactic:
simp_rw [Algebra.trace_apply, ← LinearMap.trace_conj' _ e.toLinearEquiv]

Goal state after:
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A B
inst✝ : Algebra A C
e : B ≃ₐ[A] C
x : B
⊢ (LinearMap.trace A C) ((lmul A C) (e x)) = (LinearMap.trace A C) ((↑e).conj ((lmul A B) x))
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case inr.refine_1
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -a = -↑a.valMinAbs

Tactic:
coe_valMinAbs

Goal state after:
case inr.refine_1
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -a = -a
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case succ.he
n : ℕ
a b : ZMod (n + 1)
⊢ ↑(a + b).valMinAbs = ↑a.valMinAbs + ↑b.valMinAbs

Tactic:
coe_valMinAbs

Goal state after:
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: case inr
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : IsGaloisGroup G K L
hG : Infinite G
⊢ Nat.card G = finrank K L

Tactic:
Nat.card_eq_zero_of_infinite,

Goal state after:
case inr
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : IsGaloisGroup G K L
hG : Infinite G
⊢ 0 = finrank K L
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁶ : Group G
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : MulSemiringAction G L
inst✝¹ : Finite G
inst✝ : IsGaloisGroup G K L
F : IntermediateField K L
g : Gal(L/K)
⊢ g ∈ Subgroup.map (↑(mulEquivAlgEquiv G K L)) (fixingSubgroup G ↑F) ↔ g ∈ F.fixingSubgroup

Tactic:
obtain ⟨g, rfl⟩ := (mulEquivAlgEquiv G K L).surjective g

Goal state after:
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁶ : Group G
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : MulSemiringAction G L
inst✝¹ : Finite G
inst✝ : IsGaloisGroup G K L
F : IntermediateField K L
g : G
⊢ (mulEquivAlgEquiv G K L) g ∈ Subgroup.map (↑(mulEquivAlgEquiv G K L)) (fixingSubgroup G ↑F) ↔
    (mulEquivAlgEquiv G K L) g ∈ F.fixingSubgroup
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := Fintype.card ↥G
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
⊢ False

Tactic:
cases CharP.char_is_prime_or_zero K p with
  | inr pzero =>
    exact (Fintype.card_pos).ne' <| Nat.eq_zero_of_zero_dvd <| pzero ▸ hd
  | inl pprime =>
    have fact_pprime := Fact.mk pprime
    -- G has an element x of order p by Cauchy's theorem
    have ⟨x, hx⟩ := exists_prime_orderOf_dvd_card p hd
    -- F has an element u (= ↑↑x) of order p
    let u := ((x : Kˣ) : K)
    have hu : orderOf u = p := by rwa [orderOf_units, Subgroup.orderOf_coe]
    -- u ^ p = 1 implies (u - 1) ^ p = 0 and hence u = 1 ...
    have h : u = 1 := by
      rw [← sub_left_inj, sub_self 1]
      apply eq_zero_of_pow_eq_zero (n := p)
      rw [sub_pow_char_of_commute, one_pow, ← hu, pow_orderOf_eq_one, sub_self]
      exact Commute.one_right u
    -- ... meaning x didn't have order p after all, contradiction
    apply pprime.one_lt.ne
    rw [← hu, h, orderOf_one]

Goal state after:
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
hg : G ≠ ⊥
⊢ ∑ x, ↑↑x = 0

Tactic:
rw [Subgroup.ne_bot_iff_exists_ne_one] at hg

Goal state after:
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
hg : ∃ a, a ≠ 1
⊢ ∑ x, ↑↑x = 0
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
⊢ (algebraMap K (AlgebraicClosure L)) (traceMatrix K ⇑pb.basis).det ≠ 0

Tactic:
have : FiniteDimensional K L := pb.finite

Goal state after:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
⊢ (algebraMap K (AlgebraicClosure L)) (traceMatrix K ⇑pb.basis).det ≠ 0
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: case a
a b : ℤ
⊢ (EuclideanDomain.gcd a b).natAbs ∣ a.gcd b

Tactic:
← Int.natCast_dvd_natCast

Goal state after:
case a
a b : ℤ
⊢ ↑(EuclideanDomain.gcd a b).natAbs ∣ ↑(a.gcd b)
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: case a
a b : ℤ
⊢ a.gcd b ∣ (EuclideanDomain.gcd a b).natAbs

Tactic:
← Int.natCast_dvd_natCast

Goal state after:
case a
a b : ℤ
⊢ ↑(a.gcd b) ∣ ↑(EuclideanDomain.gcd a b).natAbs
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: n : ℤ
k p : ℕ
hp : Nat.Prime p
h : ↑p ∣ n ^ k
⊢ ↑p ∣ n

Tactic:
rw [Int.natCast_dvd]

Goal state after:
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : ↑p ∣ n ^ k
⊢ p ∣ n.natAbs
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹⁷ : Group G
inst✝¹⁶ : Group G'
A : Type u_5
B : Type u_6
C : Type u_7
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : CommRing C
inst✝¹² : IsDomain C
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Algebra A C
inst✝⁹ : Algebra B C
inst✝⁸ : FaithfulSMul A B
inst✝⁷ : FaithfulSMul B C
inst✝⁶ : IsScalarTower A B C
inst✝⁵ : Finite G
inst✝⁴ : Finite G'
inst✝³ : MulSemiringAction G C
inst✝² : IsGaloisGroup G A C
inst✝¹ : MulSemiringAction G' B
inst✝ : IsGaloisGroup G' A B
g : G
x : B
this✝¹ : IsDomain B
this✝ : IsDomain A
this : FaithfulSMul A C
⊢ (algebraMap B C) ((restrictHom G G' A B C) g • x) = g • (algebraMap B C) x

Tactic:
let : MulSemiringAction G (FractionRing C) :=
    IsFractionRing.mulSemiringAction G C (FractionRing C)

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹⁷ : Group G
inst✝¹⁶ : Group G'
A : Type u_5
B : Type u_6
C : Type u_7
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : CommRing C
inst✝¹² : IsDomain C
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Algebra A C
inst✝⁹ : Algebra B C
inst✝⁸ : FaithfulSMul A B
inst✝⁷ : FaithfulSMul B C
inst✝⁶ : IsScalarTower A B C
inst✝⁵ : Finite G
inst✝⁴ : Finite G'
inst✝³ : MulSemiringAction G C
inst✝² : IsGaloisGroup G A C
inst✝¹ : MulSemiringAction G' B
inst✝ : IsGaloisGroup G' A B
g : G
x : B
this✝² : IsDomain B
this✝¹ : IsDomain A
this✝ : FaithfulSMul A C
this : MulSemiringAction G (FractionRing C) := IsFractionRing.mulSemiringAction G C (FractionRing C)
⊢ (algebraMap B C) ((restrictHom G G' A B C) g • x) = g • (algebraMap B C) x
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Group G
inst✝¹⁵ : Finite G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹² : Q.IsPrime
inst✝¹¹ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra (A ⧸ P) K
inst✝⁷ : Algebra (B ⧸ Q) L
inst✝⁶ : Algebra (A ⧸ P) L
inst✝⁵ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower (A ⧸ P) K L
inst✝² : Algebra.IsInvariant A B G
inst✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y) =
      (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
b : B ⧸ Q
a : A ⧸ P
h : x * (algebraMap (A ⧸ P) (B ⧸ Q)) a = b * y
ha : (algebraMap (A ⧸ P) L) a ≠ 0
hy : (algebraMap (B ⧸ Q) L) y ≠ 0
⊢ (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y = (algebraMap (B ⧸ Q) L) b / (algebraMap (A ⧸ P) L) a

Tactic:
rw [div_eq_div_iff hy ha, ← map_mul, ← h, map_mul, ← algebraMap_apply]

Goal state after:
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : (ZMod p)[X]
⊢ (expand (ZMod p) p) f = f ^ p

Tactic:
have h := FiniteField.expand_card f

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : (ZMod p)[X]
h : (expand (ZMod p) (Fintype.card (ZMod p))) f = f ^ Fintype.card (ZMod p)
⊢ (expand (ZMod p) p) f = f ^ p
Module: Mathlib.LinearAlgebra.Quotient.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
Ms : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommGroup (Ms i)
inst✝⁴ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
⊢ ((p i).mapQ q (f i) ⋯) (Pi.single i x i) = ((p i).mapQ q (f i) ⋯) x

Tactic:
rw [Pi.single_eq_same]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Free ℤ M
inst✝² : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst✝¹ : EquivLike E M ↥N
inst✝ : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ ↑e'
f_apply : ∀ (x : M), f x = ↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))) x) := fun x ↦ rfl
⊢ (LinearMap.det (N.subtype ∘ₗ (↑e).toIntLinearMap)).natAbs = Nat.card (M ⧸ N)

Tactic:
suffices (LinearMap.det f).natAbs = Nat.card (M ⧸ N) by
    calc
      _ = (LinearMap.det (N.subtype ∘ₗ
            (AddEquiv.toIntLinearEquiv e : M ≃ₗ[ℤ] N))).natAbs := rfl
      _ = (LinearMap.det (N.subtype ∘ₗ _)).natAbs :=
            Int.natAbs_eq_iff_associated.mpr (LinearMap.associated_det_comp_equiv _ _ _)
      _ = Nat.card (M ⧸ N) := this

Goal state after:
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Free ℤ M
inst✝² : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst✝¹ : EquivLike E M ↥N
inst✝ : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ ↑e'
f_apply : ∀ (x : M), f x = ↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))) x) := fun x ↦ rfl
⊢ (LinearMap.det f).natAbs = Nat.card (M ⧸ N)
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Free ℤ M
inst✝² : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst✝¹ : EquivLike E M ↥N
inst✝ : AddEquivClass E M ↥N
e : E
⊢ (LinearMap.det (N.subtype ∘ₗ (↑e).toIntLinearMap)).natAbs = Nat.card (M ⧸ N)

Tactic:
by
  let b := Module.Free.chooseBasis ℤ M
  -- Since `e : M ≃ₗ[ℤ] N`, the submodule `N` has full rank.
  have h : Module.finrank ℤ N = Module.finrank ℤ M :=
    (AddEquiv.toIntLinearEquiv e : M ≃ₗ[ℤ] N).symm.finrank_eq
  -- Use the Smith normal form to choose a nice basis for `N`.
  let a := smithNormalFormCoeffs b h
  let b' := smithNormalFormTopBasis b h
  let ab := smithNormalFormBotBasis b h
  have ab_eq := smithNormalFormBotBasis_def b h
  let e' : M ≃ₗ[ℤ] N := b'.equiv ab (Equiv.refl _)
  let f : M →ₗ[ℤ] M := N.subtype.comp (e' : M →ₗ[ℤ] N)
  let f_apply : ∀ x, f x = b'.equiv ab (Equiv.refl _) x := fun x ↦ rfl
  suffices (LinearMap.det f).natAbs = Nat.card (M ⧸ N) by
    calc
      _ = (LinearMap.det (N.subtype ∘ₗ
            (AddEquiv.toIntLinearEquiv e : M ≃ₗ[ℤ] N))).natAbs := rfl
      _ = (LinearMap.det (N.subtype ∘ₗ _)).natAbs :=
            Int.natAbs_eq_iff_associated.mpr (LinearMap.associated_det_comp_equiv _ _ _)
      _ = Nat.card (M ⧸ N) := this
  have ha : ∀ i, f (b' i) = a i • b' i := by
    intro i
    rw [f_apply, b'.equiv_apply, Equiv.refl_apply]
    exact ab_eq i
  calc
    Int.natAbs (LinearMap.det f) = Int.natAbs (LinearMap.toMatrix b' b' f).det := by
      rw [LinearMap.det_toMatrix]
    _ = Int.natAbs (Matrix.diagonal a).det := ?_
    _ = Int.natAbs (∏ i, a i) := by rw [Matrix.det_diagonal]
    _ = ∏ i, Int.natAbs (a i) := map_prod Int.natAbsHom a Finset.univ
    _ = Nat.card (M ⧸ N) := ?_
  -- since `LinearMap.toMatrix b' b' f` is the diagonal matrix with `a` along the diagonal.
  · congr 2; ext i j
    rw [LinearMap.toMatrix_apply, ha, map_smul, Basis.repr_self, Finsupp.smul_single,
      smul_eq_mul, mul_one]
    by_cases h : i = j
    · rw [h, Matrix.diagonal_apply_eq, Finsupp.single_eq_same]
    · rw [Matrix.diagonal_apply_ne _ h, Finsupp.single_eq_of_ne h]
  -- Now we map everything through the linear equiv `M ≃ₗ (ι → ℤ)`,
  -- which maps `(M ⧸ N)` to `Π i, ZMod (a i).nat_abs`.
  simp_rw [Nat.card_congr (quotientEquivPiZMod N b h).toEquiv, Nat.card_pi, Nat.card_zmod, a]

Goal state after:
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case pos
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ ((minpoly K (AdjoinSimple.gen K x)).aroots F).prod = ((minpoly K x).aroots F).prod

Tactic:
← minpoly.algebraMap_eq injKxL

Goal state after:
case pos
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ ((minpoly K ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x))).aroots F).prod = ((minpoly K x).aroots F).prod
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case pos.hf
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (Polynomial.map (algebraMap K F) (minpoly K (AdjoinSimple.gen K x))).Splits

Tactic:
← minpoly.algebraMap_eq injKxL

Goal state after:
case pos.hf
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (Polynomial.map (algebraMap K F) (minpoly K ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)))).Splits
Module: Mathlib.RingTheory.Artinian.Ring

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
I : Ideal R
⊢ I.jacobson = I.radical

Tactic:
by
  simp_rw [Ideal.jacobson, Ideal.radical_eq_sInf, IsArtinianRing.isPrime_iff_isMaximal]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
⊢ cardQuot (P ^ i) = cardQuot P ^ i

Tactic:
induction i with

Goal state after:
case succ
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
⊢ cardQuot (P ^ (i + 1)) = cardQuot P ^ (i + 1)
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this : P ^ (i + 1) < P ^ i
hquot : ↥(map (mkQ (P ^ i.succ)) (P ^ i)) ≃ S ⧸ P
⊢ Nat.card (S ⧸ P ^ i.succ) = cardQuot P * cardQuot (P ^ i)

Tactic:
←
      card_quotient_mul_card_quotient (P ^ i) (P ^ i.succ) this.le,

Goal state after:
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this : P ^ (i + 1) < P ^ i
hquot : ↥(map (mkQ (P ^ i.succ)) (P ^ i)) ≃ S ⧸ P
⊢ Nat.card ↥(map (mkQ (P ^ i.succ)) (P ^ i)) * Nat.card (S ⧸ P ^ i) = cardQuot P * cardQuot (P ^ i)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
⊢ f (a * b) = f a * f b

Tactic:
obtain ⟨ua, a_eq⟩ := prod_normalizedFactors ha0
    obtain ⟨ub, b_eq⟩ := prod_normalizedFactors hb0
    rw [← a_eq, ← b_eq, mul_right_comm (Multiset.prod (normalizedFactors a)) ua
        (Multiset.prod (normalizedFactors b) * ub), h1 ua.isUnit, h1 ub.isUnit, h1 ua.isUnit, ←
      mul_assoc, h1 ub.isUnit, mul_right_comm _ (f ua), ← mul_assoc]
    congr
    rw [← (normalizedFactors a).map_id, ← (normalizedFactors b).map_id,
      Finset.prod_multiset_map_count, Finset.prod_multiset_map_count,
      Finset.prod_subset (Finset.subset_union_left (s₂ := (normalizedFactors b).toFinset)),
      Finset.prod_subset (Finset.subset_union_right (s₂ := (normalizedFactors b).toFinset)), ←
      Finset.prod_mul_distrib]
    · simp_rw [id, ← pow_add, this]
    all_goals simp only [Multiset.mem_toFinset]
    · intro p _ hpb
      simp [hpb]
    · intro p _ hpa
      simp [hpa]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case inr.refine_1
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
⊢ (f '' {I | absNorm I = n}).Finite

pp: case inr.refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
⊢ Set.InjOn f {I | absNorm I = n}

Tactic:
· suffices Finite (S ⧸ @Ideal.span S _ {↑n}) by
        let g := ((↑) : Ideal (S ⧸ @Ideal.span S _ {↑n}) → Set (S ⧸ @Ideal.span S _ {↑n}))
        refine Set.Finite.of_finite_image (f := g) ?_ SetLike.coe_injective.injOn
        exact Set.Finite.subset Set.finite_univ (Set.subset_univ _)
      rw [← absNorm_ne_zero_iff, absNorm_span_singleton]
      simpa only [Ne, Int.natAbs_eq_zero, Algebra.norm_eq_zero_iff, Nat.cast_eq_zero] using
        ne_of_gt hn

Goal state after:
case inr.refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
⊢ Set.InjOn f {I | absNorm I = n}