Theorem: Matroid.nonempty_iso_unif_iff (Matroid/Constructions/Uniform.lean)

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ Nonempty (M ≂ unif a b) ↔ ∃ E, M = unifOn E ↑a ∧ E.encard = ↑b
Tactic:
refine ⟨fun ⟨e⟩ ↦ ⟨M.E, ?_⟩, ?_⟩
State after:
case refine_1
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
⊢ M = unifOn M.E ↑a ∧ M.E.encard = ↑b

case refine_2
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ (∃ E, M = unifOn E ↑a ∧ E.encard = ↑b) → Nonempty (M ≂ unif a b)

State before:
case refine_2
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ (∃ E, M = unifOn E ↑a ∧ E.encard = ↑b) → Nonempty (M ≂ unif a b)
Tactic:
rintro ⟨E, rfl, hE⟩
State after:
case refine_2.intro.intro
α : Type u_1
E✝ I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
⊢ Nonempty (unifOn E ↑a ≂ unif a b)

State before:
case refine_2.intro.intro
α : Type u_1
E✝ I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
⊢ Nonempty (unifOn E ↑a ≂ unif a b)
Tactic:
obtain ⟨e⟩ := Fin.nonempty_equiv_iff_encard_eq.2 hE
State after:
case refine_2.intro.intro.intro
α : Type u_1
E✝ I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
⊢ Nonempty (unifOn E ↑a ≂ unif a b)

State before:
case refine_2.intro.intro.intro
α : Type u_1
E✝ I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
⊢ Nonempty (unifOn E ↑a ≂ unif a b)
Tactic:
refine ⟨e.trans (Equiv.Set.univ (Fin b)).symm, fun I ↦ ?_⟩
State after:
case refine_2.intro.intro.intro
α : Type u_1
E✝ I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
I : Set ↑(unifOn E ↑a).E
⊢ (unifOn E ↑a).Indep ↑I ↔ (unif a b).Indep ↑(⇑(e.trans (Equiv.Set.univ (Fin b)).symm) '' I)

State before:
case refine_2.intro.intro.intro
α : Type u_1
E✝ I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
I : Set ↑(unifOn E ↑a).E
⊢ (unifOn E ↑a).Indep ↑I ↔ (unif a b).Indep ↑(⇑(e.trans (Equiv.Set.univ (Fin b)).symm) '' I)
Tactic:
simp only [unifOn_indep_iff, Subtype.val_injective.encard_image, image_subset_iff, unif_ground_eq,
  Equiv.Set.univ, Equiv.trans_apply, Equiv.coe_fn_symm_mk, unif_indep_iff]
State after:
case refine_2.intro.intro.intro
α : Type u_1
E✝ I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
I : Set ↑(unifOn E ↑a).E
⊢ I.encard ≤ ↑a ∧ I ⊆ Subtype.val ⁻¹' E ↔ ((fun a_1 => ⟨e a_1, trivial⟩) '' I).encard ≤ ↑a

State before:
case refine_2.intro.intro.intro
α : Type u_1
E✝ I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
I : Set ↑(unifOn E ↑a).E
⊢ I.encard ≤ ↑a ∧ I ⊆ Subtype.val ⁻¹' E ↔ ((fun a_1 => ⟨e a_1, trivial⟩) '' I).encard ≤ ↑a
Tactic:
rw [Function.Injective.encard_image (fun _ _ ↦ by simp), and_iff_left_iff_imp]
State after:
case refine_2.intro.intro.intro
α : Type u_1
E✝ I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
I : Set ↑(unifOn E ↑a).E
⊢ I.encard ≤ ↑a → I ⊆ Subtype.val ⁻¹' E

State before:
case refine_2.intro.intro.intro
α : Type u_1
E✝ I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
I : Set ↑(unifOn E ↑a).E
⊢ I.encard ≤ ↑a → I ⊆ Subtype.val ⁻¹' E
Tactic:
exact fun _ ⟨_,hx⟩ _ ↦ hx
State after:
no goals

State before:
case refine_1
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
⊢ M = unifOn M.E ↑a ∧ M.E.encard = ↑b
Tactic:
rw [eq_unifOn_iff, and_iff_right rfl, and_iff_left <| by simpa using e.toEquiv.encard_eq]
State after:
case refine_1
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
⊢ ∀ (I : Set α), M.Indep I ↔ I.encard ≤ ↑a ∧ I ⊆ M.E

