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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : PrimeSpectrum R
inst✝ : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
H : ∀ m ∈ ↑s, ∃ x, x • m = 0 ∧ x ∉ p.asIdeal
x : { a // a ∈ ↑s } → R
hx : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 • ↑x_1 = 0
hx' : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 ∉ p.asIdeal
⊢ s.attach.prod x ∈ annihilator R M

pp: case refine_2
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : PrimeSpectrum R
inst✝ : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
H : ∀ m ∈ ↑s, ∃ x, x • m = 0 ∧ x ∉ p.asIdeal
x : { a // a ∈ ↑s } → R
hx : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 • ↑x_1 = 0
hx' : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 ∉ p.asIdeal
⊢ s.attach.prod x ∉ p.asIdeal

Tactic:
· rw [← Submodule.annihilator_top, ← hs, Submodule.mem_annihilator_span]
    intro m
    obtain ⟨k, hk⟩ := Finset.dvd_prod_of_mem x (Finset.mem_attach _ m)
    rw [hk, mul_comm, mul_smul, hx, smul_zero]

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : PrimeSpectrum R
inst✝ : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
H : ∀ m ∈ ↑s, ∃ x, x • m = 0 ∧ x ∉ p.asIdeal
x : { a // a ∈ ↑s } → R
hx : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 • ↑x_1 = 0
hx' : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 ∉ p.asIdeal
⊢ s.attach.prod x ∉ p.asIdeal
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
v : Fin n → M
⊢ (toTensorPower R M n) ((ιMulti R n) v) = ∑ σ, Perm.sign σ • (tprod R) fun i ↦ v (σ i)

Tactic:
dsimp [toTensorPower]
  simp only [alternatingMapLinearEquiv_apply_ιMulti,
    MultilinearMap.alternatization_apply, MultilinearMap.domDomCongr_apply]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
this : ∀ (j : Fin l), ¬IsUnit (a n j)
⊢ v n✝ ∈ 𝔪 • ⊤

Tactic:
rw [show v n = _ from hay n]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
this : ∀ (j : Fin l), ¬IsUnit (a n j)
⊢ ∑ j, a n j • y j ∈ 𝔪 • ⊤
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: case of_add
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
b : R × ((i : ι) → s i)
a : FreeAddMonoid (R × ((i : ι) → s i))
ih : ↑a = (List.map (fun x ↦ x.1 • ⨂ₜ[R] (i : ι), x.2 i) (FreeAddMonoid.toList a)).sum
⊢ ↑(FreeAddMonoid.of b + a) =
    ((b.1 • ⨂ₜ[R] (i : ι), b.2 i) :: List.map (fun x ↦ x.1 • ⨂ₜ[R] (i : ι), x.2 i) (FreeAddMonoid.toList a)).sum

Tactic:
List.sum_cons,

Goal state after:
case of_add
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
b : R × ((i : ι) → s i)
a : FreeAddMonoid (R × ((i : ι) → s i))
ih : ↑a = (List.map (fun x ↦ x.1 • ⨂ₜ[R] (i : ι), x.2 i) (FreeAddMonoid.toList a)).sum
⊢ ↑(FreeAddMonoid.of b + a) =
    (b.1 • ⨂ₜ[R] (i : ι), b.2 i) + (List.map (fun x ↦ x.1 • ⨂ₜ[R] (i : ι), x.2 i) (FreeAddMonoid.toList a)).sum
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case insert.specialize_1
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
⊢ (⇑(Ideal.Quotient.mk 𝔪) ∘ c) ↑n = 0

Tactic:
simp_rw [Function.comp_def, c, if_pos, neg_zero, zero_mul, map_zero]

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
hR : IsNoetherianRing R
I : Ideal R
⊢ I.minimalPrimes.Finite

Tactic:
by
  by_contra hI
  obtain ⟨I : Ideal R, hI : ¬ I.minimalPrimes.Finite, hmax⟩ :=
    set_has_maximal_iff_noetherian.mpr hR {I : Ideal R | ¬ I.minimalPrimes.Finite} ⟨I, hI⟩
  simp only [Set.mem_ofPred_eq, not_imp_not] at hmax
  have h1 : ¬ I.IsPrime := by contrapose hI; simp [minimalPrimes_eq_subsingleton_self]
  have h2 : I ≠ ⊤ := by contrapose hI; simp [hI, minimalPrimes_top]
  obtain ⟨x, hx, y, hy, h⟩ := (not_isPrime_iff.mp h1).resolve_left h2
  rw [← Ideal.span_singleton_le_iff_mem, ← left_lt_sup] at hx hy
  refine hI (((hmax _ hx).union (hmax _ hy)).subset fun p ⟨⟨hp, hI⟩, hmin⟩ ↦ ?_)
  rcases hp.2 (hI h) with hxp | hyp
  · exact Or.inl ⟨⟨hp, sup_le hI (p.span_singleton_le_iff_mem.mpr hxp)⟩,
      fun q hq hqp ↦ hmin ⟨hq.1, hx.le.trans hq.2⟩ hqp⟩
  · exact Or.inr ⟨⟨hp, sup_le hI (p.span_singleton_le_iff_mem.mpr hyp)⟩,
      fun q hq hqp ↦ hmin ⟨hq.1, hy.le.trans hq.2⟩ hqp⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: case mp
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
inst✝ : IsNoetherianRing R
⊢ N.IsAssociatedPrime I → I.IsPrime ∧ ∃ x, I = N.colon {x}

Tactic:
rintro ⟨hx, x, rfl⟩

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsNoetherianRing R
x : M
hx : (N.colon {x}).radical.IsPrime
⊢ (N.colon {x}).radical.IsPrime ∧ ∃ x_1, (N.colon {x}).radical = N.colon {x_1}
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: case mpr
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
inst✝ : IsNoetherianRing R
⊢ (I.IsPrime ∧ ∃ x, I = N.colon {x}) → N.IsAssociatedPrime I

Tactic:
rintro ⟨hx, x, rfl⟩

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsNoetherianRing R
x : M
hx : (N.colon {x}).IsPrime
⊢ N.IsAssociatedPrime (N.colon {x})
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
I : Ideal R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : IsAssociatedPrime I M
hf : Function.Injective ⇑f
⊢ IsAssociatedPrime I M'

Tactic:
obtain ⟨x, rfl⟩ := h.2
  refine ⟨h.1, ⟨f x, ?_⟩⟩
  ext r
  simp_rw [Ideal.mem_radical_iff, mem_colon_singleton, mem_bot, ← map_smul, map_eq_zero_iff f hf]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
I : Ideal R
hI : IsUnit ↑I
⊢ Submodule.IsPrincipal I

Tactic:
by
  obtain ⟨a, K, ha0, h⟩ := exists_eq_spanSingleton_mul (I : FractionalIdeal R⁰ (FractionRing R))⁻¹
  have hIK : I * K = Ideal.span ({a} : Set R) :=
    (coeIdeal_inj (K := FractionRing R)).mp <| by
      rw [coeIdeal_mul, coeIdeal_span_singleton]
      rw [← mul_inv_cancel_iff_isUnit] at hI
      have ha0' := spanSingleton_mul_inv (R₁ := R) (FractionRing R)
        (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors
          (mem_nonZeroDivisors_iff_ne_zero.mpr ha0))
      replace h :=
        congrArg
          (fun t =>
            spanSingleton R⁰ ((algebraMap R (FractionRing R)) a) * I * t)
          h.symm
      rwa [mul_mul_mul_comm, ← spanSingleton_inv, ha0', one_mul, mul_assoc, hI, mul_one] at h
  refine isPrincipal_of_exists_mul_ne_zero_isPrincipal (J := I) ?_
  refine ⟨K, ?_, ?_⟩
  · simp [hIK, ha0]
  · simpa [hIK] using (inferInstance : (Ideal.span {a}).IsPrincipal)

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
α : Type u_5
β : Type u_6
f : X → α
g : α → β
h : IsLocallyConstant (g ∘ f)
inj : Function.Injective g
s : Set α
⊢ IsOpen[inst✝] (f ⁻¹' s)

Tactic:
rw [← preimage_image_eq s inj, preimage_preimage]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
α : Type u_5
β : Type u_6
f : X → α
g : α → β
h : IsLocallyConstant (g ∘ f)
inj : Function.Injective g
s : Set α
⊢ IsOpen[inst✝] ((fun x ↦ g (f x)) ⁻¹' g '' s)
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
⊢ IsLocallyConstant fun i ↦ if hi : i ∈ C₁ then f ⟨i, hi⟩ else g ⟨i, ⋯⟩

Tactic:
have : DiscreteTopology Z := discreteTopology_bot Z

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
⊢ IsLocallyConstant fun i ↦ if hi : i ∈ C₁ then f ⟨i, hi⟩ else g ⟨i, ⋯⟩
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: case mp
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₁ q₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
⊢ (preimageEquivFiber R S p) q₁ ≤ (preimageEquivFiber R S p) q₂ → q₁ ≤ q₂

Tactic:
obtain ⟨q₁, rfl⟩ := (preimageEquivFiber R S p).symm.surjective q₁

Goal state after:
case mp
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₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
q₁ : PrimeSpectrum (p.asIdeal.Fiber S)
⊢ (preimageEquivFiber R S p) ((preimageEquivFiber R S p).symm q₁) ≤ (preimageEquivFiber R S p) q₂ →
    (preimageEquivFiber R S p).symm q₁ ≤ q₂
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
x✝ : ↑(freeLocus R M)
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this✝² : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : p ∈ freeLocus R M
hp : ⟨p, hp''⟩ ∈ Subtype.val ⁻¹' ↑(basicOpen f)
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl
Rₚ : Type uR := Localization.AtPrime p.asIdeal
Mₚ : Type (max uR uM) := LocalizedModule p.asIdeal.primeCompl M
this✝¹ : Algebra (Localization.Away f) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization.Away f) Rₚ (Submonoid.powers f) p.asIdeal.primeCompl hp'
this✝ : IsScalarTower R (Localization.Away f) Rₚ
this : Module (Localization.Away f) Mₚ := compHom Mₚ (algebraMap (Localization.Away f) Rₚ)
r : R
r' : Localization.Away f
m : Mₚ
⊢ (algebraMap (Localization.Away f) Rₚ) (r • r') • m = r • r' • m

Tactic:
simp [Rₚ, Mₚ, Algebra.smul_def, ← IsScalarTower.algebraMap_apply, mul_smul]; rfl

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : Pic R
⊢ M * N = Pic.mk R (M.AsModule ⊗[R] N.AsModule)

Tactic:
rw [mk_tensor, mk_eq_self, mk_eq_self]

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ mapAlgebra R R = MonoidHom.id (Pic R)

Tactic:
mapAlgebra_self

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ MonoidHom.id (Pic R) = MonoidHom.id (Pic R)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
x✝ :
  (∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ⊆ y → B = y
B' : Set α
hB' : M.IsBase B'
hBB' : Disjoint B B'
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ⊆ y → B = y
⊢ M.IsBase (M.E \ (M.E \ B'))

Tactic:
simpa [hB'.subset_ground]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
⊢ ∃ f ∈ B' \ B, B' = insert f B \ {e}

Tactic:
by
  obtain ⟨f, hf, hb⟩ := hB.exchange hB' (h.symm.subset (mem_singleton e))
  have hne : f ≠ e := by rintro rfl; exact hf.2 (h.symm.subset (mem_singleton f)).1
  rw [insert_sdiff_singleton_comm hne] at hb
  refine ⟨f, hf, (hb.eq_of_subset_isBase hB' ?_).symm⟩
  rw [sdiff_subset_iff, insert_subset_iff, union_comm, ← sdiff_subset_iff, h,
    and_iff_left rfl.subset]
  exact Or.inl hf.1

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case neg
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h : α ^ m * (aeval (α ^ n)) s - (aeval (α ^ n)) r = 0
hm : 0 < m
hzero : s ≠ 0
⊢ IsAlgebraic F α

Tactic:
let f : F[X] := X ^ m * expand F n s - expand F n r

Goal state after:
case neg
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h : α ^ m * (aeval (α ^ n)) s - (aeval (α ^ n)) r = 0
hm : 0 < m
hzero : s ≠ 0
f : F[X] := X ^ m * (expand F n) s - (expand F n) r
⊢ IsAlgebraic F α
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
⊢ M.IsBasis I Y

Tactic:
by
  rw [isBasis_iff (hYX.trans hI.subset_ground), and_iff_right hI.indep, and_iff_right hIY]
  exact fun J hJ hIJ hJY ↦ hI.eq_of_subset_indep hJ hIJ (hJY.trans hYX)

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

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint (insert x I) B

Tactic:
use e

Goal state after:
case h
α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := ⋯
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
⊢ e ∈ X \ I ∧ insert e I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint (insert e I) B
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M ↾ M.E = M

Tactic:
refine ext_indep rfl ?_; simp_all

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

Goal state before:
pp: α : Type u_1
E I J : Set α
⊢ (freeOn I).Indep J ∧ J ⊆ E ↔ J ⊆ I ∩ E

Tactic:
freeOn_indep_iff,

Goal state after:
α : Type u_1
E I J : Set α
⊢ J ⊆ I ∧ J ⊆ E ↔ J ⊆ I ∩ E
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I J : Set α
hIE : I ⊆ E
⊢ (freeOn I).Indep J ∧ J ⊆ E ↔ J ⊆ I

Tactic:
freeOn_indep_iff,

Goal state after:
α : Type u_1
E I J : Set α
hIE : I ⊆ E
⊢ J ⊆ I ∧ J ⊆ E ↔ J ⊆ I
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
⊢ M.IsBasis' I X ↔ (M ↾ univ).IsBasis I X

Tactic:
by
  rw [isBasis_restrict_iff', isBasis'_iff_isBasis_inter_ground, and_iff_left (subset_univ _)]

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

Goal state before:
pp: α : Type u_1
I E R : Set α
⊢ True ∧ ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((uniqueBaseOn I E ↾ R).Indep I_1 ↔ (uniqueBaseOn (I ∩ R ∩ E) R).Indep I_1)

Tactic:
true_and,

Goal state after:
α : Type u_1
I E R : Set α
⊢ ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((uniqueBaseOn I E ↾ R).Indep I_1 ↔ (uniqueBaseOn (I ∩ R ∩ E) R).Indep I_1)
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
⊢ Disjoint (B ∩ X) {e}

Tactic:
disjoint_singleton_right,

Goal state after:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
⊢ e ∉ B ∩ X
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
hi : N.Indep (f '' I)
⊢ I ⊆ f ⁻¹' f '' I

Tactic:
apply subset_preimage_image

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

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
hM : ∃ M, E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I
hex : ∃ M, E = M.E ∧ M.Indep = Indep
⊢ Indep ∅

Tactic:
obtain ⟨M, -, rfl⟩ := hex; exact M.empty_indep

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ (X ∪ Y) ∩ M.E ⊆ M.closure (I ∪ J)

Tactic:
rw [closure_union_congr_left hI.closure_eq_closure,
    closure_union_congr_right hJ.closure_eq_closure]

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ (X ∪ Y) ∩ M.E ⊆ M.closure (X ∪ Y)
Module: Mathlib.Combinatorics.Matroid.Circuit

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

Tactic:
nth_rw 2 [← insert_eq_of_mem he]
  rw [← insert_sdiff_singleton, (hC.sdiff_singleton_indep he).isBasis_insert_iff,
    insert_sdiff_singleton, insert_eq_of_mem he]
  exact Or.inl hC.dep

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 : Matroid β
inst✝ : M.Nonempty
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).E.Nonempty

Tactic:
simp [M.ground_nonempty]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y

Tactic:
obtain ⟨Ii, hIi⟩ := M.exists_isBasis' (X ∩ Y)

Goal state after:
α : Type u_1
M : Matroid α
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
⊢ M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
e : α
E : Set α
⊢ (freeOn E).Indep {e} ↔ e ∈ E

Tactic:
freeOn_indep_iff,

Goal state after:
α : Type u_1
e : α
E : Set α
⊢ {e} ⊆ E ↔ e ∈ E
Module: Mathlib.Combinatorics.Matroid.Loop

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

Tactic:
and_iff_left (M.subset_closure _),

Goal state after:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ M.closure (M.closure X ∪ K) ⊆ M.closure X ∪ K
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
⊢ M₁ = M₂

Tactic:
by
  refine ext_indep hE fun I hI ↦ ?_
  rw [← sdiff_coloops_indep_iff, ← @sdiff_coloops_indep_iff _ M₂, ← hc]
  obtain hdj | hndj := em (Disjoint I (M₁.loops))
  · rw [h _ (sdiff_subset.trans hI)]
    rw [disjoint_union_right]
    exact ⟨disjoint_of_subset_left sdiff_subset hdj, disjoint_sdiff_left⟩
  obtain ⟨e, heI, hel : M₁.IsLoop e⟩ := not_disjoint_iff_nonempty_inter.mp hndj
  refine iff_of_false (hel.not_indep_of_mem ⟨heI, hel.not_isColoop⟩) ?_
  rw [isLoop_iff, hl, ← isLoop_iff] at hel
  rw [hc]
  exact hel.not_indep_of_mem ⟨heI, hel.not_isColoop⟩

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:
obtain ⟨Ii, hIi⟩ := M.exists_isBasis' (X ∩ Y)

Goal state after:
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
⊢ M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : 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
⊢ e ∈ M.E \ B

Tactic:
by
    simpa [hne] using (M.fundCocircuit_subset_insert_compl f B) he

Goal state after: