internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Flat.cl_subset_of_subset
Proof 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
h : X ⊆ F
h' : M.cl X ≤ M.cl F
⊢ M.cl X ⊆ F
Tactic:
rwa [hF.cl] at h'
Proof state after:
no goals
Theorem: Matroid.Flat.cl_eq_iff_basis_of_indep
Proof 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
hI : M.Indep I
⊢ M.cl I = F → M.Basis I F
Tactic:
rintro rfl
Proof state after:
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hI : M.Indep I
hF : M.Flat (M.cl I)
⊢ M.Basis I (M.cl I)
Theorem: Matroid.Flat.cl_eq_iff_basis_of_indep
Proof state before:
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hI : M.Indep I
hF : M.Flat (M.cl I)
⊢ M.Basis I (M.cl I)
Tactic:
exact hI.basis_cl
Proof state after:
no goals
Theorem: Matroid.Flat.cl_eq_iff_basis_of_indep
Proof 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
hI : M.Indep I
h : M.Basis I F
⊢ M.cl I = F
Tactic:
rw [h.cl_eq_cl, hF.cl]
Proof state after:
no goals
Theorem: Matroid.Flat.er_insert_eq_add_one
Proof 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
he : e ∈ M.E \ F
⊢ M.er (insert e F) = M.er F + 1
Tactic:
rw [Matroid.er_insert_eq_add_one]
Proof state after:
case he
α : 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
he : e ∈ M.E \ F
⊢ e ∈ M.E \ M.cl F
Theorem: Matroid.Flat.er_insert_eq_add_one
Proof state before:
case he
α : 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
he : e ∈ M.E \ F
⊢ e ∈ M.E \ M.cl F
Tactic:
rwa [hF.cl]
Proof state after:
no goals
Theorem: Matroid.Flat.subset_of_relRank_eq_zero
Proof 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
hr : M.relRank F X = 0
hX : autoParam (X ⊆ M.E) _auto✝
⊢ X ⊆ F
Tactic:
rwa [relRank_eq_zero_iff, hF.cl] at hr
Proof state after:
no goals
Theorem: Matroid.uniqueBaseOn_flat_iff
Proof 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 : α
I E : Set α
hIE : I ⊆ E
⊢ (uniqueBaseOn E I).Flat F ↔ F ⊆ I
Tactic:
simp [flat_iff_cl_self, diff_eq_empty.2 hIE, inter_assoc, inter_eq_self_of_subset_right hIE]
Proof state after:
no goals
Theorem: Matroid.loopyOn_flat_iff
Proof 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 : α
E : Set α
⊢ (loopyOn E).Flat F ↔ F = E
Tactic:
simp [flat_iff_cl_self, eq_comm]
Proof state after:
no goals
Theorem: Matroid.emptyOn_flat_iff
Proof 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 : α
⊢ (emptyOn α).Flat F ↔ F = ∅
Tactic:
simp [← loopyOn_empty]
Proof state after:
no goals
Theorem: Matroid.freeOn_flat_iff
Proof 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 : α
E : Set α
⊢ (freeOn E).Flat F ↔ F ⊆ E
Tactic:
simp [← uniqueBaseOn_self, uniqueBaseOn_flat_iff Subset.rfl]
Proof state after:
no goals
Theorem: Matroid.FlatOf.coe_sInf'
Proof 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 : α
Fs : Set (FlatOf M)
hne : Fs.Nonempty
⊢ ↑(sInf Fs) = ⋂ F ∈ Fs, ↑F
Tactic:
simp only [coe_sInf, inter_eq_left]
Proof 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 : α
Fs : Set (FlatOf M)
hne : Fs.Nonempty
⊢ ⋂ F ∈ Fs, ↑F ⊆ M.E
Theorem: Matroid.FlatOf.coe_sInf'
Proof 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 : α
Fs : Set (FlatOf M)
hne : Fs.Nonempty
⊢ ⋂ F ∈ Fs, ↑F ⊆ M.E
Tactic:
exact (biInter_subset_of_mem hne.some_mem).trans (hne.some.coe_subset_ground)
Proof state after:
no goals
Theorem: Matroid.FlatOf.covBy_iff
Proof 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₀ F₁ : FlatOf M
⊢ F₀ ⋖ F₁ ↔ ↑F₀ ⋖[M] ↑F₁
Tactic:
simp only [Matroid.CovBy, coe_flat, exists_true_left]
Proof 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 : α
F₀ F₁ : FlatOf M
⊢ F₀ ⋖ F₁ ↔ ⋯.toFlatOf ⋖ ⋯.toFlatOf
Theorem: Matroid.FlatOf.covBy_iff
Proof 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₀ F₁ : FlatOf M
⊢ F₀ ⋖ F₁ ↔ ⋯.toFlatOf ⋖ ⋯.toFlatOf
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.FlatOf.wcovBy_iff
Proof 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₀ F₁ : FlatOf M
⊢ F₀ ⩿ F₁ ↔ ↑F₀ ⩿[M] ↑F₁
Tactic:
simp only [Matroid.WCovBy, coe_flat, exists_true_left]
Proof 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 : α
F₀ F₁ : FlatOf M
⊢ F₀ ⩿ F₁ ↔ ⋯.toFlatOf ⩿ ⋯.toFlatOf
Theorem: Matroid.FlatOf.wcovBy_iff
Proof 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₀ F₁ : FlatOf M
⊢ F₀ ⩿ F₁ ↔ ⋯.toFlatOf ⩿ ⋯.toFlatOf
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.covBy_iff
Proof 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]
Proof 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₁
Theorem: Matroid.covBy_iff
Proof 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, ?_⟩⟩
Proof 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
Theorem: Matroid.covBy_iff
Proof 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₁)
Proof 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
Theorem: Matroid.covBy_iff
Proof 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₁
Proof 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
Theorem: Matroid.covBy_iff
Proof 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
Proof state after:
no goals
Theorem: Matroid.covBy_iff
Proof 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₁
Proof 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₁
Theorem: Matroid.covBy_iff
Proof 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
Proof state after:
no goals
Theorem: Matroid.covBy_iff
Proof 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
Proof state after:
no goals
Theorem: Matroid.covBy_iff
Proof 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
Proof state after:
no goals
Theorem: Matroid.Flat.covBy_iff_wcovBy_and_ne
Proof 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₁
⊢ F₀ ⋖[M] F₁ ↔ (F₀ ⩿[M] F₁) ∧ F₀ ≠ F₁
Tactic:
rw [show F₀ = (hF₀.toFlatOf : Set α) from rfl, show F₁ = (hF₁.toFlatOf : Set α) from rfl,
  ← FlatOf.covBy_iff, ← FlatOf.wcovBy_iff, _root_.covBy_iff_wcovBy_and_ne, ne_eq, ne_eq,
  FlatOf.coe_inj]
Proof state after:
no goals
Theorem: Matroid.Flat.covBy_iff_wcovBy_and_ssubset
Proof 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₁
⊢ F₀ ⋖[M] F₁ ↔ (F₀ ⩿[M] F₁) ∧ F₀ ⊂ F₁
Tactic:
rw [hF₀.covBy_iff_wcovBy_and_ne hF₁, and_congr_right_iff, ssubset_iff_subset_ne,
  ne_eq, iff_and_self]
Proof 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₁
⊢ F₀ ⩿[M] F₁ → ¬F₀ = F₁ → F₀ ⊆ F₁
Theorem: Matroid.Flat.covBy_iff_wcovBy_and_ssubset
Proof 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₁
⊢ F₀ ⩿[M] F₁ → ¬F₀ = F₁ → F₀ ⊆ F₁
Tactic:
exact fun h _ ↦ h.subset
Proof state after:
no goals
Theorem: Matroid.Flat.wCovBy_self
Proof 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
⊢ F ⩿[M] F
Tactic:
simpa [WCovBy]
Proof state after:
no goals
Theorem: Matroid.Flat.wCovby_iff_covBy_or_eq
Proof 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₁
⊢ F₀ ⩿[M] F₁ ↔ (F₀ ⋖[M] F₁) ∨ F₀ = F₁
Tactic:
obtain (rfl | hne) := eq_or_ne F₀ F₁
Proof state after:
case 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₀ hF₁ : M.Flat F₀
⊢ F₀ ⩿[M] F₀ ↔ (F₀ ⋖[M] F₀) ∨ F₀ = F₀

