Theorem: Matroid.Simple.of_restrict_contract (Matroid/Simple.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).Simple
h : (M ／ C).Simple
⊢ M.Simple
Tactic:
rw [simple_iff_loopless_eq_of_parallel_forall] at h hC ⊢
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).Loopless ∧ ∀ (e f : α), (M ↾ C).Parallel e f → e = f
h : (M ／ C).Loopless ∧ ∀ (e f : α), (M ／ C).Parallel e f → e = f
⊢ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).Loopless ∧ ∀ (e f : α), (M ↾ C).Parallel e f → e = f
h : (M ／ C).Loopless ∧ ∀ (e f : α), (M ／ C).Parallel e f → e = f
⊢ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
Tactic:
obtain ⟨hl, h⟩ := h
State after:
case intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).Loopless ∧ ∀ (e f : α), (M ↾ C).Parallel e f → e = f
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
⊢ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f

State before:
case intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).Loopless ∧ ∀ (e f : α), (M ↾ C).Parallel e f → e = f
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
⊢ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
Tactic:
obtain ⟨hCl, hC⟩ := hC
State after:
case intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), (M ↾ C).Parallel e f → e = f
⊢ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f

State before:
case intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), (M ↾ C).Parallel e f → e = f
⊢ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
Tactic:
simp only [restrict_parallel_iff, and_imp] at hC
State after:
case intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
⊢ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f

State before:
case intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
⊢ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
Tactic:
refine ⟨(hCl.of_restrict_contract hl), fun e f hef ↦ ?_⟩
State after:
case intro.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
⊢ e = f

State before:
case intro.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
⊢ e = f
Tactic:
by_cases heC : e ∈ C
State after:
case pos
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∈ C
⊢ e = f

case neg
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
⊢ e = f

State before:
case neg
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
⊢ e = f
Tactic:
by_cases hfC : f ∈ C
State after:
case pos
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∈ C
⊢ e = f

case neg
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∉ C
⊢ e = f

State before:
case neg
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∉ C
⊢ e = f
Tactic:
apply h
State after:
case neg.a
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∉ C
⊢ (M ／ C).Parallel e f

State before:
case neg.a
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∉ C
⊢ (M ／ C).Parallel e f
Tactic:
rw [parallel_iff, contract_cl_eq, contract_cl_eq, ← cl_union_cl_left_eq, hef.cl_eq_cl,
  cl_union_cl_left_eq, and_iff_left rfl]
State after:
case neg.a
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∉ C
⊢ (M ／ C).Nonloop e ∧ (M ／ C).Nonloop f

State before:
case neg.a
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∉ C
⊢ (M ／ C).Nonloop e ∧ (M ／ C).Nonloop f
Tactic:
exact ⟨toNonloop ⟨hef.mem_ground_left, heC⟩, toNonloop ⟨hef.mem_ground_right, hfC⟩⟩
State after:
no goals

State before:
case pos
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∈ C
⊢ e = f
Tactic:
by_cases hfC : f ∈ C
State after:
case pos
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∈ C
hfC : f ∈ C
⊢ e = f

case neg
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∈ C
hfC : f ∉ C
⊢ e = f

State before:
case neg
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∈ C
hfC : f ∉ C
⊢ e = f
Tactic:
refine by_contra fun hne ↦ not_loop (M ／ C) f ?_
State after:
case neg
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∈ C
hfC : f ∉ C
hne : ¬e = f
⊢ (M ／ C).Loop f

State before:
case neg
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∈ C
hfC : f ∉ C
hne : ¬e = f
⊢ (M ／ C).Loop f
Tactic:
exact (hef.loop_of_contract hne).minor ⟨hef.mem_ground_right, hfC⟩ (contract_minor_of_mem _ heC)
State after:
no goals

State before:
case pos
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∈ C
hfC : f ∈ C
⊢ e = f
Tactic:
exact hC _ _ hef heC hfC
State after:
no goals

State before:
case pos
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∈ C
⊢ e = f
Tactic:
refine by_contra fun (hne : e ≠ f) ↦ not_loop (M ／ C) e ?_
State after:
case pos
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∈ C
hne : e ≠ f
⊢ (M ／ C).Loop e

State before:
case pos
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∉ C
hfC : f ∈ C
hne : e ≠ f
⊢ (M ／ C).Loop e
Tactic:
exact (hef.symm.loop_of_contract hne.symm).minor ⟨hef.mem_ground_left, heC⟩
  (contract_minor_of_mem _ hfC)
State after:
no goals