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

Goal state before:
pp: α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
⊢ ∀ ⦃I : Set β⦄, I ⊆ ((N.comap f).map f hf).E → (((N.comap f).map f hf).Indep I ↔ N.Indep I)

Tactic:
simp only [map_ground, comap_ground_eq, map_indep_iff, comap_indep_iff, forall_subset_image_iff]

Goal state after:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
⊢ ∀ t ⊆ f ⁻¹' N.E, (∃ I₀, (N.Indep (f '' I₀) ∧ InjOn f I₀) ∧ f '' t = f '' I₀) ↔ N.Indep (f '' t)
Module: Mathlib.Combinatorics.Matroid.Map

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

Tactic:
refine ⟨?_, fun ⟨hb, hIX, hX⟩ ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
⊢ (∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ X = ⇑f '' X₀) → M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ range ⇑f

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
⊢ C = M.fundCircuit e I

Tactic:
by
  obtain hCI | ⟨heC, hCeI⟩ := subset_insert_iff.1 hCs
  · exact (hC.not_indep (hI.subset hCI)).elim
  suffices hss : M.fundCircuit e I ⊆ C by
    refine hC.eq_of_superset_isCircuit (hI.fundCircuit_isCircuit ?_ fun heI ↦ ?_) hss
    · rw [hI.mem_closure_iff]
      exact .inl (hC.dep.superset hCs (insert_subset (hC.subset_ground heC) hI.subset_ground))
    exact hC.not_indep (hI.subset (hCs.trans (by simp [heI])))
  have heCcl := (hC.sdiff_singleton_isBasis heC).subset_closure heC
  have heI : e ∈ M.closure I := M.closure_subset_closure hCeI heCcl
  rw [fundCircuit_eq_sInter heI]
  refine insert_subset heC <| (sInter_subset_of_mem (t := C \ {e}) ?_).trans sdiff_subset
  exact ⟨hCeI, heCcl⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
⊢ M.eRk X = I.encard

Tactic:
← hIX.eRk_eq_eRk,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
⊢ M.eRk I = I.encard
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
⊢ M.eRk X = I.encard

Tactic:
← hIX.eRk_eq_eRk,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
⊢ M.eRk I = I.encard
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ M.eRk B = M.eRank

Tactic:
rw [hB.indep.eRk_eq_encard, eRank_def, hB.isBasis_ground.encard_eq_eRk]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
E : Set α
h : M = loopyOn E
⊢ M.loops = E ∧ M.E = E

Tactic:
rw [h, loops]; simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
X : Set α
he : e ∉ M.E
⊢ M.eRk (insert e X ∩ M.E) = M.eRk X

Tactic:
insert_inter_of_notMem he,

Goal state after:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : e ∉ M.E
⊢ M.eRk (X ∩ M.E) = M.eRk X
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk (M.closure X ∪ Y) = M.eRk (X ∪ Y)

Tactic:
by
  rw [← eRk_closure_eq, closure_union_closure_left_eq, eRk_closure_eq]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
R X : Set α
⊢ (M ↾ R).eRk X = M.eRk (X ∩ R)

Tactic:
obtain ⟨I, hI⟩ := (M ↾ R).exists_isBasis' X

Goal state after:
α : Type u_1
M : Matroid α
R X I : Set α
hI : (M ↾ R).IsBasis' I X
⊢ (M ↾ R).eRk X = M.eRk (X ∩ R)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
X : Set α
M : Matroid α
R : Set α
h : X ⊆ R
⊢ (M ↾ R).eRk X = M.eRk X

Tactic:
restrict_eRk_eq',

Goal state after:
α : Type u_1
X : Set α
M : Matroid α
R : Set α
h : X ⊆ R
⊢ M.eRk (X ∩ R) = M.eRk X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inr
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I M₁.loops
e : α
heI : e ∈ I
hel : M₁.IsLoop e
⊢ M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)

Tactic:
refine iff_of_false (hel.not_indep_of_mem ⟨heI, hel.not_isColoop⟩) ?_

Goal state after:
case inr
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I M₁.loops
e : α
heI : e ∈ I
hel : M₁.IsLoop e
⊢ ¬M₂.Indep (I \ M₁.coloops)
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
obtain rfl | hne := eq_or_ne e f
  · simp [hI, heI]
  rw [← insert_sdiff_singleton_comm hne.symm, hI.insert_indep_iff, mem_sdiff_singleton,
    and_iff_left hne.symm]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
