internlm/Lean-Github huggingface dataset:
Theorem: Matroid.comap_basis_iff
Proof state before:
case refine_2.refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ (N.comap f).Dep (insert e I)
Tactic:
have hIE : insert e I ⊆ (N.comap f).E := by
    simp_rw [comap_ground_eq, ← image_subset_iff]
    exact (image_subset _ (insert_subset heX h.2.1)).trans h.1.subset_ground
Proof state after:
case refine_2.refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
hIE : insert e I ⊆ (N.comap f).E
⊢ (N.comap f).Dep (insert e I)
Theorem: Matroid.comap_basis_iff
Proof state before:
case refine_2.refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
hIE : insert e I ⊆ (N.comap f).E
⊢ (N.comap f).Dep (insert e I)
Tactic:
suffices N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e
  by simpa [← not_indep_iff hIE, injOn_insert heI, h.2.2, image_insert_eq]
Proof state after:
case refine_2.refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
hIE : insert e I ⊆ (N.comap f).E
⊢ N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e
Theorem: Matroid.comap_basis_iff
Proof state before:
case refine_2.refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
hIE : insert e I ⊆ (N.comap f).E
⊢ N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e
Tactic:
exact h.1.mem_of_insert_indep (mem_image_of_mem f heX)
Proof state after:
no goals
Theorem: Matroid.comap_basis_iff
Proof state before:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
⊢ N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
Tactic:
obtain ⟨hI, hinj⟩ := comap_indep_iff.1 h.indep
Proof state after:
case refine_1.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
⊢ N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
Theorem: Matroid.comap_basis_iff
Proof state before:
case refine_1.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
⊢ N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
Tactic:
refine ⟨hI.basis_of_forall_insert (image_subset f h.subset) fun e he ↦ ?_, h.subset, hinj⟩
Proof state after:
case refine_1.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : β
he : e ∈ f '' X \ f '' I
⊢ N.Dep (insert e (f '' I))
Theorem: Matroid.comap_basis_iff
Proof state before:
case refine_1.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : β
he : e ∈ f '' X \ f '' I
⊢ N.Dep (insert e (f '' I))
Tactic:
simp only [mem_diff, mem_image, not_exists, not_and, and_imp, forall_exists_index,
  forall_apply_eq_imp_iff₂] at he
Proof state after:
case refine_1.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : β
he : (∃ x ∈ X, f x = e) ∧ ∀ x ∈ I, ¬f x = e
⊢ N.Dep (insert e (f '' I))
Theorem: Matroid.comap_basis_iff
Proof state before:
case refine_1.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : β
he : (∃ x ∈ X, f x = e) ∧ ∀ x ∈ I, ¬f x = e
⊢ N.Dep (insert e (f '' I))
Tactic:
obtain ⟨⟨e, heX, rfl⟩, he⟩ := he
Proof state after:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
⊢ N.Dep (insert (f e) (f '' I))
Theorem: Matroid.comap_basis_iff
Proof state before:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
⊢ N.Dep (insert (f e) (f '' I))
Tactic:
have heI : e ∉ I := fun heI ↦ (he e heI rfl)
Proof state after:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
heI : e ∉ I
⊢ N.Dep (insert (f e) (f '' I))
Theorem: Matroid.comap_basis_iff
Proof state before:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : (N.comap f).Basis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
heI : e ∉ I
⊢ N.Dep (insert (f e) (f '' I))
Tactic:
replace h := h.insert_dep ⟨heX, heI⟩
Proof state after:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
heI : e ∉ I
h : (N.comap f).Dep (insert e I)
⊢ N.Dep (insert (f e) (f '' I))
Theorem: Matroid.comap_basis_iff
Proof state before:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
heI : e ∉ I
h : (N.comap f).Dep (insert e I)
⊢ N.Dep (insert (f e) (f '' I))
Tactic:
simp only [comap_dep_iff, image_insert_eq, or_iff_not_imp_right, injOn_insert heI,
  hinj, mem_image, not_exists, not_and, true_and, not_forall, Classical.not_imp, not_not] at h
Proof state after:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
heI : e ∉ I
h : (N.Indep (insert (f e) (f '' I)) → ∀ x ∈ I, ¬f x = f e) → N.Dep (insert (f e) (f '' I))
⊢ N.Dep (insert (f e) (f '' I))
Theorem: Matroid.comap_basis_iff
Proof state before:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
hI : N.Indep (f '' I)
hinj : InjOn f I
e : α
heX : e ∈ X
he : ∀ x ∈ I, ¬f x = f e
heI : e ∉ I
h : (N.Indep (insert (f e) (f '' I)) → ∀ x ∈ I, ¬f x = f e) → N.Dep (insert (f e) (f '' I))
⊢ N.Dep (insert (f e) (f '' I))
Tactic:
exact h (fun _ ↦ he)
Proof state after:
no goals
Theorem: Matroid.comap_basis_iff
Proof state before:
case refine_2.refine_1
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
⊢ (N.comap f).Indep I
Tactic:
simp [comap_indep_iff, h.1.indep, h.2]
Proof state after:
no goals
Theorem: Matroid.comap_basis_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ insert e I ⊆ (N.comap f).E
Tactic:
simp_rw [comap_ground_eq, ← image_subset_iff]
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ f '' insert e I ⊆ N.E
Theorem: Matroid.comap_basis_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ f '' insert e I ⊆ N.E
Tactic:
exact (image_subset _ (insert_subset heX h.2.1)).trans h.1.subset_ground
Proof state after:
no goals
Theorem: Matroid.comap_basis_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
hIE : insert e I ⊆ (N.comap f).E
this : N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e
⊢ (N.comap f).Dep (insert e I)
Tactic:
simpa [← not_indep_iff hIE, injOn_insert heI, h.2.2, image_insert_eq]
Proof state after:
no goals
Theorem: Matroid.comap_basis'_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
⊢ (N.comap f).Basis' I X ↔ N.Basis' (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
Tactic:
simp only [basis'_iff_basis_inter_ground, comap_ground_eq, comap_basis_iff, image_inter_preimage,
  subset_inter_iff, ← and_assoc, and_congr_left_iff, and_iff_left_iff_imp, and_imp]
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
⊢ InjOn f I → N.Basis (f '' I) (f '' X ∩ N.E) → I ⊆ X → I ⊆ f ⁻¹' N.E
Theorem: Matroid.comap_basis'_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
⊢ InjOn f I → N.Basis (f '' I) (f '' X ∩ N.E) → I ⊆ X → I ⊆ f ⁻¹' N.E
Tactic:
exact fun _ h _ ↦ (image_subset_iff.1 h.indep.subset_ground)
Proof state after:
no goals
Theorem: Matroid.comapOn_preimage_eq
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
⊢ N.comapOn (f ⁻¹' N.E) f = N.comap f
Tactic:
rw [comapOn, restrict_eq_self_iff]
Proof state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
⊢ f ⁻¹' N.E = (N.comap f).E
Theorem: Matroid.comapOn_preimage_eq
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
⊢ f ⁻¹' N.E = (N.comap f).E
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.comapOn_indep_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
⊢ (N.comapOn E f).Indep I ↔ N.Indep (f '' I) ∧ InjOn f I ∧ I ⊆ E
Tactic:
simp [comapOn, and_assoc]
Proof state after:
no goals
Theorem: Matroid.comapOn_base_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
B E : Set α
⊢ (N.comapOn E f).Base B ↔ N.Basis' (f '' B) (f '' E) ∧ B ⊆ E ∧ InjOn f B
Tactic:
rw [comapOn, base_restrict_iff', comap_basis'_iff]
Proof state after:
no goals
Theorem: Matroid.comapOn_base_iff_of_surjOn
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : SurjOn f E N.E
B : Set α
⊢ (N.comapOn E f).Base B ↔ N.Base (f '' B) ∧ B ⊆ E ∧ InjOn f B
Tactic:
simp_rw [comapOn_base_iff, and_congr_left_iff, and_imp,
  basis'_iff_basis_inter_ground, inter_eq_self_of_subset_right h, basis_ground_iff, implies_true]
Proof state after:
no goals
Theorem: Matroid.comapOn_base_iff_of_bijOn
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
⊢ (N.comapOn E f).Base B ↔ N.Base (f '' B) ∧ B ⊆ E
Tactic:
rw [← and_iff_left_of_imp (Base.subset_ground (M := N.comapOn E f) (B := B)),
  comapOn_ground_eq, and_congr_left_iff]
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
⊢ B ⊆ E → ((N.comapOn E f).Base B ↔ N.Base (f '' B))
Theorem: Matroid.comapOn_base_iff_of_bijOn
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
⊢ B ⊆ E → ((N.comapOn E f).Base B ↔ N.Base (f '' B))
Tactic:
suffices h' : B ⊆ E → InjOn f B from fun hB ↦
  by simp [hB, comapOn_base_iff_of_surjOn h.surjOn, h']
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
⊢ B ⊆ E → InjOn f B
Theorem: Matroid.comapOn_base_iff_of_bijOn
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
⊢ B ⊆ E → InjOn f B
Tactic:
exact fun hBE ↦ h.injOn.mono hBE
Proof state after:
no goals
Theorem: Matroid.comapOn_base_iff_of_bijOn
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
h' : B ⊆ E → InjOn f B
hB : B ⊆ E
⊢ (N.comapOn E f).Base B ↔ N.Base (f '' B)
Tactic:
simp [hB, comapOn_base_iff_of_surjOn h.surjOn, h']
Proof state after:
no goals
Theorem: Matroid.comapOn_dual_eq_of_bijOn
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
⊢ (N.comapOn E f)✶ = N✶.comapOn E f
Tactic:
refine eq_of_base_iff_base_forall (by simp) (fun B hB ↦ ?_)
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ (N.comapOn E f)✶.Base B ↔ (N✶.comapOn E f).Base B
Theorem: Matroid.comapOn_dual_eq_of_bijOn
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ (N.comapOn E f)✶.Base B ↔ (N✶.comapOn E f).Base B
Tactic:
rw [comapOn_base_iff_of_bijOn (by simpa), dual_base_iff, comapOn_base_iff_of_bijOn h,
  dual_base_iff _, comapOn_ground_eq, and_iff_left diff_subset, and_iff_left (by simpa),
  h.injOn.image_diff_subset (by simpa), h.image_eq]
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ f '' B ⊆ N.E
Theorem: Matroid.comapOn_dual_eq_of_bijOn
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ f '' B ⊆ N.E
Tactic:
exact (h.mapsTo.mono_left (show B ⊆ E by simpa)).image_subset
Proof state after:
no goals
Theorem: Matroid.comapOn_dual_eq_of_bijOn
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
⊢ (N.comapOn E f)✶.E = (N✶.comapOn E f).E
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.comapOn_dual_eq_of_bijOn
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ BijOn f E N✶.E
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.comapOn_dual_eq_of_bijOn
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ B ⊆ E
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.mapSetEmbedding_indep_iff'
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set β
⊢ (M.mapSetEmbedding f).Indep I ↔ ∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀
Tactic:
simp only [mapSetEmbedding_indep_iff, subset_range_iff_exists_image_eq]
Proof state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set β
⊢ (M.Indep ↑(⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I) ↔ ∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀
Theorem: Matroid.mapSetEmbedding_indep_iff'
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set β
⊢ (M.Indep ↑(⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I) ↔ ∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set β
⊢ (M.Indep ↑(⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I) → ∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀

case mpr
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set β
⊢ (∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀) → M.Indep ↑(⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I
Theorem: Matroid.mapSetEmbedding_indep_iff'
Proof state before:
case mpr
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set β
⊢ (∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀) → M.Indep ↑(⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I
Tactic:
rintro ⟨I, hI, rfl⟩
Proof state after:
case mpr.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep ↑I
⊢ M.Indep ↑(⇑f ⁻¹' (⇑f '' I)) ∧ ∃ t, ⇑f '' t = ⇑f '' I
Theorem: Matroid.mapSetEmbedding_indep_iff'
Proof state before:
case mpr.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep ↑I
⊢ M.Indep ↑(⇑f ⁻¹' (⇑f '' I)) ∧ ∃ t, ⇑f '' t = ⇑f '' I
Tactic:
rw [preimage_image_eq _ f.injective]
Proof state after:
case mpr.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep ↑I
⊢ M.Indep ↑I ∧ ∃ t, ⇑f '' t = ⇑f '' I
Theorem: Matroid.mapSetEmbedding_indep_iff'
Proof state before:
case mpr.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep ↑I
⊢ M.Indep ↑I ∧ ∃ t, ⇑f '' t = ⇑f '' I
Tactic:
exact ⟨hI, _, rfl⟩
Proof state after:
no goals
Theorem: Matroid.mapSetEmbedding_indep_iff'
Proof state before:
case mp
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set β
⊢ (M.Indep ↑(⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I) → ∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀
Tactic:
rintro ⟨hI, I, rfl⟩
Proof state after:
case mp.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep ↑(⇑f ⁻¹' (⇑f '' I))
⊢ ∃ I₀, M.Indep ↑I₀ ∧ ⇑f '' I = ⇑f '' I₀
Theorem: Matroid.mapSetEmbedding_indep_iff'
Proof state before:
case mp.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep ↑(⇑f ⁻¹' (⇑f '' I))
⊢ ∃ I₀, M.Indep ↑I₀ ∧ ⇑f '' I = ⇑f '' I₀
Tactic:
exact ⟨I, by rwa [preimage_image_eq _ f.injective] at hI, rfl⟩
Proof state after:
no goals
Theorem: Matroid.mapSetEmbedding_indep_iff'
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep ↑(⇑f ⁻¹' (⇑f '' I))
⊢ M.Indep ↑I
Tactic:
rwa [preimage_image_eq _ f.injective] at hI
Proof state after:
no goals
Theorem: Matroid.map_image_indep_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
⊢ (M.map f hf).Indep (f '' I) ↔ M.Indep I
Tactic:
rw [map_indep_iff]
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
⊢ (∃ I₀, M.Indep I₀ ∧ f '' I = f '' I₀) ↔ M.Indep I
Theorem: Matroid.map_image_indep_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
⊢ (∃ I₀, M.Indep I₀ ∧ f '' I = f '' I₀) ↔ M.Indep I
Tactic:
refine ⟨fun ⟨J, hJ, hIJ⟩ ↦ ?_, fun h ↦ ⟨I, h, rfl⟩ ⟩
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
x✝ : ∃ I₀, M.Indep I₀ ∧ f '' I = f '' I₀
J : Set α
hJ : M.Indep J
hIJ : f '' I = f '' J
⊢ M.Indep I
Theorem: Matroid.map_image_indep_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
x✝ : ∃ I₀, M.Indep I₀ ∧ f '' I = f '' I₀
J : Set α
hJ : M.Indep J
hIJ : f '' I = f '' J
⊢ M.Indep I
Tactic:
rw [hf.image_eq_image_iff hI hJ.subset_ground] at hIJ
Proof state after:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
x✝ : ∃ I₀, M.Indep I₀ ∧ f '' I = f '' I₀
J : Set α
hJ : M.Indep J
hIJ : I = J
⊢ M.Indep I
Theorem: Matroid.map_image_indep_iff
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
x✝ : ∃ I₀, M.Indep I₀ ∧ f '' I = f '' I₀
J : Set α
hJ : M.Indep J
hIJ : I = J
⊢ M.Indep I
Tactic:
rwa [hIJ]
Proof state after:
no goals
Theorem: Matroid.map_base_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
⊢ (M.map f hf).Base B ↔ ∃ B₀, M.Base B₀ ∧ B = f '' B₀
Tactic:
rw [base_iff_maximal_indep, map_indep_iff]
Proof state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
⊢ ((∃ I₀, M.Indep I₀ ∧ B = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → B ⊆ I → B = I) ↔
    ∃ B₀, M.Base B₀ ∧ B = f '' B₀
Theorem: Matroid.map_base_iff
Proof state before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
⊢ ((∃ I₀, M.Indep I₀ ∧ B = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → B ⊆ I → B = I) ↔
    ∃ B₀, M.Base B₀ ∧ B = f '' B₀
Tactic:
refine ⟨fun ⟨h, hB⟩ ↦ ?_, fun h ↦ ?_⟩
Proof state after:
case refine_1
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
x✝ : (∃ I₀, M.Indep I₀ ∧ B = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → B ⊆ I → B = I
h : ∃ I₀, M.Indep I₀ ∧ B = f '' I₀
hB : ∀ (I : Set β), (M.map f hf).Indep I → B ⊆ I → B = I
⊢ ∃ B₀, M.Base B₀ ∧ B = f '' B₀

case refine_2
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : ∃ B₀, M.Base B₀ ∧ B = f '' B₀
⊢ (∃ I₀, M.Indep I₀ ∧ B = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → B ⊆ I → B = I
Theorem: Matroid.map_base_iff
Proof state before:
case refine_2
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : ∃ B₀, M.Base B₀ ∧ B = f '' B₀
⊢ (∃ I₀, M.Indep I₀ ∧ B = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → B ⊆ I → B = I
Tactic:
obtain ⟨B₀, hB, rfl⟩ := h
Proof state after:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB : M.Base B₀
⊢ (∃ I₀, M.Indep I₀ ∧ f '' B₀ = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
Theorem: Matroid.map_base_iff
Proof state before:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB : M.Base B₀
⊢ (∃ I₀, M.Indep I₀ ∧ f '' B₀ = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
Tactic:
refine ⟨⟨B₀, hB.indep, rfl⟩, fun I hI hB₀I ↦ ?_⟩
Proof state after:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB : M.Base B₀
I : Set β
hI : (M.map f hf).Indep I
hB₀I : f '' B₀ ⊆ I
⊢ f '' B₀ = I
Theorem: Matroid.map_base_iff
Proof state before:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB : M.Base B₀
I : Set β
hI : (M.map f hf).Indep I
hB₀I : f '' B₀ ⊆ I
⊢ f '' B₀ = I
Tactic:
obtain ⟨I, hI', rfl⟩ := map_indep_iff.1 hI
Proof state after:
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB : M.Base B₀
I : Set α
hI' : M.Indep I
hI : (M.map f hf).Indep (f '' I)
hB₀I : f '' B₀ ⊆ f '' I
⊢ f '' B₀ = f '' I