mathlib-initiative/mathlib-tactics huggingface dataset:
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
hx : AlgebraicIndependent R x
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x✝ : ι
⊢ Polynomial.aeval (x x✝) = (aeval x).comp (Polynomial.aeval (X x✝))

Tactic:
ext1

Goal state after:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x✝ : ι
⊢ (Polynomial.aeval (x x✝)) Polynomial.X = ((aeval x).comp (Polynomial.aeval (X x✝))) Polynomial.X
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
a : { x // x ∈ s }
left✝ : a ∈ t
h : (Embedding.subtype fun x ↦ x ∈ s) a ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ s) t
⊢ ↑⟨(Embedding.subtype fun x ↦ x ∈ s) a, h⟩ ∈ s

Tactic:
simp only [Subtype.coe_prop, Embedding.coe_subtype]

Goal state after:
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
r : R
⊢ Polynomial.C (hx.aevalEquiv (C r)) = Polynomial.C ((algebraMap R ↥(adjoin R (range x))) r)

Tactic:
congr
  apply_fun Subtype.val using Subtype.val_injective
  simp

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

Goal state before:
pp: case mpr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
a✝ : a ∈ s
⊢ g • a ∈ (fixedBy α g)ᶜ

Tactic:
rwa [Set.mem_compl_iff, smul_mem_fixedBy_iff_mem_fixedBy]

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

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_3
inst✝² : Monoid G
inst✝¹ : MulAction G A
inst✝ : MulAction G B
f : A →ₑ[id] B
H : Submonoid G
a : A
ha : a ∈ MulAction.fixedPoints (↥H) A
⊢ f a ∈ MulAction.fixedPoints (↥H) B

Tactic:
intro ⟨h, _⟩

Goal state after:
G : Type u_1
A : Type u_2
B : Type u_3
inst✝² : Monoid G
inst✝¹ : MulAction G A
inst✝ : MulAction G B
f : A →ₑ[id] B
H : Submonoid G
a : A
ha : a ∈ MulAction.fixedPoints (↥H) A
h : G
property✝ : h ∈ H
⊢ ⟨h, property✝⟩ • f a = f a
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.{w, u} #ι) = lift.{max u w, u'} #ι'

Tactic:
hx.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.{max u w, u'} #ι'
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
⊢ (∃ n y, f = (expand F (q ^ n)) X - (expand F (q ^ n)) (C y)) ↔ ∃ n y, f = X ^ q ^ n - C y

Tactic:
expand_X,

Goal state after:
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
⊢ (∃ n y, f = X ^ q ^ n - (expand F (q ^ n)) (C y)) ↔ ∃ n y, f = X ^ q ^ n - C y
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_2
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm✝ : f.Monic
x✝ : ∃ m n y, m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m
m n : ℕ
y : F
hm : m ≠ 0
h : f = (X ^ q ^ n - C y) ^ m
⊢ (X ^ q ^ n - C y).natSepDegree = 1

Tactic:
natSepDegree_X_pow_char_pow_sub_C

Goal state after:
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:
by simp [← Subgroup.zpowers_le, ← IntermediateField.le_iff_le]

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hmul_left
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := ⋯
this✝ : TopologicalSpace R := ⋯
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)

Tactic:
intro x₀
    rw [basis.tendsto_iff basis]
    intro U
    simpa using! B.mul_left x₀

Goal state after:
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
⊢ univ ∈ 𝓝 1 ∧ ∅ * univ ⊆ W

Tactic:
by simp only [univ_mem, empty_mul, empty_subset, and_self]

Goal state after:
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 : IntermediateField K L
h_E1 : E1 ∈ finiteExts K L
E2 : IntermediateField K L
h_E2 : E2 ∈ finiteExts K L
this : FiniteDimensional K ↥E1
⊢ ∃ z ∈ (fun g ↦ g.carrier) '' fixedByFinite K L,
    z ⊆ (fun g ↦ g.carrier) E1.fixingSubgroup ∩ (fun g ↦ g.carrier) E2.fixingSubgroup

