-- Mathlib/Data/Matroid/Basic.lean
theorem finite_setOf_matroid {E : Set α} (hE : E.Finite) : {M : Matroid α | M.E ⊆ E}.Finite

Proof state:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.IsBase B})
⊢ {M | M.E ⊆ E}.Finite

Tactic:
have hf : f.Injective := by
  refine fun M M' hMM' ↦ ?_
  rw [Prod.mk.injEq, and_comm, Set.ext_iff, and_comm] at hMM'
  exact ext_isBase hMM'.1 (fun B _ ↦ hMM'.2 B)

Result:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.IsBase B})
hf : Function.Injective f
⊢ {M | M.E ⊆ E}.Finite

Proof state:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.IsBase B})
⊢ Function.Injective f

Tactic:
refine fun M M' hMM' ↦ ?_

Result:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.IsBase B})
M M' : Matroid α
hMM' : f M = f M'
⊢ M = M'

Proof state:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.IsBase B})
M M' : Matroid α
hMM' : M.E = M'.E ∧ ∀ (x : Set α), x ∈ {B | M.IsBase B} ↔ x ∈ {B | M'.IsBase B}
⊢ M = M'

Tactic:
exact ext_isBase hMM'.1 (fun B _ ↦ hMM'.2 B)

Result:
no goals

Proof state:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.IsBase B})
hf : Function.Injective f
⊢ {M | M.E ⊆ E}.Finite

Tactic:
rw [← Set.finite_image_iff hf.injOn]

Result:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.IsBase B})
hf : Function.Injective f
⊢ (f '' {M | M.E ⊆ E}).Finite

Proof state:
case intro.intro
α : Type u_1
E : Set α
hE✝ : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.IsBase B})
hf : Function.Injective f
M : Matroid α
hE : M.E ⊆ E
⊢ (f M).1 ⊆ E ∧ (f M).2 ⊆ {b | b ⊆ E}

Tactic:
exact ⟨hE, fun B hB ↦ hB.subset_ground.trans hE⟩

Result:
no goals

Proof state:
α : Type u_1
E : Set α
hE : E.Finite
⊢ {M | M.E ⊆ E}.Finite

Tactic:
set f : Matroid α → Set α × (Set (Set α)) := fun M ↦ ⟨M.E, {B | M.IsBase B}⟩

Result:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.IsBase B})
⊢ {M | M.E ⊆ E}.Finite

Proof state:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.IsBase B})
hf : Function.Injective f
⊢ f '' {M | M.E ⊆ E} ⊆ {b | b ⊆ E} ×ˢ {b | b ⊆ {b | b ⊆ E}}

Tactic:
rintro _ ⟨M, hE : M.E ⊆ E, rfl⟩

Result:
case intro.intro
α : Type u_1
E : Set α
hE✝ : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.IsBase B})
hf : Function.Injective f
M : Matroid α
hE : M.E ⊆ E
⊢ f M ∈ {b | b ⊆ E} ×ˢ {b | b ⊆ {b | b ⊆ E}}

Proof state:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.IsBase B})
M M' : Matroid α
hMM' : f M = f M'
⊢ M = M'

Tactic:
rw [Prod.mk.injEq, and_comm, Set.ext_iff, and_comm] at hMM'

Result:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.IsBase B})
M M' : Matroid α
hMM' : M.E = M'.E ∧ ∀ (x : Set α), x ∈ {B | M.IsBase B} ↔ x ∈ {B | M'.IsBase B}
⊢ M = M'

Proof state:
case intro.intro
α : Type u_1
E : Set α
hE✝ : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.IsBase B})
hf : Function.Injective f
M : Matroid α
hE : M.E ⊆ E
⊢ f M ∈ {b | b ⊆ E} ×ˢ {b | b ⊆ {b | b ⊆ E}}

Tactic:
simp only [Set.mem_prod, Set.mem_setOf_eq, Set.setOf_subset_setOf]

Result:
case intro.intro
α : Type u_1
E : Set α
hE✝ : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.IsBase B})
hf : Function.Injective f
M : Matroid α
hE : M.E ⊆ E
⊢ (f M).1 ⊆ E ∧ (f M).2 ⊆ {b | b ⊆ E}

Proof state:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.IsBase B})
hf : Function.Injective f
⊢ (f '' {M | M.E ⊆ E}).Finite

Tactic:
refine (hE.finite_subsets.prod hE.finite_subsets.finite_subsets).subset ?_

Result:
α : Type u_1
E : Set α
hE : E.Finite
f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.IsBase B})
hf : Function.Injective f
⊢ f '' {M | M.E ⊆ E} ⊆ {b | b ⊆ E} ×ˢ {b | b ⊆ {b | b ⊆ E}}