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

State before:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
⊢ M.Indep (Set.insert x I) ↔ M.relRank I (Set.insert x I) > 0
Tactic:
refine ⟨fun hIx_indep ↦ ?_, fun hr ↦ ?_⟩
State after:
case refine_1
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hIx_indep : M.Indep (Set.insert x I)
⊢ M.relRank I (Set.insert x I) > 0

case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hr : M.relRank I (Set.insert x I) > 0
⊢ M.Indep (Set.insert x I)

State before:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hr : M.relRank I (Set.insert x I) > 0
⊢ M.Indep (Set.insert x I)
Tactic:
refine M.indep_iff'.mpr ?_
State after:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hr : M.relRank I (Set.insert x I) > 0
⊢ Set.insert x I ⊆ M.E ∧ ∀ x_1 ∈ Set.insert x I, M.relRank (Set.insert x I \ {x_1}) (Set.insert x I) > 0

State before:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hr : M.relRank I (Set.insert x I) > 0
⊢ Set.insert x I ⊆ M.E ∧ ∀ x_1 ∈ Set.insert x I, M.relRank (Set.insert x I \ {x_1}) (Set.insert x I) > 0
Tactic:
refine ⟨Set.insert_subset (Set.mem_of_mem_diff hx) hI_indep.subset_ground, ?_⟩
State after:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hr : M.relRank I (Set.insert x I) > 0
⊢ ∀ x_1 ∈ Set.insert x I, M.relRank (Set.insert x I \ {x_1}) (Set.insert x I) > 0

State before:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hr : M.relRank I (Set.insert x I) > 0
⊢ ∀ x_1 ∈ Set.insert x I, M.relRank (Set.insert x I \ {x_1}) (Set.insert x I) > 0
Tactic:
contrapose! hr
State after:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hr : ∃ x_1 ∈ Set.insert x I, M.relRank (Set.insert x I \ {x_1}) (Set.insert x I) ≤ 0
⊢ M.relRank I (Set.insert x I) ≤ 0

State before:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hr : ∃ x_1 ∈ Set.insert x I, M.relRank (Set.insert x I \ {x_1}) (Set.insert x I) ≤ 0
⊢ M.relRank I (Set.insert x I) ≤ 0
Tactic:
rcases hr with ⟨y, hy, hr⟩
State after:
case refine_2.intro.intro
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert x I \ {y}) (Set.insert x I) ≤ 0
⊢ M.relRank I (Set.insert x I) ≤ 0

State before:
case refine_2.intro.intro
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert x I \ {y}) (Set.insert x I) ≤ 0
⊢ M.relRank I (Set.insert x I) ≤ 0
Tactic:
by_cases hxy : x = y
State after:
case pos
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert x I \ {y}) (Set.insert x I) ≤ 0
hxy : x = y
⊢ M.relRank I (Set.insert x I) ≤ 0

case neg
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert x I \ {y}) (Set.insert x I) ≤ 0
hxy : ¬x = y
⊢ M.relRank I (Set.insert x I) ≤ 0

State before:
case neg
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert x I \ {y}) (Set.insert x I) ≤ 0
hxy : ¬x = y
h : M.relRank (I \ {y}) (Set.insert x I) ≤ 1
⊢ M.relRank I (Set.insert x I) ≤ 0
Tactic:
set C := (Set.insert x I)
State after:
case neg
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
h : M.relRank (I \ {y}) C ≤ 1
⊢ M.relRank I C ≤ 0

State before:
case neg
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
h : M.relRank (I \ {y}) C ≤ 1
⊢ M.relRank I C ≤ 0
Tactic:
set B := (I)
State after:
case neg
α : Type u_1
A B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
h : M.relRank (B \ {y}) C ≤ 1
⊢ M.relRank B C ≤ 0

State before:
case neg
α : Type u_1
A B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
h : M.relRank (B \ {y}) C ≤ 1
⊢ M.relRank B C ≤ 0
Tactic:
set A := (I \ {y})
State after:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
⊢ M.relRank B C ≤ 0

State before:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
⊢ M.relRank B C ≤ 0
Tactic:
have h' : M.relRank A C = M.relRank A B + M.relRank B C := by
  have h₂ : B ⊆ C := Set.subset_insert x I
  have h₃ : A ⊆ B := Set.diff_subset
  exact M.relRank_add_cancel h₃ h₂
State after:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h' : M.relRank A C = M.relRank A B + M.relRank B C
⊢ M.relRank B C ≤ 0

State before:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
⊢ M.relRank B C ≤ 0
Tactic:
contrapose! h
State after:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h : 0 < M.relRank B C
⊢ 1 < M.relRank A C

State before:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h : 0 < M.relRank B C
⊢ 1 < M.relRank A C
Tactic:
rw [h']
State after:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h : 0 < M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C

State before:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h : 0 < M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C
Tactic:
have h := ENat.add_one_le_of_lt h
State after:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 0 + 1 ≤ M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C

State before:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 0 + 1 ≤ M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C
Tactic:
simp only [zero_add] at h
State after:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 1 ≤ M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C

State before:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 1 ≤ M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C
Tactic:
have := add_le_add h'' h
State after:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 1 ≤ M.relRank B C
this : 1 + 1 ≤ M.relRank A B + M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C

State before:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 1 ≤ M.relRank B C
this : 1 + 1 ≤ M.relRank A B + M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C
Tactic:
rw [one_add_one_eq_two] at this
State after:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 1 ≤ M.relRank B C
this : 2 ≤ M.relRank A B + M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C

State before:
case neg
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 1 ≤ M.relRank B C
this : 2 ≤ M.relRank A B + M.relRank B C
⊢ 1 < M.relRank A B + M.relRank B C
Tactic:
refine (ENat.add_one_le_iff ?refine_2.intro.intro.hm).mp this
State after:
case refine_2.intro.intro.hm
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 1 ≤ M.relRank B C
this : 2 ≤ M.relRank A B + M.relRank B C
⊢ 1 ≠ ⊤

State before:
case refine_2.intro.intro.hm
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h' : M.relRank A C = M.relRank A B + M.relRank B C
h'' : M.relRank A B ≥ 1
h✝ : 0 < M.relRank B C
h : 1 ≤ M.relRank B C
this : 2 ≤ M.relRank A B + M.relRank B C
⊢ 1 ≠ ⊤
Tactic:
exact ENat.coe_toNat_eq_self.mp rfl
State after:
no goals

State before:
case refine_1
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hIx_indep : M.Indep (Set.insert x I)
⊢ M.relRank I (Set.insert x I) > 0
Tactic:
have h := hIx_indep.indep x (Set.mem_insert x I)
State after:
case refine_1
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hIx_indep : M.Indep (Set.insert x I)
h : M.relRank (Set.insert x I \ {x}) (Set.insert x I) > 0
⊢ M.relRank I (Set.insert x I) > 0

State before:
case refine_1
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hIx_indep : M.Indep (Set.insert x I)
h : M.relRank (Set.insert x I \ {x}) (Set.insert x I) > 0
⊢ M.relRank I (Set.insert x I) > 0
Tactic:
have : Set.insert x I \ {x} = I :=
  Set.insert_diff_self_of_not_mem (Set.not_mem_of_mem_diff hx)
State after:
case refine_1
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hIx_indep : M.Indep (Set.insert x I)
h : M.relRank (Set.insert x I \ {x}) (Set.insert x I) > 0
this : Set.insert x I \ {x} = I
⊢ M.relRank I (Set.insert x I) > 0

State before:
case refine_1
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
hIx_indep : M.Indep (Set.insert x I)
h : M.relRank (Set.insert x I \ {x}) (Set.insert x I) > 0
this : Set.insert x I \ {x} = I
⊢ M.relRank I (Set.insert x I) > 0
Tactic:
rwa [this] at h
State after:
no goals

State before:
case pos
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert x I \ {y}) (Set.insert x I) ≤ 0
hxy : x = y
⊢ M.relRank I (Set.insert x I) ≤ 0
Tactic:
rw [hxy] at hr hx ⊢
State after:
case pos
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
y : α
hx : y ∈ M.E \ I
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert y I \ {y}) (Set.insert y I) ≤ 0
hxy : x = y
⊢ M.relRank I (Set.insert y I) ≤ 0

