mathlib-initiative/mathlib-tactics huggingface dataset:
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ₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
this✝ : Nontrivial R
this :
  Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) =
    Cardinal.lift.{uM', max uM uR'} (Module.rank Rₛ (TensorProduct R Rₛ M))
⊢ Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ)) =
    Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM', uM} (Module.rank R M))

Tactic:
simp only [rank_tensorProduct, rank_self,
    Cardinal.lift_one, one_mul, Cardinal.lift_lift] at this ⊢

Goal state after:
R : Type u_1
M : Type uM
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
this✝ : Nontrivial R
this : Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uR' uM', uM} (Module.rank R M)
⊢ Cardinal.lift.{max uM uM' uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uM' uR', uM} (Module.rank R M)
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
⊢ ∃ x, I * (toPrincipalIdeal R (FractionRing R)) x = (FractionalIdeal.mk0 (FractionRing R)) ⟨integralRep ↑I, ⋯⟩

Tactic:
refine ⟨Units.mk0 (algebraMap R _ I.1.den) fd_ne_zero, ?_⟩

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: case inr
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
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
u : (FractionalIdeal R⁰ K)ˣ
hI : (↑(↑u ^ n)).IsPrincipal
⊢ (ClassGroup.mk K) u ^ n = 1

Tactic:
← map_pow,

Goal state after:
case inr
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
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
u : (FractionalIdeal R⁰ K)ˣ
hI : (↑(↑u ^ n)).IsPrincipal
⊢ (ClassGroup.mk K) (u ^ n) = 1
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
I : Ideal R
hI0 : ¬I = 0
hI : ClassGroup.mk0 ⟨I ^ n, ⋯⟩ = 1
⊢ ClassGroup.mk0 ⟨I, ⋯⟩ ^ n = 1

Tactic:
← map_pow,

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
I : Ideal R
hI0 : ¬I = 0
hI : ClassGroup.mk0 ⟨I ^ n, ⋯⟩ = 1
⊢ ClassGroup.mk0 (⟨I, ⋯⟩ ^ n) = 1
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x✝ : ∃ a, ↑I * ↑J = R ∙ a
a : R
ha : ↑I * ↑J = R ∙ 0
this : a = 0
⊢ False

Tactic:
Submodule.span_zero_singleton

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x✝ : ∃ a, ↑I * ↑J = R ∙ a
a : R
ha : ↑I * ↑J = ⊥
this : a = 0
⊢ False
Module: Mathlib.RingTheory.Localization.Free

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
S : Submonoid R
M' : Type u_1
inst✝¹⁰ : AddCommGroup M'
inst✝⁹ : Module R M'
f : M →ₗ[R] M'
inst✝⁸ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ M'
inst✝⁴ : IsScalarTower R Rₛ M'
inst✝³ : Nontrivial Rₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
inst✝ : Free Rₛ M'
⊢ ∃ r ∈ S,
    Free (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) ∧
      finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = finrank Rₛ M'

Tactic:
by
  let I := Module.Free.ChooseBasisIndex Rₛ M'
  let b : Basis I Rₛ M' := Module.Free.chooseBasis Rₛ M'
  have : Module.Finite Rₛ M' := Module.Finite.of_isLocalizedModule S (Rₚ := Rₛ) f
  obtain ⟨r, hr, b', _⟩ := Module.FinitePresentation.exists_basis_localizedModule_powers S f Rₛ b
  have := (show Localization (.powers r) →+* Rₛ from IsLocalization.map (M := .powers r) (T := S) _
    (RingHom.id _) (Submonoid.powers_le.mpr hr)).domain_nontrivial
  refine ⟨r, hr, .of_basis b', ?_⟩
  rw [Module.finrank_eq_nat_card_basis b, Module.finrank_eq_nat_card_basis b']

Goal state after:
Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsStablyFree R M
inst✝ : Module.Invertible R M
h✝¹ : Nontrivial R
N : Type u_1
w✝³ : AddCommGroup N
w✝² : Module R N
w✝¹ : Module.Finite R N
w✝ : Free R N
h✝ : Free R (M × N)
n : ℕ := finrank R N
hp : finrank R (M × N) = n + 1
e : R ≃ₗ[R] ↥(⋀[R]^(n + 1) (M × N)) := ⋯.some
bN : Basis (Fin n) R N := finBasis R N
f : R →ₗ[R] M := exteriorPower.cofactorToLeft bN ∘ₗ ↑e
x : M
⊢ f (e.symm ((exteriorPower.ιMulti R (n + 1)) (Fin.cons (x, 0) fun i ↦ (0, bN i)))) = x

Tactic:
by
      simp [f, exteriorPower.cofactorToLeft_ιMulti_cons]

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
Rp : Type uR := Localization.AtPrime p
Mp : Type (max uR uM) := LocalizedModule.AtPrime p M
⊢ finrank K (K ⊗[Rp] Mp) = finrank R M

Tactic:
(((LocalizedModule.equivTensorProduct p.primeCompl M).baseChange Rp K Mp _)).finrank_eq,

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
Mp : Type (max uR uM) := LocalizedModule.AtPrime p M
⊢ finrank K (K ⊗[Rp] (Localization p.primeCompl ⊗[R] M)) = finrank R M
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)
⊢ β ∈ F⟮γ⟯

Tactic:
let h := EuclideanDomain.gcd ((f.map ιFE).comp (C γ - C (ιFE c) * X)) (g.map ιFE)

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)
⊢ β ∈ F⟮γ⟯
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
⊢ Fintype.card ↑((minpoly F α).rootSet A) = finrank F E ↔ Function.Injective fun φ ↦ φ α

Tactic:
← toFinset_card,

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
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
⊢ ((minpoly F α).rootSet A).toFinset.card = finrank F E ↔ Function.Injective fun φ ↦ φ α
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.E = ∅ ↔ M = emptyOn α

Tactic:
by
  simp only [emptyOn, ext_iff_indep, iff_self_and]
  exact fun h ↦ by simp [h, subset_empty_iff]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
E B I X R J : Set α
⊢ (uniqueBaseOn I E).Finitary

Tactic:
refine ⟨fun K hK ↦ ?_⟩
  simp only [uniqueBaseOn_indep_iff'] at hK ⊢
  exact fun e heK ↦ singleton_subset_iff.1 <| hK _ (by simpa) (by simp)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
hB : (N ↾ range f).IsBase (f '' I)
h_im : f '' I = f '' I'
⊢ I = I'

Tactic:
hI'inj.image_eq_image_iff hII'.subset Subset.rfl

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
hB : (N ↾ range f).IsBase (f '' I)
h_im : I = I'
⊢ I = I'
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
⊢ ∃ x ∈ B \ I, Indep (insert x I)

Tactic:
suffices hcard : I.encard < B.encard by
        obtain ⟨e, heB, heI, hi⟩ := indep_aug hI hBmax.prop hcard
        exact ⟨e, ⟨heB, heI⟩, hi⟩

Goal state after:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
⊢ I.encard < B.encard
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ : Set α
M : Matroid α
N : Matroid β
E B I : Set α
inst✝ : N.Finitary
⊢ (N.comapOn E f).Finitary

Tactic:
comapOn

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ : Set α
M : Matroid α
N : Matroid β
E B I : Set α
inst✝ : N.Finitary
⊢ (N.comap f ↾ E).Finitary
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ : Set α
M : Matroid α
N : Matroid β
E B I : Set α
inst✝ : N.RankFinite
⊢ (N.comapOn E f).RankFinite

Tactic:
comapOn

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ : Set α
M : Matroid α
N : Matroid β
E B I : Set α
inst✝ : N.RankFinite
⊢ (N.comap f ↾ E).RankFinite
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
J : Set α
hJ : M.Indep J
hins : insert (f e) (f '' I) = f '' J
⊢ False

Tactic:
rw [← image_insert_eq, hf.image_eq_image_iff hss hJ.subset_ground] at hins

Goal state after:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
J : Set α
hJ : M.Indep J
hins : insert e I = J
⊢ False
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Set α
f : α → β
hf : InjOn f (freeOn E).E
⊢ (freeOn E).map f hf = freeOn (f '' E)

Tactic:
rw [← dual_inj]; simp

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

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

Tactic:
simp_rw [indep_iff_forall_subset_not_isCircuit hI, h',
    indep_iff_forall_subset_not_isCircuit (hI.trans_eq hE)]

Goal state after:
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ι : IsEmpty ι
⊢ M.IsCircuit J

Tactic:
simpa [range_eq_empty] using hJx

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
⊢ M.IsCircuit {e, f}

Tactic:
rw [isCircuit_iff_dep_forall_sdiff_singleton_indep, dep_iff, insert_subset_iff,
      and_iff_right he.mem_ground, singleton_subset_iff, and_iff_left hf.mem_ground]

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
⊢ ¬M.Indep {e, f} ∧ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
h : M.eRk X < M.eRk Y
hz : ¬Y ∩ M.E ⊆ M.closure X
e : α
heX : e ∉ M.closure X
heZ : e ∈ Y
heE : e ∈ M.E
⊢ ∃ y ∈ Y \ X, M.eRk (insert y X) = M.eRk X + 1

Tactic:
refine ⟨e, ⟨heZ, fun heX' ↦ heX (mem_closure_of_mem' _ heX')⟩, eRk_insert_eq_add_one ⟨heE, heX⟩⟩

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

Goal state before:
pp: case neg
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X
hX : ¬M.IsRkFinite X
⊢ M.eRk X = M.eRk Y

Tactic:
rw [eRk_eq_top_iff.2 hX, eRk_eq_top_iff.2 (mt (fun h ↦ h.subset hXY) hX)]

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, Xs i) = M.closure (⋃ i ∈ A, Ys i)

Tactic:
by
  rw [← closure_biUnion_closure_eq_closure_biUnion, iUnion₂_congr h,
    closure_biUnion_closure_eq_closure_biUnion]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ M.closure (X \ K) \ K = M.closure (X \ K)

Tactic:
sdiff_eq_self_iff_disjoint,

Goal state after:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ Disjoint K (M.closure (X \ K))
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: case refine_2
α : Type u
β : Type v
M : Matroid β
f : α → β
X I₀ : Set α
hI₀X : I₀ ⊆ X
hfI₀ : InjOn f I₀
hIX : M.IsBasis' (f '' I₀) (f '' X)
⊢ lift.{u, v} #↑(f '' I₀) ≤ lift.{v, u} (⨆ B, #↑↑B)

Tactic:
mk_image_eq_of_injOn_lift _ _ hfI₀,

Goal state after:
case refine_2
α : Type u
β : Type v
M : Matroid β
f : α → β
X I₀ : Set α
hI₀X : I₀ ⊆ X
hfI₀ : InjOn f I₀
hIX : M.IsBasis' (f '' I₀) (f '' X)
⊢ lift.{v, u} #↑I₀ ≤ lift.{v, u} (⨆ B, #↑↑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:
rw [fundCocircuit, fundCircuit_eq_of_mem (by simp [hfE, hfB])] at he

Goal state after:
case inr.inr.inl
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ {f}
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∉ B
⊢ f ∈ M.fundCircuit e B
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
a : A
⊢ (AlgebraicIndependent R fun o ↦ o.elim a x) ↔ Transcendental (↥(adjoin R (range x))) a

Tactic:
rw [algebraicIndependent_iff_injective_aeval, transcendental_iff_injective,
    ← AlgHom.coe_toRingHom, ← hx.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin,
    RingHom.coe_comp]

Goal state after:
ι : 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
a : A
⊢ Injective (⇑↑(Polynomial.aeval a) ∘ ⇑hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom) ↔
    Injective ⇑(Polynomial.aeval a)
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

pp: F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
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
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:
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
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
hm : m ≤ m'
⊢ g.natDegree = g'.natDegree
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
A : Type (max u_1 u) := MvPolynomial ι R
⊢ Algebra.IsAlgebraic (↥⊤) (MvPolynomial ι R)

Tactic:
have := Algebra.isIntegral_of_surjective (R := (⊤ : Subalgebra R A)) (B := A) (⟨⟨·, ⟨⟩⟩, rfl⟩)

Goal state after:
ι : Type u
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
A : Type (max u_1 u) := MvPolynomial ι R
this : Algebra.IsIntegral (↥⊤) A
⊢ Algebra.IsAlgebraic (↥⊤) (MvPolynomial ι R)
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 t : Set A
⊢ Maximal (fun A_1 ↦ (matroid R A).Indep A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔
    AlgebraicIndepOn R _root_.id s ∧ s ⊆ t ∧ ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a

Tactic:
maximal_iff_forall_insert fun s t h hst ↦ ⟨h.1.subset hst, hst.trans h.2⟩

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 t : Set A
⊢ (((matroid R A).Indep s ∧ s ⊆ t) ∧ ∀ x ∉ s, ¬((matroid R A).Indep (insert x s) ∧ insert x s ⊆ t)) ∧
      t ⊆ (matroid R A).E ↔
    AlgebraicIndepOn R _root_.id s ∧ s ⊆ t ∧ ∀ a ∈ t, IsAlgebraic (↥(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✝ : Subsingleton A
s : Set A
⊢ ⋂₀ {F | s ∩ univ ⊆ F} = s

Tactic:
inter_univ

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✝ : Subsingleton A
s : Set A
⊢ ⋂₀ {F | s ⊆ F} = s
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: E : Type v
inst✝¹ : Field E
K : Type w
inst✝ : Field K
f : E[X]
i : E →+* K
⊢ (map i f).natSepDegree = f.natSepDegree

Tactic:
classical
  let _ := i.toAlgebra
  simp_rw [show i = algebraMap E K by rfl, natSepDegree_eq_of_isAlgClosed (AlgebraicClosure K),
    aroots_def, map_map, ← IsScalarTower.algebraMap_eq]

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ insepDegree F F = 1

Tactic:
rw [insepDegree, Subsingleton.elim (separableClosure F F) ⊤, IntermediateField.rank_top]

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

Goal state before:
pp: case right
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K L : IntermediateField F E
inst✝¹ : IsGalois F ↥K
inst✝ : FiniteDimensional F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ : (Polynomial.map (algebraMap F ↥K) T).Splits ∧ adjoin F (Subtype.val '' T.rootSet ↥K) = lift ⊤
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
h' : T'.rootSet E = T.rootSet E
⊢ adjoin (↥L) (T'.rootSet E) = ⊤

Tactic:
← coe_val,

Goal state after:
case right
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K L : IntermediateField F E
inst✝¹ : IsGalois F ↥K
inst✝ : FiniteDimensional F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ : (Polynomial.map (algebraMap F ↥K) T).Splits ∧ adjoin F (⇑K.val '' T.rootSet ↥K) = lift ⊤
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
h' : T'.rootSet E = T.rootSet E
⊢ adjoin (↥L) (T'.rootSet E) = ⊤
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_3
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0
⊢ eval₂ σ y (minpolyDiv R x) = if σ x = y then σ ((aeval x) (derivative (minpoly R x))) else 0

Tactic:
split_ifs with h
  · rw [← h, eval₂_hom, eval_minpolyDiv_self]
  · rw [← eval₂_map, ← minpolyDiv_spec] at hy
    simpa [sub_eq_zero, Ne.symm h] using hy

Goal state after: