mathlib-initiative/mathlib-tactics huggingface dataset:
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 α⦄,
    (∀ (J : Finset α), ↑J ⊆ I → Indep J) →
      I.Finite →
        (∀ (J_1 : Finset α), ↑J_1 ⊆ J → Indep J_1) →
          J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ ∀ (J : Finset α), ↑J ⊆ insert e I → Indep J

Tactic:
intro I J hI hIfin hJ hJfin 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 : I.ncard < J.ncard
⊢ ∃ 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 α
X : Set α
⊢ M.Coindep X ↔ (∃ B, M.IsBase B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E

Tactic:
by
  simp_rw [Coindep, dual_indep_iff_exists', and_comm (a := (_ : Set α) ⊆ _), and_congr_left_iff,
    subset_sdiff]
  exact fun _ ↦ ⟨fun ⟨B, hB, hXB⟩ ↦ ⟨B, hB, hB.subset_ground, hXB.symm⟩,
    fun ⟨B, hB, _, hBX⟩ ↦ ⟨B, hB, hBX.symm⟩⟩

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ e ∉ ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}

Tactic:
simp [show ∃ x ⊆ I, e ∈ M.closure x ∧ e ∉ x from ⟨I, by simp [hecl, heI]⟩]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ I.encard ≤ M.eRank

Tactic:
rw [← hI.eRk_eq_encard, eRank_def]

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.eRk I ≤ M.eRk M.E
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
⊢ M.closure {e} = M.closure {f} ↔ M.IsCircuit {e, f}

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · have hf := he.isNonloop_of_mem_closure (by rw [← h]; exact M.mem_closure_self e)
    rw [isCircuit_iff_dep_forall_sdiff_singleton_indep, dep_iff, insert_subset_iff,
      and_iff_right he.mem_ground, singleton_subset_iff, and_iff_left hf.mem_ground]
    suffices ¬ M.Indep {e, f} by simpa [pair_sdiff_left hef, hf, pair_sdiff_right hef, he]
    rw [Indep.insert_indep_iff_of_notMem (by simpa) (by simpa)]
    simp [← h, mem_closure_self _ _ he.mem_ground]
  have hclosure := (h.closure_sdiff_singleton_eq e).trans
    (h.closure_sdiff_singleton_eq f).symm
  rwa [pair_sdiff_left hef, pair_sdiff_right hef, eq_comm] at hclosure

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

Goal state before:
pp: α : Type u_1
M : Matroid α
Y X : Set α
hY : M.eRk Y ≤ 0
⊢ M.eRk X + M.eRk Y ≤ M.eRk X + 0

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
X : Set α
⊢ M.eRk X + M.eRk {e} ≤ M.eRk X + 1

Tactic:
gcongr

Goal state after:
case h₂
α : Type u_1
M : Matroid α
e : α
X : Set α
⊢ M.eRk {e} ≤ 1
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
I : Set α
he : e ∈ M.E ∧ (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I))
hI : M.IsBasis' I X
⊢ M.Indep (insert e I)

Tactic:
by tauto

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
I : Set α
he : e ∈ M.E ∧ (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I))
hI : M.IsBasis' I X
⊢ e ∉ I

Tactic:
by tauto

Goal state after:
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)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.closure (M.E \ K ∪ {e} ∪ C) ⊆ M.closure (M.E \ K)

Tactic:
rw [union_assoc, singleton_union, insert_eq_of_mem heC, ← closure_union_congr_right
      (hC.closure_sdiff_singleton_eq e), union_eq_self_of_subset_right]

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}))
⊢ C \ {e} ⊆ M.E \ K
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ (∀ (x : Set α), ¬M.IsCircuit x) ↔ ∀ C ⊆ M.E, ¬M.IsCircuit C

Tactic:
exact ⟨fun h C _ ↦ h C, fun h C hC ↦ h C hC.subset_ground hC⟩

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
⊢ LinearIndependent R x

Tactic:
by
  rw [linearIndependent_iff_injective_finsuppLinearCombination]
  have : Finsupp.linearCombination R x =
      (MvPolynomial.aeval x).toLinearMap.comp (Finsupp.linearCombination R X) := by
    ext
    simp
  rw [this]
  refine (algebraicIndependent_iff_injective_aeval.mp hx).comp ?_
  rw [← linearIndependent_iff_injective_finsuppLinearCombination]
  exact linearIndependent_X _ _

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

Goal state before:
pp: α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ #↑(f '' J \ f '' I) + #↑((f '' I ∩ f '' J) \ f '' (I ∩ J)) =
    #↑(f '' J \ f '' I) + #↑((f '' I ∩ f '' J) \ f '' (J ∩ I))

pp: α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ Disjoint (f '' J \ f '' I) ((f '' I ∩ f '' J) \ f '' (J ∩ I))

pp: α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ Disjoint (f '' I \ f '' J) ((f '' J ∩ f '' I) \ f '' (I ∩ J))

Tactic:
inter_comm J I

Goal state after:
α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ #↑(f '' J \ f '' I) + #↑((f '' I ∩ f '' J) \ f '' (I ∩ J)) =
    #↑(f '' J \ f '' I) + #↑((f '' I ∩ f '' J) \ f '' (I ∩ J))

α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ Disjoint (f '' J \ f '' I) ((f '' I ∩ f '' J) \ f '' (J ∩ I))

α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ Disjoint (f '' I \ f '' J) ((f '' J ∩ f '' I) \ f '' (I ∩ J))
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) ∪ M.E ∩ {e})

Tactic:
inter_eq_self_of_subset_right (by simpa),

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 f (M.E \ insert f (M.E \ B) ∪ {e})
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: R : Type u_3
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ trdeg R A ≠ 0 ↔ Algebra.Transcendental R A

Tactic:
Algebra.transcendental_iff_not_isAlgebraic,

Goal state after:
R : Type u_3
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ trdeg R A ≠ 0 ↔ ¬Algebra.IsAlgebraic R A
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
simpa [show e ∉ B from fun h ↦ hf (hB.1.1.2 h)] using hB

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
⊢ M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I

Tactic:
rw [indep_iff_forall_notMem_closure_sdiff']
  refine ⟨fun ⟨hIE, h⟩ e heI h_eq ↦ h e heI (h_eq.symm.subset (M.mem_closure_of_mem heI)),
    fun h ↦ ⟨fun e heI ↦ by_contra fun heE ↦ h heI ?_,fun e heI hin ↦ h heI ?_⟩⟩
  · rw [← closure_inter_ground, inter_comm, inter_sdiff_distrib_left,
      inter_singleton_eq_empty.mpr heE, sdiff_empty, inter_comm, closure_inter_ground]
  nth_rw 2 [show I = insert e (I \ {e}) by simp [heI]]
  rw [← closure_insert_closure_eq_closure_insert, insert_eq_of_mem hin, closure_closure]

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : AlgebraicIndependent R x
⊢ lift.{v, u} #ι ≤ lift.{u, v} (trdeg R A)

Tactic:
by
  rw [lift_mk_eq'.mpr ⟨.ofInjective _ hx.injective⟩, lift_le]
  exact le_ciSup_of_le bddAbove_of_small ⟨_, hx.to_subtype_range⟩ le_rfl

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
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✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
this✝⁴ : Nontrivial S
this✝³ : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this✝² : Algebra.IsAlgebraic (↥Sy) A
x✝ : Algebra ↥Rxy ↥Sy := (Subalgebra.inclusion ⋯).toAlgebra
this✝¹ : IsScalarTower (↥Rxy) (↥Sy) A
this✝ : IsScalarTower ↥Rx ↥Rxy ↥Sy
this : Algebra.IsAlgebraic ↥Rxy ↥Sy
⊢ Algebra.IsAlgebraic (↥Rxy) A

Tactic:
exact .trans _ Sy _

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
hx : IsTranscendenceBasis R x
⊢ ¬IsEmpty ι ↔ Algebra.Transcendental R A

Tactic:
Algebra.transcendental_iff_not_isAlgebraic,

Goal state after:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
⊢ ¬IsEmpty ι ↔ ¬Algebra.IsAlgebraic R A
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inr.inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝³ : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝² : Nontrivial S
this✝¹ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this✝ : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
hi' : v i ∉ v '' s
this : InjOn v (insert i s)
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

Tactic:
← isTranscendenceBasis_subtype_range
    (by exact injOn_iff_injective.1 (this.mono sdiff_subset)),

Goal state after:
case inr.inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝³ : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝² : Nontrivial S
this✝¹ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this✝ : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
hi' : v i ∉ v '' s
this : InjOn v (insert i s)
⊢ IsTranscendenceBasis R Subtype.val
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 : 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

Tactic:
refine ⟨V, V, ⟨V_in, V_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 : Set G
V_in : V ∈ B
hV : V * V ⊆ U
⊢ ∀ (a b : G), a ∈ V → b ∈ V → a * b ∈ 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 : Set R
U_in : U ∈ B'
V : Set R
V_in : V ∈ B
hV : V * V ⊆ U
⊢ ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U

Tactic:
refine ⟨V, V, ⟨V_in, V_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 : Set R
V_in : V ∈ B
hV : V * V ⊆ U
⊢ ∀ (a b : R), a ∈ V → b ∈ V → a * b ∈ U
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
L : IntermediateField F E
x : E
h : finSepDegree F ↥L ∣ finrank F ↥L
M : IntermediateField (↥L) E := (↥L)⟮x⟯
hdvd : finSepDegree F ↥M ∣ finrank F ↥L * finrank ↥L ↥M
⊢ finSepDegree F ↥(IntermediateField.restrictScalars F M) ∣ finrank F ↥(IntermediateField.restrictScalars F M)

Tactic:
Module.finrank_mul_finrank F L M

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
M : IntermediateField (↥L) E := (↥L)⟮x⟯
hdvd : finSepDegree F ↥M ∣ finrank F ↥M
⊢ finSepDegree F ↥(IntermediateField.restrictScalars F M) ∣ finrank F ↥(IntermediateField.restrictScalars F M)
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: 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
a✝ b✝ : G
ha : a✝ ∈ ⋃ n, V ^ (n + 1)
hb : b✝ ∈ ⋃ n, V ^ (n + 1)
k : ℕ
hk : a✝ ∈ V ^ (k + 1)
l : ℕ
hl : b✝ ∈ V ^ (l + 1)
⊢ a✝ * b✝ ∈ ⋃ n, V ^ (n + 1)

Tactic:
apply mem_iUnion.mpr

Goal state after:
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
a✝ b✝ : G
ha : a✝ ∈ ⋃ n, V ^ (n + 1)
hb : b✝ ∈ ⋃ n, V ^ (n + 1)
k : ℕ
hk : a✝ ∈ V ^ (k + 1)
l : ℕ
hl : b✝ ∈ V ^ (l + 1)
⊢ ∃ i, a✝ * b✝ ∈ V ^ (i + 1)
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: 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
⊢ 1 ∈ ⋃ n, V ^ (n + 1)

Tactic:
apply mem_iUnion.mpr

Goal state after:
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
⊢ ∃ i, 1 ∈ V ^ (i + 1)
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: 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
x✝ : G
ha : x✝ ∈ ⋃ n, V ^ (n + 1)
k : ℕ
hk : x✝ ∈ V ^ (k + 1)
⊢ x✝⁻¹ ∈ ⋃ n, V ^ (n + 1)

Tactic:
apply mem_iUnion.mpr

Goal state after:
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
x✝ : G
ha : x✝ ∈ ⋃ n, V ^ (n + 1)
k : ℕ
hk : x✝ ∈ V ^ (k + 1)
⊢ ∃ i, x✝⁻¹ ∈ V ^ (i + 1)
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 : Type v
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree F ↥L = finrank F ↥L
M : IntermediateField (↥L) E := (↥L)⟮x⟯
heq : finSepDegree F ↥M = finrank F ↥L * finrank ↥L ↥M
⊢ finSepDegree F ↥(IntermediateField.restrictScalars F M) = finrank F ↥(IntermediateField.restrictScalars F M)

Tactic:
Module.finrank_mul_finrank F L M

Goal state after:
F : Type u
E✝ : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E✝
inst✝³ : Algebra F E✝
E : Type v
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree F ↥L = finrank F ↥L
M : IntermediateField (↥L) E := (↥L)⟮x⟯
heq : finSepDegree F ↥M = finrank F ↥M
⊢ finSepDegree F ↥(IntermediateField.restrictScalars F M) = finrank F ↥(IntermediateField.restrictScalars F M)
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
E : IntermediateField K L
inst✝ : FiniteDimensional K ↥E
⊢ IsOpen ↑E.fixingSubgroup

Tactic:
have h_basis : E.fixingSubgroup.carrier ∈ galGroupBasis K L :=
    ⟨E.fixingSubgroup, ⟨E, ‹_›, rfl⟩, rfl⟩

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
inst✝ : FiniteDimensional K ↥E
h_basis : E.fixingSubgroup.carrier ∈ galGroupBasis K L
⊢ IsOpen ↑E.fixingSubgroup
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝ : Field F
⊢ PerfectField F ↔ ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits

Tactic:
refine ⟨fun ⟨h⟩ f hf ↦ ?_, fun h ↦ ?_⟩
  · 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
  obtain ⟨p, _⟩ := ExpChar.exists F
  have := PerfectRing.ofSurjective F p fun x ↦ by
    obtain ⟨y, hy⟩ := Splits.exists_eval_eq_zero
      (h _ (pow_one p ▸ natSepDegree_X_pow_char_pow_sub_C p 1 x))
      ((degree_X_pow_sub_C (expChar_pos F p) x).symm ▸ Nat.cast_pos.2 (expChar_pos F p)).ne'
    exact ⟨y, by rwa [eval_sub, eval_X_pow, eval_C, sub_eq_zero] at hy⟩
  exact PerfectRing.toPerfectField F p

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
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H :
  Polynomial.map (algebraMap R K) p =
    Polynomial.map (algebraMap R K) a' * (C a.leadingCoeff * (C b.leadingCoeff * Polynomial.map (algebraMap R K) b'))
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit b

Tactic:
← mul_assoc (C a.leadingCoeff),

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ₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H :
  Polynomial.map (algebraMap R K) p =
    Polynomial.map (algebraMap R K) a' * (C a.leadingCoeff * C b.leadingCoeff * Polynomial.map (algebraMap R K) b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit b
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
inst✝ : Nontrivial S
e : minpolyDiv R x = 0
this : 0 = map (algebraMap R S) (minpoly R x)
⊢ False

Tactic:
exact ((minpoly.monic hx).map (algebraMap R S)).ne_zero this.symm

Goal state after:
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
h : x ∈ ↑(lift (fixedField (Subgroup.map (restrictNormalHom ↥L) H)))
⊢ x ∈ ↑(fixedField H ⊓ L)

Tactic:
have xL := lift_le _ 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
h : x ∈ ↑(lift (fixedField (Subgroup.map (restrictNormalHom ↥L) H)))
xL : x ∈ L
⊢ x ∈ ↑(fixedField H ⊓ L)
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case e'_3
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
hInt : IsIntegral R s
q : R[X]
hMul : p = minpoly R s * q
⊢ (minpoly R s).degree + q.degree = p.degree

Tactic:
rw [hMul, degree_mul]

Goal state after: