mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
⊢ (∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J') →
    ∃ x, I * (toPrincipalIdeal R (FractionRing R)) x = J

Tactic:
rintro ⟨x, y, hx, hy, h⟩

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
⊢ ∃ x, I * (toPrincipalIdeal R (FractionRing R)) x = J
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤) → ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}

Tactic:
rintro ⟨x, y, hx, hy, h⟩

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * ⊤
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ (∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), Ideal.span {x} * ↑I = Ideal.span {y} * ↑J) →
    ∃ x, ∃ (_ : x ≠ 0), spanSingleton R⁰ x * ↑↑I = ↑↑J

Tactic:
rintro ⟨x, y, hx, hy, h⟩

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
⊢ ∃ x, ∃ (_ : x ≠ 0), spanSingleton R⁰ x * ↑↑I = ↑↑J
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
fd_ne_zero : (algebraMap R (FractionRing R)) ↑(↑I).den ≠ 0
⊢ I * (toPrincipalIdeal R (FractionRing R)) (Units.mk0 ((algebraMap R (FractionRing R)) ↑(↑I).den) fd_ne_zero) =
    (FractionalIdeal.mk0 (FractionRing R)) ⟨integralRep ↑I, ⋯⟩

Tactic:
apply Units.ext

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
fd_ne_zero : (algebraMap R (FractionRing R)) ↑(↑I).den ≠ 0
⊢ ↑(I * (toPrincipalIdeal R (FractionRing R)) (Units.mk0 ((algebraMap R (FractionRing R)) ↑(↑I).den) fd_ne_zero)) =
    ↑((FractionalIdeal.mk0 (FractionRing R)) ⟨integralRep ↑I, ⋯⟩)
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : Subsingleton (ClassGroup R)
I : (FractionalIdeal R⁰ K)ˣ
⊢ (↑↑I).IsPrincipal

Tactic:
rw [← ClassGroup.mk_eq_one_iff, Subsingleton.elim (ClassGroup.mk K I) 1]

Goal state after:
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₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x ↦ x ∈ C₁
⊢ IsLocallyConstant fun i ↦ if hi : i ∈ C₁ then f ⟨i, hi⟩ else g ⟨i, ⋯⟩

Tactic:
let dZ : TopologicalSpace Z := ⊥

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
⊢ IsLocallyConstant fun i ↦ if hi : i ∈ C₁ then f ⟨i, hi⟩ else g ⟨i, ⋯⟩
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst✝⁷ : CommRing Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p.asIdeal
inst✝⁴ : AddCommGroup Mₚ
inst✝³ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝² : IsLocalizedModule p.asIdeal.primeCompl f
inst✝¹ : Module Rₚ Mₚ
inst✝ : IsScalarTower R Rₚ Mₚ
e : Localization.AtPrime p.asIdeal ≃+* Rₚ := ⋯
⊢ LocalizedModule p.asIdeal.primeCompl M ≃ₛₗ[↑e] Mₚ

Tactic:
refine { __ := IsLocalizedModule.iso p.asIdeal.primeCompl f, map_smul' := ?_ }

Goal state after:
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst✝⁷ : CommRing Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p.asIdeal
inst✝⁴ : AddCommGroup Mₚ
inst✝³ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝² : IsLocalizedModule p.asIdeal.primeCompl f
inst✝¹ : Module Rₚ Mₚ
inst✝ : IsScalarTower R Rₚ Mₚ
e : Localization.AtPrime p.asIdeal ≃+* Rₚ :=
  (IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ).toRingEquiv
⊢ ∀ (m : Localization.AtPrime p.asIdeal) (x : LocalizedModule p.asIdeal.primeCompl M),
    (↑(IsLocalizedModule.iso p.asIdeal.primeCompl f)).toFun (m • x) =
      ↑e m • (↑(IsLocalizedModule.iso p.asIdeal.primeCompl f)).toFun x
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
⊢ ∃ t ⊆ freeLocus R M, IsOpen t ∧ x ∈ t

Tactic:
obtain ⟨r, hr, hr', _⟩ := Module.FinitePresentation.exists_free_localizedModule_powers
    x.asIdeal.primeCompl (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
    (Localization.AtPrime x.asIdeal)

Goal state after:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
r : R
hr : r ∈ x.asIdeal.primeCompl
hr' : Free (Localization (Submonoid.powers r)) (LocalizedModule.Away r M)
right✝ :
  finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
⊢ ∃ t ⊆ freeLocus R M, IsOpen t ∧ x ∈ t
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
⊢ IsLocallyConstant fun x ↦ rankAtStalk M ↑x

Tactic:
refine (IsLocallyConstant.iff_exists_open _).mpr fun ⟨x, hx⟩ ↦ ?_
  have : Module.Free _ _ := hx
  obtain ⟨f, hf, hf', hf''⟩ := Module.FinitePresentation.exists_free_localizedModule_powers
    x.asIdeal.primeCompl (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
    (Localization.AtPrime x.asIdeal)
  refine ⟨Subtype.val ⁻¹' basicOpen f, (basicOpen f).2.preimage continuous_subtype_val, hf, ?_⟩
  rintro ⟨p, hp''⟩ hp
  let p' := Algebra.algebraMapSubmonoid (Localization (.powers f)) p.asIdeal.primeCompl
  have hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl := by
    simpa [Submonoid.powers_le, Ideal.primeCompl]
  let Rₚ := Localization.AtPrime p.asIdeal
  let Mₚ := LocalizedModule p.asIdeal.primeCompl M
  let : Algebra (Localization.Away f) Rₚ :=
    IsLocalization.localizationAlgebraOfSubmonoidLe _ _ (.powers f) p.asIdeal.primeCompl hp'
  have : IsScalarTower R (Localization.Away f) Rₚ :=
    IsLocalization.localization_isScalarTower_of_submonoid_le ..
  let : Module (Localization.Away f) Mₚ := Module.compHom Mₚ (algebraMap _ Rₚ)
  have : IsScalarTower R (Localization.Away f) Mₚ :=
    ⟨fun r r' m ↦ show algebraMap _ Rₚ (r • r') • m = _ by
      simp [Rₚ, Mₚ, Algebra.smul_def, ← IsScalarTower.algebraMap_apply, mul_smul]; rfl⟩
  have : IsScalarTower (Localization.Away f) Rₚ Mₚ :=
    ⟨fun r r' m ↦ show _ = algebraMap _ Rₚ r • r' • m by rw [← mul_smul, ← Algebra.smul_def]⟩
  let l := (IsLocalizedModule.liftOfLE _ _ hp' (LocalizedModule.mkLinearMap (.powers f) M)
    (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M)).extendScalarsOfIsLocalization (.powers f)
    (Localization.Away f)
  have : IsLocalization p' Rₚ :=
    IsLocalization.isLocalization_of_submonoid_le (Localization.Away f) Rₚ _ _ hp'
  have : IsLocalizedModule p.asIdeal.primeCompl (l.restrictScalars R) :=
    inferInstanceAs (IsLocalizedModule p.asIdeal.primeCompl
    ((IsLocalizedModule.liftOfLE _ _ hp' (LocalizedModule.mkLinearMap (.powers f) M)
      (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M))))
  have : IsLocalizedModule (Algebra.algebraMapSubmonoid _ p.asIdeal.primeCompl) l :=
      IsLocalizedModule.of_restrictScalars p.asIdeal.primeCompl ..
  have := Module.finrank_of_isLocalizedModule_of_free Rₚ p' l
  simp [Rₚ, rankAtStalk, this, hf'']

Goal state after:
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
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
x : (Polynomial.map ιFE g).SplittingField
hx : eval₂ ιEE' x h = 0
⊢ ιEE' γ - ιEE' (ιFE c) * x ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots

Tactic:
have f_root := root_left_of_root_gcd hx
      rw [eval₂_comp, eval₂_sub, eval₂_mul, eval₂_C, eval₂_C, eval₂_X, eval₂_map] at f_root
      exact (mem_roots_map (minpoly.ne_zero hα)).mpr f_root

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
⊢ M.IsBasis' I X ↔ M.IsBasis I (X ∩ M.E)

Tactic:
rw [IsBasis', IsBasis, and_iff_left inter_subset_right, maximal_iff_maximal_of_imp_of_forall]

Goal state after:
case hPQ
α : Type u_1
M : Matroid α
I X : Set α
⊢ ∀ ⦃x : Set α⦄, M.Indep x ∧ x ⊆ X ∩ M.E → M.Indep x ∧ x ⊆ X

case h
α : Type u_1
M : Matroid α
I X : Set α
⊢ ∀ ⦃x : Set α⦄, M.Indep x ∧ x ⊆ X → ∃ y, x ⊆ y ∧ M.Indep y ∧ y ⊆ X ∩ M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
⊢ M ↾ R ↾ R = M ↾ R

Tactic:
rw [M.restrict_restrict_eq Subset.rfl]

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

Goal state before:
pp: α : Type u_2
⊢ freeOn ∅ = emptyOn α

Tactic:
by
  simp [freeOn]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ (N.comap f).E ↔ N.Dep (f '' I) ∨ N.Indep (f '' I) ∧ ¬InjOn f I

Tactic:
comap_ground_eq,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E ↔ N.Dep (f '' I) ∨ N.Indep (f '' I) ∧ ¬InjOn f I
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
h : ¬M.IsBase (M.E \ ∅)
⊢ ¬M.IsBase M.E

Tactic:
sdiff_empty

Goal state after:
α : Type u_1
M : Matroid α
h : ¬M.IsBase M.E
⊢ ¬M.IsBase M.E
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ insert e I ⊆ (N.comap f).E

Tactic:
comap_ground_eq,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ insert e I ⊆ f ⁻¹' N.E
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ M.Coindep X ↔ ∃ B, M.IsBase B ∧ B ⊆ M.E \ X

Tactic:
rw [coindep_iff_exists', and_iff_left hX]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
ι : Type u_2
inst✝ : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
hfin : (⋃ i, Is i).Finite
⊢ (⋃ i, Xs i) ∩ M.E ⊆ M.closure (⋃ i, Is i)

Tactic:
iUnion_inter,

Goal state after:
α : Type u_1
M : Matroid α
ι : Type u_2
inst✝ : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
hfin : (⋃ i, Is i).Finite
⊢ ⋃ i, Xs i ∩ M.E ⊆ M.closure (⋃ i, Is i)
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set α
hI : M.Indep I
⊢ M.Indep I ∧ ⇑f '' I ⊆ range ⇑f

Tactic:
exact ⟨hI, image_subset_range _ _⟩

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

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

Tactic:
univ_inter,

Goal state after:
α : Type u_1
M : Matroid α
⊢ M.eRk M.E = M.eRank
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_2
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
C : Set α
hCE : C ⊆ M₁.E
hC : M₂.IsCircuit C
⊢ M₁.IsCircuit C

Tactic:
obtain ⟨C', hC'C, hC'⟩ := ((not_indep_iff hCE).1 (h₂ C hC)).exists_isCircuit_subset

Goal state after:
case refine_2
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
C : Set α
hCE : C ⊆ M₁.E
hC : M₂.IsCircuit C
C' : Set α
hC'C : C' ⊆ C
hC' : M₁.IsCircuit C'
⊢ M₁.IsCircuit C
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X.Finite
hXE : X ⊆ M.E
h : M.eRk X < X.encard
⊢ ¬M.Indep X

Tactic:
indep_iff_eRk_eq_encard_of_finite hX

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : X.Finite
hXE : X ⊆ M.E
h : M.eRk X < X.encard
⊢ ¬M.eRk X = X.encard
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
⊢ M.closure (univ ∩ M.E) = M.E

Tactic:
univ_inter,

Goal state after:
α : Type u_2
M : Matroid α
⊢ M.closure M.E = M.E
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ ↑(M.subtypeClosure ⟨(⋃ i, ↑(M.subtypeClosure ⟨Xs i ∩ M.E, ⋯⟩)) ∩ M.E, ⋯⟩) = ↑(M.subtypeClosure ⟨(⋃ i, Xs i) ∩ M.E, ⋯⟩)

Tactic:
iUnion_inter,

Goal state after:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ ↑(M.subtypeClosure ⟨⋃ i, ↑(M.subtypeClosure ⟨Xs i ∩ M.E, ⋯⟩) ∩ M.E, ⋯⟩) = ↑(M.subtypeClosure ⟨⋃ i, Xs i ∩ M.E, ⋯⟩)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
h : M = loopyOn M.E
⊢ M.eRank = 0

Tactic:
by rw [h, eRank_loopyOn]

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

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

Tactic:
closure_biUnion_closure_eq_closure_biUnion

Goal state after:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs Ys : ι → Set α
A : Set ι
h : ∀ i ∈ A, M.closure (Xs i) = M.closure (Ys i)
⊢ M.closure (⋃ i ∈ A, Ys i) = M.closure (⋃ i ∈ A, Ys i)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
⊢ (M ↾ X).cRk Y = M.cRk Y

Tactic:
have aux : ∀ ⦃I⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y := by
    simp_rw [isBasis'_restrict_iff, inter_eq_self_of_subset_left hYX, iff_self_and]
    exact fun I h ↦ h.subset.trans hYX

Goal state after:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
aux : ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y
⊢ (M ↾ X).cRk Y = M.cRk Y
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
by
  obtain rfl | hne := eq_or_ne e f
  · simp [hI, heI]
  rw [← insert_sdiff_singleton_comm hne.symm, hI.insert_indep_iff, mem_sdiff_singleton,
    and_iff_left hne.symm]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
⊢ M.IsCocircuit (M.E \ M.closure (B \ {e}))

Tactic:
rw [isCocircuit_iff_minimal_compl_nonspanning, minimal_subset_iff,
    sdiff_sdiff_cancel_left (M.closure_subset_ground _),
    closure_spanning_iff (sdiff_subset.trans hB.subset_ground)]
  have hB' := (isBase_iff_minimal_spanning.1 hB)
  refine ⟨fun hsp ↦ hB'.notMem_of_prop_sdiff_singleton hsp he, fun X hX hXss ↦ hXss.antisymm' ?_⟩
  rw [sdiff_subset_comm]
  refine fun f hf ↦ by_contra fun fcl ↦ hX ?_
  rw [subset_sdiff] at hXss
  suffices hsp : M.IsBase (insert f (B \ {e})) by
    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
  exact hB.exchange_base_of_notMem_closure he fcl

Goal state after:
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: case inr
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m m' : ℕ
h_expand : (expand F (q ^ m)) g = (expand F (q ^ m')) g'
hg : g.Separable
hg' : g'.Separable
this :
  ∀ {F : Type u_1} [inst : Field F] (q : ℕ) [hq : NeZero q] [CharP F q] (g g' : F[X]) (m m' : ℕ),
    (expand F (q ^ m)) g = (expand F (q ^ m')) g' → g.Separable → g'.Separable → m ≤ m' → g.natDegree = g'.natDegree
hm : ¬m ≤ m'
⊢ g.natDegree = g'.natDegree

Tactic:
exact (this q g' g m' m h_expand.symm hg' hg (le_of_not_ge hm)).symm

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

Goal state before:
pp: α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
⊢ ∀ (x : α), x ∈ (M.comap f).E ∧ ((M.comap f).Indep (insert x I) → x ∈ I) ↔ x ∈ f ⁻¹' M.closure (f '' I)

Tactic:
comap_ground_eq,

Goal state after:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
⊢ ∀ (x : α), x ∈ f ⁻¹' M.E ∧ ((M.comap f).Indep (insert x I) → x ∈ I) ↔ x ∈ f ⁻¹' M.closure (f '' I)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s B : Set A
hB : (matroid R A).IsBasis B s
⊢ ∀ (x : A), (∀ a ∈ insert x B, IsAlgebraic (↥(adjoin R B)) a) ↔ x ∈ ↑(algebraicClosure (↥(adjoin R s)) A)

Tactic:
SetLike.mem_coe,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s B : Set A
hB : (matroid R A).IsBasis B s
⊢ ∀ (x : A), (∀ a ∈ insert x B, IsAlgebraic (↥(adjoin R B)) a) ↔ x ∈ algebraicClosure (↥(adjoin R s)) A
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Set A
⊢ (∀ (x : A), x ∈ ↑(algebraicClosure (↥(adjoin R s)) A)) ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A

Tactic:
SetLike.mem_coe,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Set A
⊢ (∀ (x : A), x ∈ algebraicClosure (↥(adjoin R s)) A) ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
Module: Mathlib.FieldTheory.SeparableDegree

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✝ : Algebra E K := (↑i).toAlgebra
x : K
h : IsAlgebraic E ((algebraMap E K) (↑i.symm x))
⊢ IsAlgebraic E x

Tactic:
show ∀ y : E, (algebraMap E K) y = i.toAlgHom y from fun y ↦ rfl

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E ≃ₐ[F] K
x✝ : Algebra E K := (↑i).toAlgebra
x : K
h : IsAlgebraic E (↑i (↑i.symm x))
⊢ IsAlgebraic E x
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
n : ℕ
⊢ (f ^ n).natSepDegree = if n = 0 then 0 else f.natSepDegree

Tactic:
by
  classical
  simp only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_pow]
  by_cases h : n = 0
  · simp only [h, zero_smul, Multiset.toFinset_zero, Finset.card_empty, ite_true]
  simp only [h, Multiset.toFinset_nsmul _ n h, ite_false]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f✝ f g : F[X]
h : f = 0 ∨ g = 0
hf : f = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
rw [hf, zero_mul, natSepDegree_zero, zero_add, isCoprime_zero_left, isUnit_iff, eq_comm,
      natSepDegree_eq_zero_iff, natDegree_eq_zero]

Goal state after:
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h : f = 0 ∨ g = 0
hf : f = 0
⊢ (∃ x, C x = g) ↔ 0 = 0 ∧ g = 0 ∨ ∃ r, IsUnit r ∧ C r = g
Module: Mathlib.FieldTheory.SeparableDegree

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

Tactic:
refine ⟨n, y, (em _).imp id fun hn ⟨z, hy⟩ ↦ ?_, hf⟩

Goal state after:
case prime
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
n : ℕ
y : F
hf : f = X ^ q ^ n - C y
hq : Nat.Prime q
hchar✝ : CharP F q
hn : ¬n = 0
x✝ : y ∈ (frobenius F q).range
z : F
hy : (frobenius F q) z = y
⊢ False
Module: Mathlib.FieldTheory.SeparableDegree

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

Tactic:
cases id ‹ExpChar F q› with

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

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : IsGalois F E
inst✝ : FiniteDimensional F E
x : E
⊢ x ∈ ⊥ ↔ ∀ (f : Gal(E/F)), f x = x

Tactic:
rw [← fixedField_top, mem_fixedField_iff]

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : IsGalois F E
inst✝ : FiniteDimensional F E
x : E
⊢ (∀ f ∈ ⊤, f x = x) ↔ ∀ (f : Gal(E/F)), f x = x
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
inst✝⁷ : Field F
E✝ : Type u_2
inst✝⁶ : Field E✝
inst✝⁵ : Algebra F E✝
H : Subgroup Gal(E✝/F)
K✝ : IntermediateField F E✝
K : Type u_3
L : Type u_4
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : IntermediateField K L
inst✝¹ : IsGalois K L
inst✝ : IsGalois K ↥E
σ : Gal(L/K)
⊢ MulAut.conj σ • E.fixingSubgroup = E.fixingSubgroup

Tactic:
rw [← map_fixingSubgroup, normal_iff_forall_map_eq'.mp inferInstance σ]

Goal state after: