mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: case mpr.map_unit
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
g : N →ₗ[R] M
s : ↥I.primeCompl
⊢ ∀ (x : ↥I.primeCompl), IsUnit ((algebraMap R (Module.End R (LocalizedModule I.primeCompl N))) ↑x)

pp: case mpr.h
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
g : N →ₗ[R] M
s : ↥I.primeCompl
⊢ ↑R ((LocalizedModule.map I.primeCompl) (f ∘ₗ g)) ∘ₗ LocalizedModule.mkLinearMap I.primeCompl N =
    ↑R
        (((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
              (LocalizedModule I.primeCompl N))
            ((LocalizedModule.map I.primeCompl) f))
          ((LocalizedModule.map I.primeCompl) g)) ∘ₗ
      LocalizedModule.mkLinearMap I.primeCompl N

Tactic:
· exact IsLocalizedModule.map_units (LocalizedModule.mkLinearMap I.primeCompl N)

Goal state after:
case mpr.h
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
g : N →ₗ[R] M
s : ↥I.primeCompl
⊢ ↑R ((LocalizedModule.map I.primeCompl) (f ∘ₗ g)) ∘ₗ LocalizedModule.mkLinearMap I.primeCompl N =
    ↑R
        (((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
              (LocalizedModule I.primeCompl N))
            ((LocalizedModule.map I.primeCompl) f))
          ((LocalizedModule.map I.primeCompl) g)) ∘ₗ
      LocalizedModule.mkLinearMap I.primeCompl N
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
h : IsEmpty X
⊢ ∃ y, f = Function.const X y

Tactic:
exact ⟨Classical.arbitrary Y, funext <| h.elim⟩

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 : ⇑f ⁻¹' {0} = ⇑g ⁻¹' {0}
⊢ f = g

Tactic:
simp only [Set.ext_iff, mem_singleton_iff, mem_preimage] at h
  ext1 x
  exact Fin.fin_two_eq_of_eq_zero_iff (h x)

Goal state after:
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
M : Type u_3
N : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : AddCommMonoid N'
inst✝⁵ : Module R M'
inst✝⁴ : Module R N'
inst✝³ : Module S M'
inst✝² : Module S N'
inst✝¹ : IsScalarTower R S M'
inst✝ : IsScalarTower R S N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
hf : IsBaseChange S f
hg : IsBaseChange S g
⊢ IsBaseChange S (f.prodMap g)

Tactic:
apply of_equiv (prodRight R _ S M N ≪≫ₗ hf.equiv.prodCongr hg.equiv)
  intro p
  simp [equiv_tmul]

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
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
⊢ p ∈ freeLocus (Localization S) (LocalizedModule S M) ↔ comap (algebraMap R (Localization S)) p ∈ freeLocus R M

Tactic:
let : Algebra (Localization S) Rₚ :=
    IsLocalization.localizationAlgebraOfSubmonoidLe _ _ S p'.primeCompl hp'

Goal state after:
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
⊢ p ∈ freeLocus (Localization S) (LocalizedModule S M) ↔ comap (algebraMap R (Localization S)) p ∈ freeLocus R M
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:
← freeLocus_eq_univ_iff,

Goal state after:
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 ↔ freeLocus (Localization.Away f) (LocalizedModule.Away f M) = Set.univ
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case zero
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
⊢ ∀ (a b : G), a * b = b * a

pp: case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
n✝ : ℕ
hn : derivedSeries G (n✝ + 1) = ⊥
⊢ ∀ (a b : G), a * b = b * a

Tactic:
· intro a b
      refine (mem_bot.1 ?_).trans (mem_bot.1 ?_).symm <;>
        · rw [← hn]
          exact mem_top _

Goal state after:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
n✝ : ℕ
hn : derivedSeries G (n✝ + 1) = ⊥
⊢ ∀ (a b : G), a * b = b * a
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
⊢ Function.Bijective ⇑(toModuleEnd R M)

Tactic:
by
  have : toModuleEnd R (S := R) M = (lid R M).conj ∘ rTensorEquiv R R
      (comm .. ≪≫ₗ linearEquiv R M) ∘ RingEquiv.moduleEndSelf R ∘ MulOpposite.opEquiv := by
    ext; simp [LinearEquiv.conj, liftAux]
  simpa [this] using MulOpposite.opEquiv.bijective

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
⊢ ∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c

Tactic:
let sg := (g.map ϕ).roots

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
⊢ ∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case refine_2
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
S : Finset (Dual R M × M)
hS : (linearEquiv R M).symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
f : Dual R M
m : M
left✝ : (f, m) ∈ S
hr : (f, m).1 (f, m).2 ∈ Finset.image (fun i ↦ i.1 i.2) S
⊢ Free (Localization.Away ((f, m).1 (f, m).2)) (LocalizedModule.Away ((f, m).1 (f, m).2) M)

Tactic:
let f' : Dual (Localization.Away (f m)) (LocalizedModule.Away (f m) M) :=
    .extendScalarsOfIsLocalization (.powers (f m)) _ <| IsLocalizedModule.map
      (.powers (f m)) (LocalizedModule.mkLinearMap _ M) (Algebra.linearMap R _) f

Goal state after:
case refine_2
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
S : Finset (Dual R M × M)
hS : (linearEquiv R M).symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
f : Dual R M
m : M
left✝ : (f, m) ∈ S
hr : (f, m).1 (f, m).2 ∈ Finset.image (fun i ↦ i.1 i.2) S
f' : Dual (Localization.Away (f m)) (LocalizedModule.Away (f m) M) :=
  LinearMap.extendScalarsOfIsLocalization (Submonoid.powers (f m)) (Localization.Away (f m))
    ((IsLocalizedModule.map (Submonoid.powers (f m)) (LocalizedModule.mkLinearMap (Submonoid.powers (f m)) M)
        (Algebra.linearMap R (Localization.Away (f m))))
      f)
⊢ Free (Localization.Away ((f, m).1 (f, m).2)) (LocalizedModule.Away ((f, m).1 (f, m).2) 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)
h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
x : (Polynomial.map ιFE g).SplittingField
hx : eval₂ ιEE' x h = 0
f_root : eval₂ ιEE' x ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) = 0
⊢ ιEE' γ - ιEE' (ιFE c) * x ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots

Tactic:
eval₂_comp,

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
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
x : (Polynomial.map ιFE g).SplittingField
hx : eval₂ ιEE' x h = 0
f_root : eval₂ ιEE' (eval₂ ιEE' x (C γ - C (ιFE c) * X)) (Polynomial.map ιFE f) = 0
⊢ ιEE' γ - ιEE' (ιFE c) * x ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B B₁ : Set α
hB : M.IsBase B
h : B.Infinite
hB₁ : M.IsBase B₁
⊢ B₁.Infinite

Tactic:
contrapose! h

Goal state after:
α : Type u_1
M : Matroid α
B B₁ : Set α
hB : M.IsBase B
hB₁ : M.IsBase B₁
h : B₁.Finite
⊢ B.Finite
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ ∃ J, M.IsBasis' J X ∧ I ⊆ J

Tactic:
by
  simp_rw [isBasis'_iff_isBasis_inter_ground]
  exact hI.subset_isBasis_of_subset (subset_inter hIX hI.subset_ground)

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
⊢ ((M.Indep I ∧ I ⊆ X) ∧ ∀ x ∉ I, ¬(M.Indep (insert x I) ∧ insert x I ⊆ X)) ∧ X ⊆ M.E ↔ ∀ e ∈ X \ I, M.Dep (insert e I)

Tactic:
simp only [hI, hIX, and_self, insert_subset_iff, and_true, not_and, true_and, mem_sdiff, and_imp,
    Dep, hI.subset_ground]

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ (∀ x ∉ I, M.Indep (insert x I) → x ∉ X) ∧ X ⊆ M.E ↔ ∀ e ∈ X, e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
A : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
⊢ ⊤ * submoduleAlgebra e = ⊤

Tactic:
rw [← Submodule.mulMap_range]

Goal state after:
R : Type u
M : Type v
A : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
⊢ (⊤.mulMap (submoduleAlgebra e)).range = ⊤
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M ↾ ∅ = emptyOn α

Tactic:
simp [← ground_eq_empty_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ (emptyOn β).comap f = emptyOn α

Tactic:
simp [← ground_eq_empty_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ f '' B ⊆ N.E

Tactic:
exact (h.mapsTo.mono_left (show B ⊆ E by simpa)).image_subset

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ (emptyOn α).map f ⋯ = emptyOn β

Tactic:
simp [← ground_eq_empty_iff]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set ↑M.E
⊢ M.IsBasis' (Subtype.val '' B) M.E ↔ M.IsBase (Subtype.val '' B)

Tactic:
isBasis'_iff_isBasis,

Goal state after:
α : Type u_1
M : Matroid α
B : Set ↑M.E
⊢ M.IsBasis (Subtype.val '' B) M.E ↔ M.IsBase (Subtype.val '' B)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).loops = M.loops ∩ R

Tactic:
restrict_loops_eq',

Goal state after:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ M.loops ∩ R ∪ R \ M.E = M.loops ∩ R
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.loops
⊢ (M ↾ X).loops = X ∧ (M ↾ X).E = X

Tactic:
restrict_loops_eq',

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.loops
⊢ M.loops ∩ X ∪ X \ M.E = X ∧ (M ↾ X).E = X
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ Monotone M.eRk

Tactic:
by
  rintro X Y (hXY : X ⊆ Y)
  obtain ⟨I, hI⟩ := M.exists_isBasis' X
  obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_isBasis'_of_subset (hI.subset.trans hXY)
  rw [hI.eRk_eq_encard, hJ.eRk_eq_encard]
  exact encard_mono hIJ

Goal state after:
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
⊢ ¬Y ∩ M.E ⊆ M.closure X

Tactic:
contrapose! h

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
h : Y ∩ M.E ⊆ M.closure X
⊢ M.eRk Y ≤ M.eRk X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
F : ↑(Iic M.E)
⊢ M.subtypeClosure.IsClosed F ↔ M.IsFlat ↑F

Tactic:
simp [subtypeClosure]

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

Goal state before:
pp: α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y : Set α
⊢ M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y

Tactic:
by
  obtain ⟨Ii, hIi⟩ := M.exists_isBasis' (X ∩ Y)
  obtain ⟨IX, hIX, hIX'⟩ :=
    hIi.indep.subset_isBasis'_of_subset (hIi.subset.trans inter_subset_left)
  obtain ⟨IY, hIY, hIY'⟩ :=
    hIi.indep.subset_isBasis'_of_subset (hIi.subset.trans inter_subset_right)
  rw [← cRk_union_closure_eq, ← hIX.closure_eq_closure, ← hIY.closure_eq_closure,
    cRk_union_closure_eq, ← hIi.cardinalMk_eq_cRk, ← hIX.cardinalMk_eq_cRk,
    ← hIY.cardinalMk_eq_cRk, ← mk_union_add_mk_inter, add_comm]
  exact add_le_add (M.cRk_le_cardinalMk _) (mk_le_mk_of_subset (subset_inter hIX' hIY'))

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
⊢ e ∈ M.fundCocircuit f B ↔ f ∈ M.fundCircuit e B

Tactic:
suffices aux : ∀ {N : Matroid α} {B' : Set α} (hB' : N.IsBase B') {e f},
      e ∈ N.fundCocircuit f B' → f ∈ N.fundCircuit e B' from
    ⟨fun h ↦ aux hB h, fun h ↦ aux hB.compl_isBase_dual <| by
      simpa [fundCocircuit, inter_eq_self_of_subset_right hB.subset_ground]⟩
  clear! B M e f
  intro M B hB e f he
  -- discharge the various degenerate cases.
  obtain rfl | hne := eq_or_ne e f
  · simp [mem_fundCircuit]
  have hB' : M✶.IsBase (M✶.E \ B) := hB.compl_isBase_dual
  obtain hfE | hfE := em' <| f ∈ M.E
  · rw [fundCocircuit, fundCircuit_eq_of_notMem_ground (by simpa)] at he
    contradiction
  obtain hfB | hfB := em' <| f ∈ B
  · rw [fundCocircuit, fundCircuit_eq_of_mem (by simp [hfE, hfB])] at he
    contradiction
  obtain ⟨heE, heB⟩ : e ∈ M.E \ B := by
    simpa [hne] using (M.fundCocircuit_subset_insert_compl f B) he
  -- Use basis exchange to argue the equivalence.
  rw [fundCocircuit, hB'.indep.mem_fundCircuit_iff (by rwa [hB'.closure_eq]) (by simp [hfB])] at he
  rw [hB.indep.mem_fundCircuit_iff (by rwa [hB.closure_eq]) heB]
  have hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e})) :=
    (hB'.exchange_isBase_of_indep' ⟨heE, heB⟩ (by simp [hfE, hfB]) he).compl_isBase_of_dual
  refine hB'.indep.subset ?_
  simp only [dual_ground, sdiff_singleton_subset_iff]
  rw [sdiff_sdiff_right, inter_eq_self_of_subset_right (by simpa), union_singleton, insert_comm,
    ← union_singleton (s := M.E \ B), ← sdiff_sdiff, sdiff_sdiff_cancel_left hB.subset_ground]
  simp [hfB]

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
i : ι
this✝ : AlgebraicIndependent R (x ∘ ![i])
this : AlgebraicIndependent R ![x i]
⊢ Transcendental R (x i)

Tactic:
← algebraicIndependent_iff_transcendental

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
i : ι
this✝ : AlgebraicIndependent R (x ∘ ![i])
this : AlgebraicIndependent R ![x i]
⊢ AlgebraicIndependent R ![x i]
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✝ : Algebra.IsAlgebraic R A
⊢ IsEmpty ι

Tactic:
rcases isEmpty_or_nonempty ι with h | ⟨⟨i⟩⟩
  · exact h
  exact False.elim (hx.transcendental i (Algebra.IsAlgebraic.isAlgebraic _))

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

Goal state before:
pp: case a
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
⊢ insert f I \ {e} ⊆ M.closure I

pp: case a
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
⊢ I ⊆ M.closure (insert f I \ {e})

Tactic:
· simp only [subset_def, mem_sdiff, mem_insert_iff, mem_singleton_iff]
    rintro a (rfl | haI)
    exacts [hf, M.subset_closure _ hI.subset_ground haI]

Goal state after:
case a
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
⊢ I ⊆ M.closure (insert f I \ {e})
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
s : Set ι
ind : AlgebraicIndependent R fun i ↦ x✝ ↑i
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i ↦ x✝ ↑i) → ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x✝ '' t))) (x✝ i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t \ s
hu : u ⊆ t \ s
ha' : a ∉ u
h : AlgebraicIndependent R fun i ↦ x✝ ↑i
this : a ∉ t ∩ s ∪ u
x : ↑(t ∩ s ∪ insert a u)
⊢ x✝ ↑x = (((fun o ↦ o.elim (x✝ a) fun i ↦ x✝ ↑i) ∘ ⇑(subtypeInsertEquivOption this)) ∘ ⇑(Equiv.setCongr ⋯)) x

Tactic:
by_cases h : ↑x = a

Goal state after:
case pos
ι : Type u_1
R : Type u_3
A : Type v
x✝ : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
ind : AlgebraicIndependent R fun i ↦ x✝ ↑i
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i ↦ x✝ ↑i) → ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x✝ '' t))) (x✝ i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t \ s
hu : u ⊆ t \ s
ha' : a ∉ u
h✝ : AlgebraicIndependent R fun i ↦ x✝ ↑i
this : a ∉ t ∩ s ∪ u
x : ↑(t ∩ s ∪ insert a u)
h : ↑x = a
⊢ x✝ ↑x = (((fun o ↦ o.elim (x✝ a) fun i ↦ x✝ ↑i) ∘ ⇑(subtypeInsertEquivOption this)) ∘ ⇑(Equiv.setCongr ⋯)) x

case neg
ι : Type u_1
R : Type u_3
A : Type v
x✝ : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
ind : AlgebraicIndependent R fun i ↦ x✝ ↑i
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i ↦ x✝ ↑i) → ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x✝ '' t))) (x✝ i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t \ s
hu : u ⊆ t \ s
ha' : a ∉ u
h✝ : AlgebraicIndependent R fun i ↦ x✝ ↑i
this : a ∉ t ∩ s ∪ u
x : ↑(t ∩ s ∪ insert a u)
h : ¬↑x = a
⊢ x✝ ↑x = (((fun o ↦ o.elim (x✝ a) fun i ↦ x✝ ↑i) ∘ ⇑(subtypeInsertEquivOption this)) ∘ ⇑(Equiv.setCongr ⋯)) x
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: case prime
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hg : IsSeparableContraction q f g
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
⊢ g.natDegree = hf.degree

Tactic:
rcases hg with ⟨hg, m, hm⟩

Goal state after:
case prime
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : g.Separable
m : ℕ
hm : (expand F (q ^ m)) g = f
⊢ g.natDegree = hf.degree
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
I E X : Set α
⊢ (uniqueBaseOn I E).closure X = X ∩ I ∩ E ∪ E \ I

Tactic:
rw [uniqueBaseOn, restrict_closure_eq', freeOn_closure_eq, inter_right_comm,
    inter_assoc (c := E), inter_self, inter_right_comm, freeOn_ground]

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
⊢ AlgebraicIndependent R Subtype.val

Tactic:
by
  refine algebraicIndependent_of_finite (⋃ i, s i) fun t ht ft => ?_
  rcases finite_subset_iUnion ft ht with ⟨I, fi, hI⟩
  rcases hs.finset_le fi.toFinset with ⟨i, hi⟩
  exact (h i).mono (Subset.trans hI <| iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))

Goal state after: