Theorem: Matroid.Simple.map (Matroid/Simple.lean)

State before:
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).Simple
Tactic:
simp only [simple_iff_forall_pair_indep, map_ground, mem_image, map_indep_iff,
  forall_exists_index, and_imp]
State after:
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
f : α → β
hf : InjOn f M.E
⊢ ∀ ⦃e f_1 : β⦄, ∀ x ∈ M.E, f x = e → ∀ x ∈ M.E, f x = f_1 → ∃ I₀, M.Indep I₀ ∧ {e, f_1} = f '' I₀

State before:
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
f : α → β
hf : InjOn f M.E
⊢ ∀ ⦃e f_1 : β⦄, ∀ x ∈ M.E, f x = e → ∀ x ∈ M.E, f x = f_1 → ∃ I₀, M.Indep I₀ ∧ {e, f_1} = f '' I₀
Tactic:
rintro _ _ x hx rfl y hy rfl
State after:
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
f : α → β
hf : InjOn f M.E
x : α
hx : x ∈ M.E
y : α
hy : y ∈ M.E
⊢ ∃ I₀, M.Indep I₀ ∧ {f x, f y} = f '' I₀

State before:
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
f : α → β
hf : InjOn f M.E
x : α
hx : x ∈ M.E
y : α
hy : y ∈ M.E
⊢ ∃ I₀, M.Indep I₀ ∧ {f x, f y} = f '' I₀
Tactic:
exact ⟨_, pair_indep hx hy, by simp [image_insert_eq]⟩
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
f : α → β
hf : InjOn f M.E
x : α
hx : x ∈ M.E
y : α
hy : y ∈ M.E
⊢ {f x, f y} = f '' {x, y}
Tactic:
simp [image_insert_eq]
State after:
no goals