⊢ Disjoint C K ∨ (C ∩ K).Nontrivial

Tactic:
rw [or_iff_not_imp_left, disjoint_iff_inter_eq_empty, ← ne_eq, ← nonempty_iff_ne_empty]
  exact hC.isCocircuit_inter_nontrivial hK

Goal state after:
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
⊢ i ∉ s

pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
⊢ Transcendental R f

Tactic:
· rw [Transcendental] at h
    contrapose h
    refine isAlgebraic_algebraMap (⟨Polynomial.aeval (X i) f, ?_⟩ : supported R s)
    exact Algebra.adjoin_mono (Set.singleton_subset_iff.2 (Set.mem_image_of_mem _ h))
      (Polynomial.aeval_mem_adjoin_singleton _ _)

Goal state after:
case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
⊢ Transcendental R f
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
hx : AlgebraicIndependent R x
i : ι
⊢ Transcendental R (x i)

Tactic:
have := hx.comp ![i] (Function.injective_of_subsingleton _)
  have : AlgebraicIndependent R ![x i] := by rwa [← FinVec.map_eq] at this
  rwa [← algebraicIndependent_iff_transcendental]

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

Goal state before:
pp: case e'_1.e'_4
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
i : ι
h : i ∉ s
⊢ (fun i_1 ↦ x ↑i_1) ∘ ⇑(subtypeInsertEquivOption h).symm = fun o ↦ o.elim (x i) fun i ↦ x ↑i

Tactic:
ext (_ | _)

Goal state after:
case e'_1.e'_4.none
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
i : ι
h : i ∉ s
⊢ ((fun i_1 ↦ x ↑i_1) ∘ ⇑(subtypeInsertEquivOption h).symm) none = none.elim (x i) fun i ↦ x ↑i

case e'_1.e'_4.some
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
i : ι
h : i ∉ s
val✝ : { i // i ∈ s }
⊢ ((fun i_1 ↦ x ↑i_1) ∘ ⇑(subtypeInsertEquivOption h).symm) (some val✝) = (some val✝).elim (x i) fun i ↦ x ↑i
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 (_ | _)

Goal state after:
case inl
ι : 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)
val✝ : ι'
⊢ (aeval (Sum.elim y x)) (X (Sum.inl val✝)) = ((AlgHom.restrictScalars R (aeval y)).comp ↑e) (X (Sum.inl val✝))

case inr
ι : 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)
val✝ : ι
⊢ (aeval (Sum.elim y x)) (X (Sum.inr val✝)) = ((AlgHom.restrictScalars R (aeval y)).comp ↑e) (X (Sum.inr val✝))
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: case e'_1
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
⊢ x ∘ ⇑((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s)) = Sum.elim (fun i ↦ x ↑i) fun i ↦ x ↑i

Tactic:
ext (_ | _)

Goal state after:
case e'_1.inl
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
val✝ : ↑sᶜ
⊢ (x ∘ ⇑((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s))) (Sum.inl val✝) =
    Sum.elim (fun i ↦ x ↑i) (fun i ↦ x ↑i) (Sum.inl val✝)

case e'_1.inr
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
val✝ : ↑s
⊢ (x ∘ ⇑((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s))) (Sum.inr val✝) =
    Sum.elim (fun i ↦ x ↑i) (fun i ↦ x ↑i) (Sum.inr val✝)
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
exact hS.superset (subset_inter hST hS.subset_ground)

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X R : Set α
⊢ (M ↾ R).closure X = M.closure (X ∩ R) ∩ R ∪ R \ M.E

Tactic:
obtain ⟨I, hI⟩ := (M ↾ R).exists_isBasis' X

Goal state after:
α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
⊢ (M ↾ R).closure X = M.closure (X ∩ R) ∩ R ∪ R \ M.E
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
X R : Set α
M : Matroid α
hXR : X ⊆ R
hR : R ⊆ M.E
⊢ M.closure (X ∩ R) ∩ R ∪ R \ M.E = M.closure X ∩ R

Tactic:
sdiff_eq_empty.mpr hR,

