mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: A : Type u
inst✝³ : CommRing A
inst✝² : IsNoetherianRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
x✝ : Module.Finite A M
motive : (N : Type v) → [inst : AddCommGroup N] → [inst_1 : Module A N] → [Module.Finite A N] → Prop
subsingleton :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] [Subsingleton N], motive N
quotient :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] (p : PrimeSpectrum A)
    (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N
exact :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (N₃ : Type v)
    [inst_6 : AddCommGroup N₃] [inst_7 : Module A N₃] [inst_8 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂) (g : N₂ →ₗ[A] N₃),
    Function.Injective ⇑f → Function.Surjective ⇑g → Function.Exact ⇑f ⇑g → motive N₁ → motive N₃ → motive N₂
equiv :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (f : N₁ ≃ₗ[A] N₂),
    motive N₁ → motive N₂
s : RelSeries {(N₁, N₂) | N₁.IsQuotientEquivQuotientPrime N₂}
hs1 : s.head = ⊥
hs2 : s.last = ⊤
⊢ ∀ (n : ℕ) (h : n < s.length + 1), motive ↥(s.toFun ⟨n, h⟩)

Tactic:
intro n h

Goal state after:
A : Type u
inst✝³ : CommRing A
inst✝² : IsNoetherianRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
x✝ : Module.Finite A M
motive : (N : Type v) → [inst : AddCommGroup N] → [inst_1 : Module A N] → [Module.Finite A N] → Prop
subsingleton :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] [Subsingleton N], motive N
quotient :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] (p : PrimeSpectrum A)
    (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N
exact :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (N₃ : Type v)
    [inst_6 : AddCommGroup N₃] [inst_7 : Module A N₃] [inst_8 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂) (g : N₂ →ₗ[A] N₃),
    Function.Injective ⇑f → Function.Surjective ⇑g → Function.Exact ⇑f ⇑g → motive N₁ → motive N₃ → motive N₂
equiv :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (f : N₁ ≃ₗ[A] N₂),
    motive N₁ → motive N₂
s : RelSeries {(N₁, N₂) | N₁.IsQuotientEquivQuotientPrime N₂}
hs1 : s.head = ⊥
hs2 : s.last = ⊤
n : ℕ
h : n < s.length + 1
⊢ motive ↥(s.toFun ⟨n, h⟩)
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
⊢ (LocalizedModule.map I.primeCompl) id ∈
    Submodule.localized₀ I.primeCompl (LocalizedModule.map I.primeCompl) ((llcomp R N M N) f).range

Tactic:
LocalizedModule.map_id

Goal state after:
R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
⊢ id ∈ Submodule.localized₀ I.primeCompl (LocalizedModule.map I.primeCompl) ((llcomp R N M N) f).range
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
hden0 : (algebraMap R (FractionRing R)) ↑I.den ≠ 0
u : (FractionRing R)ˣ := Units.mk0 ((algebraMap R (FractionRing R)) ↑I.den) hden0
hdenUnit : IsUnit (spanSingleton R⁰ ((algebraMap R (FractionRing R)) ↑I.den))
⊢ IsUnit ↑I.num ↔ IsUnit I

Tactic:
obtain ⟨c, hc⟩ := hdenUnit

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
hden0 : (algebraMap R (FractionRing R)) ↑I.den ≠ 0
u : (FractionRing R)ˣ := Units.mk0 ((algebraMap R (FractionRing R)) ↑I.den) hden0
c : (FractionalIdeal R⁰ (FractionRing R))ˣ
hc : ↑c = spanSingleton R⁰ ((algebraMap R (FractionRing R)) ↑I.den)
⊢ IsUnit ↑I.num ↔ IsUnit I
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: R : Type u_1
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Rₚ I) (Mₚ I)
inst✝ : FinitePresentation R M
⊢ Projective R M

Tactic:
apply Module.projective_of_localization_maximal

Goal state after:
R : Type u_1
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Rₚ I) (Mₚ I)
inst✝ : FinitePresentation R M
⊢ ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case zero
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
⊢ derivedSeries G' 0 ≤ map f (derivedSeries G 0)

Tactic:
exact (map_top_of_surjective f hf).ge

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✝⁹ : Flat R M
inst✝⁸ : Module.Finite R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
inst✝¹ : Module.Finite S N
inst✝ : Flat S N
p : PrimeSpectrum S
⊢ rankAtStalk (N ⊗[R] M) p = rankAtStalk N p * rankAtStalk M (comap (algebraMap R S) p)

Tactic:
simp [rankAtStalk_eq_of_equiv (AlgebraTensorModule.cancelBaseChange R S S N M).symm,
    rankAtStalk_tensorProduct, rankAtStalk_baseChange]

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✝³ : Flat R M
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
p : Ideal R
inst✝ : p.IsPrime
K : Type uR := FractionRing R
⊢ finrank p.ResidueField (p.Fiber M) = finrank R M

Tactic:
let Rp := Localization.AtPrime p

Goal state after:
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
p : Ideal R
inst✝ : p.IsPrime
K : Type uR := FractionRing R
Rp : Type uR := Localization.AtPrime p
⊢ finrank p.ResidueField (p.Fiber M) = finrank R M
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module.Invertible R M
f : N →ₗ[R] P
⊢ Function.Injective ⇑(LinearMap.rTensor M f) ∧ Function.Surjective ⇑(LinearMap.rTensor M f) ↔
    Function.Injective ⇑f ∧ Function.Surjective ⇑f

Tactic:
rTensor_injective_iff,

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module.Invertible R M
f : N →ₗ[R] P
⊢ Function.Injective ⇑f ∧ Function.Surjective ⇑(LinearMap.rTensor M f) ↔ Function.Injective ⇑f ∧ Function.Surjective ⇑f
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
⊢ Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = C h.leadingCoeff * (X - C β)

Tactic:
have h_sep : h.Separable := separable_gcd_right _ (.map (Algebra.IsSeparable.isSeparable F β))

Goal state after:
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
⊢ Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = C h.leadingCoeff * (X - C β)
Module: Mathlib.Combinatorics.Matroid.Basic

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

Tactic:
have h' : ∀ B, M₁.IsBase B ↔ M₂.IsBase B :=
    fun B ↦ ⟨fun hB ↦ (h hB.subset_ground).1 hB,
      fun hB ↦ (h <| hB.subset_ground.trans_eq hE.symm).2 hB⟩

Goal state after:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)
h' : ∀ (B : Set α), M₁.IsBase B ↔ M₂.IsBase B
⊢ M₁ = M₂
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
⊢ (emptyOn α)✶ = emptyOn α

Tactic:
by
  rw [← ground_eq_empty_iff]; rfl

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

Goal state before:
pp: α : Type u_1
I : Set α
⊢ uniqueBaseOn ∅ I = loopyOn I

Tactic:
by
  rw [← dual_inj, uniqueBaseOn_dual_eq, sdiff_empty, uniqueBaseOn_self, loopyOn_dual_eq]

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

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

Tactic:
have _ : Nonempty α := ⟨e⟩

Goal state after:
case inr
α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : ↑M.E ↪ β
e : α
he : e ∈ M.E
x✝¹ : Nonempty ↑M.E
x✝ : Nonempty α
⊢ ∃ M_1, range ⇑f = M_1.E ∧ ∀ (I : Set β), M_1.Indep I ↔ M.Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set β
⊢ (∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = ⇑f '' I₀) → M.Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I

Tactic:
rintro ⟨I, hI, rfl⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep (Subtype.val '' I)
⊢ M.Indep (Subtype.val '' ⇑f ⁻¹' ⇑f '' I) ∧ ∃ t, ⇑f '' t = ⇑f '' I
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) → M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

Tactic:
rintro ⟨I, hI, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set α
hI : M.Indep I
⊢ M.Indep (⇑f ⁻¹' ⇑f '' I) ∧ ⇑f '' I ⊆ range ⇑f
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) → M.Indep (⇑f.symm '' I)

Tactic:
rintro ⟨I, hI, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set α
hI : M.Indep I
⊢ M.Indep (⇑f.symm '' ⇑f '' I)
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
D : Set β
⊢ (∃ D₀, M.Dep D₀ ∧ D = ⇑f '' D₀) → M.Dep (⇑f.symm '' D)

Tactic:
rintro ⟨I, hI, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set α
hI : M.Dep I
⊢ M.Dep (⇑f.symm '' ⇑f '' I)
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
B : Set β
⊢ (∃ B₀, M.IsBase B₀ ∧ B = ⇑f '' B₀) → M.IsBase (⇑f.symm '' B)

Tactic:
rintro ⟨I, hI, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set α
hI : M.IsBase I
⊢ M.IsBase (⇑f.symm '' ⇑f '' I)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
⊢ M.Dep (insert e I) ∨ e ∈ I

Tactic:
exact .inl (hC.dep.superset hCs (insert_subset (hC.subset_ground heC) hI.subset_ground))

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

Goal state before:
pp: α : Type u_2
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hX : X ⊆ M.E
⊢ X ⊆ M.closure Y

Tactic:
rw [← closure_inter_ground]

Goal state after:
α : Type u_2
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hX : X ⊆ M.E
⊢ X ⊆ M.closure (Y ∩ M.E)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_3
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
⊢ ∀ (i : ↑X), ↑i ∈ C ↑i

Tactic:
simp only [Subtype.forall, ← singleton_subset_iff (s := C _)]
    exact fun e heX ↦ by simp [← hC.2 e heX]

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

Goal state before:
pp: α : Type u_2
X : Set α
e : α
M : Matroid α
heX : e ∈ X
h : e ∈ M.E
⊢ e ∈ M.closure X

Tactic:
rw [← closure_inter_ground]

Goal state after:
α : Type u_2
X : Set α
e : α
M : Matroid α
heX : e ∈ X
h : e ∈ M.E
⊢ e ∈ M.closure (X ∩ M.E)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ M.IsBasis ((⋂ i ∈ A, X i) ∩ I) (⋂ i ∈ A, X i)

Tactic:
by
  refine (hI.inter_left _).isBasis_of_subset_of_subset_closure inter_subset_left ?_
  simp_rw [← biInter_inter hA,
  closure_biInter_eq_biInter_closure_of_biUnion_indep hA (I := fun i ↦ (X i) ∩ I)
      (hI.subset (by simp)), subset_iInter_iff]
  exact fun i hiA ↦ (biInter_subset_of_mem hiA).trans (h i hiA).subset_closure

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι S), (aeval (⇑g ∘ x)) p = 0 → p = 0
hf : Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
p : MvPolynomial ι R
hp : (aeval x) p = 0
this : ↑g ((aeval x) p) = 0
⊢ (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) p) = 0

Tactic:
map_aeval,

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι S), (aeval (⇑g ∘ x)) p = 0 → p = 0
hf : Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
p : MvPolynomial ι R
hp : (aeval x) p = 0
this : (eval₂Hom ((↑g).comp (algebraMap R A)) fun i ↦ ↑g (x i)) p = 0
⊢ (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) p) = 0
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
hf : Surjective ⇑f
hg : Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : MvPolynomial ι R
hp : (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) q) = 0
⊢ ↑g ((aeval x) q) = 0

Tactic:
map_aeval,

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
hf : Surjective ⇑f
hg : Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : MvPolynomial ι R
hp : (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) q) = 0
⊢ (eval₂Hom ((↑g).comp (algebraMap R A)) fun i ↦ ↑g (x i)) q = 0
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
f : F[X]
irred : Irreducible f
inst✝ : CharZero F
⊢ (expand F (1 ^ 0)) f = f

Tactic:
rw [pow_zero, expand_one]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
R S : Set α
hSR : S ⊆ R
hR : R ⊆ M.E
⊢ M.closure S ∩ R = R ↔ R ⊆ M.closure S

Tactic:
inter_eq_right

Goal state after:
α : Type u_2
M : Matroid α
R S : Set α
hSR : S ⊆ R
hR : R ⊆ M.E
⊢ R ⊆ M.closure S ↔ R ⊆ M.closure S
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
A' : Type v
inst✝¹ : CommRing A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Injective ⇑f
⊢ trdeg R A ≤ trdeg R A'

Tactic:
rw [← (trdeg R A).lift_id, ← (trdeg R A').lift_id]; exact lift_trdeg_le_of_injective f hf

Goal state after:
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
η : Type u_3
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
t : Set A
ht : t ⊆ ⋃ i, s i
ft : t.Finite
I : Set η
fi : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
⊢ AlgebraicIndependent R Subtype.val

Tactic:
rcases hs.finset_le fi.toFinset with ⟨i, hi⟩

Goal state after:
R : Type u_2
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
η : Type u_3
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
t : Set A
ht : t ⊆ ⋃ i, s i
ft : t.Finite
I : Set η
fi : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
i : η
hi : ∀ i_1 ∈ fi.toFinset, s i_1 ⊆ s i
⊢ AlgebraicIndependent R Subtype.val
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
x✝ : α
⊢ x✝ ∈ fixedBy α g⁻¹ ↔ x✝ ∈ fixedBy α g

Tactic:
mem_fixedBy,

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

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

Tactic:
mem_fixedBy,

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

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g : G
⊢ g • a ∈ fixedBy α g ↔ a ∈ fixedBy α g

Tactic:
mem_fixedBy,

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g : G
⊢ g • g • a = g • a ↔ a ∈ fixedBy α g
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 : ℤ
⊢ a ∈ fixedBy α (g ^ j)

Tactic:
mem_fixedBy,

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

Tactic:
mem_fixedBy,

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 : α
⊢ h⁻¹ • a ∈ fixedBy α g ↔ a ∈ fixedBy α (h * g * h⁻¹)

Tactic:
mem_fixedBy,

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 α
s : Set α
g : G
⊢ s ∈ fixedBy (Set α) g ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s

Tactic:
mem_fixedBy,

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
⊢ g • s = s ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s