mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
z : R
⊢ ∀ (f : (i : ι) → s i), (liftAux φ) (r • tprodCoeff R z f) = r • (liftAux φ) (tprodCoeff R z f)

Tactic:
f

Goal state after:
case refine_1
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
z : R
f : (i : ι) → s i
⊢ (liftAux φ) (r • tprodCoeff R z f) = r • (liftAux φ) (tprodCoeff R z f)
Module: Mathlib.LinearAlgebra.TensorPower.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
⊢ (cast R M ⋯) (GradedMonoid.GMul.mul (algebraMap₀ r) (algebraMap₀ s)) = algebraMap₀ (r * s)

Tactic:
by
  rw [← smul_eq_mul, map_smul]
  exact algebraMap₀_mul r (@algebraMap₀ R M _ _ _ s)

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
e : ι ≃ ι₂
φ : MultilinearMap R (fun i ↦ s (e.symm i)) E
⊢ lift φ ∘ₗ ↑(reindex R s e) = lift ((domDomCongrLinearEquiv' R R s E e).symm φ)

Tactic:
ext; simp [reindex]

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
e : ι ≃ ι₂
φ : MultilinearMap R s E
⊢ lift φ ∘ₗ ↑(reindex R s e).symm = lift ((domDomCongrLinearEquiv' R R s E e) φ)

Tactic:
ext; simp [reindex]

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝³ : CommSemiring R
M : Type u_8
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
i₀ : ι
x : M
⊢ (subsingletonEquiv i₀).symm x = (tprod R) fun x_1 ↦ x

Tactic:
simp [LinearEquiv.symm_apply_eq, subsingletonEquiv_apply_tprod]

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : N₁.IsQuotientEquivQuotientPrime N₂
h : N₁ ≤ N₂
p : PrimeSpectrum A
e : (↥N₂ ⧸ N₁.submoduleOf N₂) ≃ₗ[A] A ⧸ p.asIdeal
x : M
hx : x ∈ N₂
hx' : (N₁.submoduleOf N₂).mkQ ⟨x, hx⟩ = e.symm 1
hx'' : N₁.mkQ x = f (e.symm 1)
r : A
⊢ r ∈ ⊥.colon {N₁.mkQ x} ↔ r ∈ p.asIdeal

Tactic:
simp [hx'', ← map_smul, Algebra.smul_def, show f _ = 0 ↔ _ from congr(_ ∈ $hf₁),
        Ideal.Quotient.eq_zero_iff_mem]

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
p : Ideal R
toIsPrime✝ : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
h : ∃ a ∈ p.primeCompl, ∃ y k, f y = a ^ k • x
⊢ p ∈ associatedPrimes R M ∪ associatedPrimes R M''

pp: case neg
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
p : Ideal R
toIsPrime✝ : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
h : ∀ a ∈ p.primeCompl, ∀ (y : M) (k : ℕ), f y ≠ a ^ k • x
⊢ p ∈ associatedPrimes R M ∪ associatedPrimes R M''

Tactic:
· obtain ⟨a, ha, y, k, h⟩ := h
    left
    refine ⟨‹_›, y, le_antisymm (fun b hb ↦ ?_) (fun b ⟨n, hb⟩ ↦ ?_)⟩
    · rw [hx] at hb
      obtain ⟨n, hb⟩ := hb
      use n
      rw [mem_colon_singleton, mem_bot] at hb ⊢
      apply_fun _ using hf
      rw [map_smul, h, smul_comm, hb, smul_zero, map_zero]
    · rw [mem_colon_singleton, mem_bot] at hb
      apply_fun f at hb
      rw [map_smul, map_zero, h, ← mul_smul, ← mem_bot R, ← mem_colon_singleton] at hb
      replace hb := hx.ge (Ideal.le_radical hb)
      contrapose hb
      exact p.primeCompl.mul_mem (p.primeCompl.pow_mem hb n) (p.primeCompl.pow_mem ha k)

Goal state after:
case neg
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
p : Ideal R
toIsPrime✝ : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
h : ∀ a ∈ p.primeCompl, ∀ (y : M) (k : ℕ), f y ≠ a ^ k • x
⊢ p ∈ associatedPrimes R M ∪ associatedPrimes R M''
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: case refine_2.refine_3
A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x
x : M
hx : (⊥.colon {N₁.mkQ x}).IsPrime
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
⊢ map (N₁.submoduleOf N₂).mkQ (toSpanSingleton A ↥N₂ ⟨x, hxN₂⟩).range = ⊤

Tactic:
have := congr($(hx').submoduleOf N₂)

Goal state after:
case refine_2.refine_3
A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x
x : M
hx : (⊥.colon {N₁.mkQ x}).IsPrime
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
this : N₂.submoduleOf N₂ = (N₁ ⊔ A ∙ x).submoduleOf N₂
⊢ map (N₁.submoduleOf N₂).mkQ (toSpanSingleton A ↥N₂ ⟨x, hxN₂⟩).range = ⊤
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mp.refine_1
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✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
X : (FractionalIdeal R⁰ K)ˣ
hx : ↑↑I * ↑X = ↑↑J
hX : spanSingleton R⁰ 0 = ↑X
⊢ False

Tactic:
simp [X.ne_zero.symm] at hX

Goal state after:
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
f : R
⊢ ↑(basicOpen f) ⊆ freeLocus R M ↔ Projective (Localization.Away f) (LocalizedModule.Away f M)

Tactic:
by
  rw [← freeLocus_eq_univ_iff, freeLocus_localization,
    Set.preimage_eq_univ_iff, localization_away_comap_range _ f]

Goal state after:
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✝ : ↑(freeLocus R M)
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this✝² : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : p ∈ freeLocus R M
hp : ⟨p, hp''⟩ ∈ Subtype.val ⁻¹' ↑(basicOpen f)
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl
Rₚ : Type uR := Localization.AtPrime p.asIdeal
Mₚ : Type (max uR uM) := LocalizedModule p.asIdeal.primeCompl M
this✝¹ : Algebra (Localization.Away f) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization.Away f) Rₚ (Submonoid.powers f) p.asIdeal.primeCompl hp'
this✝ : IsScalarTower R (Localization.Away f) Rₚ
this : Module (Localization.Away f) Mₚ := compHom Mₚ (algebraMap (Localization.Away f) Rₚ)
⊢ rankAtStalk M ↑⟨p, hp''⟩ = rankAtStalk M ↑⟨x, hx⟩

Tactic:
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⟩

Goal state after:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x✝ : ↑(freeLocus R M)
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this✝³ : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : p ∈ freeLocus R M
hp : ⟨p, hp''⟩ ∈ Subtype.val ⁻¹' ↑(basicOpen f)
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl
Rₚ : Type uR := Localization.AtPrime p.asIdeal
Mₚ : Type (max uR uM) := LocalizedModule p.asIdeal.primeCompl M
this✝² : Algebra (Localization.Away f) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization.Away f) Rₚ (Submonoid.powers f) p.asIdeal.primeCompl hp'
this✝¹ : IsScalarTower R (Localization.Away f) Rₚ
this✝ : Module (Localization.Away f) Mₚ := compHom Mₚ (algebraMap (Localization.Away f) Rₚ)
this : IsScalarTower R (Localization.Away f) Mₚ
⊢ rankAtStalk M ↑⟨p, hp''⟩ = rankAtStalk M ↑⟨x, hx⟩
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
⊢ ⨆ f, f.fieldRange ≤ K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K

Tactic:
iSup_le_iff

Goal state after:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
⊢ (∀ (i : ↥K →ₐ[F] L), i.fieldRange ≤ K) ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
⊢ ⨆ f, map f K ≤ K ↔ ∀ (σ : L →ₐ[F] L), map σ K ≤ K

Tactic:
iSup_le_iff

Goal state after:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
⊢ (∀ (i : L →ₐ[F] L), map i K ≤ K) ↔ ∀ (σ : L →ₐ[F] L), map σ K ≤ K
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
⊢ ⨆ f, map (↑f) K ≤ K ↔ ∀ (σ : Gal(L/F)), map (↑σ) K ≤ K

Tactic:
iSup_le_iff

Goal state after:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
⊢ (∀ (i : Gal(L/F)), map (↑i) K ≤ K) ↔ ∀ (σ : Gal(L/F)), map (↑σ) K ≤ K
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ {I | ∃ B, M.IsBase B ∧ I ⊆ B} = {x | ∃ a ∈ {B | M.IsBase B}, x ⊆ a}

Tactic:
mem_ofPred

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B I : Set α
hB : M.IsBase B
hI : M.Indep I
hBI : B ⊆ I
B' : Set α
hB' : M.IsBase B'
hB'I : I ⊆ B'
⊢ I ⊆ B

Tactic:
rwa [hB.eq_of_subset_isBase hB' (hBI.trans hB'I)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : SurjOn f E N.E
⊢ InjOn f B → B ⊆ E → (N.IsBasis (f '' B) (f '' E ∩ N.E) ↔ N.IsBase (f '' B))

Tactic:
inter_eq_self_of_subset_right h,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : SurjOn f E N.E
⊢ InjOn f B → B ⊆ E → (N.IsBasis (f '' B) N.E ↔ N.IsBase (f '' B))
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ : Set α
M✝ : Matroid α
N : Matroid β
E X I : Set α
M : Matroid α
inst✝ : M.RankPos
B : Set ↑M.E
hB : (M.restrictSubtype M.E).IsBase B
hB' : M.IsBase (Subtype.val '' B)
⊢ B.Nonempty

Tactic:
simpa using hB'.nonempty

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

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

Tactic:
← hI.eRk_eq_eRk,

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

Goal state before:
pp: α : Type u_1
M : Matroid α
R X I : Set α
hI : (M ↾ R).IsBasis' I X
⊢ (M ↾ R).eRk X = M.eRk (X ∩ R)

Tactic:
rw [hI.eRk_eq_encard]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ M.eRk X ≤ X.encard

Tactic:
rw [hI.eRk_eq_encard]

Goal state after:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ I.encard ≤ X.encard
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hcl : z ∈ M.closure ((⋃ i, I i) ∪ J \ {z})
⊢ ∃ C' ⊆ J ∪ ⋃ i, I i, M.IsCircuit C' ∧ z ∈ C'

Tactic:
rw [mem_closure_iff_exists_isCircuit (by simp [hzI])] at hcl
    obtain ⟨C', hC'ss, hC', hzC'⟩ := hcl
    refine ⟨C', ?_, hC', hzC'⟩
    rwa [union_comm, ← insert_union, insert_sdiff_singleton, insert_eq_of_mem hzJ] at hC'ss

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

Goal state before:
pp: α : Type u_1
X Y : Set α
M : Matroid α
h : Y ⊆ X
⊢ M.eRk X ≤ M.eRk Y + M.eRk (X \ Y)

Tactic:
by
  nth_rw 1 [← union_sdiff_cancel h]; apply eRk_union_le_eRk_add_eRk

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.Nonempty
hX : X ⊆ M.E
⊢ M.eRk X ≤ 1 ↔ ∃ e ∈ M.E, X ⊆ M.closure {e}

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨e, _, he⟩ ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.Nonempty
hX : X ⊆ M.E
h : M.eRk X ≤ 1
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}

case refine_2
α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.Nonempty
hX : X ⊆ M.E
x✝ : ∃ e ∈ M.E, X ⊆ M.closure {e}
e : α
left✝ : e ∈ M.E
he : X ⊆ M.closure {e}
⊢ M.eRk X ≤ 1
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: case refine_1.inl
α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.Nonempty
hX : X ⊆ M.E
hI : M.IsBasis ∅ X
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}

Tactic:
obtain ⟨e, he⟩ := M.ground_nonempty

Goal state after:
case refine_1.inl
α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.Nonempty
hX : X ⊆ M.E
hI : M.IsBasis ∅ X
e : α
he : e ∈ M.E
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.RankFinite
hX : X ⊆ M.E
⊢ M.Spanning X ↔ M.eRank ≤ M.eRk X

Tactic:
spanning_iff_eRk_le',

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.RankFinite
hX : X ⊆ M.E
⊢ M.eRank ≤ M.eRk X ∧ X ⊆ M.E ↔ M.eRank ≤ M.eRk X
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:
by
  rw [← closure_closure_union_closure_eq_closure_union, closure_closure,
    closure_closure_union_closure_eq_closure_union]

Goal state after:
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:
by
  rw [← closure_closure_union_closure_eq_closure_union, closure_closure,
    closure_closure_union_closure_eq_closure_union]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.IsBasis I (insert e I) ↔ e ∈ {x | M.IsBasis I (insert x I)}

Tactic:
mem_ofPred

Goal state after:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.IsBasis I (insert e I) ↔ M.IsBasis I (insert e I)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e : α
⊢ ∀ {f : α}, e ∈ M.fundCocircuit f B → f ∈ M.fundCircuit e B

Tactic:
f

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
⊢ e ∈ M.fundCocircuit f B → f ∈ M.fundCircuit e B
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : ¬Injective ⇑(algebraMap R A)
this : IsEmpty { s // AlgebraicIndepOn R _root_.id s }
⊢ trdeg R A = 0

Tactic:
rw [trdeg, ciSup_of_empty, bot_eq_zero]

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

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
h : a ∈ fixedBy α g
j : ℤ
⊢ g ^ j • a = a

Tactic:
zpow_smul_eq_iff_minimalPeriod_dvd,

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
h : a ∈ fixedBy α g
j : ℤ
⊢ ↑(Function.minimalPeriod (fun x ↦ g • x) a) ∣ j
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
h : a ∈ fixedBy α g
j : ℤ
⊢ 1 ∣ j

Tactic:
exact one_dvd j

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

Goal state before:
pp: case neg
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
s : Set A
inst✝ : NoZeroDivisors A
alg : Algebra.IsAlgebraic (↥(adjoin R s)) A
h : ¬Injective ⇑(algebraMap R A)
⊢ trdeg R A ≤ #↑s

Tactic:
simp [trdeg_eq_zero_of_not_injective h]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
x : F
hx : x ≠ 0
⊢ (C x * f).natSepDegree = f.natSepDegree

Tactic:
by
  classical
  simp only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_C_mul _ hx]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
x y : F
n : ℕ
hx : x ≠ 0
⊢ (C x * (X - C y) ^ n).natSepDegree = if n = 0 then 0 else 1

Tactic:
simp only [natSepDegree_C_mul _ hx, natSepDegree_X_sub_C_pow]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
q : ℕ
hF : ExpChar F q
n : ℕ
⊢ ((expand F (q ^ n)) f).natSepDegree = f.natSepDegree

Tactic:
obtain - | hprime := hF
  · simp only [one_pow, expand_one]
  have := Fact.mk hprime
  classical
  simpa only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_def, map_expand,
    Fintype.card_coe] using Fintype.card_eq.2
      ⟨(f.map (algebraMap F (AlgebraicClosure F))).rootsExpandPowEquivRoots q n⟩

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

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

Tactic:
rw [B.nhds_one_eq]
  exact B.toFilterBasis.hasBasis

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✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Nat.card Gal(E/F) = finrank F E
tfae_1_to_4 : IsGalois F E → ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : fixedField ⊤ = ⊥ → IsGalois F E
⊢ [IsGalois F E, fixedField ⊤ = ⊥, Nat.card Gal(E/F) = finrank F E,
      ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE

Tactic:
tfae_have 3 → 1 := of_card_aut_eq_finrank F E

Goal state after:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Nat.card Gal(E/F) = finrank F E
tfae_1_to_4 : IsGalois F E → ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : fixedField ⊤ = ⊥ → IsGalois F E
tfae_3_to_1 : Nat.card Gal(E/F) = finrank F E → IsGalois F E
⊢ [IsGalois F E, fixedField ⊤ = ⊥, Nat.card Gal(E/F) = finrank F E,
      ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE
Module: Mathlib.FieldTheory.Galois.GaloisClosure

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
f : K →ₐ[k] K
s : Set K
inst✝ : Finite ↑s
⊢ normalClosure k (↥(map f (IntermediateField.adjoin k s))) K = normalClosure k (↥(IntermediateField.adjoin k s)) K

Tactic:
IntermediateField.normalClosure_map_eq

Goal state after:
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
f : K →ₐ[k] K
s : Set K
inst✝ : Finite ↑s
⊢ normalClosure k (↥(IntermediateField.adjoin k s)) K = normalClosure k (↥(IntermediateField.adjoin k s)) K
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
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
⊢ (algebraMap R S) ((minpoly R x).coeff ((minpolyDiv R x).natDegree - (i + 1) + 1)) +
      ((minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - (i + 1) + 1) * x - x ^ i * x) ∈
    Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))

Tactic:
← sub_mul,

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
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
⊢ (algebraMap R S) ((minpoly R x).coeff ((minpolyDiv R x).natDegree - (i + 1) + 1)) +
      ((minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - (i + 1) + 1) - x ^ i) * x ∈
    Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = (algebraMap R K[X]) c * p
⊢ IsUnit p

Tactic:
algebraMap_apply

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
⊢ IsUnit p