Theorem: Matroid.indep_iff_range_indep_of_paraMap (Matroid/Parallel.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
⊢ M.Indep I ↔ M.Indep (range φ)
Tactic:
set ψ := Equiv.ofInjective _ hφ
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep I ↔ M.Indep (range φ)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep I ↔ M.Indep (range φ)
Tactic:
convert Iso.indep_image_iff (I := univ) <|
  (isoOfMapParallelRestr ψ (by simpa only [Equiv.ofInjective_apply, ψ] using h_para)) using 1
State after:
case h.e'_1.a
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep I ↔ (M ↾ I).Indep ↑univ

case h.e'_2.a
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep (range φ) ↔ (M ↾ range φ).Indep ↑(⇑(isoOfMapParallelRestr ψ ⋯) '' univ)

State before:
case h.e'_2.a
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep (range φ) ↔ (M ↾ range φ).Indep ↑(⇑(isoOfMapParallelRestr ψ ⋯) '' univ)
Tactic:
simp only [restrict_ground_eq, image_univ, restrict_indep_iff, image_subset_iff,
  Subtype.coe_preimage_self, subset_univ, and_true]
State after:
case h.e'_2.a
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep (range φ) ↔ M.Indep ((fun a => ↑a) '' range fun a => (isoOfMapParallelRestr ψ ⋯) a)

State before:
case h.e'_2.a
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep (range φ) ↔ M.Indep ((fun a => ↑a) '' range fun a => (isoOfMapParallelRestr ψ ⋯) a)
Tactic:
simp_rw [← image_univ, image_image, image_univ]
State after:
case h.e'_2.a
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep (range φ) ↔ M.Indep (range fun x => ↑((isoOfMapParallelRestr ψ ⋯) x))

State before:
case h.e'_2.a
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep (range φ) ↔ M.Indep (range fun x => ↑((isoOfMapParallelRestr ψ ⋯) x))
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ ∀ (e : ↑I), ?m.371381.Parallel' ↑e ↑(ψ e)
Tactic:
simpa only [Equiv.ofInjective_apply, ψ] using h_para
State after:
no goals

State before:
case h.e'_1.a
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ✝ φ : ↑I → α
hφ : Function.Injective φ
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
ψ : ↑I ≃ ↑(range φ) := Equiv.ofInjective φ hφ
⊢ M.Indep I ↔ (M ↾ I).Indep ↑univ
Tactic:
simp [Subset.rfl]
State after:
no goals