Theorem: Matroid.IsoRestr.exists_restr_iso (Matroid/Minor/Iso.lean)

State before:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤ir M
I : Set ↑N.E
⊢ N.Indep ↑I ↔ (M ↾ range (val ∘ ⇑i)).Indep ↑(⇑(Equiv.ofInjective (fun y => (val ∘ ⇑i) y) ⋯) '' I)
Tactic:
simp only [← i.indep_image_iff, restrict_ground_eq, comp_apply, Equiv.ofInjective_apply,
  restrict_indep_iff, image_subset_iff, Subtype.coe_preimage_self, subset_univ, and_true]
State after:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤ir M
I : Set ↑N.E
⊢ M.Indep ↑(⇑i '' I) ↔ M.Indep ((fun a => ↑a) '' ((fun a => (Equiv.ofInjective (fun y => ↑(i y)) ⋯) a) '' I))

State before:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤ir M
I : Set ↑N.E
⊢ M.Indep ↑(⇑i '' I) ↔ M.Indep ((fun a => ↑a) '' ((fun a => (Equiv.ofInjective (fun y => ↑(i y)) ⋯) a) '' I))
Tactic:
simp only [image_image]
State after:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤ir M
I : Set ↑N.E
⊢ M.Indep ((fun x => ↑(i x)) '' I) ↔ M.Indep ((fun x => ↑((Equiv.ofInjective (fun y => ↑(i y)) ⋯) x)) '' I)

State before:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤ir M
I : Set ↑N.E
⊢ M.Indep ((fun x => ↑(i x)) '' I) ↔ M.Indep ((fun x => ↑((Equiv.ofInjective (fun y => ↑(i y)) ⋯) x)) '' I)
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤ir M
⊢ range (val ∘ ⇑i) ⊆ M.E
Tactic:
simp [range_comp]
State after:
no goals