Theorem: Matroid.comapOn_base_iff_of_bijOn (Matroid/Map.lean)

State before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
⊢ (N.comapOn E f).Base B ↔ N.Base (f '' B) ∧ B ⊆ E
Tactic:
rw [← and_iff_left_of_imp (Base.subset_ground (M := N.comapOn E f) (B := B)),
  comapOn_ground_eq, and_congr_left_iff]
State after:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
⊢ B ⊆ E → ((N.comapOn E f).Base B ↔ N.Base (f '' B))

State before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
⊢ B ⊆ E → ((N.comapOn E f).Base B ↔ N.Base (f '' B))
Tactic:
suffices h' : B ⊆ E → InjOn f B from fun hB ↦
  by simp [hB, comapOn_base_iff_of_surjOn h.surjOn, h']
State after:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
⊢ B ⊆ E → InjOn f B

State before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
⊢ B ⊆ E → InjOn f B
Tactic:
exact fun hBE ↦ h.injOn.mono hBE
State after:
no goals

State before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
h' : B ⊆ E → InjOn f B
hB : B ⊆ E
⊢ (N.comapOn E f).Base B ↔ N.Base (f '' B)
Tactic:
simp [hB, comapOn_base_iff_of_surjOn h.surjOn, h']
State after:
no goals