internlm/Lean-Github huggingface dataset:
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_1
α : 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 : ℕ∞
⊢ P 0
Tactic:
intro A B _ _ h
Proof state after:
case refine_1
α : 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 : ℕ∞
A B : Set α
a✝¹ : A ⊆ B
a✝ : M.Indep B
h : (B \ A).encard = 0
⊢ M.relRank A B = 0
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_1
α : 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 : ℕ∞
A B : Set α
a✝¹ : A ⊆ B
a✝ : M.Indep B
h : (B \ A).encard = 0
⊢ M.relRank A B = 0
Tactic:
have := M.relRank_le_encard_diff A B
Proof state after:
case refine_1
α : 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 : ℕ∞
A B : Set α
a✝¹ : A ⊆ B
a✝ : M.Indep B
h : (B \ A).encard = 0
this : M.relRank A B ≤ (B \ A).encard
⊢ M.relRank A B = 0
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_1
α : 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 : ℕ∞
A B : Set α
a✝¹ : A ⊆ B
a✝ : M.Indep B
h : (B \ A).encard = 0
this : M.relRank A B ≤ (B \ A).encard
⊢ M.relRank A B = 0
Tactic:
rw [h] at this
Proof state after:
case refine_1
α : 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 : ℕ∞
A B : Set α
a✝¹ : A ⊆ B
a✝ : M.Indep B
h : (B \ A).encard = 0
this : M.relRank A B ≤ 0
⊢ M.relRank A B = 0
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_1
α : 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 : ℕ∞
A B : Set α
a✝¹ : A ⊆ B
a✝ : M.Indep B
h : (B \ A).encard = 0
this : M.relRank A B ≤ 0
⊢ M.relRank A B = 0
Tactic:
simp only [nonpos_iff_eq_zero] at this
Proof state after:
case refine_1
α : 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 : ℕ∞
A B : Set α
a✝¹ : A ⊆ B
a✝ : M.Indep B
h : (B \ A).encard = 0
this : M.relRank A B = 0
⊢ M.relRank A B = 0
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_1
α : 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 : ℕ∞
A B : Set α
a✝¹ : A ⊆ B
a✝ : M.Indep B
h : (B \ A).encard = 0
this : M.relRank A B = 0
⊢ M.relRank A B = 0
Tactic:
assumption
Proof state after:
no goals
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_2
α : 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 : ℕ), P ↑n → P ↑n.succ
Tactic:
intro n hPn A B hA hB_indep h
Proof state after:
case refine_2
α : 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
⊢ M.relRank A B = ↑n.succ
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_2
α : 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
⊢ M.relRank A B = ↑n.succ
Tactic:
have : (n.succ : ℕ∞) > 0 := by exact NeZero.pos (n.succ : ℕ∞)
Proof state after:
case refine_2
α : 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 : ↑n.succ > 0
⊢ M.relRank A B = ↑n.succ
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_2
α : 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 : ↑n.succ > 0
⊢ M.relRank A B = ↑n.succ
Tactic:
rw [<-h] at this
Proof state after:
case refine_2
α : 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
⊢ M.relRank A B = ↑n.succ
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_2
α : 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
⊢ M.relRank A B = ↑n.succ
Tactic:
rcases (Set.encard_pos.mp this) with ⟨x, hx⟩
Proof state after:
case refine_2.intro
α : 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
⊢ M.relRank A B = ↑n.succ
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_2.intro
α : 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
⊢ M.relRank A B = ↑n.succ
Tactic:
set B' := B \ {x}
Proof state after:
case refine_2.intro
α : 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}
⊢ M.relRank A B = ↑n.succ
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_2.intro
α : 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}
⊢ M.relRank A B = ↑n.succ
Tactic:
have hxB : x ∈ B := Set.mem_of_mem_diff hx
Proof state after:
case refine_2.intro
α : 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
⊢ M.relRank A B = ↑n.succ
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_2.intro
α : 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
⊢ M.relRank A B = ↑n.succ
Tactic:
have hB'B : B' ⊆ B := by exact Set.diff_subset
Proof state after:
case refine_2.intro
α : 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
⊢ M.relRank A B = ↑n.succ
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_2.intro
α : 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
⊢ M.relRank A B = ↑n.succ
Tactic:
have hAB' : A ⊆ B' := Set.subset_diff_singleton hA (Set.not_mem_of_mem_diff hx)
Proof state after:
case refine_2.intro
α : 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'
⊢ M.relRank A B = ↑n.succ
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_2.intro
α : 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'
⊢ M.relRank A B = ↑n.succ
Tactic:
have hB'_indep : M.Indep B' := M.indep_subset hB_indep hB'B
Proof state after:
case refine_2.intro
α : 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'
⊢ M.relRank A B = ↑n.succ
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_2.intro
α : 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'
⊢ M.relRank A B = ↑n.succ
Tactic:
have hB'dA : B' \ A = (B \ A) \ {x} := by exact Set.diff_diff_comm
Proof state after:
case refine_2.intro
α : 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}
⊢ M.relRank A B = ↑n.succ
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_2.intro
α : 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}
⊢ M.relRank A B = ↑n.succ
Tactic:
have : (B' \ A).encard = n := by
  rw [hB'dA]
  rw [<-Set.encard_diff_singleton_add_one hx] at h
  simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one] at h
  exact WithTop.add_right_cancel (ENat.coe_toNat_eq_self.mp (refl 1)) h
Proof state after:
case refine_2.intro
α : 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
⊢ M.relRank A B = ↑n.succ
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_2.intro
α : 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
⊢ M.relRank A B = ↑n.succ
Tactic:
have hrAB' : M.relRank A B' = n := hPn A B' hAB' hB'_indep this
Proof state after:
case refine_2.intro
α : 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 A B = ↑n.succ
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_2.intro
α : 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 A B = ↑n.succ
Tactic:
have hrB'B : M.relRank B' B = 1 := by
  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
  have hgt : M.relRank B' B > 0 := by exact hB_indep.indep x hxB
  refine le_antisymm_iff.mpr ⟨hle, ENat.one_le_iff_pos.mpr hgt⟩
Proof state after:
case refine_2.intro
α : 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
hrB'B : M.relRank B' B = 1
⊢ M.relRank A B = ↑n.succ
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_2.intro
α : 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
hrB'B : M.relRank B' B = 1
⊢ M.relRank A B = ↑n.succ
Tactic:
rw [M.relRank_add_cancel hAB' hB'B, hrAB', hrB'B]
Proof state after:
case refine_2.intro
α : 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
hrB'B : M.relRank B' B = 1
⊢ ↑n + 1 = ↑n.succ
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_2.intro
α : 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
hrB'B : M.relRank B' B = 1
⊢ ↑n + 1 = ↑n.succ
Tactic:
have h11: (1 : ℕ) = (1 : ℕ∞) := rfl
Proof state after:
case refine_2.intro
α : 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
hrB'B : M.relRank B' B = 1
h11 : ↑1 = 1
⊢ ↑n + 1 = ↑n.succ
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_2.intro
α : 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
hrB'B : M.relRank B' B = 1
h11 : ↑1 = 1
⊢ ↑n + 1 = ↑n.succ
Tactic:
rw [<-h11, <-(ENat.coe_add n 1), Nat.succ_eq_add_one]
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
⊢ ↑n.succ > 0
Tactic:
exact NeZero.pos (n.succ : ℕ∞)
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
⊢ B' ⊆ B
Tactic:
exact Set.diff_subset
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'
⊢ B' \ A = (B \ A) \ {x}
Tactic:
exact Set.diff_diff_comm
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}
⊢ (B' \ A).encard = ↑n
Tactic:
rw [hB'dA]
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}
⊢ ((B \ A) \ {x}).encard = ↑n