Theorem: Matroid.Indep.paraMap_injective (Matroid/Parallel.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
φ : ↑I → α
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
⊢ Function.Injective φ
Tactic:
intro x y hxy
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
φ : ↑I → α
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
x y : ↑I
hxy : φ x = φ y
⊢ x = y

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
φ : ↑I → α
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
x y : ↑I
hxy : φ x = φ y
⊢ x = y
Tactic:
have hx := h_para x
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
φ : ↑I → α
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
x y : ↑I
hxy : φ x = φ y
hx : M.Parallel' (↑x) (φ x)
⊢ x = y

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
φ : ↑I → α
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
x y : ↑I
hxy : φ x = φ y
hx : M.Parallel' (↑x) (φ x)
⊢ x = y
Tactic:
rw [hxy] at hx
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
φ : ↑I → α
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
x y : ↑I
hxy : φ x = φ y
hx : M.Parallel' (↑x) (φ y)
⊢ x = y

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
φ : ↑I → α
h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)
x y : ↑I
hxy : φ x = φ y
hx : M.Parallel' (↑x) (φ y)
⊢ x = y
Tactic:
exact Subtype.val_inj.1
  ((hx.trans (h_para y).symm).eq_of_indep (hI.subset (pair_subset x.2 y.2)))
State after:
no goals