case 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
hne : F₀ ≠ F₁
⊢ F₀ ⩿[M] F₁ ↔ (F₀ ⋖[M] F₁) ∨ F₀ = F₁
Theorem: Matroid.Flat.wCovby_iff_covBy_or_eq
Proof state before:
case 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
hne : F₀ ≠ F₁
⊢ F₀ ⩿[M] F₁ ↔ (F₀ ⋖[M] F₁) ∨ F₀ = F₁
Tactic:
simp [hF₀, hF₀.covBy_iff_wcovBy_and_ne hF₁, or_iff_not_imp_right, hne]
Proof state after:
no goals
Theorem: Matroid.Flat.wCovby_iff_covBy_or_eq
Proof state before:
case 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₀ hF₁ : M.Flat F₀
⊢ F₀ ⩿[M] F₀ ↔ (F₀ ⋖[M] F₀) ∨ F₀ = F₀
Tactic:
simp [hF₀]
Proof state after:
no goals
Theorem: Matroid.WCovBy.eq_or_covBy
Proof 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 : F₀ ⩿[M] F₁
⊢ F₀ = F₁ ∨ (F₀ ⋖[M] F₁)
Tactic:
rw [or_iff_not_imp_left]
Proof 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 : F₀ ⩿[M] F₁
⊢ ¬F₀ = F₁ → F₀ ⋖[M] F₁
Theorem: Matroid.WCovBy.eq_or_covBy
Proof 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 : F₀ ⩿[M] F₁
⊢ ¬F₀ = F₁ → F₀ ⋖[M] F₁
Tactic:
exact h.covBy_of_ne
Proof state after:
no goals
Theorem: Matroid.Flat.covBy_iff_of_flat
Proof 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₁
⊢ F₀ ⋖[M] F₁ ↔ F₀ ⊂ F₁ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
Tactic:
rw [covBy_iff, and_iff_right hF₀, and_iff_right hF₁]
Proof state after:
no goals
Theorem: Matroid.Flat.wcovBy_iff_of_flat
Proof 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₁
⊢ F₀ ⩿[M] F₁ ↔ F₀ ⊆ F₁ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
Tactic:
obtain (rfl | hne) := eq_or_ne F₀ F₁
Proof state after:
case 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₀ hF₁ : M.Flat F₀
⊢ F₀ ⩿[M] F₀ ↔ F₀ ⊆ F₀ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₀ → F = F₀ ∨ F = F₀

case 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
hne : F₀ ≠ F₁
⊢ F₀ ⩿[M] F₁ ↔ F₀ ⊆ F₁ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
Theorem: Matroid.Flat.wcovBy_iff_of_flat
Proof state before:
case 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
hne : F₀ ≠ F₁
⊢ F₀ ⩿[M] F₁ ↔ F₀ ⊆ F₁ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁
Tactic:
rw [wCovby_iff_covBy_or_eq hF₀ hF₁, subset_iff_ssubset_or_eq, or_iff_left hne, or_iff_left hne,
  hF₀.covBy_iff_of_flat hF₁]
Proof state after:
no goals
Theorem: Matroid.Flat.wcovBy_iff_of_flat
Proof state before:
case 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₀ hF₁ : M.Flat F₀
⊢ F₀ ⩿[M] F₀ ↔ F₀ ⊆ F₀ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₀ → F = F₀ ∨ F = F₀
Tactic:
simp only [hF₀, wCovBy_self, or_self, true_iff]
Proof state after:
case 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₀ hF₁ : M.Flat F₀
⊢ F₀ ⊆ F₀ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₀ → F = F₀
Theorem: Matroid.Flat.wcovBy_iff_of_flat
Proof state before:
case 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₀ hF₁ : M.Flat F₀
⊢ F₀ ⊆ F₀ ∧ ∀ (F : Set α), M.Flat F → F₀ ⊆ F → F ⊆ F₀ → F = F₀
Tactic:
exact ⟨Subset.rfl, fun _ _  ↦ antisymm'⟩
Proof state after:
no goals
Theorem: Matroid.CovBy.cl_insert_eq
Proof 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 : F₀ ⋖[M] F₁
he : e ∈ F₁ \ F₀
⊢ M.cl (insert e F₀) = F₁
Tactic:
refine'
  h.eq_of_ssubset_of_subset (M.cl_flat _)
    ((ssubset_insert he.2).trans_subset (M.subset_cl _ _))
    (h.flat_right.cl_subset_of_subset (insert_subset he.1 h.ssubset.subset))
Proof 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 : F₀ ⋖[M] F₁
he : e ∈ F₁ \ F₀
⊢ insert e F₀ ⊆ M.E
Theorem: Matroid.CovBy.cl_insert_eq
Proof 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 : F₀ ⋖[M] F₁
he : e ∈ F₁ \ F₀
⊢ insert e F₀ ⊆ M.E
Tactic:
rw [insert_eq, union_subset_iff, singleton_subset_iff]
Proof 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 : F₀ ⋖[M] F₁
he : e ∈ F₁ \ F₀
⊢ e ∈ M.E ∧ F₀ ⊆ M.E
Theorem: Matroid.CovBy.cl_insert_eq
Proof 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 : F₀ ⋖[M] F₁
he : e ∈ F₁ \ F₀
⊢ e ∈ M.E ∧ F₀ ⊆ M.E
Tactic:
exact ⟨h.flat_right.subset_ground he.1, h.flat_left.subset_ground⟩
Proof state after:
no goals
Theorem: Matroid.CovBy.exists_eq_cl_insert
Proof 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 : F₀ ⋖[M] F₁
⊢ ∃ e ∈ F₁ \ F₀, M.cl (insert e F₀) = F₁
Tactic:
obtain ⟨e, he⟩ := exists_of_ssubset h.ssubset
Proof state after:
case intro
α : 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 : F₀ ⋖[M] F₁
e : α
he : e ∈ F₁ ∧ e ∉ F₀
⊢ ∃ e ∈ F₁ \ F₀, M.cl (insert e F₀) = F₁
Theorem: Matroid.CovBy.exists_eq_cl_insert
Proof state before:
case intro
α : 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 : F₀ ⋖[M] F₁
e : α
he : e ∈ F₁ ∧ e ∉ F₀
⊢ ∃ e ∈ F₁ \ F₀, M.cl (insert e F₀) = F₁
Tactic:
exact ⟨e, he, h.cl_insert_eq he⟩
Proof state after:
no goals
Theorem: Matroid.CovBy.exists_eq_cl_insert'
Proof 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.cl X ⋖[M] F
⊢ ∃ e ∈ F \ M.cl X, F = M.cl (insert e X)
Tactic:
obtain ⟨e, he, rfl⟩ := h.exists_eq_cl_insert
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f e : α
h : M.cl X ⋖[M] M.cl (insert e (M.cl X))
he : e ∈ M.cl (insert e (M.cl X)) \ M.cl X
⊢ ∃ e_1 ∈ M.cl (insert e (M.cl X)) \ M.cl X, M.cl (insert e (M.cl X)) = M.cl (insert e_1 X)
Theorem: Matroid.CovBy.exists_eq_cl_insert'
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f e : α
h : M.cl X ⋖[M] M.cl (insert e (M.cl X))
he : e ∈ M.cl (insert e (M.cl X)) \ M.cl X
⊢ ∃ e_1 ∈ M.cl (insert e (M.cl X)) \ M.cl X, M.cl (insert e (M.cl X)) = M.cl (insert e_1 X)
Tactic:
exact ⟨e, he, by simp⟩
Proof state after:
no goals
Theorem: Matroid.CovBy.exists_eq_cl_insert'
Proof state before:
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f e : α
h : M.cl X ⋖[M] M.cl (insert e (M.cl X))
he : e ∈ M.cl (insert e (M.cl X)) \ M.cl X
⊢ M.cl (insert e (M.cl X)) = M.cl (insert e X)
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.Flat.covBy_iff_eq_cl_insert
Proof 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₀
⊢ F₀ ⋖[M] F₁ ↔ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)
Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
Proof 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 : α
hF₀ : M.Flat F₀
h : F₀ ⋖[M] F₁
⊢ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e 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 : α
hF₀ : M.Flat F₀
⊢ (∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) → F₀ ⋖[M] F₁
Theorem: Matroid.Flat.covBy_iff_eq_cl_insert
Proof 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 : α
hF₀ : M.Flat F₀
⊢ (∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) → F₀ ⋖[M] F₁
Tactic:
rintro ⟨e, heF₀, rfl⟩
Proof state after:
case refine_2.intro.intro
α : 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₀
e : α
heF₀ : e ∈ M.E \ F₀
⊢ F₀ ⋖[M] M.cl (insert e F₀)