awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
hnot : ¬Maximal M.Indep (insert f (B \ {e}))
x : α
hxB : x ∈ B \ insert f (B \ {e})
hind : M.Indep (insert x (insert f (B \ {e})))
he₁ : x ∈ B \ B'
hnotmax₁ : ¬Maximal M.Indep (B \ {x})
hfB₁ : M.Indep (insert f (B \ {x}))
hnot₁ : ¬Maximal M.Indep (insert f (B \ {x}))
⊢ x ∈ B \ insert f (B \ {x})

Tactic:
obtain ⟨-, rfl⟩ : _ ∧ x = e := by simpa [hxB.1] using hxB

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
hnot : ¬Maximal M.Indep (insert f (B \ {e}))
x : α
hxB : x ∈ B \ insert f (B \ {e})
hind : M.Indep (insert x (insert f (B \ {e})))
he₁ : x ∈ B \ B'
hnotmax₁ : ¬Maximal M.Indep (B \ {x})
hfB₁ : M.Indep (insert f (B \ {x}))
hnot₁ : ¬Maximal M.Indep (insert f (B \ {x}))
hxB₁ : x ∈ B \ insert f (B \ {x})
⊢ M.Indep (insert x (insert f (B \ {x})))

Tactic:
obtain ⟨-, rfl⟩ : _ ∧ x = e := by simpa [hxB.1] using hxB

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
f : α
hf : f ∈ B' \ B
x : α
he : x ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {x})
hfB : M.Indep (insert f (B \ {x}))
hnot : ¬Maximal M.Indep (insert f (B \ {x}))
hxB : x ∈ B \ insert f (B \ {x})
hind : M.Indep (insert x (insert f (B \ {x})))
⊢ False

Tactic:
hB.not_prop_of_ssuperset ?_ hind

Premises used: Maximal.not_prop_of_ssuperset
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
f : α
hf : f ∈ B' \ B
x : α
he : x ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {x})
hfB : M.Indep (insert f (B \ {x}))
hnot : ¬Maximal M.Indep (insert f (B \ {x}))
hxB : x ∈ B \ insert f (B \ {x})
hind : M.Indep (insert x (insert f (B \ {x})))
refine : B ⊂ insert x (insert f (B \ {x}))
⊢ False

Tactic:
refine hB.not_prop_of_ssuperset ?_ hind

Premises used: Maximal.not_prop_of_ssuperset
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
f : α
hf : f ∈ B' \ B
x : α
he : x ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {x})
hfB : M.Indep (insert f (B \ {x}))
hnot : ¬Maximal M.Indep (insert f (B \ {x}))
hxB : x ∈ B \ insert f (B \ {x})
hind : M.Indep (insert x (insert f (B \ {x})))
rw : B ⊂ insert f B
⊢ B ⊂ insert x (insert f (B \ {x}))

Tactic:
rw [insert_comm, insert_diff_singleton, insert_eq_of_mem he.1]

Premises used: Set.insert_eq_of_mem, Set.insert_comm, And.left, Set.insert_diff_singleton
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
f : α
hf : f ∈ B' \ B
x : α
he : x ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {x})
hfB : M.Indep (insert f (B \ {x}))
hnot : ¬Maximal M.Indep (insert f (B \ {x}))
hxB : x ∈ B \ insert f (B \ {x})
hind : M.Indep (insert x (insert f (B \ {x})))
⊢ B ⊂ insert f B

Tactic:
ssubset_insert hf.2

Premises used: Set.ssubset_insert, And.right
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
f : α
hf : f ∈ B' \ B
x : α
he : x ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {x})
hfB : M.Indep (insert f (B \ {x}))
hnot : ¬Maximal M.Indep (insert f (B \ {x}))
hxB : x ∈ B \ insert f (B \ {x})
hind : M.Indep (insert x (insert f (B \ {x})))
⊢ B ⊂ insert f B

Tactic:
exact ssubset_insert hf.2

Premises used: Set.ssubset_insert, And.right
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
M : IndepMatroid α
I : Set α
⊢ M.matroid.Indep I ↔ M.Indep I

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty Indep X

Tactic:
fun X _ I hI hIX ↦ zorn_subset_nonempty {Y | Indep Y ∧ Y ⊆ X} ?_ I ⟨hI, hIX⟩

Premises used: Matroid.ExistsMaximalSubsetProperty, Set.Mem, setOf, HasSubset.Subset, And, zorn_subset_nonempty, And.intro
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
refine :
  ∀ X ⊆ E,
    ∀ (I : Set α) (hI : Indep I) (hIX : I ⊆ X),
      ∀ c ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X},
        IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c →
          c.Nonempty →
            ∃ (ub : Set α), Membership.mem (γ := Set (Set α)) {Y : Set α | Indep Y ∧ Y ⊆ X} ub ∧ ∀ s ∈ c, s ⊆ ub
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty Indep X

Tactic:
refine fun X _ I hI hIX ↦ zorn_subset_nonempty {Y | Indep Y ∧ Y ⊆ X} ?_ I ⟨hI, hIX⟩

Premises used: setOf, HasSubset.Subset, And, zorn_subset_nonempty, And.intro
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
⊢ ∀ c ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X},
    IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c →
      c.Nonempty → ∃ (ub : Set α), Membership.mem (γ := Set (Set α)) {Y : Set α | Indep Y ∧ Y ⊆ X} ub ∧ ∀ s ∈ c, s ⊆ ub

Tactic:
fun Is hIs hchain _ ↦
      ⟨⋃₀ Is, ⟨?_, sUnion_subset fun Y hY ↦ (hIs hY).2⟩, fun _ ↦ subset_sUnion_of_mem⟩

Premises used: Set.sUnion, Set.sUnion_subset, And.right, And.intro, Exists.intro, Set.subset_sUnion_of_mem
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
refine :
  ∀ (Is : Set (Set α)) (hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}) (hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is),
    Is.Nonempty → Indep (⋃₀ Is)
⊢ ∀ c ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X},
    IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c →
      c.Nonempty → ∃ (ub : Set α), Membership.mem (γ := Set (Set α)) {Y : Set α | Indep Y ∧ Y ⊆ X} ub ∧ ∀ s ∈ c, s ⊆ ub

Tactic:
refine fun Is hIs hchain _ ↦
      ⟨⋃₀ Is, ⟨?_, sUnion_subset fun Y hY ↦ (hIs hY).2⟩, fun _ ↦ subset_sUnion_of_mem⟩
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
⊢ Indep (⋃₀ Is)

Tactic:
indep_compact _ fun J hJ hJfin ↦ ?_
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
refine : ∀ (J : Set α) (hJ : J ⊆ ⋃₀ Is) (hJfin : J.Finite), Indep J
⊢ Indep (⋃₀ Is)

Tactic:
refine indep_compact _ fun J hJ hJfin ↦ ?_
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
have : ∀ (hchoose : ∀ e ∈ J, ∃ I ∈ Is, e ∈ I), Indep J
⊢ Indep J

Tactic:
have hchoose : ∀ e, e ∈ J → ∃ I, I ∈ Is ∧ (e : α) ∈ I := fun _ he ↦ mem_sUnion.1 <| hJ he
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
hchoose : ∀ e ∈ J, ∃ I ∈ Is, e ∈ I
choose! : ∀ (f : (e : α) → Set α) (hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e), Indep J
⊢ Indep J

Tactic:
choose! f hf using hchoose
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : (e : α) → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
⊢ Indep J

Tactic:
J.eq_empty_or_nonempty.elim (fun hJ ↦ hJ ▸ indep_empty) (fun hne ↦ ?_)

Premises used: Eq.rec, Set.eq_empty_or_nonempty, Or.elim, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : (e : α) → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
⊢ J.Nonempty

Tactic:
refine J.eq_empty_or_nonempty.elim (fun hJ ↦ hJ ▸ indep_empty) (fun hne ↦ ?_)

Premises used: Set.eq_empty_or_nonempty, Or.elim
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : (e : α) → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
obtain : ∀ (x : α) (hxJ : x ∈ J) (hxmax : ∀ ⦃j : α⦄, (fun (x : α) ↦ x ∈ J) j → f x ≤ f j → f j ≤ f x), Indep J
⊢ Indep J

Tactic:
obtain ⟨x, hxJ, hxmax⟩ := Finite.exists_maximalFor f _ hJfin hne

Premises used: Set.Finite.exists_maximalFor
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : (e : α) → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun (x : α) ↦ x ∈ J) j → f x ≤ f j → f j ≤ f x
⊢ Indep J

Tactic:
indep_subset (hIs (hf x hxJ).1).1 fun y hyJ ↦ ?_

Premises used: And.left
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : (e : α) → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun (x : α) ↦ x ∈ J) j → f x ≤ f j → f j ≤ f x
refine : ∀ (y : α) (hyJ : y ∈ J), y ∈ f x
⊢ Indep J

Tactic:
refine indep_subset (hIs (hf x hxJ).1).1 fun y hyJ ↦ ?_

Premises used: And.left
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : (e : α) → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun (x : α) ↦ x ∈ J) j → f x ≤ f j → f j ≤ f x
y : α
hyJ : y ∈ J
inl : ∀ (hle : f x ⊆ f y), y ∈ f x
inr : ∀ (hle : f y ⊆ f x), y ∈ f x
⊢ y ∈ f x

Tactic:
obtain (hle | hle) := hchain.total (hf _ hxJ).1 (hf _ hyJ).1

Premises used: And.left, IsChain.total
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : (e : α) → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun (x : α) ↦ x ∈ J) j → f x ≤ f j → f j ≤ f x
y : α
hyJ : y ∈ J
hle : f x ⊆ f y
⊢ y ∈ f x

Tactic:
hxmax hyJ hle <| (hf _ hyJ).2

Premises used: And.right
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : (e : α) → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun (x : α) ↦ x ∈ J) j → f x ≤ f j → f j ≤ f x
y : α
hyJ : y ∈ J
hle : f x ⊆ f y
⊢ y ∈ f x

Tactic:
exact hxmax hyJ hle <| (hf _ hyJ).2

Premises used: And.right
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : (e : α) → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun (x : α) ↦ x ∈ J) j → f x ≤ f j → f j ≤ f x
y : α
hyJ : y ∈ J
hle : f y ⊆ f x
⊢ y ∈ f x

Tactic:
hle (hf _ hyJ).2

Premises used: And.right
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : (e : α) → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun (x : α) ↦ x ∈ J) j → f x ≤ f j → f j ≤ f x
y : α
hyJ : y ∈ J
hle : f y ⊆ f x
⊢ y ∈ f x

Tactic:
exact hle (hf _ hyJ).2

Premises used: And.right
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
⊢ (IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).Indep = Indep

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
⊢ ∀ (I : Set α),
    (∀ J ⊆ I,
        J.Finite →
          (IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).matroid.Indep
            J) →
      (IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).matroid.Indep I

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
by_contra! :
  ∀ (I : Set α) (e : α) (hIe : ¬Indep (insert e I))
    (h : ∀ (I₀ : Set α) (_ : I₀ ⊆ I) (_ : I₀.Finite), Indep (insert e I₀)), False
⊢ ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)

Tactic:
by_contra! ⟨I, e, -, hIe, h⟩
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I : Set α
e : α
hIe : ¬Indep (insert e I)
h : ∀ (I₀ : Set α) (_ : I₀ ⊆ I) (_ : I₀.Finite), Indep (insert e I₀)
⊢ False

Tactic:
hIe <| indep_compact _ fun J hJss hJfin ↦ ?_
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I : Set α
e : α
hIe : ¬Indep (insert e I)
h : ∀ (I₀ : Set α) (_ : I₀ ⊆ I) (_ : I₀.Finite), Indep (insert e I₀)
refine : ∀ (J : Set α) (hJss : J ⊆ insert e I) (hJfin : J.Finite), Indep J
⊢ False

Tactic:
refine hIe <| indep_compact _ fun J hJss hJfin ↦ ?_
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I : Set α
e : α
hIe : ¬Indep (insert e I)
h : ∀ (I₀ : Set α) (_ : I₀ ⊆ I) (_ : I₀.Finite), Indep (insert e I₀)
J : Set α
hJss : J ⊆ insert e I
hJfin : J.Finite
rwa rwa₁ rwa₂ rwa₃ : J ⊆ {e} ∪ I
⊢ J \ {e} ⊆ I

Tactic:
rwa [diff_subset_iff]

Premises used: Set.diff_subset_iff
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I : Set α
e : α
hIe : ¬Indep (insert e I)
h : ∀ (I₀ : Set α) (_ : I₀ ⊆ I) (_ : I₀.Finite), Indep (insert e I₀)
J : Set α
hJss : J ⊆ insert e I
hJfin : J.Finite
⊢ J ⊆ insert e (J \ {e})

Tactic:
simp