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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase (M.E \ B) ↔ Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) B

Tactic:
simp_rw [maximal_iff, and_iff_right hB, and_imp, forall_exists_index]
  refine ⟨fun h ↦ ⟨⟨_, h, disjoint_sdiff_right⟩,
    fun I hI B' ⟨hB', hIB'⟩ hBI ↦ hBI.antisymm ?_⟩, fun ⟨⟨B', hB', hBB'⟩,h⟩ ↦ ?_⟩
  · rw [hB'.eq_of_subset_isBase h, ← subset_compl_iff_disjoint_right, sdiff_eq, compl_inter,
      compl_compl] at hIB'
    · exact fun e he ↦ (hIB' he).elim (fun h' ↦ (h' (hI he)).elim) id
    rw [subset_sdiff, and_iff_right hB'.subset_ground, disjoint_comm]
    exact disjoint_of_subset_left hBI hIB'
  rw [h sdiff_subset B' ⟨hB', disjoint_sdiff_left⟩]
  · simpa [hB'.subset_ground]
  simp [subset_sdiff, hB, hBB']

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ M.IsBasis I (X ∪ Y)

Tactic:
by
  convert! hIX.union_isBasis_union hIY _ <;> rw [union_self]; exact hIX.indep

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u_5
inst✝³ : CommRing R
inst✝² : IsFractionRing R R
I J : Ideal R
inst✝¹ : Module.Invertible R ↥I
inst✝ : Module.Invertible R ↥J
h : Pic.mk R (↥I ⊗[R] ↥J) = 1
e✝ : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
x✝ : R
⊢ x✝ • ↑(e 1) = (Subtype.val ∘ ⇑e) x✝

Tactic:
← Submodule.coe_smul,

Goal state after:
R : Type u_5
inst✝³ : CommRing R
inst✝² : IsFractionRing R R
I J : Ideal R
inst✝¹ : Module.Invertible R ↥I
inst✝ : Module.Invertible R ↥J
h : Pic.mk R (↥I ⊗[R] ↥J) = 1
e✝ : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
x✝ : R
⊢ ↑(x✝ • e 1) = (Subtype.val ∘ ⇑e) x✝
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: case neg
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
E₀ : Set α := insert e (I₀ ∪ B₀)
hE₀fin : E₀.Finite
J : Set α
hJmax : ∀ ⦃j : Set α⦄, (fun x ↦ x ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}) j → id J ⊆ id j → id j ⊆ id J
hB₀J : B₀ ⊆ J
hJ : Indep J
hJss : J ⊆ E₀
heI₀ : e ∉ I₀
heI₀i : Indep (insert e I₀)
heJ : e ∉ J
hJfin : J.Finite
hcard : I₀.ncard + 1 ≤ J.ncard
⊢ False

Tactic:
← Nat.lt_iff_add_one_le

Goal state after:
case neg
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
E₀ : Set α := insert e (I₀ ∪ B₀)
hE₀fin : E₀.Finite
J : Set α
hJmax : ∀ ⦃j : Set α⦄, (fun x ↦ x ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}) j → id J ⊆ id j → id j ⊆ id J
hB₀J : B₀ ⊆ J
hJ : Indep J
hJss : J ⊆ E₀
heI₀ : e ∉ I₀
heI₀i : Indep (insert e I₀)
heJ : e ∉ J
hJfin : J.Finite
hcard : I₀.ncard < J.ncard
⊢ False
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
R R' : Set α
M : Matroid α
h : R ⊆ R'
⊢ M ↾ R ≤r M ↾ R'

Tactic:
by
  rw [← restrict_restrict_eq M h]; exact restrict_isRestriction _ _ h

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.IsRkFinite X
e : α
⊢ M.IsRkFinite (Insert.insert e X)

Tactic:
by
  rw [← union_singleton]
  exact hX.union M.isRkFinite_singleton

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 : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
I : Set β
⊢ (M.mapSetEmbedding { toFun := M.E.domRestrict f, inj' := ⋯ }).Indep I ↔ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀

Tactic:
simp_rw [mapSetEmbedding_indep_iff', Embedding.coeFn_mk, domRestrict_apply,
      ← image_image f Subtype.val, Subtype.exists_set_subtype (p := fun J ↦ M.Indep J ∧ I = f '' J)]

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
I : Set β
⊢ (∃ s ⊆ M.E, M.Indep s ∧ I = f '' s) ↔ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ BijOn Subtype.val (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E

Tactic:
exact ⟨by simp [MapsTo], Subtype.val_injective.injOn, by simp [SurjOn]⟩

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

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

Tactic:
by
  rw [← eRk_inter_ground, inter_eq_self_of_subset_right subset_union_right, eRank_def]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
M✝ : Matroid α
F X Y : Set α
e f : α
M : Matroid α
s : Set ↑(Iic M.E)
hs : ∀ a ∈ s, M.IsFlat ↑a
⊢ M.IsFlat ↑(sInf s)

Tactic:
obtain (rfl | hne) := s.eq_empty_or_nonempty

Goal state after:
case inl
ι : Type u_1
α : Type u_2
M✝ : Matroid α
F X Y : Set α
e f : α
M : Matroid α
hs : ∀ a ∈ ∅, M.IsFlat ↑a
⊢ M.IsFlat ↑(sInf ∅)

case inr
ι : Type u_1
α : Type u_2
M✝ : Matroid α
F X Y : Set α
e f : α
M : Matroid α
s : Set ↑(Iic M.E)
hs : ∀ a ∈ s, M.IsFlat ↑a
hne : s.Nonempty
⊢ M.IsFlat ↑(sInf s)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
I : Set α
he : M.IsColoop e
hI : M.Indep I
⊢ M.Indep (insert e I)

Tactic:
by
  refine (em (e ∈ I)).elim (fun h ↦ by rwa [insert_eq_of_mem h]) fun h ↦ ?_
  rw [← hI.notMem_closure_iff_of_notMem h]
  exact he.notMem_closure_of_notMem h

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

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

Tactic:
rw [hI.insert_indep_iff, and_iff_right hI, or_iff_not_imp_right]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := mapAlgHom (Polynomial.aeval f)
hf : Function.Injective ⇑g
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (((supported R (insert i s)).val.comp
            ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                (supportedEquivMvPolynomial (insert i s)).symm)).comp
        g).comp
    ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s))
⊢ Function.Injective ⇑(Polynomial.aeval ((Polynomial.aeval (X i)) f))

Tactic:
let v := ((Polynomial.aeval (R := supported R s)
    (Polynomial.aeval (X i : MvPolynomial σ R) f)).restrictScalars R).comp
      (Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm).toAlgHom

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := mapAlgHom (Polynomial.aeval f)
hf : Function.Injective ⇑g
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (((supported R (insert i s)).val.comp
            ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                (supportedEquivMvPolynomial (insert i s)).symm)).comp
        g).comp
    ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s))
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
    ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm)
⊢ Function.Injective ⇑(Polynomial.aeval ((Polynomial.aeval (X i)) f))
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case refine_2
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBase B ∧ B ⊆ S
⊢ S ⊆ M.closure B

Tactic:
rw [h.1.closure_eq]

Goal state after:
case refine_2
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBase B ∧ B ⊆ S
⊢ S ⊆ M.E
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: case inl
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
s : ℕ
hm : m ≤ m + s
hg : ((expand F (q ^ s)) g').Separable
h : IsUnit g'
⊢ g'.natDegree * q ^ s = g'.natDegree

Tactic:
natDegree_eq_zero_of_isUnit h,

Goal state after:
case inl
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
s : ℕ
hm : m ≤ m + s
hg : ((expand F (q ^ s)) g').Separable
h : IsUnit g'
⊢ 0 * q ^ s = 0
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X B : Set α
hB : M.IsBase B
hX : M.Spanning X
hXB : X ⊆ B
B' : Set α
hB' : M.IsBase B'
hB'X : B' ⊆ X
⊢ B ⊆ X

Tactic:
rwa [← hB'.eq_of_subset_isBase hB (hB'X.trans hXB)]

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

Goal state before:
pp: case inr
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : IsTranscendenceBasis R x
h✝ : Nontrivial R
⊢ IsTranscendenceBasis R Subtype.val

Tactic:
· rwa [isTranscendenceBasis_subtype_range hx.1.injective]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
R S : Set α
⊢ (M ↾ R).Spanning S ↔ R ∩ M.E ⊆ M.closure S ∧ S ⊆ R

Tactic:
by
  rw [spanning_iff, restrict_closure_eq', restrict_ground_eq, and_congr_left_iff,
    sdiff_eq_compl_inter, ← union_inter_distrib_right, inter_eq_right, union_comm,
    ← sdiff_subset_iff, sdiff_compl]
  intro hSR
  rw [inter_eq_self_of_subset_left hSR]

Goal state after:
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
⊢ lift.{v', v} (trdeg R A) ≤ lift.{v, v'} (trdeg R A')

Tactic:
rw [trdeg, lift_iSup bddAbove_of_small]

Goal state after:
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')
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 : Surjective ⇑f
a✝ : Nontrivial R
⊢ lift.{v, v'} (trdeg R A') ≤ lift.{v', v} (trdeg R A)

Tactic:
rw [trdeg, lift_iSup bddAbove_of_small]

Goal state after:
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 : Surjective ⇑f
a✝ : Nontrivial R
⊢ ⨆ i, lift.{v, v'} #↑↑i ≤ lift.{v', v} (trdeg R A)
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
hx : AlgebraicIndependent R x
⊢ Polynomial.map (↑hx.aevalEquiv) (none.elim Polynomial.X fun s ↦ Polynomial.C (X s)) = Polynomial.X

Tactic:
Option.elim,

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
⊢ Polynomial.map (↑hx.aevalEquiv) Polynomial.X = Polynomial.X
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
hx : AlgebraicIndependent R x
i : ι
⊢ Polynomial.map (↑hx.aevalEquiv) ((some i).elim Polynomial.X fun s ↦ Polynomial.C (X s)) =
    Polynomial.C (hx.aevalEquiv (X i))

Tactic:
Option.elim,

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
i : ι
⊢ Polynomial.map (↑hx.aevalEquiv) (Polynomial.C (X i)) = Polynomial.C (hx.aevalEquiv (X i))
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: case refine_2
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ ∀ (i : Option ι),
    (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (X i)) = (aeval fun o ↦ o.elim a x) (X i)

Tactic:
rintro (⟨⟩ | ⟨i⟩)
    · rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_none, aeval_X, Polynomial.aeval_X,
        Option.elim]
    · rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_some, Polynomial.aeval_C,
        hx.algebraMap_aevalEquiv, aeval_X, aeval_X, Option.elim]

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

Goal state before:
pp: case inr
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
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✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : IsTranscendenceBasis R Subtype.val
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
h✝ : Nontrivial R
⊢ Algebra.IsAlgebraic (↥(adjoin R (range fun i ↦ _root_.id ↑i))) A

Tactic:
replace B_base := B_base.isAlgebraic

Goal state after:
case inr
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
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✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
h✝ : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R (range Subtype.val))) A
⊢ Algebra.IsAlgebraic (↥(adjoin R (range fun i ↦ _root_.id ↑i))) A
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
inst✝ : IsTopologicalRing R
⊢ ContinuousSMul R M

Tactic:
by
  let B' := B.toAddGroupFilterBasis
  let _ := B'.topology
  exact ContinuousSMul.of_basis_zero B'.nhds_zero_hasBasis
      (fun {_} => by simpa using! B.smul)
      (by simpa using! B.smul_left) B.smul_right

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case pos
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:
refine induction_on_adjoin (fun K : IntermediateField F E ↦ finSepDegree F K ∣ finrank F K)
      (by simp_rw [finSepDegree_bot, IntermediateField.finrank_bot, one_dvd]) (fun L x h ↦ ?_) ⊤

Goal state after:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree F ↥L ∣ finrank F ↥L
⊢ finSepDegree F ↥(IntermediateField.restrictScalars F (↥L)⟮x⟯) ∣
    finrank F ↥(IntermediateField.restrictScalars F (↥L)⟮x⟯)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case inr
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst : Field E] [inst_1 : Algebra F E] [Algebra.IsSeparable F E],
    FiniteDimensional F E → finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
L : IntermediateField F E
h : FiniteDimensional F ↥L
h' : finSepDegree F E < finrank F ↥L
hd : finSepDegree F ↥L * finSepDegree (↥L) E = finSepDegree F E
⊢ finSepDegree F E = 0

Tactic:
rw [H L h] at hd

Goal state after:
case inr
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst : Field E] [inst_1 : Algebra F E] [Algebra.IsSeparable F E],
    FiniteDimensional F E → finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
L : IntermediateField F E
h : FiniteDimensional F ↥L
h' : finSepDegree F E < finrank F ↥L
hd : finrank F ↥L * finSepDegree (↥L) E = finSepDegree F E
⊢ finSepDegree F E = 0
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
⊢ (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g

Tactic:
obtain ⟨x, hx⟩ := DFunLike.exists_ne hfg

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
⊢ (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
⊢ ∃ g', map (algebraMap R K) g' * C g.leadingCoeff = g

Tactic:
have g_ne_0 : g ≠ 0 := ne_zero_of_dvd_ne_zero (Monic.ne_zero <| hf.map (algebraMap R K)) hg

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
⊢ ∃ g', map (algebraMap R K) g' * C g.leadingCoeff = g
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
⊢ Irreducible p ↔ Irreducible (Polynomial.map (algebraMap R K) p)

Tactic:
refine
    ⟨fun hp =>
      irreducible_iff.mpr
        ⟨hp.not_isUnit.imp h.isPrimitive.isUnit_iff_isUnit_map.mpr, fun a b H =>
          or_iff_not_imp_left.mpr fun hₐ => ?_⟩,
      fun hp =>
      h.isPrimitive.irreducible_of_irreducible_map_of_injective (IsFractionRing.injective R K) hp⟩

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
H : Polynomial.map (algebraMap R K) p = a * b
hₐ : ¬IsUnit a
⊢ IsUnit b
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
h1 : C c * C d * p = integerNormalization R⁰ a * integerNormalization R⁰ b
this : NormalizedGCDMonoid R
⊢ Associated (c * d) ((C (c * d)).content * p.content)

Tactic:
content_C,

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
h1 : C c * C d * p = integerNormalization R⁰ a * integerNormalization R⁰ b
this : NormalizedGCDMonoid R
⊢ Associated (c * d) (normalize (c * d) * p.content)
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

Goal state after:
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) :=
  fun x ↦ Subgroup.map (restrictNormalHom ↥(adjoin k {x}).toIntermediateField) L.fixingSubgroup
f : ↥L → IntermediateField k K := fun x ↦ IntermediateField.lift (IntermediateField.fixedField (g ↑x))
this✝ : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal k ↥(f l)
n : Normal k ↥(⨆ l, f l)
l : K
hl : l ∈ L
⊢ l ∈ ⨆ l, f l
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
L : IntermediateField k K
inst✝ : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(adjoin k {x}).toIntermediateField/k) :=
  fun x ↦ Subgroup.map (restrictNormalHom ↥(adjoin k {x}).toIntermediateField) L.fixingSubgroup
f : ↥L → IntermediateField k K := fun x ↦ IntermediateField.lift (IntermediateField.fixedField (g ↑x))
this✝¹ : ∀ (x : K), (g x).Normal
this✝ : ∀ (l : ↥L), Normal k ↥(f l)
n : Normal k ↥(⨆ l, f l)
this : ⨆ l, f l = L
⊢ IsGalois k ↥L

Tactic:
rw [this] at n

Goal state after:
case refine_1
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) :=
  fun x ↦ Subgroup.map (restrictNormalHom ↥(adjoin k {x}).toIntermediateField) L.fixingSubgroup
f : ↥L → IntermediateField k K := fun x ↦ IntermediateField.lift (IntermediateField.fixedField (g ↑x))
this✝¹ : ∀ (x : K), (g x).Normal
this✝ : ∀ (l : ↥L), Normal k ↥(f l)
n : Normal k ↥L
this : ⨆ l, f l = L
⊢ IsGalois 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
inst✝ : Algebra.IsAlgebraic F E
⊢ #(Emb F ↥(separableClosure F E)) = #(Emb F E)

Tactic:
← (embProdEmbOfIsAlgebraic F (separableClosure F E) E).cardinal_eq,

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
⊢ #(Emb F ↥(separableClosure F E)) = #(Emb F ↥(separableClosure F E) × Emb (↥(separableClosure F E)) E)