mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Colon

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hI : I ∈ (N.colon {x}).minimalPrimes
hx : x ∈ N
⊢ ∃ x', I = N.colon {x'}

pp: case neg
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hI : I ∈ (N.colon {x}).minimalPrimes
hx : x ∉ N
⊢ ∃ x', I = N.colon {x'}

Tactic:
· simp [show (colon N {x}) = ⊤ by simpa, Ideal.minimalPrimes_top] at hI

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hI : I ∈ (N.colon {x}).minimalPrimes
hx : x ∉ N
⊢ ∃ x', I = N.colon {x'}
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : g * z ∈ span {g}
⊢ b * (g * z) ∈ span {x}

Tactic:
mem_span_singleton,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : g * z ∈ span {g}
⊢ x ∣ b * (g * z)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
J : Ideal R := (↑I).num
⊢ (↑↑I).IsPrincipal

Tactic:
have hJunit : IsUnit (J : FractionalIdeal R⁰ (FractionRing R)) :=
    FractionalIdeal.isUnit_num.mpr ⟨I, rfl⟩

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
J : Ideal R := (↑I).num
hJunit : IsUnit ↑J
⊢ (↑↑I).IsPrincipal
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
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
      ((Units.map ↑(canonicalEquiv R⁰ K' (FractionRing R))) ((Units.map ↑(canonicalEquiv R⁰ K K')) I)) =
    (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
      ((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I)

Tactic:
← MonoidHom.comp_apply (Units.map _),

Goal state after:
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
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
      (((Units.map ↑(canonicalEquiv R⁰ K' (FractionRing R))).comp (Units.map ↑(canonicalEquiv R⁰ K K'))) I) =
    (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
      ((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I)
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: case mp
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
this :
  id ∈
    ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f✝)).range
f : LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N
⊢ f ∈ Submodule.localized₀ I.primeCompl (LocalizedModule.map I.primeCompl) ((llcomp R N M N) f✝).range →
    f ∈
      ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
            (LocalizedModule I.primeCompl N))
          ((LocalizedModule.map I.primeCompl) f✝)).range

Tactic:
intro hf

Goal state after:
case mp
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
this :
  id ∈
    ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f✝)).range
f : LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N
hf : f ∈ Submodule.localized₀ I.primeCompl (LocalizedModule.map I.primeCompl) ((llcomp R N M N) f✝).range
⊢ f ∈
    ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f✝)).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
x : K
hX : spanSingleton R⁰ x = ↑X
⊢ x ≠ 0

Tactic:
rintro rfl; simp [X.ne_zero.symm] at hX

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_5
inst✝ : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h : ∀ (x : X), f x = 0 ↔ g x = 0
⊢ f = g

Tactic:
ext1 x

Goal state after:
X : Type u_5
inst✝ : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h : ∀ (x : X), f x = 0 ↔ g x = 0
x : X
⊢ f x = g x
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module S M'
inst✝ : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
x : ι →₀ M
⊢ (LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ ⋯.equiv ≪≫ₗ
        (finsuppLEquivDirectSum S M' ι).symm)
      (1 ⊗ₜ[R] x) =
    (Finsupp.mapRange.linearMap ε) x

Tactic:
LinearEquiv.trans_apply,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module S M'
inst✝ : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
x : ι →₀ M
⊢ (finsuppLEquivDirectSum S M' ι).symm
      ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ ⋯.equiv) (1 ⊗ₜ[R] x)) =
    (Finsupp.mapRange.linearMap ε) x
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
inst✝³ : p.IsPrime
inst✝² : IsLocalRing R
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom (algebraMap R S)
eSp : ResidueField R ⊗[R] S ≃ₐ[R] S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R) :=
  (Algebra.TensorProduct.comm R (ResidueField R) S).trans
    (AlgEquiv.restrictScalars R (quotIdealMapEquivTensorQuot S (maximalIdeal R)).symm)
⊢ Ideal.map (algebraMap R S) (maximalIdeal R) ≠ ⊤

Tactic:
exact ((((local_hom_TFAE (algebraMap R S)).out 0 2 rfl rfl).mp inferInstance).trans_lt
      (inferInstance : (maximalIdeal S).IsMaximal).lt_top).ne

Goal state after:
Module: Mathlib.GroupTheory.Perm.ViaEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
e : Perm α
ι : α ↪ β
x : α
⊢ (e.viaEmbedding ι) (ι x) = ι (e x)

Tactic:
exact extendDomain_apply_image e (ofInjective ι.1 ι.2) x

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
p✝ : Ideal R✝
inst✝³ : p✝.IsPrime
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
H : Topology.IsEmbedding ⇑(preimageOrderIsoFiber R S p).symm := preimageHomeomorphFiber._proof_1 R S p
⊢ (preimageOrderIsoFiber R S p).toFun = ⇑(H.toHomeomorphOfSurjective ⋯).symm

Tactic:
ext1 x

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
p✝ : Ideal R✝
inst✝³ : p✝.IsPrime
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
H : Topology.IsEmbedding ⇑(preimageOrderIsoFiber R S p).symm := preimageHomeomorphFiber._proof_1 R S p
x : ↑(comap (algebraMap R S) ⁻¹' {p})
⊢ (preimageOrderIsoFiber R S p).toFun x = (H.toHomeomorphOfSurjective ⋯).symm x
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: case inl
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
hFEp : IsSplittingField F E 0
⊢ Normal F E

Tactic:
have := hFEp.adjoin_rootSet

Goal state after:
case inl
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
hFEp : IsSplittingField F E 0
this : Algebra.adjoin F (rootSet 0 E) = ⊤
⊢ Normal F E
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
⊢ normalClosure F (↥K) L ≤ K ↔ ∀ (σ : Gal(L/F)), map (↑σ) K ≤ K

Tactic:
normalClosure_def'',

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
⊢ ⨆ f, map (↑f) K ≤ K ↔ ∀ (σ : Gal(L/F)), 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
σ✝ : L →ₐ[F] L
σ : Gal(L/F)
⊢ normalClosure F (↥(map (↑σ) K)) L = normalClosure F (↥K) L

Tactic:
normalClosure_def'',

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
σ✝ : L →ₐ[F] L
σ : Gal(L/F)
⊢ ⨆ f, map (↑f) (map (↑σ) K) = ⨆ f, map (↑f) K
Module: Mathlib.RingTheory.AlgebraicIndependent.Defs

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
f : ι' → ι
hf : Injective f
p q : MvPolynomial ι' R
⊢ (aeval (x ∘ f)) p = (aeval (x ∘ f)) q → p = q

Tactic:
simpa [aeval_rename, (rename_injective f hf).eq_iff] using @hx (rename f p) (rename f q)

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := ⋯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ F⟮α + x • β⟯ ≤ F⟮α, β⟯

Tactic:
rw [adjoin_simple_le_iff]
    have α_in_Fαβ : α ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert α {β})
    have β_in_Fαβ : β ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert_of_mem α rfl)
    exact F⟮α, β⟯.add_mem α_in_Fαβ (F⟮α, β⟯.smul_mem β_in_Fαβ)

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hmax : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I
hX : X ⊆ M.E
⊢ X ⊆ M.E

Tactic:
aesop_mat

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_3
E : Type u_4
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
⊢ F⟮α⟯ = ⊤ ↔ (minpoly F α).degree = ↑(finrank F E)

Tactic:
rw [degree_eq_iff_natDegree_eq, primitive_element_iff_minpoly_natDegree_eq]

Goal state after:
F : Type u_3
E : Type u_4
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
⊢ minpoly F α ≠ 0
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), (Polynomial.map (algebraMap F A) (minpoly F x)).Splits
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
this : Algebra (↥F⟮α⟯) A := (φ.comp F⟮α⟯.val).toAlgebra
⊢ ∃ x, ∀ (y : E →ₐ[↥F⟮α⟯] A), y = x

Tactic:
exact ⟨{ __ := φ, commutes' := fun _ ↦ rfl }, fun ψ ↦ AlgHom.restrictScalars_injective F <|
      Eq.symm <| h _ (ψ.commutes <| AdjoinSimple.gen F α).symm⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : IsEmpty α
M : Matroid α
⊢ M = emptyOn α

Tactic:
rw [← ground_eq_empty_iff]
  exact M.E.eq_empty_of_isEmpty

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

Goal state before:
pp: case refine_1
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ I' ⊆ X \ B' ∩ M.E

Tactic:
rw [subset_inter_iff, and_iff_left hI'E, subset_sdiff, and_iff_right hI'X]

Goal state after:
case refine_1
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ Disjoint I' B'
Module: Mathlib.Combinatorics.Matroid.Constructions

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

Tactic:
sdiff_empty,

Goal state after:
α : Type u_1
I : Set α
⊢ uniqueBaseOn I I = (loopyOn I)✶
Module: Mathlib.Combinatorics.Matroid.Rank.Finite

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
h : M.IsRkFinite X
hXY : Y ⊆ X
⊢ M.IsRkFinite Y

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' Y

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
h : M.IsRkFinite X
hXY : Y ⊆ X
I : Set α
hI : M.IsBasis' I Y
⊢ M.IsRkFinite Y
Module: Mathlib.Combinatorics.Matroid.Map

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

Tactic:
simp [range_eq_empty f, subset_empty_iff]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
⊢ M.Dep {e} ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B

Tactic:
simp only [dep_iff, singleton_subset_iff, mem_sdiff, forall_and]

Goal state after:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
⊢ ¬M.Indep {e} ∧ e ∈ M.E ↔ (∀ (x : Set α), M.IsBase x → e ∈ M.E) ∧ ∀ (x : Set α), M.IsBase x → e ∉ x
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ M.eRk B = M.eRank

Tactic:
hB.indep.eRk_eq_encard,

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ B.encard = M.eRank
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
h : ¬M.IsNonloop e
⊢ M.IsLoop e

Tactic:
by
  rwa [isNonloop_iff, and_iff_left he, not_not] at h

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
⊢ C ⊆ M.closure (C \ {e})

Tactic:
hC.closure_sdiff_singleton_eq

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
⊢ C ⊆ M.closure C
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.eRk I = I.encard
J : Set α
hJ : M.IsBasis' J I
⊢ I.encard ≤ J.encard

Tactic:
rw [← h, ← hJ.eRk_eq_encard]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
⊢ M.E ⊆ M.closure X ↔ M.closure X = M.E

Tactic:
by
  simp [M.closure_subset_ground X, subset_antisymm_iff]

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

Goal state before:
pp: case refine_4
α : 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}
e : α
heX : e ∈ X
f : α
hfX : f ∈ X
hef : e ∈ C f
⊢ e = f

Tactic:
simpa [hC.2 f hfX] using subset_inter (singleton_subset_iff.2 hef) (singleton_subset_iff.2 heX)

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e : α
he : e ∈ M.closure X
⊢ M.closure (insert e X) = M.closure X

Tactic:
rw [← closure_insert_closure_eq_closure_insert, insert_eq_of_mem he, closure_closure]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ ¬M.IsBase (M.E \ ∅) ↔ ∃ C, M.IsCircuit C

Tactic:
sdiff_empty,

Goal state after:
α : Type u_1
M : Matroid α
⊢ ¬M.IsBase M.E ↔ ∃ C, M.IsCircuit C
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
X : Set α
he : e ∉ M.E
⊢ M.fundCocircuit e X = {e}

Tactic:
fundCocircuit,

Goal state after:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : e ∉ M.E
⊢ M✶.fundCircuit e (M✶.E \ X) = {e}
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case pos
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∈ M.E
⊢ M.fundCocircuit e X = {e}

Tactic:
fundCocircuit,

Goal state after:
case pos
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∈ M.E
⊢ M✶.fundCircuit e (M✶.E \ X) = {e}
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : ¬IsAlgebraic (↥(supported R s)) ((Polynomial.aeval (X i)) f)
⊢ i ∉ s

Tactic:
contrapose h

Goal state after:
case refine_1
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : i ∈ s
⊢ IsAlgebraic (↥(supported R s)) ((Polynomial.aeval (X i)) f)
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

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

Tactic:
refine h.restrictScalars fun _ _ heq ↦ MvPolynomial.C_injective σ R ?_

Goal state after:
case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
x✝¹ x✝ : R
heq : (algebraMap R ↥(supported R s)) x✝¹ = (algebraMap R ↥(supported R s)) x✝
⊢ C x✝¹ = C x✝
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inr.inl
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∉ M.E
⊢ f ∈ M.fundCircuit e B

Tactic:
fundCocircuit,

Goal state after:
case inr.inl
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M✶.fundCircuit f (M✶.E \ B)
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∉ M.E
⊢ f ∈ M.fundCircuit e B
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inr.inr.inl
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∉ B
⊢ f ∈ M.fundCircuit e B

Tactic:
fundCocircuit,

Goal state after:
case inr.inr.inl
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M✶.fundCircuit f (M✶.E \ B)
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∉ B
⊢ f ∈ M.fundCircuit e B
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inr.inr.inr
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
⊢ f ∈ M.fundCircuit e B

Tactic:
fundCocircuit,

Goal state after:
case inr.inr.inr
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M✶.fundCircuit f (M✶.E \ B)
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
⊢ f ∈ M.fundCircuit e B
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
⊢ M.IsBasis' I X ↔ M.IsBasis I (M.closure X) ∧ I ⊆ X

Tactic:
rw [← closure_inter_ground, isBasis'_iff_isBasis_inter_ground]

Goal state after:
α : Type u_2
M : Matroid α
X I : Set α
⊢ M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I (M.closure (X ∩ M.E)) ∧ I ⊆ X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case refine_1
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
heE : e ∉ M.E
⊢ M.closure ((M.E ∩ I) \ ∅) = M.closure I

Tactic:
sdiff_empty,

Goal state after:
case refine_1
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
heE : e ∉ M.E
⊢ M.closure (M.E ∩ I) = M.closure I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
⊢ M.Indep (I ∪ J) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J)

Tactic:
by
  simp_rw [union_comm I J, hJ.union_indep_iff_forall_notMem_closure_right hI, union_comm]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s : Set ι
i : ι
⊢ Transcendental (↥(adjoin R (x '' s))) (x i) ↔ i ∉ s

Tactic:
by
  rw [← Set.disjoint_singleton_right]
  convert! ← hx.adjoin_iff_disjoint (t := { i })
  rw [algebraicIndependent_singleton_iff ⟨i, rfl⟩]

Goal state after: