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 : ℕ∞
⊢ P n
Tactic:
refine (@ENat.nat_induction P n ?_ ?_ ?_)
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 : ℕ∞
⊢ P 0

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

case refine_3
α : 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 ⊤
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_3
α : 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 ⊤
Tactic:
intro hP A B hB hA_indep h
Proof state after:
case refine_3
α : 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 : (B \ A).encard = ⊤
⊢ M.relRank A B = ⊤
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_3
α : 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 : (B \ A).encard = ⊤
⊢ M.relRank A B = ⊤
Tactic:
by_contra! h_finite
Proof state after:
case refine_3
α : 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 : (B \ A).encard = ⊤
h_finite : M.relRank A B ≠ ⊤
⊢ False
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_3
α : 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 : (B \ A).encard = ⊤
h_finite : M.relRank A B ≠ ⊤
⊢ False
Tactic:
have : ∃ n, M.relRank A B = n := exists_eq'
Proof state after:
case refine_3
α : 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 : (B \ A).encard = ⊤
h_finite : M.relRank A B ≠ ⊤
this : ∃ n, M.relRank A B = n
⊢ False
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_3
α : 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 : (B \ A).encard = ⊤
h_finite : M.relRank A B ≠ ⊤
this : ∃ n, M.relRank A B = n
⊢ False
Tactic:
rcases this with ⟨c, hc⟩
Proof state after:
case refine_3.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 : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
h : (B \ A).encard = ⊤
h_finite : M.relRank A B ≠ ⊤
c : ℕ∞
hc : M.relRank A B = c
⊢ False
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_3.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 : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
h : (B \ A).encard = ⊤
h_finite : M.relRank A B ≠ ⊤
c : ℕ∞
hc : M.relRank A B = c
⊢ False
Tactic:
simp at h
Proof state after:
case refine_3.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 : ℕ∞
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
⊢ False
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_3.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 : ℕ∞
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
⊢ False
Tactic:
obtain ⟨D, hD_subset, hD_finite, hD_ncard⟩ := Set.Infinite.exists_subset_ncard_eq h (ENat.toNat c + 1)
Proof state after:
case refine_3.intro.intro.intro.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 : ℕ∞
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
⊢ False
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_3.intro.intro.intro.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 : ℕ∞
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
⊢ False
Tactic:
have c_finite : c ≠ ⊤ := by rwa [hc] at h_finite
Proof state after:
case refine_3.intro.intro.intro.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 : ℕ∞
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 ≠ ⊤
⊢ False
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_3.intro.intro.intro.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 : ℕ∞
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 ≠ ⊤
⊢ False
Tactic:
have hcc : c + 1 = ↑(ENat.toNat c + 1) := by
  simp only [Nat.cast_add, Nat.cast_one, ENat.coe_toNat_eq_self.mpr c_finite]
Proof state after:
case refine_3.intro.intro.intro.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 : ℕ∞
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)
⊢ False
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_3.intro.intro.intro.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 : ℕ∞
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)
⊢ False
Tactic:
have hD_encard : D.encard = c + 1 := by
  have : D.encard = (D.ncard : ℕ∞) := by exact Eq.symm (Set.Finite.cast_ncard_eq hD_finite)
  rw [this, congrArg (Nat.cast) hD_ncard, hcc]
Proof state after:
case refine_3.intro.intro.intro.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 : ℕ∞
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)
hD_encard : D.encard = c + 1
⊢ False
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_3.intro.intro.intro.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 : ℕ∞
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)
hD_encard : D.encard = c + 1
⊢ False
Tactic:
clear hD_ncard hD_finite h_finite
Proof state after:
case refine_3.intro.intro.intro.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 : ℕ∞
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
⊢ False
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_3.intro.intro.intro.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 : ℕ∞
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
⊢ False
Tactic:
let A' := A ∪ D
Proof state after:
case refine_3.intro.intro.intro.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 : ℕ∞
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
⊢ False
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_3.intro.intro.intro.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 : ℕ∞
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
⊢ False
Tactic:
have hD_subset_B : D ⊆ B := hD_subset.trans (Set.diff_subset)
Proof state after:
case refine_3.intro.intro.intro.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 : ℕ∞
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
⊢ False
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_3.intro.intro.intro.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 : ℕ∞
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
⊢ False
Tactic:
have hA'_subset_B : A' ⊆ B := by exact (Set.union_subset hB hD_subset_B)
Proof state after:
case refine_3.intro.intro.intro.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 : ℕ∞
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
⊢ False
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_3.intro.intro.intro.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 : ℕ∞
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
⊢ False
Tactic:
have hA'_indep : M.Indep A' := by exact M.indep_subset hA_indep hA'_subset_B
Proof state after:
case refine_3.intro.intro.intro.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 : ℕ∞
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'
⊢ False
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_3.intro.intro.intro.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 : ℕ∞
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'
⊢ False
Tactic:
have hA'A : (A' \ A).encard = ↑(ENat.toNat c + 1) := by
  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
  rw [Set.union_diff_cancel_left this, hD_encard, hcc]
Proof state after:
case refine_3.intro.intro.intro.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 : ℕ∞
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'
hA'A : (A' \ A).encard = ↑(ENat.toNat c + 1)
⊢ False
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_3.intro.intro.intro.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 : ℕ∞
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'
hA'A : (A' \ A).encard = ↑(ENat.toNat c + 1)
⊢ False
Tactic:
have hrAA' : M.relRank A A' = c + 1 := by
  rw [hP (ENat.toNat c + 1) A A' (Set.subset_union_left) hA'_indep hA'A, hcc]
Proof state after:
case refine_3.intro.intro.intro.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 : ℕ∞
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'
hA'A : (A' \ A).encard = ↑(ENat.toNat c + 1)
hrAA' : M.relRank A A' = c + 1
⊢ False
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_3.intro.intro.intro.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 : ℕ∞
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'
hA'A : (A' \ A).encard = ↑(ENat.toNat c + 1)
hrAA' : M.relRank A A' = c + 1
⊢ False
Tactic:
have hbad : M.relRank A B ≥ c + 1 := by
  rw [M.relRank_add_cancel Set.subset_union_left hA'_subset_B, hrAA']
  simp only [ge_iff_le, self_le_add_right]
Proof state after:
case refine_3.intro.intro.intro.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 : ℕ∞
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'
hA'A : (A' \ A).encard = ↑(ENat.toNat c + 1)
hrAA' : M.relRank A A' = c + 1
hbad : M.relRank A B ≥ c + 1
⊢ False
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_3.intro.intro.intro.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 : ℕ∞
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'
hA'A : (A' \ A).encard = ↑(ENat.toNat c + 1)
hrAA' : M.relRank A A' = c + 1
hbad : M.relRank A B ≥ c + 1
⊢ False
Tactic:
rw [hc] at hbad
Proof state after:
case refine_3.intro.intro.intro.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 : ℕ∞
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'
hA'A : (A' \ A).encard = ↑(ENat.toNat c + 1)
hrAA' : M.relRank A A' = c + 1
hbad : c ≥ c + 1
⊢ False
Theorem: RankMatroid.relRank_indeps_eq_encard_diff
Proof state before:
case refine_3.intro.intro.intro.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 : ℕ∞
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'
hA'A : (A' \ A).encard = ↑(ENat.toNat c + 1)
hrAA' : M.relRank A A' = c + 1
hbad : c ≥ c + 1
⊢ False
Tactic:
exact (lt_irrefl c) ((ENat.add_one_le_iff c_finite).mp hbad)
Proof state after:
no goals