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ₚ : (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
P : Ideal R
hP : P.IsMaximal
e : Rₚ P ≃+* Localization.AtPrime P :=
  (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P)).toRingEquiv
⊢ ∀ (m : Rₚ P) (x : Mₚ P),
    (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M))).toFun (m • x) =
      ↑e m • (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M))).toFun x

Tactic:
intro r m
    obtain ⟨r, s, rfl⟩ := IsLocalization.exists_mk'_eq P.primeCompl r
    apply ((Module.End.isUnit_iff _).mp
      (IsLocalizedModule.map_units (LocalizedModule.mkLinearMap P.primeCompl M) s)).1
    dsimp [e]
    simp only [← map_smul, ← smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul,
      IsLocalization.map_id_mk']

Goal state after:
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'
I : Type u_1 := Free.ChooseBasisIndex 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:
let b : Basis I Rₛ M' := Module.Free.chooseBasis Rₛ M'

Goal state after:
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'
I : Type u_1 := Free.ChooseBasisIndex Rₛ M'
b : Basis I Rₛ M' := Free.chooseBasis 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'
Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible

Goal state before:
pp: case inr
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
⊢ Free R M

Tactic:
have hp : Module.finrank R (M × N) = n + 1 := by
    let 𝔭 : PrimeSpectrum R := Nonempty.some inferInstance
    have h1 : rankAtStalk M 𝔭 = 1 := by simp [rankAtStalk, Invertible.finrank_eq_one]
    have heq := congr($(rankAtStalk_prod M N) 𝔭)
    simp only [rankAtStalk_eq_finrank_of_free, Pi.natCast_apply, Pi.add_apply, h1] at heq
    grind

Goal state after:
case inr
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
⊢ Free R M
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
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉ q.asIdeal

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
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉
    ((fun q ↦
          {
            asIdeal :=
              RingHom.ker
                (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                    (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
            isPrime := ⋯ })
        ((fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩) q)).asIdeal

Tactic:
· rw [← Ideal.mem_comap, ← PrimeSpectrum.comap_asIdeal]
      convert! hr
      exact (residueField_comap _).le ⟨q.comap (algebraMap _ _), rfl⟩

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
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉
    ((fun q ↦
          {
            asIdeal :=
              RingHom.ker
                (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                    (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
            isPrime := ⋯ })
        ((fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩) q)).asIdeal
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
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉
    ((fun q ↦
          {
            asIdeal :=
              RingHom.ker
                (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                    (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
            isPrime := ⋯ })
        ((fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩) q)).asIdeal

Tactic:
simpa [-Algebra.algebraMap_self, -AlgHom.commutes, -AlgHom.map_algebraMap,
        -Ideal.ResidueField.map_algebraMap]

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
p : PrimeSpectrum S
q : PrimeSpectrum R := comap (algebraMap R S) p
this : Algebra (Localization.AtPrime q.asIdeal) (Localization.AtPrime p.asIdeal) :=
  AtPrime.algebraOfLiesOver q.asIdeal p.asIdeal
e : LocalizedModule p.asIdeal.primeCompl (S ⊗[R] M) ≃ₗ[Localization.AtPrime p.asIdeal]
  Localization.AtPrime p.asIdeal ⊗[Localization.AtPrime q.asIdeal] LocalizedModule q.asIdeal.primeCompl M :=
  equivTensorProduct p.asIdeal.primeCompl (S ⊗[R] M) ≪≫ₗ
        AlgebraTensorModule.cancelBaseChange R S (Localization.AtPrime p.asIdeal) (Localization p.asIdeal.primeCompl)
          M ≪≫ₗ
      (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime q.asIdeal) (Localization.AtPrime p.asIdeal)
          (Localization p.asIdeal.primeCompl) M).symm ≪≫ₗ
    AlgebraTensorModule.congr (LinearEquiv.refl (Localization.AtPrime p.asIdeal) (Localization p.asIdeal.primeCompl))
      (equivTensorProduct q.asIdeal.primeCompl M).symm
⊢ finrank (Localization.AtPrime p.asIdeal)
      (Localization.AtPrime p.asIdeal ⊗[Localization.AtPrime q.asIdeal] LocalizedModule q.asIdeal.primeCompl M) =
    rankAtStalk M (comap (algebraMap R S) p)

Tactic:
apply Module.finrank_baseChange

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case hg
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] := ⋯
g : F[X] := ⋯
ιFE : F →+* E := ⋯
ιEE' : 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 := ⋯
p : (↥F⟮γ⟯)[X] := ⋯
h : E[X] := ⋯
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
⊢ eval β (Polynomial.map ιFE g) = 0

Tactic:
· rw [eval_map_algebraMap, minpoly.aeval]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
inst✝ : M.RankPos
hB : M.IsBase B
⊢ B.Nonempty

Tactic:
rw [nonempty_iff_ne_empty]

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
inst✝ : M.RankPos
hB : M.IsBase B
⊢ B ≠ ∅
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
D : Set α
hD : M.Dep D
⊢ D.Nonempty

Tactic:
rw [nonempty_iff_ne_empty]

Goal state after:
α : Type u_1
M : Matroid α
D : Set α
hD : M.Dep D
⊢ D ≠ ∅
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
h : ∃ α, F⟮α⟯ = ⊤
⊢ Finite (IntermediateField F E)

Tactic:
have := FiniteDimensional.of_exists_primitive_element F E h
  obtain ⟨α, hprim⟩ := h
  -- Let `f` be the minimal polynomial of `α ∈ E` over `F`
  let f : F[X] := minpoly F α
  let G := { g : E[X] // g.Monic ∧ g ∣ f.map (algebraMap F E) }
  -- Then `f` has only finitely many monic factors
  have hfin : Finite G := @Finite.of_fintype _ <| fintypeSubtypeMonicDvd
    (f.map (algebraMap F E)) <| map_ne_zero (minpoly.ne_zero_of_finite F α)
  -- If `K` is an intermediate field of `E/F`, let `g` be the minimal polynomial of `α` over `K`
  -- which is a monic factor of `f`
  let g : IntermediateField F E → G := fun K ↦
    ⟨(minpoly K α).map (algebraMap K E), (minpoly.monic <| .of_finite K α).map _, by
      convert! Polynomial.map_dvd (algebraMap K E) (minpoly.dvd_map_of_isScalarTower F K α)
      rw [Polynomial.map_map]; rfl⟩
  -- The map `K ↦ g` is injective
  have hinj : Function.Injective g := fun K K' heq ↦ by
    rw [Subtype.mk.injEq] at heq
    apply_fun fun f : E[X] ↦ adjoin F (f.coeffs : Set E) at heq
    simpa only [adjoin_minpoly_coeff_of_exists_primitive_element F hprim] using heq
  -- Therefore there are only finitely many intermediate fields
  exact Finite.of_injective g hinj

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊂ Y
hYX : Y ⊆ X
this : X ⊆ M.E
⊢ M.Dep Y

Tactic:
rw [← not_indep_iff]

Goal state after:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊂ Y
hYX : Y ⊆ X
this : X ⊆ M.E
⊢ ¬M.Indep Y
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
⊢ M.IsBasis (⋃ i, I i) (⋃ i, X i)

Tactic:
by
  refine h_ind.isBasis_of_forall_insert
    (iUnion_subset (fun i ↦ (hI i).subset.trans (subset_iUnion _ _))) ?_
  rintro e ⟨⟨_, ⟨⟨i, hi, rfl⟩, (hes : e ∈ X i)⟩⟩, he'⟩
  rw [mem_iUnion, not_exists] at he'
  refine ((hI i).insert_dep ⟨hes, he' _⟩).superset (insert_subset_insert (subset_iUnion _ _)) ?_
  rw [insert_subset_iff, iUnion_subset_iff, and_iff_left (fun i ↦ (hI i).indep.subset_ground)]
  exact (hI i).subset_ground hes

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.IsBasis (I ∪ J) (X ∪ Y)

Tactic:
union_eq_iUnion,

Goal state after:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.IsBasis (⋃ b, bif b then I else J) (X ∪ Y)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.Indep (⋃ i, bif i then I else J)

Tactic:
rwa [← union_eq_iUnion]

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

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

Tactic:
obtain ⟨B', hB', hIB'⟩ := hI.subset_isBasis_of_subset <| subset_union_left (t := B)
  exact ⟨B', hB.isBase_of_isBasis_superset subset_union_right hB', hIB', hB'.subset⟩

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I R : Set α
hR : R ⊆ M.E
hI : (M ↾ R).IsBase I
⊢ M.IsBasis I (M ↾ R).E

Tactic:
rwa [isBase_restrict_iff] at hI

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
x✝ : Nonempty α
⊢ ∃ M_1, range ⇑f = M_1.E ∧ ∀ (I : Set β), M_1.Indep I ↔ M.Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

Tactic:
refine ⟨M.comapOn (range f) (fun x ↦ ↑(invFunOn f univ x)), rfl, ?_⟩

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 α
⊢ ∀ (I : Set β),
    (M.comapOn (range ⇑f) fun x ↦ ↑(invFunOn (⇑f) univ x)).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
f : α → β
M : Matroid α
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
I : Set α
hI : M.Indep I
h_eq : f '' D₀ = f '' I
⊢ False

Tactic:
hf.image_eq_image_iff hD₀E hI.subset_ground

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
I : Set α
hI : M.Indep I
h_eq : D₀ = I
⊢ False
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:
rw [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: case refine_2
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.encard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hIc : I.encard = n
⊢ n ≤ M.eRk X

Tactic:
rw [← hIc, ← hI.eRk_eq_encard]

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.encard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hIc : I.encard = n
⊢ M.eRk I ≤ M.eRk X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hf : M.IsNonloop f
hne : e ≠ f
⊢ M.IsCircuit {e, f} ↔ e = f ∨ ¬M.Indep {e, f}

Tactic:
or_iff_right hne,

Goal state after:
case inr
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hf : M.IsNonloop f
hne : e ≠ f
⊢ M.IsCircuit {e, f} ↔ ¬M.Indep {e, f}
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
h : M✶.IsLoop e
⊢ M✶✶.IsColoop e

Tactic:
exact h.dual_isColoop

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.RankFinite
x✝ : M.eRank ≤ M.eRk X ∧ X ⊆ M.E
h : M.eRank ≤ M.eRk X
hX : X ⊆ M.E
I : Set α
hI : M.IsBasis I X
⊢ M.Spanning X

Tactic:
exact (hI.indep.isBase_of_eRk_ge
    hI.indep.finite (h.trans hI.eRk_eq_eRk.symm.le)).spanning_of_superset hI.subset

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X Y : Set α
⊢ M.closure (X ∪ Y) = M.closure (M.closure X ∪ M.closure Y)

Tactic:
union_eq_iUnion,

Goal state after:
α : Type u_2
M : Matroid α
X Y : Set α
⊢ M.closure (⋃ b, bif b then X else Y) = M.closure (M.closure X ∪ M.closure Y)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case pos
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∈ C₁
he₂ : e ∈ C₂
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

Tactic:
obtain ⟨C, hC, hC', -⟩ := hC₁.strong_elimination hC₂ he₁ he₂ hf₁ hf₂
      exact ⟨C, hC, hC'⟩

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

Goal state before:
pp: case pos
α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
heY : e ∈ X
J : Set α
hJ : M.IsBasis J {e}
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

Tactic:
exact ⟨J, hJ.subset.trans (by simpa), (finite_singleton e).subset hJ.subset, hJ.indep,
      by simpa using hJ.subset_closure⟩

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

Goal state before:
pp: α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ ⨆ i, lift.{v, u} #↑↑i ≤ lift.{u, v} (⨆ B, #↑↑B) ∧ ⨆ i, lift.{u, v} #↑↑i ≤ lift.{v, u} (⨆ B, #↑↑B)

Tactic:
simp only [ciSup_le_iff bddAbove_of_small, Subtype.forall, isBase_restrict_iff',
    comap_isBasis'_iff, and_imp]

Goal state after:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ (∀ (a : Set α), M.IsBasis' (f '' a) (f '' X) → InjOn f a → a ⊆ X → lift.{v, u} #↑a ≤ lift.{u, v} (⨆ B, #↑↑B)) ∧
    ∀ (a : Set β), M.IsBasis' a (f '' X) → lift.{u, v} #↑a ≤ lift.{v, u} (⨆ B, #↑↑B)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ (∃ C, M✶.IsCircuit C) ↔ ∃ K, M✶✶.IsCocircuit K

Tactic:
dual_dual M

Goal state after:
α : Type u_1
M : Matroid α
⊢ (∃ C, M✶.IsCircuit C) ↔ ∃ K, M.IsCocircuit K
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
e : α
M : Matroid α
B : Set α
he : e ∈ B
⊢ M.fundCocircuit e B ∩ B = {e}

Tactic:
refine subset_antisymm ?_ (singleton_subset_iff.2 ⟨M.mem_fundCocircuit _ _, he⟩)
  refine (inter_subset_inter_left _ (M.fundCocircuit_subset_insert_compl _ _)).trans ?_
  simp +contextual

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

Goal state before:
pp: case h
α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
⊢ M.Indep (⋃ i, bif i then I else J)

Tactic:
rwa [← union_eq_iUnion]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e f : α
B : Set α
hB : M.IsBasis B X
he : e ∈ M.closure (insert f B \ {e})
heB : e ∈ insert f B
hfX : f ∈ X
⊢ M.IsBasis (insert f B \ {e}) X

Tactic:
by
  rw [isBasis_iff_indep_closure] at hB ⊢
  exact ⟨hB.1.indep_insert_sdiff_of_mem_closure (hB.2.1 hfX) he heB, hB.2.1.trans_eq
    (hB.1.closure_insert_sdiff_eq_of_mem_closure (hB.2.1 hfX) he).symm, sdiff_subset.trans
    (insert_subset hfX hB.2.2)⟩

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

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

Tactic:
rw [← closure_inter_ground] at *

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f X ∩ M.E)
⊢ f ∈ M.closure (insert e X ∩ M.E)
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
insert_eq_of_mem hf.1,

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
⊢ M.closure (M.closure (M.closure (insert e X))) = M.closure (insert e X)
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: case zero
F : Type u_1
inst✝¹ : Field F
f g : F[X]
inst✝ : CharZero F
hf : HasSeparableContraction 1 f
hg : IsSeparableContraction 1 f g
⊢ g.natDegree = hf.degree

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 ⟨_, m, hm⟩
    rw [one_pow, expand_one] at hm
    rw [hf.eq_degree, hm]

Goal state after:
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
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: case mpr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
a✝ : a ∈ s
⊢ g • a ∉ fixedBy α g

Tactic:
smul_mem_fixedBy_iff_mem_fixedBy

Goal state after:
case mpr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
a✝ : a ∈ s
⊢ a ∉ fixedBy α g
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
ind : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
⊢ range x = Subtype.val '' range (Set.inclusion hxs)

Tactic:
← range_comp,

Goal state after:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
ind : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
⊢ range x = range (Subtype.val ∘ Set.inclusion hxs)
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 B : Set A
hB : (matroid R A).IsBasis B s
⊢ ∀ (x : A), (∀ a ∈ insert x B, IsAlgebraic (↥(adjoin R B)) a) ↔ IsAlgebraic (↥(adjoin R B)) x

Tactic:
forall_mem_insert

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 B : Set A
hB : (matroid R A).IsBasis B s
⊢ ∀ (x : A), (IsAlgebraic (↥(adjoin R B)) x ∧ ∀ x ∈ B, IsAlgebraic (↥(adjoin R B)) x) ↔ IsAlgebraic (↥(adjoin R B)) x