mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Flat R M
inst✝⁴ : Module.Finite R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Finite R N
inst✝ : Flat R N
p : PrimeSpectrum R
e : Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
  Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N) :=
  (AlgebraTensorModule.assoc R R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal) M N).symm ≪≫ₗ
    (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal)
        (Localization.AtPrime p.asIdeal ⊗[R] M) N).symm
⊢ rankAtStalk M p * rankAtStalk N p = (rankAtStalk M * rankAtStalk N) p

Tactic:
Pi.mul_apply

Goal state after:
R : Type uR
M : Type uM
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Flat R M
inst✝⁴ : Module.Finite R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Finite R N
inst✝ : Flat R N
p : PrimeSpectrum R
e : Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
  Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N) :=
  (AlgebraTensorModule.assoc R R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal) M N).symm ≪≫ₗ
    (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal)
        (Localization.AtPrime p.asIdeal ⊗[R] M) N).symm
⊢ rankAtStalk M p * rankAtStalk N p = rankAtStalk M p * rankAtStalk N p
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
M : IndepMatroid α
I : Set α
h : M.Indep I
J : Set α
hIJ : I ⊆ J
hmax : Maximal (fun K ↦ M.Indep K ∧ K ⊆ M.E) J
⊢ ∃ B, Maximal M.Indep B ∧ I ⊆ B

Tactic:
rw [maximal_and_iff_right_of_imp M.subset_ground] at hmax

Goal state after:
α : Type u_1
M : IndepMatroid α
I : Set α
h : M.Indep I
J : Set α
hIJ : I ⊆ J
hmax : Maximal M.Indep J ∧ J ⊆ M.E
⊢ ∃ B, Maximal M.Indep B ∧ I ⊆ B
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ B
hI : M.Indep (insert f B \ {e})
hfe : f ≠ e
⊢ M.IsBase (insert f B \ {e})

Tactic:
← insert_sdiff_singleton_comm hfe

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
hfe : f ≠ e
⊢ M.IsBase (insert f (B \ {e}))
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), (Polynomial.map (algebraMap F A) (minpoly F x)).Splits
α : E
⊢ ((minpoly F α).rootSet A).toFinset.card = finrank F E ↔ Function.Injective fun φ ↦ φ α

Tactic:
← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,

Goal state after:
F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), (Polynomial.map (algebraMap F A) (minpoly F x)).Splits
α : E
⊢ (range fun ψ ↦ ψ α).toFinset.card = finrank F E ↔ Function.Injective fun ψ ↦ ψ α
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R X : Set α
⊢ (M ↾ R).Dep X ↔ ¬M.Indep X ∧ X ⊆ R

Tactic:
rw [Dep, restrict_indep_iff, restrict_ground_eq]

Goal state after:
α : Type u_1
M : Matroid α
R X : Set α
⊢ ¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N <r M
⊢ N = M ↾ N.E

Tactic:
by rw [h.eq_restrict]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : SurjOn f E N.E
⊢ (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ InjOn f B ∧ B ⊆ E

Tactic:
simp_rw [comapOn_isBase_iff, and_congr_left_iff, and_imp, isBasis'_iff_isBasis_inter_ground,
    inter_eq_self_of_subset_right h, isBasis_ground_iff, implies_true]

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

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.IsCircuit {e, f}
hclosure : M.closure ({e, f} \ {e}) = M.closure ({e, f} \ {f})
⊢ M.closure {e} = M.closure {f}

Tactic:
rwa [pair_sdiff_left hef, pair_sdiff_right hef, eq_comm] at hclosure

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
⊢ ∀ (i : ↑X), M.IsCircuit (C ↑i)

Tactic:
simpa using fun e heX ↦ hCS _ <| hC.1 e heX

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

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.E
⊢ e ∉ M.closure I ↔ M.Indep (insert e I)

Tactic:
rw [hI.notMem_closure_iff, and_iff_left heI]

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

Goal state before:
pp: α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
I₀ : Set α
hI₀ss : I₀ ⊆ f ⁻¹' I ∩ X
hbij : BijOn f I₀ (f '' (f ⁻¹' I ∩ X))
⊢ f '' I₀ = I

Tactic:
hbij.image_eq,

Goal state after:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
I₀ : Set α
hI₀ss : I₀ ⊆ f ⁻¹' I ∩ X
hbij : BijOn f I₀ (f '' (f ⁻¹' I ∩ X))
⊢ f '' (f ⁻¹' I ∩ X) = I
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.removeLoops.IsBasis' = M.IsBasis'

Tactic:
by
  ext
  simp [IsBasis']

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
⊢ M.removeLoops.IsBase B ↔ M.IsBase B

Tactic:
rw [isBase_iff_maximal_indep, removeLoops_indep_eq, isBase_iff_maximal_indep]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.closure (M.E \ K ∪ insert e C) ⊆ M.closure (M.E \ K)

Tactic:
insert_eq_of_mem heC,

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.closure (M.E \ K ∪ C) ⊆ M.closure (M.E \ K)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ {e} ⊆ M.E

Tactic:
rw [← he]

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ C ∩ K ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
X : Set α
⊢ M.IsRkFinite X ↔ M.cRk X < ℵ₀

Tactic:
rw [IsRkFinite, rankFinite_iff_cRank_lt_aleph0, cRank_restrict]

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ⇑f ↑(adjoin R (range x))
⊢ AlgebraicIndependent R (⇑f ∘ x)

Tactic:
have : aeval (f ∘ x) = f.comp (aeval x) := by ext; simp
  have h : ∀ p : MvPolynomial ι R, aeval x p ∈ (@aeval R _ _ _ _ _ ((↑) : range x → A)).range := by
    intro p
    rw [AlgHom.mem_range]
    refine ⟨MvPolynomial.rename (codRestrict x (range x) mem_range_self) p, ?_⟩
    simp [Function.comp_def, aeval_rename]
  intro x y hxy
  rw [this] at hxy
  rw [adjoin_eq_range] at hf_inj
  exact hx (hf_inj (h x) (h y) hxy)

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

Goal state before:
pp: case e'_2
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
i : ι
h : i ∉ s
⊢ Transcendental (↥(adjoin R (x '' s))) (x i) ↔ Transcendental (↥(adjoin R (range fun i ↦ x ↑i))) (x i)

Tactic:
· rw [Set.image_eq_range]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
⊢ M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I

Tactic:
by
  rw [indep_iff_forall_notMem_closure_sdiff']
  refine ⟨fun ⟨hIE, h⟩ e heI h_eq ↦ h e heI (h_eq.symm.subset (M.mem_closure_of_mem heI)),
    fun h ↦ ⟨fun e heI ↦ by_contra fun heE ↦ h heI ?_,fun e heI hin ↦ h heI ?_⟩⟩
  · rw [← closure_inter_ground, inter_comm, inter_sdiff_distrib_left,
      inter_singleton_eq_empty.mpr heE, sdiff_empty, inter_comm, closure_inter_ground]
  nth_rw 2 [show I = insert e (I \ {e}) by simp [heI]]
  rw [← closure_insert_closure_eq_closure_insert, insert_eq_of_mem hin, closure_closure]

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

Goal state before:
pp: ι : Type u
ι' : 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✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
this✝¹ : Nontrivial S
this✝ : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this : Algebra.IsAlgebraic (↥Sy) A
⊢ Algebra ↥Rxy ↥Sy

Tactic:
refine (Subalgebra.inclusion (T := Sy.restrictScalars Rx) <| adjoin_le ?_).toAlgebra
    rintro _ ⟨i, rfl⟩; exact subset_adjoin (s := range y) ⟨i, rfl⟩

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

Goal state before:
pp: 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 A
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis R Subtype.val
t : Set A
ht : IsTranscendenceBasis S Subtype.val
this✝ : NoZeroDivisors S
this : Nontrivial S
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)

Tactic:
rw [← hs.cardinalMk_eq_trdeg, ← ht.cardinalMk_eq_trdeg, ← lift_umax.{w}, add_comm,
    ← (hs.sumElim_comp ht).lift_cardinalMk_eq_trdeg, mk_sum, lift_add, lift_lift, lift_lift]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
⊢ Infinite (Emb F ↥(adjoin F (Set.range x)))

Tactic:
← (embEquivOfEquiv _ _ _ hx.1.aevalEquivField).infinite_iff

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
⊢ Infinite (Emb F (FractionRing (MvPolynomial ι F)))
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
inst✝ : FiniteDimensional F E
h : Nat.card Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
⊢ finrank F ↥(fixedField ⊤) * finrank (↥(fixedField ⊤)) E = 1 * finrank (↥(fixedField ⊤)) E

Tactic:
finrank_mul_finrank,

Goal state after:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Nat.card Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
⊢ finrank F E = 1 * finrank (↥(fixedField ⊤)) E
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
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
this✝ : ExpChar E q
this : ExpChar E[X] q
h : (minpoly F x).natSepDegree = 1
⊢ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n

Tactic:
obtain ⟨n, y, h⟩ := (natSepDegree_eq_one_iff_eq_X_pow_sub_C q).1 h
    have hx := congr_arg (Polynomial.aeval x) h.symm
    rw [minpoly.aeval, map_sub, map_pow, aeval_X, aeval_C, sub_eq_zero, eq_comm] at hx
    use n
    rw [h, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, hx, map_pow,
      ← sub_pow_expChar_pow_of_commute _ _ (commute_X _)]

Goal state after:
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
s : Set Gal(L/K)
x✝ : ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s
E : IntermediateField K L
left✝ : FiniteDimensional K ↥E
hE : ↑E.fixingSubgroup ⊆ s
⊢ FiniteDimensional K ↥(IntermediateField.normalClosure K (↥E) L) ∧
    Normal K ↥(IntermediateField.normalClosure K (↥E) L) ∧
      ↑(IntermediateField.normalClosure K (↥E) L).fixingSubgroup ⊆ s

Tactic:
simp only [normalClosure.is_finiteDimensional K E L, normalClosure.normal K E L, true_and]

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
s : Set Gal(L/K)
x✝ : ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s
E : IntermediateField K L
left✝ : FiniteDimensional K ↥E
hE : ↑E.fixingSubgroup ⊆ s
⊢ ↑(IntermediateField.normalClosure K (↥E) L).fixingSubgroup ⊆ s
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K L : IntermediateField F E
inst✝³ : Normal F ↥K
inst✝² : FiniteDimensional F ↥K
inst✝¹ : FiniteDimensional (↥L) E
inst✝ : IsGalois (↥L) E
h : K ⊓ L = ⊥
x✝ : ↥K
x : E
hx₁ : x ∈ K
hx₂ : ⟨x, hx₁⟩ ∈ fixedField (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E).range
φ : Gal(E/↥L)
⊢ ↑(((restrictRestrictAlgEquivMapHom F (↥K) (↥L) E) φ) ⟨x, hx₁⟩) = x

Tactic:
rw [mem_fixedField_iff] at hx₂

Goal state after:
F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K L : IntermediateField F E
inst✝³ : Normal F ↥K
inst✝² : FiniteDimensional F ↥K
inst✝¹ : FiniteDimensional (↥L) E
inst✝ : IsGalois (↥L) E
h : K ⊓ L = ⊥
x✝ : ↥K
x : E
hx₁ : x ∈ K
hx₂ : ∀ f ∈ (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E).range, f ⟨x, hx₁⟩ = ⟨x, hx₁⟩
φ : Gal(E/↥L)
⊢ ↑(((restrictRestrictAlgEquivMapHom F (↥K) (↥L) E) φ) ⟨x, hx₁⟩) = x
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: case mp
F : Type u_1
E : Type u_2
E' : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E
inst✝³ : Algebra F E'
inst✝² : Algebra E E'
inst✝¹ : IsScalarTower F E E'
L : IntermediateField F E
inst✝ : Normal F E
f : Gal(E'/F)
⊢ (∀ x ∈ map (IsScalarTower.toAlgHom F E E') L, f x = x) → ∀ x ∈ L, ((restrictNormalHom E) f) x = x

Tactic:
rintro h x hx
    change f.restrictNormal E x = x
    apply_fun _ using (algebraMap E E').injective
    rw [AlgEquiv.restrictNormal_commutes]
    exact h _ ⟨x, hx, rfl⟩

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

Goal state before:
pp: case a
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
⊢ ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range (minpoly R x).natDegree)) ⊆
    ↑(Submodule.span R (Set.range (minpolyDiv R x).coeff))

Tactic:
simp only [Finset.coe_image, Finset.coe_range, Set.image_subset_iff]

Goal state after:
case a
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
⊢ Set.Iio (minpoly R x).natDegree ⊆ (fun x_1 ↦ x ^ x_1) ⁻¹' ↑(Submodule.span R (Set.range (minpolyDiv R x).coeff))
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
⊢ f.natDegree ≠ 0

Tactic:
have : C 0 * X ^ n + C b * X = 0 * X ^ n + C b * X := by grind

Goal state after:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
this : C 0 * X ^ n + C b * X = 0 * X ^ n + C b * X
⊢ f.natDegree ≠ 0
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
this : C 0 * X ^ n + C b * X = 0 * X ^ n + C b * X
ha : ¬a = 0
⊢ f.natDegree ≠ 0

Tactic:
grind [natDegree_add_eq_left_of_natDegree_lt]

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✝¹ : 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
h1 : C c * C d * p = integerNormalization R⁰ a * integerNormalization R⁰ b
this : NormalizedGCDMonoid R
⊢ Associated (c * d) (normalize (c * d) * p.content)

Tactic:
hp.content_eq_one,

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✝¹ : 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
h1 : C c * C d * p = integerNormalization R⁰ a * integerNormalization R⁰ b
this : NormalizedGCDMonoid R
⊢ Associated (c * d) (normalize (c * d) * 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
hA : IsGaloisGroup G A B
inst✝ : FaithfulSMul A B
x✝¹ x✝ : A
⊢ ⟨(algebraMap A B) (x✝¹ * x✝), ⋯⟩ = ⟨(algebraMap A B) x✝¹, ⋯⟩ * ⟨(algebraMap A B) x✝, ⋯⟩

Tactic:
simp [Subtype.ext_iff]

Goal state after:
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
hA : IsGaloisGroup G A B
inst✝ : FaithfulSMul A B
x✝¹ x✝ : A
⊢ ⟨(algebraMap A B) (x✝¹ + x✝), ⋯⟩ = ⟨(algebraMap A B) x✝¹, ⋯⟩ + ⟨(algebraMap A B) x✝, ⋯⟩

Tactic:
simp [Subtype.ext_iff]

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
x : L
⊢ finrank (↥K⟮x⟯) L • -(minpoly K x).nextCoeff = ↑(finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff

Tactic:
Algebra.smul_def

Goal state after:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
⊢ (algebraMap ℕ K) (finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff = ↑(finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
⊢ ((leftMulMatrix b) x).det = 0 → x = 0

Tactic:
← Matrix.exists_mulVec_eq_zero_iff

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
⊢ (∃ v, v ≠ 0 ∧ (leftMulMatrix b) x *ᵥ v = 0) → x = 0
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
r : S
s : Set S
⊢ absNorm (span {r}) ∣ ((Algebra.norm ℤ) r).natAbs

Tactic:
rw [absNorm_span_singleton]

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
inst✝ : CharZero S
n : ℕ
this : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
⊢ {I | absNorm ↑I ≤ n}.Finite

Tactic:
exact Finite.of_equiv _ (Equiv.subtypeSubtypeEquivSubtypeInter _ (fun I ↦ absNorm I ≤ n)).symm

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst✝², inst✝¹] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
x : Y
hx : x ∈ f '' (S ∩ closedPoints X)
⊢ IsClosed[inst✝¹] {x}

Tactic:
exact H₂ hx

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
x : S
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ Nat.Prime ((Algebra.norm ℤ) x).natAbs

Tactic:
← Int.prime_iff_natAbs_prime

Goal state after:
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
x : S
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ Prime ((Algebra.norm ℤ) x)