Theorem: foo (Matroid/scratch.lean)

State before:
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
⊢ P univ
Tactic:
set r : ι → ι → Prop := WellOrderingRel
State after:
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
⊢ P univ

State before:
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
⊢ P univ
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
  rw [eq_comm, eq_univ_iff_forall]
  refine fun i ↦ ⟨⟨Ordinal.typein r i, Ordinal.typein_lt_type r i⟩, Ordinal.enum_typein _ _⟩
State after:
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
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 α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
⊢ ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
Tactic:
intro o
State after:
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
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 α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
o : Ordinal.{u}
⊢ ∀ (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
Tactic:
induction' o using Ordinal.induction with p hp
State after:
case h
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
p : Ordinal.{u}
hp : ∀ k < p, ∀ (ho : k ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ ∀ (ho : p ≤ Ordinal.type r), P (range fun p_1 => Ordinal.enum r ↑p_1 ⋯)

State before:
case h
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
p : Ordinal.{u}
hp : ∀ k < p, ∀ (ho : k ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ ∀ (ho : p ≤ Ordinal.type r), P (range fun p_1 => Ordinal.enum r ↑p_1 ⋯)
Tactic:
intro hpr
State after:
case h
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
p : Ordinal.{u}
hp : ∀ k < p, ∀ (ho : k ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
hpr : p ≤ Ordinal.type r
⊢ P (range fun p_1 => Ordinal.enum r ↑p_1 ⋯)

State before:
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ P univ
Tactic:
convert hwin (Ordinal.type r) rfl.le
State after:
case h.e'_1
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ univ = range fun p => Ordinal.enum r ↑p ⋯

State before:
case h.e'_1
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ univ = range fun p => Ordinal.enum r ↑p ⋯
Tactic:
rw [eq_comm, eq_univ_iff_forall]
State after:
case h.e'_1
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ ∀ (x : ι), x ∈ range fun p => Ordinal.enum r ↑p ⋯

State before:
case h.e'_1
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ ∀ (x : ι), x ∈ range fun p => Ordinal.enum r ↑p ⋯
Tactic:
refine fun i ↦ ⟨⟨Ordinal.typein r i, Ordinal.typein_lt_type r i⟩, Ordinal.enum_typein _ _⟩
State after:
no goals