Tactic:
have : FiniteDimensional K E2 := h_E2

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 : IntermediateField K L
h_E1 : E1 ∈ finiteExts K L
E2 : IntermediateField K L
h_E2 : E2 ∈ finiteExts K L
this✝ : FiniteDimensional K ↥E1
this : FiniteDimensional K ↥E2
⊢ ∃ z ∈ (fun g ↦ g.carrier) '' fixedByFinite K L,
    z ⊆ (fun g ↦ g.carrier) E1.fixingSubgroup ∩ (fun g ↦ g.carrier) E2.fixingSubgroup
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
⊢ B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

Tactic:
let := b.finiteDimensional_of_finite
  rw [dualSubmodule_span_of_basis _ hB.flip, dualSubmodule_span_of_basis B hB,
    dualBasis_dualBasis_flip hB]

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

Goal state before:
pp: case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
x : E
hdeg : (minpoly F x).natSepDegree = 1
halg : IsIntegral F x
hsep : IsSeparable F x
⊢ x ∈ (algebraMap F E).range

Tactic:
hsep.natSepDegree_eq_natDegree,

Goal state after:
case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
x : E
hdeg : (minpoly F x).natDegree = 1
halg : IsIntegral F x
hsep : IsSeparable F x
⊢ x ∈ (algebraMap F E).range
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: 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 R T
inst✝³ : Free R S
inst✝² : Free R T
inst✝¹ : Module.Finite R S
inst✝ : Module.Finite R T
x : S × T
f : S × T →ₗ[R] End R S × End R T := (lmul R S).toLinearMap.prodMap (lmul R T).toLinearMap
this : (lmul R (S × T)).toLinearMap = prodMapLinear R S T S T R ∘ₗ f
⊢ (trace R (S × T)) x = (trace R S) x.1 + (trace R T) x.2

Tactic:
simp_rw [trace, this]

Goal state after:
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 R T
inst✝³ : Free R S
inst✝² : Free R T
inst✝¹ : Module.Finite R S
inst✝ : Module.Finite R T
x : S × T
f : S × T →ₗ[R] End R S × End R T := (lmul R S).toLinearMap.prodMap (lmul R T).toLinearMap
this : (lmul R (S × T)).toLinearMap = prodMapLinear R S T S T R ∘ₗ f
⊢ (LinearMap.trace R (S × T) ∘ₗ prodMapLinear R S T S T R ∘ₗ f) x =
    (LinearMap.trace R S ∘ₗ (lmul R S).toLinearMap) x.1 + (LinearMap.trace R T ∘ₗ (lmul R T).toLinearMap) x.2
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
h : ∀ (L : IntermediateField F E), FiniteDimensional F ↥L → IsPurelyInseparable F ↥L
x : E
hx : IsIntegral F x
x✝ : IsSeparable F x
⊢ (minpoly F (AdjoinSimple.gen F x)).Separable

Tactic:
rwa [minpoly_eq]

Goal state after:
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case pos
n : ℕ
a : ZMod (n + 1)
h : a.val ≤ n.succ / 2
⊢ ↑a.val * 2 = ↑n + 1 ↔ 2 * a.val = n + 1

Tactic:
← Int.natCast_inj,