State before:
case refine_1
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
⊢ ∀ (I : Set α), M.Indep I ↔ I.encard ≤ ↑a ∧ I ⊆ M.E
Tactic:
refine fun I ↦ ?_
State after:
case refine_1
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
⊢ M.Indep I ↔ I.encard ≤ ↑a ∧ I ⊆ M.E

State before:
case refine_1
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
⊢ M.Indep I ↔ I.encard ≤ ↑a ∧ I ⊆ M.E
Tactic:
obtain (hIE | hIE) := em' <| I ⊆ M.E
State after:
case refine_1.inl
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : ¬I ⊆ M.E
⊢ M.Indep I ↔ I.encard ≤ ↑a ∧ I ⊆ M.E

case refine_1.inr
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : I ⊆ M.E
⊢ M.Indep I ↔ I.encard ≤ ↑a ∧ I ⊆ M.E

State before:
case refine_1.inr
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : I ⊆ M.E
⊢ M.Indep I ↔ I.encard ≤ ↑a ∧ I ⊆ M.E
Tactic:
rw [and_iff_left hIE]
State after:
case refine_1.inr
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : I ⊆ M.E
⊢ M.Indep I ↔ I.encard ≤ ↑a

State before:
case refine_1.inr
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : I ⊆ M.E
⊢ M.Indep I ↔ I.encard ≤ ↑a
Tactic:
have hwin := e.indep_image_iff (I := M.E ↓∩ I)
State after:
case refine_1.inr
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : I ⊆ M.E
hwin : M.Indep ↑(M.E ↓∩ I) ↔ (unif a b).Indep ↑(⇑e '' M.E ↓∩ I)
⊢ M.Indep I ↔ I.encard ≤ ↑a

State before:
case refine_1.inr
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : I ⊆ M.E
hwin : M.Indep ↑(M.E ↓∩ I) ↔ (unif a b).Indep ↑(⇑e '' M.E ↓∩ I)
⊢ M.Indep I ↔ I.encard ≤ ↑a
Tactic:
simp only [Subtype.image_preimage_coe, inter_eq_self_of_subset_right hIE, unif_ground_eq,
  unif_indep_iff] at hwin
State after:
case refine_1.inr
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : I ⊆ M.E
hwin : M.Indep I ↔ ((fun a => ↑a) '' ((fun a_1 => e a_1) '' M.E ↓∩ I)).encard ≤ ↑a
⊢ M.Indep I ↔ I.encard ≤ ↑a

State before:
case refine_1.inr
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : I ⊆ M.E
hwin : M.Indep I ↔ ((fun a => ↑a) '' ((fun a_1 => e a_1) '' M.E ↓∩ I)).encard ≤ ↑a
⊢ M.Indep I ↔ I.encard ≤ ↑a
Tactic:
rwa [Subtype.val_injective.encard_image, (EmbeddingLike.injective' _).encard_image,
  encard_preimage_of_injective_subset_range Subtype.val_injective (by simpa)] at hwin
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
⊢ M.E.encard = ↑b
Tactic:
simpa using e.toEquiv.encard_eq
State after:
no goals

State before:
case refine_1.inl
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : ¬I ⊆ M.E
⊢ M.Indep I ↔ I.encard ≤ ↑a ∧ I ⊆ M.E
Tactic:
exact iff_of_false (fun h ↦ hIE h.subset_ground) (by simp [hIE])
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : ¬I ⊆ M.E
⊢ ¬(I.encard ≤ ↑a ∧ I ⊆ M.E)
Tactic:
simp [hIE]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
I : Set α
hIE : I ⊆ M.E
hwin : M.Indep I ↔ (M.E ↓∩ I).encard ≤ ↑a
⊢ I ⊆ range Subtype.val
Tactic:
simpa
State after:
no goals

State before:
α : Type u_1
E✝ I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
e : ↑E ≃ Fin b
I : Set ↑(unifOn E ↑a).E
x✝¹ x✝ : ↑(unifOn E ↑a).E
⊢ ⟨e x✝¹, trivial⟩ = ⟨e x✝, trivial⟩ → x✝¹ = x✝
Tactic:
simp
State after:
no goals