mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ (M ↾ {e | M.IsNonloop e} ↾ M.E).E = M.E ∧
    ∀ ⦃I : Set α⦄, I ⊆ (M ↾ {e | M.IsNonloop e} ↾ M.E).E → ((M ↾ {e | M.IsNonloop e} ↾ M.E).Indep I ↔ M.Indep I)

Tactic:
simp only [restrict_ground_eq, restrict_indep_iff, true_and]

Goal state after:
α : Type u_1
M : Matroid α
⊢ ∀ ⦃I : Set α⦄, I ⊆ M.E → ((M.Indep I ∧ I ⊆ {e | M.IsNonloop e}) ∧ I ⊆ M.E ↔ M.Indep I)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
e : α
heCK : e ∈ C ∩ K
⊢ (C ∩ K).Nontrivial

Tactic:
rw [nontrivial_iff_ne_singleton heCK]

Goal state after:
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
e : α
heCK : e ∈ C ∩ K
⊢ C ∩ K ≠ {e}
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case inl
α : Type u_2
M : Matroid α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.IsBasis J (insert e (insert f (J \ {e})))
hIb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hIs : X ⊆ insert f (J \ {e})
hX' : X ∈ Js
hfX : f ∉ X
hd : M.Dep (insert e X)
⊢ X ⊆ J

Tactic:
rw [← singleton_union, ← sdiff_subset_iff, sdiff_singleton_eq_self hfX] at hIs

Goal state after:
case inl
α : Type u_2
M : Matroid α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.IsBasis J (insert e (insert f (J \ {e})))
hIb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hIs : X ⊆ J \ {e}
hX' : X ∈ Js
hfX : f ∉ X
hd : M.Dep (insert e X)
⊢ X ⊆ J
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
⊢ LinearIndependent R x

Tactic:
linearIndependent_iff_injective_finsuppLinearCombination

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
⊢ Injective ⇑(Finsupp.linearCombination R x)
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
A : Type v
x : ι → A
inst✝⁴ : CommRing A
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsEmpty ι
inst✝ : Nontrivial A
⊢ AlgebraicIndependent K x

Tactic:
algebraicIndependent_empty_type_iff

