Theorem: Matroid.Iso.base_image (Matroid/Equiv.lean)

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
hB : M.Base ↑B
⊢ N.Base ↑(⇑e '' B)
Tactic:
rw [base_iff_maximal_indep, ← e.indep_image_iff, and_iff_right hB.indep]
State after:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
hB : M.Base ↑B
⊢ ∀ (I : Set β), N.Indep I → ↑(⇑e '' B) ⊆ I → ↑(⇑e '' B) = I

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
hB : M.Base ↑B
⊢ ∀ (I : Set β), N.Indep I → ↑(⇑e '' B) ⊆ I → ↑(⇑e '' B) = I
Tactic:
intro I hI h'
State after:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
hB : M.Base ↑B
I : Set β
hI : N.Indep I
h' : ↑(⇑e '' B) ⊆ I
⊢ ↑(⇑e '' B) = I

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
hB : M.Base ↑B
I : Set β
hI : N.Indep I
h' : ↑(⇑e '' B) ⊆ I
⊢ ↑(⇑e '' B) = I
Tactic:
obtain ⟨I, rfl⟩ := Subset.eq_image_val hI.subset_ground
State after:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
hB : M.Base ↑B
I : Set ↑N.E
hI : N.Indep ↑I
h' : ↑(⇑e '' B) ⊆ ↑I
⊢ ↑(⇑e '' B) = ↑I

State before:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
hB : M.Base ↑B
I : Set ↑N.E
hI : N.Indep ↑I
h' : ↑(⇑e '' B) ⊆ ↑I
⊢ ↑(⇑e '' B) = ↑I
Tactic:
replace hB := hB.eq_of_subset_indep (e.symm.image_indep hI)
State after:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
I : Set ↑N.E
hI : N.Indep ↑I
h' : ↑(⇑e '' B) ⊆ ↑I
hB : ↑B ⊆ ↑(⇑e.symm '' I) → ↑B = ↑(⇑e.symm '' I)
⊢ ↑(⇑e '' B) = ↑I

State before:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
I : Set ↑N.E
hI : N.Indep ↑I
h' : ↑(⇑e '' B) ⊆ ↑I
hB : ↑B ⊆ ↑(⇑e.symm '' I) → ↑B = ↑(⇑e.symm '' I)
⊢ ↑(⇑e '' B) = ↑I
Tactic:
simp only [image_subset_iff, preimage_val_image_val_eq_self, image_val_inj,
  image_symm_eq_preimage] at hB
State after:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
I : Set ↑N.E
hI : N.Indep ↑I
h' : ↑(⇑e '' B) ⊆ ↑I
hB : B ⊆ ⇑e ⁻¹' I → B = ⇑e ⁻¹' I
⊢ ↑(⇑e '' B) = ↑I

State before:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
I : Set ↑N.E
hI : N.Indep ↑I
h' : ↑(⇑e '' B) ⊆ ↑I
hB : B ⊆ ⇑e ⁻¹' I → B = ⇑e ⁻¹' I
⊢ ↑(⇑e '' B) = ↑I
Tactic:
simp only [image_subset_iff, preimage_val_image_val_eq_self] at h'
State after:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
I : Set ↑N.E
hI : N.Indep ↑I
hB : B ⊆ ⇑e ⁻¹' I → B = ⇑e ⁻¹' I
h' : B ⊆ ⇑e ⁻¹' I
⊢ ↑(⇑e '' B) = ↑I

State before:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
I : Set ↑N.E
hI : N.Indep ↑I
hB : B ⊆ ⇑e ⁻¹' I → B = ⇑e ⁻¹' I
h' : B ⊆ ⇑e ⁻¹' I
⊢ ↑(⇑e '' B) = ↑I
Tactic:
simp [hB h', image_image]
State after:
no goals