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

Goal state before:
pp: α : Type u
M : Matroid α
I J X : Set α
inst✝ : M.InvariantCardinalRank
hIX : M.IsBasis I X
hJX : M.IsBasis J X
⊢ #↑I = #↑J

Tactic:
rw [← sdiff_union_inter I J,
    mk_union_of_disjoint (disjoint_sdiff_left.mono_right inter_subset_right),
    hIX.cardinalMk_sdiff_comm hJX,
    ← mk_union_of_disjoint (disjoint_sdiff_left.mono_right inter_subset_left),
    inter_comm, sdiff_union_inter]

Goal state after:
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
hCK : (C ∩ K).Nonempty
⊢ (C ∩ K).Nontrivial

Tactic:
obtain ⟨e, heCK⟩ := hCK

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).Nontrivial
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
⊢ M.fundCocircuit e X = {e}

Tactic:
by_cases he : e ∈ M.E
  · rw [fundCocircuit, fundCircuit_eq_of_mem]
    exact ⟨he, heX⟩
  rw [fundCocircuit_eq_of_notMem_ground _ he]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid α
inst✝ : M.InvariantCardinalRank
hf : InjOn f M.E
I X : Set α
hIX : M.IsBasis I X
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
J : Set α
hJ : (M.map f hf).IsBasis (f '' J) (f '' X)
hJX : M.IsBasis J X
h' : f '' X = f '' X
hcard : #↑(I \ J) = #↑(J \ I)
⊢ #↑(f '' I \ f '' J) = #↑(f '' J \ f '' I)

Tactic:
rwa [← lift_inj.{u, v},
    ← mk_image_eq_of_injOn_lift _ _ (hf.mono ((hIX.indep.sdiff _).subset_ground)),
    ← mk_image_eq_of_injOn_lift _ _ (hf.mono ((hJX.indep.sdiff _).subset_ground)),
    lift_inj, (hf.mono hIX.indep.subset_ground).image_sdiff,
    (hf.mono hJX.indep.subset_ground).image_sdiff, inter_comm,
    hf.image_inter hJX.indep.subset_ground hIX.indep.subset_ground,
    sdiff_inter_self_eq_sdiff, sdiff_self_inter] at hcard

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : ¬AlgebraicIndependent R x
h : AlgebraicIndependent R (Sum.elim y x)
⊢ AlgebraicIndependent R x

Tactic:
by apply h.comp _ Sum.inr_injective

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
h : M.closure ∅ = M.E
X : Set α
⊢ M.closure X ⊆ (loopyOn M.E).closure X

Tactic:
simp [closure_subset_ground]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : FaithfulSMul G α
g h : G
ne_one : g ≠ 1
disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)
⊢ ¬Commute g h

Tactic:
contrapose ne_one with comm

Goal state after:
α : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : FaithfulSMul G α
g h : G
disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)
comm : Commute g h
⊢ g = 1
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
S : Type v
A : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors S
inst✝¹ : Algebra.IsAlgebraic S A
inst✝ : FaithfulSMul S A
x : ι → S
hx : IsTranscendenceBasis R x
⊢ IsTranscendenceBasis R (⇑(algebraMap S A) ∘ x)

Tactic:
let f := IsScalarTower.toAlgHom R S A

Goal state after:
ι : Type u
R : Type u_1
S : Type v
A : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors S
inst✝¹ : Algebra.IsAlgebraic S A
inst✝ : FaithfulSMul S A
x : ι → S
hx : IsTranscendenceBasis R x
f : S →ₐ[R] A := IsScalarTower.toAlgHom R S A
⊢ IsTranscendenceBasis R (⇑(algebraMap S A) ∘ x)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
this✝² : Nontrivial ↥(adjoin R t)
this✝¹ : Nontrivial A
this✝ : IsDomain A
this : FaithfulSMul R A
ht : (matroid R A).Spanning t
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ IsTranscendenceBasis R Subtype.val

