mathlib-initiative/mathlib-tactics huggingface dataset:
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, I ⊆ J ∧ Maximal (fun K ↦ (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) K ∧ K ⊆ X) J

Tactic:
obtain ⟨J, hJ⟩ := (N ↾ range f).existsMaximalSubsetProperty_indep (f '' X) (by simp)
        (f '' I) (by simpa) (image_mono hIX)

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 β
hJ : f '' I ⊆ J ∧ Maximal (fun K ↦ (N ↾ range f).Indep K ∧ K ⊆ f '' X) J
⊢ ∃ J, I ⊆ J ∧ Maximal (fun K ↦ (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) K ∧ K ⊆ X) J
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 ⊆ 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

Tactic:
refine ⟨J₀, hIJ₀, hJ, hbj.injOn, hJ₀X, fun K hK hKinj hKX hJ₀K ↦ ?_⟩

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₀)
K : Set α
hK : N.Indep (f '' K)
hKinj : InjOn f K
hKX : K ⊆ X
hJ₀K : J₀ ⊆ K
⊢ J₀ = K
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E
I J : Set α
hI : ∀ (J : Finset α), ↑J ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), ↑J_1 ⊆ J → Indep J_1
hJfin : J.Finite
hIJ : hIfin.toFinset.card < hJfin.toFinset.card
⊢ ∃ e ∈ J, e ∉ I ∧ ∀ (J : Finset α), ↑J ⊆ insert e I → Indep J

Tactic:
have aug := indep_aug (hI _ (by simp)) (hJ _ (by simp)) hIJ

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E
I J : Set α
hI : ∀ (J : Finset α), ↑J ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), ↑J_1 ⊆ J → Indep J_1
hJfin : J.Finite
hIJ : hIfin.toFinset.card < hJfin.toFinset.card
aug : ∃ e ∈ hJfin.toFinset, e ∉ hIfin.toFinset ∧ Indep (insert e hIfin.toFinset)
⊢ ∃ e ∈ J, e ∉ I ∧ ∀ (J : Finset α), ↑J ⊆ insert e I → Indep J
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hX : X ⊆ M.E
⊢ M.IsBasis (B ∩ X) X ↔ M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)

Tactic:
refine ⟨hB.compl_inter_isBasis_of_inter_isBasis, fun h ↦ ?_⟩
  simpa [inter_eq_self_of_subset_right hX, inter_eq_self_of_subset_right hB.subset_ground] using
    hB.compl_isBase_dual.compl_inter_isBasis_of_inter_isBasis h

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 ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C

Tactic:
isCircuit_def,

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
⊢ Minimal M.Dep C ↔ M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
X : Set α
x✝ : M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' ⇑f '' X) ∧ I ⊆ ⇑f '' X ∧ ⇑f '' X ⊆ range ⇑f
hb : M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' ⇑f '' X)
hIX : I ⊆ ⇑f '' X
hX : ⇑f '' X ⊆ range ⇑f
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ ⇑f '' X = ⇑f '' X₀

Tactic:
obtain ⟨I, -, rfl⟩ := subset_image_iff.1 hIX

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
X : Set α
hX : ⇑f '' X ⊆ range ⇑f
I : Set α
x✝ : M.IsBasis (⇑f ⁻¹' ⇑f '' I) (⇑f ⁻¹' ⇑f '' X) ∧ ⇑f '' I ⊆ ⇑f '' X ∧ ⇑f '' X ⊆ range ⇑f
hb : M.IsBasis (⇑f ⁻¹' ⇑f '' I) (⇑f ⁻¹' ⇑f '' X)
hIX : ⇑f '' I ⊆ ⇑f '' X
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ ⇑f '' I = ⇑f '' I₀ ∧ ⇑f '' X = ⇑f '' X₀
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
X I : Set α
hX : X ⊆ M.loops
h : M.IsBasis I X
this : M.IsBasis I M.loops
⊢ I = ∅

Tactic:
simpa using this

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
R : Set α
⊢ (M ↾ R).Indep {e} ↔ M.IsNonloop e ∧ e ∈ R

Tactic:
restrict_indep_iff,

Goal state after:
α : Type u_1
M : Matroid α
e : α
R : Set α
⊢ M.Indep {e} ∧ {e} ⊆ R ↔ M.IsNonloop e ∧ e ∈ R
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
Y X : Set α
hX : X ⊆ M.E
⊢ Y ⊆ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F