State before:
case pos
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
y : α
hx : y ∈ M.E \ I
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert y I \ {y}) (Set.insert y I) ≤ 0
hxy : x = y
⊢ M.relRank I (Set.insert y I) ≤ 0
Tactic:
have := Set.not_mem_of_mem_diff hx
State after:
case pos
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
y : α
hx : y ∈ M.E \ I
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert y I \ {y}) (Set.insert y I) ≤ 0
hxy : x = y
this : y ∉ I
⊢ M.relRank I (Set.insert y I) ≤ 0

State before:
case pos
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
y : α
hx : y ∈ M.E \ I
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert y I \ {y}) (Set.insert y I) ≤ 0
hxy : x = y
this : y ∉ I
⊢ M.relRank I (Set.insert y I) ≤ 0
Tactic:
have : Set.insert y I \ {y} = I := Set.insert_diff_self_of_not_mem this
State after:
case pos
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
y : α
hx : y ∈ M.E \ I
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert y I \ {y}) (Set.insert y I) ≤ 0
hxy : x = y
this✝ : y ∉ I
this : Set.insert y I \ {y} = I
⊢ M.relRank I (Set.insert y I) ≤ 0

State before:
case pos
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
y : α
hx : y ∈ M.E \ I
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert y I \ {y}) (Set.insert y I) ≤ 0
hxy : x = y
this✝ : y ∉ I
this : Set.insert y I \ {y} = I
⊢ M.relRank I (Set.insert y I) ≤ 0
Tactic:
rwa [this] at hr
State after:
no goals

State before:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert x I \ {y}) (Set.insert x I) ≤ 0
hxy : ¬x = y
⊢ M.relRank (I \ {y}) (Set.insert x I) ≤ 1
Tactic:
set C := (Set.insert x I)
State after:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
⊢ M.relRank (I \ {y}) C ≤ 1

State before:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
⊢ M.relRank (I \ {y}) C ≤ 1
Tactic:
set B := (Set.insert x I \ {y})
State after:
α : Type u_1
A B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
⊢ M.relRank (I \ {y}) C ≤ 1

State before:
α : Type u_1
A B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
⊢ M.relRank (I \ {y}) C ≤ 1
Tactic:
set A := (I \ {y})
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
⊢ M.relRank A C ≤ 1

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
⊢ M.relRank A C ≤ 1
Tactic:
have h₂ : B ⊆ C := @Set.diff_subset α (insert x I) {y}
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
⊢ M.relRank A C ≤ 1

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
⊢ M.relRank A C ≤ 1
Tactic:
have h₃ : A ⊆ B := by
  refine Set.diff_singleton_subset_iff.mpr ?_
  rw [Set.insert_diff_singleton]
  exact (Set.subset_insert x I).trans (Set.subset_insert y (Set.insert x I))
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
⊢ M.relRank A C ≤ 1

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
hrAB : M.relRank A B ≤ 1
⊢ M.relRank A C ≤ 1
Tactic:
have h : M.relRank A B + M.relRank B C <= 1 := by
  exact add_le_add hrAB hr
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
hrAB : M.relRank A B ≤ 1
h : M.relRank A B + M.relRank B C ≤ 1
⊢ M.relRank A C ≤ 1

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
hrAB : M.relRank A B ≤ 1
h : M.relRank A B + M.relRank B C ≤ 1
⊢ M.relRank A C ≤ 1
Tactic:
have := M.relRank_add_cancel h₃ h₂
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
hrAB : M.relRank A B ≤ 1
h : M.relRank A B + M.relRank B C ≤ 1
this : M.relRank A C = M.relRank A B + M.relRank B C
⊢ M.relRank A C ≤ 1

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
hrAB : M.relRank A B ≤ 1
h : M.relRank A B + M.relRank B C ≤ 1
this : M.relRank A C = M.relRank A B + M.relRank B C
⊢ M.relRank A C ≤ 1
Tactic:
rwa [<-this] at h
State after:
no goals

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
⊢ A ⊆ B
Tactic:
refine Set.diff_singleton_subset_iff.mpr ?_
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
⊢ I ⊆ insert y B

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
⊢ I ⊆ insert y B
Tactic:
rw [Set.insert_diff_singleton]
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
⊢ I ⊆ insert y (Set.insert x I)

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
⊢ I ⊆ insert y (Set.insert x I)
Tactic:
exact (Set.subset_insert x I).trans (Set.subset_insert y (Set.insert x I))
State after:
no goals

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
⊢ M.relRank A B ≤ 1
Tactic:
have h := M.relRank_le_encard_diff A B
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h : M.relRank A B ≤ (B \ A).encard
⊢ M.relRank A B ≤ 1

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h : M.relRank A B ≤ (B \ A).encard
⊢ M.relRank A B ≤ 1
Tactic:
rw [Set.diff_diff_right] at h
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
⊢ M.relRank A B ≤ 1

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
⊢ M.relRank A B ≤ 1
Tactic:
have h := h.trans (Set.encard_union_le (B \ I) (B ∩ {y}))
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard + (B ∩ {y}).encard
⊢ M.relRank A B ≤ 1

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard + (B ∩ {y}).encard
⊢ M.relRank A B ≤ 1
Tactic:
rw [Set.encard_eq_zero.mpr Set.diff_inter_self] at h
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard + 0
⊢ M.relRank A B ≤ 1

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard + 0
⊢ M.relRank A B ≤ 1
Tactic:
simp only [add_zero] at h
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
⊢ M.relRank A B ≤ 1

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
⊢ M.relRank A B ≤ 1
Tactic:
have : B \ I ⊆ {x} := by refine Set.diff_subset_iff.mpr ?_; simp only [Set.union_singleton]; exact h₂
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
this : B \ I ⊆ {x}
⊢ M.relRank A B ≤ 1

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
this : B \ I ⊆ {x}
⊢ M.relRank A B ≤ 1
Tactic:
rcases Set.subset_singleton_iff_eq.mp this with h' | h'
State after:
case inl
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
this : B \ I ⊆ {x}
h' : B \ I = ∅
⊢ M.relRank A B ≤ 1

case inr
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
this : B \ I ⊆ {x}
h' : B \ I = {x}
⊢ M.relRank A B ≤ 1

State before:
case inr
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
this : B \ I ⊆ {x}
h' : B \ I = {x}
⊢ M.relRank A B ≤ 1
Tactic:
rw [h'] at h
State after:
case inr
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ {x}.encard
this : B \ I ⊆ {x}
h' : B \ I = {x}
⊢ M.relRank A B ≤ 1

State before:
case inr
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ {x}.encard
this : B \ I ⊆ {x}
h' : B \ I = {x}
⊢ M.relRank A B ≤ 1
Tactic:
rwa [Set.encard_singleton] at h
State after:
no goals

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
⊢ B \ I ⊆ {x}
Tactic:
refine Set.diff_subset_iff.mpr ?_
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
⊢ B ⊆ I ∪ {x}

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
⊢ B ⊆ I ∪ {x}
Tactic:
simp only [Set.union_singleton]
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
⊢ B ⊆ insert x I

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
⊢ B ⊆ insert x I
Tactic:
exact h₂
State after:
no goals

State before:
case inl
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ (B \ I).encard
this : B \ I ⊆ {x}
h' : B \ I = ∅
⊢ M.relRank A B ≤ 1
Tactic:
rw [h'] at h
State after:
case inl
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ ∅.encard
this : B \ I ⊆ {x}
h' : B \ I = ∅
⊢ M.relRank A B ≤ 1

State before:
case inl
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ ∅.encard
this : B \ I ⊆ {x}
h' : B \ I = ∅
⊢ M.relRank A B ≤ 1
Tactic:
rw [Set.encard_empty] at h
State after:
case inl
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ 0
this : B \ I ⊆ {x}
h' : B \ I = ∅
⊢ M.relRank A B ≤ 1

State before:
case inl
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h✝ : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
h : M.relRank A B ≤ 0
this : B \ I ⊆ {x}
h' : B \ I = ∅
⊢ M.relRank A B ≤ 1
Tactic:
exact h.trans zero_le_one
State after:
no goals

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
hrAB : M.relRank A B ≤ 1
⊢ M.relRank A B + M.relRank B C ≤ 1
Tactic:
exact add_le_add hrAB hr
State after:
no goals

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
⊢ M.relRank A C = M.relRank A B + M.relRank B C
Tactic:
have h₂ : B ⊆ C := Set.subset_insert x I
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h₂ : B ⊆ C
⊢ M.relRank A C = M.relRank A B + M.relRank B C

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h₂ : B ⊆ C
⊢ M.relRank A C = M.relRank A B + M.relRank B C
Tactic:
have h₃ : A ⊆ B := Set.diff_subset
State after:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h₂ : B ⊆ C
h₃ : A ⊆ B
⊢ M.relRank A C = M.relRank A B + M.relRank B C

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h₂ : B ⊆ C
h₃ : A ⊆ B
⊢ M.relRank A C = M.relRank A B + M.relRank B C
Tactic:
exact M.relRank_add_cancel h₃ h₂
State after:
no goals

State before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h' : M.relRank A C = M.relRank A B + M.relRank B C
⊢ M.relRank A B ≥ 1
Tactic:
rcases Set.mem_insert_iff.mp hy with rfl | hy
State after:
case inl
α : Type u_1
A✝ B✝ I J X : Set α
M : RankMatroid α
y : α
B : Set α := I
hI_indep : M.Indep B
A : Set α := I \ {y}
hxy : ¬y = y
C : Set α := Set.insert y I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
hx : y ∈ M.E \ B
h : M.relRank A C ≤ 1
h' : M.relRank A C = M.relRank A B + M.relRank B C
⊢ M.relRank A B ≥ 1

case inr
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy✝ : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h' : M.relRank A C = M.relRank A B + M.relRank B C
hy : y ∈ I
⊢ M.relRank A B ≥ 1

State before:
case inr
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy✝ : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h' : M.relRank A C = M.relRank A B + M.relRank B C
hy : y ∈ I
⊢ M.relRank A B ≥ 1
Tactic:
have := hI_indep.indep y hy
State after:
case inr
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy✝ : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h' : M.relRank A C = M.relRank A B + M.relRank B C
hy : y ∈ I
this : M.relRank (B \ {y}) B > 0
⊢ M.relRank A B ≥ 1

State before:
case inr
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy✝ : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h' : M.relRank A C = M.relRank A B + M.relRank B C
hy : y ∈ I
this : M.relRank (B \ {y}) B > 0
⊢ M.relRank A B ≥ 1
Tactic:
exact ENat.one_le_iff_pos.mpr this
State after:
no goals

State before:
case inl
α : Type u_1
A✝ B✝ I J X : Set α
M : RankMatroid α
y : α
B : Set α := I
hI_indep : M.Indep B
A : Set α := I \ {y}
hxy : ¬y = y
C : Set α := Set.insert y I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
hx : y ∈ M.E \ B
h : M.relRank A C ≤ 1
h' : M.relRank A C = M.relRank A B + M.relRank B C
⊢ M.relRank A B ≥ 1
Tactic:
contradiction
State after:
no goals