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

Goal state before:
pp: α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hcl : z ∈ M.closure ((⋃ i, I i) ∪ J \ {z})
⊢ ∃ C' ⊆ J ∪ ⋃ i, I i, M.IsCircuit C' ∧ z ∈ C'

Tactic:
mem_closure_iff_exists_isCircuit (by simp [hzI])

Goal state after:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hcl : ∃ C ⊆ insert z ((⋃ i, I i) ∪ J \ {z}), M.IsCircuit C ∧ z ∈ C
⊢ ∃ C' ⊆ J ∪ ⋃ i, I i, M.IsCircuit C' ∧ z ∈ C'
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (Insert.insert e X) ≤ M.eRk X
⊢ M.closure X = M.closure Y

Tactic:
refine hX.closure_eq_closure_of_subset_of_eRk_ge_eRk hXY <| not_lt.1 fun hlt ↦ ?_
  obtain ⟨z, hz, hr⟩ := exists_eRk_insert_eq_add_one_of_lt hlt
  simpa [hr, ENat.add_one_le_iff hX.eRk_lt_top.ne] using hY z hz

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hX : M.IsRkFinite I
h : I.encard ≤ M.eRk I
⊢ M.eRk I = I.encard

Tactic:
exact (M.eRk_le_encard I).antisymm h

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

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
X : Set α
hX : X ⊆ M.E
⊢ (∀ t ∈ {F | M.IsFlat F ∧ X ⊆ F}, e ∈ t) ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F

Tactic:
mem_ofPred,

Goal state after:
α : Type u_2
M : Matroid α
e : α
X : Set α
hX : X ⊆ M.E
⊢ (∀ (t : Set α), M.IsFlat t ∧ X ⊆ t → e ∈ t) ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
Y X : Set α
hX : X ⊆ M.E
⊢ (∀ t' ∈ {F | M.IsFlat F ∧ X ⊆ F}, Y ⊆ t') ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F

Tactic:
mem_ofPred,

Goal state after:
α : Type u_2
M : Matroid α
Y X : Set α
hX : X ⊆ M.E
⊢ (∀ (t' : Set α), M.IsFlat t' ∧ X ⊆ t' → Y ⊆ t') ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
by
  simp [h, ← M.closure_iUnion_closure_eq_closure_iUnion]

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:
← sdiff_eq_empty,

Goal state after:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K) = ∅
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
hB' : M✶.IsBase B
hd : M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
⊢ (B ∩ X ∪ M.E \ B).encard = (M.E \ B ∩ (M.E \ X) ∪ X).encard

Tactic:
exact congr_arg _ (by tauto_set)

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

Goal state before:
pp: α : Type u
M : Matroid α
B : { B // M.IsBase B }
⊢ #↑↑B ≤ #↑↑⟨↑B, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.Finitary ↔ ∀ (C : Set α), M.IsCircuit C → C.Finite

Tactic:
refine ⟨fun _ _ ↦ IsCircuit.finite, fun h ↦
    ⟨fun I hI ↦ indep_iff_not_dep.2 ⟨fun hd ↦ ?_,fun x hx ↦ ?_⟩⟩⟩

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
⊢ False

case refine_2
α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
x : α
hx : x ∈ I
⊢ x ∈ M.E
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
mem_ofPred,

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
⊢ M.IsBasis I (insert x I) ↔ M.Dep (insert x I) ∨ x ∈ I
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: case refine_1
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I X' : Set α
hIX : M.IsBasis I X'
hXX' : f '' X = f '' X'
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ lift.{u, v} #↑(f '' I) ≤ lift.{v, u} (⨆ B, #↑↑B)

Tactic:
rw [mk_image_eq_of_injOn_lift _ _ (hf.mono hIX.indep.subset_ground), lift_le]

Goal state after:
case refine_1
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I X' : Set α
hIX : M.IsBasis I X'
hXX' : f '' X = f '' X'
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ #↑I ≤ ⨆ B, #↑↑B
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
⊢ M.IsNonloop e ∧ e ∈ {e | M.IsNonloop e} ↔ M.IsNonloop e

Tactic:
mem_ofPred,

Goal state after:
α : Type u_1
M : Matroid α
e : α
⊢ M.IsNonloop e ∧ M.IsNonloop e ↔ M.IsNonloop e
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
⊢ False

Tactic:
have' hKe := hK.2 (t := K \ {e}) (sdiff_singleton_ssubset.2 (he.symm.subset rfl).2)

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ False
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
heI : e ∈ I
X : Set α
hX' : X ∈ Js
⊢ e ∈ X

Tactic:
rw [← hI.closure_inter_eq_self_of_subset (hIs X hX')]

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)
heI : e ∈ I
X : Set α
hX' : X ∈ Js
⊢ e ∈ M.closure X ∩ I
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
this : Transcendental (↥(supported R ∅)) ((Polynomial.aeval (X i)) f)
g : R ≃ₐ[R] ↥(supported R ∅) := (Algebra.botEquivOfInjective ⋯).symm.trans ((supported R ∅).equivOfEq ⊥ ⋯).symm
x✝ : R
⊢ ((algebraMap (↥(supported R ∅)) (MvPolynomial σ R)).comp ↑g) x✝ =
    ((↑(RingHom.id (MvPolynomial σ R))).comp (algebraMap R (MvPolynomial σ R))) x✝

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
⊢ M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I (M.closure (X ∩ M.E)) ∧ I ⊆ X

Tactic:
exact ⟨fun h ↦ ⟨h.isBasis_closure_right, h.subset.trans inter_subset_left⟩,
    fun h ↦ h.1.isBasis_subset (subset_inter h.2 h.1.indep.subset_ground) (M.subset_closure _)⟩

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

Goal state before:
pp: case inr.inr.inr
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'✝ : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ insert e B ⊆ insert f (M.E \ (insert f (M.E \ B) \ {e}))

Tactic:
rw [sdiff_sdiff_right, inter_eq_self_of_subset_right (by simpa), union_singleton, insert_comm,
    ← union_singleton (s := M.E \ B), ← sdiff_sdiff, sdiff_sdiff_cancel_left hB.subset_ground]

Goal state after:
case inr.inr.inr
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'✝ : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ insert e B ⊆ insert e (insert f (B \ {f}))
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e f : α
B : Set α
hB : M.IsBasis B X
he : e ∈ M.closure (insert f B \ {e})
heB : e ∈ insert f B
hfX : f ∈ X
⊢ M.IsBasis (insert f B \ {e}) X

Tactic:
isBasis_iff_indep_closure

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e f : α
B : Set α
hB : M.Indep B ∧ X ⊆ M.closure B ∧ B ⊆ X
he : e ∈ M.closure (insert f B \ {e})
heB : e ∈ insert f B
hfX : f ∈ X
⊢ M.Indep (insert f B \ {e}) ∧ X ⊆ M.closure (insert f B \ {e}) ∧ insert f B \ {e} ⊆ X
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: 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

Tactic:
rfl

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

Goal state before:
pp: 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

Tactic:
rfl

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

Goal state before:
pp: case neg
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e})
heB : e ∈ insert f B
hf : f ∉ M.E
⊢ M.IsBasis (insert f B \ {e}) M.E

Tactic:
obtain rfl | heB := heB

Goal state after:
case neg.inl
α : Type u_2
M : Matroid α
e : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert e B \ {e})
hf : e ∉ M.E
⊢ M.IsBasis (insert e B \ {e}) M.E

case neg.inr
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e})
hf : f ∉ M.E
heB : e ∈ B
⊢ M.IsBasis (insert f B \ {e}) M.E
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: 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✝)

Tactic:
rfl

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

Goal state before:
pp: 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✝)

Tactic:
rfl

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
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s t : Set ι
⊢ (AlgebraicIndependent ↥(adjoin R (x '' s)) fun i ↦ x ↑i) ↔ Disjoint s t

Tactic:
by
  refine ⟨fun ind ↦ of_not_not fun ndisj ↦ ?_, adjoin_of_disjoint hx⟩
  have ⟨i, hs, ht⟩ := Set.not_disjoint_iff.mp ndisj
  refine ind.transcendental ⟨i, ht⟩ (isAlgebraic_algebraMap (⟨_, subset_adjoin ?_⟩ : adjoin R _))
  exact ⟨i, hs, rfl⟩

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 = a ↔ a ∈ fixedBy α g

Tactic:
rfl

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

Goal state before:
pp: ι : 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
B : Set A
⊢ Maximal (AlgebraicIndepOn R _root_.id) B ↔ Maximal (indepMatroid R A).matroid.Indep B

Tactic:
rfl

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✝ : IsDomain A
s B : Set A
hB : (matroid R A).IsBasis B s
⊢ ∀ (x : A), x ∈ {x | (matroid R A).IsBasis B (insert x B)} ↔ x ∈ ↑(algebraicClosure (↥(adjoin R s)) A)

Tactic:
mem_ofPred,

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✝ : IsDomain A
s B : Set A
hB : (matroid R A).IsBasis B s
⊢ ∀ (x : A), (matroid R A).IsBasis B (insert x B) ↔ x ∈ ↑(algebraicClosure (↥(adjoin R s)) A)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔ (f.aroots f.SplittingField).toFinset.card = f.natDegree

Tactic:
rfl

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: E : Type v
inst✝¹ : Field E
K : Type w
inst✝ : Field K
f : E[X]
i : E →+* K
x✝ : Algebra E K := i.toAlgebra
⊢ i = algebraMap E K

Tactic:
rfl

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

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
sets : Set (Set G)
nonempty : sets.Nonempty
inter_sets : ∀ (x y : Set G), x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y
one : ∀ U ∈ sets, 1 ∈ U
mul : ∀ U ∈ sets, ∃ V ∈ sets, V * V ⊆ U
inv : ∀ U ∈ sets, ∃ V ∈ sets, V ⊆ (fun x ↦ x⁻¹) ⁻¹' U
x : G
U : Set G
U_in : U ∈ sets
⊢ U ⊆ U

Tactic:
rfl

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
⊢ f.natSepDegree = 1 ↔ ∃ n y, f = X ^ q ^ n - C y

Tactic:
by
  simp_rw [hi.natSepDegree_eq_one_iff_of_monic' q hm, map_sub, expand_X, expand_C]

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

Goal state before:
pp: case refine_3
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
⊢ B.N x₀ = map (fun x ↦ x₀ * x) B.filter

Tactic:
rfl

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

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

Tactic:
have : IsTopologicalGroup G := hG ▸ F.isTopologicalGroup

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

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

Tactic:
F.t2Space_iff hG,

Goal state after:
G : Type u
inst✝ : Group G
t : TopologicalSpace G
F : GroupFilterBasis G
hG : F.topology = t
⊢ ⋂₀ F.sets = {1} ↔ ⋂₀ F.sets ⊆ {1}
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
⊢ ⊥.fixingSubgroup = ⊤

Tactic:
by
  ext
  simp [mem_bot]

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
H : Subgroup Gal(E/F)
K : IntermediateField F E
x✝¹ x✝ : ↥K.fixingSubgroup
a✝ : E
⊢ (let __src := (↑(x✝¹ * x✝)).toRingEquiv;
      { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ })
      a✝ =
    ((let __src := (↑x✝¹).toRingEquiv;
        { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }) *
        let __src := (↑x✝).toRingEquiv;
        { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ })
      a✝

Tactic:
rfl

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
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
x : E
⊢ IsSeparable F (i x) ↔ IsSeparable F x

Tactic:
IsSeparable,

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
i : E →ₐ[F] K
x : E
⊢ (minpoly F (i x)).Separable ↔ (minpoly F x).Separable
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
⊢ ∀ {U : Set M},
    U ∈
        (have this := default;
          this).sets →
      ∃ V ∈ 𝓝 0,
        ∃
          W ∈
            (have this := default;
              this).sets,
          V • W ⊆ U

Tactic:
rintro U (rfl : U ∈ {{(0 : M)}})

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
⊢ ∃ V ∈ 𝓝 0,
    ∃
      W ∈
        (have this := default;
          this).sets,
      V • W ⊆ {0}
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
H : Subgroup Gal(E/F)
K✝ : IntermediateField F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
K L : IntermediateField F E
⊢ { toFun := ⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup, invFun := fixedField ∘ ⇑OrderDual.ofDual,
          left_inv := ⋯, right_inv := ⋯ }
        K ≤
      { toFun := ⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup, invFun := fixedField ∘ ⇑OrderDual.ofDual,
          left_inv := ⋯, right_inv := ⋯ }
        L ↔
    L.fixingSubgroup ≤ K.fixingSubgroup

Tactic:
rfl

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

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
σ τ : Gal(L/K)
⊢ (∀ a ∈ E, σ.symm (τ (σ a)) = a) ↔ ∀ y ∈ E, ((MulAut.conj σ)⁻¹ • τ) y = y

Tactic:
rfl

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
α : E
halg : IsAlgebraic F α
⊢ finSepDegree F ↥F⟮α⟯ = (minpoly F α).natSepDegree

Tactic:
by
  have : finSepDegree F F⟮α⟯ = _ := Nat.card_congr
    (algHomAdjoinIntegralEquiv F (K := AlgebraicClosure F⟮α⟯) halg.isIntegral)
  classical
  rw [this, Nat.card_eq_fintype_card, natSepDegree_eq_of_isAlgClosed (E := AlgebraicClosure F⟮α⟯),
    ← Fintype.card_coe]
  simp_rw [Multiset.mem_toFinset]

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
α : E
halg : IsAlgebraic F α
⊢ (minpoly F α).Separable ↔ IsSeparable F α

Tactic:
IsSeparable

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
⊢ (minpoly F α).Separable ↔ (minpoly F α).Separable
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: case refine_1
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑σ.symm) E
this : FiniteDimensional K ↥E
⊢ F ∈ finiteExts K L

Tactic:
exact IntermediateField.finiteDimensional_map σ.symm.toAlgHom

Goal state after:
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_ne_0 : g ≠ 0
g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f
algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)
x : ↥(integralClosure R K)
⊢ ((algebraMap R K).comp (↑algeq).toRingHom) x = (integralClosure R K).toSubring.subtype (algeq.symm (algeq x))

Tactic:
rfl

Goal state after:
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
p : R[X]
hirr : Irreducible p
hp : (Polynomial.aeval x) p = 0
int_x : IsIntegral R x
⊢ IsUnit p.leadingCoeff

Tactic:
obtain ⟨p, rfl⟩ := isIntegrallyClosed_dvd int_x hp

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
x : S
int_x : IsIntegral R x
p : R[X]
hirr : Irreducible (minpoly R x * p)
hp : (Polynomial.aeval x) (minpoly R x * p) = 0
⊢ IsUnit (minpoly R x * p).leadingCoeff
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 * x) '' Set.Iio i) ≤ Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))

Tactic:
apply Submodule.span_mono

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
⊢ (fun x_1 ↦ x ^ x_1 * x) '' Set.Iio i ⊆ (fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1)
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case pos
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : IsIntegral R x
⊢ (minpolyDiv R x).natDegree = (minpolyDiv R x).natDegree + 1 - 1

Tactic:
rfl

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

Goal state before:
pp: case neg
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : ¬IsIntegral R x
⊢ natDegree 0 = natDegree 0 - 1

Tactic:
rfl

Goal state after:
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
⊢ C 0 * X ^ n + C b * X = 0 * X ^ n + C b * X

Tactic:
grind

Goal state after:
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
H : (ClosedSubgroup Gal(K/k))ᵒᵈ
⊢ { toSubgroup := ↑H, isClosed' := ⋯ } = H

Tactic:
rfl

Goal state after:
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✝
K L : IntermediateField k K✝
⊢ { toFun := fun L ↦ { toSubgroup := L.fixingSubgroup, isClosed' := ⋯ },
          invFun := fun H ↦ IntermediateField.fixedField ↑H, left_inv := ⋯, right_inv := ⋯ }
        K ≤
      { toFun := fun L ↦ { toSubgroup := L.fixingSubgroup, isClosed' := ⋯ },
          invFun := fun H ↦ IntermediateField.fixedField ↑H, left_inv := ⋯, right_inv := ⋯ }
        L ↔
    L.fixingSubgroup ≤ K.fixingSubgroup

Tactic:
rfl

Goal state after: