Theorem: cl_iInter_eq_iInter_cl (Matroid/scratch.lean)

State before:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
⊢ M.cl (⋂ i, Xs i) = {k}
Tactic:
set r : ι → ι → Prop := WellOrderingRel
State after:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r : ι → ι → Prop := WellOrderingRel
⊢ M.cl (⋂ i, Xs i) = {k}

State before:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r : ι → ι → Prop := WellOrderingRel
⊢ M.cl (⋂ i, Xs i) = {k}
Tactic:
set P : Set ι → Prop := fun I ↦ M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
State after:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
⊢ M.cl (⋂ i, Xs i) = {k}

State before:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
⊢ M.cl (⋂ i, Xs i) = {k}
Tactic:
suffices hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r),
    P (range (fun p : Iio o ↦ Ordinal.enum r p.1 (lt_of_lt_of_le p.2 ho))) by
  convert hwin (Ordinal.type r) rfl.le
State after:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
⊢ ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)

State before:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
⊢ ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
Tactic:
set r : ι → ι → Prop := WellOrderingRel
State after:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r✝ : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
r : ι → ι → Prop := WellOrderingRel
⊢ ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r✝), P (range fun p => Ordinal.enum r✝ ↑p ⋯)

State before:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r✝ : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
r : ι → ι → Prop := WellOrderingRel
⊢ ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r✝), P (range fun p => Ordinal.enum r✝ ↑p ⋯)
Tactic:
suffices : ∀ (o : Ordinal.{u}) (ho : o < Ordinal.type r),
  M.cl (⋂ (o' : Ordinal.{u}) (ho' : o' < o), Xs (Ordinal.enum r o' (ho'.trans ho))) = {k}
State after:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r✝ : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
r : ι → ι → Prop := WellOrderingRel
this : ∀ (o : Ordinal.{u}) (ho : o < Ordinal.type r), M.cl (⋂ o', ⋂ (ho' : o' < o), Xs (Ordinal.enum r o' ⋯)) = {k}
⊢ ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r✝), P (range fun p => Ordinal.enum r✝ ↑p ⋯)

case this
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r✝ : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
r : ι → ι → Prop := WellOrderingRel
⊢ ∀ (o : Ordinal.{u}) (ho : o < Ordinal.type r), M.cl (⋂ o', ⋂ (ho' : o' < o), Xs (Ordinal.enum r o' ⋯)) = {k}

State before:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r✝ : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
r : ι → ι → Prop := WellOrderingRel
this : ∀ (o : Ordinal.{u}) (ho : o < Ordinal.type r), M.cl (⋂ o', ⋂ (ho' : o' < o), Xs (Ordinal.enum r o' ⋯)) = {k}
⊢ ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r✝), P (range fun p => Ordinal.enum r✝ ↑p ⋯)

case this
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r✝ : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
r : ι → ι → Prop := WellOrderingRel
⊢ ∀ (o : Ordinal.{u}) (ho : o < Ordinal.type r), M.cl (⋂ o', ⋂ (ho' : o' < o), Xs (Ordinal.enum r o' ⋯)) = {k}
Tactic:
sorry
State after:
case this
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r✝ : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
r : ι → ι → Prop := WellOrderingRel
⊢ ∀ (o : Ordinal.{u}) (ho : o < Ordinal.type r), M.cl (⋂ o', ⋂ (ho' : o' < o), Xs (Ordinal.enum r o' ⋯)) = {k}

State before:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ M.cl (⋂ i, Xs i) = {k}
Tactic:
convert hwin (Ordinal.type r) rfl.le
State after:
case h.e'_2.h.e'_3.h.e'_3.h
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
x✝ : ι
⊢ Xs x✝ = ⋂ (_ : x✝ ∈ range fun p => Ordinal.enum r ↑p ⋯), Xs x✝

case h.e'_3
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ {k} = ⋂ i ∈ range fun p => Ordinal.enum r ↑p ⋯, M.cl (Xs i)