Tactic:
simp_rw [M.closure_def' X, subset_sInter_iff, mem_ofPred, and_imp]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.RankFinite
⊢ M.Spanning X ↔ M.eRank ≤ M.eRk X ∧ X ⊆ M.E

Tactic:
by
  refine ⟨fun h ↦ ⟨h.eRk_eq.symm.le, h.subset_ground⟩, fun ⟨h, hX⟩ ↦ ?_⟩
  obtain ⟨I, hI⟩ := M.exists_isBasis X
  exact (hI.indep.isBase_of_eRk_ge
    hI.indep.finite (h.trans hI.eRk_eq_eRk.symm.le)).spanning_of_superset hI.subset

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I K : Set α
hK : K ⊆ M.coloops
⊢ M.Indep (I \ K) ↔ M.Indep I

Tactic:
by
  rw [← union_indep_iff_indep_of_subset_coloops hK, sdiff_union_self,
    union_indep_iff_indep_of_subset_coloops hK]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun X ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
⊢ M✶.IsCircuit K ↔ Minimal (fun X ↦ ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K

Tactic:
isCircuit_def,

Goal state after:
α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun X ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
⊢ Minimal M✶.Dep K ↔ Minimal (fun X ↦ ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
⊢ (M ↾ {e | M.IsNonloop e}).Indep I ↔ M.Indep I

Tactic:
restrict_indep_iff,

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I ∧ I ⊆ {e | M.IsNonloop e} ↔ M.Indep I
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ {e | M.IsNonloop e}
⊢ M.removeLoops ↾ X = M ↾ X

Tactic:
rwa [removeLoops_eq_restrict, restrict_restrict_eq]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : AlgebraicIndependent R x
e : MvPolynomial (ι' ⊕ ι) R ≃ₐ[R] MvPolynomial ι' ↥(adjoin R (range x)) :=
  (sumAlgEquiv R ι' ι).trans (mapAlgEquiv ι' hx.aevalEquiv)
⊢ aeval (Sum.elim y x) = (AlgHom.restrictScalars R (aeval y)).comp ↑e

Tactic:
ext (_ | _) <;> simp [e]

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

Goal state before:
pp: α : Type u_2
M₁ M₂ : Matroid α
h : ∀ (X : Set α), M₁.closure X = M₂.closure X
x✝¹ : Set α
x✝ : x✝¹ ⊆ M₁.E
⊢ M₁.Indep x✝¹ ↔ M₂.Indep x✝¹

Tactic:
indep_iff_forall_closure_sdiff_ne,

Goal state after:
α : Type u_2
M₁ M₂ : Matroid α
h : ∀ (X : Set α), M₁.closure X = M₂.closure X
x✝¹ : Set α
x✝ : x✝¹ ⊆ M₁.E
⊢ (∀ ⦃e : α⦄, e ∈ x✝¹ → M₁.closure (x✝¹ \ {e}) ≠ M₁.closure x✝¹) ↔
    ∀ ⦃e : α⦄, e ∈ x✝¹ → M₂.closure (x✝¹ \ {e}) ≠ M₂.closure x✝¹
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t

Tactic:
refine ⟨fun h ↦ ⟨h.spanning, fun _ ↦ h.eq_of_superset_spanning⟩, fun ⟨h, h'⟩ ↦ ?_⟩

Goal state after:
α : Type u_2
M : Matroid α
B : Set α
x✝ : M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
h : M.Spanning B
h' : ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
⊢ M.IsBase B
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
hI' : M.IsBasis' I (X ∩ R)
hIR : I ⊆ R
e : α
⊢ e ∈ R ∧ ((M ↾ R).Indep (insert e I) → e ∈ I) ↔ (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R \ M.E

Tactic:
restrict_indep_iff,

Goal state after:
α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
hI' : M.IsBasis' I (X ∩ R)
hIR : I ⊆ R
e : α
⊢ e ∈ R ∧ (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I) ↔
    (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R \ M.E
Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
x✝ : M
hx : x✝ ∈ (fixingSubmonoid M s).carrier
z : ↑s
⊢ x✝⁻¹ • ↑z = ↑z

Tactic:
by rw [inv_smul_eq_iff, hx z]

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

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s : Set A
⊢ (matroid R A).closure s = s

Tactic:
simp_rw [Matroid.closure, matroid_isFlat_of_subsingleton, true_and, matroid_e, inter_univ]
  exact subset_antisymm (sInter_subset_of_mem <| subset_refl s) (subset_sInter fun _ ↦ id)

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

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s : Set A
⊢ (matroid R A).closure s = (matroid R A).E ∧ s ⊆ (matroid R A).E ↔ s = univ

Tactic:
matroid_closure_of_subsingleton,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s : Set A
⊢ s = (matroid R A).E ∧ s ⊆ (matroid R A).E ↔ s = univ
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
x : G
memW : x ∈ W
this : (x, 1) ∈ (fun p ↦ p.1 * p.2) ⁻¹' W
U V : Set G
Uopen : IsOpen[inst✝³] U
Vopen : IsOpen[inst✝³] V
xmemU : x ∈ U
onememV : 1 ∈ V
prodsub : U ×ˢ V ⊆ (fun p ↦ p.1 * p.2) ⁻¹' W
⊢ ∃ t ∈ 𝓝[W] x, ∃ T ∈ 𝓝 1, t * T ⊆ W

Tactic:
have h6 : U * V ⊆ W := mul_subset_iff.mpr (fun _ hx _ hy ↦ prodsub (mk_mem_prod hx hy))

Goal state after:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
x : G
memW : x ∈ W
this : (x, 1) ∈ (fun p ↦ p.1 * p.2) ⁻¹' W
U V : Set G
Uopen : IsOpen[inst✝³] U
Vopen : IsOpen[inst✝³] V
xmemU : x ∈ U
onememV : 1 ∈ V
prodsub : U ×ˢ V ⊆ (fun p ↦ p.1 * p.2) ⁻¹' W
h6 : U * V ⊆ W
⊢ ∃ t ∈ 𝓝[W] x, ∃ T ∈ 𝓝 1, t * T ⊆ W
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: case h
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ n, V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this✝ : IsOpen[inst✝²] (⋃ n, V ^ (n + 1))
mulVpow : ∀ (n : ℕ), W * V ^ (n + 1) ⊆ W
this : ∀ (n : ℕ), V ^ (n + 1) ⊆ W * V ^ (n + 1)
⊢ ↑{ toSubgroup := S, isOpen' := this✝ } ⊆ W

Tactic:
apply iUnion_subset fun i _ a ↦ mulVpow i (this i a)

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
⊢ f.Splits

Tactic:
have hf0 : f ≠ 0 := by aesop
    obtain ⟨u, hu⟩ := UniqueFactorizationMonoid.factors_prod hf0
    rw [← hu]
    refine (Splits.multisetProd fun g hg ↦ ?_).mul u.isUnit.splits
    specialize h (UniqueFactorizationMonoid.irreducible_of_factor g hg)
    have key := natSepDegree_le_of_dvd g f (UniqueFactorizationMonoid.dvd_of_mem_factors hg) hf0
    rw [h.natSepDegree_eq_natDegree, hf] at key
    exact Splits.of_natDegree_le_one key

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

Goal state before:
pp: F : Type u_1
E' : Type u_3
inst✝³ : Field F
inst✝² : Field E'
inst✝¹ : Algebra F E'
inst✝ : IsGalois F E'
L : IntermediateField F E'
hnfd : FiniteDimensional F ↥L
⊢ finrank F ↥L = L.fixingSubgroup.index

Tactic:
let E := normalClosure F L E'

Goal state after:
F : Type u_1
E' : Type u_3
inst✝³ : Field F
inst✝² : Field E'
inst✝¹ : Algebra F E'
inst✝ : IsGalois F E'
L : IntermediateField F E'
hnfd : FiniteDimensional F ↥L
E : IntermediateField F E' := normalClosure F (↥L) E'
⊢ finrank F ↥L = L.fixingSubgroup.index
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
L : IntermediateField k K
inst✝ : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup)ᶜ
⊢ ∃ t ⊆ (↑L.fixingSubgroup)ᶜ, IsOpen t ∧ σ ∈ t

Tactic:
rcases Set.not_subset.mp ((mem_fixingSubgroup_iff Gal(K/k)).not.mp h) with ⟨y, yL, ne⟩

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a ↦ σ • a = a
⊢ ∃ t ⊆ (↑L.fixingSubgroup)ᶜ, IsOpen t ∧ σ ∈ t
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: case refine_1
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
h : x ∈ ↑(fixedField H ⊓ L)
xL : x ∈ (fun x ↦ ↑x) L
⊢ ∀ a ∈ H, ((restrictNormalHom ↥L) a) ⟨x, xL⟩ = ⟨x, xL⟩

Tactic:
intro σ hσ

Goal state after:
case refine_1
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
h : x ∈ ↑(fixedField H ⊓ L)
xL : x ∈ (fun x ↦ ↑x) L
σ : Gal(K/k)
hσ : σ ∈ H
⊢ ((restrictNormalHom ↥L) σ) ⟨x, xL⟩ = ⟨x, xL⟩
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: case refine_2
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
xL : x ∈ L
h : ∀ a ∈ H, ((restrictNormalHom ↥L) a) ⟨x, xL⟩ = ⟨x, xL⟩
⊢ ∀ f ∈ H, f x = x

Tactic:
intro σ hσ

Goal state after:
case refine_2
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
xL : x ∈ L
h : ∀ a ∈ H, ((restrictNormalHom ↥L) a) ⟨x, xL⟩ = ⟨x, xL⟩
σ : Gal(K/k)
hσ : σ ∈ H
⊢ σ x = x
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
⊢ (fixedField ↑H).fixingSubgroup ≤ ↑H

Tactic:
intro σ hσ

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
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
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i) * (R ∙ x) ≤
    Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))

Tactic:
rw [Submodule.span_mul_span, Set.mul_singleton, Set.image_image]

Goal state after:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ Submodule.span R ((fun x_1 ↦ x ^ x_1 * x) '' Set.Iio i) ≤ Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))
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
x : S
hx : IsIntegral R x
⊢ Injective ⇑(Minpoly.toAdjoin R x)

Tactic:
by
  refine (injective_iff_map_eq_zero _).2 fun P₁ hP₁ => ?_
  obtain ⟨P, rfl⟩ := mk_surjective P₁
  simpa [← Subalgebra.coe_eq_zero, isIntegrallyClosed_dvd_iff hx, ← aeval_def] using hP₁

Goal state after:
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: case inr
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
h : p.roots = 0
hd : 0 < p.degree
z : k
hz : z ∈ 0
⊢ p = C (p.coeff 0)

Tactic:
simp at hz

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

Goal state before:
pp: case hcard.refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ ↦ σ x
⊢ Finset.fold max 0 (natDegree ∘ fun σ ↦ map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x))
      Finset.univ <
    Fintype.card (L →ₐ[K] E)

