mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case zero.refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ b * a ∈ ⊥

Tactic:
← hn

Goal state after:
case zero.refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ b * a ∈ derivedSeries G 0
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type u_7
T : Type u_8
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* S
g : S →+* T
⊢ (mapRingHom g).comp (mapRingHom f) = mapRingHom (g.comp f)

Tactic:
by
  algebraize [f, g, g.comp f]
  simp_rw [mapRingHom, mapAlgebra_comp_mapAlgebra]

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
E : IntermediateField F K
inst✝ : Normal F ↥E
f : ↥E →ₐ[F] K
⊢ f.fieldRange = E

Tactic:
let g := f.restrictNormal' E

Goal state after:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
E : IntermediateField F K
inst✝ : Normal F ↥E
f : ↥E →ₐ[F] K
g : Gal(↥E/F) := f.restrictNormal' ↥E
⊢ f.fieldRange = E
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := ⋯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ F⟮α, β⟯ ≤ F⟮α + x • β⟯

pp: case a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := ⋯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ F⟮α + x • β⟯ ≤ F⟮α, β⟯

Tactic:
· rw [adjoin_le_iff]
    have αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯ := mem_adjoin_simple_self F _
    have αyβ_in_K : α + y • β ∈ F⟮α + y • β⟯ := mem_adjoin_simple_self F _
    dsimp [f] at *
    simp only [← heq] at αyβ_in_K
    have β_in_K := sub_mem αxβ_in_K αyβ_in_K
    rw [show (α + x • β) - (α + y • β) = (x - y) • β by rw [sub_smul]; abel1] at β_in_K
    replace β_in_K := smul_mem _ β_in_K (x := (x - y)⁻¹)
    rw [smul_smul, inv_mul_eq_div, div_self (sub_ne_zero.2 hneq), one_smul] at β_in_K
    have α_in_K : α ∈ F⟮α + x • β⟯ := by
      convert! ← sub_mem αxβ_in_K (smul_mem _ β_in_K)
      apply add_sub_cancel_right
    rintro x (rfl | rfl) <;> assumption

Goal state after:
case a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := ⋯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ F⟮α + x • β⟯ ≤ F⟮α, β⟯
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra F L
hL : ∀ (x : E), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
⊢ Nat.card (E →ₐ[F] L) = finrank F E

Tactic:
AlgHom.natCard_of_splits F E L hL

Goal state after:
F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra F L
hL : ∀ (x : E), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
⊢ finrank F E = finrank F E
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ B' ∩ (M.E \ (R ∩ M.E))) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R

Tactic:
sdiff_inter_sdiff

Goal state after:
α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case refine_4
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
B₁ : Set α
hB₁ hB' : M.IsBase B₁
hI : M.IsBasis (B₁ \ X) (M.E \ X)
hIB' : B₁ \ X ⊆ B₁
hB'IB : B₁ ⊆ B₁ \ X ∪ B
hXJ : X \ B₁ ∩ M.E ⊆ J
hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B₁ \ X
hdj' : ¬Disjoint J B₁
⊢ False

Tactic:
obtain ⟨e, heJ, heB'⟩ := not_disjoint_iff.mp hdj'

Goal state after:
case refine_4
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
B₁ : Set α
hB₁ hB' : M.IsBase B₁
hI : M.IsBasis (B₁ \ X) (M.E \ X)
hIB' : B₁ \ X ⊆ B₁
hB'IB : B₁ ⊆ B₁ \ X ∪ B
hXJ : X \ B₁ ∩ M.E ⊆ J
hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B₁ \ X
hdj' : ¬Disjoint J B₁
e : α
heJ : e ∈ J
heB' : e ∈ B₁
⊢ False
Module: Mathlib.Combinatorics.Matroid.Map

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

Tactic:
by
  simp [comapOn, and_assoc]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure I
⊢ M.fundCircuit e I = insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})

Tactic:
rw [fundCircuit]
  simp_rw [closure_subset_closure_iff_subset_closure
    (show {e} ⊆ M.E by simpa using mem_ground_of_mem_closure he), singleton_subset_iff]
  rw [inter_eq_self_of_subset_right (sInter_subset_of_mem (by simpa))]

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

Goal state before:
pp: α : Type u_1
e : α
E : Set α
⊢ (loopyOn E).IsLoop e ↔ e ∈ E

Tactic:
simp [isLoop_iff, loops]

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

Goal state before:
pp: α : Type u_1
E : Set α
e : α
⊢ ¬(freeOn E).IsLoop e

Tactic:
simp [isLoop_iff, loops]

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

Goal state before:
pp: α : Type u_1
e : α
I E : Set α
⊢ (uniqueBaseOn I E).IsLoop e ↔ e ∈ E \ I

Tactic:
simp [isLoop_iff, loops]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M.RankPos
⊢ 1 ≤ M.eRank

Tactic:
obtain ⟨B, hB⟩ := M.exists_isBase
  rw [← hB.encard_eq_eRank, one_le_encard_iff_nonempty]
  exact hB.nonempty

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

