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

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
⊢ ∃ f, ∃ (hf : InjOn f M.E), N = M.map f hf
Tactic:
set f : α → β := fun x ↦ if hx : x ∈ M.E then e ⟨x,hx⟩ else Classical.arbitrary (α → β) x
State after:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
⊢ ∃ f, ∃ (hf : InjOn f M.E), N = M.map f hf

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
⊢ ∃ f, ∃ (hf : InjOn f M.E), N = M.map f hf
Tactic:
have hf_im' : ∀ X ⊆ M.E, f '' X = e '' (M.E ↓∩ X) := by
  simp [← Subtype.forall_set_subtype, preimage_image_eq _ Subtype.val_injective,
    image_image, show ∀ x : M.E, f x = e x from fun x ↦ by simp [f, x.2]]
State after:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
⊢ ∃ f, ∃ (hf : InjOn f M.E), N = M.map f hf

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
⊢ ∃ f, ∃ (hf : InjOn f M.E), N = M.map f hf
Tactic:
have hf_im : ∀ X : Set M.E, f '' X = e '' X := fun X ↦ by
  rw [hf_im' _ (by simp), preimage_image_eq _ Subtype.val_injective]
State after:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
hf_im : ∀ (X : Set ↑M.E), f '' ↑X = ↑(⇑e '' X)
⊢ ∃ f, ∃ (hf : InjOn f M.E), N = M.map f hf

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
hf_im : ∀ (X : Set ↑M.E), f '' ↑X = ↑(⇑e '' X)
⊢ ∃ f, ∃ (hf : InjOn f M.E), N = M.map f hf
Tactic:
refine ⟨f, fun _ hx _ hy ↦ by simp [f, hx, hy, Subtype.val_inj],
  eq_of_indep_iff_indep_forall ?_ ?_⟩
State after:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
hf_im : ∀ (X : Set ↑M.E), f '' ↑X = ↑(⇑e '' X)
⊢ N.E = (M.map f ⋯).E

case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
hf_im : ∀ (X : Set ↑M.E), f '' ↑X = ↑(⇑e '' X)
⊢ ∀ I ⊆ N.E, N.Indep I ↔ (M.map f ⋯).Indep I

State before:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
hf_im : ∀ (X : Set ↑M.E), f '' ↑X = ↑(⇑e '' X)
⊢ ∀ I ⊆ N.E, N.Indep I ↔ (M.map f ⋯).Indep I
Tactic:
simp_rw [map_indep_iff, ← Subtype.forall_set_subtype]
State after:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
hf_im : ∀ (X : Set ↑M.E), f '' ↑X = ↑(⇑e '' X)
⊢ ∀ (s : Set ↑N.E), N.Indep ↑s ↔ ∃ I₀, M.Indep I₀ ∧ ↑s = f '' I₀

State before:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
hf_im : ∀ (X : Set ↑M.E), f '' ↑X = ↑(⇑e '' X)
⊢ ∀ (s : Set ↑N.E), N.Indep ↑s ↔ ∃ I₀, M.Indep I₀ ∧ ↑s = f '' I₀
Tactic:
refine fun I ↦ ⟨fun hI ↦ ⟨↑(e.symm '' I), ?_⟩, fun ⟨I₀, hI₀, h⟩ ↦ ?_⟩
State after:
case refine_2.refine_1
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
hf_im : ∀ (X : Set ↑M.E), f '' ↑X = ↑(⇑e '' X)
I : Set ↑N.E
hI : N.Indep ↑I
⊢ M.Indep ↑(⇑e.symm '' I) ∧ ↑I = f '' ↑(⇑e.symm '' I)

case refine_2.refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
hf_im : ∀ (X : Set ↑M.E), f '' ↑X = ↑(⇑e '' X)
I : Set ↑N.E
x✝ : ∃ I₀, M.Indep I₀ ∧ ↑I = f '' I₀
I₀ : Set α
hI₀ : M.Indep I₀
h : ↑I = f '' I₀
⊢ N.Indep ↑I

State before:
case refine_2.refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
hf_im : ∀ (X : Set ↑M.E), f '' ↑X = ↑(⇑e '' X)
I : Set ↑N.E
x✝ : ∃ I₀, M.Indep I₀ ∧ ↑I = f '' I₀
I₀ : Set α
hI₀ : M.Indep I₀
h : ↑I = f '' I₀
⊢ N.Indep ↑I
Tactic:
rwa [h, hf_im' _ hI₀.subset_ground, ← e.indep_image_iff,
  Subset.image_val_preimage_val_eq hI₀.subset_ground]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
⊢ ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
Tactic:
simp [← Subtype.forall_set_subtype, preimage_image_eq _ Subtype.val_injective,
  image_image, show ∀ x : M.E, f x = e x from fun x ↦ by simp [f, x.2]]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
x : ↑M.E
⊢ f ↑x = ↑(e x)
Tactic:
simp [f, x.2]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
X : Set ↑M.E
⊢ f '' ↑X = ↑(⇑e '' X)
Tactic:
rw [hf_im' _ (by simp), preimage_image_eq _ Subtype.val_injective]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
X : Set ↑M.E
⊢ ↑X ⊆ M.E
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
hf_im : ∀ (X : Set ↑M.E), f '' ↑X = ↑(⇑e '' X)
x✝¹ : α
hx : x✝¹ ∈ M.E
x✝ : α
hy : x✝ ∈ M.E
⊢ f x✝¹ = f x✝ → x✝¹ = x✝
Tactic:
simp [f, hx, hy, Subtype.val_inj]
State after:
no goals

State before:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
hf_im : ∀ (X : Set ↑M.E), f '' ↑X = ↑(⇑e '' X)
⊢ N.E = (M.map f ⋯).E
Tactic:
simp [map_ground, hf_im' _ Subset.rfl]
State after:
no goals

State before:
case refine_2.refine_1
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
hf_im : ∀ (X : Set ↑M.E), f '' ↑X = ↑(⇑e '' X)
I : Set ↑N.E
hI : N.Indep ↑I
⊢ M.Indep ↑(⇑e.symm '' I) ∧ ↑I = f '' ↑(⇑e.symm '' I)
Tactic:
rw [hf_im, image_symm_image, and_iff_left rfl]
State after:
case refine_2.refine_1
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
hf_im : ∀ (X : Set ↑M.E), f '' ↑X = ↑(⇑e '' X)
I : Set ↑N.E
hI : N.Indep ↑I
⊢ M.Indep ↑(⇑e.symm '' I)

State before:
case refine_2.refine_1
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
hf_im : ∀ (X : Set ↑M.E), f '' ↑X = ↑(⇑e '' X)
I : Set ↑N.E
hI : N.Indep ↑I
⊢ M.Indep ↑(⇑e.symm '' I)
Tactic:
rwa [← e.symm.indep_image_iff]
State after:
no goals