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

Goal state before:
pp: α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y : Set α
⊢ M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y

Tactic:
obtain ⟨Ii, hIi⟩ := M.exists_isBasis' (X ∩ Y)
  obtain ⟨IX, hIX, hIX'⟩ :=
    hIi.indep.subset_isBasis'_of_subset (hIi.subset.trans inter_subset_left)
  obtain ⟨IY, hIY, hIY'⟩ :=
    hIi.indep.subset_isBasis'_of_subset (hIi.subset.trans inter_subset_right)
  rw [← cRk_union_closure_eq, ← hIX.closure_eq_closure, ← hIY.closure_eq_closure,
    cRk_union_closure_eq, ← hIi.cardinalMk_eq_cRk, ← hIX.cardinalMk_eq_cRk,
    ← hIY.cardinalMk_eq_cRk, ← mk_union_add_mk_inter, add_comm]
  exact add_le_add (M.cRk_le_cardinalMk _) (mk_le_mk_of_subset (subset_inter hIX' hIY'))

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

Goal state before:
pp: α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e ∈ insert f I
⊢ M.Indep (insert f I \ {e})

Tactic:
by
  simp only [mem_insert_iff] at heI
  obtain rfl | heI := heI
  · exact hI.subset (by simp)
  rw [Indep.insert_sdiff_indep_iff (hI.subset (sdiff_subset ..)) heI]
  refine .inl ⟨mem_ground_of_mem_closure hfI, fun h ↦ hI.notMem_closure_sdiff_of_mem heI ?_⟩
  exact closure_insert_eq_of_mem_closure h ▸ M.closure_subset_closure (by intro; simp_all) he

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
f : ι → MvPolynomial ι R
H : AlgebraicIndependent R fun i ↦ (aeval x) (f i)
⊢ AlgebraicIndependent R f

Tactic:
by
  rw [algebraicIndependent_iff] at H ⊢
  intro p hp
  exact H p (by rw [← aeval_comp_bind₁, AlgHom.comp_apply, bind₁, hp, map_zero])

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

Goal state before:
pp: σ : Type u_3
R : Type u_4
inst✝ : CommRing R
⊢ AlgebraicIndependent R X

Tactic:
AlgebraicIndependent,

Goal state after:
σ : Type u_3
R : Type u_4
inst✝ : CommRing R
⊢ Injective ⇑(aeval X)
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: case pos
ι : 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
e : MvPolynomial (ι' ⊕ ι) R ≃ₐ[R] MvPolynomial ι' ↥(adjoin R (range x)) :=
  (sumAlgEquiv R ι' ι).trans (mapAlgEquiv ι' hx.aevalEquiv)
this : aeval (Sum.elim y x) = (AlgHom.restrictScalars R (aeval y)).comp ↑e
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ True ∧ AlgebraicIndependent (↥(adjoin R (range x))) y

Tactic:
AlgebraicIndependent,

Goal state after:
case pos
ι : 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
e : MvPolynomial (ι' ⊕ ι) R ≃ₐ[R] MvPolynomial ι' ↥(adjoin R (range x)) :=
  (sumAlgEquiv R ι' ι).trans (mapAlgEquiv ι' hx.aevalEquiv)
this : aeval (Sum.elim y x) = (AlgHom.restrictScalars R (aeval y)).comp ↑e
⊢ Injective ⇑(aeval (Sum.elim y x)) ↔ True ∧ Injective ⇑(aeval y)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case refine_2.inr
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
⊢ False

Tactic:
have heJI : e ∈ J \ I := by
    rw [← union_sdiff_right, union_comm]
    exact ⟨heI, notMem_subset hK heK⟩

Goal state after:
case refine_2.inr
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
heJI : e ∈ J \ I
⊢ False
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
hT : T ⊆ M.E
⊢ M.E ⊆ M.closure T

Tactic:
rw [← hS.closure_eq]; exact M.closure_subset_closure hST

Goal state after:
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i ↦ ↑i) → s.card ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ t.card ≤ n

Tactic:
← Finset.card_map (Embedding.subtype (· ∈ s))

Goal state after:
R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i ↦ ↑i) → s.card ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ (Finset.map (Embedding.subtype fun x ↦ x ∈ s) t).card ≤ n
Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
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 S
hx : AlgebraicIndependent R x
inst✝ : Algebra.IsIntegral R S
⊢ AlgebraicIndependent S x

Tactic:
nontriviality S
  have := Module.nontrivial R S
  exact hx.extendScalars S