Tactic:
rw [← matroid_indep_iff] at hs

Goal state after:
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
s t : Set A
hst : s ⊆ t
this✝² : Nontrivial ↥(adjoin R t)
this✝¹ : Nontrivial A
this✝ : IsDomain A
this : FaithfulSMul R A
hs : (matroid R A).Indep s
ht : (matroid R A).Spanning t
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ IsTranscendenceBasis R Subtype.val
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
⊢ (minpoly F x).natSepDegree = 1 ↔ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Tactic:
by
  convert_to _ ↔ ∃ (n : ℕ) (y : F), Polynomial.aeval x (X ^ q ^ n - C y) = 0
  · simp_rw [RingHom.mem_range, map_sub, map_pow, aeval_C, aeval_X, sub_eq_zero, eq_comm]
  refine ⟨fun h ↦ ?_, fun ⟨n, y, h⟩ ↦ ?_⟩
  · obtain ⟨n, y, hx⟩ := (minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C q).1 h
    exact ⟨n, y, hx ▸ aeval F x⟩
  have hnezero := X_pow_sub_C_ne_zero (expChar_pow_pos F q n) y
  refine ((natSepDegree_le_of_dvd _ _ (minpoly.dvd F x h) hnezero).trans_eq <|
    natSepDegree_X_pow_char_pow_sub_C q n y).antisymm ?_
  rw [Nat.one_le_iff_ne_zero, natSepDegree_ne_zero_iff, ← Nat.one_le_iff_ne_zero]
  exact minpoly.natDegree_pos <| IsAlgebraic.isIntegral ⟨_, hnezero, h⟩

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

Goal state before:
pp: F : Type u_1
E' : Type u_3
inst✝³ : Field F
inst✝² : Field E'
inst✝¹ : Algebra F E'
L : IntermediateField F E'
inst✝ : IsGalois F E'
⊢ finrank F ↥L = L.fixingSubgroup.index

