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
⊢ ∃ x ∈ B \ I, Indep (insert x I)
have neg : ∀ (hcon : ∀ (x : α) (_ : x ∈ B \ I), ¬Indep (insert x I)), False
Tactic: by_contra! hcon
-- 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)
⊢ False
have heBdep : ¬Indep (insert e B)
Tactic: have heBdep := hBmax.not_prop_of_ssuperset (ssubset_insert heB)
-- 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)
⊢ False
have neg : ∀ (B₀ : Set α) (hB₀B : B₀ ⊆ B) (hB₀fin : B₀.Finite) (hB₀e : ¬Indep (insert e B₀)), False
Tactic: obtain ⟨B₀, hB₀B, hB₀fin, hB₀e⟩ := htofin B e hBmax.1 heBdep
-- 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₀)
⊢ False
have hB₀ : Indep B₀
Tactic: have hB₀ := indep_subset hBmax.1 hB₀B
-- 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₀ ⊆ I, I₀.Finite ∧ ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
have hch : ∀ (b : (↑(B₀ \ I) : Type u_1)), ∃ Ib ⊆ I, Ib.Finite ∧ ¬Indep (insert (↑b : α) Ib)
Tactic: have hch : ∀ (b : ↑(B₀ \ I)), ∃ Ib, Ib ⊆ I ∧ Ib.Finite ∧ ¬Indep (insert (b : α) Ib) := by
          rintro ⟨b, hb⟩; exact htofin I b hI (hcon b ⟨hB₀B hb.1, hb.2⟩)
-- 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₀
hch : ∀ (b : (↑(B₀ \ I) : Type u_1)), ∃ Ib ⊆ I, Ib.Finite ∧ ¬Indep (insert (↑b : α) Ib)
⊢ ∃ I₀ ⊆ I, I₀.Finite ∧ ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
have choose! : ∀ (f : (b : (↑(B₀ \ I) : Type u_1)) → Set α)
  (hf : ∀ (b : (↑(B₀ \ I) : Type u_1)), f b ⊆ I ∧ (f b).Finite ∧ ¬Indep (insert (↑b : α) (f b))),
  ∃ I₀ ⊆ I, I₀.Finite ∧ ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
Tactic: choose! f hf using hch
Cleared hypotheses: hch
-- 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₀
f : (b : (↑(B₀ \ I) : Type u_1)) → Set α
hf : ∀ (b : (↑(B₀ \ I) : Type u_1)), f b ⊆ I ∧ (f b).Finite ∧ ¬Indep (insert (↑b : α) (f b))
⊢ ∃ I₀ ⊆ I, I₀.Finite ∧ ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
have this : Finite.{u_1 + 1} (↑(B₀ \ I) : Type u_1)
Tactic: have : Finite ↑(B₀ \ I) := hB₀fin.diff.to_subtype
-- 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₀
f : (b : (↑(B₀ \ I) : Type u_1)) → Set α
hf : ∀ (b : (↑(B₀ \ I) : Type u_1)), f b ⊆ I ∧ (f b).Finite ∧ ¬Indep (insert (↑b : α) (f b))
this : Finite.{u_1 + 1} (↑(B₀ \ I) : Type u_1)
⊢ ∃ I₀ ⊆ I, I₀.Finite ∧ ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
have refine : ∀ x ∈ B₀ \ (iUnion f ∪ B₀ ∩ I),
  ∀ (hi : Indep (insert x (iUnion f ∪ B₀ ∩ I))) (hxB₀ : x ∈ B₀) (hxn : x ∉ iUnion f ∪ B₀ ∩ I), False
Tactic: refine ⟨iUnion f ∪ (B₀ ∩ I),
          union_subset (iUnion_subset (fun i ↦ (hf i).1)) inter_subset_right,
          (finite_iUnion fun i ↦ (hf i).2.1).union (hB₀fin.subset inter_subset_left),
          fun x ⟨hxB₀, hxn⟩ hi ↦ ?_⟩