Goal state after:
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
inst✝ : NoZeroDivisors A
hx : IsTranscendenceBasis R x
this : FaithfulSMul R A
⊢ lift.{w, u} #ι = lift.{u, w} (matroid R A).cRank

Tactic:
← (matroid_isBase_iff.mpr hx.to_subtype_range).cardinalMk_eq_cRank,

Goal state after:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
hx : IsTranscendenceBasis R x
this : FaithfulSMul R A
⊢ lift.{w, u} #ι = lift.{u, w} #↑(range x)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
his : v i ∈ v '' s
⊢ v j ∈ (matroid R S).closure (v '' s \ {v j})

Tactic:
refine Matroid.closure_subset_closure _ ?_ H₂

Goal state after:
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
his : v i ∈ v '' s
⊢ v '' (insert i s \ {j}) ⊆ v '' s \ {v j}
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
⊢ IsTopologicalGroup G

Tactic:
let := B.topology
  have basis := B.nhds_one_hasBasis
  have basis' := basis.prod basis
  refine IsTopologicalGroup.of_nhds_one ?_ ?_ ?_ ?_
  · rw [basis'.tendsto_iff basis]
    suffices ∀ U ∈ B, ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ a b, a ∈ V → b ∈ W → a * b ∈ U by simpa
    intro U U_in
    rcases mul U_in with ⟨V, V_in, hV⟩
    refine ⟨V, V, ⟨V_in, V_in⟩, ?_⟩
    intro a b a_in b_in
    exact hV <| mul_mem_mul a_in b_in
  · rw [basis.tendsto_iff basis]
    intro U U_in
    simpa using! inv U_in
  · intro x₀
    rw [nhds_eq, nhds_one_eq]
    rfl
  · intro x₀
    rw [basis.tendsto_iff basis]
    intro U U_in
    exact conj x₀ U_in

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

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
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : separableClosure E K = ⊥
y : E
hx : (algebraMap E K) y ∈ separableClosure F K
⊢ (algebraMap E K) y ∈ IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E)

Tactic:
exact ⟨y, (map_mem_separableClosure_iff <| IsScalarTower.toAlgHom F E K).mp hx, rfl⟩

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : IsSplittingField F E p
hp : p.Separable
⊢ Algebra.IsSeparable F E

Tactic:
← isSeparable_top,

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : IsSplittingField F E p
hp : p.Separable
⊢ Algebra.IsSeparable F ↥⊤
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, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n

Tactic:
have := expChar_of_injective_algebraMap (algebraMap F E).injective q

Goal state after:
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
⊢ (minpoly F x).natSepDegree = 1 ↔ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
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 : fixedField ⊤ = ⊥
⊢ IsGalois F E

Tactic:
rw [← isGalois_iff_isGalois_bot, ← h]

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 : fixedField ⊤ = ⊥
⊢ IsGalois (↥(fixedField ⊤)) E
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
⊢ finSepDegree F ↥F⟮α⟯ = (minpoly F α).natSepDegree

Tactic:
have : finSepDegree F F⟮α⟯ = _ := Nat.card_congr
    (algHomAdjoinIntegralEquiv F (K := AlgebraicClosure F⟮α⟯) halg.isIntegral)

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
this : finSepDegree F ↥F⟮α⟯ = Nat.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) }
⊢ finSepDegree F ↥F⟮α⟯ = (minpoly F α).natSepDegree
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
σ : Gal(L/K)
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑σ.symm) E
g : Gal(L/K)
hg : g ∈ F.fixingSubgroup.carrier
x : L
hx : x ∈ E
⊢ ↑↑σ.symm x = σ⁻¹ x

Tactic:
dsimp

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

Goal state before:
pp: case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H✝ : (minpolyDiv R x).coeff i ∉ R[x]
j : ℕ
IH : (minpolyDiv R x).coeff (i + j) ∉ R[x]
H : (minpolyDiv R x).coeff (i + (j + 1)) ∈ R[x]
⊢ (algebraMap R S) ((minpoly R x).coeff (i + j + 1)) ∈ R[x]

Tactic:
exact Subalgebra.algebraMap_mem _ _

Goal state after:
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
hdeg : f.degree ≠ 0
⊢ ∃ x, a * x ^ n + b * x + c = 0

Tactic:
have hsep : f.Separable := separable_C_mul_X_pow_add_C_mul_X_add_C a b c hn hb.isUnit

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
hdeg : f.degree ≠ 0
hsep : f.Separable
⊢ ∃ x, a * x ^ n + b * x + c = 0
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly

Goal state before:
pp: case inr.hp
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ (aeval h.gen) ((leftMulMatrix h.basis) h.gen).charpoly = 0

pp: case inr.hl
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ ∀ (q : R[X]), q.degree < ((leftMulMatrix h.basis) h.gen).charpoly.degree → q = 0 ∨ (aeval h.gen) q ≠ 0

Tactic:
· apply (injective_iff_map_eq_zero (G := S) (leftMulMatrix _)).mp
      (leftMulMatrix_injective h.basis)
    rw [← Polynomial.aeval_algHom_apply, aeval_self_charpoly]

Goal state after:
case inr.hl
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ ∀ (q : R[X]), q.degree < ((leftMulMatrix h.basis) h.gen).charpoly.degree → q = 0 ∨ (aeval h.gen) q ≠ 0
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
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : IsPurelyInseparable F K
q : ℕ
h✝ : ExpChar F q
⊢ IsPurelyInseparable E K

Tactic:
have := expChar_of_injective_algebraMap (algebraMap F E).injective q

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
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : IsPurelyInseparable F K
q : ℕ
h✝ : ExpChar F q
this : ExpChar E q
⊢ IsPurelyInseparable E K
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
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h1 : IsPurelyInseparable F E
h2 : IsPurelyInseparable E K
q : ℕ
h✝ : ExpChar F q
⊢ IsPurelyInseparable F K

Tactic:
have := expChar_of_injective_algebraMap (algebraMap F E).injective q

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
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h1 : IsPurelyInseparable F E
h2 : IsPurelyInseparable E K
q : ℕ
h✝ : ExpChar F q
this : ExpChar E q
⊢ IsPurelyInseparable F K
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
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
p : ℕ
inst✝ : ExpChar A p
x : R
⊢ (algebraMap R A) x ^ p ^ 0 ∈ (algebraMap R A).rangeS

Tactic:
by rw [pow_zero, pow_one]; exact ⟨x, rfl⟩

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

Goal state before:
pp: case inr
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
x : R ⊗[k] K
a✝ : Nontrivial (R ⊗[k] K)
inst✝ : ExpChar k 1
⊢ ∃ n, x ^ 1 ^ n ∈ (algebraMap R (R ⊗[k] K)).range

Tactic:
have : CharZero k := charZero_of_expChar_one' k

Goal state after:
case inr
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
x : R ⊗[k] K
a✝ : Nontrivial (R ⊗[k] K)
inst✝ : ExpChar k 1
this : CharZero k
⊢ ∃ n, x ^ 1 ^ n ∈ (algebraMap R (R ⊗[k] K)).range
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : 𝓞 K
hx : (algebraMap (𝓞 K) (𝓞 L)) x = 0
⊢ x = 0

Tactic:
have h : (algebraMap K L) x = (algebraMap (𝓞 K) (𝓞 L)) x := rfl
  simp only [hx, map_zero, map_eq_zero, RingOfIntegers.coe_eq_zero_iff] at h
  exact h

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

Goal state before:
pp: B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
⊢ eval b (charpoly G b) = 0

Tactic:
charpoly_eq,

Goal state after:
B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
⊢ eval b (∏ g, (X - C (g • b))) = 0
Module: Mathlib.RingTheory.IsGaloisGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝⁹ : Group G
H : Subgroup G
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁸ : CommSemiring A
inst✝⁷ : Semiring C
inst✝⁶ : Algebra A C
inst✝⁵ : MulSemiringAction G C
N : Subgroup G
inst✝⁴ : CommSemiring B
inst✝³ : Algebra B C
inst✝² : FaithfulSMul B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
this : MulSemiringAction G B := mulSemiringActionOfNormal G B C N
q : G ⧸ N
x : B
g₁ g₂ : G
h : (QuotientGroup.leftRel N) g₁ g₂
⊢ g₁ • x = g₂ • x

Tactic:
by
      apply FaithfulSMul.algebraMap_injective B C
      rw [algebraMap.smul', algebraMap.smul', smul_eq_iff_eq_inv_smul, ← smul_assoc, smul_eq_mul,
        Subgroup.smul_algebraMap C (by rwa [← QuotientGroup.leftRel_apply])]

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

Goal state before:
pp: case neg
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing 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 ((trace A C) x) = (trace B C) x

