awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
M : IndepMatroid α
⊢ ∀ ⦃I : Set α⦄, M.Indep I ↔ ∃ (B : Set α), Maximal M.Indep B ∧ I ⊆ B
have refine : ∀ (I : Set α) (h : M.Indep I), ∃ (B : Set α), Maximal M.Indep B ∧ I ⊆ B
Tactic: refine fun I ↦ ⟨fun h ↦ ?_, fun ⟨B, ⟨h, _⟩, hIB'⟩ ↦ M.indep_subset h hIB'⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
M : IndepMatroid α
I : Set α
h : M.Indep I
⊢ ∃ (B : Set α), Maximal M.Indep B ∧ I ⊆ B
have obtain : ∀ (J : Set α) (hIJ : I ⊆ J) (hmax : Maximal (fun (K : Set α) ↦ M.Indep K ∧ K ⊆ M.E) J),
  ∃ (B : Set α), Maximal M.Indep B ∧ I ⊆ B
Tactic: obtain ⟨J, hIJ, hmax⟩ := M.indep_maximal M.E rfl.subset I h (M.subset_ground I h)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
Goal:
α : Type u_1
M : IndepMatroid α
I : Set α
h : M.Indep I
J : Set α
hIJ : I ⊆ J
hmax : Maximal (fun (K : Set α) ↦ M.Indep K ∧ K ⊆ M.E) J
⊢ ∃ (B : Set α), Maximal M.Indep B ∧ I ⊆ B
have hmax₁ : Maximal M.Indep J ∧ J ⊆ M.E
Tactic: rw [maximal_and_iff_right_of_imp M.subset_ground] at hmax
Cleared hypotheses: hmax
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
M : IndepMatroid α
⊢ ∃ (B : Set α), Maximal M.Indep B
have obtain : ∀ (B : Set α) (hB : Maximal (fun (K : Set α) ↦ M.Indep K ∧ K ⊆ M.E) B), ∃ (B : Set α), Maximal M.Indep B
Tactic: obtain ⟨B, -, hB⟩ := M.indep_maximal M.E rfl.subset ∅ M.indep_empty <| empty_subset _
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
Goal:
α : Type u_1
M : IndepMatroid α
B : Set α
hB : Maximal (fun (K : Set α) ↦ M.Indep K ∧ K ⊆ M.E) B
⊢ ∃ (B : Set α), Maximal M.Indep B
have hB₁ : Maximal M.Indep B ∧ B ⊆ M.E
Tactic: rw [maximal_and_iff_right_of_imp M.subset_ground] at hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
⊢ ∃ b ∈ B' \ B, Maximal M.Indep (insert b (B \ {e}))
have hnotmax : ¬Maximal M.Indep (B \ {e})
Tactic: have hnotmax : ¬ Maximal M.Indep (B \ {e}) :=
      fun h ↦ h.not_prop_of_ssuperset (diff_singleton_ssubset.2 he.1) hB.prop
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
⊢ ∃ b ∈ B' \ B, Maximal M.Indep (insert b (B \ {e}))
have obtain : ∀ (f : α) (hf : f ∈ B' \ (B \ {e})) (hfB : M.Indep (insert f (B \ {e}))),
  ∃ b ∈ B' \ B, Maximal M.Indep (insert b (B \ {e}))
Tactic: obtain ⟨f, hf, hfB⟩ := M.indep_aug (M.indep_subset hB.prop diff_subset) hnotmax hB'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hf : f ∈ B' \ (B \ {e})
hfB : M.Indep (insert f (B \ {e}))
⊢ ∃ b ∈ B' \ B, Maximal M.Indep (insert b (B \ {e}))
have hf₁ : f ∈ B' \ B
Tactic: replace hf := show f ∈ B' \ B by simpa [show f ≠ e by rintro rfl; exact he.2 hf.1] using hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
⊢ ∃ b ∈ B' \ B, Maximal M.Indep (insert b (B \ {e}))
have refine : ∀ (hnot : ¬Maximal M.Indep (insert f (B \ {e}))), False
Tactic: refine ⟨f, hf, by_contra fun hnot ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
hnot : ¬Maximal M.Indep (insert f (B \ {e}))
⊢ False
have obtain : ∀ (x : α) (hxB : x ∈ B \ insert f (B \ {e})) (hind : M.Indep (insert x (insert f (B \ {e})))), False
Tactic: obtain ⟨x, hxB, hind⟩ := M.indep_aug hfB hnot hB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
hnot : ¬Maximal M.Indep (insert f (B \ {e}))
x : α
hxB : x ∈ B \ insert f (B \ {e})
hind : M.Indep (insert x (insert f (B \ {e})))
⊢ False
have he₁ : x ∈ B \ B'
Tactic: obtain ⟨-, rfl⟩ : _ ∧ x = e := by simpa [hxB.1] using hxB
Cleared hypotheses: e, he, hnotmax, hfB, hnot, hxB, hind
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
hnot : ¬Maximal M.Indep (insert f (B \ {e}))
x : α
hxB : x ∈ B \ insert f (B \ {e})
hind : M.Indep (insert x (insert f (B \ {e})))
he₁ : x ∈ B \ B'
⊢ False
have hnotmax₁ : ¬Maximal M.Indep (B \ {x})
Tactic: obtain ⟨-, rfl⟩ : _ ∧ x = e := by simpa [hxB.1] using hxB
Cleared hypotheses: e, he, hnotmax, hfB, hnot, hxB, hind
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
hnot : ¬Maximal M.Indep (insert f (B \ {e}))
x : α
hxB : x ∈ B \ insert f (B \ {e})
hind : M.Indep (insert x (insert f (B \ {e})))
he₁ : x ∈ B \ B'
hnotmax₁ : ¬Maximal M.Indep (B \ {x})
⊢ False
have hfB₁ : M.Indep (insert f (B \ {x}))
Tactic: obtain ⟨-, rfl⟩ : _ ∧ x = e := by simpa [hxB.1] using hxB
Cleared hypotheses: e, he, hnotmax, hfB, hnot, hxB, hind
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
hnot : ¬Maximal M.Indep (insert f (B \ {e}))
x : α
hxB : x ∈ B \ insert f (B \ {e})
hind : M.Indep (insert x (insert f (B \ {e})))
he₁ : x ∈ B \ B'
hnotmax₁ : ¬Maximal M.Indep (B \ {x})
hfB₁ : M.Indep (insert f (B \ {x}))
⊢ False
have hnot₁ : ¬Maximal M.Indep (insert f (B \ {x}))
Tactic: obtain ⟨-, rfl⟩ : _ ∧ x = e := by simpa [hxB.1] using hxB
Cleared hypotheses: e, he, hnotmax, hfB, hnot, hxB, hind
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
hnot : ¬Maximal M.Indep (insert f (B \ {e}))
x : α
hxB : x ∈ B \ insert f (B \ {e})
hind : M.Indep (insert x (insert f (B \ {e})))
he₁ : x ∈ B \ B'
hnotmax₁ : ¬Maximal M.Indep (B \ {x})
hfB₁ : M.Indep (insert f (B \ {x}))
hnot₁ : ¬Maximal M.Indep (insert f (B \ {x}))
⊢ False
have hxB₁ : x ∈ B \ insert f (B \ {x})
Tactic: obtain ⟨-, rfl⟩ : _ ∧ x = e := by simpa [hxB.1] using hxB
Cleared hypotheses: e, he, hnotmax, hfB, hnot, hxB, hind
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (hypothesis)
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
hnot : ¬Maximal M.Indep (insert f (B \ {e}))
x : α
hxB : x ∈ B \ insert f (B \ {e})
hind : M.Indep (insert x (insert f (B \ {e})))
he₁ : x ∈ B \ B'
hnotmax₁ : ¬Maximal M.Indep (B \ {x})
hfB₁ : M.Indep (insert f (B \ {x}))
hnot₁ : ¬Maximal M.Indep (insert f (B \ {x}))
hxB₁ : x ∈ B \ insert f (B \ {x})
⊢ False
have hind₁ : M.Indep (insert x (insert f (B \ {x})))
Tactic: obtain ⟨-, rfl⟩ : _ ∧ x = e := by simpa [hxB.1] using hxB
Cleared hypotheses: e, he, hnotmax, hfB, hnot, hxB, hind
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
f : α
hf : f ∈ B' \ B
x : α
he : x ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {x})
hfB : M.Indep (insert f (B \ {x}))
hnot : ¬Maximal M.Indep (insert f (B \ {x}))
hxB : x ∈ B \ insert f (B \ {x})
hind : M.Indep (insert x (insert f (B \ {x})))
⊢ False
have refine : B ⊂ insert x (insert f (B \ {x}))
Tactic: refine hB.not_prop_of_ssuperset ?_ hind
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.IndepAxioms (goal)
Goal:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
f : α
hf : f ∈ B' \ B
x : α
he : x ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {x})
hfB : M.Indep (insert f (B \ {x}))
hnot : ¬Maximal M.Indep (insert f (B \ {x}))
hxB : x ∈ B \ insert f (B \ {x})
hind : M.Indep (insert x (insert f (B \ {x})))
⊢ B ⊂ insert x (insert f (B \ {x}))
have rw : B ⊂ insert f B
Tactic: rw [insert_comm, insert_diff_singleton, insert_eq_of_mem he.1]
-- 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)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty Indep X
have refine : ∀ X ⊆ E,
  ∀ (I : Set α) (hI : Indep I) (hIX : I ⊆ X),
    ∀ c ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X},
      IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c →
        c.Nonempty →
          ∃ (ub : Set α), Membership.mem (γ := Set (Set α)) {Y : Set α | Indep Y ∧ Y ⊆ X} ub ∧ ∀ s ∈ c, s ⊆ ub
Tactic: refine fun X _ I hI hIX ↦ zorn_subset_nonempty {Y | Indep Y ∧ Y ⊆ X} ?_ I ⟨hI, hIX⟩
-- 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)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
⊢ ∀ c ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X},
    IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c →
      c.Nonempty → ∃ (ub : Set α), Membership.mem (γ := Set (Set α)) {Y : Set α | Indep Y ∧ Y ⊆ X} ub ∧ ∀ s ∈ c, s ⊆ ub
have refine : ∀ (Is : Set (Set α)) (hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}) (hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is),
  Is.Nonempty → Indep (⋃₀ Is)
Tactic: refine fun Is hIs hchain _ ↦
      ⟨⋃₀ Is, ⟨?_, sUnion_subset fun Y hY ↦ (hIs hY).2⟩, fun _ ↦ subset_sUnion_of_mem⟩
-- 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)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
⊢ Indep (⋃₀ Is)
have refine : ∀ (J : Set α) (hJ : J ⊆ ⋃₀ Is) (hJfin : J.Finite), Indep J
Tactic: refine indep_compact _ fun J hJ hJfin ↦ ?_
-- 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)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
⊢ Indep J
have have : ∀ (hchoose : ∀ e ∈ J, ∃ I ∈ Is, e ∈ I), Indep J
Tactic: have hchoose : ∀ e, e ∈ J → ∃ I, I ∈ Is ∧ (e : α) ∈ I := fun _ he ↦ mem_sUnion.1 <| hJ he
-- 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)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
hchoose : ∀ e ∈ J, ∃ I ∈ Is, e ∈ I
⊢ Indep J
have choose! : ∀ (f : (e : α) → Set α) (hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e), Indep J
Tactic: choose! f hf using hchoose
Cleared hypotheses: hchoose
-- 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 B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : (e : α) → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
⊢ Indep J
have hne : J.Nonempty
Tactic: refine J.eq_empty_or_nonempty.elim (fun hJ ↦ hJ ▸ indep_empty) (fun hne ↦ ?_)
-- 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)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : (e : α) → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
⊢ Indep J
have obtain : ∀ (x : α) (hxJ : x ∈ J) (hxmax : ∀ ⦃j : α⦄, (fun (x : α) ↦ x ∈ J) j → f x ≤ f j → f j ≤ f x), Indep J
Tactic: obtain ⟨x, hxJ, hxmax⟩ := Finite.exists_maximalFor f _ hJfin hne
-- 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)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : (e : α) → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun (x : α) ↦ x ∈ J) j → f x ≤ f j → f j ≤ f x
⊢ Indep J
have refine : ∀ (y : α) (hyJ : y ∈ J), y ∈ f x
Tactic: refine indep_subset (hIs (hf x hxJ).1).1 fun y hyJ ↦ ?_
-- 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)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : (e : α) → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun (x : α) ↦ x ∈ J) j → f x ≤ f j → f j ≤ f x
y : α
hyJ : y ∈ J
⊢ y ∈ f x
have inl : ∀ (hle : f x ⊆ f y), y ∈ f x
Tactic: obtain (hle | hle) := hchain.total (hf _ hxJ).1 (hf _ hyJ).1
-- 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)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
h : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y : Set α | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) Is
h_1 : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : (e : α) → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun (x : α) ↦ x ∈ J) j → f x ≤ f j → f j ≤ f x
y : α
hyJ : y ∈ J
inl : ∀ (hle : f x ⊆ f y), y ∈ f x
⊢ y ∈ f x
have inr : ∀ (hle : f y ⊆ f x), y ∈ f x
Tactic: obtain (hle | hle) := hchain.total (hf _ hxJ).1 (hf _ hyJ).1
-- 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
⊢ ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
have by_contra! : ∀ (I : Set α) (e : α) (hIe : ¬Indep (insert e I))
  (h : ∀ (I₀ : Set α) (_ : I₀ ⊆ I) (_ : I₀.Finite), Indep (insert e I₀)), False
