-- Mathlib/Combinatorics/Configuration.lean
theorem Nondegenerate.exists_injective_of_card_le [Nondegenerate P L] [Fintype P] [Fintype L]
    (h : Fintype.card L ≤ Fintype.card P) : ∃ f : L → P, Function.Injective f ∧ ∀ l, f l ∉ l

Proof state:
case pos.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => {p | p ∉ l}.toFinset
l : L
hs₀ : ¬#{l} = 0
hs₁ : #{l} = 1
⊢ #{l} ≤ #({l}.biUnion t)

Tactic:
obtain ⟨p, hl⟩ := exists_point (P := P) l

Result:
case pos.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => {p | p ∉ l}.toFinset
l : L
hs₀ : ¬#{l} = 0
hs₁ : #{l} = 1
p : P
hl : p ∉ l
⊢ #{l} ≤ #({l}.biUnion t)

Proof state:
case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : #s = 1
⊢ #s ≤ #(s.biUnion t)

Tactic:
obtain ⟨l, rfl⟩ := Finset.card_eq_one.mp hs₁

Result:
case pos.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => {p | p ∉ l}.toFinset
l : L
hs₀ : ¬#{l} = 0
hs₁ : #{l} = 1
⊢ #{l} ≤ #({l}.biUnion t)

Proof state:
case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => {p | p ∉ l}.toFinset
s : Finset L
hs₀ : #s = 0
⊢ #s ≤ #(s.biUnion t)

Tactic:
simp_rw [hs₀, zero_le]

Result:
no goals

Proof state:
case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
⊢ #(s.biUnion t)ᶜ ≤ #sᶜ

Tactic:
by_cases hs₃ : #sᶜ = 0

Result:
case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : #sᶜ = 0
⊢ #(s.biUnion t)ᶜ ≤ #sᶜ

case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : ¬#sᶜ = 0
⊢ #(s.biUnion t)ᶜ ≤ #sᶜ

Proof state:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => {p | p ∉ l}.toFinset
⊢ ∃ f, Function.Injective f ∧ ∀ (l : L), f l ∉ l

Tactic:
suffices ∀ s : Finset L, #s ≤ (s.biUnion t).card by
  obtain ⟨f, hf1, hf2⟩ := (Finset.all_card_le_biUnion_card_iff_exists_injective t).mp this
  exact ⟨f, hf1, fun l => Set.mem_toFinset.mp (hf2 l)⟩

Result:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => {p | p ∉ l}.toFinset
⊢ ∀ (s : Finset L), #s ≤ #(s.biUnion t)

Proof state:
case pos.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l => {p | p ∉ l}.toFinset
l : L
hs₀ : ¬#{l} = 0
hs₁ : #{l} = 1
p : P
hl : p ∉ l
⊢ #(t l) ≠ 0

Tactic:
exact Finset.card_ne_zero_of_mem (Set.mem_toFinset.mpr hl)

Result:
no goals