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

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
hE : E.Finite
⊢ (unifOn E k)✶ = unifOn E (E.encard - k)
Tactic:
obtain (rfl | hk) := eq_or_ne k ⊤
State after:
case inl
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
⊢ (unifOn E ⊤)✶ = unifOn E (E.encard - ⊤)

case inr
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
hE : E.Finite
hk : k ≠ ⊤
⊢ (unifOn E k)✶ = unifOn E (E.encard - k)

State before:
case inl
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
⊢ (unifOn E ⊤)✶ = unifOn E (E.encard - ⊤)

case inr
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
hE : E.Finite
hk : k ≠ ⊤
⊢ (unifOn E k)✶ = unifOn E (E.encard - k)
Tactic:
simp
State after:
case inr
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
hE : E.Finite
hk : k ≠ ⊤
⊢ (unifOn E k)✶ = unifOn E (E.encard - k)

State before:
case inr
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
hE : E.Finite
hk : k ≠ ⊤
⊢ (unifOn E k)✶ = unifOn E (E.encard - k)
Tactic:
lift k to ℕ using hk
State after:
case inr.intro
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
k : ℕ
⊢ (unifOn E ↑k)✶ = unifOn E (E.encard - ↑k)

State before:
case inr.intro
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
k : ℕ
⊢ (unifOn E ↑k)✶ = unifOn E (E.encard - ↑k)
Tactic:
obtain (hle | hlt) := le_or_lt E.encard k
State after:
case inr.intro.inl
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
k : ℕ
hle : E.encard ≤ ↑k
⊢ (unifOn E ↑k)✶ = unifOn E (E.encard - ↑k)

case inr.intro.inr
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
k : ℕ
hlt : ↑k < E.encard
⊢ (unifOn E ↑k)✶ = unifOn E (E.encard - ↑k)

State before:
case inr.intro.inr
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
k : ℕ
hlt : ↑k < E.encard
⊢ (unifOn E ↑k)✶ = unifOn E (E.encard - ↑k)
Tactic:
refine eq_of_base_iff_base_forall (by simp) (fun B hBE ↦ ?_)
State after:
case inr.intro.inr
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
hE : E.Finite
k : ℕ
hlt : ↑k < E.encard
B : Set α
hBE : B ⊆ (unifOn E ↑k)✶.E
⊢ (unifOn E ↑k)✶.Base B ↔ (unifOn E (E.encard - ↑k)).Base B

State before:
case inr.intro.inr
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
hE : E.Finite
k : ℕ
hlt : ↑k < E.encard
B : Set α
hBE : B ⊆ (unifOn E ↑k)✶.E
⊢ (unifOn E ↑k)✶.Base B ↔ (unifOn E (E.encard - ↑k)).Base B
Tactic:
simp only [dual_ground, unifOn_ground_eq] at hBE
State after:
case inr.intro.inr
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
hE : E.Finite
k : ℕ
hlt : ↑k < E.encard
B : Set α
hBE : B ⊆ E
⊢ (unifOn E ↑k)✶.Base B ↔ (unifOn E (E.encard - ↑k)).Base B

State before:
case inr.intro.inr
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
hE : E.Finite
k : ℕ
hlt : ↑k < E.encard
B : Set α
hBE : B ⊆ E
⊢ (unifOn E ↑k)✶.Base B ↔ (unifOn E (E.encard - ↑k)).Base B
Tactic:
rw [dual_base_iff', unifOn_base_iff' ((tsub_le_self.trans_lt hE.encard_lt_top).ne) (by simp) hBE,
  unifOn_ground_eq, and_iff_left hBE, unifOn_base_iff hlt.le diff_subset,
  ← WithTop.add_right_cancel_iff (hE.subset hBE).encard_lt_top.ne,
  encard_diff_add_encard_of_subset hBE, Iff.comm, eq_comm, add_comm,
  ← WithTop.add_right_cancel_iff (hlt.trans_le le_top).ne, tsub_add_cancel_of_le hlt.le]
State after:
no goals

State before:
case inr.intro.inl
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
k : ℕ
hle : E.encard ≤ ↑k
⊢ (unifOn E ↑k)✶ = unifOn E (E.encard - ↑k)
Tactic:
rw [unifOn_eq_of_le hle, freeOn_dual_eq, tsub_eq_zero_of_le hle, unifOn_zero]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
k : ℕ
hlt : ↑k < E.encard
⊢ (unifOn E ↑k)✶.E = (unifOn E (E.encard - ↑k)).E
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
hE : E.Finite
k : ℕ
hlt : ↑k < E.encard
B : Set α
hBE : B ⊆ E
⊢ E.encard - ↑k ≤ E.encard
Tactic:
simp
State after:
no goals