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

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
⊢ M.Basis ↑I ↑X ↔ N.Basis ↑(⇑e '' I) ↑(⇑e '' X)
Tactic:
simp only [image_subset_iff, Subtype.coe_preimage_self, subset_univ, basis_iff_mem_maximals,
  mem_maximals_iff, mem_setOf_eq, ← e.indep_image_iff, preimage_val_image_val_eq_self, and_imp,
  preimage_image, and_congr_right_iff]
State after:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
⊢ M.Indep ↑I →
    I ⊆ X →
      ((∀ ⦃y : Set α⦄, M.Indep y → y ⊆ ↑X → I ⊆ Subtype.val ⁻¹' y → ↑I = y) ↔
        ∀ ⦃y : Set β⦄, N.Indep y → y ⊆ ↑(⇑e '' X) → I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' y) → ↑(⇑e '' I) = y)

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
⊢ M.Indep ↑I →
    I ⊆ X →
      ((∀ ⦃y : Set α⦄, M.Indep y → y ⊆ ↑X → I ⊆ Subtype.val ⁻¹' y → ↑I = y) ↔
        ∀ ⦃y : Set β⦄, N.Indep y → y ⊆ ↑(⇑e '' X) → I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' y) → ↑(⇑e '' I) = y)
Tactic:
intro hI hIX
State after:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
⊢ (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ ↑X → I ⊆ Subtype.val ⁻¹' y → ↑I = y) ↔
    ∀ ⦃y : Set β⦄, N.Indep y → y ⊆ ↑(⇑e '' X) → I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' y) → ↑(⇑e '' I) = y

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
⊢ (∀ ⦃y : Set α⦄, M.Indep y → y ⊆ ↑X → I ⊆ Subtype.val ⁻¹' y → ↑I = y) ↔
    ∀ ⦃y : Set β⦄, N.Indep y → y ⊆ ↑(⇑e '' X) → I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' y) → ↑(⇑e '' I) = y
Tactic:
refine ⟨fun h J hJ hJX hIJ ↦ ?_, fun h J hJ hJX hIJ ↦ ?_⟩
State after:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
h : ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ ↑X → I ⊆ Subtype.val ⁻¹' y → ↑I = y
J : Set β
hJ : N.Indep J
hJX : J ⊆ ↑(⇑e '' X)
hIJ : I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' J)
⊢ ↑(⇑e '' I) = J

case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
h : ∀ ⦃y : Set β⦄, N.Indep y → y ⊆ ↑(⇑e '' X) → I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' y) → ↑(⇑e '' I) = y
J : Set α
hJ : M.Indep J
hJX : J ⊆ ↑X
hIJ : I ⊆ Subtype.val ⁻¹' J
⊢ ↑I = J

State before:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
h : ∀ ⦃y : Set β⦄, N.Indep y → y ⊆ ↑(⇑e '' X) → I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' y) → ↑(⇑e '' I) = y
J : Set α
hJ : M.Indep J
hJX : J ⊆ ↑X
hIJ : I ⊆ Subtype.val ⁻¹' J
⊢ ↑I = J
Tactic:
specialize h (y := ↑(e '' (M.E ↓∩ J)))
State after:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set α
hJ : M.Indep J
hJX : J ⊆ ↑X
hIJ : I ⊆ Subtype.val ⁻¹' J
h :
  N.Indep ↑(⇑e '' M.E ↓∩ J) →
    ↑(⇑e '' M.E ↓∩ J) ⊆ ↑(⇑e '' X) → I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' ↑(⇑e '' M.E ↓∩ J)) → ↑(⇑e '' I) = ↑(⇑e '' M.E ↓∩ J)
⊢ ↑I = J

State before:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set α
hJ : M.Indep J
hJX : J ⊆ ↑X
hIJ : I ⊆ Subtype.val ⁻¹' J
h :
  N.Indep ↑(⇑e '' M.E ↓∩ J) →
    ↑(⇑e '' M.E ↓∩ J) ⊆ ↑(⇑e '' X) → I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' ↑(⇑e '' M.E ↓∩ J)) → ↑(⇑e '' I) = ↑(⇑e '' M.E ↓∩ J)
⊢ ↑I = J
Tactic:
simp only [← e.indep_image_iff, Subtype.image_preimage_coe,
  inter_eq_self_of_subset_right hJ.subset_ground, hJ, image_subset_iff,
  preimage_val_image_val_eq_self, preimage_image, image_val_inj, true_implies] at h
State after:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set α
hJ : M.Indep J
hJX : J ⊆ ↑X
hIJ : I ⊆ Subtype.val ⁻¹' J
h : M.E ↓∩ J ⊆ X → I ⊆ M.E ↓∩ J → ⇑e '' I = ⇑e '' M.E ↓∩ J
⊢ ↑I = J

State before:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set α
hJ : M.Indep J
hJX : J ⊆ ↑X
hIJ : I ⊆ Subtype.val ⁻¹' J
h : M.E ↓∩ J ⊆ X → I ⊆ M.E ↓∩ J → ⇑e '' I = ⇑e '' M.E ↓∩ J
⊢ ↑I = J
Tactic:
rw [← image_subset_image_iff Subtype.val_injective] at h
State after:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set α
hJ : M.Indep J
hJX : J ⊆ ↑X
hIJ : I ⊆ Subtype.val ⁻¹' J
h : ↑(M.E ↓∩ J) ⊆ ↑X → I ⊆ M.E ↓∩ J → ⇑e '' I = ⇑e '' M.E ↓∩ J
⊢ ↑I = J

State before:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set α
hJ : M.Indep J
hJX : J ⊆ ↑X
hIJ : I ⊆ Subtype.val ⁻¹' J
h : ↑(M.E ↓∩ J) ⊆ ↑X → I ⊆ M.E ↓∩ J → ⇑e '' I = ⇑e '' M.E ↓∩ J
⊢ ↑I = J
Tactic:
simp only [Subtype.image_preimage_coe, inter_eq_self_of_subset_right hJ.subset_ground] at h
State after:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set α
hJ : M.Indep J
hJX : J ⊆ ↑X
hIJ : I ⊆ Subtype.val ⁻¹' J
h : J ⊆ ↑X → I ⊆ M.E ↓∩ J → ⇑e '' I = ⇑e '' M.E ↓∩ J
⊢ ↑I = J

State before:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set α
hJ : M.Indep J
hJX : J ⊆ ↑X
hIJ : I ⊆ Subtype.val ⁻¹' J
h : J ⊆ ↑X → I ⊆ M.E ↓∩ J → ⇑e '' I = ⇑e '' M.E ↓∩ J
⊢ ↑I = J
Tactic:
specialize h hJX (by convert hIJ)
State after:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set α
hJ : M.Indep J
hJX : J ⊆ ↑X
hIJ : I ⊆ Subtype.val ⁻¹' J
h : ⇑e '' I = ⇑e '' M.E ↓∩ J
⊢ ↑I = J

State before:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set α
hJ : M.Indep J
hJX : J ⊆ ↑X
hIJ : I ⊆ Subtype.val ⁻¹' J
h : ⇑e '' I = ⇑e '' M.E ↓∩ J
⊢ ↑I = J
Tactic:
rw [← e.symm_image_image I, h]
State after:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set α
hJ : M.Indep J
hJX : J ⊆ ↑X
hIJ : I ⊆ Subtype.val ⁻¹' J
h : ⇑e '' I = ⇑e '' M.E ↓∩ J
⊢ ↑(⇑e.symm '' (⇑e '' M.E ↓∩ J)) = J

State before:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set α
hJ : M.Indep J
hJX : J ⊆ ↑X
hIJ : I ⊆ Subtype.val ⁻¹' J
h : ⇑e '' I = ⇑e '' M.E ↓∩ J
⊢ ↑(⇑e.symm '' (⇑e '' M.E ↓∩ J)) = J
Tactic:
simp [hJ.subset_ground]
State after:
no goals

State before:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
h : ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ ↑X → I ⊆ Subtype.val ⁻¹' y → ↑I = y
J : Set β
hJ : N.Indep J
hJX : J ⊆ ↑(⇑e '' X)
hIJ : I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' J)
⊢ ↑(⇑e '' I) = J
Tactic:
specialize h (y := ↑(e.symm '' (N.E ↓∩ J)))
State after:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set β
hJ : N.Indep J
hJX : J ⊆ ↑(⇑e '' X)
hIJ : I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' J)
h :
  M.Indep ↑(⇑e.symm '' N.E ↓∩ J) →
    ↑(⇑e.symm '' N.E ↓∩ J) ⊆ ↑X → I ⊆ Subtype.val ⁻¹' ↑(⇑e.symm '' N.E ↓∩ J) → ↑I = ↑(⇑e.symm '' N.E ↓∩ J)
⊢ ↑(⇑e '' I) = J

State before:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set β
hJ : N.Indep J
hJX : J ⊆ ↑(⇑e '' X)
hIJ : I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' J)
h :
  M.Indep ↑(⇑e.symm '' N.E ↓∩ J) →
    ↑(⇑e.symm '' N.E ↓∩ J) ⊆ ↑X → I ⊆ Subtype.val ⁻¹' ↑(⇑e.symm '' N.E ↓∩ J) → ↑I = ↑(⇑e.symm '' N.E ↓∩ J)
⊢ ↑(⇑e '' I) = J
Tactic:
simp only [image_symm_eq_preimage, e.indep_image_iff, image_preimage,
  Subtype.image_preimage_coe, inter_eq_self_of_subset_right hJ.subset_ground, hJ,
  image_subset_iff, preimage_val_image_val_eq_self, preimage_subset_iff, image_val_inj,
  true_implies] at h
State after:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set β
hJ : N.Indep J
hJX : J ⊆ ↑(⇑e '' X)
hIJ : I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' J)
h : N.E ↓∩ J ⊆ ⇑e '' X → I ⊆ ⇑e ⁻¹' N.E ↓∩ J → I = ⇑e ⁻¹' N.E ↓∩ J
⊢ ↑(⇑e '' I) = J

State before:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set β
hJ : N.Indep J
hJX : J ⊆ ↑(⇑e '' X)
hIJ : I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' J)
h : N.E ↓∩ J ⊆ ⇑e '' X → I ⊆ ⇑e ⁻¹' N.E ↓∩ J → I = ⇑e ⁻¹' N.E ↓∩ J
⊢ ↑(⇑e '' I) = J
Tactic:
specialize h <| by simpa [Set.preimage_val_image_val_eq_self]
  using (show N.E ↓∩ J ⊆ _ from preimage_mono (f := Subtype.val) hJX)
State after:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set β
hJ : N.Indep J
hJX : J ⊆ ↑(⇑e '' X)
hIJ : I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' J)
h : I ⊆ ⇑e ⁻¹' N.E ↓∩ J → I = ⇑e ⁻¹' N.E ↓∩ J
⊢ ↑(⇑e '' I) = J

State before:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set β
hJ : N.Indep J
hJX : J ⊆ ↑(⇑e '' X)
hIJ : I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' J)
h : I ⊆ ⇑e ⁻¹' N.E ↓∩ J → I = ⇑e ⁻¹' N.E ↓∩ J
⊢ ↑(⇑e '' I) = J
Tactic:
obtain rfl := h (by convert hIJ)
State after:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
X : Set ↑M.E
J : Set β
hJ : N.Indep J
hJX : J ⊆ ↑(⇑e '' X)
hI : M.Indep ↑(⇑e ⁻¹' N.E ↓∩ J)
hIX : ⇑e ⁻¹' N.E ↓∩ J ⊆ X
hIJ : ⇑e ⁻¹' N.E ↓∩ J ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' J)
h : ⇑e ⁻¹' N.E ↓∩ J ⊆ ⇑e ⁻¹' N.E ↓∩ J → ⇑e ⁻¹' N.E ↓∩ J = ⇑e ⁻¹' N.E ↓∩ J
⊢ ↑(⇑e '' (⇑e ⁻¹' N.E ↓∩ J)) = J

State before:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
X : Set ↑M.E
J : Set β
hJ : N.Indep J
hJX : J ⊆ ↑(⇑e '' X)
hI : M.Indep ↑(⇑e ⁻¹' N.E ↓∩ J)
hIX : ⇑e ⁻¹' N.E ↓∩ J ⊆ X
hIJ : ⇑e ⁻¹' N.E ↓∩ J ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' J)
h : ⇑e ⁻¹' N.E ↓∩ J ⊆ ⇑e ⁻¹' N.E ↓∩ J → ⇑e ⁻¹' N.E ↓∩ J = ⇑e ⁻¹' N.E ↓∩ J
⊢ ↑(⇑e '' (⇑e ⁻¹' N.E ↓∩ J)) = J
Tactic:
simp [hJ.subset_ground]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set β
hJ : N.Indep J
hJX : J ⊆ ↑(⇑e '' X)
hIJ : I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' J)
h : N.E ↓∩ J ⊆ ⇑e '' X → I ⊆ ⇑e ⁻¹' N.E ↓∩ J → I = ⇑e ⁻¹' N.E ↓∩ J
⊢ N.E ↓∩ J ⊆ ⇑e '' X
Tactic:
simpa [Set.preimage_val_image_val_eq_self]
using (show N.E ↓∩ J ⊆ _ from preimage_mono (f := Subtype.val) hJX)
State after:
no goals

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set β
hJ : N.Indep J
hJX : J ⊆ ↑(⇑e '' X)
hIJ : I ⊆ ⇑e ⁻¹' (Subtype.val ⁻¹' J)
h : I ⊆ ⇑e ⁻¹' N.E ↓∩ J → I = ⇑e ⁻¹' N.E ↓∩ J
⊢ I ⊆ ⇑e ⁻¹' N.E ↓∩ J
Tactic:
convert hIJ
State after:
no goals

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set α
hJ : M.Indep J
hJX : J ⊆ ↑X
hIJ : I ⊆ Subtype.val ⁻¹' J
h : J ⊆ ↑X → I ⊆ M.E ↓∩ J → ⇑e '' I = ⇑e '' M.E ↓∩ J
⊢ I ⊆ M.E ↓∩ J
Tactic:
convert hIJ
State after:
no goals