Theorem: Matroid.Flat.covBy_and_covBy_of_ssubset_of_ssubset_of_relRank_eq_two (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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Tactic:
have h0le := hF₀.one_le_relRank_of_ssubset h₀
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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Tactic:
have h1le := hF.one_le_relRank_of_ssubset h₁
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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Tactic:
rw [← M.relRank_add_of_subset_of_subset h₀.subset h₁.subset] at h
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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Tactic:
have h0top : M.relRank F₀ F ≠ ⊤ := by
  intro h'; rw [h'] at h; norm_cast at h
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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Tactic:
have h1top : M.relRank F F₁ ≠ ⊤ := by
  intro h'; rw [h', add_top] at h; norm_cast at h
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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h1top : M.relRank F F₁ ≠ ⊤
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h1top : M.relRank F F₁ ≠ ⊤
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Tactic:
have hle1 := WithTop.le_of_add_le_add_left h0top <| h.le.trans (add_le_add_right h0le 1)
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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h1top : M.relRank F F₁ ≠ ⊤
hle1 : M.relRank F F₁ ≤ 1
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h1top : M.relRank F F₁ ≠ ⊤
hle1 : M.relRank F F₁ ≤ 1
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Tactic:
have hle0 := WithTop.le_of_add_le_add_right h1top <| h.le.trans (add_le_add_left h1le 1)
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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h1top : M.relRank F F₁ ≠ ⊤
hle1 : M.relRank F F₁ ≤ 1
hle0 : M.relRank F₀ F ≤ 1
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h1top : M.relRank F F₁ ≠ ⊤
hle1 : M.relRank F F₁ ≤ 1
hle0 : M.relRank F₀ F ≤ 1
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Tactic:
rw [hF₀.covBy_iff_relRank_eq_one hF, hF.covBy_iff_relRank_eq_one hF₁,
  and_iff_right h₀.subset, and_iff_right h₁.subset]
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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h1top : M.relRank F F₁ ≠ ⊤
hle1 : M.relRank F F₁ ≤ 1
hle0 : M.relRank F₀ F ≤ 1
⊢ M.relRank F₀ F = 1 ∧ M.relRank F F₁ = 1

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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h1top : M.relRank F F₁ ≠ ⊤
hle1 : M.relRank F F₁ ≤ 1
hle0 : M.relRank F₀ F ≤ 1
⊢ M.relRank F₀ F = 1 ∧ M.relRank F F₁ = 1
Tactic:
exact ⟨hle0.antisymm h0le, hle1.antisymm h1le⟩
State after:
no goals

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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
⊢ M.relRank F₀ F ≠ ⊤
Tactic:
intro h'
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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h' : M.relRank F₀ F = ⊤
⊢ False

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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h' : M.relRank F₀ F = ⊤
⊢ False
Tactic:
rw [h'] at h
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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : ⊤ + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h' : M.relRank F₀ F = ⊤
⊢ False

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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : ⊤ + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h' : M.relRank F₀ F = ⊤
⊢ False
Tactic:
norm_cast at h
State after:
no goals

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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
⊢ M.relRank F F₁ ≠ ⊤
Tactic:
intro h'
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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h' : M.relRank F F₁ = ⊤
⊢ False

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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h' : M.relRank F F₁ = ⊤
⊢ False
Tactic:
rw [h', add_top] at h
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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : ⊤ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h' : M.relRank F F₁ = ⊤
⊢ False

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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : ⊤ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h' : M.relRank F F₁ = ⊤
⊢ False
Tactic:
norm_cast at h
State after:
no goals