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

Goal state before:
pp: α : Type u_1
E : Set α
hE : E.Finite
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
I : Set α
hI : Indep I
⊢ I.encard ≤ ↑E.ncard

Tactic:
hE.cast_ncard_eq

Goal state after:
α : Type u_1
E : Set α
hE : E.Finite
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
I : Set α
hI : Indep I
⊢ I.encard ≤ E.encard
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : M.E ∩ B' ∩ (B ∪ X)ᶜ = ∅ ∧ e ∉ B'
⊢ False

Tactic:
inter_eq_self_of_subset_right hB'.subset_ground,

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ∩ (B ∪ X)ᶜ = ∅ ∧ e ∉ B'
⊢ False
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
hM : ∃ M, E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I
⊢ ∃ M, E = M.E ∧ M.Indep = Indep

Tactic:
obtain ⟨M, rfl, h⟩ := hM; refine ⟨_, rfl, funext (by simp [h])⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I X : Set α
hIX : M.IsBasis I X
⊢ (M.map f hf).IsBasis (f '' I) (f '' X)

Tactic:
exact hIX.map hf

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ (M ↾ R).fundCircuit e I = M.fundCircuit e I

Tactic:
fundCircuit,

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ (M ↾ R).closure {e} ⊆ (M ↾ R).closure J}) =
    insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})
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:
by rw [h, loops]; simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsNonloop e ↔ e ∉ M.loops

Tactic:
rw [isNonloop_iff, isLoop_iff, and_iff_left he]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
he : e ∉ C
⊢ M.closure (C \ {e}) = M.closure C

Tactic:
rw [sdiff_singleton_eq_self he]

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
⊢ (¬M.Indep {e, f} ∧ {f} ⊆ M.E) ∧ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})

Tactic:
singleton_subset_iff,

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
⊢ (¬M.Indep {e, f} ∧ f ∈ M.E) ∧ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hf : M.IsNonloop f
hne : e ≠ f
⊢ ((¬M.Indep {e, f} ∧ e ∈ M.E ∧ {f} ⊆ M.E) ∧ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})) ↔ ¬M.Indep {e, f}

Tactic:
singleton_subset_iff,

Goal state after:
case inr
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hf : M.IsNonloop f
hne : e ≠ f
⊢ ((¬M.Indep {e, f} ∧ e ∈ M.E ∧ f ∈ M.E) ∧ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})) ↔ ¬M.Indep {e, f}
Module: Mathlib.Combinatorics.Matroid.Loop

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

Tactic:
singleton_subset_iff,

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X Y : Set α
⊢ M.closure (⋃ b, bif b then X else Y) = M.closure (M.closure X ∪ M.closure Y)

Tactic:
← closure_iUnion_closure_eq_closure_iUnion,

Goal state after:
α : Type u_2
M : Matroid α
X Y : Set α
⊢ M.closure (⋃ i, M.closure (bif i then X else Y)) = M.closure (M.closure X ∪ M.closure Y)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
inst✝ : M.Loopless
hI : I.Subsingleton
hIE : I ⊆ M.E
⊢ M.Indep I

Tactic:
by
  obtain rfl | ⟨x, rfl⟩ := hI.eq_empty_or_singleton
  · simp
  simpa using M.isNonloop_of_loopless

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

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

Tactic:
simp [hI, heI]

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
hf : InjOn f M.E
J : Set β
I X : Set α
hIX : M.IsBasis I X
hJ : (M.map f hf).IsBasis J (f '' X)
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ #↑(f '' I \ J) = #↑(J \ f '' I)

Tactic:
obtain ⟨J, X', hJX, rfl, h'⟩ := map_isBasis_iff'.1 hJ

Goal state after:
α : Type u
β : Type v
f : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid α
inst✝ : M.InvariantCardinalRank
hf : InjOn f M.E
I X : Set α
hIX : M.IsBasis I X
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
J X' : Set α
hJX : M.IsBasis J X'
h' : f '' X = f '' X'
hJ : (M.map f hf).IsBasis (f '' J) (f '' X)
⊢ #↑(f '' I \ f '' J) = #↑(f '' J \ f '' I)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.fundCocircuit e B ∩ I ⊆ {e} ∧ {e} ⊆ M.fundCocircuit e B ∧ {e} ⊆ I

Tactic:
singleton_subset_iff,

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.fundCocircuit e B ∩ I ⊆ {e} ∧ e ∈ M.fundCocircuit e B ∧ {e} ⊆ I
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.fundCocircuit e B ∩ I ⊆ {e} ∧ {e} ⊆ I

Tactic:
singleton_subset_iff,

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.fundCocircuit e B ∩ I ⊆ {e} ∧ e ∈ I
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
use fun h e heI he ↦ ((h.closure_inter_eq_self_of_subset sdiff_subset).subset ⟨he, heI⟩).2 rfl

Goal state after:
case mpr
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
⊢ (∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})) → M.Indep I
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i ↦ (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i ↦ x ↑i
i : ι
hi : i ∉ t
a✝ : ι
h : a✝ ∈ t
⊢ {X a✝} ⊆ X '' t

Tactic:
singleton_subset_iff,

Goal state after:
ι : Type u_1
R : Type u_3
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i ↦ (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i ↦ x ↑i
i : ι
hi : i ∉ t
a✝ : ι
h : a✝ ∈ t
⊢ X a✝ ∈ X '' t
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
⊢ AlgebraicIndependent R fun i ↦ (Polynomial.aeval (X i)) (f i)

Tactic:
by
  set x := fun i ↦ Polynomial.aeval (X i : MvPolynomial ι R) (f i)
  refine algebraicIndependent_of_finite_type' (C_injective _ _) fun t _ _ i hi ↦ ?_
  have hle : adjoin R (x '' t) ≤ supported R t := by
    rw [Algebra.adjoin_le_iff, Set.image_subset_iff]
    intro _ h
    rw [Set.mem_preimage]
    refine Algebra.adjoin_mono ?_ (Polynomial.aeval_mem_adjoin_singleton R _)
    simp_rw [singleton_subset_iff, Set.mem_image_of_mem _ h]
  exact (transcendental_supported_polynomial_aeval_X R hi (hf i)).of_tower_top_of_subalgebra_le hle

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
⊢ ∃ s, IsTranscendenceBasis R Subtype.val

Tactic:
simpa using exists_isTranscendenceBasis_superset
    ((algebraicIndependent_empty_iff R A).mpr (FaithfulSMul.algebraMap_injective R A))

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

Goal state before:
pp: 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✝¹ : IsDomain S
inst✝ : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
⊢ Algebra.IsAlgebraic S A ↔ ∀ (i : ι), IsAlgebraic S (v i)

Tactic:
refine ⟨fun _ i ↦ Algebra.IsAlgebraic.isAlgebraic (v i), fun H ↦ ?_⟩
  let Rv := adjoin R (range v)
  let Sv := adjoin S (range v)
  have : Algebra.IsAlgebraic S Sv := by
    simpa [Sv, ← Subalgebra.isAlgebraic_iff, isAlgebraic_adjoin_iff]
  have le : Rv ≤ Sv.restrictScalars R := by
    rw [Subalgebra.restrictScalars_adjoin]; exact le_sup_right
  let : Algebra Rv Sv := (Subalgebra.inclusion le).toAlgebra
  have : IsScalarTower Rv Sv A := .of_algebraMap_eq fun x ↦ rfl
  have := (algebraMap R S).domain_nontrivial
  have := hv.isAlgebraic
  have : Algebra.IsAlgebraic Sv A := .extendScalars (Subalgebra.inclusion_injective le)
  exact .trans _ Sv _

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
⊢ IsTranscendenceBasis R (Sum.elim y (⇑(algebraMap S A) ∘ x))

Tactic:
(hx.1.sumElim_comp hy.1).isTranscendenceBasis_iff_isAlgebraic

Goal state after:
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
⊢ Algebra.IsAlgebraic (↥(adjoin R (range (Sum.elim y (⇑(algebraMap S A) ∘ x))))) A
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
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
h✝ : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R B)) A
⊢ Algebra.IsAlgebraic (↥(adjoin R I)) A

Tactic:
refine ⟨fun a ↦ (B_base.1 a).adjoin_of_forall_isAlgebraic fun x hx ↦ ?_⟩

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 B)) A
a x : A
hx : x ∈ B \ I
⊢ IsAlgebraic (↥(adjoin R I)) x
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✝ : NoZeroDivisors A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
ht : Algebra.IsAlgebraic (↥(adjoin R t)) A
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ IsTranscendenceBasis R Subtype.val

Tactic:
have := ht.nontrivial
  have := Subtype.val_injective (p := (· ∈ adjoin R t)).nontrivial
  have := (isDomain_iff_noZeroDivisors_and_nontrivial A).mpr ⟨inferInstance, inferInstance⟩
  have := (faithfulSMul_iff_algebraMap_injective R A).mpr hs.algebraMap_injective
  rw [← matroid_spanning_iff] at ht
  rw [← matroid_indep_iff] at hs
  have ⟨B, base, hsB, hBt⟩ := hs.exists_isBase_subset_spanning ht hst
  exact ⟨B, hsB, hBt, base⟩

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

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ B.filter.HasBasis (fun V ↦ V ∈ B) id

Tactic:
exact B.toFilterBasis.hasBasis

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 v
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
this✝ : Algebra ↥(separableClosure F K) ↥(restrictScalars F (separableClosure E K)) := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥(separableClosure F K)) (↥(restrictScalars F (separableClosure E K))) K
⊢ insepDegree E K ≤ insepDegree F K

Tactic:
exact Module.rank_top_le_rank_of_isScalarTower
    (separableClosure F K) ((separableClosure E K).restrictScalars F) K

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
inst✝ : Algebra.IsSeparable F E
⊢ sepDegree F E = Module.rank F E

Tactic:
by
  rw [sepDegree, (separableClosure.eq_top_iff F E).2 ‹_›, IntermediateField.rank_top']

Goal state after:
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)
⊢ a✝ * b✝ ∈ ⋃ n, V ^ (n + 1)

Tactic:
by
      rcases mem_iUnion.mp ha with ⟨k, hk⟩
      rcases mem_iUnion.mp hb with ⟨l, hl⟩
      apply mem_iUnion.mpr
      use k + 1 + l
      rw [add_assoc, pow_add]
      exact Set.mul_mem_mul hk hl

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

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

Tactic:
exact (Set.mul_subset_mul_right ih).trans hV.mul

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

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

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup

Goal state before:
pp: G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : SeparatelyContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h : T1Space (G ⧸ H)
⊢ IsOpen ↑H

Tactic:
← QuotientGroup.discreteTopology_iff

Goal state after:
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : SeparatelyContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h : T1Space (G ⧸ H)
⊢ DiscreteTopology (G ⧸ H)
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: case h.left
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a ↦ σ • a = a
f : Gal(K/k)
hf : f ∈ σ • ↑(adjoin k {y}).fixingSubgroup
g : Gal(K/k)
hg : g ∈ ↑(adjoin k {y}).fixingSubgroup
eq : σ • g = f
⊢ f ∈ (↑L.fixingSubgroup)ᶜ

Tactic:
simp only [Set.mem_compl_iff, SetLike.mem_coe, ← eq]

Goal state after:
case h.left
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a ↦ σ • a = a
f : Gal(K/k)
hf : f ∈ σ • ↑(adjoin k {y}).fixingSubgroup
g : Gal(K/k)
hg : g ∈ ↑(adjoin k {y}).fixingSubgroup
eq : σ • g = f
⊢ σ • g ∉ L.fixingSubgroup
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ IsUnit (map φ a) → IsUnit a

Tactic:
apply ((isPrimitive_of_dvd hf _).isUnit_iff_isUnit_map_of_injective hinj).mpr

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ a ∣ f
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ IsUnit (map φ b) → IsUnit b

Tactic:
apply ((isPrimitive_of_dvd hf _).isUnit_iff_isUnit_map_of_injective hinj).mpr

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ b ∣ f
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
⊢ L ≤ IntermediateField.fixedField L.fixingSubgroup

Tactic:
· exact (IntermediateField.le_iff_le L.fixingSubgroup L).mpr le_rfl

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

Goal state before:
pp: case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H✝ : (minpolyDiv R x).coeff i ∉ R[x]
j : ℕ
IH : (minpolyDiv R x).coeff (i + j) ∉ R[x]
H : (minpolyDiv R x).coeff (i + (j + 1)) ∈ R[x]
⊢ (minpolyDiv R x).coeff (i + j) ∈ R[x]

Tactic:
rw [coeff_minpolyDiv]

Goal state after:
case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H✝ : (minpolyDiv R x).coeff i ∉ R[x]
j : ℕ
IH : (minpolyDiv R x).coeff (i + j) ∉ R[x]
H : (minpolyDiv R x).coeff (i + (j + 1)) ∈ R[x]
⊢ (algebraMap R S) ((minpoly R x).coeff (i + j + 1)) + (minpolyDiv R x).coeff (i + j + 1) * x ∈ R[x]
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_2
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
x✝ : C p.leadingCoeff ∣ p
q : R[X]
hMul : p = C p.leadingCoeff * q
⊢ minpoly R s ≠ 0

Tactic:
convert! right_ne_zero_of_mul <| hMul ▸ h₀

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
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
x✝ : C p.leadingCoeff ∣ p
q : R[X]
hMul : p = C p.leadingCoeff * q
⊢ minpoly R s = q
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i) * (R ∙ x) ≤
    Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))

Tactic:
Submodule.span_mul_span,

Goal state after:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i * {x}) ≤ Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_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
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (Polynomial.aeval ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s))
      ((minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r)) =
    0

pp: case refine_4
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
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r) ∣
    minpoly K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)

Tactic:
· exact scaleRoots_aeval_eq_zero (minpoly.aeval _ _)

Goal state after:
case refine_4
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
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r) ∣
    minpoly K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsSeparable k K
x : K
hq : (minpoly k x).leadingCoeff = 1
hsep : IsSeparable k x
h : (minpoly k x).degree = 1
this : x = -(algebraMap k K) ((minpoly k x).coeff 0)
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x

Tactic:
exact (map_neg (algebraMap k K) ((minpoly k x).coeff 0)).symm ▸ this.symm

Goal state after: