mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ mapRingHom (RingHom.id R) = MonoidHom.id (Pic R)

Tactic:
mapRingHom,

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ mapAlgebra R R = MonoidHom.id (Pic R)
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := ⋯
g : F[X] := ⋯
ιFE : F →+* E := ⋯
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := ⋯
c : F
γ : E := ⋯
p : (↥F⟮γ⟯)[X] := ⋯
h : E[X] := ⋯
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
x : (Polynomial.map ιFE g).SplittingField
hc : -(ιEE' γ - ιEE' (ιFE c) * x - ιEE' α) / (x - ιEE' β) ≠ (ιEE'.comp ιFE) c
hx : eval₂ ιEE' x h = 0
a : ¬x = ιEE' β
⊢ -(ιEE' γ - ιEE' (ιFE c) * x - ιEE' α) / (x - ιEE' β) = (ιEE'.comp ιFE) c

Tactic:
apply (div_eq_iff (sub_ne_zero.mpr a)).mpr

Goal state after:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := ⋯
g : F[X] := ⋯
ιFE : F →+* E := ⋯
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := ⋯
c : F
γ : E := ⋯
p : (↥F⟮γ⟯)[X] := ⋯
h : E[X] := ⋯
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
x : (Polynomial.map ιFE g).SplittingField
hc : -(ιEE' γ - ιEE' (ιFE c) * x - ιEE' α) / (x - ιEE' β) ≠ (ιEE'.comp ιFE) c
hx : eval₂ ιEE' x h = 0
a : ¬x = ιEE' β
⊢ -(ιEE' γ - ιEE' (ιFE c) * x - ιEE' α) = (ιEE'.comp ιFE) c * (x - ιEE' β)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B₁ B₂ : Set α
e : α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
hxB₁ : e ∈ B₁
hxB₂ : e ∉ B₂
⊢ ∃ y, (y ∈ B₂ ∧ y ∉ B₁) ∧ M.IsBase (insert y (B₁ \ {e}))

Tactic:
simpa using hB₁.exchange hB₂ ⟨hxB₁, hxB₂⟩

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

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : B' \ B = ∅
hfB : f ∈ B'
h : B \ B' = ∅
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
eq_empty_iff_forall_notMem

Goal state after:
case inl
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : ∀ (x : α), x ∉ B' \ B
hfB : f ∈ B'
h : B \ B' = ∅
⊢ M.IsBase (insert f (B \ {e}))
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hf : f ∈ B' \ (B \ {e})
hfB : M.Indep (insert f (B \ {e}))
⊢ ∃ b ∈ B' \ B, Maximal M.Indep (insert b (B \ {e}))

Tactic:
replace hf := show f ∈ B' \ B by simpa [show f ≠ e by rintro rfl; exact he.2 hf.1] using hf

Goal state after:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
⊢ ∃ b ∈ B' \ B, Maximal M.Indep (insert b (B \ {e}))
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ M.IsBasis I (X ∩ M.E)

Tactic:
convert! hI

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ X ∩ M.E = X
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊆ Y
hYX : Y ⊆ X
⊢ M.IsBasis I Y

Tactic:
rw [isBasis_iff (hYX.trans hI.subset_ground), and_iff_right hI.indep, and_iff_right hIY]

Goal state after:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊆ Y
hYX : Y ⊆ X
⊢ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ Y → I = J
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
E : Set α
hE : E.Finite
⊢ {M | M.E ⊆ E}.Finite

Tactic:
by
  set f : Matroid α → Set α × (Set (Set α)) := fun M ↦ ⟨M.E, {B | M.IsBase B}⟩
  have hf : f.Injective := by
    refine fun M M' hMM' ↦ ?_
    rw [Prod.mk.injEq, and_comm, Set.ext_iff, and_comm] at hMM'
    exact ext_isBase hMM'.1 (fun B _ ↦ hMM'.2 B)
  rw [← Set.finite_image_iff hf.injOn]
  refine (hE.finite_subsets.prod hE.finite_subsets.finite_subsets).subset ?_
  rintro _ ⟨M, hE : M.E ⊆ E, rfl⟩
  simp only [Set.mem_prod, Set.mem_ofPred_eq]
  exact ⟨hE, fun B hB ↦ hB.subset_ground.trans hE⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
⊢ ∃ x ∈ B \ I, N.Indep (f '' insert x I) ∧ InjOn f (insert x I)

Tactic:
have h₂ : (N ↾ range f).IsBase (f '' B) := by
        refine Indep.isBase_of_forall_insert (by simpa using hBmax.1.1) ?_
        rintro _ ⟨⟨e, heB, rfl⟩, hfe⟩ hi
        rw [restrict_indep_iff, ← image_insert_eq] at hi
        have hinj : InjOn f (insert e B) := by
          rw [injOn_insert (fun heB ↦ hfe (mem_image_of_mem f heB))]
          exact ⟨hBmax.1.2, hfe⟩
        refine hBmax.not_prop_of_ssuperset (t := insert e B) (ssubset_insert ?_) ⟨hi.1, hinj⟩
        exact fun heB ↦ hfe <| mem_image_of_mem f heB

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
h₂ : (N ↾ range f).IsBase (f '' B)
⊢ ∃ x ∈ B \ I, N.Indep (f '' insert x I) ∧ InjOn f (insert x I)
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J : Set β
hIJ : I ⊆ f ⁻¹' J
hJ : N.Indep J
hJf : J ⊆ range f
hJX : J ⊆ f '' X
hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t
J₀ : Set α
hIJ₀ : I ⊆ J₀
hJ₀X : J₀ ⊆ X
hbj : BijOn f J₀ (f '' f ⁻¹' J)
⊢ ∃ J,
    I ⊆ J ∧ N.Indep (f '' J) ∧ InjOn f J ∧ J ⊆ X ∧ ∀ ⦃t : Set α⦄, N.Indep (f '' t) → InjOn f t → t ⊆ X → J ⊆ t → J = t

Tactic:
obtain rfl : f '' J₀ = J := by rw [← image_preimage_eq_of_subset hJf, hbj.image_eq]

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J₀ : Set α
hIJ₀ : I ⊆ J₀
hJ₀X : J₀ ⊆ X
hIJ : I ⊆ f ⁻¹' f '' J₀
hJ : N.Indep (f '' J₀)
hJf : f '' J₀ ⊆ range f
hJX : f '' J₀ ⊆ f '' X
hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → f '' J₀ ⊆ t → f '' J₀ = t
hbj : BijOn f J₀ (f '' f ⁻¹' f '' J₀)
⊢ ∃ J,
    I ⊆ J ∧ N.Indep (f '' J) ∧ InjOn f J ∧ J ⊆ X ∧ ∀ ⦃t : Set α⦄, N.Indep (f '' t) → InjOn f t → t ⊆ X → J ⊆ t → J = t
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y J : Set α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
hXY : X ⊆ Y
hJY : (M ↾ Y).IsBase J
⊢ (M ↾ Y).IsBase I

Tactic:
exact hJY.isBase_of_isBasis_superset hJX.subset (hIX.isBasis_restrict_of_subset hXY)

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I

Tactic:
rw [IsCircuit, minimal_iff_forall_ssubset, and_congr_right_iff]
  exact fun h ↦ ⟨fun h' I hIC ↦ ((not_dep_iff (hIC.subset.trans h.subset_ground)).1 (h' hIC)),
    fun h I hIC ↦ (h hIC).not_dep⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).IsCircuit C ↔ M.IsCircuit C ∧ C ⊆ R

Tactic:
refine ⟨?_, fun h ↦ h.1.isCircuit_restrict_of_subset h.2⟩

Goal state after:
α : Type u_1
M : Matroid α
C R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).IsCircuit C → M.IsCircuit C ∧ C ⊆ R
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ (M.restrictSubtype Y).IsBasis I X ↔ M.IsBasis' (Subtype.val '' I) (Subtype.val '' X)

Tactic:
rw [restrictSubtype, comap_isBasis_iff, and_iff_right Subtype.val_injective.injOn,
    and_iff_left_of_imp, isBasis_restrict_iff', isBasis'_iff_isBasis_inter_ground]

Goal state after:
α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ M.IsBasis (↑I) (↑X ∩ M.E) ∧ ↑X ⊆ Y ↔ M.IsBasis (Subtype.val '' I) (Subtype.val '' X ∩ M.E)

α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ (M ↾ Y).IsBasis ↑I ↑X → I ⊆ X
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
hX : X ⊆ M.E
x✝ : ∃ I, M.IsBasis I X ∧ I.encard = n
I : Set α
hI : M.IsBasis I X
hIc : I.encard = n
⊢ M.eRk X = n

Tactic:
by rw [← hI.encard_eq_eRk, hIc]

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

Goal state before:
pp: α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
⊢ M₁ = M₂

Tactic:
refine ext_isCircuit hE fun C hCE ↦ ⟨fun hC ↦ ?_, fun hC ↦ ?_⟩
  · obtain ⟨C', hC'C, hC'⟩ := ((not_indep_iff (by rwa [← hE])).1 (h₁ C hC)).exists_isCircuit_subset
    rwa [← hC.eq_of_not_indep_subset (h₂ C' hC') hC'C]
  obtain ⟨C', hC'C, hC'⟩ := ((not_indep_iff hCE).1 (h₂ C hC)).exists_isCircuit_subset
  rwa [← hC.eq_of_not_indep_subset (h₁ C' hC') hC'C]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
⊢ n ≤ M.eRk X ↔ ∃ I ⊆ X, M.Indep I ∧ I.encard = n

Tactic:
by
  refine ⟨fun h ↦ ?_, fun ⟨I, hIX, hI, hIc⟩ ↦ ?_⟩
  · obtain ⟨J, hJ⟩ := M.exists_isBasis' X
    rw [← hJ.encard_eq_eRk] at h
    obtain ⟨I, hIJ, rfl⟩ := exists_subset_encard_eq h
    exact ⟨_, hIJ.trans hJ.subset, hJ.indep.subset hIJ, rfl⟩
  rw [← hIc, ← hI.eRk_eq_encard]
  exact M.eRk_mono hIX

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
inst✝ : M✶.RankPos
⊢ M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C

Tactic:
by
  by_cases he : e ∈ M.E
  · simp [isColoop_iff_forall_notMem_isCircuit, he]
  obtain ⟨C, hC⟩ := M.exists_isCircuit
  exact iff_of_false (fun h ↦ he h.mem_ground) fun h ↦ he (h C hC).1

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:
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 (M.closure X ∪ K) \ (M.closure X ∪ K) = ∅

Tactic:
eq_empty_iff_forall_notMem

Goal state after:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ ∀ (x : α), x ∉ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)
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 : e ∈ ⋂ J ∈ Js, M.closure J
he' : e ∉ M.closure (⋂₀ Js)
⊢ False

Tactic:
rw [mem_iInter₂] at he

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' : e ∉ M.closure (⋂₀ Js)
⊢ False
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
hB' : N.IsBase B'
h : Infinite ↑(B' \ B)
a : α
ha : a ∈ B' \ B
this : ∀ (S : Set α), Finite ↑S → S ⊆ B → N.Indep (insert a S)
⊢ N.Indep (insert a B)

Tactic:
exact Finitary.indep_of_forall_finite _ fun J hJ fin ↦ (this (J \ {a}) fin.sdiff.to_subtype <|
      sdiff_singleton_subset_iff.mpr hJ).subset (subset_insert_sdiff_singleton ..)

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
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)
q : MvPolynomial ι R
hp : (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) q) = 0
⊢ (MvPolynomial.map ↑f) q = 0

Tactic:
rw [H q (hg (by rwa [map_zero, ← RingHom.coe_coe g, map_aeval, ← h, ← eval₂Hom_map_hom,
    ← aeval_eq_eval₂Hom])), map_zero]

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
⊢ AlgebraicIndependent R Subtype.val → Cardinal.mk ↑s ≤ ↑n

Tactic:
li

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
⊢ Cardinal.mk ↑s ≤ ↑n
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Injective ⇑f
a✝ : Nontrivial R
⊢ ⨆ i, lift.{v', v} #↑↑i ≤ lift.{v, v'} (trdeg R A')

Tactic:
exact ciSup_le' fun i ↦ (i.2.map' hf).lift_cardinalMk_le_trdeg

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

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g : G
⊢ g⁻¹ • a ∈ fixedBy α g⁻¹ ↔ a ∈ fixedBy α g⁻¹

Tactic:
smul_mem_fixedBy_iff_mem_fixedBy,

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g : G
⊢ a ∈ fixedBy α g⁻¹ ↔ a ∈ fixedBy α g⁻¹
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 : AlgebraicIndependent R x
fin : trdeg R A < ℵ₀
le : lift.{u, w} (trdeg R A) ≤ lift.{w, u} #ι
⊢ IsTranscendenceBasis R x

Tactic:
have := (faithfulSMul_iff_algebraMap_injective R A).mpr hx.algebraMap_injective
  rw [← matroid_cRank_eq, ← Matroid.rankFinite_iff_cRank_lt_aleph0] at fin
  exact .of_subtype_range hx.injective <| matroid_indep_iff.mpr hx.to_subtype_range
    |>.isBase_of_cRank_le <| lift_le.mp <| (matroid_cRank_eq R A ▸ le).trans_eq
      (mk_range_eq_of_injective hx.injective).symm

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
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)

Tactic:
by
  have ⟨s, hs⟩ := exists_isTranscendenceBasis R S
  have ⟨t, ht⟩ := exists_isTranscendenceBasis S A
  have := (FaithfulSMul.algebraMap_injective S A).noZeroDivisors _ (map_zero _) (map_mul _)
  have := (FaithfulSMul.algebraMap_injective R S).nontrivial
  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.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inl
ι : 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 ι
j : ι
v : ι → S
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial S
this✝¹ : IsDomain S
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})
k : ι
hkj : k ∉ {j}
hj : j ∈ insert k s
this : Nontrivial ↥(adjoin R (v '' (insert k s \ {j})))
H₂ : v j ∈ (matroid R S).closure (v '' (insert k s \ {j}))
hi : k ∉ s
ne : v k ≠ v j
his : v k ∈ v '' s
⊢ v k ∈ v '' s \ {v j}

Tactic:
exact ⟨his, ne⟩

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

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ (B.N x₀).HasBasis (fun V ↦ V ∈ B) fun V ↦ (fun y ↦ x₀ * y) '' V

Tactic:
apply B.hasBasis

Goal state after:
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
h : f.natSepDegree = 1
⊢ ∃ n y, (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = X ^ q ^ n - C y

Tactic:
obtain ⟨n, y, hf⟩ := (hm.natSepDegree_eq_one_iff_of_irreducible q hi).1 h

Goal state after:
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
n : ℕ
y : F
hf : f = X ^ q ^ n - C y
⊢ ∃ n y, (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = X ^ q ^ n - C y
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: case mp
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsGalois (↥⊥) E → IsGalois F E

Tactic:
intro h
    exact IsGalois.tower_top_of_isGalois (⊥ : IntermediateField F E) F E

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✝¹ : IsGalois F E
inst✝ : FiniteDimensional F E
⊢ fixedField ⊥.fixingSubgroup = ⊥

Tactic:
fixedField_fixingSubgroup

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : IsGalois F E
inst✝ : FiniteDimensional F E
⊢ ⊥ = ⊥
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✝¹ : IsGalois F E
inst✝ : FiniteDimensional F E
⊢ fixedField ⊤ = ⊥

Tactic:
by
  rw [← fixingSubgroup_bot, fixedField_fixingSubgroup]

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
this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = Cardinal.lift.{v, u} (sepDegree F F)
⊢ sepDegree F ↥⊥ = 1

Tactic:
rwa [sepDegree_self, Cardinal.lift_one, ← Cardinal.lift_one.{v, u}, Cardinal.lift_inj] at this

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
hfd : FiniteDimensional F E
⊢ finSepDegree F ↥⊥ ∣ finrank F ↥⊥

Tactic:
by simp_rw [finSepDegree_bot, IntermediateField.finrank_bot, one_dvd]

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
⊢ ∃ T, mulInvClosureNhd T W

Tactic:
rcases exist_mul_closure_nhds WClopen with ⟨S, Smemnhds, mulclose⟩
  rcases mem_nhds_iff.mp Smemnhds with ⟨U, UsubS, Uopen, onememU⟩
  use U ∩ U⁻¹
  constructor
  · simp [Uopen.mem_nhds onememU, inv_mem_nhds_one]
  · simp [inter_comm]
  · exact Uopen.inter Uopen.inv
  · exact fun a ha ↦ mulclose (mul_subset_mul_left UsubS (mul_subset_mul_left inter_subset_left ha))

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
⊢ ∀ (x₀ : Gal(L/K)) {U : Set Gal(L/K)},
    U ∈ (galBasis K L).sets → ∃ V ∈ (galBasis K L).sets, V ⊆ (fun x ↦ x₀ * x * x₀⁻¹) ⁻¹' U

Tactic:
by
    rintro σ U ⟨H, ⟨E, hE, rfl⟩, rfl⟩
    let F : IntermediateField K L := E.map σ.symm.toAlgHom
    refine ⟨F.fixingSubgroup.carrier, ⟨⟨F.fixingSubgroup, ⟨F, ?_, rfl⟩, rfl⟩, fun g hg => ?_⟩⟩
    · have : FiniteDimensional K E := hE
      exact IntermediateField.finiteDimensional_map σ.symm.toAlgHom
    change σ * g * σ⁻¹ ∈ E.fixingSubgroup
    rw [IntermediateField.mem_fixingSubgroup_iff]
    intro x hx
    change σ (g (σ⁻¹ x)) = x
    have h_in_F : σ⁻¹ x ∈ F := ⟨x, hx, by dsimp⟩
    have h_g_fix : g (σ⁻¹ x) = σ⁻¹ x := by
      rw [Subgroup.mem_carrier, IntermediateField.mem_fixingSubgroup_iff F g] at hg
      exact hg (σ⁻¹ x) h_in_F
    rw [h_g_fix]
    change σ (σ⁻¹ x) = x
    exact AlgEquiv.apply_symm_apply σ x

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u_1
inst✝ : Field F
x✝ : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * ↑u = f
g : F[X]
hg : g ∈ UniqueFactorizationMonoid.factors f
⊢ g.Splits

Tactic:
specialize h (UniqueFactorizationMonoid.irreducible_of_factor g hg)

Goal state after:
case refine_1
F : Type u_1
inst✝ : Field F
x✝ : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * ↑u = f
g : F[X]
h : g.Separable
hg : g ∈ UniqueFactorizationMonoid.factors f
⊢ g.Splits
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
hs : IsIntegral R s
p : R[X]
⊢ ↑(Polynomial.aeval s) p = 0 ↔ p ∈ Ideal.span {minpoly R s}

Tactic:
AlgHom.coe_toRingHom,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
hs : IsIntegral R s
p : R[X]
⊢ (Polynomial.aeval s) p = 0 ↔ p ∈ Ideal.span {minpoly R s}
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
inst✝ : IsGalois k K
⊢ IntermediateField.fixedField ⊥.fixingSubgroup = ⊥

Tactic:
fixedField_fixingSubgroup

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
⊢ ⊥ = ⊥