internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Iso.basis_image_iff
Proof 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 ↦ ?_⟩
Proof 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
Theorem: Matroid.Iso.basis_image_iff
Proof 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)))
Proof 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
Theorem: Matroid.Iso.basis_image_iff
Proof 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
Proof 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
Theorem: Matroid.Iso.basis_image_iff
Proof 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
Proof 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
Theorem: Matroid.Iso.basis_image_iff
Proof 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
Proof 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
Theorem: Matroid.Iso.basis_image_iff
Proof 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)
Proof 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
Theorem: Matroid.Iso.basis_image_iff
Proof 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]
Proof 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
Theorem: Matroid.Iso.basis_image_iff
Proof 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]
Proof state after:
no goals
Theorem: Matroid.Iso.basis_image_iff
Proof 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)))
Proof 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
Theorem: Matroid.Iso.basis_image_iff
Proof 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
Proof 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
Theorem: Matroid.Iso.basis_image_iff
Proof 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)
Proof 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
Theorem: Matroid.Iso.basis_image_iff
Proof 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)
Proof 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
Theorem: Matroid.Iso.basis_image_iff
Proof 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]
Proof state after:
no goals
Theorem: Matroid.Iso.basis_image_iff
Proof 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)
Proof state after:
no goals
Theorem: Matroid.Iso.basis_image_iff
Proof 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
Proof state after:
no goals
Theorem: Matroid.Iso.basis_image_iff
Proof 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
Proof state after:
no goals
Theorem: Matroid.Iso.exists_eq_map
Proof 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
Proof 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
Theorem: Matroid.Iso.exists_eq_map
Proof 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]]
Proof 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
Theorem: Matroid.Iso.exists_eq_map
Proof 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]
Proof 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
Theorem: Matroid.Iso.exists_eq_map
Proof 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 ?_ ?_⟩
Proof 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
Theorem: Matroid.Iso.exists_eq_map
Proof 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]
Proof 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₀
Theorem: Matroid.Iso.exists_eq_map
Proof 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⟩ ↦ ?_⟩
Proof 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
Theorem: Matroid.Iso.exists_eq_map
Proof 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]
Proof state after:
no goals
Theorem: Matroid.Iso.exists_eq_map
Proof 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]]
Proof state after:
no goals
Theorem: Matroid.Iso.exists_eq_map
Proof 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]
Proof state after:
no goals
Theorem: Matroid.Iso.exists_eq_map
Proof 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]
Proof state after:
no goals
Theorem: Matroid.Iso.exists_eq_map
Proof 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
Proof state after:
no goals
Theorem: Matroid.Iso.exists_eq_map
Proof 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]
Proof state after:
no goals
Theorem: Matroid.Iso.exists_eq_map
Proof 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]
Proof state after:
no goals
Theorem: Matroid.Iso.exists_eq_map
Proof 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]
Proof 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)
Theorem: Matroid.Iso.exists_eq_map
Proof 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]
Proof state after:
no goals
Theorem: LinearEquiv.map_trans
Proof state before:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
e₁₂ : M₁ ≃ₗ[R] M₂
e₂₃ : M₂ ≃ₗ[R] M₃
U : Submodule R M₁
⊢ Submodule.map (e₁₂ ≪≫ₗ e₂₃) U = Submodule.map e₂₃ (Submodule.map e₁₂ U)
Tactic:
rw [← LinearEquiv.map_coe,  LinearEquiv.coe_trans, Submodule.map_comp]
Proof state after:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
e₁₂ : M₁ ≃ₗ[R] M₂
e₂₃ : M₂ ≃ₗ[R] M₃
U : Submodule R M₁
⊢ Submodule.map (↑e₂₃) (Submodule.map (↑e₁₂) U) = Submodule.map e₂₃ (Submodule.map e₁₂ U)
Theorem: LinearEquiv.map_trans
Proof state before:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
e₁₂ : M₁ ≃ₗ[R] M₂
e₂₃ : M₂ ≃ₗ[R] M₃
U : Submodule R M₁
⊢ Submodule.map (↑e₂₃) (Submodule.map (↑e₁₂) U) = Submodule.map e₂₃ (Submodule.map e₁₂ U)
Tactic:
rfl
Proof state after:
no goals
Theorem: LinearMap.range_domRestrict
Proof state before:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R M
⊢ range (f.domRestrict p) = Submodule.map f p
Tactic:
ext
Proof state after:
case h
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R M
x✝ : M₂
⊢ x✝ ∈ range (f.domRestrict p) ↔ x✝ ∈ Submodule.map f p
Theorem: LinearMap.range_domRestrict
Proof state before:
case h
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R M
x✝ : M₂
⊢ x✝ ∈ range (f.domRestrict p) ↔ x✝ ∈ Submodule.map f p
Tactic:
simp
Proof state after:
no goals
Theorem: LinearMap.domRestrict_injective
Proof state before:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
hf : Function.Injective ⇑f
p : Submodule R M
⊢ Function.Injective ⇑(f.domRestrict p)
Tactic:
intro x y h
Proof state after:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
hf : Function.Injective ⇑f
p : Submodule R M
x y : ↥p
h : (f.domRestrict p) x = (f.domRestrict p) y
⊢ x = y
Theorem: LinearMap.domRestrict_injective
Proof state before:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
hf : Function.Injective ⇑f
p : Submodule R M
x y : ↥p
h : (f.domRestrict p) x = (f.domRestrict p) y
⊢ x = y
Tactic:
apply_fun (↑) using Subtype.coe_injective
Proof state after:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
hf : Function.Injective ⇑f
p : Submodule R M
x y : ↥p
h : (f.domRestrict p) x = (f.domRestrict p) y
⊢ ↑x = ↑y