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 → 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
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ (x : α) (_ : x ∈ B \ I), ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
E₀ : Set α := insert e (I₀ ∪ B₀)
hE₀fin : E₀.Finite
J : Set α
hJmax :
  ∀ ⦃j : Set α⦄,
    (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {J : Set α | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀} x) j →
      id J ≤ id j → id j ≤ id J
hB₀J : B₀ ⊆ J
hJ : Indep J
hJss : J ⊆ E₀
heI₀ : e ∉ I₀
heI₀i : Indep (insert e I₀)
heJ : e ∉ J
hJfin : J.Finite
hcard : I₀.ncard < J.ncard
neg : ∀ (f : α) (hfJ : f ∈ J) (hfI₀ : f ∉ I₀) (hfi : Indep (insert f I₀)), False
⊢ False

Tactic:
obtain ⟨f, hfJ, hfI₀, hfi⟩ := indep_aug (indep_subset hI hI₀I) hI₀fin hJ hJfin hcard
-- 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
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ (x : α) (_ : x ∈ B \ I), ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
E₀ : Set α := insert e (I₀ ∪ B₀)
hE₀fin : E₀.Finite
J : Set α
hJmax :
  ∀ ⦃j : Set α⦄,
    (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {J : Set α | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀} x) j →
      id J ≤ id j → id j ≤ id J
hB₀J : B₀ ⊆ J
hJ : Indep J
hJss : J ⊆ E₀
heI₀ : e ∉ I₀
heI₀i : Indep (insert e I₀)
heJ : e ∉ J
hJfin : J.Finite
hcard : I₀.ncard < J.ncard
f : α
hfJ : f ∈ J
hfI₀ : f ∉ I₀
hfi : Indep (insert f I₀)
⊢ f ∈ I₀ ∪ B₀ → f ∈ B₀

Tactic:
aesop
-- 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
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ (x : α) (_ : x ∈ B \ I), ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
E₀ : Set α := insert e (I₀ ∪ B₀)
hE₀fin : E₀.Finite
J : Set α
hJmax :
  ∀ ⦃j : Set α⦄,
    (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {J : Set α | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀} x) j →
      id J ≤ id j → id j ≤ id J
hB₀J : B₀ ⊆ J
hJ : Indep J
hJss : J ⊆ E₀
heI₀ : e ∉ I₀
heI₀i : Indep (insert e I₀)
heJ : e ∉ J
hJfin : J.Finite
hcard : I₀.ncard < J.ncard
f : α
hfJ : f ∈ J
hfI₀ : f ∉ I₀
hfi : Indep (insert f I₀)
⊢ False

Tactic:
exact hI₀ f ⟨Or.elim (hJss hfJ) (fun hfe ↦ (heJ <| hfe ▸ hfJ).elim) (by aesop), hfI₀⟩ hfi

Premises used: False.elim, Eq.rec, And.intro, 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 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
⊢ (IndepMatroid.ofFinitaryCardAugment 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 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 α),
    (∀ J ⊆ I,
        J.Finite →
          (IndepMatroid.ofFinitaryCardAugment E Indep indep_empty indep_subset indep_aug indep_compact
                  subset_ground).matroid.Indep
            J) →
      (IndepMatroid.ofFinitaryCardAugment 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
P : Set α → Prop
hP : ∃ (n : ℕ), ∀ (Y : Set α), P Y → Y.encard ≤ (↑n : ℕ∞)
X : Set α
obtain : ∀ (n : ℕ) (hP : ∀ (Y : Set α), P Y → Y.encard ≤ (↑n : ℕ∞)), ExistsMaximalSubsetProperty P X
⊢ ExistsMaximalSubsetProperty P X

Tactic:
obtain ⟨n, hP⟩ := hP
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ (↑n : ℕ∞)
I : Set α
hI : P I
hIX : I ⊆ X
rw : ∃ (x : ℕ), ∀ y ∈ image.{u_1, 0} (α := Set α) ncard {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, y ≤ x
⊢ (image.{u_1, 0} (α := Set α) ncard {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite

Tactic:
rw [finite_iff_bddAbove, bddAbove_def]

Premises used: Set.finite_iff_bddAbove, bddAbove_def
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ (↑n : ℕ∞)
I : Set α
hI : P I
hIX : I ⊆ X
⊢ ∀ (Y : Set α), P Y → ∃ (n₀ : ℕ), Y.encard = (↑n₀ : ℕ∞) ∧ n₀ ≤ n

Tactic:
simp_rw [ENat.le_coe_iff] at hP

Premises used: ENat.le_coe_iff
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
I : Set α
hI : P I
hIX : I ⊆ X
hP : ∀ (Y : Set α), P Y → ∃ (n₀ : ℕ), Y.encard = (↑n₀ : ℕ∞) ∧ n₀ ≤ n
h : ∀ y ∈ image.{u_1, 0} (α := Set α) ncard {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, y ≤ n
⊢ ∃ (x : ℕ), ∀ y ∈ image.{u_1, 0} (α := Set α) ncard {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, y ≤ x

Tactic:
use n
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
I : Set α
hI : P I
hIX : I ⊆ X
hP : ∀ (Y : Set α), P Y → ∃ (n₀ : ℕ), Y.encard = (↑n₀ : ℕ∞) ∧ n₀ ≤ n
Y : Set α
hY : P Y
h : ∀ (n₀ : ℕ) (heq : Y.encard = (↑n₀ : ℕ∞)) (hle : n₀ ≤ n), Y.ncard ≤ n
⊢ Y.ncard ≤ n

Tactic:
obtain ⟨n₀, heq, hle⟩ := hP Y hY
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
I : Set α
hI : P I
hIX : I ⊆ X
hP : ∀ (Y : Set α), P Y → ∃ (n₀ : ℕ), Y.encard = (↑n₀ : ℕ∞) ∧ n₀ ≤ n
Y : Set α
hY : P Y
n₀ : ℕ
heq : Y.encard = (↑n₀ : ℕ∞)
hle : n₀ ≤ n
h : Y.encard.toNat ≤ n
h₁ : ENat.toNat (↑n₀ : ℕ∞) ≤ n
h₂ h₃ h₄ h₅ : n₀ ≤ n
⊢ Y.ncard ≤ n

Tactic:
rwa [ncard_def, heq, ENat.toNat_coe]

Premises used: Set.ncard_def, ENat.toNat_coe
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ (↑n : ℕ∞)
I : Set α
hI : P I
hIX : I ⊆ X
⊢ (image.{u_1, 0} (α := Set α) ncard {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite

Tactic:
have hfin : Set.Finite (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}) := by
    rw [finite_iff_bddAbove, bddAbove_def]
    simp_rw [ENat.le_coe_iff] at hP
    use n
    rintro x ⟨Y, ⟨hY, -, -⟩, rfl⟩
    obtain ⟨n₀, heq, hle⟩ := hP Y hY
    rwa [ncard_def, heq, ENat.toNat_coe]
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ (↑n : ℕ∞)
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (image.{u_1, 0} (α := Set α) ncard {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
obtain :
  ∀ (Y : Set α)
    (hY' :
      ∀ ⦃j : Set α⦄,
        (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X} x) j →
          Y.ncard ≤ j.ncard → j.ncard ≤ Y.ncard)
    (hY : P Y) (hIY : I ⊆ Y) (hYX : Y ⊆ X), ∃ (J : Set α), I ⊆ J ∧ Maximal (fun (K : Set α) ↦ P K ∧ K ⊆ X) J
⊢ ∃ (J : Set α), I ⊆ J ∧ Maximal (fun (K : Set α) ↦ P K ∧ K ⊆ X) J

Tactic:
obtain ⟨Y, ⟨hY, hIY, hYX⟩, hY'⟩ :=
    Finite.exists_maximalFor' ncard _ hfin ⟨I, hI, rfl.subset, hIX⟩

Premises used: Eq.subset, And.intro, Exists.intro, Set.Finite.exists_maximalFor', Set.ncard, rfl
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ (↑n : ℕ∞)
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (image.{u_1, 0} (α := Set α) ncard {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
Y : Set α
hY' :
  ∀ ⦃j : Set α⦄,
    (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X} x) j →
      Y.ncard ≤ j.ncard → j.ncard ≤ Y.ncard
hY : P Y
hIY : I ⊆ Y
hYX : Y ⊆ X
⊢ ∃ (J : Set α), I ⊆ J ∧ Maximal (fun (K : Set α) ↦ P K ∧ K ⊆ X) J

Tactic:
⟨Y, hIY, ⟨hY, hYX⟩, fun K ⟨hPK, hKX⟩ hYK ↦ ?_⟩

Premises used: _private.0.Matroid.existsMaximalSubsetProperty_of_bdd.match_1, LE.le, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ (↑n : ℕ∞)
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (image.{u_1, 0} (α := Set α) ncard {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
Y : Set α
hY' :
  ∀ ⦃j : Set α⦄,
    (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X} x) j →
      Y.ncard ≤ j.ncard → j.ncard ≤ Y.ncard
hY : P Y
hIY : I ⊆ Y
hYX : Y ⊆ X
refine : ∀ (K : Set α), (fun (K : Set α) ↦ P K ∧ K ⊆ X) K → ∀ (hYK : Y ≤ K) (hPK : P K) (hKX : K ⊆ X), K ≤ Y
⊢ ∃ (J : Set α), I ⊆ J ∧ Maximal (fun (K : Set α) ↦ P K ∧ K ⊆ X) J

Tactic:
refine ⟨Y, hIY, ⟨hY, hYX⟩, fun K ⟨hPK, hKX⟩ hYK ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ (↑n : ℕ∞)
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (image.{u_1, 0} (α := Set α) ncard {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
Y : Set α
hY' :
  ∀ ⦃j : Set α⦄,
    (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X} x) j →
      Y.ncard ≤ j.ncard → j.ncard ≤ Y.ncard
hY : P Y
hIY : I ⊆ Y
hYX : Y ⊆ X
K : Set α
h : (fun (K : Set α) ↦ P K ∧ K ⊆ X) K
hYK : Y ≤ K
hPK : P K
hKX : K ⊆ X
⊢ K.Finite

Tactic:
have hKfin : K.Finite := finite_of_encard_le_coe (hP K hPK)
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ (↑n : ℕ∞)
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (image.{u_1, 0} (α := Set α) ncard {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
Y : Set α
hY' :
  ∀ ⦃j : Set α⦄,
    (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X} x) j →
      Y.ncard ≤ j.ncard → j.ncard ≤ Y.ncard
hY : P Y
hIY : I ⊆ Y
hYX : Y ⊆ X
K : Set α
h : (fun (K : Set α) ↦ P K ∧ K ⊆ X) K
hYK : Y ≤ K
hPK : P K
hKX : K ⊆ X
hKfin : K.Finite
⊢ K ≤ Y

Tactic:
(eq_of_subset_of_ncard_le hYK ?_ hKfin).symm.subset

Premises used: Eq.subset, Set.eq_of_subset_of_ncard_le, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ (↑n : ℕ∞)
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (image.{u_1, 0} (α := Set α) ncard {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
Y : Set α
hY' :
  ∀ ⦃j : Set α⦄,
    (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X} x) j →
      Y.ncard ≤ j.ncard → j.ncard ≤ Y.ncard
hY : P Y
hIY : I ⊆ Y
hYX : Y ⊆ X
K : Set α
h : (fun (K : Set α) ↦ P K ∧ K ⊆ X) K
hYK : Y ≤ K
hPK : P K
hKX : K ⊆ X
hKfin : K.Finite
refine : K.ncard ≤ Y.ncard
⊢ K ≤ Y

Tactic:
refine (eq_of_subset_of_ncard_le hYK ?_ hKfin).symm.subset

Premises used: Eq.subset, Set.eq_of_subset_of_ncard_le, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ (↑n : ℕ∞)
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (image.{u_1, 0} (α := Set α) ncard {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
Y : Set α
hY' :
  ∀ ⦃j : Set α⦄,
    (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X} x) j →
      Y.ncard ≤ j.ncard → j.ncard ≤ Y.ncard
hY : P Y
hIY : I ⊆ Y
hYX : Y ⊆ X
K : Set α
h : (fun (K : Set α) ↦ P K ∧ K ⊆ X) K
hYK : Y ≤ K
hPK : P K
hKX : K ⊆ X
hKfin : K.Finite
⊢ K.ncard ≤ Y.ncard

Tactic:
hY' ⟨hPK, hIY.trans hYK, hKX⟩ (ncard_le_ncard hYK hKfin)

Premises used: HasSubset.Subset.trans, And.intro, Set.ncard_le_ncard
-- Module: Mathlib.Combinatorics.Matroid.IndepAxioms
Goal:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ (↑n : ℕ∞)
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (image.{u_1, 0} (α := Set α) ncard {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
Y : Set α
hY' :
  ∀ ⦃j : Set α⦄,
    (fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X} x) j →
      Y.ncard ≤ j.ncard → j.ncard ≤ Y.ncard
hY : P Y
hIY : I ⊆ Y
hYX : Y ⊆ X
K : Set α
h : (fun (K : Set α) ↦ P K ∧ K ⊆ X) K
hYK : Y ≤ K
hPK : P K
hKX : K ⊆ X
hKfin : K.Finite
⊢ K.ncard ≤ Y.ncard

Tactic:
exact hY' ⟨hPK, hIY.trans hYK, hKX⟩ (ncard_le_ncard hYK hKfin)

Premises used: HasSubset.Subset.trans, And.intro, Set.ncard_le_ncard
-- 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)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
h_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)
⊢ (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd).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)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
h_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)
obtain :
  ∀ (B : Set α)
    (hB : (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd).matroid.IsBase B),
    (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd).matroid.RankFinite
⊢ (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd).matroid.RankFinite

Tactic:
obtain ⟨B, hB⟩ := (IndepMatroid.ofBdd E Indep _ _ _ _ _).matroid.exists_isBase

Premises used: IndepMatroid.ofBdd, Matroid.exists_isBase, IndepMatroid.matroid
-- 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)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
h_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)
B : Set α
hB : (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd).matroid.IsBase B
⊢ (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd).matroid.RankFinite

Tactic:
hB.rankFinite_of_finite ?_

Premises used: Matroid.IsBase.rankFinite_of_finite
-- 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)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
h_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)
B : Set α
hB : (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd).matroid.IsBase B
refine : B.Finite
⊢ (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd).matroid.RankFinite

Tactic:
refine hB.rankFinite_of_finite ?_

Premises used: Matroid.IsBase.rankFinite_of_finite
-- 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)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
h_bdd : ∃ (n : ℕ), ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)
B : Set α
hB : (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd).matroid.IsBase B
obtain :
  ∀ (n : ℕ) (hn : ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞))
    (hB : (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground ⋯).matroid.IsBase B), B.Finite
⊢ B.Finite

Tactic:
obtain ⟨n, hn⟩ := h_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 B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
B : Set α
n : ℕ
hn : ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)
hB : (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground ⋯).matroid.IsBase B
⊢ Indep B

Tactic:
simpa using hB.indep

Premises used: Matroid.IsBase.indep
-- 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)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
B : Set α
n : ℕ
hn : ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)
hB : (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground ⋯).matroid.IsBase B
⊢ B.Finite

Tactic:
exact finite_of_encard_le_coe <| hn B (by simpa using hB.indep)

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
hcard : I.encard < B.encard
obtain : ∀ (e : α) (heB : e ∈ B) (heI : e ∉ I) (hi : Indep (insert e I)), ∃ x ∈ B \ I, Indep (insert x I)
⊢ ∃ x ∈ B \ I, Indep (insert x I)

Tactic:
obtain ⟨e, heB, heI, hi⟩ := indep_aug hI hBmax.prop hcard

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
hcard : I.encard < B.encard
e : α
heB : e ∈ B
heI : e ∉ I
hi : Indep (insert e I)
⊢ ∃ x ∈ B \ I, Indep (insert x I)

Tactic:
⟨e, ⟨heB, heI⟩, hi⟩

Premises used: And.intro, Exists.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 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
hcard : I.encard < B.encard
e : α
heB : e ∈ B
heI : e ∉ I
hi : Indep (insert e I)
⊢ ∃ x ∈ B \ I, Indep (insert x I)

Tactic:
exact ⟨e, ⟨heB, heI⟩, 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
suffices : I.encard < B.encard
⊢ ∃ x ∈ B \ I, Indep (insert x I)

Tactic:
suffices hcard : I.encard < B.encard by
        obtain ⟨e, heB, heI, hi⟩ := indep_aug hI hBmax.prop hcard
        exact ⟨e, ⟨heB, heI⟩, 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
⊢ I.encard < B.encard

Tactic:
lt_of_not_ge fun hle ↦ ?_

Premises used: lt_of_not_ge
-- 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
refine : ∀ (hle : B.encard ≤ I.encard), False
⊢ I.encard < B.encard

Tactic:
refine lt_of_not_ge fun hle ↦ ?_

Premises used: lt_of_not_ge
-- 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
obtain : ∀ (x : α) (hxnot : x ∉ I) (hxI : Indep (insert x I)), False
⊢ False

Tactic:
obtain ⟨x, hxnot, hxI⟩ := exists_insert_of_not_maximal indep_subset hI hImax

Premises used: Set.exists_insert_of_not_maximal