mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x ↦ x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j ↦ decidable_of_iff (↑j ∈ C₁) ⋯
⊢ ∀ (x : ↑C₀) (hx : x ∈ Subtype.val ⁻¹' C₁ ∩ Subtype.val ⁻¹' C₂),
    (comap { toFun := C₁.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₁) ⟨x, ⋯⟩ =
      (comap { toFun := C₂.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₂) ⟨x, ⋯⟩

Tactic:
rintro ⟨x, hx₀⟩ ⟨hx₁ : x ∈ C₁, hx₂ : x ∈ C₂⟩
      simpa using hf x ⟨hx₁, hx₂⟩

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case zero
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ a * b = b * a

Tactic:
refine (mem_bot.1 ?_).trans (mem_bot.1 ?_).symm

Goal state after:
case zero.refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ a * b ∈ ⊥

case zero.refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ b * a ∈ ⊥
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case inl
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
h : Normal F L
h✝ : IsEmpty (K →ₐ[F] L)
⊢ Normal F ↥⊥

Tactic:
exact Normal.of_algEquiv (botEquiv F L).symm

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
x : ↥(⨆ i, t i)
s : Finset ((i : ι) × ↥(t i))
hx : ↑x ∈ ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet K)
hF : Normal F ↥E
i : (i : ι) × ↥(t i)
x✝ : i ∈ s
⊢ ⇑(t i.fst).val '' (minpoly F i.snd).rootSet ↥(t i.fst) ⊆ ↑(t i.fst)

Tactic:
exact fun _ ⟨a, _, h⟩ => h ▸ a.2

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

Goal state before:
pp: case refine_1
F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
f : ↥(iInf t) →ₐ[F] ↥(t hι.some) := inclusion ⋯
⊢ Algebra.IsAlgebraic F ↥(⨅ i, t i)

Tactic:
exact Algebra.IsAlgebraic.of_injective f f.injective

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
x : ↥(⨅ i, t i)
i : ι
⊢ (Polynomial.map (algebraMap F ↥(t i)) (minpoly F x)).Splits

Tactic:
rw [← minpoly.algHom_eq (inclusion (iInf_le t i)) (inclusion (iInf_le t i)).injective]

Goal state after:
F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
x : ↥(⨅ i, t i)
i : ι
⊢ (Polynomial.map (algebraMap F ↥(t i)) (minpoly F ((inclusion ⋯) x))).Splits
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ M.Indep X ∨ M.Dep X

Tactic:
rw [Dep, and_iff_left hX]
  apply em

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
h : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → I = J
⊢ M.IsBase I

Tactic:
by
  rwa [isBase_iff_maximal_indep, maximal_subset_iff, and_iff_right hI]

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

Goal state before:
pp: α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
⊢ ∃ b ∈ B' \ B, Maximal M.Indep (insert b (B \ {e}))

Tactic:
by
    have hnotmax : ¬ Maximal M.Indep (B \ {e}) :=
      fun h ↦ h.not_prop_of_ssuperset (sdiff_singleton_ssubset.2 he.1) hB.prop
    obtain ⟨f, hf, hfB⟩ := M.indep_aug (M.indep_subset hB.prop sdiff_subset) hnotmax hB'
    replace hf := show f ∈ B' \ B by simpa [show f ≠ e by rintro rfl; exact he.2 hf.1] using hf
    refine ⟨f, hf, by_contra fun hnot ↦ ?_⟩
    obtain ⟨x, hxB, hind⟩ := M.indep_aug hfB hnot hB
    obtain ⟨-, rfl⟩ : _ ∧ x = e := by simpa [hxB.1] using hxB
    refine hB.not_prop_of_ssuperset ?_ hind
    rw [insert_comm, insert_sdiff_singleton, insert_eq_of_mem he.1]
    exact ssubset_insert hf.2

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

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

Tactic:
by_cases hI : I ⊆ M₁.E

Goal state after:
case pos
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I

case neg
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : ¬I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
x✝ : Set α
⊢ Indep x✝ ↔ ∃ B, IsBase B ∧ x✝ ⊆ B

Tactic:
by simp_rw [hI, hB, M.indep_iff]

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

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint (insert x I) B

Tactic:
obtain ⟨e, ⟨(heB'' : e ∉ _), heE⟩, heI⟩ := exists_of_ssubset hssu

Goal state after:
α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint (insert x I) B
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
⊢ (M ↾ I).E = I ∧ (M ↾ I).Indep I ↔ M.Indep I

Tactic:
and_iff_right M.restrict_ground_eq,

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
⊢ (M ↾ I).Indep I ↔ M.Indep I
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 : ¬(insert e (M.E \ B ∩ (M.E \ X)) ∩ B').Nonempty
⊢ False

Tactic:
rw [nonempty_iff_ne_empty, not_ne_iff, ← union_singleton, sdiff_inter_sdiff,
    union_inter_distrib_right, union_empty_iff, singleton_inter_eq_empty, sdiff_eq,
    inter_right_comm, inter_eq_self_of_subset_right hB'.subset_ground, ← sdiff_eq,
    sdiff_eq_empty] at hem

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.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
N : Matroid α
hI : M.IsBasis I X
hNM : N ≤r M
hX : X ⊆ N.E
⊢ N.IsBasis I X

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
R : Set α
hR : R ⊆ M.E
hX : X ⊆ (M ↾ R).E
⊢ (M ↾ R).IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
N : Matroid α
hI : N.IsBasis I X
hNM : N ≤r M
⊢ M.IsBasis I X

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM

Goal state after:
α : Type u_1
M : Matroid α
I X R : Set α
hR : R ⊆ M.E
hI : (M ↾ R).IsBasis I X
⊢ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
N : Matroid α
hI : N.IsBase I
hNM : N ≤r M
⊢ M.IsBasis I N.E

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM

Goal state after:
α : Type u_1
M : Matroid α
I R : Set α
hR : R ⊆ M.E
hI : (M ↾ R).IsBase I
⊢ M.IsBasis I (M ↾ R).E
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
N : Matroid α
hX : N.Dep X
hNM : N ≤r M
⊢ M.Dep X

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM

Goal state after:
α : Type u_1
M : Matroid α
X R : Set α
hR : R ⊆ M.E
hX : (M ↾ R).Dep X
⊢ M.Dep X
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hC : M.IsCircuit I
h : M.IsBasis I I
⊢ False

Tactic:
exact hC.dep.not_indep h.indep

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X I : Set α
hX : X ⊆ M.loops
⊢ M.IsBasis I X ↔ I = ∅

Tactic:
refine ⟨fun h ↦ ?_, by rintro rfl; simpa⟩

Goal state after:
α : Type u_1
M : Matroid α
X I : Set α
hX : X ⊆ M.loops
h : M.IsBasis I X
⊢ I = ∅
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M N : Matroid α
e : α
hNM : N ≤r M
⊢ N.IsLoop e ↔ e ∈ N.E ∧ M.IsLoop e

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM

Goal state after:
α : Type u_1
M : Matroid α
e : α
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).IsLoop e ↔ e ∈ (M ↾ R).E ∧ M.IsLoop e
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
rw [inter_comm, eRk_inter_ground]

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

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

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨I, hIX, hI, hIc⟩ ↦ ?_⟩
  · 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⟩
  rw [← hIc, ← hI.eRk_eq_encard]
  exact M.eRk_mono hIX

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ M.eRk X = 1 → ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis X
    rw [hI.eRk_eq_encard, encard_eq_one]
    rintro ⟨e, rfl⟩
    exact ⟨e, singleton_subset_iff.1 hI.subset, indep_singleton.1 hI.indep, hI.subset_closure⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hinj : InjOn f I
⊢ I.encard = M.eRk (f '' X)

Tactic:
← hI'.encard_eq_eRk,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hinj : InjOn f I
⊢ I.encard = (f '' I).encard
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E ∧ Disjoint X (M.closure (B \ {e}))
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
hsp : M.IsBase (insert f (B \ {e}))
⊢ M.Spanning (M.E \ X)

Tactic:
refine hsp.spanning.superset <| insert_subset hf <|
      (M.subset_closure _ (sdiff_subset.trans hB.subset_ground)).trans ?_
    rw [subset_sdiff, and_iff_left hXss.2.symm]
    apply closure_subset_ground

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
hf : Transcendental R f
⊢ Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)

Tactic:
rw [transcendental_iff_injective] at hf ⊢
  let g := MvPolynomial.mapAlgHom (R := R) (σ := s) (Polynomial.aeval (R := R) f)
  replace hf : Function.Injective g := MvPolynomial.map_injective _ hf
  let u := (Subalgebra.val _).comp
    ((optionEquivRight R s).symm |>.trans
      (renameEquiv R (Set.subtypeInsertEquivOption h).symm) |>.trans
      (supportedEquivMvPolynomial _).symm).toAlgHom |>.comp
    g |>.comp
    ((optionEquivLeft R s).symm.trans (optionEquivRight R s)).toAlgHom
  let v := ((Polynomial.aeval (R := supported R s)
    (Polynomial.aeval (X i : MvPolynomial σ R) f)).restrictScalars R).comp
      (Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm).toAlgHom
  replace hf : Function.Injective u := by
    simp only [AlgHom.coe_comp, Subalgebra.coe_val,
      AlgEquiv.coe_toAlgHom, AlgEquiv.coe_trans, Function.comp_assoc, u]
    apply Subtype.val_injective.comp
    simp only [EquivLike.comp_injective]
    apply hf.comp
    simp only [EquivLike.comp_injective, EquivLike.injective]
  have h1 : Polynomial.aeval (X i : MvPolynomial σ R) = ((Subalgebra.val _).comp
      (supportedEquivMvPolynomial _).symm.toAlgHom |>.comp
      (Polynomial.aeval (X ⟨i, s.mem_insert i⟩ : MvPolynomial ↑(insert i s) R))) := by
    ext1; simp
  have h2 : u = v := by
    simp only [u, v, g]
    ext1
    · ext1
      simp [Set.subtypeInsertEquivOption, Subalgebra.algebraMap_eq, optionEquivLeft_symm_apply]
    · simp [Set.subtypeInsertEquivOption, h1, optionEquivLeft_symm_apply]
  simpa only [h2, v, AlgHom.coe_comp, AlgEquiv.coe_toAlgHom,
    EquivLike.injective_comp, AlgHom.coe_restrictScalars'] using hf

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
⊢ M.closure (I ∩ J) = M.closure I ∩ M.closure J

Tactic:
rw [inter_eq_iInter, closure_iInter_eq_iInter_closure_of_iUnion_indep, inter_eq_iInter]
  · exact iInter_congr (by simp)
  rwa [← union_eq_iUnion]

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

Goal state before:
pp: ι : Type u
A : Type v
x : ι → A
inst✝⁴ : CommRing A
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsEmpty ι
inst✝ : Nontrivial A
⊢ Injective ⇑(algebraMap K A)

Tactic:
exact RingHom.injective _

Goal state after:
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
a : α
h₁ : a ∈ fixedBy α m₁
h₂ : a ∈ fixedBy α m₂
⊢ (m₁ * m₂) • a = a

Tactic:
mul_smul,

Goal state after:
α : Type u_1
M : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
m₁ m₂ : M
a : α
h₁ : a ∈ fixedBy α m₁
h₂ : a ∈ fixedBy α m₂
⊢ m₁ • m₂ • a = a
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
a : α
⊢ g • h⁻¹ • a = h⁻¹ • a ↔ (h * g * h⁻¹) • a = a

Tactic:
mul_smul,

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
a : α
⊢ g • h⁻¹ • a = h⁻¹ • a ↔ h • g • h⁻¹ • a = a
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
comm : Commute g h
x : α
⊢ (h⁻¹ * g) • x = h⁻¹ • x ↔ x ∈ fixedBy α g

Tactic:
mul_smul,

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
comm : Commute g h
x : α
⊢ h⁻¹ • g • x = h⁻¹ • x ↔ x ∈ fixedBy α g
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_3
inst✝² : Monoid G
inst✝¹ : MulAction G A
inst✝ : MulAction G B
f : A →ₑ[id] B
H : Submonoid G
a : A
ha : a ∈ MulAction.fixedPoints (↥H) A
h : G
property✝ : h ∈ H
⊢ ⟨h, property✝⟩ • f a = f a

Tactic:
simp_all [← f.map_smul h a]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M α
s : Set α
x y : M
hx : x ∈ {ϕ | ∀ (x : ↑s), ϕ • ↑x = ↑x}
hy : y ∈ {ϕ | ∀ (x : ↑s), ϕ • ↑x = ↑x}
z : ↑s
⊢ (x * y) • ↑z = ↑z

Tactic:
mul_smul,

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M α
s : Set α
x y : M
hx : x ∈ {ϕ | ∀ (x : ↑s), ϕ • ↑x = ↑x}
hy : y ∈ {ϕ | ∀ (x : ↑s), ϕ • ↑x = ↑x}
z : ↑s
⊢ x • y • ↑z = ↑z
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
a : A
ai : AlgebraicIndependent R fun o ↦ o.elim a x
h₁ : range x ⊆ range fun o ↦ o.elim a x
h : range x = range fun o ↦ o.elim a x
this : a ∈ range x
⊢ False

Tactic:
rcases this with ⟨b, rfl⟩

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
b : ι
ai : AlgebraicIndependent R fun o ↦ o.elim (x b) x
h₁ : range x ⊆ range fun o ↦ o.elim (x b) x
h : range x = range fun o ↦ o.elim (x b) x
⊢ False
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : 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
⊢ IsTranscendenceBasis R (Sum.elim y (⇑(algebraMap S A) ∘ x))

Tactic:
by
  cases subsingleton_or_nontrivial R
  · rw [isTranscendenceBasis_iff_of_subsingleton] at hx ⊢; infer_instance
  rw [(hx.1.sumElim_comp hy.1).isTranscendenceBasis_iff_isAlgebraic]
  set Rx := adjoin R (range x)
  let Rxy := adjoin Rx (range y)
  rw [show adjoin R (range <| Sum.elim y (algebraMap S A ∘ x)) = Rxy.restrictScalars R by
    rw [← adjoin_algebraMap_image_union_eq_adjoin_adjoin, Sum.elim_range, union_comm, range_comp]]
  change Algebra.IsAlgebraic Rxy A
  have := hx.1.algebraMap_injective.nontrivial
  have := hy.1.algebraMap_injective.nontrivial
  have := hy.isAlgebraic
  set Sy := adjoin S (range y)
  let _ : Algebra Rxy Sy := by
    refine (Subalgebra.inclusion (T := Sy.restrictScalars Rx) <| adjoin_le ?_).toAlgebra
    rintro _ ⟨i, rfl⟩; exact subset_adjoin (s := range y) ⟨i, rfl⟩
  have : IsScalarTower Rxy Sy A := .of_algebraMap_eq fun ⟨a, _⟩ ↦ show a = _ from rfl
  have : IsScalarTower Rx Rxy Sy := .of_algebraMap_eq fun ⟨a, _⟩ ↦ Subtype.ext rfl
  have : Algebra.IsAlgebraic Rxy Sy := by
    refine ⟨fun ⟨a, ha⟩ ↦ adjoin_induction ?_ (fun _ ↦ .extendScalars (R := Rx) ?_ ?_)
      (fun _ _ _ _ ↦ .add) (fun _ _ _ _ ↦ .mul) ha⟩
    · rintro _ ⟨i, rfl⟩; exact isAlgebraic_algebraMap (⟨y i, subset_adjoin ⟨i, rfl⟩⟩ : Rxy)
    · exact fun _ _ ↦ (Subtype.ext <| hy.1.algebraMap_injective <| Subtype.ext_iff.mp ·)
    · exact (hx.isAlgebraic.1 _).algHom (IsScalarTower.toAlgHom Rx S Sy)
  exact .trans _ Sy _

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_2.inl
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
h : g = 0
⊢ ∃ x, C x = g

pp: case refine_2.inr
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
x : F
h : C x = g
⊢ ∃ x, C x = g

Tactic:
· exact ⟨0, by rw [h, map_zero]⟩

Goal state after:
case refine_2.inr
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
x : F
h : C x = g
⊢ ∃ x, C x = g
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: case refine_1
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✝
K L : IntermediateField F E
le : K ≤ L
x : E
hx : x ∈ (fun K ↦ IntermediateField.restrictScalars F (separableClosure (↥K) E)) K
x✝ : Algebra ↥K ↥L := (inclusion le).toAlgebra
⊢ x ∈ (fun K ↦ IntermediateField.restrictScalars F (separableClosure (↥K) E)) L

Tactic:
have : IsScalarTower K L E := .of_algebraMap_eq' rfl

Goal state after:
case refine_1
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✝
K L : IntermediateField F E
le : K ≤ L
x : E
hx : x ∈ (fun K ↦ IntermediateField.restrictScalars F (separableClosure (↥K) E)) K
x✝ : Algebra ↥K ↥L := (inclusion le).toAlgebra
this : IsScalarTower (↥K) (↥L) E
⊢ x ∈ (fun K ↦ IntermediateField.restrictScalars F (separableClosure (↥K) E)) L
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case convert_2.refine_2
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
x✝ : ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0
n : ℕ
y : F
h : (Polynomial.aeval x) (X ^ q ^ n - C y) = 0
⊢ (minpoly F x).natSepDegree = 1

Tactic:
have hnezero := X_pow_sub_C_ne_zero (expChar_pow_pos F q n) y

Goal state after:
case convert_2.refine_2
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
x✝ : ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0
n : ℕ
y : F
h : (Polynomial.aeval x) (X ^ q ^ n - C y) = 0
hnezero : X ^ q ^ n - C y ≠ 0
⊢ (minpoly F x).natSepDegree = 1
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)
⊢ τ ∈ (map (↑σ) E).fixingSubgroup ↔ τ ∈ MulAut.conj σ • E.fixingSubgroup

Tactic:
simp only [coe_map, AlgEquiv.coe_toAlgHom, Set.mem_image, SetLike.mem_coe, AlgEquiv.smul_def,
    forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
    Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ← symm_apply_eq,
    IntermediateField.fixingSubgroup, mem_fixingSubgroup_iff]

Goal state after:
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
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 α
this : finSepDegree F ↥F⟮α⟯ = Nat.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) }
⊢ Fintype.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) } =
    Fintype.card ↥((minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯)).toFinset

Tactic:
simp_rw [Multiset.mem_toFinset]

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

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
U V : Set G
x✝¹ : ∃ T ∈ 𝓝 1, U * T ⊆ W
x✝ : ∃ T ∈ 𝓝 1, V * T ⊆ W
T₁ : Set G
hT₁ : T₁ ∈ 𝓝 1
mem1 : U * T₁ ⊆ W
T₂ : Set G
hT₂ : T₂ ∈ 𝓝 1
mem2 : V * T₂ ⊆ W
⊢ (U ∪ V) * (T₁ ∩ T₂) ⊆ W

Tactic:
union_mul

Goal state after:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
U V : Set G
x✝¹ : ∃ T ∈ 𝓝 1, U * T ⊆ W
x✝ : ∃ T ∈ 𝓝 1, V * T ⊆ W
T₁ : Set G
hT₁ : T₁ ∈ 𝓝 1
mem1 : U * T₁ ⊆ W
T₂ : Set G
hT₂ : T₂ ∈ 𝓝 1
mem2 : V * T₂ ⊆ W
⊢ U * (T₁ ∩ T₂) ∪ V * (T₁ ∩ T₂) ⊆ W