Theorem: Matroid.parallelExtend_parallel (Matroid/Constructions/ParallelExtension.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
⊢ (M.parallelExtend e f).Parallel e f
Tactic:
have he' : (M.parallelExtend e f).Nonloop e := by
  rw [parallelExtend_nonloop_iff he]; left; assumption
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
⊢ (M.parallelExtend e f).Parallel e f

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
⊢ (M.parallelExtend e f).Parallel e f
Tactic:
have hf : (M.parallelExtend e f).Nonloop f := by
  rw [parallelExtend_nonloop_iff he]; right; rfl
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
⊢ (M.parallelExtend e f).Parallel e f

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
⊢ (M.parallelExtend e f).Parallel e f
Tactic:
obtain (rfl | hef) := eq_or_ne e f
State after:
case inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
he' hf : (M.parallelExtend e e).Nonloop e
⊢ (M.parallelExtend e e).Parallel e e

case inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
hef : e ≠ f
⊢ (M.parallelExtend e f).Parallel e f

State before:
case inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
hef : e ≠ f
⊢ (M.parallelExtend e f).Parallel e f
Tactic:
rw [he'.parallel_iff_dep hf hef, Dep, pair_subset_iff, and_iff_right he'.mem_ground,
  and_iff_left hf.mem_ground, parallelExtend, restrict_indep_iff, comap_indep_iff,
  image_update, image_id, image_id,
  if_pos (mem_insert_of_mem _ (show f ∈ ({f} : Set α) from rfl))]
State after:
case inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
hef : e ≠ f
⊢ ¬((M.Indep (insert e ({e, f} \ {f})) ∧ InjOn (update id f e) {e, f}) ∧ {e, f} ⊆ insert f M.E)

State before:
case inr
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
hef : e ≠ f
⊢ ¬((M.Indep (insert e ({e, f} \ {f})) ∧ InjOn (update id f e) {e, f}) ∧ {e, f} ⊆ insert f M.E)
Tactic:
exact fun hcon ↦ hef <| hcon.1.2 (by simp) (by simp) (by simp [update_noteq hef e id])
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
⊢ (M.parallelExtend e f).Nonloop e
Tactic:
rw [parallelExtend_nonloop_iff he]
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
⊢ M.Nonloop e ∨ e = f

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
⊢ M.Nonloop e ∨ e = f
Tactic:
left
State after:
case h
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
⊢ M.Nonloop e

State before:
case h
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
⊢ M.Nonloop e
Tactic:
assumption
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
⊢ (M.parallelExtend e f).Nonloop f
Tactic:
rw [parallelExtend_nonloop_iff he]
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
⊢ M.Nonloop f ∨ f = f

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
⊢ M.Nonloop f ∨ f = f
Tactic:
right
State after:
case h
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
⊢ f = f

State before:
case h
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
⊢ f = f
Tactic:
rfl
State after:
no goals

State before:
case inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
he' hf : (M.parallelExtend e e).Nonloop e
⊢ (M.parallelExtend e e).Parallel e e
Tactic:
rwa [parallel_self_iff]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
hef : e ≠ f
hcon : (M.Indep (insert e ({e, f} \ {f})) ∧ InjOn (update id f e) {e, f}) ∧ {e, f} ⊆ insert f M.E
⊢ e ∈ {e, f}
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
hef : e ≠ f
hcon : (M.Indep (insert e ({e, f} \ {f})) ∧ InjOn (update id f e) {e, f}) ∧ {e, f} ⊆ insert f M.E
⊢ f ∈ {e, f}
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
hf : (M.parallelExtend e f).Nonloop f
hef : e ≠ f
hcon : (M.Indep (insert e ({e, f} \ {f})) ∧ InjOn (update id f e) {e, f}) ∧ {e, f} ⊆ insert f M.E
⊢ update id f e e = update id f e f
Tactic:
simp [update_noteq hef e id]
State after:
no goals