-- 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₀
f : (b : (↑(B₀ \ I) : Type u_1)) → Set α
hf : ∀ (b : (↑(B₀ \ I) : Type u_1)), f b ⊆ I ∧ (f b).Finite ∧ ¬Indep (insert (↑b : α) (f b))
this : Finite.{u_1 + 1} (↑(B₀ \ I) : Type u_1)
x : α
h : x ∈ B₀ \ (iUnion f ∪ B₀ ∩ I)
hi : Indep (insert x (iUnion f ∪ B₀ ∩ I))
hxB₀ : x ∈ B₀
hxn : x ∉ iUnion f ∪ B₀ ∩ I
⊢ False
have hxI : x ∉ I
Tactic: have hxI : x ∉ I := fun hxI ↦ hxn <| Or.inr ⟨hxB₀, hxI⟩
-- 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₀
f : (b : (↑(B₀ \ I) : Type u_1)) → Set α
hf : ∀ (b : (↑(B₀ \ I) : Type u_1)), f b ⊆ I ∧ (f b).Finite ∧ ¬Indep (insert (↑b : α) (f b))
this : Finite.{u_1 + 1} (↑(B₀ \ I) : Type u_1)
x : α
h : x ∈ B₀ \ (iUnion f ∪ B₀ ∩ I)
hi : Indep (insert x (iUnion f ∪ B₀ ∩ I))
hxB₀ : x ∈ B₀
hxn : x ∉ iUnion f ∪ B₀ ∩ I
hxI : x ∉ I
⊢ False
have refine : f (Subtype.mk (p := fun (x : α) ↦ x ∈ B₀ \ I) x sorry) ⊆ iUnion f ∪ B₀ ∩ I
Tactic: refine (hf ⟨x, ⟨hxB₀, hxI⟩⟩).2.2 (indep_subset hi <| insert_subset_insert ?_)
-- 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₀
f : (b : (↑(B₀ \ I) : Type u_1)) → Set α
hf : ∀ (b : (↑(B₀ \ I) : Type u_1)), f b ⊆ I ∧ (f b).Finite ∧ ¬Indep (insert (↑b : α) (f b))
this : Finite.{u_1 + 1} (↑(B₀ \ I) : Type u_1)
x : α
h : x ∈ B₀ \ (iUnion f ∪ B₀ ∩ I)
hi : Indep (insert x (iUnion f ∪ B₀ ∩ I))
hxB₀ : x ∈ B₀
hxn : x ∉ iUnion f ∪ B₀ ∩ I
hxI : x ∉ I
⊢ f (Subtype.mk (p := fun (x : α) ↦ x ∈ B₀ \ I) x ⋯) ⊆ iUnion f ∪ B₀ ∩ I
have h : f (Subtype.mk (p := fun (x : α) ↦ x ∈ B₀ \ I) x sorry) ⊆ iUnion f
Tactic: apply subset_union_of_subset_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₀
⊢ False
have hexI₀ : ∃ I₀ ⊆ I, I₀.Finite ∧ ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
Tactic: have hexI₀ : ∃ I₀, I₀ ⊆ I ∧ I₀.Finite ∧ ∀ x, x ∈ B₀ \ I₀ → ¬Indep (insert x I₀) := by
        have hch : ∀ (b : ↑(B₀ \ I)), ∃ Ib, Ib ⊆ I ∧ Ib.Finite ∧ ¬Indep (insert (b : α) Ib) := by
          rintro ⟨b, hb⟩; exact htofin I b hI (hcon b ⟨hB₀B hb.1, hb.2⟩)
        choose! f hf using hch
        have : Finite ↑(B₀ \ I) := hB₀fin.diff.to_subtype
        refine ⟨iUnion f ∪ (B₀ ∩ I),
          union_subset (iUnion_subset (fun i ↦ (hf i).1)) inter_subset_right,
          (finite_iUnion fun i ↦ (hf i).2.1).union (hB₀fin.subset inter_subset_left),
          fun x ⟨hxB₀, hxn⟩ hi ↦ ?_⟩
        have hxI : x ∉ I := fun hxI ↦ hxn <| Or.inr ⟨hxB₀, hxI⟩
        refine (hf ⟨x, ⟨hxB₀, hxI⟩⟩).2.2 (indep_subset hi <| insert_subset_insert ?_)
        apply subset_union_of_subset_left
        apply subset_iUnion
-- 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₀
hexI₀ : ∃ I₀ ⊆ I, I₀.Finite ∧ ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
⊢ False
have neg : ∀ (I₀ : Set α) (hI₀I : I₀ ⊆ I) (hI₀fin : I₀.Finite) (hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)), False
Tactic: obtain ⟨I₀, hI₀I, hI₀fin, hI₀⟩ := hexI₀
Cleared hypotheses: hexI₀
-- 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₀)
⊢ False
have hE₀fin : E₀.Finite
Tactic: have hE₀fin : E₀.Finite := (hI₀fin.union hB₀fin).insert e
-- 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
⊢ False
have neg : ∀ (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₀), False
Tactic: obtain ⟨J, ⟨hB₀J, hJ, hJss⟩, hJmax⟩ := Finite.exists_maximalFor (f := id)
        (s := {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀})
        (hE₀fin.finite_subsets.subset (by simp))
        ⟨B₀, Subset.rfl, hB₀, subset_union_right.trans (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₀
⊢ False
have heI₀ : e ∉ I₀
Tactic: have heI₀ : e ∉ I₀ := notMem_subset hI₀I heI
-- 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₀
⊢ False
have heI₀i : Indep (insert e I₀)
Tactic: have heI₀i : Indep (insert e I₀) := indep_subset hins (insert_subset_insert hI₀I)
-- 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₀)
⊢ False
have heJ : e ∉ J
Tactic: have heJ : e ∉ J := fun heJ ↦ hB₀e (indep_subset hJ <| insert_subset heJ hB₀J)
-- 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
⊢ False
have hJfin : J.Finite
Tactic: have hJfin := hE₀fin.subset hJss