Theorem: Matroid.covBy_iff (Matroid/Flat.lean)

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ F₀ ⋖[M] F₁ ↔ M.Flat F₀ ∧ M.Flat F₁ ∧ F₀ ⊂ F₁ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
Tactic:
simp_rw [CovBy, covBy_iff_lt_and_eq_or_eq]
State after:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ (∃ (h : M.Flat F₀) (h_1 : M.Flat F₁),
      ⋯.toFlatOf < ⋯.toFlatOf ∧ ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf) ↔
    M.Flat F₀ ∧ M.Flat F₁ ∧ F₀ ⊂ F₁ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ (∃ (h : M.Flat F₀) (h_1 : M.Flat F₁),
      ⋯.toFlatOf < ⋯.toFlatOf ∧ ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf) ↔
    M.Flat F₀ ∧ M.Flat F₁ ∧ F₀ ⊂ F₁ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
Tactic:
refine ⟨fun ⟨h₀, h₁, hlt, hforall⟩ ↦ ⟨h₀, h₁, hlt, fun F hF hF₀ hF₁ ↦ ?_⟩,
  fun ⟨hF₀, hF₁, hss, hforall⟩ ↦ ⟨hF₀, hF₁, hss, ?_⟩⟩
State after:
case refine_1
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
x✝ :
  ∃ (h : M.Flat F₀) (h_1 : M.Flat F₁),
    ⋯.toFlatOf < ⋯.toFlatOf ∧ ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
h₀ : M.Flat F₀
h₁ : M.Flat F₁
hlt : ⋯.toFlatOf < ⋯.toFlatOf
hforall : ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
F : Set α
hF : M.Flat F
hF₀ : F₀ ⊆ F
hF₁ : F ⊆ F₁
⊢ F = F₀ ∨ F = F₁

case refine_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
x✝ : M.Flat F₀ ∧ M.Flat F₁ ∧ F₀ ⊂ F₁ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
hforall : ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
⊢ ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf

State before:
case refine_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
x✝ : M.Flat F₀ ∧ M.Flat F₁ ∧ F₀ ⊂ F₁ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
hforall : ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
⊢ ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
Tactic:
rintro ⟨F, hF⟩ (h₀ : F₀ ⊆ F) (h₁ : F ⊆ F₁)
State after:
case refine_2.mk
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
x✝ : M.Flat F₀ ∧ M.Flat F₁ ∧ F₀ ⊂ F₁ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
hforall : ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
F : Set α
hF : M.Flat F
h₀ : F₀ ⊆ F
h₁ : F ⊆ F₁
⊢ ⟨F, hF⟩ = ⋯.toFlatOf ∨ ⟨F, hF⟩ = ⋯.toFlatOf

State before:
case refine_2.mk
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
x✝ : M.Flat F₀ ∧ M.Flat F₁ ∧ F₀ ⊂ F₁ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
hforall : ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
F : Set α
hF : M.Flat F
h₀ : F₀ ⊆ F
h₁ : F ⊆ F₁
⊢ ⟨F, hF⟩ = ⋯.toFlatOf ∨ ⟨F, hF⟩ = ⋯.toFlatOf
Tactic:
obtain (rfl | rfl) := hforall F hF h₀ h₁
State after:
case refine_2.mk.inl
α : Type u_1
M : Matroid α
I F✝ X Y F' F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF₁ : M.Flat F₁
F : Set α
hF : M.Flat F
h₁ : F ⊆ F₁
x✝ : M.Flat F ∧ M.Flat F₁ ∧ F ⊂ F₁ ∧ ∀ (F_1 : Set α), M.Flat F_1 → F ⊆ F_1 → F_1 ⊆ F₁ → F_1 = F ∨ F_1 = F₁
hF₀ : M.Flat F
hss : F ⊂ F₁
hforall : ∀ (F_1 : Set α), M.Flat F_1 → F ⊆ F_1 → F_1 ⊆ F₁ → F_1 = F ∨ F_1 = F₁
h₀ : F ⊆ F
⊢ ⟨F, hF⟩ = ⋯.toFlatOf ∨ ⟨F, hF⟩ = ⋯.toFlatOf

case refine_2.mk.inr
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF₀ : M.Flat F₀
F : Set α
hF : M.Flat F
h₀ : F₀ ⊆ F
x✝ : M.Flat F₀ ∧ M.Flat F ∧ F₀ ⊂ F ∧ ∀ (F_1 : Set α), M.Flat F_1 → F₀ ⊆ F_1 → F_1 ⊆ F → F_1 = F₀ ∨ F_1 = F
hF₁ : M.Flat F
hss : F₀ ⊂ F
hforall : ∀ (F_1 : Set α), M.Flat F_1 → F₀ ⊆ F_1 → F_1 ⊆ F → F_1 = F₀ ∨ F_1 = F
h₁ : F ⊆ F
⊢ ⟨F, hF⟩ = ⋯.toFlatOf ∨ ⟨F, hF⟩ = ⋯.toFlatOf

State before:
case refine_2.mk.inr
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF₀ : M.Flat F₀
F : Set α
hF : M.Flat F
h₀ : F₀ ⊆ F
x✝ : M.Flat F₀ ∧ M.Flat F ∧ F₀ ⊂ F ∧ ∀ (F_1 : Set α), M.Flat F_1 → F₀ ⊆ F_1 → F_1 ⊆ F → F_1 = F₀ ∨ F_1 = F
hF₁ : M.Flat F
hss : F₀ ⊂ F
hforall : ∀ (F_1 : Set α), M.Flat F_1 → F₀ ⊆ F_1 → F_1 ⊆ F → F_1 = F₀ ∨ F_1 = F
h₁ : F ⊆ F
⊢ ⟨F, hF⟩ = ⋯.toFlatOf ∨ ⟨F, hF⟩ = ⋯.toFlatOf
Tactic:
exact Or.inr rfl
State after:
no goals

State before:
case refine_1
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
x✝ :
  ∃ (h : M.Flat F₀) (h_1 : M.Flat F₁),
    ⋯.toFlatOf < ⋯.toFlatOf ∧ ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
h₀ : M.Flat F₀
h₁ : M.Flat F₁
hlt : ⋯.toFlatOf < ⋯.toFlatOf
hforall : ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
F : Set α
hF : M.Flat F
hF₀ : F₀ ⊆ F
hF₁ : F ⊆ F₁
⊢ F = F₀ ∨ F = F₁
Tactic:
obtain (h1 | h2) := hforall ⟨F, hF⟩ hF₀ hF₁
State after:
case refine_1.inl
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
x✝ :
  ∃ (h : M.Flat F₀) (h_1 : M.Flat F₁),
    ⋯.toFlatOf < ⋯.toFlatOf ∧ ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
h₀ : M.Flat F₀
h₁ : M.Flat F₁
hlt : ⋯.toFlatOf < ⋯.toFlatOf
hforall : ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
F : Set α
hF : M.Flat F
hF₀ : F₀ ⊆ F
hF₁ : F ⊆ F₁
h1 : ⟨F, hF⟩ = ⋯.toFlatOf
⊢ F = F₀ ∨ F = F₁

case refine_1.inr
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
x✝ :
  ∃ (h : M.Flat F₀) (h_1 : M.Flat F₁),
    ⋯.toFlatOf < ⋯.toFlatOf ∧ ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
h₀ : M.Flat F₀
h₁ : M.Flat F₁
hlt : ⋯.toFlatOf < ⋯.toFlatOf
hforall : ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
F : Set α
hF : M.Flat F
hF₀ : F₀ ⊆ F
hF₁ : F ⊆ F₁
h2 : ⟨F, hF⟩ = ⋯.toFlatOf
⊢ F = F₀ ∨ F = F₁

State before:
case refine_1.inr
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
x✝ :
  ∃ (h : M.Flat F₀) (h_1 : M.Flat F₁),
    ⋯.toFlatOf < ⋯.toFlatOf ∧ ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
h₀ : M.Flat F₀
h₁ : M.Flat F₁
hlt : ⋯.toFlatOf < ⋯.toFlatOf
hforall : ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
F : Set α
hF : M.Flat F
hF₀ : F₀ ⊆ F
hF₁ : F ⊆ F₁
h2 : ⟨F, hF⟩ = ⋯.toFlatOf
⊢ F = F₀ ∨ F = F₁
Tactic:
exact Or.inr <| congr_arg ((↑) : M.FlatOf → Set α) h2
State after:
no goals

State before:
case refine_1.inl
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
x✝ :
  ∃ (h : M.Flat F₀) (h_1 : M.Flat F₁),
    ⋯.toFlatOf < ⋯.toFlatOf ∧ ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
h₀ : M.Flat F₀
h₁ : M.Flat F₁
hlt : ⋯.toFlatOf < ⋯.toFlatOf
hforall : ∀ (c : FlatOf M), ⋯.toFlatOf ≤ c → c ≤ ⋯.toFlatOf → c = ⋯.toFlatOf ∨ c = ⋯.toFlatOf
F : Set α
hF : M.Flat F
hF₀ : F₀ ⊆ F
hF₁ : F ⊆ F₁
h1 : ⟨F, hF⟩ = ⋯.toFlatOf
⊢ F = F₀ ∨ F = F₁
Tactic:
exact Or.inl <| congr_arg ((↑) : M.FlatOf → Set α) h1
State after:
no goals

State before:
case refine_2.mk.inl
α : Type u_1
M : Matroid α
I F✝ X Y F' F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF₁ : M.Flat F₁
F : Set α
hF : M.Flat F
h₁ : F ⊆ F₁
x✝ : M.Flat F ∧ M.Flat F₁ ∧ F ⊂ F₁ ∧ ∀ (F_1 : Set α), M.Flat F_1 → F ⊆ F_1 → F_1 ⊆ F₁ → F_1 = F ∨ F_1 = F₁
hF₀ : M.Flat F
hss : F ⊂ F₁
hforall : ∀ (F_1 : Set α), M.Flat F_1 → F ⊆ F_1 → F_1 ⊆ F₁ → F_1 = F ∨ F_1 = F₁
h₀ : F ⊆ F
⊢ ⟨F, hF⟩ = ⋯.toFlatOf ∨ ⟨F, hF⟩ = ⋯.toFlatOf
Tactic:
exact Or.inl rfl
State after:
no goals