Tactic:
simp only [Polynomial.map_smul,
        map_div₀, map_pow, RingHom.coe_coe, Function.comp_apply,
        Finset.mem_univ, forall_true_left, Finset.fold_max_lt, AlgHom.card]

Goal state after:
case hcard.refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ ↦ σ x
⊢ 0 < finrank K L ∧
    ∀ (x_1 : L →ₐ[K] E),
      ((x_1 x ^ r / x_1 ((aeval x) (derivative (minpoly K x)))) • map (↑x_1) (minpolyDiv K x)).natDegree < finrank K L
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
L : IntermediateField F E
inst✝¹ : IsPurelyInseparable F ↥L
inst✝ : Algebra.IsSeparable F ↥L
x : E
hx : x ∈ L
⊢ x ∈ ⊥

Tactic:
obtain ⟨y, hy⟩ := IsPurelyInseparable.surjective_algebraMap_of_isSeparable F L ⟨x, hx⟩
  exact ⟨y, congr_arg (algebraMap L E) hy⟩

Goal state after:
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: case a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(adjoin k {x}).toIntermediateField/k) := ⋯
f : ↥L → IntermediateField k K := ⋯
this✝ : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal k ↥(f l)
n : Normal k ↥(⨆ l, f l)
⊢ L ≤ ⨆ l, f l

Tactic:
intro l hl
        apply le_iSup f ⟨l, hl⟩
        simpa only [f, g, ← restrict_fixedField L.fixingSubgroup (adjoin k {l}),
          fixedField_fixingSubgroup L, IntermediateField.mem_inf, hl, true_and]
          using adjoin_simple_le_iff.mp le_rfl

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: case refine_2
A : Type u_1
K : Type u_2
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_3
inst✝¹⁰ : Field L
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsDomain A
inst✝ : Algebra.IsAlgebraic K L
this✝¹ : IsDomain C
this✝ : IsTorsionFree A L
this : IsTorsionFree A C
z : L
⊢ ∃ x, z * (algebraMap C L) ↑x.2 = (algebraMap C L) x.1

Tactic:
obtain ⟨m, hm⟩ :=
      IsIntegral.exists_multiple_integral_of_isLocalization A⁰ z
        (Algebra.IsIntegral.isIntegral (R := K) z)

Goal state after:
case refine_2
A : Type u_1
K : Type u_2
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_3
inst✝¹⁰ : Field L
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsDomain A
inst✝ : Algebra.IsAlgebraic K L
this✝¹ : IsDomain C
this✝ : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥A⁰
hm : IsIntegral A (m • z)
⊢ ∃ x, z * (algebraMap C L) ↑x.2 = (algebraMap C L) x.1
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✝ : SMul G B := smulOfNormal G B C N
this : SMulDistribClass G B C
⊢ MulSemiringAction G B

Tactic:
exact mulSemiringActionOfSmulDistribClass B C G

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
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∑ σ, σ ((algebraMap L F) pb.gen) = finrank L F • ∑ σ, σ pb.gen

Tactic:
rw [Fintype.sum_equiv algHomEquivSigma (fun σ : F →ₐ[K] E => _) fun σ => σ.1 pb.gen,
    ← Finset.univ_sigma_univ, Finset.sum_sigma, ← Finset.sum_nsmul]

Goal state after:
K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∑ a, ∑ s, ⟨a, s⟩.fst pb.gen = ∑ x, finrank L F • x pb.gen

K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : F →ₐ[K] E), x ((algebraMap L F) pb.gen) = (algHomEquivSigma x).fst pb.gen