internlm/Lean-Github huggingface dataset:
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
h : (B \ A).encard = ↑n.succ
this : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
⊢ ((B \ A) \ {x}).encard = ↑n
Tactic:
rw [<-Set.encard_diff_singleton_add_one hx] at h
Proof state after:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
this : (B \ A).encard > 0
x : α
h : ((B \ A) \ {x}).encard + 1 = ↑n.succ
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
⊢ ((B \ A) \ {x}).encard = ↑n
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
this : (B \ A).encard > 0
x : α
h : ((B \ A) \ {x}).encard + 1 = ↑n.succ
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
⊢ ((B \ A) \ {x}).encard = ↑n
Tactic:
simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one] at h
Proof state after:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
this : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
h : ((B \ A) \ {x}).encard + 1 = ↑n + 1
⊢ ((B \ A) \ {x}).encard = ↑n
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
this : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
h : ((B \ A) \ {x}).encard + 1 = ↑n + 1
⊢ ((B \ A) \ {x}).encard = ↑n
Tactic:
exact WithTop.add_right_cancel (ENat.coe_toNat_eq_self.mp (refl 1)) h
Proof state after:
no goals
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
h : (B \ A).encard = ↑n.succ
this✝ : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
this : (B' \ A).encard = ↑n
hrAB' : M.relRank A B' = ↑n
⊢ M.relRank B' B = 1
Tactic:
have hle : M.relRank B' B <= 1 := by
  have := M.relRank_le_encard_diff (B \ {x}) B
  rw [Set.diff_diff_cancel_left (Set.singleton_subset_iff.mpr hxB)] at this
  simp only [Set.encard_singleton] at this; exact this
Proof state after:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
h : (B \ A).encard = ↑n.succ
this✝ : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
this : (B' \ A).encard = ↑n
hrAB' : M.relRank A B' = ↑n
hle : M.relRank B' B ≤ 1
⊢ M.relRank B' B = 1
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
h : (B \ A).encard = ↑n.succ
this✝ : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
this : (B' \ A).encard = ↑n
hrAB' : M.relRank A B' = ↑n
hle : M.relRank B' B ≤ 1
⊢ M.relRank B' B = 1
Tactic:
have hgt : M.relRank B' B > 0 := by exact hB_indep.indep x hxB
Proof state after:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
h : (B \ A).encard = ↑n.succ
this✝ : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
this : (B' \ A).encard = ↑n
hrAB' : M.relRank A B' = ↑n
hle : M.relRank B' B ≤ 1
hgt : M.relRank B' B > 0
⊢ M.relRank B' B = 1
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
h : (B \ A).encard = ↑n.succ
this✝ : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
this : (B' \ A).encard = ↑n
hrAB' : M.relRank A B' = ↑n
hle : M.relRank B' B ≤ 1
hgt : M.relRank B' B > 0
⊢ M.relRank B' B = 1
Tactic:
refine le_antisymm_iff.mpr ⟨hle, ENat.one_le_iff_pos.mpr hgt⟩
Proof state after:
no goals
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
h : (B \ A).encard = ↑n.succ
this✝ : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
this : (B' \ A).encard = ↑n
hrAB' : M.relRank A B' = ↑n
⊢ M.relRank B' B ≤ 1
Tactic:
have := M.relRank_le_encard_diff (B \ {x}) B
Proof state after:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
h : (B \ A).encard = ↑n.succ
this✝¹ : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
this✝ : (B' \ A).encard = ↑n
hrAB' : M.relRank A B' = ↑n
this : M.relRank (B \ {x}) B ≤ (B \ (B \ {x})).encard
⊢ M.relRank B' B ≤ 1
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
h : (B \ A).encard = ↑n.succ
this✝¹ : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
this✝ : (B' \ A).encard = ↑n
hrAB' : M.relRank A B' = ↑n
this : M.relRank (B \ {x}) B ≤ (B \ (B \ {x})).encard
⊢ M.relRank B' B ≤ 1
Tactic:
rw [Set.diff_diff_cancel_left (Set.singleton_subset_iff.mpr hxB)] at this
Proof state after:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
h : (B \ A).encard = ↑n.succ
this✝¹ : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
this✝ : (B' \ A).encard = ↑n
hrAB' : M.relRank A B' = ↑n
this : M.relRank (B \ {x}) B ≤ {x}.encard
⊢ M.relRank B' B ≤ 1
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
h : (B \ A).encard = ↑n.succ
this✝¹ : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
this✝ : (B' \ A).encard = ↑n
hrAB' : M.relRank A B' = ↑n
this : M.relRank (B \ {x}) B ≤ {x}.encard
⊢ M.relRank B' B ≤ 1
Tactic:
simp only [Set.encard_singleton] at this
Proof state after:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
h : (B \ A).encard = ↑n.succ
this✝¹ : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
this✝ : (B' \ A).encard = ↑n
hrAB' : M.relRank A B' = ↑n
this : M.relRank (B \ {x}) B ≤ 1
⊢ M.relRank B' B ≤ 1
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
h : (B \ A).encard = ↑n.succ
this✝¹ : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
this✝ : (B' \ A).encard = ↑n
hrAB' : M.relRank A B' = ↑n
this : M.relRank (B \ {x}) B ≤ 1
⊢ M.relRank B' B ≤ 1
Tactic:
exact this
Proof state after:
no goals
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
h : (B \ A).encard = ↑n.succ
this✝ : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
this : (B' \ A).encard = ↑n
hrAB' : M.relRank A B' = ↑n
hle : M.relRank B' B ≤ 1
⊢ M.relRank B' B > 0
Tactic:
exact hB_indep.indep x hxB
Proof state after:
no goals
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ : Set α
hA : A✝ ⊆ B✝
hB✝ : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
h_finite : M.relRank A B ≠ ⊤
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
hD_finite : D.Finite
hD_ncard : D.ncard = ENat.toNat c + 1
⊢ c ≠ ⊤
Tactic:
rwa [hc] at h_finite
Proof state after:
no goals
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ : Set α
hA : A✝ ⊆ B✝
hB✝ : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
h_finite : M.relRank A B ≠ ⊤
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
hD_finite : D.Finite
hD_ncard : D.ncard = ENat.toNat c + 1
c_finite : c ≠ ⊤
⊢ c + 1 = ↑(ENat.toNat c + 1)
Tactic:
simp only [Nat.cast_add, Nat.cast_one, ENat.coe_toNat_eq_self.mpr c_finite]
Proof state after:
no goals
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ : Set α
hA : A✝ ⊆ B✝
hB✝ : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
h_finite : M.relRank A B ≠ ⊤
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
hD_finite : D.Finite
hD_ncard : D.ncard = ENat.toNat c + 1
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
⊢ D.encard = c + 1
Tactic:
have : D.encard = (D.ncard : ℕ∞) := by exact Eq.symm (Set.Finite.cast_ncard_eq hD_finite)
Proof state after:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ : Set α
hA : A✝ ⊆ B✝
hB✝ : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
h_finite : M.relRank A B ≠ ⊤
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
hD_finite : D.Finite
hD_ncard : D.ncard = ENat.toNat c + 1
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
this : D.encard = ↑D.ncard
⊢ D.encard = c + 1
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ : Set α
hA : A✝ ⊆ B✝
hB✝ : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
h_finite : M.relRank A B ≠ ⊤
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
hD_finite : D.Finite
hD_ncard : D.ncard = ENat.toNat c + 1
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
this : D.encard = ↑D.ncard
⊢ D.encard = c + 1
Tactic:
rw [this, congrArg (Nat.cast) hD_ncard, hcc]
Proof state after:
no goals
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ : Set α
hA : A✝ ⊆ B✝
hB✝ : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
h_finite : M.relRank A B ≠ ⊤
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
hD_finite : D.Finite
hD_ncard : D.ncard = ENat.toNat c + 1
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
⊢ D.encard = ↑D.ncard
Tactic:
exact Eq.symm (Set.Finite.cast_ncard_eq hD_finite)
Proof state after:
no goals
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ : Set α
hA : A✝ ⊆ B✝
hB✝ : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
hD_encard : D.encard = c + 1
A' : Set α := A ∪ D
hD_subset_B : D ⊆ B
⊢ A' ⊆ B
Tactic:
exact (Set.union_subset hB hD_subset_B)
Proof state after:
no goals
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ : Set α
hA : A✝ ⊆ B✝
hB✝ : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
hD_encard : D.encard = c + 1
A' : Set α := A ∪ D
hD_subset_B : D ⊆ B
hA'_subset_B : A' ⊆ B
⊢ M.Indep A'
Tactic:
exact M.indep_subset hA_indep hA'_subset_B
Proof state after:
no goals
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ : Set α
hA : A✝ ⊆ B✝
hB✝ : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
hD_encard : D.encard = c + 1
A' : Set α := A ∪ D
hD_subset_B : D ⊆ B
hA'_subset_B : A' ⊆ B
hA'_indep : M.Indep A'
⊢ (A' \ A).encard = ↑(ENat.toNat c + 1)
Tactic:
have : A ∩ D ⊆ ∅ := by
  have : Disjoint A (B \ A) := Set.disjoint_sdiff_right
  have : Disjoint A D := by exact Set.disjoint_of_subset (fun ⦃a⦄ a ↦ a) hD_subset this
  exact Set.disjoint_iff.mp this
Proof state after:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ : Set α
hA : A✝ ⊆ B✝
hB✝ : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
hD_encard : D.encard = c + 1
A' : Set α := A ∪ D
hD_subset_B : D ⊆ B
hA'_subset_B : A' ⊆ B
hA'_indep : M.Indep A'
this : A ∩ D ⊆ ∅
⊢ (A' \ A).encard = ↑(ENat.toNat c + 1)
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ : Set α
hA : A✝ ⊆ B✝
hB✝ : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
hD_encard : D.encard = c + 1
A' : Set α := A ∪ D
hD_subset_B : D ⊆ B
hA'_subset_B : A' ⊆ B
hA'_indep : M.Indep A'
this : A ∩ D ⊆ ∅
⊢ (A' \ A).encard = ↑(ENat.toNat c + 1)
Tactic:
rw [Set.union_diff_cancel_left this, hD_encard, hcc]
Proof state after:
no goals
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ : Set α
hA : A✝ ⊆ B✝
hB✝ : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
hD_encard : D.encard = c + 1
A' : Set α := A ∪ D
hD_subset_B : D ⊆ B
hA'_subset_B : A' ⊆ B
hA'_indep : M.Indep A'
⊢ A ∩ D ⊆ ∅
Tactic:
have : Disjoint A (B \ A) := Set.disjoint_sdiff_right
Proof state after:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ : Set α
hA : A✝ ⊆ B✝
hB✝ : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
hD_encard : D.encard = c + 1
A' : Set α := A ∪ D
hD_subset_B : D ⊆ B
hA'_subset_B : A' ⊆ B
hA'_indep : M.Indep A'
this : Disjoint A (B \ A)
⊢ A ∩ D ⊆ ∅
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ : Set α
hA : A✝ ⊆ B✝
hB✝ : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
hD_encard : D.encard = c + 1
A' : Set α := A ∪ D
hD_subset_B : D ⊆ B
hA'_subset_B : A' ⊆ B
hA'_indep : M.Indep A'
this : Disjoint A (B \ A)
⊢ A ∩ D ⊆ ∅
Tactic:
have : Disjoint A D := by exact Set.disjoint_of_subset (fun ⦃a⦄ a ↦ a) hD_subset this
Proof state after:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ : Set α
hA : A✝ ⊆ B✝
hB✝ : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
hD_encard : D.encard = c + 1
A' : Set α := A ∪ D
hD_subset_B : D ⊆ B
hA'_subset_B : A' ⊆ B
hA'_indep : M.Indep A'
this✝ : Disjoint A (B \ A)
this : Disjoint A D
⊢ A ∩ D ⊆ ∅
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ : Set α
hA : A✝ ⊆ B✝
hB✝ : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
hD_encard : D.encard = c + 1
A' : Set α := A ∪ D
hD_subset_B : D ⊆ B
hA'_subset_B : A' ⊆ B
hA'_indep : M.Indep A'
this✝ : Disjoint A (B \ A)
this : Disjoint A D
⊢ A ∩ D ⊆ ∅
Tactic:
exact Set.disjoint_iff.mp this
Proof state after:
no goals
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ : Set α
hA : A✝ ⊆ B✝
hB✝ : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
hD_encard : D.encard = c + 1
A' : Set α := A ∪ D
hD_subset_B : D ⊆ B
hA'_subset_B : A' ⊆ B
hA'_indep : M.Indep A'
this : Disjoint A (B \ A)
⊢ Disjoint A D
Tactic:
exact Set.disjoint_of_subset (fun ⦃a⦄ a ↦ a) hD_subset this
Proof state after:
no goals