mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
s : Finset E := (sf.bind fun α' ↦ Multiset.map (fun β' ↦ -(α' - α) / (β' - β)) sg).toFinset
s' : Finset F := s.preimage ⇑ϕ ⋯
c : F
hc : ¬∃ a ∈ sf, ϕ c ∈ Multiset.map (fun β' ↦ -(a - α) / (β' - β)) sg
⊢ ∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c

Tactic:
Multiset.mem_map

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
s : Finset E := (sf.bind fun α' ↦ Multiset.map (fun β' ↦ -(α' - α) / (β' - β)) sg).toFinset
s' : Finset F := s.preimage ⇑ϕ ⋯
c : F
hc : ¬∃ a ∈ sf, ∃ a_1 ∈ sg, -(a - α) / (a_1 - β) = ϕ c
⊢ ∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M₁ M₂ : Matroid α
h : M₁ = M₂
⊢ M₁.E = M₂.E ∧ ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)

Tactic:
subst h; simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊆ Y
hYX : Y ⊆ X
⊢ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ Y → I = J

Tactic:
exact fun J hJ hIJ hJY ↦ hI.eq_of_subset_indep hJ hIJ (hJY.trans hYX)

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R P
inst✝⁴ : Module R Q
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
x : A ⊗[R] ↥(submoduleAlgebra e)
⊢ ∀ (x : A) (y : ↥(submoduleAlgebra e)),
    (LinearMap.mul'' R A ∘ₗ (AlgebraTensorModule.lTensor A A) (submoduleAlgebra e).subtype) (x ⊗ₜ[R] y) =
      (AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e) (x ⊗ₜ[R] y)

Tactic:
intro a

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R P
inst✝⁴ : Module R Q
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
x : A ⊗[R] ↥(submoduleAlgebra e)
a : A
⊢ ∀ (y : ↥(submoduleAlgebra e)),
    (LinearMap.mul'' R A ∘ₗ (AlgebraTensorModule.lTensor A A) (submoduleAlgebra e).subtype) (a ⊗ₜ[R] y) =
      (AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e) (a ⊗ₜ[R] y)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B X : Set α
hX : X ⊆ M.E
hB : M.IsBase B
hBX : B ⊆ X
⊢ ∀ (J : Set α), M.Indep J → B ⊆ J → J ⊆ X → B = J

Tactic:
exact fun J hJ hBJ _ ↦ hB.eq_of_subset_indep hJ hBJ

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
⊢ Disjoint X (I' \ I)

Tactic:
disjoint_iff_forall_ne

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
⊢ ∀ ⦃a : α⦄, a ∈ X → ∀ ⦃b : α⦄, b ∈ I' \ I → a ≠ b
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I E : Set α
⊢ (uniqueBaseOn I E)✶ = uniqueBaseOn (E \ I) E

Tactic:
rw [← uniqueBaseOn_inter_ground_eq]

Goal state after:
α : Type u_1
I E : Set α
⊢ (uniqueBaseOn (I ∩ E) E)✶ = uniqueBaseOn (E \ I) E
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn I E).RankFinite

Tactic:
rw [← uniqueBaseOn_inter_ground_eq]

Goal state after:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).RankFinite
Module: Mathlib.Combinatorics.Matroid.Rank.Finite

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ M.IsRkFinite X ↔ ∃ I, M.IsBasis I X ∧ I.Finite

Tactic:
simp_rw [isRkFinite_iff_exists_isBasis', M.isBasis'_iff_isBasis hX]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M : Matroid α
N : Matroid β
f : ↑(emptyOn α).E ↪ β
⊢ ∃ M, range ⇑f = M.E ∧ ∀ (I : Set β), M.Indep I ↔ (emptyOn α).Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

Tactic:
refine ⟨emptyOn β, ?_⟩
      simp only [emptyOn_ground] at f
      simp [range_eq_empty f, subset_empty_iff]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ ∀ ⦃t : Set α⦄, t ⊂ C → M.Indep t

Tactic:
exact fun ⦃t⦄ a ↦ ssubset_indep hC a

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
I X : Set β
hf : InjOn f M.E
⊢ (M.map f hf).IsBasis I X ↔ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
  · obtain ⟨I, hI, rfl⟩ := subset_image_iff.1 h.indep.subset_ground
    obtain ⟨X, hX, rfl⟩ := subset_image_iff.1 h.subset_ground
    rw [map_isBasis_iff _ _ hI hX] at h
    exact ⟨I, X, h, rfl, rfl⟩
  rintro ⟨I, X, hIX, rfl, rfl⟩
  exact hIX.map hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
⊢ (M.map f hf)✶ = M✶.map f hf

Tactic:
by
  apply ext_isBase (by simp)
  simp only [dual_ground, map_ground, subset_image_iff, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, dual_isBase_iff']
  intro B hB
  simp_rw [← hf.image_sdiff_subset hB, map_image_isBase_iff sdiff_subset,
    map_image_isBase_iff (show B ⊆ M✶.E from hB), dual_isBase_iff hB, and_iff_left_iff_imp]
  exact fun _ ↦ ⟨B, hB, rfl⟩

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

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk ((X ∪ M.E) ∩ M.E) = M.eRank
Module: Mathlib.Combinatorics.Matroid.Loop

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

Tactic:
← closure_empty_eq_ground_iff,

Goal state after:
α : Type u_1
M : Matroid α
E : Set α
h : M.loops = E
h' : M.E = E
⊢ M.closure ∅ = M.E
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
← eRk_inter_ground,

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

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

Tactic:
← closure_empty_eq_ground_iff,

Goal state after:
α : Type u_1
M : Matroid α
E : Set α
x✝ : M.loops = E ∧ M.E = E
h : M.loops = E
h' : M.E = E
⊢ M.closure ∅ = M.E
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.E ⊆ X
⊢ M.eRk X = M.eRank

Tactic:
← eRk_inter_ground,

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

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

Tactic:
← eRk_inter_ground,

Goal state after:
α : Type u_1
X Y : Set α
M : Matroid α
hXY : Disjoint X Y
⊢ M.eRk ((M.E \ X ∪ Y) ∩ M.E) = M.eRk (M.E \ X)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.eRk univ = M.eRank

Tactic:
← eRk_inter_ground,

Goal state after:
α : Type u_1
M : Matroid α
⊢ M.eRk (univ ∩ M.E) = M.eRank
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
R X I : Set α
hI : M.IsBasis I (X ∩ R ∩ M.E) ∧ X ∩ R ⊆ R
⊢ I.encard = M.eRk (X ∩ R)

Tactic:
← eRk_inter_ground,

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : n ≤ M.eRk X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n

pp: case refine_2
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.encard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hIc : I.encard = n
⊢ n ≤ M.eRk X

Tactic:
· obtain ⟨J, hJ⟩ := M.exists_isBasis' X
    rw [← hJ.encard_eq_eRk] at h
    obtain ⟨I, hIJ, rfl⟩ := exists_subset_encard_eq h
    exact ⟨_, hIJ.trans hJ.subset, hJ.indep.subset hIJ, rfl⟩

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.encard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hIc : I.encard = n
⊢ n ≤ M.eRk X
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
⊢ M.eRk X = 0 ↔ X ∩ M.E ⊆ M.loops

Tactic:
← eRk_inter_ground,

Goal state after:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
⊢ M.eRk (X ∩ M.E) = 0 ↔ X ∩ M.E ⊆ M.loops
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
← eRk_inter_ground,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRank ≤ M.eRk ((X ∪ M.E \ X) ∩ M.E)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_5
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ i, C i \ {x i}
hC' : M.IsCircuit C'
hzC' : z ∈ C'
i : ι
⊢ Disjoint (C i \ {x i}) (range x)

Tactic:
disjoint_iff_forall_ne

Goal state after:
case refine_5
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ i, C i \ {x i}
hC' : M.IsCircuit C'
hzC' : z ∈ C'
i : ι
⊢ ∀ ⦃a : α⦄, a ∈ C i \ {x i} → ∀ ⦃b : α⦄, b ∈ range x → a ≠ b
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
← closure_closure_union_closure_eq_closure_union,

Goal state after:
α : Type u_2
M : Matroid α
X Y : Set α
⊢ M.closure (M.closure X ∪ M.closure (M.closure Y)) = M.closure (X ∪ Y)
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
← closure_closure_union_closure_eq_closure_union,

Goal state after:
α : Type u_2
M : Matroid α
X Y : Set α
⊢ M.closure (M.closure (M.closure X) ∪ M.closure Y) = M.closure (X ∪ Y)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ Disjoint K (M.closure (X \ K))

Tactic:
disjoint_iff_forall_ne

Goal state after:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ ∀ ⦃a : α⦄, a ∈ K → ∀ ⦃b : α⦄, b ∈ M.closure (X \ K) → a ≠ b
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ M.closure I = M.closure X

Tactic:
refine subset_antisymm (M.closure_subset_closure h.subset) ?_

Goal state after:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ M.closure X ⊆ M.closure I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
⊢ ¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (¬M.Indep (insert x I) ∨ x ∈ I)

Tactic:
have := hI.subset_ground

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
this : I ⊆ M.E
⊢ ¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (¬M.Indep (insert x I) ∨ x ∈ I)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case a
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
⊢ I ⊆ M.closure (insert f I \ {e})

Tactic:
intro a

Goal state after:
case a
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
a : α
⊢ a ∈ I → a ∈ M.closure (insert f I \ {e})
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S I : Set α
hI : M.Indep I
hS : M.Spanning S
hIS : I ⊆ S
⊢ ∃ B, M.IsBase B ∧ I ⊆ B ∧ B ⊆ S

Tactic:
by
  obtain ⟨B, hB⟩ := hI.subset_isBasis_of_subset hIS
  exact ⟨B, hB.1.isBase_of_spanning hS, hB.2, hB.1.subset⟩

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

Goal state before:
pp: α : Type u_2
M : Matroid α
B : Set α
x✝ : M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
h : M.Spanning B
h' : ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
⊢ M.IsBase B

Tactic:
obtain ⟨B', hB', hBB'⟩ := h.exists_isBase_subset

Goal state after:
α : Type u_2
M : Matroid α
B : Set α
x✝ : M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
h : M.Spanning B
h' : ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
B' : Set α
hB' : M.IsBase B'
hBB' : B' ⊆ B
⊢ M.IsBase B
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
m₁ m₂ : M
⊢ fixedBy α m₁ ∩ fixedBy α m₂ ⊆ fixedBy α (m₁ * m₂)

Tactic:
intro a

Goal state after:
α : Type u_1
M : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
m₁ m₂ : M
a : α
⊢ a ∈ fixedBy α m₁ ∩ fixedBy α m₂ → a ∈ fixedBy α (m₁ * m₂)
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
⊢ ∀ (x_1 : A), IsAlgebraic (↥(adjoin R (range x))) x_1

Tactic:
intro a

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
a : A
⊢ IsAlgebraic (↥(adjoin R (range x))) a
Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
⊢ orbit (↥(fixingSubgroup M sᶜ)) a ⊆ s

Tactic:
intro b b_in_orbit
  let ⟨⟨g, g_fixing⟩, g_eq⟩ := MulAction.mem_orbit_iff.mp b_in_orbit
  rw [Submonoid.mk_smul] at g_eq
  rw [mem_fixingSubgroup_compl_iff_movedBy_subset] at g_fixing
  rwa [← g_eq, smul_mem_of_set_mem_fixedBy (set_mem_fixedBy_of_movedBy_subset g_fixing)]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
h : Irreducible f
q : ℕ
h✝ : ExpChar F q
hf : HasSeparableContraction q f
⊢ f.natSepDegree ∣ f.natDegree

Tactic:
hf.natSepDegree_eq

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
h : Irreducible f
q : ℕ
h✝ : ExpChar F q
hf : HasSeparableContraction q f
⊢ hf.degree ∣ f.natDegree
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
h : Irreducible f
q : ℕ
h✝ : ExpChar F q
hf : HasSeparableContraction q f
⊢ f.natSepDegree ∣ f.natDegree

Tactic:
rw [hf.natSepDegree_eq]

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
h : Irreducible f
q : ℕ
h✝ : ExpChar F q
hf : HasSeparableContraction q f
⊢ hf.degree ∣ f.natDegree
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hpure
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ ∀ (a : G), ∀ i ∈ B.toFilterBasis, a ∈ (fun y ↦ a * y) '' id i

Tactic:
intro a

Goal state after:
case hpure
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
⊢ ∀ i ∈ B.toFilterBasis, a ∈ (fun y ↦ a * y) '' id i
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hopen
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ ∀ (a : G),
    ∀ i ∈ B.toFilterBasis,
      ∀ᶠ (x : G) in map (fun y ↦ a * y) B.filter, (fun y ↦ a * y) '' id i ∈ map (fun y ↦ x * y) B.filter

Tactic:
intro a

Goal state after:
case hopen
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
⊢ ∀ i ∈ B.toFilterBasis,
    ∀ᶠ (x : G) in map (fun y ↦ a * y) B.filter, (fun y ↦ a * y) '' id i ∈ map (fun y ↦ x * y) B.filter
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_1
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
U : 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

Tactic:
intro a

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 : G
⊢ ∀ (b : G), a ∈ V → b ∈ V → a * b ∈ U
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case zero
F : Type u
inst✝² : Field F
f : F[X]
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
n : ℕ
y : F
inst✝¹ : CharZero F
inst✝ : ExpChar F 1
hf : f = X ^ 1 ^ n - C y
⊢ ∃ n y, (n = 0 ∨ y ∉ (frobenius F 1).range) ∧ f = X ^ 1 ^ n - C y

Tactic:
| zero =>

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
⊢ ∃ m n y, m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m

pp: case refine_2
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm✝ : f.Monic
x✝ : ∃ m n y, m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m
m n : ℕ
y : F
hm : m ≠ 0
h : f = (X ^ q ^ n - C y) ^ m
⊢ f.natSepDegree = 1

Tactic:
· obtain ⟨m, n, y, hm, -, h⟩ := hm.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one q h
    exact ⟨m, n, y, hm, h⟩

Goal state after:
case refine_2
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm✝ : f.Monic
x✝ : ∃ m n y, m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m
m n : ℕ
y : F
hm : m ≠ 0
h : f = (X ^ q ^ n - C y) ^ m
⊢ f.natSepDegree = 1
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
⊢ ∀ (a b : R), a ∈ V → b ∈ V → a * b ∈ U

Tactic:
intro a

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 : R
⊢ ∀ (b : R), a ∈ V → b ∈ V → a * b ∈ U
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
x : E
⊢ i x ∈ separableClosure F K ↔ x ∈ separableClosure F E

Tactic:
simp_rw [mem_separableClosure_iff, IsSeparable, minpoly.algHom_eq i i.injective]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

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

Tactic:
obtain ⟨n, y, h⟩ := (natSepDegree_eq_one_iff_eq_X_pow_sub_C q).1 h

Goal state after:
case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
h✝ : (minpoly F x).natSepDegree = 1
n : ℕ
y : F
h : minpoly F x = X ^ q ^ n - C y
⊢ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
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
inst✝ : Module.Finite F K
⊢ finInsepDegree E K ≤ finInsepDegree F K

Tactic:
let := (IntermediateField.inclusion (separableClosure.le_restrictScalars F E K)).toAlgebra
  have : IsScalarTower (separableClosure F K) ((separableClosure E K).restrictScalars F) K :=
    .of_algebraMap_eq' rfl
  exact Module.finrank_top_le_finrank_of_isScalarTower
    (separableClosure F K) ((separableClosure E K).restrictScalars F) K

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

Goal state before:
pp: case zero
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))
⊢ W * V ^ (0 + 1) ⊆ W

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ¬IsIntegral R x
⊢ minpolyDiv R x = 0

Tactic:
delta minpolyDiv minpoly
  rw [dif_neg hx, Polynomial.map_zero, zero_divByMonic]

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
s : S
hs : IsIntegral R s
p : R[X]
hp : (Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x✝ : Algebra K L := FractionRing.liftAlgebra R L
this : map (algebraMap R K) (minpoly R s) ∣ map (algebraMap R K) (p %ₘ minpoly R s)
⊢ minpoly R s ∣ p

Tactic:
map_dvd_map (algebraMap R K) (IsFractionRing.injective R K) (minpoly.monic hs)

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
hs : IsIntegral R s
p : R[X]
hp : (Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x✝ : Algebra K L := FractionRing.liftAlgebra R L
this : minpoly R s ∣ p %ₘ minpoly R s
⊢ minpoly R s ∣ p
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case zero
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]
⊢ (minpolyDiv R x).coeff (i + 0) ∉ R[x]

Tactic:
| zero =>

Goal state after: