internlm/Lean-Github huggingface dataset:
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
⊢ I ∈
    {a |
      a ∈ {S | M.Indep S ∧ S ⊆ A} ∧
        ∀ ⦃b : Set α⦄, b ∈ {S | M.Indep S ∧ S ⊆ A} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
Tactic:
simp only [Set.mem_setOf_eq, and_imp]
Proof state after:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
⊢ (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
⊢ (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
Tactic:
exact ⟨⟨hI_indep, hI_subset⟩, hI_max⟩
Proof state after:
no goals
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
⊢ M.relRank J B = 0
Tactic:
rw [<-indep_subset_maximal_iff_relRank_zero hJ_subset hJ_indep]
Proof state after:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
⊢ J ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ B}
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
⊢ J ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ B}
Tactic:
unfold maximals
Proof state after:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
⊢ J ∈
    {a |
      a ∈ {S | M.Indep S ∧ S ⊆ B} ∧
        ∀ ⦃b : Set α⦄, b ∈ {S | M.Indep S ∧ S ⊆ B} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
⊢ J ∈
    {a |
      a ∈ {S | M.Indep S ∧ S ⊆ B} ∧
        ∀ ⦃b : Set α⦄, b ∈ {S | M.Indep S ∧ S ⊆ B} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
Tactic:
simp only [Set.mem_setOf_eq, and_imp]
Proof state after:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
⊢ (M.Indep J ∧ J ⊆ B) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
⊢ (M.Indep J ∧ J ⊆ B) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
Tactic:
exact ⟨⟨hJ_indep, hJ_subset⟩, hJ_max⟩
Proof state after:
no goals
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
hJB : M.relRank J B = 0
⊢ M.relRank A B = M.relRank I A + M.relRank A B
Tactic:
rw [hIA]
Proof state after:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
hJB : M.relRank J B = 0
⊢ M.relRank A B = 0 + M.relRank A B
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
hJB : M.relRank J B = 0
⊢ M.relRank A B = 0 + M.relRank A B
Tactic:
simp only [zero_add]
Proof state after:
no goals
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
hJB : M.relRank J B = 0
⊢ M.relRank I A + M.relRank A B = M.relRank I B
Tactic:
exact eq_comm.mp (M.relRank_add_cancel hI_subset hA)
Proof state after:
no goals
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
hJB : M.relRank J B = 0
⊢ M.relRank I B = M.relRank I J + M.relRank J B
Tactic:
exact M.relRank_add_cancel hI hJ_subset
Proof state after:
no goals
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
hJB : M.relRank J B = 0
⊢ M.relRank I J + M.relRank J B = M.relRank I J
Tactic:
rw [hJB]
Proof state after:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
hJB : M.relRank J B = 0
⊢ M.relRank I J + 0 = M.relRank I J
Theorem: RankMatroid.rankMatroid_relRank_eq_matroid_relRank
Proof state before:
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
hJB : M.relRank J B = 0
⊢ M.relRank I J + 0 = M.relRank I J
Tactic:
simp only [add_zero]
Proof state after:
no goals
Theorem: Matroid.numPoints_eq_encard_parallelClasses
Proof state before:
α : Type u_1
M✝ M : Matroid α
⊢ M.numPoints = (↑M.parallelClasses).encard
Tactic:
rw [numPoints, ← encard_univ_coe, M.parallelPointEquiv.symm.encard_univ_eq, encard_univ_coe]
Proof state after:
no goals
Theorem: Matroid.numPoints_eq_encard_ground_simplification
Proof state before:
α : Type u_1
M✝ M : Matroid α
⊢ M.numPoints = M.simplification.E.encard
Tactic:
rw [numPoints_eq_encard_parallelClasses, M.simplification_equiv.encard_eq]
Proof state after:
α : Type u_1
M✝ M : Matroid α
⊢ (↑M.parallelClasses).encard = M.simplification.E.encard
Theorem: Matroid.numPoints_eq_encard_ground
Proof state before:
α : Type u_1
M✝ M : Matroid α
inst✝ : M.Simple
⊢ M.numPoints = M.E.encard
Tactic:
simp [numPoints_eq_encard_ground_simplification]
Proof state after:
no goals
Theorem: Matroid.encard_ground_eq_sum_encard_lines_through
Proof state before:
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ M.E.encard = 1 + ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard
Tactic:
rw [← encard_diff_add_encard_of_subset (singleton_subset_iff.2 he), add_comm, encard_singleton]
Proof state after:
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ 1 + (M.E \ {e}).encard = 1 + ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard
Theorem: Matroid.encard_ground_eq_sum_encard_lines_through
Proof state before:
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ (M.E \ {e}).encard = ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard
Tactic:
convert (ENat.tsum_encard_eq_encard_sUnion (M ／ e).parallelClasses.pairwiseDisjoint).symm using 1
Proof state after:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ (M.E \ {e}).encard = (⋃₀ ↑(M ／ e).parallelClasses).encard

case h.e'_3
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard = ∑' (t : ↑↑(M ／ e).parallelClasses), (↑t).encard
Theorem: Matroid.encard_ground_eq_sum_encard_lines_through
Proof state before:
case h.e'_3
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard = ∑' (t : ↑↑(M ／ e).parallelClasses), (↑t).encard
Tactic:
convert ENat.tsum_comp_eq_tsum_of_equiv (M ／ e).parallelPointEquiv.symm (g := fun x ↦ x.1.encard)
  using 1
Proof state after:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard =
    ∑' (x : { P // (M ／ e).Point P }), (↑((M ／ e).parallelPointEquiv.symm x)).encard
Theorem: Matroid.encard_ground_eq_sum_encard_lines_through
Proof state before:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard =
    ∑' (x : { P // (M ／ e).Point P }), (↑((M ／ e).parallelPointEquiv.symm x)).encard
Tactic:
rw [← ENat.tsum_comp_eq_tsum_of_equiv (toNonloop he).lineContractPointEquiv]
Proof state after:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ ∑' (x : { P // (M ／ e).Point P }), (↑(⋯.lineContractPointEquiv x) \ {e}).encard =
    ∑' (x : { P // (M ／ e).Point P }), (↑((M ／ e).parallelPointEquiv.symm x)).encard
Theorem: Matroid.encard_ground_eq_sum_encard_lines_through
Proof state before:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ ∑' (x : { P // (M ／ e).Point P }), (↑(⋯.lineContractPointEquiv x) \ {e}).encard =
    ∑' (x : { P // (M ／ e).Point P }), (↑((M ／ e).parallelPointEquiv.symm x)).encard
Tactic:
refine tsum_congr (fun ⟨P,hP⟩ ↦ ?_)
Proof state after:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
x✝ : { P // (M ／ e).Point P }
P : Set α
hP : (M ／ e).Point P
⊢ (↑(⋯.lineContractPointEquiv ⟨P, hP⟩) \ {e}).encard = (↑((M ／ e).parallelPointEquiv.symm ⟨P, hP⟩)).encard
Theorem: Matroid.encard_ground_eq_sum_encard_lines_through
Proof state before:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
x✝ : { P // (M ／ e).Point P }
P : Set α
hP : (M ／ e).Point P
⊢ (↑(⋯.lineContractPointEquiv ⟨P, hP⟩) \ {e}).encard = (↑((M ／ e).parallelPointEquiv.symm ⟨P, hP⟩)).encard
Tactic:
simp [Nonloop.lineContractPointEquiv, cl_singleton_eq he,
  diff_singleton_eq_self (fun heP ↦ (hP.subset_ground heP).2 rfl)]
Proof state after:
no goals
Theorem: Matroid.encard_ground_eq_sum_encard_lines_through
Proof state before:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ (M.E \ {e}).encard = (⋃₀ ↑(M ／ e).parallelClasses).encard
Tactic:
simp only [contract_elem, Partition.sUnion_eq, contract_nonloop_iff, mem_diff]
Proof state after:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ (M.E \ {e}).encard = {e_1 | e_1 ∈ M.E ∧ e_1 ∉ M.cl {e}}.encard
Theorem: Matroid.encard_ground_eq_sum_encard_lines_through
Proof state before:
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ (M.E \ {e}).encard = {e_1 | e_1 ∈ M.E ∧ e_1 ∉ M.cl {e}}.encard
Tactic:
congr
Proof state after:
case h.e'_2.e_s.e_a
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ {e} = M.cl {e}
Theorem: Matroid.encard_ground_eq_sum_encard_lines_through
Proof state before:
case h.e'_2.e_s.e_a
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ {e} = M.cl {e}
Tactic:
rw [cl_singleton_eq]
Proof state after:
no goals
Theorem: Matroid.kung
Proof state before:
α : Type u_1
M✝ : Matroid α
q : ℕ
M : Matroid α
hM : ¬sorryAx Prop true
⊢ M.numPoints ≤ ↑(∑' (i : { i // ↑i ≤ M.erk }), q ^ ↑i)
Tactic:
_
Proof state after:
no goals
Theorem: Matroid.comap_dep_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
⊢ (N.comap f).Dep I ↔ N.Dep (f '' I) ∨ N.Indep (f '' I) ∧ ¬InjOn f I
Tactic:
rw [Dep, comap_indep_iff, not_and, comap_ground_eq, Dep, image_subset_iff]
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E ↔ ¬N.Indep (f '' I) ∧ I ⊆ f ⁻¹' N.E ∨ N.Indep (f '' I) ∧ ¬InjOn f I
Theorem: Matroid.comap_dep_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E ↔ ¬N.Indep (f '' I) ∧ I ⊆ f ⁻¹' N.E ∨ N.Indep (f '' I) ∧ ¬InjOn f I
Tactic:
refine ⟨fun ⟨hi, h⟩ ↦ ?_, ?_⟩
Proof state after:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
x✝ : (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E
hi : N.Indep (f '' I) → ¬InjOn f I
h : I ⊆ f ⁻¹' N.E
⊢ ¬N.Indep (f '' I) ∧ I ⊆ f ⁻¹' N.E ∨ N.Indep (f '' I) ∧ ¬InjOn f I

case refine_2
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
⊢ ¬N.Indep (f '' I) ∧ I ⊆ f ⁻¹' N.E ∨ N.Indep (f '' I) ∧ ¬InjOn f I → (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E
Theorem: Matroid.comap_dep_iff
Proof state before:
case refine_2
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
⊢ ¬N.Indep (f '' I) ∧ I ⊆ f ⁻¹' N.E ∨ N.Indep (f '' I) ∧ ¬InjOn f I → (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E
Tactic:
rintro (⟨hI, hIE⟩ | hI)
Proof state after:
case refine_2.inl.intro
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hI : ¬N.Indep (f '' I)
hIE : I ⊆ f ⁻¹' N.E
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E

case refine_2.inr
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E
Theorem: Matroid.comap_dep_iff
Proof state before:
case refine_2.inr
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E
Tactic:
rw [iff_true_intro hI.1, iff_true_intro hI.2, implies_true, true_and]
Proof state after:
case refine_2.inr
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ I ⊆ f ⁻¹' N.E
Theorem: Matroid.comap_dep_iff
Proof state before:
case refine_2.inr
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ I ⊆ f ⁻¹' N.E
Tactic:
simpa using hI.1.subset_ground
Proof state after:
no goals
Theorem: Matroid.comap_dep_iff
Proof state before:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
x✝ : (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E
hi : N.Indep (f '' I) → ¬InjOn f I
h : I ⊆ f ⁻¹' N.E
⊢ ¬N.Indep (f '' I) ∧ I ⊆ f ⁻¹' N.E ∨ N.Indep (f '' I) ∧ ¬InjOn f I
Tactic:
rw [and_iff_left h, ← imp_iff_not_or]
Proof state after:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
x✝ : (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E
hi : N.Indep (f '' I) → ¬InjOn f I
h : I ⊆ f ⁻¹' N.E
⊢ N.Indep (f '' I) → N.Indep (f '' I) ∧ ¬InjOn f I
Theorem: Matroid.comap_dep_iff
Proof state before:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
x✝ : (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E
hi : N.Indep (f '' I) → ¬InjOn f I
h : I ⊆ f ⁻¹' N.E
⊢ N.Indep (f '' I) → N.Indep (f '' I) ∧ ¬InjOn f I
Tactic:
exact fun hI ↦ ⟨hI, hi hI⟩
Proof state after:
no goals
Theorem: Matroid.comap_dep_iff
Proof state before:
case refine_2.inl.intro
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hI : ¬N.Indep (f '' I)
hIE : I ⊆ f ⁻¹' N.E
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E
Tactic:
exact ⟨fun h ↦ (hI h).elim, hIE⟩
Proof state after:
no goals
Theorem: Matroid.comap_id
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N✝ N : Matroid β
⊢ ∀ I ⊆ (N.comap id).E, (N.comap id).Indep I ↔ N.Indep I
Tactic:
simp [injective_id.injOn]
Proof state after:
no goals
Theorem: Matroid.comap_indep_iff_of_injOn
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
⊢ (N.comap f).Indep I ↔ N.Indep (f '' I)
Tactic:
rw [comap_indep_iff, and_iff_left_iff_imp]
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
⊢ N.Indep (f '' I) → InjOn f I
Theorem: Matroid.comap_indep_iff_of_injOn
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
⊢ N.Indep (f '' I) → InjOn f I
Tactic:
refine fun hi ↦ hf.mono <| subset_trans ?_ (preimage_mono hi.subset_ground)
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
hi : N.Indep (f '' I)
⊢ I ⊆ f ⁻¹' (f '' I)
Theorem: Matroid.comap_indep_iff_of_injOn
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
hi : N.Indep (f '' I)
⊢ I ⊆ f ⁻¹' (f '' I)
Tactic:
apply subset_preimage_image
Proof state after:
no goals
Theorem: Matroid.comap_emptyOn
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α → β
⊢ (emptyOn β).comap f = emptyOn α
Tactic:
simp [← ground_eq_empty_iff]
Proof state after:
no goals
Theorem: Matroid.comap_loopyOn
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
f : α → β
E : Set β
⊢ (loopyOn E).comap f = loopyOn (f ⁻¹' E)
Tactic:
rw [eq_loopyOn_iff]
Proof state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
f : α → β
E : Set β
⊢ ((loopyOn E).comap f).E = f ⁻¹' E ∧ ∀ X ⊆ ((loopyOn E).comap f).E, ((loopyOn E).comap f).Indep X → X = ∅
Theorem: Matroid.comap_loopyOn
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
f : α → β
E : Set β
⊢ ((loopyOn E).comap f).E = f ⁻¹' E ∧ ∀ X ⊆ ((loopyOn E).comap f).E, ((loopyOn E).comap f).Indep X → X = ∅
Tactic:
aesop
Proof state after:
no goals
Theorem: Matroid.comap_basis_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
⊢ (N.comap f).Basis I X ↔ N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
Proof state after:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
⊢ N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I

case refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
⊢ (N.comap f).Basis I X
Theorem: Matroid.comap_basis_iff
Proof state before:
case refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
⊢ (N.comap f).Basis I X
Tactic:
refine Indep.basis_of_forall_insert ?_ h.2.1 fun e ⟨heX, heI⟩ ↦ ?_
Proof state after:
case refine_2.refine_1
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
⊢ (N.comap f).Indep I

case refine_2.refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ (N.comap f).Dep (insert e I)