Goal state before:
pp: α : Type u_1
e : α
M : Matroid α
X Y : Set α
⊢ M.eRk (M.E \ insert e (X ∪ Y)) + M.eRk (M.E \ insert e (X ∩ Y)) ≤ M.eRk (M.E \ insert e X) + M.eRk (M.E \ insert e Y)

Tactic:
rw [insert_union_distrib, insert_inter_distrib]

Goal state after:
α : Type u_1
e : α
M : Matroid α
X Y : Set α
⊢ M.eRk (M.E \ (insert e X ∪ insert e Y)) + M.eRk (M.E \ (insert e X ∩ insert e Y)) ≤
    M.eRk (M.E \ insert e X) + M.eRk (M.E \ insert e Y)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
X Y I : Set α
hI : (loopyOn Y).IsBasis' I X
⊢ (loopyOn Y).eRk X = 0

Tactic:
rw [hI.eRk_eq_encard, loopyOn_indep_iff.1 hI.indep, encard_empty]

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

Goal state before:
pp: α : Type u_1
X Y : Set α
⊢ (loopyOn Y).eRk X = 0

Tactic:
by
  obtain ⟨I, hI⟩ := (loopyOn Y).exists_isBasis' X
  rw [hI.eRk_eq_encard, loopyOn_indep_iff.1 hI.indep, encard_empty]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ M.closure (⋃ i, M.closure (Xs i)) = M.closure (⋃ i, Xs i)

Tactic:
by
  simp_rw [closure_eq_subtypeClosure, iUnion_inter, Subtype.coe_inj]
  convert! M.subtypeClosure.closure_iSup_closure (fun i ↦ ⟨Xs i ∩ M.E, inter_subset_right⟩) <;>
  simp [← iUnion_inter, subtypeClosure]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ M.closure (X ∪ K) = M.closure X ∪ K

Tactic:
rw [← closure_union_closure_left_eq, subset_antisymm_iff, and_iff_left (M.subset_closure _),
    ← sdiff_eq_empty, eq_empty_iff_forall_notMem]
  refine fun e ⟨hecl, he⟩ ↦ he (.inl ?_)
  obtain ⟨C, hCss, hC, heC⟩ := (mem_closure_iff_exists_isCircuit he).1 hecl
  rw [← singleton_union, ← union_assoc, union_comm, ← sdiff_subset_iff,
    (hC.disjoint_coloops.mono_right hK).sdiff_eq_left, singleton_union] at hCss
  exact M.closure_subset_closure_of_subset_closure (by simpa) <|
    hC.mem_closure_sdiff_singleton_of_mem heC

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
⊢ x ∈ M.closure I ↔ M.Dep (insert x I) ∨ x ∈ I

Tactic:
by
  rwa [hI.closure_eq_setOfPred_isBasis_insert, mem_ofPred, isBasis_insert_iff]

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

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

Tactic:
rw [hI.mem_closure_iff, dep_iff, insert_subset_iff, and_iff_right he,
    and_iff_left hI.subset_ground]

Goal state after:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ M.E
⊢ ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I X' : Set α
hIX : M.IsBasis I X'
hXX' : f '' X = f '' X'
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ X = X'

Tactic:
by rwa [hf.image_eq_image_iff hX hIX.subset_ground] at hXX'

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 α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
⊢ N.IsBase B' → #↑(B \ B') ≤ #↑(B' \ B)

Tactic:
hB'

Goal state after:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
⊢ #↑(B \ B') ≤ #↑(B' \ B)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
⊢ False

Tactic:
obtain ⟨f, hfIJ, hfb⟩ := hJI.exchange hIb ⟨heJ (mem_insert e _), heEI.2⟩

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e I)
⊢ False
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:
by
  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.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:
rw [algebraicIndependent_iff] at H ⊢

Goal state after:
ι : 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 : ∀ (p : MvPolynomial ι R), (aeval fun i ↦ (aeval x) (f i)) p = 0 → p = 0
⊢ ∀ (p : MvPolynomial ι R), (aeval f) p = 0 → p = 0
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
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : AlgebraicIndependent S (⇑g ∘ x)
hf : Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ AlgebraicIndependent R x

Tactic:
rw [algebraicIndependent_iff] at H ⊢

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι S), (aeval (⇑g ∘ x)) p = 0 → p = 0
hf : Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
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
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : AlgebraicIndependent R x
hf : Surjective ⇑f
hg : Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ AlgebraicIndependent S (⇑g ∘ x)

Tactic:
rw [algebraicIndependent_iff] at H ⊢

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
hf : Surjective ⇑f
hg : Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ ∀ (p : MvPolynomial ι S), (aeval (⇑g ∘ x)) p = 0 → p = 0
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
h : a ∈ fixedBy α g
j : ℤ
⊢ a ∈ fixedBy α (g ^ j)

Tactic:
by
  rw [mem_fixedBy, zpow_smul_eq_iff_minimalPeriod_dvd, minimalPeriod_eq_one_iff_fixedBy.mpr h,
    Int.natCast_one]
  exact one_dvd j

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✝¹ : IsDomain S
inst✝ : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
⊢ Algebra.IsAlgebraic S A ↔ ∀ (i : ι), IsAlgebraic S (v i)

Tactic:
by
  refine ⟨fun _ i ↦ Algebra.IsAlgebraic.isAlgebraic (v i), fun H ↦ ?_⟩
  let Rv := adjoin R (range v)
  let Sv := adjoin S (range v)
  have : Algebra.IsAlgebraic S Sv := by
    simpa [Sv, ← Subalgebra.isAlgebraic_iff, isAlgebraic_adjoin_iff]
  have le : Rv ≤ Sv.restrictScalars R := by
    rw [Subalgebra.restrictScalars_adjoin]; exact le_sup_right
  let : Algebra Rv Sv := (Subalgebra.inclusion le).toAlgebra
  have : IsScalarTower Rv Sv A := .of_algebraMap_eq fun x ↦ rfl
  have := (algebraMap R S).domain_nontrivial
  have := hv.isAlgebraic
  have : Algebra.IsAlgebraic Sv A := .extendScalars (Subalgebra.inclusion_injective le)
  exact .trans _ Sv _

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
inst✝ : FiniteDimensional F E
α : E
hα : IsIntegral F α
h_sep : IsSeparable F α
h_splits : (Polynomial.map (algebraMap F ↥F⟮α⟯) (minpoly F α)).Splits
⊢ Nat.card Gal(↥F⟮α⟯/F) = finrank F ↥F⟮α⟯

Tactic:
rw [IntermediateField.adjoin.finrank 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
α : E
hα : IsIntegral F α
h_sep : IsSeparable F α
h_splits : (Polynomial.map (algebraMap F ↥F⟮α⟯) (minpoly F α)).Splits
⊢ Nat.card Gal(↥F⟮α⟯/F) = (minpoly F α).natDegree
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
t : TopologicalSpace G
F : GroupFilterBasis G
hG : F.topology = t
this : IsTopologicalGroup G
⊢ T2Space G ↔ ⋂₀ F.sets = {1}

Tactic:
IsTopologicalGroup.t2Space_iff_one_closed,

Goal state after:
G : Type u
inst✝ : Group G
t : TopologicalSpace G
F : GroupFilterBasis G
hG : F.topology = t
this : IsTopologicalGroup G
⊢ IsClosed[t] {1} ↔ ⋂₀ F.sets = {1}
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hmulright
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
x₀ : R
i : ι
hi : p i
⊢ ∀ᶠ (x : M) in 𝓝 0, x₀ • x ∈ b i

Tactic:
rcases hsmul_left x₀ hi with ⟨j, hj, hji⟩

Goal state after:
case hmulright
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
x₀ : R
i : ι
hi : p i
j : ι
hj : p j
hji : MapsTo (fun x ↦ x₀ • x) (b j) (b i)
⊢ ∀ᶠ (x : M) in 𝓝 0, x₀ • x ∈ b i
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
inst✝ : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : f x ≠ g x
⊢ f (f.symm (g x)) ≠ f x

Tactic:
rw [AlgEquiv.apply_symm_apply f (g x), ne_comm]

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : f x ≠ g x
⊢ f x ≠ g x
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: 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)
⊢ f ∈ (map (IsScalarTower.toAlgHom F E E') L).fixingSubgroup ↔ f ∈ Subgroup.comap (restrictNormalHom E) L.fixingSubgroup

Tactic:
simp only [Subgroup.mem_comap, mem_fixingSubgroup_iff]

Goal state after:
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
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : (C (f.coeff 0)).IsPrimitive
h : IsUnit (map φ f)
u : Sˣ
hu : C ↑u = map φ f
hdeg : f.degree = 0
⊢ IsUnit (C (f.coeff 0))

Tactic:
exact isUnit_C.mpr (isPrimitive_iff_isUnit_of_C_dvd.mp hf (f.coeff 0) dvd_rfl)

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
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
y : S
hy : (aeval y) (minpoly R x) = 0
⊢ (if x = y then (RingHom.id S) ((aeval x) (derivative (minpoly R x))) else 0) =
    if x = y then (aeval x) (derivative (minpoly R x)) else 0

pp: case hy
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
x : S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
y : S
hy : (aeval y) (minpoly R x) = 0
⊢ eval₂ ((RingHom.id S).comp (algebraMap R S)) y (minpoly R x) = 0

Tactic:
RingHom.id_apply

Goal state after:
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
x : S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
y : S
hy : (aeval y) (minpoly R x) = 0
⊢ (if x = y then (aeval x) (derivative (minpoly R x)) else 0) =
    if x = y then (aeval x) (derivative (minpoly R x)) else 0

case hy
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
x : S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
y : S
hy : (aeval y) (minpoly R x) = 0
⊢ eval₂ ((RingHom.id S).comp (algebraMap R S)) y (minpoly R x) = 0
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
⊢ False

Tactic:
let L' : FiniteGaloisIntermediateField k K := {
    normalClosure k L K with
    finiteDimensional := normalClosure.is_finiteDimensional k L K
    isGalois := IsGalois.normalClosure k L K }

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
⊢ False