Tactic:
by
  wlog hnfd : FiniteDimensional F L generalizing L
  · rw [Module.finrank_of_infinite_dimensional hnfd]
    by_contra! h
    replace h : L.fixingSubgroup.FiniteIndex := ⟨h.symm⟩
    obtain ⟨L', hfd, hL'⟩ :=
      exists_lt_finrank_of_infinite_dimensional hnfd L.fixingSubgroup.index
    let i := (liftAlgEquiv L').toLinearEquiv
    replace hfd := i.finiteDimensional
    rw [i.finrank_eq, this _ hfd] at hL'
    exact (Subgroup.index_antitone <| fixingSubgroup_le <|
      IntermediateField.lift_le L').not_gt hL'
  let E := normalClosure F L E'
  have hle : L ≤ E := by simpa only [fieldRange_val] using L.val.fieldRange_le_normalClosure
  let L' := restrict hle
  have h := Module.finrank_mul_finrank F ↥L' ↥E
  classical
  rw [← IsGalois.card_fixingSubgroup_eq_finrank L', ← IsGalois.card_aut_eq_finrank F E] at h
  rw [← L'.fixingSubgroup.index_mul_card, Nat.mul_left_inj Finite.card_pos.ne'] at h
  rw [(restrictAlgEquiv hle).toLinearEquiv.finrank_eq, h, ← L'.map_fixingSubgroup_index E']
  congr 2
  exact lift_restrict hle

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f
algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)
⊢ ∃ g', map (algebraMap R K) g' = g * C g.leadingCoeff⁻¹

Tactic:
have :
    (algebraMap R _).comp algeq.toAlgHom.toRingHom = (integralClosure R _).toSubring.subtype := by
    ext x; (conv_rhs => rw [← algeq.symm_apply_apply x]); rfl

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f
algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)
this : (algebraMap R K).comp (↑algeq).toRingHom = (integralClosure R K).toSubring.subtype
⊢ ∃ g', map (algebraMap R K) g' = g * C g.leadingCoeff⁻¹
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
p : R[X]
hp0 : p ≠ 0
hp : (Polynomial.aeval s) p = 0
hs : IsIntegral R s
⊢ (minpoly R s).natDegree ≤ p.natDegree

Tactic:
exact natDegree_le_of_dvd ((isIntegrallyClosed_dvd_iff hs _).mp hp) hp0

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 = (minpoly R x).natDegree

Tactic:
rw [← (minpoly.monic hx).natDegree_map (algebraMap R S), ← minpolyDiv_spec, natDegree_mul']
  · simp
  · simpa using minpolyDiv_ne_zero hx

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ ¬IsUnit a'

Tactic:
by_contra h_contra

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
h_contra : IsUnit a'
⊢ False
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
K : Type u_3
inst✝² : Ring K
inst✝¹ : Algebra F K
e : K ≃ₐ[F] E
inst✝ : IsPurelyInseparable F K
x✝ : E
⊢ IsIntegral F x✝

Tactic:
rw [← isIntegral_algEquiv e.symm]; exact IsPurelyInseparable.isIntegral' F _

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case inl
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
inst✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
this : NormalizedGCDMonoid R
u : Rˣ
h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
h0 : a ≠ 0 ∧ b ≠ 0
h : IsUnit (C ↑u * (integerNormalization R⁰ b).primPart)
⊢ IsUnit a ∨ IsUnit b

pp: case inr
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
inst✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
this : NormalizedGCDMonoid R
u : Rˣ
h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
h0 : a ≠ 0 ∧ b ≠ 0
h : IsUnit (integerNormalization R⁰ a).primPart
⊢ IsUnit a ∨ IsUnit b

Tactic:
· right
    apply
      isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart h0.2
        (isUnit_of_mul_isUnit_right h)

Goal state after:
case inr
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
inst✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
this : NormalizedGCDMonoid R
u : Rˣ
h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
h0 : a ≠ 0 ∧ b ≠ 0
h : IsUnit (integerNormalization R⁰ a).primPart
⊢ IsUnit a ∨ IsUnit b
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case inr
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
inst✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
this : NormalizedGCDMonoid R
u : Rˣ
h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
h0 : a ≠ 0 ∧ b ≠ 0
h : IsUnit (integerNormalization R⁰ a).primPart
⊢ IsUnit a ∨ IsUnit b

Tactic:
left
    apply isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart h0.1 h

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

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsDomain A
⊢ ∃ s b, ∀ (x : ↥s), IsIntegral A (b x)

Tactic:
let := Classical.decEq L
  let s' := IsNoetherian.finsetBasisIndex K L
  let bs' := IsNoetherian.finsetBasis K L
  obtain ⟨y, hy, his'⟩ := exists_integral_multiples A K (Finset.univ.image bs')
  have hy' : algebraMap A L y ≠ 0 := by
    refine mt ((injective_iff_map_eq_zero (algebraMap A L)).mp ?_ _) hy
    rw [IsScalarTower.algebraMap_eq A K L]
    exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)
  refine ⟨s', bs'.map {Algebra.lmul _ _ (algebraMap A L y) with
    toFun := fun x => algebraMap A L y * x
    invFun := fun x => (algebraMap A L y)⁻¹ * x
    left_inv := ?_
    right_inv := ?_}, ?_⟩
  · intro x; simp only [inv_mul_cancel_left₀ hy']
  · intro x; simp only [mul_inv_cancel_left₀ hy']
  · rintro ⟨x', hx'⟩
    simp only [Algebra.smul_def, Finset.mem_image, Finset.mem_univ,
      true_and] at his'
    exact his' _ ⟨_, rfl⟩

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

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_3
inst✝¹³ : Field L
C : Type u_4
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsDomain A
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
⊢ Module.Finite A C

Tactic:
have := IsIntegralClosure.isNoetherian A K L C
  exact Module.IsNoetherian.finite A C

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

Goal state before:
pp: G : Type u_1
inst✝⁹ : Group G
B : Type u_3
C : Type u_4
inst✝⁸ : Semiring C
inst✝⁷ : MulSemiringAction G C
N : Subgroup G
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra B C
inst✝⁴ : FaithfulSMul B C
inst✝³ : MulSemiringAction G B
inst✝² : SMulDistribClass G B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
g : G
b : B
⊢ ↑g • b = g • b

Tactic:
let := mulSemiringActionOfNormal G B C N
  refine (Quotient.liftOn'_mk'' (· • b) _ g).trans (FaithfulSMul.algebraMap_injective B C ?_)
  rw [algebraMap.smul', algebraMap.smul']

Goal state after:
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
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
b : B
hb : b ∈ ↑Q
a : A
ha : (algebraMap A B) a = ∏ g, g • b
⊢ a ∈ Ideal.comap (algebraMap A B) P

Tactic:
← P.under_def A,

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 Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
b : B
hb : b ∈ ↑Q
a : A
ha : (algebraMap A B) a = ∏ g, g • b
⊢ a ∈ Ideal.under A P
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
L : Type u_5
inst✝⁶ : Field L
F : Type u_6
inst✝⁵ : Field F
inst✝⁴ : Algebra R L
inst✝³ : Algebra L F
inst✝² : Algebra R F
inst✝¹ : IsScalarTower R L F
inst✝ : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
y : AlgebraicClosure F
hy : eval₂ (algebraMap L (AlgebraicClosure F)) y (minpoly L x) = 0
⊢ IsIntegral R y

Tactic:
use minpoly R x, minpoly.monic hx

Goal state after:
case right
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_5
inst✝⁶ : Field L
F : Type u_6
inst✝⁵ : Field F
inst✝⁴ : Algebra R L
inst✝³ : Algebra L F
inst✝² : Algebra R F
inst✝¹ : IsScalarTower R L F
inst✝ : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
y : AlgebraicClosure F
hy : eval₂ (algebraMap L (AlgebraicClosure F)) y (minpoly L x) = 0
⊢ eval₂ (algebraMap R (AlgebraicClosure F)) y (minpoly R x) = 0
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
⊢ ∃ 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 j := (f.map (algebraMap B (B ⧸ Q))).rootMultiplicity 0

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)
⊢ ∃ 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: case mpr
n : ℕ
a b : ZMod n
⊢ a = b ∨ a = -b → a.valMinAbs.natAbs = b.valMinAbs.natAbs

Tactic:
· rintro (rfl | rfl)
    · rfl
    · rw [natAbs_valMinAbs_neg]

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

Goal state before:
pp: case refine_1
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))
hr✝ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
⊢ ¬(Ideal.Quotient.mk Q) a = 0

Tactic:
← Ideal.Quotient.algebraMap_eq,

Goal state after:
case refine_1
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))
hr✝ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
⊢ ¬(algebraMap B (B ⧸ Q)) a = 0
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : CommRing R
inst✝ : Algebra K R
x✝¹ x✝ : R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain ⟨p, _, _, hp, card_eq⟩ := card' K
    nontriviality R
    have : CharP R p := charP_of_injective_algebraMap' K p
    have : ExpChar R p := .prime hp
    simp only [OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, powMonoidHom_apply, card_eq]
    exact add_pow_expChar_pow ..

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

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
n : ℤ
this : Fact (Nat.Prime p)
⊢ n ^ p ≡ n [ZMOD ↑p]

Tactic:
simp [← ZMod.intCast_eq_intCast_iff]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this✝¹ : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
ha0 : ¬a = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
⊢ ∀ p ∈ normalizedFactors a, ∀ q ∈ normalizedFactors a, p ∣ q → p = q

Tactic:
apply normalizedFactors_eq_of_dvd

Goal state after: