awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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
⊢ (insert e I₀).ncard ≤ J.ncard
have refine : ∀ (hlt : J.ncard < (insert e I₀).ncard), False
Tactic: refine not_lt.1 fun hlt ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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
hlt : J.ncard < (insert e I₀).ncard
⊢ False
have obtain : ∀ (f : α) (hfI : f ∈ insert e I₀) (hfJ : f ∉ J) (hfi : Indep (insert f J)), False
Tactic: obtain ⟨f, hfI, hfJ, hfi⟩ := indep_aug hJ hJfin heI₀i (hI₀fin.insert e) hlt
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
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
hlt : J.ncard < (insert e I₀).ncard
f : α
hfI : f ∈ insert e I₀
hfJ : f ∉ J
hfi : Indep (insert f J)
⊢ False
have hfE₀ : f ∈ E₀
Tactic: have hfE₀ : f ∈ E₀ := mem_of_mem_of_subset hfI (insert_subset_insert subset_union_left)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
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
⊢ False
have hcard : (insert e I₀).ncard ≤ J.ncard
Tactic: have hcard : (insert e I₀).ncard ≤ J.ncard := by
        refine not_lt.1 fun hlt ↦ ?_
        obtain ⟨f, hfI, hfJ, hfi⟩ := indep_aug hJ hJfin heI₀i (hI₀fin.insert e) hlt
        have hfE₀ : f ∈ E₀ := mem_of_mem_of_subset hfI (insert_subset_insert subset_union_left)
        exact hfJ <| insert_eq_self.1 <| le_imp_eq_iff_le_imp_ge'.2 (hJmax
          ⟨hB₀J.trans <| subset_insert _ _, hfi, insert_subset hfE₀ hJss⟩) (subset_insert _ _)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
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 : (insert e I₀).ncard ≤ J.ncard
⊢ False
have hcard₁ : I₀.ncard < J.ncard
Tactic: rw [ncard_insert_of_notMem heI₀ hI₀fin, ← Nat.lt_iff_add_one_le] at hcard
Cleared hypotheses: hcard
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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
⊢ False
have neg : ∀ (f : α) (hfJ : f ∈ J) (hfI₀ : f ∉ I₀) (hfi : Indep (insert f I₀)), False
Tactic: obtain ⟨f, hfJ, hfI₀, hfi⟩ := indep_aug (indep_subset hI hI₀I) hI₀fin hJ hJfin hcard
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
P : Set α → Prop
hP : ∃ (n : ℕ), ∀ (Y : Set α), P Y → Y.encard ≤ (↑n : ℕ∞)
X : Set α
⊢ ExistsMaximalSubsetProperty P X
have obtain : ∀ (n : ℕ) (hP : ∀ (Y : Set α), P Y → Y.encard ≤ (↑n : ℕ∞)), ExistsMaximalSubsetProperty P X
Tactic: obtain ⟨n, hP⟩ := hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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
have rw : ∃ (x : ℕ), ∀ y ∈ image.{u_1, 0} (α := Set α) ncard {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, y ≤ x
Tactic: rw [finite_iff_bddAbove, bddAbove_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
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
⊢ ∃ (x : ℕ), ∀ y ∈ image.{u_1, 0} (α := Set α) ncard {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, y ≤ x
have hP₁ : ∀ (Y : Set α), P Y → ∃ (n₀ : ℕ), Y.encard = (↑n₀ : ℕ∞) ∧ n₀ ≤ n
Tactic: simp_rw [ENat.le_coe_iff] at hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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
⊢ ∃ (x : ℕ), ∀ y ∈ image.{u_1, 0} (α := Set α) ncard {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, y ≤ x
have h : ∀ y ∈ image.{u_1, 0} (α := Set α) ncard {Y : Set α | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, y ≤ n
Tactic: use n
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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
⊢ Y.ncard ≤ n
have h : ∀ (n₀ : ℕ) (heq : Y.encard = (↑n₀ : ℕ∞)) (hle : n₀ ≤ n), Y.ncard ≤ n
Tactic: obtain ⟨n₀, heq, hle⟩ := hP Y hY
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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
⊢ Y.ncard ≤ n
have h : Y.encard.toNat ≤ n
Tactic: rwa [ncard_def, heq, ENat.toNat_coe]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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
⊢ Y.ncard ≤ n
have h₁ : ENat.toNat (↑n₀ : ℕ∞) ≤ n
Tactic: rwa [ncard_def, heq, ENat.toNat_coe]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
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
⊢ ∃ (J : Set α), I ⊆ J ∧ Maximal (fun (K : Set α) ↦ P K ∧ K ⊆ X) J
have hfin : (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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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
⊢ ∃ (J : Set α), I ⊆ J ∧ Maximal (fun (K : Set α) ↦ P K ∧ K ⊆ X) J
have 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
Tactic: obtain ⟨Y, ⟨hY, hIY, hYX⟩, hY'⟩ :=
    Finite.exists_maximalFor' ncard _ hfin ⟨I, hI, rfl.subset, hIX⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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
have refine : ∀ (K : Set α), (fun (K : Set α) ↦ P K ∧ K ⊆ X) K → ∀ (hYK : Y ≤ K) (hPK : P K) (hKX : K ⊆ X), K ≤ Y
Tactic: refine ⟨Y, hIY, ⟨hY, hYX⟩, fun K ⟨hPK, hKX⟩ hYK ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
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 ≤ Y
have hKfin : K.Finite
Tactic: have hKfin : K.Finite := finite_of_encard_le_coe (hP K hPK)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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
have refine : K.ncard ≤ Y.ncard
Tactic: refine (eq_of_subset_of_ncard_le hYK ?_ hKfin).symm.subset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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).matroid.RankFinite
have 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
Tactic: obtain ⟨B, hB⟩ := (IndepMatroid.ofBdd E Indep _ _ _ _ _).matroid.exists_isBase
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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
have refine : B.Finite
Tactic: refine hB.rankFinite_of_finite ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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
⊢ B.Finite
have obtain : ∀ (n : ℕ) (hn : ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞))
  (hB : (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground sorry).matroid.IsBase B), B.Finite
Tactic: obtain ⟨n, hn⟩ := h_bdd
Cleared hypotheses: h_bdd, hB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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
⊢ ∃ x ∈ B \ I, Indep (insert x I)
have obtain : ∀ (e : α) (heB : e ∈ B) (heI : e ∉ I) (hi : Indep (insert e I)), ∃ x ∈ B \ I, Indep (insert x I)
Tactic: obtain ⟨e, heB, heI, hi⟩ := indep_aug hI hBmax.prop hcard
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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
⊢ ∃ x ∈ B \ I, Indep (insert x I)
have suffices : I.encard < B.encard
Tactic: suffices hcard : I.encard < B.encard by
        obtain ⟨e, heB, heI, hi⟩ := indep_aug hI hBmax.prop hcard
        exact ⟨e, ⟨heB, heI⟩, hi⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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
have refine : ∀ (hle : B.encard ≤ I.encard), False
Tactic: refine lt_of_not_ge fun hle ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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
⊢ False
have obtain : ∀ (x : α) (hxnot : x ∉ I) (hxI : Indep (insert x I)), False
Tactic: obtain ⟨x, hxnot, hxI⟩ := exists_insert_of_not_maximal indep_subset hI hImax
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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
have rwa : I.encard ≠ ⊤
Tactic: rwa [encard_insert_of_notMem hxnot, ← not_le, ENat.add_one_le_iff, not_lt]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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)
⊢ I.encard ≠ ⊤
have rw : I.Finite
Tactic: rw [encard_ne_top_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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)
⊢ I.Finite
have obtain : ∀ (n : ℕ) (hn : ∀ (I : Set α), Indep I → I.encard ≤ (↑n : ℕ∞)), I.Finite
Tactic: obtain ⟨n, hn⟩ := indep_bdd
Cleared hypotheses: indep_bdd
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
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)
⊢ False
have hlt : 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)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
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
⊢ False
have obtain : ∀ (y : α) (hyB : y ∉ B) (hi : Indep (insert y B)), False
Tactic: obtain ⟨y, -, hyB, hi⟩ := indep_aug hBmax.prop hxI hlt