awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hle : B.encard ≤ I.encard
x : α
hxnot : x ∉ I
hxI : Indep (insert x I)
rwa : I.encard ≠ ⊤
⊢ B.encard < (insert x I).encard

Tactic:
rwa [encard_insert_of_notMem hxnot, ← not_le, ENat.add_one_le_iff, not_lt]

Premises used: not_le, ENat.add_one_le_iff, not_lt, Set.encard_insert_of_notMem
-- 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 → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hle : B.encard ≤ I.encard
x : α
hxnot : x ∉ I
hxI : Indep (insert x I)
rw : I.Finite
⊢ I.encard ≠ ⊤

Tactic:
rw [encard_ne_top_iff]

Premises used: Set.encard_ne_top_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 → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hle : B.encard ≤ I.encard
x : α
hxnot : x ∉ I
hxI : Indep (insert x I)
obtain : ∀ (n : ℕ) (hn : ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)), I.Finite
⊢ I.Finite

Tactic:
obtain ⟨n, hn⟩ := indep_bdd
-- 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 → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hle : B.encard ≤ I.encard
x : α
hxnot : x ∉ I
hxI : Indep (insert x I)
n : ℕ
hn : ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)
⊢ I.Finite

Tactic:
finite_of_encard_le_coe (hn _ hI)

Premises used: Set.finite_of_encard_le_coe
-- 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 → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hle : B.encard ≤ I.encard
x : α
hxnot : x ∉ I
hxI : Indep (insert x I)
n : ℕ
hn : ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)
⊢ I.Finite

Tactic:
exact finite_of_encard_le_coe (hn _ hI)

Premises used: Set.finite_of_encard_le_coe
-- 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 → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hle : B.encard ≤ I.encard
x : α
hxnot : x ∉ I
hxI : Indep (insert x I)
⊢ B.encard < (insert x I).encard

Tactic:
have hlt : B.encard < (insert x I).encard := by
        rwa [encard_insert_of_notMem hxnot, ← not_le, ENat.add_one_le_iff, not_lt]
        rw [encard_ne_top_iff]
        obtain ⟨n, hn⟩ := indep_bdd
        exact finite_of_encard_le_coe (hn _ hI)
-- 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 → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hle : B.encard ≤ I.encard
x : α
hxnot : x ∉ I
hxI : Indep (insert x I)
hlt : B.encard < (insert x I).encard
obtain : ∀ (y : α) (hyB : y ∉ B) (hi : Indep (insert y B)), False
⊢ False

Tactic:
obtain ⟨y, -, hyB, hi⟩ := indep_aug hBmax.prop hxI hlt

Premises used: Maximal.prop
-- 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 → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hle : B.encard ≤ I.encard
x : α
hxnot : x ∉ I
hxI : Indep (insert x I)
hlt : B.encard < (insert x I).encard
y : α
hyB : y ∉ B
hi : Indep (insert y B)
⊢ False

Tactic:
hBmax.not_prop_of_ssuperset (ssubset_insert hyB) hi

Premises used: Set.ssubset_insert, Maximal.not_prop_of_ssuperset
-- 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 → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hle : B.encard ≤ I.encard
x : α
hxnot : x ∉ I
hxI : Indep (insert x I)
hlt : B.encard < (insert x I).encard
y : α
hyB : y ∉ B
hi : Indep (insert y B)
⊢ False

Tactic:
exact hBmax.not_prop_of_ssuperset (ssubset_insert hyB) hi

Premises used: Set.ssubset_insert, Maximal.not_prop_of_ssuperset
-- 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 → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
⊢ (IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd subset_ground).E = E

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 J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
⊢ (IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd 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 J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
⊢ (IndepMatroid.ofBdd E Indep indep_empty indep_subset ⋯ subset_ground indep_bdd).matroid.RankFinite

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
hE : E.Finite
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
⊢ ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)

Tactic:
fun {I J} hI hJ hIJ ↦ indep_aug hI hJ ?_
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
hE : E.Finite
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
refine : ∀ {I J : Set α} (hI : Indep I) (hJ : Indep J) (hIJ : I.encard < J.encard), I.ncard < J.ncard
⊢ ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)

Tactic:
refine fun {I J} hI hJ hIJ ↦ indep_aug hI hJ ?_
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
hE : E.Finite
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
I J : Set α
hI : Indep I
hJ : Indep J
hIJ : I.encard < J.encard
rwa : LT.lt (α := ℕ∞) (↑I.ncard : ℕ∞) (↑J.ncard : ℕ∞)
rwa₁ : (↑I.ncard : ℕ∞) < J.encard
rwa₂ rwa₃ rwa₄ rwa₅ : I.encard < J.encard
⊢ I.ncard < J.ncard

Tactic:
rwa [← Nat.cast_lt (α := ℕ∞), (hE.subset (subset_ground hJ)).cast_ncard_eq,
        (hE.subset (subset_ground hI)).cast_ncard_eq]

Premises used: Set.Finite.subset, Nat.cast_lt, Set.Finite.cast_ncard_eq
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
hE : E.Finite
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
I : Set α
hI : Indep I
rw : I.encard ≤ E.encard
⊢ I.encard ≤ (↑E.ncard : ℕ∞)

Tactic:
rw [hE.cast_ncard_eq]

Premises used: Set.Finite.cast_ncard_eq
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
hE : E.Finite
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
I : Set α
hI : Indep I
⊢ I.encard ≤ E.encard

Tactic:
encard_le_encard <| subset_ground hI

Premises used: Set.encard_le_encard
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
hE : E.Finite
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
I : Set α
hI : Indep I
⊢ I.encard ≤ E.encard

Tactic:
exact encard_le_encard <| subset_ground hI

Premises used: Set.encard_le_encard
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
hE : E.Finite
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
⊢ (IndepMatroid.ofFinite (E := E) hE Indep indep_empty indep_subset indep_aug subset_ground).E = E

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
hE : E.Finite
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
⊢ (IndepMatroid.ofFinite (E := E) hE Indep indep_empty indep_subset indep_aug subset_ground).Indep = Indep

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
hE : E.Finite
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Set α⦄, Indep I → I ⊆ E
⊢ (IndepMatroid.ofFinite (E := E) hE Indep indep_empty indep_subset indep_aug subset_ground).matroid.Finite

Tactic:
⟨hE⟩

Premises used: Matroid.Finite.mk
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
inst : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → (↑I : Set α) ⊆ E
⊢ (fun (I : Set α) ↦ ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J) ∅

Tactic:
simpa [subset_empty_iff]

Premises used: Set.subset_empty_iff
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
inst : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → (↑I : Set α) ⊆ E
I J : Set α
hI : ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), (↑J_1 : Set α) ⊆ J → Indep J_1
hJfin : J.Finite
hIJ : I.ncard < J.ncard
⊢ hIfin.toFinset (s := I).card < hJfin.toFinset (s := J).card

Tactic:
rw [ncard_eq_toFinset_card _ hIfin, ncard_eq_toFinset_card _ hJfin] at hIJ

Premises used: Set.ncard_eq_toFinset_card
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
inst : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → (↑I : Set α) ⊆ E
I J : Set α
hI : ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), (↑J_1 : Set α) ⊆ J → Indep J_1
hJfin : J.Finite
hIJ : hIfin.toFinset (s := I).card < hJfin.toFinset (s := J).card
⊢ (↑(hIfin.toFinset (s := I)) : Set α) ⊆ I

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
inst : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → (↑I : Set α) ⊆ E
I J : Set α
hI : ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), (↑J_1 : Set α) ⊆ J → Indep J_1
hJfin : J.Finite
hIJ : hIfin.toFinset (s := I).card < hJfin.toFinset (s := J).card
⊢ (↑(hJfin.toFinset (s := J)) : Set α) ⊆ J

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
inst : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → (↑I : Set α) ⊆ E
I J : Set α
hI : ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), (↑J_1 : Set α) ⊆ J → Indep J_1
hJfin : J.Finite
hIJ : hIfin.toFinset (s := I).card < hJfin.toFinset (s := J).card
⊢ ∃ e ∈ hJfin.toFinset (s := J), e ∉ hIfin.toFinset (s := I) ∧ Indep (insert e (hIfin.toFinset (s := I)))

Tactic:
have aug := indep_aug (hI _ (by simp)) (hJ _ (by simp)) hIJ
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
inst : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → (↑I : Set α) ⊆ E
I J : Set α
hI : ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), (↑J_1 : Set α) ⊆ J → Indep J_1
hJfin : J.Finite
hIJ : hIfin.toFinset (s := I).card < hJfin.toFinset (s := J).card
aug : ∃ e ∈ hJfin.toFinset (s := J), e ∉ hIfin.toFinset (s := I) ∧ Indep (insert e (hIfin.toFinset (s := I)))
⊢ ∃ e ∈ J, e ∉ I ∧ Indep (insert e (hIfin.toFinset (s := I)))

Tactic:
simp only [Finite.mem_toFinset] at aug

Premises used: Set.Finite.mem_toFinset
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
inst : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → (↑I : Set α) ⊆ E
I J : Set α
hI : ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), (↑J_1 : Set α) ⊆ J → Indep J_1
hJfin : J.Finite
hIJ : hIfin.toFinset (s := I).card < hJfin.toFinset (s := J).card
aug : ∃ e ∈ J, e ∉ I ∧ Indep (insert e (hIfin.toFinset (s := I)))
obtain :
  ∀ (e : α) (heJ : e ∈ J) (heI : e ∉ I) (hi : Indep (insert e (hIfin.toFinset (s := I)))),
    ∃ e ∈ J, e ∉ I ∧ (fun (I : Set α) ↦ ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J) (insert e I)
⊢ ∃ e ∈ J, e ∉ I ∧ (fun (I : Set α) ↦ ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J) (insert e I)

Tactic:
obtain ⟨e, heJ, heI, hi⟩ := aug
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
inst : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → (↑I : Set α) ⊆ E
I J : Set α
hI : ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), (↑J_1 : Set α) ⊆ J → Indep J_1
hJfin : J.Finite
hIJ : hIfin.toFinset (s := I).card < hJfin.toFinset (s := J).card
e : α
heJ : e ∈ J
heI : e ∉ I
hi : Indep (insert e (hIfin.toFinset (s := I)))
K : Finset α
hK : (↑K : Set α) ⊆ insert e I
⊢ (↑K : Set α) ⊆ (↑(insert e (hIfin.toFinset (s := I))) : Set α)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
inst : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → (↑I : Set α) ⊆ E
I J : Set α
hI : ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), (↑J_1 : Set α) ⊆ J → Indep J_1
hJfin : J.Finite
hIJ : hIfin.toFinset (s := I).card < hJfin.toFinset (s := J).card
e : α
heJ : e ∈ J
heI : e ∉ I
hi : Indep (insert e (hIfin.toFinset (s := I)))
⊢ ∃ e ∈ J, e ∉ I ∧ (fun (I : Set α) ↦ ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J) (insert e I)

Tactic:
exact ⟨e, heJ, heI, fun K hK ↦ indep_subset hi <| Finset.coe_subset.1 (by simpa)⟩
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
inst : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → (↑I : Set α) ⊆ E
I : Set α
hI : (fun (I : Set α) ↦ ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J) I
x : α
hxI : x ∈ I
⊢ (↑{x} : Set α) ⊆ I

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
inst : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → (↑I : Set α) ⊆ E
I : Set α
hI : (fun (I : Set α) ↦ ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J) I
x : α
hxI : x ∈ I
⊢ x ∈ E

Tactic:
simpa using subset_ground <| hI {x} (by simpa)

Premises used: Singleton.singleton
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
inst : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → (↑I : Set α) ⊆ E
⊢ (IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).E = E

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
inst : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → (↑I : Set α) ⊆ E
I : Finset α
⊢ (∀ J ⊆ I, Indep J) ↔ Indep I

Tactic:
⟨fun h ↦ h _ Subset.rfl, fun h J hJI ↦ indep_subset h hJI⟩

Premises used: Set.Subset.rfl, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
inst : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → (↑I : Set α) ⊆ E
I : Finset α
⊢ (∀ J ⊆ I, Indep J) ↔ Indep I

Tactic:
exact ⟨fun h ↦ h _ Subset.rfl, fun h J hJI ↦ indep_subset h hJI⟩
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
inst : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → (↑I : Set α) ⊆ E
I : Set α
⊢ (IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).Indep I ↔
    ∀ (J : Finset α), (↑J : Set α) ⊆ I → Indep J

Tactic:
simp only [IndepMatroid.ofFinset, ofFinitaryCardAugment_indep]

Premises used: IndepMatroid.ofFinset, IndepMatroid.ofFinitaryCardAugment_indep
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
hM : ∃ (M : Matroid α), E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I
obtain :
  ∀ (M : Matroid α) (h : ∀ (I : Set α), M.Indep I ↔ Indep I), ∃ (M_1 : Matroid α), M.E = M_1.E ∧ M_1.Indep = Indep
⊢ ∃ (M : Matroid α), E = M.E ∧ M.Indep = Indep

Tactic:
obtain ⟨M, rfl, h⟩ := hM

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
Indep : Set α → Prop
M : Matroid α
h : ∀ (I : Set α), M.Indep I ↔ Indep I
⊢ ∀ (x : Set α), M.Indep x = Indep x

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
Indep : Set α → Prop
M : Matroid α
h : ∀ (I : Set α), M.Indep I ↔ Indep I
⊢ ∃ (M_1 : Matroid α), M.E = M_1.E ∧ M_1.Indep = Indep

Tactic:
refine ⟨_, rfl, funext (by simp [h])⟩
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
E : Set α
Indep : Set α → Prop
hM : ∃ (M : Matroid α), E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I
hex : ∃ (M : Matroid α), E = M.E ∧ M.Indep = Indep
obtain : ∀ (M : Matroid α) (hM : ∃ (M_1 : Matroid α), E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I), M.Indep ∅
⊢ Indep ∅

Tactic:
obtain ⟨M, -, rfl⟩ := hex

Premises used: rfl