Theorem: Matroid.modular_finite_intersection (Matroid/Old/ModularCut.lean)

State before:
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
⊢ ⋂₀ X ∈ C
Tactic:
obtain (⟨x, rfl⟩ | X_nt) := X_none.exists_eq_singleton_or_nontrivial
State after:
case inl.intro
α : Type u_1
α✝ : Type u_2
C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
x : Set α✝
X_fin : {x}.Finite
X_sub : {x} ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : {x}.Nonempty
⊢ ⋂₀ {x} ∈ C

case inr
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
⊢ ⋂₀ X ∈ C

State before:
case inr
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
⊢ ⋂₀ X ∈ C
Tactic:
obtain ⟨x, y, xy_ne, xy_sub⟩ := nontrivial_iff_pair_subset.1 X_nt
State after:
case inr.intro.intro.intro
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
x y : Set α✝
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
⊢ ⋂₀ X ∈ C

State before:
case inr.intro.intro.intro
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
x y : Set α✝
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
⊢ ⋂₀ X ∈ C
Tactic:
have x_eq_insert : X = insert x (X \ {x})
State after:
case x_eq_insert
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
x y : Set α✝
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
⊢ X = insert x (X \ {x})

case inr.intro.intro.intro
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
x y : Set α✝
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
⊢ ⋂₀ X ∈ C

State before:
case inr.intro.intro.intro
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
x y : Set α✝
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
⊢ ⋂₀ X ∈ C
Tactic:
rw [x_eq_insert, sInter_insert]
State after:
case inr.intro.intro.intro
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
x y : Set α✝
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
⊢ x ∩ ⋂₀ (X \ {x}) ∈ C

State before:
case inr.intro.intro.intro
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
x y : Set α✝
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
⊢ x ∩ ⋂₀ (X \ {x}) ∈ C
Tactic:
obtain ⟨B, B_mod⟩ := X_mod
State after:
case inr.intro.intro.intro.intro
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_none : X.Nonempty
X_nt : X.Nontrivial
x y : Set α✝
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : ?m.1084 C_mod X_fin X_sub
B_mod : sorryAx Prop true
⊢ x ∩ ⋂₀ (X \ {x}) ∈ C

State before:
case inl.intro
α : Type u_1
α✝ : Type u_2
C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
x : Set α✝
X_fin : {x}.Finite
X_sub : {x} ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : {x}.Nonempty
⊢ ⋂₀ {x} ∈ C
Tactic:
rwa [sInter_singleton, ← singleton_subset_iff]
State after:
no goals

State before:
case x_eq_insert
α : Type u_1
α✝ : Type u_2
X C : Set (Set α✝)
M : Matroid α
C_mod : sorryAx (Sort u_3) true
X_fin : X.Finite
X_sub : X ⊆ C
X_mod : ∃ B, sorryAx Prop true
X_none : X.Nonempty
X_nt : X.Nontrivial
x y : Set α✝
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
⊢ X = insert x (X \ {x})
Tactic:
simp [pair_subset_iff.1 xy_sub]
State after:
no goals