Goal state after:
α : Type u_2
X R : Set α
M : Matroid α
hXR : X ⊆ R
hR : R ⊆ M.E
⊢ M.closure (X ∩ R) ∩ R ∪ ∅ = M.closure X ∩ R
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)

Tactic:
suffices aux : ∀ ⦃I⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' (M.closure I) by
    obtain ⟨I, hI⟩ := M.exists_isBasis (f ⁻¹' X ∩ M.E)
    rw [← closure_inter_ground, map_ground, ← M.closure_inter_ground, ← hI.closure_eq_closure,
      ← aux hI.indep, ← image_preimage_inter, ← (hI.map hf).closure_eq_closure]
  -- Let `I` be independent, and transform the goal using closure/independence lemmas
  refine fun I hI ↦ Set.ext fun e ↦ ?_
  simp only [(hI.map f hf).mem_closure_iff', map_ground, mem_image, map_indep_iff,
    forall_exists_index, and_imp, hI.mem_closure_iff']
  -- The goal now easily follows from the invariance of independence under maps.
  constructor
  · rintro ⟨⟨x, hxE, rfl⟩, h2⟩
    refine ⟨x, ⟨hxE, fun hI' ↦ ?_⟩, rfl⟩
    obtain ⟨y, hyI, hfy⟩ := h2 _ hI' image_insert_eq.symm
    rw [hf.eq_iff (hI.subset_ground hyI) hxE] at hfy
    rwa [← hfy]
  rintro ⟨x, ⟨hxE, hxi⟩, rfl⟩
  refine ⟨⟨x, hxE, rfl⟩, fun J hJ hJI ↦ ⟨x, hxi ?_, rfl⟩⟩
  replace hJ := hJ.map f hf
  have hrw := image_insert_eq ▸ hJI
  rwa [← hrw, map_image_indep_iff (insert_subset hxE hI.subset_ground)] at hJ

Goal state after:
Module: Mathlib.FieldTheory.AlgebraicClosure

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : algebraicClosure E K = ⊥
⊢ IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E) = algebraicClosure F K

Tactic:
refine le_antisymm (map_le_of_algHom _) (fun x hx ↦ ?_)

Goal state after:
F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : algebraicClosure E K = ⊥
x : K
hx : x ∈ algebraicClosure F K
⊢ x ∈ IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E)
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
comm : Commute g h
x : α
⊢ g • x = x ↔ x ∈ fixedBy α g

Tactic:
mem_fixedBy

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
comm : Commute g h
x : α
⊢ g • x = x ↔ g • x = x
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : FaithfulSMul M α
m : M
⊢ (∀ (x : α), x ∈ fixedBy α m) ↔ ∀ (x : α), m • x = x

Tactic:
mem_fixedBy

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
m : M
⊢ (∀ y ∈ s, m • y = y) ↔ ∀ x ∈ s, x ∈ fixedBy α m

Tactic:
mem_fixedBy

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
ι' : Type u
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis R y
⊢ #ι = #ι'

