Theorem: Matroid.unif_dual' (Matroid/Constructions/Uniform.lean)

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' n : ℕ
h : a + b = n
⊢ (unif a n)✶ = unif b n
Tactic:
subst h
State after:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ (unif a (a + b))✶ = unif b (a + b)

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ (unif a (a + b))✶ = unif b (a + b)
Tactic:
refine eq_of_base_iff_base_forall rfl (fun B _ ↦ ?_)
State after:
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
B : Set (Fin (a + b))
x✝ : B ⊆ (unif a (a + b))✶.E
⊢ (unif a (a + b))✶.Base B ↔ (unif b (a + b)).Base B

State before:
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
B : Set (Fin (a + b))
x✝ : B ⊆ (unif a (a + b))✶.E
⊢ (unif a (a + b))✶.Base B ↔ (unif b (a + b)).Base B
Tactic:
rw [dual_base_iff, unif_ground_eq, unif_base_iff (Nat.le_add_right _ _),
  unif_base_iff (Nat.le_add_left _ _),
  ← WithTop.add_right_cancel_iff (encard_ne_top_iff.2 B.toFinite),
  encard_diff_add_encard_of_subset (subset_univ _), Iff.comm,
  ← WithTop.add_left_cancel_iff (WithTop.coe_ne_top (a := a)), eq_comm]
State after:
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
B : Set (Fin (a + b))
x✝ : B ⊆ (unif a (a + b))✶.E
⊢ ↑a + ↑b = ↑a + B.encard ↔ univ.encard = ↑a + B.encard

State before:
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
B : Set (Fin (a + b))
x✝ : B ⊆ (unif a (a + b))✶.E
⊢ ↑a + ↑b = ↑a + B.encard ↔ univ.encard = ↑a + B.encard
Tactic:
convert Iff.rfl
State after:
case h.e'_2.h.e'_2
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
B : Set (Fin (a + b))
x✝ : B ⊆ (unif a (a + b))✶.E
⊢ univ.encard = ↑a + ↑b

State before:
case h.e'_2.h.e'_2
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
B : Set (Fin (a + b))
x✝ : B ⊆ (unif a (a + b))✶.E
⊢ univ.encard = ↑a + ↑b
Tactic:
rw [encard_univ, PartENat.card_eq_coe_fintype_card, Fintype.card_fin,
  PartENat.withTopEquiv_natCast, ENat.some_eq_coe, eq_comm, Nat.cast_add]
State after:
no goals