Theorem: Matroid.basis_of_maximal_extension (Matroid/Constructions/RankAxioms.lean)

State before:
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
h : J ∈ maximals (fun x x_1 => x ⊆ x_1) {I' | M.Indep I' ∧ I ⊆ I' ∧ I' ⊆ X}
⊢ M.Basis J X
Tactic:
unfold Basis
State after:
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
h : J ∈ maximals (fun x x_1 => x ⊆ x_1) {I' | M.Indep I' ∧ I ⊆ I' ∧ I' ⊆ X}
⊢ J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.Indep A ∧ A ⊆ X} ∧ X ⊆ M.E

State before:
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
h : J ∈ maximals (fun x x_1 => x ⊆ x_1) {I' | M.Indep I' ∧ I ⊆ I' ∧ I' ⊆ X}
⊢ J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.Indep A ∧ A ⊆ X} ∧ X ⊆ M.E
Tactic:
unfold maximals at h ⊢
State after:
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
h :
  J ∈
    {a |
      a ∈ {I' | M.Indep I' ∧ I ⊆ I' ∧ I' ⊆ X} ∧
        ∀ ⦃b : Set α⦄,
          b ∈ {I' | M.Indep I' ∧ I ⊆ I' ∧ I' ⊆ X} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
⊢ J ∈
      {a |
        a ∈ {A | M.Indep A ∧ A ⊆ X} ∧
          ∀ ⦃b : Set α⦄, b ∈ {A | M.Indep A ∧ A ⊆ X} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a} ∧
    X ⊆ M.E

State before:
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
h :
  J ∈
    {a |
      a ∈ {I' | M.Indep I' ∧ I ⊆ I' ∧ I' ⊆ X} ∧
        ∀ ⦃b : Set α⦄,
          b ∈ {I' | M.Indep I' ∧ I ⊆ I' ∧ I' ⊆ X} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
⊢ J ∈
      {a |
        a ∈ {A | M.Indep A ∧ A ⊆ X} ∧
          ∀ ⦃b : Set α⦄, b ∈ {A | M.Indep A ∧ A ⊆ X} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a} ∧
    X ⊆ M.E
Tactic:
simp only [Set.mem_setOf_eq, and_imp] at h ⊢
State after:
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
h : (M.Indep J ∧ I ⊆ J ∧ J ⊆ X) ∧ ∀ ⦃b : Set α⦄, M.Indep b → I ⊆ b → b ⊆ X → J ⊆ b → b ⊆ J
⊢ ((M.Indep J ∧ J ⊆ X) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ X → J ⊆ b → b ⊆ J) ∧ X ⊆ M.E

State before:
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
h : (M.Indep J ∧ I ⊆ J ∧ J ⊆ X) ∧ ∀ ⦃b : Set α⦄, M.Indep b → I ⊆ b → b ⊆ X → J ⊆ b → b ⊆ J
⊢ ((M.Indep J ∧ J ⊆ X) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ X → J ⊆ b → b ⊆ J) ∧ X ⊆ M.E
Tactic:
obtain ⟨⟨hJ_indep, hIJ, hJX⟩, hJ_max⟩ := h
State after:
case intro.intro.intro
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → I ⊆ b → b ⊆ X → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
⊢ ((M.Indep J ∧ J ⊆ X) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ X → J ⊆ b → b ⊆ J) ∧ X ⊆ M.E

State before:
case intro.intro.intro
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → I ⊆ b → b ⊆ X → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
⊢ ((M.Indep J ∧ J ⊆ X) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ X → J ⊆ b → b ⊆ J) ∧ X ⊆ M.E
Tactic:
refine ⟨⟨⟨hJ_indep, hJX⟩, ?_⟩, hX⟩
State after:
case intro.intro.intro
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → I ⊆ b → b ⊆ X → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
⊢ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ X → J ⊆ b → b ⊆ J

State before:
case intro.intro.intro
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → I ⊆ b → b ⊆ X → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
⊢ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ X → J ⊆ b → b ⊆ J
Tactic:
intro J' hJ'_indep hJ'X hJJ'
State after:
case intro.intro.intro
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → I ⊆ b → b ⊆ X → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
J' : Set α
hJ'_indep : M.Indep J'
hJ'X : J' ⊆ X
hJJ' : J ⊆ J'
⊢ J' ⊆ J

State before:
case intro.intro.intro
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → I ⊆ b → b ⊆ X → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
J' : Set α
hJ'_indep : M.Indep J'
hJ'X : J' ⊆ X
hJJ' : J ⊆ J'
⊢ J' ⊆ J
Tactic:
exact hJ_max hJ'_indep (hIJ.trans hJJ') hJ'X hJJ'
State after:
no goals