Goal state after:
ι : Type u
A : Type v
x : ι → A
inst✝⁴ : CommRing A
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsEmpty ι
inst✝ : Nontrivial A
⊢ Injective ⇑(algebraMap K A)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
⊢ IsEmpty ι ↔ Algebra.IsAlgebraic R A

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ hx.1.isEmpty_of_isAlgebraic⟩
  have := hx.isAlgebraic
  rw [Set.range_eq_empty x, adjoin_empty] at this
  exact algebra_isAlgebraic_of_algebra_isAlgebraic_bot_left R A

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
ι' : Type u'
R : Type u_1
A : Type w
x : ι → A
y : ι' → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis R y
⊢ lift.{u', max w u} (lift.{u, w} (trdeg R A)) = lift.{u, max w u'} (lift.{w, u'} #ι')

Tactic:
hy.lift_cardinalMk_eq_trdeg,

Goal state after:
ι : Type u
ι' : Type u'
R : Type u_1
A : Type w
x : ι → A
y : ι' → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis R y
⊢ lift.{u', max w u} (lift.{u, w} (trdeg R A)) = lift.{u, max w u'} (lift.{u', w} (trdeg R A))
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: E : Type v
inst✝¹ : Field E
K : Type w
inst✝ : Field K
f : E[X]
i : E →+* K
x✝ : Algebra E K := i.toAlgebra
⊢ (map i f).natSepDegree = f.natSepDegree

Tactic:
show i = algebraMap E K by rfl,

Goal state after:
E : Type v
inst✝¹ : Field E
K : Type w
inst✝ : Field K
f : E[X]
i : E →+* K
x✝ : Algebra E K := i.toAlgebra
⊢ (map (algebraMap E K) f).natSepDegree = f.natSepDegree
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K L : IntermediateField F E
φ : Gal(E/F)
⊢ φ ∈ K.fixingSubgroup ⊓ L.fixingSubgroup → φ ∈ (K ⊔ L).fixingSubgroup

Tactic:
simp [← Subgroup.zpowers_le, ← IntermediateField.le_iff_le]

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

Goal state before:
pp: case h_splits
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) := ⋯
this✝ : ∀ (f : K →ₐ[F] E), Finite (↥K⟮x⟯ →ₐ[K] E)
this : FiniteDimensional F K
f : K →ₐ[F] E
a✝ : f ∈ Finset.univ
⊢ Polynomial.map (algebraMap K E) (minpoly K x) ∣ Polynomial.map (algebraMap F E) p

Tactic:
rwa [← f.comp_algebraMap, ← p.map_map, RingHom.algebraMap_toAlgebra, Polynomial.map_dvd_map']

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
⊢ (minpolyDiv R x).natDegree + 1 = (map (algebraMap R S) (minpoly R x)).natDegree

Tactic:
← minpolyDiv_spec,

Goal state after:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
⊢ (minpolyDiv R x).natDegree + 1 = (minpolyDiv R x * (X - C x)).natDegree
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
H : ∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))
x : K
hx : IsIntegral R x
⊢ (minpoly R x).degree = 1

Tactic:
← Monic.degree_map (minpoly.monic hx) (algebraMap R K)

Goal state after:
case mpr
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
H : ∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))
x : K
hx : IsIntegral R x
⊢ (map (algebraMap R K) (minpoly R x)).degree = 1
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁶ : Group G
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
inst✝² : MulSemiringAction G B
hG : IsGaloisGroup G A B
inst✝¹ : CommSemiring A'
inst✝ : Algebra A' B
e : A →+* A'
he : ∀ (a : A), (algebraMap A' B) (e a) = (algebraMap A B) a
he' : Function.Surjective ⇑e
g : G
b : B
a : A
⊢ g • a • b = a • g • b

Tactic:
exact hG.commutes.smul_comm g a b

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ¬IsField (𝓞 K)

Tactic:
have h_inj : Function.Injective (algebraMap ℤ (𝓞 K)) := RingHom.injective_int (algebraMap ℤ (𝓞 K))
  intro hf
  exact Int.not_isField
    (((IsIntegralClosure.isIntegral_algebra ℤ K).isField_iff_isField h_inj).mpr hf)

Goal state after:
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✝³ : MulSemiringAction G B
inst✝² : SMulCommClass G A B
H : Subgroup G
inst✝¹ : H.Normal
inst✝ : Algebra.IsInvariant A B G
x : ↥(FixedPoints.subalgebra A B ↥H)
hx : ∀ (g : G ⧸ H), g • x = x
y : A
hy : (algebraMap A B) y = ↑x
⊢ ∃ a, (algebraMap A ↥(FixedPoints.subalgebra A B ↥H)) a = x

Tactic:
exact ⟨y, Subtype.ext hy⟩

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

Goal state before:
pp: B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
⊢ ∃ a b,
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧ ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)

Tactic:
let r := ∑ i ∈ Finset.range (k + 1), Polynomial.monomial i (f.coeff (i + j))

Goal state after:
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
⊢ ∃ a b,
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧ ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
⊢ (-a).valMinAbs = -a.valMinAbs

Tactic:
rcases eq_zero_or_neZero n with rfl | h

Goal state after:
case inl
a : ZMod 0
ha : 2 * a.val ≠ 0
⊢ (-a).valMinAbs = -a.valMinAbs

case inr
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ (-a).valMinAbs = -a.valMinAbs
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
x : L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((Algebra.trace K L) x)) =
    ∑ x_1, (algebraMap L (AlgebraicClosure L)) (x_1 x)

Tactic:
← Fintype.sum_equiv (Normal.algHomEquivAut K (AlgebraicClosure L) L)

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
x : L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((Algebra.trace K L) x)) = ∑ x, ?f x

case f
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
x : L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
⊢ (L →ₐ[K] AlgebraicClosure L) → AlgebraicClosure L