Tactic:
rw [trace_eq_zero_of_not_exists_basis _ h, trace_eq_zero_of_not_exists_basis,
    LinearMap.zero_apply, LinearMap.zero_apply, map_zero]

Goal state after:
case neg.h
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing 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)
⊢ ¬∃ s, Nonempty (Basis (↥s) A C)
Module: Mathlib.RingTheory.Int.Basic

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

Tactic:
Int.natAbs_pow

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
⊢ x ^ p = x

Tactic:
have h := FiniteField.pow_card x

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
h : x ^ Fintype.card (ZMod p) = x
⊢ x ^ p = x
Module: Mathlib.RingTheory.ZMod

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Ring R
f g : R →+* ZMod n
h : RingHom.ker f = RingHom.ker g
this : ((f.liftOfRightInverse cast ⋯) ⟨g, ⋯⟩).comp f = ↑⟨g, ⋯⟩
⊢ f = g

Tactic:
rw [Subtype.coe_mk] at this

Goal state after:
n : ℕ
R : Type u_1
inst✝ : Ring R
f g : R →+* ZMod n
h : RingHom.ker f = RingHom.ker g
this : ((f.liftOfRightInverse cast ⋯) ⟨g, ⋯⟩).comp f = g
⊢ f = g
Module: Mathlib.LinearAlgebra.Quotient.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ Function.RightInverse (invFun p) (toFun p)

Tactic:
by
  dsimp only [toFun, invFun]
  rw [Function.rightInverse_iff_comp, ← coe_comp, ← @id_coe R]
  congr
  refine pi_ext fun i x ↦ ?_
  induction x using Submodule.Quotient.induction_on with | _ x'
  refine funext fun j ↦ ?_
  rw [comp_apply, piQuotientLift_single, mapQ_apply,
    quotientPiLift_mk, id_apply]
  by_cases hij : i = j <;> simp only [mkQ_apply, coe_single]
  · subst hij
    rw [Pi.single_eq_same, Pi.single_eq_same]
  · rw [Pi.single_eq_of_ne (Ne.symm hij), Pi.single_eq_of_ne (Ne.symm hij), Quotient.mk_zero]

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

Goal state before:
pp: case refine_1
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
f : B ⧸ Q →ₐ[A ⧸ P] k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective ⇑f
τ₁ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q
h₁ : ∀ (x : B ⧸ Q), (algebraMap (B ⧸ Q) k) (τ₁ x) = ↑σ ((algebraMap (B ⧸ Q) k) x)
τ₂ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q
h₂ : ∀ (x : B ⧸ Q), (algebraMap (B ⧸ Q) k) (τ₂ x) = ↑σ.symm ((algebraMap (B ⧸ Q) k) x)
x : B
⊢ τ₂ ((↑↑τ₁.toRingHom).toFun ((mk Q) x)) = (mk Q) x

Tactic:
obtain ⟨y, e⟩ := Ideal.Quotient.mk_surjective (τ₁ (Ideal.Quotient.mk Q x))

Goal state after:
case refine_1
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
f : B ⧸ Q →ₐ[A ⧸ P] k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective ⇑f
τ₁ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q
h₁ : ∀ (x : B ⧸ Q), (algebraMap (B ⧸ Q) k) (τ₁ x) = ↑σ ((algebraMap (B ⧸ Q) k) x)
τ₂ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q
h₂ : ∀ (x : B ⧸ Q), (algebraMap (B ⧸ Q) k) (τ₂ x) = ↑σ.symm ((algebraMap (B ⧸ Q) k) x)
x y : B
e : (mk Q) y = τ₁ ((mk Q) x)
⊢ τ₂ ((↑↑τ₁.toRingHom).toFun ((mk Q) x)) = (mk Q) x
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
this : 0 < Nat.card F / 2
m : ℕ
h : (fun x ↦ g ^ x) (2 * m) ^ (Nat.card F / 2) = 1
key : 2 * (Nat.card F / 2) ∣ 2 * m * (Nat.card F / 2)
⊢ (fun x ↦ g ^ x) (2 * m) = g ^ m * g ^ m

Tactic:
dsimp

Goal state after:
case mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
this : 0 < Nat.card F / 2
m : ℕ
h : (fun x ↦ g ^ x) (2 * m) ^ (Nat.card F / 2) = 1
key : 2 * (Nat.card F / 2) ∣ 2 * m * (Nat.card F / 2)
⊢ g ^ (2 * m) = g ^ m * g ^ m