Tactic: by_contra! ⟨I, e, -, hIe, h⟩
-- 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
I : Set α
e : α
hIe : ¬Indep (insert e I)
h : ∀ (I₀ : Set α) (_ : I₀ ⊆ I) (_ : I₀.Finite), Indep (insert e I₀)
⊢ False
have refine : ∀ (J : Set α) (hJss : J ⊆ insert e I) (hJfin : J.Finite), Indep J
Tactic: refine hIe <| indep_compact _ fun J hJss hJfin ↦ ?_
-- 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
I : Set α
e : α
hIe : ¬Indep (insert e I)
h : ∀ (I₀ : Set α) (_ : I₀ ⊆ I) (_ : I₀.Finite), Indep (insert e I₀)
J : Set α
hJss : J ⊆ insert e I
hJfin : J.Finite
⊢ J \ {e} ⊆ I
have rwa : J ⊆ {e} ∪ I
Tactic: rwa [diff_subset_iff]
-- 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
⊢ ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
have htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
Tactic: have htofin : ∀ I e, Indep I → ¬ Indep (insert e I) →
        ∃ I₀, I₀ ⊆ I ∧ I₀.Finite ∧ ¬ Indep (insert e I₀) := by
        by_contra! ⟨I, e, -, hIe, h⟩
        refine hIe <| indep_compact _ fun J hJss hJfin ↦ ?_
        exact indep_subset (h (J \ {e}) (by rwa [diff_subset_iff]) hJfin.diff) (by simp)
-- 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
⊢ ∃ x ∈ B \ I, Indep (insert x I)
have obtain : ∀ (e : α) (heI : e ∉ I) (hins : Indep (insert e I)), ∃ x ∈ B \ I, Indep (insert x I)
Tactic: obtain ⟨e, heI, hins⟩ := 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 → 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)
⊢ ∃ x ∈ B \ I, Indep (insert x I)
have pos : ∀ (heB : e ∈ B), ∃ x ∈ B \ I, Indep (insert x I)
Tactic: by_cases heB : e ∈ B
-- 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)
pos : ∀ (heB : e ∈ B), ∃ x ∈ B \ I, Indep (insert x I)
⊢ ∃ x ∈ B \ I, Indep (insert x I)
have neg : ∀ (heB : e ∉ B), ∃ x ∈ B \ I, Indep (insert x I)
Tactic: by_cases heB : e ∈ B