mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
⊢ M✶.Dep I ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
⊢ M✶.Dep I ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I : Set α
⊢ uniqueBaseOn ∅ I = loopyOn I

Tactic:
rw [← dual_inj, uniqueBaseOn_dual_eq, sdiff_empty, uniqueBaseOn_self, loopyOn_dual_eq]

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

Goal state before:
pp: α : Type u_1
I E R : Set α
⊢ uniqueBaseOn I E ↾ R = uniqueBaseOn (I ∩ R ∩ E) R

Tactic:
[

Goal state after:
α : Type u_1
I E R : Set α
⊢ uniqueBaseOn I E ↾ R = uniqueBaseOn (I ∩ R ∩ E) R
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case refine_2
α : 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
⊢ M✶.Dep (insert e (M.E \ B ∩ (M.E \ X)))

Tactic:
[

Goal state after:
case refine_2
α : 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
⊢ M✶.Dep (insert e (M.E \ B ∩ (M.E \ X)))
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}))
⊢ B ∩ X ⊆ B \ {e}

Tactic:
[

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}))
⊢ B ∩ X ⊆ B \ {e}
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.Coindep X ↔ (∃ B, M.IsBase B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.Coindep X ↔ (∃ B, M.IsBase B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ insert e I ⊆ (N.comap f).E

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ insert e I ⊆ (N.comap f).E
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.Coindep X ↔ ∃ B, M.IsBase B ∧ X ⊆ M.E \ B

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.Coindep X ↔ ∃ B, M.IsBase B ∧ X ⊆ M.E \ B
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
⊢ (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ InjOn f B ∧ B ⊆ E

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : SurjOn f E N.E
⊢ (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ InjOn f B ∧ B ⊆ E
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)
⊢ M.IsBasis I (I ∪ J)

Tactic:
[

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)
⊢ M.IsBasis I (I ∪ J)
Module: Mathlib.Combinatorics.Matroid.Rank.Finite

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ M.IsRkFinite X ↔ ∃ I, M.IsBasis I X ∧ I.Finite

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ M.IsRkFinite X ↔ ∃ I, M.IsBasis I X ∧ I.Finite
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 α
⊢ ∀ (I : Set β),
    (M.comapOn (range ⇑f) fun x ↦ ↑(invFunOn (⇑f) univ x)).Indep I ↔ M.Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

Tactic:
[

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: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
I : Set β
⊢ (M.mapSetEmbedding { toFun := M.E.domRestrict f, inj' := ⋯ }).Indep I ↔ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
I : Set β
⊢ (M.mapSetEmbedding { toFun := M.E.domRestrict f, inj' := ⋯ }).Indep I ↔ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
x✝ : ∃ I₀, M.Indep I₀ ∧ f '' I = f '' I₀
J : Set α
hJ : M.Indep J
hIJ : f '' I = f '' J
⊢ M.Indep I

Tactic:
rw [hf.image_eq_image_iff hI hJ.subset_ground] at hIJ

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
x✝ : ∃ I₀, M.Indep I₀ ∧ f '' I = f '' I₀
J : Set α
hJ : M.Indep J
hIJ : I = J
⊢ M.Indep I
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ Minimal (fun x ↦ ¬M.Indep x) C

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ Minimal (fun x ↦ ¬M.Indep x) C
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 '' M.E \ f '' B) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ (M✶.map f hf).IsBase (f '' B)

Tactic:
[

Goal state after:
α : 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 '' M.E \ f '' B) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ (M✶.map f hf).IsBase (f '' B)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C R : Set α
hC : M.IsCircuit C
hCR : C ⊆ R
⊢ (M ↾ R).IsCircuit C

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
C R : Set α
hC : M.IsCircuit C
hCR : C ⊆ R
⊢ (M ↾ R).IsCircuit C
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).IsCircuit C → M.IsCircuit C ∧ C ⊆ R

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
C R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).IsCircuit C → M.IsCircuit C ∧ C ⊆ R
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure I
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}) = insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure I
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}) = insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
⊢ ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
⊢ ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e
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.Finitary
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).Finitary

Tactic:
refine ⟨fun I hI ↦ ?_⟩
  simp only [map_indep_iff]
  have h' : I ⊆ f '' M.E := by
    intro e he
    obtain ⟨I₀, hI₀, h_eq⟩ := hI {e} (by simpa) (by simp)
    exact image_mono hI₀.subset_ground <| h_eq.subset rfl
  obtain ⟨I₀, hI₀E, rfl⟩ := subset_image_iff.1 h'
  refine ⟨I₀, indep_of_forall_finite_subset_indep _ fun J₀ hJ₀I₀ hJ₀ ↦ ?_, rfl⟩
  specialize hI (f '' J₀) (image_mono hJ₀I₀) (hJ₀.image _)
  rwa [map_image_indep_iff (hJ₀I₀.trans hI₀E)] at hI

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
⊢ (M.mapEmbedding f).Indep I ↔ M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

Tactic:
by
  rw [mapEmbedding, map_indep_iff]
  refine ⟨?_, fun ⟨h,h'⟩ ↦ ⟨f ⁻¹' I, h, by rwa [eq_comm, image_preimage_eq_iff]⟩⟩
  rintro ⟨I, hI, rfl⟩
  rw [preimage_image_eq _ f.injective]
  exact ⟨hI, image_subset_range _ _⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsLoop e ↔ ∀ (B : Set α), M.IsBase B → e ∉ B

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsLoop e ↔ ∀ (B : Set α), M.IsBase B → e ∉ B
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ (M ↾ R).fundCircuit e I = M.fundCircuit e I

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ (M ↾ R).fundCircuit e I = M.fundCircuit e I
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
⊢ M.E = N.E

Tactic:
hN

Goal state after:
α : Type u_1
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
⊢ M.E = M.E
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.closure {e} = M.loops ∧ e ∈ M.E ↔ M.closure {e} = M.loops

Tactic:
and_iff_left he

Goal state after:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.closure {e} = M.loops ↔ M.closure {e} = M.loops
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
h : ¬M.IsNonloop e
⊢ M.IsLoop e

Tactic:
rwa [isNonloop_iff, and_iff_left he, not_not] at h

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

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

Tactic:
exact hB.nonempty

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsLoop e ∨ ¬M.IsLoop e ∧ e ∈ M.E

Tactic:
and_iff_left he

Goal state after:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsLoop e ∨ ¬M.IsLoop e
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ e ∉ M.loops ∧ e ∈ M.E ↔ e ∉ M.loops

Tactic:
and_iff_left he

Goal state after:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ e ∉ M.loops ↔ e ∉ M.loops
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I ↔ (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I ↔ (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Circuit

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

Tactic:
[

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

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

Tactic:
rw [Indep.insert_indep_iff_of_notMem (by simpa) (by simpa)]

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
⊢ e ∉ M.E \ M.closure {f}
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.closure {e} = M.closure {f} ↔ e = f ∨ ¬M.Indep {e, f}

Tactic:
[

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.eRank = ⊤ ↔ ¬M.RankFinite

Tactic:
← eRank_ne_top_iff,

Goal state after:
α : Type u_1
M : Matroid α
⊢ M.eRank = ⊤ ↔ ¬M.eRank ≠ ⊤
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
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}
⊢ M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B

Tactic:
[

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}
⊢ M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
inst✝ : M.RankFinite
⊢ M.Indep I ↔ M.eRk I = I.encard

Tactic:
by
  refine ⟨Indep.eRk_eq_encard, fun h ↦ ?_⟩
  obtain hfin | hinf := I.finite_or_infinite
  · rwa [indep_iff_eRk_eq_encard_of_finite hfin]
  rw [hinf.encard_eq] at h
  exact False.elim <| (M.isRkFinite_set I).eRk_lt_top.ne h

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

Goal state before:
pp: α : Type u_2
M : Matroid α
ι : Type u_3
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ i, Fs i)
hIX : M.IsBasis I X
i : ι
J : Set α
hIJ : M.IsBasis J (Fs i)
hJ : I ⊆ J
⊢ X ⊆ Fs i

Tactic:
refine subset_union_right.trans ((hFs i).1 (X := Fs i ∪ X) hIJ ?_)

Goal state after:
α : Type u_2
M : Matroid α
ι : Type u_3
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ i, Fs i)
hIX : M.IsBasis I X
i : ι
J : Set α
hIJ : M.IsBasis J (Fs i)
hJ : I ⊆ J
⊢ M.IsBasis J (Fs i ∪ X)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_6
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
hwin : ∃ C' ⊆ (C₀ ∪ ⋃ i, C ↑i) \ range fun x ↦ ↑x, M.IsCircuit C' ∧ z ∈ C'
⊢ ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'

Tactic:
obtain ⟨C', hC'ss, hC', hz⟩ := hwin
    refine ⟨C', hC'ss.trans (sdiff_subset_sdiff (union_subset_union_right _ ?_) (by simp)), hC', hz⟩
    simpa using fun e heX ↦ (subset_sUnion_of_mem (hC.1 e heX))

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

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

Tactic:
[

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.closure (X ∩ M.E) = M.closure X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
⊢ X ∩ M.E ⊆ M.closure X

Tactic:
[

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
⊢ X ∩ M.E ⊆ M.closure X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
X : Set α
hX : X ⊆ M.E
⊢ e ∈ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F

Tactic:
[

Goal state after:
α : Type u_2
M : Matroid α
e : α
X : Set α
hX : X ⊆ M.E
⊢ e ∈ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
Y X : Set α
hX : X ⊆ M.E
⊢ Y ⊆ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F

Tactic:
[

Goal state after:
α : Type u_2
M : Matroid α
Y X : Set α
hX : X ⊆ M.E
⊢ Y ⊆ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsColoop e ↔ ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsColoop e ↔ ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C

Tactic:
and_iff_left he

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
x✝ : (∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X) ∧ e ∈ M.E
h : ∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
X : Set α
⊢ e ∈ X ∧ e ∈ M.E ↔ e ∈ X

Tactic:
and_iff_left he

Goal state after:
α : Type u_1
M : Matroid α
e : α
x✝ : (∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X) ∧ e ∈ M.E
h : ∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
X : Set α
⊢ e ∈ X ↔ e ∈ X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
⊢ M.IsColoop e ↔ M.closure (M.E \ {e}) ≠ M.E

Tactic:
rw [isColoop_iff_sdiff_not_spanning, spanning_iff_closure_eq]

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

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

Tactic:
[

Goal state after:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ M.closure (⋃ i, M.closure (Xs i)) = M.closure (⋃ i, Xs i)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
eRank_loopyOn

Goal state after:
α : Type u_1
M : Matroid α
h : M = loopyOn M.E
⊢ 0 = 0
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure X ∩ M.coloops = X ∩ M.coloops

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure X ∩ M.coloops = X ∩ M.coloops
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X Y : Set α
⊢ M.closure (⋃ i, M.closure (bif i then X else Y)) = M.closure (⋃ b, bif b then M.closure X else M.closure Y)

Tactic:
[

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

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

Tactic:
[

Goal state after:
α : Type u_2
M : Matroid α
e : α
X : Set α
⊢ M.closure (insert e (M.closure X)) = M.closure (insert e X)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
X : Set α
κ : Cardinal.{u}
⊢ M.cRk X ≤ κ ↔ ∀ ⦃I : Set α⦄, M.IsBasis' I X → #↑I ≤ κ

Tactic:
[

Goal state after:
α : Type u
M : Matroid α
X : Set α
κ : Cardinal.{u}
⊢ M.cRk X ≤ κ ↔ ∀ ⦃I : Set α⦄, M.IsBasis' I X → #↑I ≤ κ
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
⊢ ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y

Tactic:
[

Goal state after:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
⊢ ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
aux : ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y
⊢ (M ↾ X).cRk Y = M.cRk Y

Tactic:
[

Goal state after:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
aux : ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y
⊢ (M ↾ X).cRk Y = M.cRk Y
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case inl
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I

Tactic:
[

Goal state after:
case inl
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun X ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
X : Set α
hX : ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty
B : Set α
hB : M.IsBase B
⊢ (X ∩ (M.E ∩ B)).Nonempty

Tactic:
inter_eq_self_of_subset_right hB.subset_ground

Goal state after:
α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun X ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
X : Set α
hX : ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty
B : Set α
hB : M.IsBase B
⊢ (X ∩ B).Nonempty
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case e'_2
α : Type u_1
M : Matroid α
K✝ K : Set α
⊢ (¬∃ B, M.IsBase B ∧ B ⊆ M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty

Tactic:
[

Goal state after:
case e'_2
α : Type u_1
M : Matroid α
K✝ K : Set α
⊢ (¬∃ B, M.IsBase B ∧ B ⊆ M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ M.closure B = M.E

Tactic:
rw [← isBasis_ground_iff] at hB; rw [hB.closure_eq_closure, closure_ground]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
he : C ∩ K = {e}
heC : e ∈ C
⊢ False

Tactic:
[

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
he : C ∩ K = {e}
heC : e ∈ C
⊢ False
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
⊢ e ∈ M✶.closure (M.E \ B)

Tactic:
rw [hB.compl_isBase_dual.closure_eq, dual_ground]

Goal state after:
α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
⊢ e ∈ M.E
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
⊢ Transcendental R ((Polynomial.aeval (X i)) f) → Transcendental R f

Tactic:
[

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
⊢ Transcendental R ((Polynomial.aeval (X i)) f) → Transcendental R f
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
x✝¹ x✝ : R
heq : (algebraMap R ↥(supported R s)) x✝¹ = (algebraMap R ↥(supported R s)) x✝
⊢ C x✝¹ = C x✝

Tactic:
[

Goal state after:
case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
x✝¹ x✝ : R
heq : (algebraMap R ↥(supported R s)) x✝¹ = (algebraMap R ↥(supported R s)) x✝
⊢ C x✝¹ = C x✝