Theorem: Matroid.extendBy_injective (Matroid/Extension.lean)

State before:
α : Type u_1
M✝ : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
⊢ Injective (M.extendBy e)
Tactic:
refine fun U U' h_eq ↦ SetLike.coe_set_eq.1 (Set.ext fun F ↦ ?_)
State after:
α : Type u_1
M✝ : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
⊢ F ∈ ↑U ↔ F ∈ ↑U'

State before:
α : Type u_1
M✝ : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
⊢ F ∈ ↑U ↔ F ∈ ↑U'
Tactic:
obtain (hF | hF) := em' (M.Flat F)
State after:
case inl
α : Type u_1
M✝ : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
hF : ¬M.Flat F
⊢ F ∈ ↑U ↔ F ∈ ↑U'

case inr
α : Type u_1
M✝ : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
hF : M.Flat F
⊢ F ∈ ↑U ↔ F ∈ ↑U'

State before:
case inr
α : Type u_1
M✝ : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
hF : M.Flat F
⊢ F ∈ ↑U ↔ F ∈ ↑U'
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis F
State after:
case inr.intro
α : Type u_1
M✝ : Matroid α
I✝ J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
hF : M.Flat F
I : Set α
hI : M.Basis I F
⊢ F ∈ ↑U ↔ F ∈ ↑U'

State before:
case inr.intro
α : Type u_1
M✝ : Matroid α
I✝ J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
hF : M.Flat F
I : Set α
hI : M.Basis I F
⊢ F ∈ ↑U ↔ F ∈ ↑U'
Tactic:
have heI : e ∉ I := not_mem_subset hI.indep.subset_ground he
State after:
case inr.intro
α : Type u_1
M✝ : Matroid α
I✝ J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
hF : M.Flat F
I : Set α
hI : M.Basis I F
heI : e ∉ I
⊢ F ∈ ↑U ↔ F ∈ ↑U'

State before:
case inr.intro
α : Type u_1
M✝ : Matroid α
I✝ J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
hF : M.Flat F
I : Set α
hI : M.Basis I F
heI : e ∉ I
⊢ F ∈ ↑U ↔ F ∈ ↑U'
Tactic:
apply_fun (fun M ↦ M.Indep (insert e I)) at h_eq
State after:
case inr.intro
α : Type u_1
M✝ : Matroid α
I✝ J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
F : Set α
hF : M.Flat F
I : Set α
hI : M.Basis I F
heI : e ∉ I
h_eq : (M.extendBy e U).Indep (insert e I) = (M.extendBy e U').Indep (insert e I)
⊢ F ∈ ↑U ↔ F ∈ ↑U'

State before:
case inr.intro
α : Type u_1
M✝ : Matroid α
I✝ J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
F : Set α
hF : M.Flat F
I : Set α
hI : M.Basis I F
heI : e ∉ I
h_eq : (M.extendBy e U).Indep (insert e I) = (M.extendBy e U').Indep (insert e I)
⊢ F ∈ ↑U ↔ F ∈ ↑U'
Tactic:
simpa [extendBy_Indep, ModularCut.extIndep_iff_of_mem (mem_insert e I), heI, hI.indep,
  not_iff_not, ← hF.eq_cl_of_basis hI] using h_eq
State after:
no goals

State before:
case inl
α : Type u_1
M✝ : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
hF : ¬M.Flat F
⊢ F ∈ ↑U ↔ F ∈ ↑U'
Tactic:
exact iff_of_false (hF ∘ U.flat_of_mem) (hF ∘ U'.flat_of_mem)
State after:
no goals