Tactic:
by
  rw [← lift_id #ι, lift_cardinalMk_eq hx hy, lift_id]

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

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : U ∈ B.toFilterBasis
V : Set G
V_in : V ∈ B
hVU : V * V ⊆ U
⊢ ∀ a_1 ∈ (fun y ↦ a * y) '' V, (fun y ↦ a * y) '' id U ∈ map (fun y ↦ a_1 * y) B.filter

Tactic:
rintro _ ⟨x, hx, rfl⟩

Goal state after:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : U ∈ B.toFilterBasis
V : Set G
V_in : V ∈ B
hVU : V * V ⊆ U
x : G
hx : x ∈ V
⊢ (fun y ↦ a * y) '' id U ∈ map (fun y ↦ (fun y ↦ a * y) x * y) B.filter
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_1
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ U ∈ B, ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U

Tactic:
intro U U_in

Goal state after:
case refine_1
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
U : Set G
U_in : U ∈ B
⊢ ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_1
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
U : Set G
U_in : U ∈ B
⊢ ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U

Tactic:
rcases mul U_in with ⟨V, V_in, hV⟩

Goal state after:
case refine_1
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
U : Set G
U_in : U ∈ B
V : Set G
V_in : V ∈ B
hV : V * V ⊆ U
⊢ ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_2
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ ib ∈ B, ∃ ia ∈ B, ∀ x ∈ id ia, x⁻¹ ∈ id ib

Tactic:
intro U U_in

Goal state after:
case refine_2
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
U : Set G
U_in : U ∈ B
⊢ ∃ ia ∈ B, ∀ x ∈ id ia, x⁻¹ ∈ id U
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
h : f.natSepDegree = 1
⊢ ∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m

Tactic:
obtain ⟨p, hM, hI, hf⟩ := exists_monic_irreducible_factor _ <| not_isUnit_of_natDegree_pos _
    <| Nat.pos_of_ne_zero <| (natSepDegree_ne_zero_iff _).1 (h.symm ▸ Nat.one_ne_zero)

Goal state after:
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
⊢ ∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_4
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
x₀ : G
⊢ ∀ ib ∈ B, ∃ ia ∈ B, ∀ x ∈ id ia, x₀ * x * x₀⁻¹ ∈ id ib

Tactic:
intro U U_in

Goal state after:
case refine_4
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
x₀ : G
U : Set G
U_in : U ∈ B
⊢ ∃ ia ∈ B, ∀ x ∈ id ia, x₀ * x * x₀⁻¹ ∈ id U
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hmul
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := B.toAddGroupFilterBasis
this✝ : TopologicalSpace R := B'.topology
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ ∀ U ∈ B', ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U

Tactic:
intro U U_in

Goal state after:
case hmul
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := B.toAddGroupFilterBasis
this✝ : TopologicalSpace R := B'.topology
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
U : Set R
U_in : U ∈ B'
⊢ ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U
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 = ⊥
⊢ IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E) = separableClosure F K

Tactic:
refine le_antisymm (map_le_of_algHom _) (fun x hx ↦ ?_)

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 : separableClosure E K = ⊥
x : K
hx : x ∈ separableClosure F K
⊢ x ∈ IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case e'_2
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
⊢ (∃ n x_1, (algebraMap F E) x_1 = x ^ q ^ n) ↔ ∃ n y, x ^ q ^ n - (algebraMap F E) y = 0

Tactic:
sub_eq_zero,

Goal state after:
case e'_2
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
⊢ (∃ n x_1, (algebraMap F E) x_1 = x ^ q ^ n) ↔ ∃ n y, x ^ q ^ n = (algebraMap F E) y
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
h✝ : (minpoly F x).natSepDegree = 1
n : ℕ
y : F
h : minpoly F x = X ^ q ^ n - C y
hx : x ^ q ^ n - (algebraMap F E) y = 0
⊢ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n

Tactic:
sub_eq_zero,

Goal state after:
case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
h✝ : (minpoly F x).natSepDegree = 1
n : ℕ
y : F
h : minpoly F x = X ^ q ^ n - C y
hx : x ^ q ^ n = (algebraMap F E) y
⊢ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case h
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
h✝ : (minpoly F x).natSepDegree = 1
n : ℕ
y : F
h : minpoly F x = X ^ q ^ n - C y
hx : (algebraMap F E) y = x ^ q ^ n
⊢ X ^ q ^ n - Polynomial.map (algebraMap F E) (C y) = (X - C x) ^ q ^ n

Tactic:
map_C,

Goal state after:
case h
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
h✝ : (minpoly F x).natSepDegree = 1
n : ℕ
y : F
h : minpoly F x = X ^ q ^ n - C y
hx : (algebraMap F E) y = x ^ q ^ n
⊢ X ^ q ^ n - C ((algebraMap F E) y) = (X - C x) ^ q ^ n
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : ModuleFilterBasis R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun x ↦ x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun x ↦ x • m₀) ⁻¹' U
x✝ : TopologicalSpace R := BR.topology
⊢ ∀ {U : Set M}, U ∈ BM.sets → ∃ V ∈ 𝓝 0, ∃ W ∈ BM.sets, V • W ⊆ U

Tactic:
intro U U_in

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : ModuleFilterBasis R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun x ↦ x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun x ↦ x • m₀) ⁻¹' U
x✝ : TopologicalSpace R := BR.topology
U : Set M
U_in : U ∈ BM.sets
⊢ ∃ V ∈ 𝓝 0, ∃ W ∈ BM.sets, V • W ⊆ U