Goal state after:
case pos
n : ℕ
a : ZMod (n + 1)
h : a.val ≤ n.succ / 2
⊢ ↑a.val * 2 = ↑n + 1 ↔ ↑(2 * a.val) = ↑(n + 1)
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case hfg
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : { x // x ∈ (minpoly K pb.gen).aroots E }), ?f✝ x = _root_.id ↑x

pp: case f
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := ⋯
this : Fintype (L →ₐ[K] E) := ⋯
⊢ { x // x ∈ (minpoly K pb.gen).aroots E } → E

pp: case h
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : L →ₐ[K] E), x pb.gen = ?f✝ (pb.liftEquiv' x)

Tactic:
· intro x; rfl

Goal state after:
case h
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : Type u_7
inst✝¹ : Field E
inst✝ : Algebra K E
pb : PowerBasis K L
hE : (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits
hfx : IsSeparable K pb.gen
this✝ : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : L →ₐ[K] E), x pb.gen = _root_.id ↑(pb.liftEquiv' x)
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case neg.succ.hnc
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this✝ : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
h : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - 1
this : p ^ (n + 1) = 1
⊢ False

Tactic:
obtain rfl : g = minpoly K x := by simpa [this] using hg₂
          cases hx hg₁

Goal state after:
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
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
inst✝ : Finite G
⊢ FixedPoints.intermediateField ↥(fixingSubgroup G ↑F) = F

Tactic:
rw [← ofDual_intermediateFieldEquivSubgroup_apply, ← intermediateFieldEquivSubgroup_symm_apply,
    OrderIso.symm_apply_apply]

Goal state after:
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
inst✝ : FiniteDimensional K L
tfae_1_to_3 : Algebra.IsSeparable K L → (traceForm K L).Nondegenerate
H₁ : (traceForm K L).Nondegenerate
H₂ : Algebra.trace K L = 0
⊢ traceForm K L = 0

Tactic:
ext; simp [H₂]

Goal state after:
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
H : Subgroup G
hGKL : IsGaloisGroup G K L
E : Type u_5
inst✝⁶ : Field E
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra E L
inst✝³ : IsScalarTower K E L
inst✝² : Finite G
inst✝¹ : IsGaloisGroup (↥H) E L
inst✝ : IsGalois K E
F : IntermediateField K L := (IsScalarTower.toAlgHom K E L).fieldRange
this✝¹ : IsGalois K ↥F
hFL : IsGaloisGroup (↥H) (↥F) L
this✝ : IsGalois K L
this : Finite Gal(L/K)
⊢ (Subgroup.map (↑(mulEquivCongr Gal(L/K) G K L)) (fixingSubgroup Gal(L/K) ↑F)).Normal

Tactic:
MulEquiv.normal_map_iff

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
H : Subgroup G
hGKL : IsGaloisGroup G K L
E : Type u_5
inst✝⁶ : Field E
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra E L
inst✝³ : IsScalarTower K E L
inst✝² : Finite G
inst✝¹ : IsGaloisGroup (↥H) E L
inst✝ : IsGalois K E
F : IntermediateField K L := (IsScalarTower.toAlgHom K E L).fieldRange
this✝¹ : IsGalois K ↥F
hFL : IsGaloisGroup (↥H) (↥F) L
this✝ : IsGalois K L
this : Finite Gal(L/K)
⊢ (fixingSubgroup Gal(L/K) ↑F).Normal
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: p x y : ℕ
hp : Nat.Prime p
h : p - 1 ∣ x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
⊢ n ^ x ≡ n ^ y [ZMOD ↑p]

Tactic:
by
  rw [← Nat.mul_div_eq_iff_dvd] at h
  by_cases hn : n ≡ 0 [ZMOD p]
  · grw [hn, zero_pow (hy.trans_le hxy).ne', zero_pow hy.ne']
  · rw [Int.modEq_zero_iff_dvd, ← (Nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd] at hn
    grw [← pow_sub_mul_pow n hxy, ← h, pow_mul, Int.ModEq.pow_card_sub_one_eq_one hp hn.symm,
      one_pow, one_mul]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
k : Type u_3
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u_4
inst✝¹⁰ : Finite G
inst✝⁹ : Group G
inst✝⁸ : MulSemiringAction G B
inst✝⁷ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝⁶ : Q.LiesOver P
inst✝⁵ : CommRing k
inst✝⁴ : Algebra (A ⧸ P) k
inst✝³ : Algebra (B ⧸ Q) k
inst✝² : IsScalarTower (A ⧸ P) (B ⧸ Q) k
inst✝¹ : IsDomain k
inst✝ : FaithfulSMul (B ⧸ Q) k
σ : k →ₐ[A ⧸ P] k
⊢ ∃ τ, ∀ (x : B ⧸ Q), (algebraMap (B ⧸ Q) k) (τ x) = σ ((algebraMap (B ⧸ Q) k) x)

Tactic:
let f : (B ⧸ Q) →ₐ[A ⧸ P] k := IsScalarTower.toAlgHom _ _ _
  have hf : Function.Injective f := FaithfulSMul.algebraMap_injective _ _
  suffices (σ.comp f).range ≤ f.range by
    let e := (AlgEquiv.ofInjective f hf)
    exact ⟨(e.symm.toAlgHom.comp (Subalgebra.inclusion this)).comp (σ.comp f).rangeRestrict,
      fun x ↦ congr_arg Subtype.val (e.apply_symm_apply ⟨_, _⟩)⟩
  rintro _ ⟨x, rfl⟩
  obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
  cases nonempty_fintype G
  algebraize [(algebraMap (A ⧸ P) k).comp (algebraMap A (A ⧸ P)),
    (algebraMap (B ⧸ Q) k).comp (algebraMap B (B ⧸ Q))]
  have : IsScalarTower A (B ⧸ Q) k := .of_algebraMap_eq fun x ↦
    (IsScalarTower.algebraMap_apply (A ⧸ P) (B ⧸ Q) k (mk P x))
  have : IsScalarTower A B k := .of_algebraMap_eq fun x ↦
    (IsScalarTower.algebraMap_apply (A ⧸ P) (B ⧸ Q) k (mk P x))
  obtain ⟨P, hp⟩ := Algebra.IsInvariant.charpoly_mem_lifts A B G x
  have : Polynomial.aeval x P = 0 := by
    rw [Polynomial.aeval_def, ← Polynomial.eval_map,
      ← Polynomial.coe_mapRingHom (R := A), hp, MulSemiringAction.eval_charpoly]
  have : Polynomial.aeval (σ (algebraMap (B ⧸ Q) k (mk _ x))) P = 0 := by
    refine (DFunLike.congr_fun (Polynomial.aeval_algHom ((σ.restrictScalars A).comp
      (IsScalarTower.toAlgHom A (B ⧸ Q) k)) _) P).trans ?_
    rw [AlgHom.comp_apply, ← algebraMap_eq, Polynomial.aeval_algebraMap_apply, this,
      map_zero, map_zero]
  rw [← Polynomial.aeval_map_algebraMap B, ← Polynomial.coe_mapRingHom, hp] at this
  obtain ⟨τ, hτ⟩ : ∃ τ : G, σ (algebraMap _ _ x) = algebraMap _ _ (τ • x) := by
    simpa [MulSemiringAction.charpoly, sub_eq_zero, Finset.prod_eq_zero_iff] using! this
  exact ⟨Ideal.Quotient.mk _ (τ • x), hτ.symm⟩

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

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁸ : Group G
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsFractionRing B L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : MulSemiringAction G B
inst✝³ : MulSemiringAction G L
inst✝² : SMulDistribClass G B L
hAB : Algebra.IsInvariant A B G
inst✝¹ : SMulCommClass G A B
inst✝ : Algebra.IsIntegral A B
hc : ∀ (a : A), (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) ((algebraMap A B) a)
this✝ : Nontrivial A
this : Nontrivial B
x y : B
hy : y ∈ nonZeroDivisors B
h : ∀ (g : G), g • ((algebraMap B L) x / (algebraMap B L) y) = (algebraMap B L) x / (algebraMap B L) y
hy' : (algebraMap B L) y ≠ 0
⊢ ∃ a, (algebraMap K L) a = (algebraMap B L) x / (algebraMap B L) y

Tactic:
obtain ⟨b, a, ha, hb⟩ := (Algebra.IsAlgebraic.isAlgebraic (R := A) y).exists_smul_eq_mul x hy

Goal state after:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁸ : Group G
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsFractionRing B L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : MulSemiringAction G B
inst✝³ : MulSemiringAction G L
inst✝² : SMulDistribClass G B L
hAB : Algebra.IsInvariant A B G
inst✝¹ : SMulCommClass G A B
inst✝ : Algebra.IsIntegral A B
hc : ∀ (a : A), (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) ((algebraMap A B) a)
this✝ : Nontrivial A
this : Nontrivial B
x y : B
hy : y ∈ nonZeroDivisors B
h : ∀ (g : G), g • ((algebraMap B L) x / (algebraMap B L) y) = (algebraMap B L) x / (algebraMap B L) y
hy' : (algebraMap B L) y ≠ 0
b : B
a : A
ha : a ≠ 0
hb : a • x = y * b
⊢ ∃ a, (algebraMap K L) a = (algebraMap B L) x / (algebraMap B L) y
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case neg
α : 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 (∏ m ∈ (normalizedFactors a).toFinset, id m ^ Multiset.count m (normalizedFactors a))

Tactic:
refine induction_on_prime_power _ _ ?_ ?_ @h1 @hpr @hcp <;> simp only [Multiset.mem_toFinset]

Goal state after:
case neg.refine_1
α : 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, Prime p

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
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case hfg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ∀ (x : { x // x ∈ (minpoly R pb.gen).aroots F }), ↑x = _root_.id ↑x

Tactic:
· intro x; rfl

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed[inst✝] Z
H' : ((closure[inst✝] (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
this : ((closure[inst✝] (Z ∩ closedPoints X))ᶜ ∩ Z ∩ closedPoints X).Nonempty
⊢ False

Tactic:
rw [Set.nonempty_iff_ne_empty, Set.inter_assoc, ne_eq,
      ← Set.disjoint_iff_inter_eq_empty, Set.disjoint_compl_left_iff_subset] at this

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed[inst✝] Z
H' : ((closure[inst✝] (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
this : ¬Z ∩ closedPoints X ⊆ closure[inst✝] (Z ∩ closedPoints X)
⊢ False
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: case refine_2
R₀ : Type u_1
R : Type u_2
M✝ : Type u
inst✝⁹ : Ring R₀
inst✝⁸ : Ring R
inst✝⁷ : Module R₀ R
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R₀ M✝
inst✝⁴ : Module R M✝
inst✝³ : IsScalarTower R₀ R M✝
inst✝² : IsSemiprimaryRing R
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  IsNoetherian R ↥(Ring.jacobson R • ⊤) ∨ IsArtinian R ↥(Ring.jacobson R • ⊤) → Module.Finite R₀ ↥(Ring.jacobson R • ⊤)
hq :
  IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ∨ IsArtinian R (M ⧸ Ring.jacobson R • ⊤) →
    Module.Finite R₀ (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (Ring.jacobson R • ⊤)
this : Module.Finite R₀ ↥N
⊢ Module.Finite R₀ M

Tactic:
have : Module.Finite R₀ (M ⧸ N) := by refine hq (h.imp ?_ ?_) <;> (intro; infer_instance)

Goal state after:
case refine_2
R₀ : Type u_1
R : Type u_2
M✝ : Type u
inst✝⁹ : Ring R₀
inst✝⁸ : Ring R
inst✝⁷ : Module R₀ R
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R₀ M✝
inst✝⁴ : Module R M✝
inst✝³ : IsScalarTower R₀ R M✝
inst✝² : IsSemiprimaryRing R
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  IsNoetherian R ↥(Ring.jacobson R • ⊤) ∨ IsArtinian R ↥(Ring.jacobson R • ⊤) → Module.Finite R₀ ↥(Ring.jacobson R • ⊤)
hq :
  IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ∨ IsArtinian R (M ⧸ Ring.jacobson R • ⊤) →
    Module.Finite R₀ (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (Ring.jacobson R • ⊤)
this✝ : Module.Finite R₀ ↥N
this : Module.Finite R₀ (M ⧸ N)
⊢ Module.Finite R₀ M
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case e'_3
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ ↑(U i)
y : ↥(U i)
hy : y ∈ Subtype.val ⁻¹' Z
hy' : y ∈ closedPoints ↥(U i)
j : ι
h : ↑y ∉ U j
z : ↥(U j)
hz : ↑z = ↑y
⊢ False

Tactic:
exact h (hz ▸ z.2)

Goal state after: