mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ↑(comap (algebraMap R S) ⁻¹' {p})
⊢ (fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩)
      ((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 := ⋯ })
        q) =
    q

Tactic:
ext x; simp

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Finite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
inst✝¹ : Module.Finite A B
x : B
inst✝ : Module.Free A B
⊢ (minpoly A x).natDegree ≤ Module.finrank A B

Tactic:
nontriviality A
  simpa [Module.finrank_eq_spanFinrank_of_free] using natDegree_le_spanFinrank A x

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✝ : Subsingleton M
⊢ rankAtStalk M = 0

Tactic:
ext p
  exact Module.finrank_zero_of_subsingleton

Goal state after:
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case neg
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
h : IsNormalClosure F K L
L' : Type ?u.22
inst✝¹ : Field L'
inst✝ : Algebra F L'
splits : ∀ (x : K), (Polynomial.map (algebraMap F L') (minpoly F x)).Splits
this : adjoin F (⨆ x, (minpoly F x).rootSet L) = ⊤
x : L
hx✝ : x ∈ ⨆ x, (minpoly F x).rootSet L
y : K
hx : x ∈ (minpoly F y).rootSet L
iy : ¬IsIntegral F y
⊢ (Polynomial.map (algebraMap F L') (minpoly F x)).Splits

Tactic:
· simp [minpoly.eq_zero iy] at hx

Goal state after:
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case neg
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : Algebra.IsAlgebraic F K
h : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
L' : Type u_4
inst✝¹ : Field L'
inst✝ : Algebra F L'
x : L'
hx✝ : x ∈ ⨆ x, (minpoly F x).rootSet L'
y : K
hx : x ∈ (minpoly F y).rootSet L'
iy : ¬IsIntegral F y
⊢ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits

Tactic:
· simp [minpoly.eq_zero iy] at hx

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case hf
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
⊢ (aeval α) f = 0

Tactic:
minpoly.aeval

Goal state after:
case hf
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
⊢ 0 = 0
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] := 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
⊢ (aeval β) g = 0

Tactic:
minpoly.aeval

Goal state after:
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] := 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
⊢ 0 = 0
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
⊢ (B₁ \ B₂).ncard = (B₂ \ B₁).ncard

Tactic:
rw [ncard_def, hB₁.encard_sdiff_comm hB₂, ← ncard_def]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M.RankInfinite
h : M.RankFinite
B : Set α
hB : M.IsBase B
⊢ False

Tactic:
exact hB.infinite hB.finite

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

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M.RankFinite
h : M.RankInfinite
B : Set α
hB : M.IsBase B
⊢ False

Tactic:
exact hB.infinite hB.finite

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

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

Tactic:
and_imp,

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase (M.E \ B) ↔
    (∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → (∃ B, M.IsBase B ∧ Disjoint y B) → B ⊆ y → B = y
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✝ : Finite (IntermediateField F E)
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯

Tactic:
by
  let f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯
  obtain ⟨x, y, hneq, heq⟩ := Finite.exists_ne_map_eq_of_infinite f
  use α + x • β
  apply le_antisymm
  · rw [adjoin_le_iff]
    have αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯ := mem_adjoin_simple_self F _
    have αyβ_in_K : α + y • β ∈ F⟮α + y • β⟯ := mem_adjoin_simple_self F _
    dsimp [f] at *
    simp only [← heq] at αyβ_in_K
    have β_in_K := sub_mem αxβ_in_K αyβ_in_K
    rw [show (α + x • β) - (α + y • β) = (x - y) • β by rw [sub_smul]; abel1] at β_in_K
    replace β_in_K := smul_mem _ β_in_K (x := (x - y)⁻¹)
    rw [smul_smul, inv_mul_eq_div, div_self (sub_ne_zero.2 hneq), one_smul] at β_in_K
    have α_in_K : α ∈ F⟮α + x • β⟯ := by
      convert! ← sub_mem αxβ_in_K (smul_mem _ β_in_K)
      apply add_sub_cancel_right
    rintro x (rfl | rfl) <;> assumption
  · rw [adjoin_simple_le_iff]
    have α_in_Fαβ : α ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert α {β})
    have β_in_Fαβ : β ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert_of_mem α rfl)
    exact F⟮α, β⟯.add_mem α_in_Fαβ (F⟮α, β⟯.smul_mem β_in_Fαβ)

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ M.Indep X ∨ M.Dep X

Tactic:
by
  rw [Dep, and_iff_left hX]
  apply em

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ ¬M.Indep X ↔ M.Dep X

Tactic:
by
  rw [Dep, and_iff_left hX]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
⊢ (∀ (e_1 : α), e_1 = e ∧ e_1 ∉ I → ¬M.Indep (insert e_1 I) ∧ e_1 ∈ M.E) ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I

Tactic:
and_imp,

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
⊢ (∀ (e_1 : α), e_1 = e → e_1 ∉ I → ¬M.Indep (insert e_1 I) ∧ e_1 ∈ M.E) ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
Xs : Set (Set α)
hne : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis I X
⊢ M.IsBasis I (⋃ i, ↑i)

Tactic:
have := Iff.mpr nonempty_coe_sort hne

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
Xs : Set (Set α)
hne : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis I X
this : Nonempty ↑Xs
⊢ M.IsBasis I (⋃ i, ↑i)
Module: Mathlib.Combinatorics.Matroid.Constructions

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

Tactic:
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
E B I : Set α
hIE : I ⊆ E
⊢ B = E ∩ I ↔ B = I

Tactic:
inter_eq_self_of_subset_right hIE

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

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

Tactic:
isBasis_restrict_iff',

Goal state after:
α : Type u_1
M : Matroid α
R I X : Set α
hR : R ⊆ M.E
⊢ M.IsBasis I (X ∩ M.E) ∧ X ⊆ R ↔ M.IsBasis I X ∧ X ⊆ R
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:
isBasis_restrict_iff',

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
⊢ M.IsBasis' I X ↔ M.IsBasis I (X ∩ M.E) ∧ X ⊆ univ
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : SurjOn f E N.E
⊢ InjOn f B ∧ B ⊆ E → (N.IsBasis' (f '' B) (f '' E) ↔ N.IsBase (f '' B))

Tactic:
and_imp,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : SurjOn f E N.E
⊢ InjOn f B → B ⊆ E → (N.IsBasis' (f '' B) (f '' E) ↔ N.IsBase (f '' B))
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
⊢ ∀ (e : α), e ∈ J ∧ e ∉ I → M.Dep (insert e I)

Tactic:
and_imp,

Goal state after:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
⊢ ∀ e ∈ J, e ∉ I → M.Dep (insert e I)
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).IsBase (f '' B)

Tactic:
map_isBase_iff

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α → β
hf : InjOn f M.E
⊢ ∃ B₀, M.IsBase B₀ ∧ f '' B = f '' B₀
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ (M.map f hf).IsBase (f '' B) ↔ M.IsBase B

Tactic:
map_isBase_iff

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ (∃ B₀, M.IsBase B₀ ∧ f '' B = f '' B₀) ↔ M.IsBase B
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
⊢ (M.map f hf).IsBasis (f '' I) (f '' X) ↔ M.IsBasis I X

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.map hf⟩

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
⊢ M.IsBasis I C ↔ ∃ e ∈ C \ I, C = insert e I

Tactic:
rw [hC.isBasis_iff_eq_sdiff_singleton]

Goal state after:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
⊢ (∃ e ∈ C, I = C \ {e}) ↔ ∃ e ∈ C \ I, C = insert e I
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C R : Set α
hR : R ⊆ M.E
⊢ ((¬M.Indep C ∧ C ⊆ R) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D ∧ D ⊆ R → D ⊆ C → D = C) →
    (M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C) ∧ C ⊆ R

Tactic:
and_imp,

Goal state after:
α : Type u_1
M : Matroid α
C R : Set α
hR : R ⊆ M.E
⊢ ¬M.Indep C →
    C ⊆ R →
      (∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ R → D ⊆ C → D = C) → (M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C) ∧ C ⊆ R
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α ↪ β
⊢ (M.map ⇑f ⋯).IsBase (⇑f '' B)

Tactic:
map_isBase_iff

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α ↪ β
⊢ ∃ B₀, M.IsBase B₀ ∧ ⇑f '' B = ⇑f '' B₀
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set β
⊢ (M.map ⇑f ⋯).IsBase B ↔ M.IsBase (⇑f ⁻¹' B) ∧ B ⊆ range ⇑f

Tactic:
map_isBase_iff

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set β
⊢ (∃ B₀, M.IsBase B₀ ∧ B = ⇑f '' B₀) ↔ M.IsBase (⇑f ⁻¹' B) ∧ B ⊆ range ⇑f
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ e ∈ M.closure (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})

Tactic:
hI.closure_sInter_eq_biInter_closure_of_forall_subset ⟨I, by simpa⟩ (by simp +contextual)

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ e ∈ ⋂ J ∈ {J | J ⊆ I ∧ e ∈ M.closure J}, M.closure J
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
B : Set β
⊢ (M.map ⇑f ⋯).IsBase B ↔ M.IsBase (⇑f.symm '' B)

Tactic:
map_isBase_iff

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
B : Set β
⊢ (∃ B₀, M.IsBase B₀ ∧ B = ⇑f '' B₀) ↔ M.IsBase (⇑f.symm '' B)
Module: Mathlib.Combinatorics.Matroid.Map

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

pp: α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ (M ↾ Y).IsBasis ↑I ↑X → I ⊆ X

Tactic:
isBasis_restrict_iff',

Goal state after:
α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ M.IsBasis (↑I) (↑X ∩ M.E) ∧ ↑X ⊆ Y ↔ M.IsBasis' (Subtype.val '' I) (Subtype.val '' X)

α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ (M ↾ Y).IsBasis ↑I ↑X → I ⊆ X
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ (M.restrictSubtype M.E)✶ = M✶.restrictSubtype M.E

Tactic:
by
  rw [restrictSubtype, ← comapOn_preimage_eq, comapOn_dual_eq_of_bijOn, restrict_ground_eq_self,
    ← dual_ground, comapOn_preimage_eq, restrictSubtype, restrict_ground_eq_self]
  exact ⟨by simp [MapsTo], Subtype.val_injective.injOn, by simp [SurjOn]⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
e : α
f : α → β
hf : InjOn f M.E
he : e ∈ M.E
⊢ (M.map f hf).IsLoop (f e) ↔ M.IsLoop e

Tactic:
rw [isLoop_iff, map_loops, hf.mem_image_iff M.loops_subset_ground he, isLoop_iff]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
R X I : Set α
hI : (M ↾ R).IsBasis I (X ∩ (M ↾ R).E)
⊢ I.encard = M.eRk (X ∩ R)

Tactic:
isBasis_restrict_iff',

Goal state after:
α : Type u_1
M : Matroid α
R X I : Set α
hI : M.IsBasis I (X ∩ (M ↾ R).E ∩ M.E) ∧ X ∩ (M ↾ R).E ⊆ R
⊢ I.encard = M.eRk (X ∩ R)
Module: Mathlib.Combinatorics.Matroid.Loop

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

Tactic:
by rw [← dual_dual M]; exact h.dual_isColoop

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hXI : X ⊆ M.closure I
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
⊢ M.IsBasis I X

Tactic:
have hIJ := hJ.subset.trans inter_subset_left

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hXI : X ⊆ M.closure I
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hXI : X ⊆ M.closure I
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ M.IsBasis I X

Tactic:
rw [← closure_inter_ground] at hXI

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hXI : X ⊆ M.closure (I ∩ M.E)
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
this :
  ∀ {α : Type u_1} (M : Matroid α) (e : α),
    (M.IsColoop e ↔ e ∈ M.coloops) →
      (M.IsColoop e ↔ M.IsCocircuit {e}) →
        (M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B) →
          (M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E) →
            ((∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B) →
              ((∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X) →
                e ∈ M.E → (M.IsColoop e ↔ ¬M.Spanning (M.E \ {e}))
he : e ∉ M.E
⊢ M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})

pp: α✝ α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
⊢ M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})

Tactic:
· exact iff_of_false (fun h ↦ he h.mem_ground) <| by simp [he, M.ground_spanning]

Goal state after:
α✝ α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
⊢ M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.eRank = 0 ↔ M = loopyOn M.E

Tactic:
refine ⟨fun h ↦ closure_empty_eq_ground_iff.1 ?_, fun h ↦ by rw [h, eRank_loopyOn]⟩
  obtain ⟨B, hB⟩ := M.exists_isBase
  rw [← hB.encard_eq_eRank, encard_eq_zero] at h
  rw [← h, hB.closure_eq]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
Xs : Set (Set α)
⊢ M.closure (⋃ X ∈ Xs, M.closure X) = M.closure (⋃ i, ↑i)

Tactic:
biUnion_eq_iUnion,

Goal state after:
α : Type u_2
M : Matroid α
Xs : Set (Set α)
⊢ M.closure (⋃ x, M.closure ↑x) = M.closure (⋃ i, ↑i)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
A : Set ι
⊢ M.closure (⋃ i ∈ A, M.closure (Xs i)) = M.closure (⋃ i ∈ A, Xs i)

Tactic:
biUnion_eq_iUnion,

Goal state after:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
A : Set ι
⊢ M.closure (⋃ x, M.closure (Xs ↑x)) = M.closure (⋃ i ∈ A, Xs i)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
⊢ M.closure (⋂₀ Js) ⊆ ⋂ J ∈ Js, M.closure J ∧ ⋂ J ∈ Js, M.closure J ⊆ M.closure (⋂₀ Js)

Tactic:
subset_iInter₂_iff

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
⊢ (∀ i ∈ Js, M.closure (⋂₀ Js) ⊆ M.closure i) ∧ ⋂ J ∈ Js, M.closure J ⊆ M.closure (⋂₀ Js)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite ↑(B' \ B)
S : (a : α) → a ∈ B' \ B → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite ↑(S a ha)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ a, S ↑a ⋯
this : B \ B' ⊆ U
⊢ #↑(B \ B') ≤ #↑(B' \ B)

Tactic:
refine (mk_le_mk_of_subset this).trans <| (mk_iUnion_le ..).trans
      <| (mul_le_max_of_aleph0_le_left (by simp)).trans ?_

Goal state after:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite ↑(B' \ B)
S : (a : α) → a ∈ B' \ B → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite ↑(S a ha)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ a, S ↑a ⋯
this : B \ B' ⊆ U
⊢ max (#↑(B' \ B)) (⨆ i, #↑(S ↑i ⋯)) ≤ #↑(B' \ B)