[GOAL]
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a a' : α
b b' : β
inst✝² : DecidablePred (r a)
inst✝¹ : (a : α) → Decidable (r a b)
m n : ℕ
inst✝ : (a : α) → (b : β) → Decidable (r a b)
⊢ ∑ a in s, card (bipartiteAbove r t a) = ∑ b in t, card (bipartiteBelow r s b)
[PROOFSTEP]
simp_rw [card_eq_sum_ones, bipartiteAbove, bipartiteBelow, sum_filter]
[GOAL]
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a a' : α
b b' : β
inst✝² : DecidablePred (r a)
inst✝¹ : (a : α) → Decidable (r a b)
m n : ℕ
inst✝ : (a : α) → (b : β) → Decidable (r a b)
⊢ (∑ x in s, ∑ a in t, if r x a then 1 else 0) = ∑ x in t, ∑ a in s, if r a x then 1 else 0
[PROOFSTEP]
exact sum_comm
[GOAL]
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a a' : α
b b' : β
inst✝¹ : DecidablePred (r a)
inst✝ : (a : α) → Decidable (r a b)
m n : ℕ
hs : ∀ (a : α), a ∈ s → ∃ b, b ∈ t ∧ r a b
ht : ∀ (b : β), b ∈ t → Set.Subsingleton {a | a ∈ s ∧ r a b}
⊢ card s ≤ card t
[PROOFSTEP]
classical
rw [← mul_one s.card, ← mul_one t.card]
exact
  card_mul_le_card_mul r
    (fun a h ↦
      card_pos.2
        (by
          rw [← coe_nonempty, coe_bipartiteAbove]
          exact hs _ h : (t.bipartiteAbove r a).Nonempty))
    (fun b h ↦
      card_le_one.2
        (by
          simp_rw [mem_bipartiteBelow]
          exact ht _ h))
[GOAL]
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a a' : α
b b' : β
inst✝¹ : DecidablePred (r a)
inst✝ : (a : α) → Decidable (r a b)
m n : ℕ
hs : ∀ (a : α), a ∈ s → ∃ b, b ∈ t ∧ r a b
ht : ∀ (b : β), b ∈ t → Set.Subsingleton {a | a ∈ s ∧ r a b}
⊢ card s ≤ card t
[PROOFSTEP]
rw [← mul_one s.card, ← mul_one t.card]
[GOAL]
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a a' : α
b b' : β
inst✝¹ : DecidablePred (r a)
inst✝ : (a : α) → Decidable (r a b)
m n : ℕ
hs : ∀ (a : α), a ∈ s → ∃ b, b ∈ t ∧ r a b
ht : ∀ (b : β), b ∈ t → Set.Subsingleton {a | a ∈ s ∧ r a b}
⊢ card s * 1 ≤ card t * 1
[PROOFSTEP]
exact
  card_mul_le_card_mul r
    (fun a h ↦
      card_pos.2
        (by
          rw [← coe_nonempty, coe_bipartiteAbove]
          exact hs _ h : (t.bipartiteAbove r a).Nonempty))
    (fun b h ↦
      card_le_one.2
        (by
          simp_rw [mem_bipartiteBelow]
          exact ht _ h))
[GOAL]
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a✝ a' : α
b b' : β
inst✝¹ : DecidablePred (r a✝)
inst✝ : (a : α) → Decidable (r a b)
m n : ℕ
hs : ∀ (a : α), a ∈ s → ∃ b, b ∈ t ∧ r a b
ht : ∀ (b : β), b ∈ t → Set.Subsingleton {a | a ∈ s ∧ r a b}
a : α
h : a ∈ s
⊢ Finset.Nonempty (bipartiteAbove r t a)
[PROOFSTEP]
rw [← coe_nonempty, coe_bipartiteAbove]
[GOAL]
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a✝ a' : α
b b' : β
inst✝¹ : DecidablePred (r a✝)
inst✝ : (a : α) → Decidable (r a b)
m n : ℕ
hs : ∀ (a : α), a ∈ s → ∃ b, b ∈ t ∧ r a b
ht : ∀ (b : β), b ∈ t → Set.Subsingleton {a | a ∈ s ∧ r a b}
a : α
h : a ∈ s
⊢ Set.Nonempty {b | b ∈ t ∧ r a b}
[PROOFSTEP]
exact hs _ h
[GOAL]
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a a' : α
b✝ b' : β
inst✝¹ : DecidablePred (r a)
inst✝ : (a : α) → Decidable (r a b✝)
m n : ℕ
hs : ∀ (a : α), a ∈ s → ∃ b, b ∈ t ∧ r a b
ht : ∀ (b : β), b ∈ t → Set.Subsingleton {a | a ∈ s ∧ r a b}
b : β
h : b ∈ t
⊢ ∀ (a : α), a ∈ bipartiteBelow r s b → ∀ (b_1 : α), b_1 ∈ bipartiteBelow r s b → a = b_1
[PROOFSTEP]
simp_rw [mem_bipartiteBelow]
[GOAL]
α : Type u_1
β : Type u_2
r : α → β → Prop
s : Finset α
t : Finset β
a a' : α
b✝ b' : β
inst✝¹ : DecidablePred (r a)
inst✝ : (a : α) → Decidable (r a b✝)
m n : ℕ
hs : ∀ (a : α), a ∈ s → ∃ b, b ∈ t ∧ r a b
ht : ∀ (b : β), b ∈ t → Set.Subsingleton {a | a ∈ s ∧ r a b}
b : β
h : b ∈ t
⊢ ∀ (a : α), a ∈ s ∧ r a b → ∀ (b_1 : α), b_1 ∈ s ∧ r b_1 b → a = b_1
[PROOFSTEP]
exact ht _ h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
r : α → β → Prop
h₁ : LeftTotal r
h₂ : LeftUnique r
⊢ ∀ (a : α), a ∈ univ → ∃ b, b ∈ univ ∧ r a b
[PROOFSTEP]
simpa using h₁
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
r : α → β → Prop
h₁ : RightTotal r
h₂ : RightUnique r
⊢ ∀ (b : β), b ∈ univ → ∃ a, a ∈ univ ∧ r a b
[PROOFSTEP]
simpa using h₁
