Theorem: RankMatroid.relRank_indeps_eq_encard_diff (Matroid/Constructions/RankAxioms.lean)

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
⊢ M.relRank A B = (B \ A).encard
Tactic:
set P := fun n ↦ ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
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
⊢ M.relRank A B = (B \ A).encard

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
h_induc : ∀ (n : ℕ∞), P n
⊢ M.relRank A B = (B \ A).encard
Tactic:
exact h_induc (B \ A).encard A B hA hB rfl
State after:
no goals

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:
intro n
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 : ℕ∞
⊢ P n

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 ?_ ?_ ?_)
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 ⊤

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
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 = ⊤

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
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

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'
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

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⟩
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

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
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

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)
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

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
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

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]
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

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]
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

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
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

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
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

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)
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

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)
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

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
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

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]
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

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]
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

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]
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

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
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

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)
State after:
no goals

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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 : ℕ∞)
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

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
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

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⟩
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

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}
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

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
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

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
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

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)
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

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
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

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
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

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
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

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
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

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⟩
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

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]
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

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
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

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]
State after:
no goals

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 : ℕ∞)
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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⟩
State after:
no goals

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
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

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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)
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

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]
State after:
no goals

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)
State after:
no goals

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)
State after:
no goals

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
State after:
no goals

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
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)

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]
State after:
no goals

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
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 ⊆ ∅

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
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 ⊆ ∅

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
State after:
no goals

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
State after:
no goals

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'
hA'A : (A' \ A).encard = ↑(ENat.toNat c + 1)
⊢ M.relRank A A' = c + 1
Tactic:
rw [hP (ENat.toNat c + 1) A A' (Set.subset_union_left) hA'_indep hA'A, hcc]
State after:
no goals

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'
hA'A : (A' \ A).encard = ↑(ENat.toNat c + 1)
hrAA' : M.relRank A A' = c + 1
⊢ M.relRank A B ≥ c + 1
Tactic:
rw [M.relRank_add_cancel Set.subset_union_left hA'_subset_B, hrAA']
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'
hA'A : (A' \ A).encard = ↑(ENat.toNat c + 1)
hrAA' : M.relRank A A' = c + 1
⊢ c + 1 + M.relRank (A ∪ D) B ≥ c + 1

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'
hA'A : (A' \ A).encard = ↑(ENat.toNat c + 1)
hrAA' : M.relRank A A' = c + 1
⊢ c + 1 + M.relRank (A ∪ D) B ≥ c + 1
Tactic:
simp only [ge_iff_le, self_le_add_right]
State after:
no goals