Theorem: Matroid.Iso.on_basis (Matroid/Old/_Equiv.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hI : M.Basis I X
⊢ N.Basis (↑e.toPartialEquiv '' I) (↑e.toPartialEquiv '' X)
Tactic:
rw [← base_restrict_iff _, (e.restrict X).symm.on_base_iff _, base_restrict_iff]
State after:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hI : M.Basis I X
⊢ M.Basis (↑(e.restrict X ⋯).symm.toPartialEquiv '' (↑e.toPartialEquiv '' I)) X

α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hI : M.Basis I X
⊢ ↑e.toPartialEquiv '' I ⊆ (N ↾ ↑e.toPartialEquiv '' X).E

α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hI : M.Basis I X
⊢ ↑e.toPartialEquiv '' X ⊆ N.E

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hI : M.Basis I X
⊢ ↑e.toPartialEquiv '' X ⊆ N.E
Tactic:
exact e.image_subset_ground X hI.subset_ground
State after:
no goals

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hI : M.Basis I X
⊢ M.Basis (↑(e.restrict X ⋯).symm.toPartialEquiv '' (↑e.toPartialEquiv '' I)) X
Tactic:
convert hI
State after:
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hI : M.Basis I X
⊢ ↑(e.restrict X ⋯).symm.toPartialEquiv '' (↑e.toPartialEquiv '' I) = I

State before:
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hI : M.Basis I X
⊢ ↑(e.restrict X ⋯).symm.toPartialEquiv '' (↑e.toPartialEquiv '' I) = I
Tactic:
simp only [symm_apply, restrict_apply, restr_coe_symm]
State after:
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hI : M.Basis I X
⊢ (fun a => ↑e.toPartialEquiv.symm a) '' (↑e.toPartialEquiv '' I) = I

State before:
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hI : M.Basis I X
⊢ (fun a => ↑e.toPartialEquiv.symm a) '' (↑e.toPartialEquiv '' I) = I
Tactic:
apply e.toPartialEquiv.symm_image_image_of_subset_source
State after:
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hI : M.Basis I X
⊢ I ⊆ e.toPartialEquiv.source

State before:
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hI : M.Basis I X
⊢ I ⊆ e.toPartialEquiv.source
Tactic:
rw [e.source_eq]
State after:
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hI : M.Basis I X
⊢ I ⊆ M.E

State before:
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hI : M.Basis I X
⊢ I ⊆ M.E
Tactic:
exact hI.indep.subset_ground
State after:
no goals

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hI : M.Basis I X
⊢ ↑e.toPartialEquiv '' I ⊆ (N ↾ ↑e.toPartialEquiv '' X).E
Tactic:
simp only [restrict_ground_eq]
State after:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hI : M.Basis I X
⊢ ↑e.toPartialEquiv '' I ⊆ ↑e.toPartialEquiv '' X

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
e : M.Iso N
hI : M.Basis I X
⊢ ↑e.toPartialEquiv '' I ⊆ ↑e.toPartialEquiv '' X
Tactic:
exact image_subset _ hI.subset
State after:
no goals