case h
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
x : L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
⊢ ∀ (x_1 : L →ₐ[K] AlgebraicClosure L),
    ?f x_1 = (algebraMap L (AlgebraicClosure L)) (((Normal.algHomEquivAut K (AlgebraicClosure L) L) x_1) x)
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
x : L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((Algebra.trace K L) x)) = ∑ x, ?f x

pp: case f
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
x : L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
⊢ (L →ₐ[K] AlgebraicClosure L) → AlgebraicClosure L

pp: case h
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
x : L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
⊢ ∀ (x_1 : L →ₐ[K] AlgebraicClosure L),
    ?f x_1 = (algebraMap L (AlgebraicClosure L)) (((Normal.algHomEquivAut K (AlgebraicClosure L) L) x_1) x)

Tactic:
· rw [← trace_eq_sum_embeddings (AlgebraicClosure L) (x := x)]
    simp only [algebraMap_eq_smul_one, smul_one_smul]

Goal state after:
case h
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
x : L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
⊢ ∀ (x_1 : L →ₐ[K] AlgebraicClosure L),
    x_1 x = (algebraMap L (AlgebraicClosure L)) (((Normal.algHomEquivAut K (AlgebraicClosure L) L) x_1) x)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  __src
n : ℕ
h : q = Fintype.card (ZMod p) ^ n
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n

Tactic:
ZMod.card

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  __src
n : ℕ
h : q = p ^ n
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x ↦ ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this : Decidable (φ = 1)
⊢ q - 1 ∣ i ↔ φ = 1

Tactic:
← forall_pow_eq_one_iff,

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x ↦ ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this : Decidable (φ = 1)
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ φ = 1
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'
N : Subgroup G
inst✝⁵ : N.Normal
inst✝⁴ : MulSemiringAction G C
inst✝³ : IsGaloisGroup G A C
inst✝² : IsGaloisGroup (↥N) B C
inst✝¹ : MulSemiringAction G' B
inst✝ : IsGaloisGroup G' A B
g : G
x : B
this✝³ : IsDomain B
this✝² : MulSemiringAction G B := mulSemiringActionOfNormal G B C N
this✝¹ : MulSemiringAction (G ⧸ N) B := mulSemiringActionQuotient G B C N
this✝ : SMulCommClass (G ⧸ N) A B
this : IsGaloisGroup (G ⧸ N) A B
⊢ (algebraMap B C) ((quotientMulEquiv G G' A B C N) ↑g • x) = g • (algebraMap B C) x

Tactic:
rw [← algebraMap_smulOfNormal G B C N g x]

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'
N : Subgroup G
inst✝⁵ : N.Normal
inst✝⁴ : MulSemiringAction G C
inst✝³ : IsGaloisGroup G A C
inst✝² : IsGaloisGroup (↥N) B C
inst✝¹ : MulSemiringAction G' B
inst✝ : IsGaloisGroup G' A B
g : G
x : B
this✝³ : IsDomain B
this✝² : MulSemiringAction G B := mulSemiringActionOfNormal G B C N
this✝¹ : MulSemiringAction (G ⧸ N) B := mulSemiringActionQuotient G B C N
this✝ : SMulCommClass (G ⧸ N) A B
this : IsGaloisGroup (G ⧸ N) A B
⊢ (algebraMap B C) ((quotientMulEquiv G G' A B C N) ↑g • x) = (algebraMap B C) (g • x)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K' : Type u_3
inst✝ : Field K'
p : ℕ
hp : 1 < p
⊢ X.degree < (X ^ p).degree

Tactic:
rw [degree_X_pow, degree_X]

Goal state after:
K' : Type u_3
inst✝ : Field K'
p : ℕ
hp : 1 < p
⊢ 1 < ↑p
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K' : Type u_3
inst✝ : Field K'
p : ℕ
hp : 1 < p
h1 : X.degree < (X ^ p).degree
⊢ (X ^ p - X).natDegree = p

Tactic:
natDegree_eq_of_degree_eq (degree_sub_eq_left_of_degree_lt h1),

Goal state after:
K' : Type u_3
inst✝ : Field K'
p : ℕ
hp : 1 < p
h1 : X.degree < (X ^ p).degree
⊢ (X ^ p).natDegree = p
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : ¬a ≠ 0
⊢ a ^ (p - 1) = 0

Tactic:
· simp [of_not_not ha, (Fact.out : p.Prime).one_lt, tsub_eq_zero_iff_le]

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

Goal state before:
pp: case succ
p a m : ℕ
hm : (1 + p * a) ^ p ^ m ≡ 1 [MOD p ^ m]
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]

Tactic:
Nat.ModEq.comm,

Goal state after:
case succ
p a m : ℕ
hm : 1 ≡ (1 + p * a) ^ p ^ m [MOD p ^ m]
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]
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))
⊢ (LinearMap.det (N.subtype ∘ₗ (↑e).toIntLinearMap)).natAbs = Nat.card (M ⧸ N)

Tactic:
let f : M →ₗ[ℤ] M := N.subtype.comp (e' : M →ₗ[ℤ] N)

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'
⊢ (LinearMap.det (N.subtype ∘ₗ (↑e).toIntLinearMap)).natAbs = Nat.card (M ⧸ N)
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: case calc_2
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
ha : ∀ (i : Free.ChooseBasisIndex ℤ M), f (b' i) = a i • b' i
⊢ ∏ i, (a i).natAbs = ∏ a, Nat.card (ZMod (smithNormalFormCoeffs b h a).natAbs)

Tactic:
Nat.card_zmod,

Goal state after:
case calc_2
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
ha : ∀ (i : Free.ChooseBasisIndex ℤ M), f (b' i) = a i • b' i
⊢ ∏ i, (a i).natAbs = ∏ x, (smithNormalFormCoeffs b h x).natAbs
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case pos
A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ∃ s, Nonempty (Basis (↥s) B C)
⊢ e ((norm A) x) = (norm B) x

pp: case neg
A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ e ((norm A) x) = (norm B) x

Tactic:
· obtain ⟨s, ⟨b⟩⟩ := h
    let : Algebra A B := RingHom.toAlgebra e
    let : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' he.symm
    rw [Algebra.norm_eq_matrix_det b,
      Algebra.norm_eq_matrix_det (b.mapCoeffs e.symm (by simp [Algebra.smul_def, ← he])),
      e.map_det]
    congr
    ext i j
    simp [leftMulMatrix_apply, LinearMap.toMatrix_apply]

Goal state after:
case neg
A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ e ((norm A) x) = (norm B) x
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case mp
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : absNorm I = 0
⊢ I = ⊥

Tactic:
rw [← le_bot_iff]

Goal state after:
case mp
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : absNorm I = 0
⊢ I ≤ ⊥
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case mpr
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
⊢ absNorm ⊥ = 0

Tactic:
exact absNorm_bot

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

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
P : Ideal S
inst✝ : P.IsMaximal
⊢ ∃ p n, 0 < n ∧ ↑p ∈ P ∧ Nat.Prime p ∧ absNorm P = p ^ n

Tactic:
by
  have : IsAddTorsionFree S := .of_isTorsionFree ℤ _
  have := CharZero.of_isAddTorsionFree S S
  have : Finite (S ⧸ P) := Submodule.finiteQuotientOfFreeOfRankEq (P.restrictScalars ℤ)
    (Ideal.finrank_eq_finrank (Module.Free.chooseBasis _ _) _
      (Ideal.IsMaximal.ne_bot_of_isIntegral_int P))
  cases nonempty_fintype (S ⧸ P)
  let := Ideal.Quotient.field P
  obtain ⟨p, hpR⟩ := CharP.exists (S ⧸ P)
  obtain ⟨n, hp, e⟩ := FiniteField.card (S ⧸ P) p
  have hP : P.absNorm = p ^ (n : ℕ) := (Nat.card_eq_fintype_card.trans e:)
  refine ⟨p, n, n.2, ?_, hp, hP⟩
  rw [← Ideal.IsPrime.pow_mem_iff_mem (I := P) inferInstance _ n.pos, ← Nat.cast_pow, ← hP]
  exact P.absNorm_mem

Goal state after: