-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ a ∈ s, Injective (f a)
hs : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑s : Set α)) id
empty :
  ∀ (hf : ∀ (a : α), Membership.mem (γ := Finset α) ∅ a → Injective (f a))
    (hs : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑∅ : Set α)) id),
    #t ∣ #(image₂ f ∅ t)
insert insert₁ :
  ∀ (a : α) (s : Finset α),
    a ∉ s →
      ∀
        (ih :
          ∀ (hf : ∀ a ∈ s, Injective (f a))
            (hs : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑s : Set α)) id),
            #t ∣ #(image₂ f s t))
        (hf : ∀ a_2 ∈ Insert.insert a s, Injective (f a_2))
        (hs :
          PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(Insert.insert a s) : Set α))
            id),
        #t ∣ #(image₂ f (Insert.insert a s) t)
insert₂ :
  ∀ (a : α) (s : Finset α),
    a ∉ s →
      ∀ (hf : ∀ a_2 ∈ Insert.insert a s, Injective (f a_2))
        (hs :
          PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(Insert.insert a s) : Set α))
            id)
        (ih : #t ∣ #(image₂ f s t)), #t ∣ #(image₂ f (Insert.insert a s) t)
insert₃ :
  ∀ (a : α) (s : Finset α),
    a ∉ s →
      ∀ (hf : ∀ a_2 ∈ Insert.insert a s, Injective (f a_2))
        (hs :
          PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(Insert.insert a s) : Set α))
            id)
        (ih : #t ∣ #(image₂ f s t)), #t ∣ #(image (fun (b : β) ↦ f a b) t ∪ image₂ f s t)
pos :
  ∀ (a : α) (s : Finset α),
    a ∉ s →
      ∀ (hf : ∀ a_2 ∈ Insert.insert a s, Injective (f a_2))
        (hs :
          PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(Insert.insert a s) : Set α))
            id)
        (ih : #t ∣ #(image₂ f s t)) (h : Disjoint (image (f a) t) (image₂ f s t)),
        #t ∣ #(image (fun (b : β) ↦ f a b) t ∪ image₂ f s t)
neg neg₁ :
  ∀ (a : α) (s : Finset α),
    a ∉ s →
      ∀ (hf : ∀ a_2 ∈ Insert.insert a s, Injective (f a_2))
        (hs :
          PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(Insert.insert a s) : Set α))
            id)
        (ih : #t ∣ #(image₂ f s t)) (h : ¬Disjoint (image (f a) t) (image₂ f s t)),
        #t ∣ #(image (fun (b : β) ↦ f a b) t ∪ image₂ f s t)
neg₂ :
  ∀ (a : α) (s : Finset α),
    a ∉ s →
      ∀ (hf : ∀ a_2 ∈ Insert.insert a s, Injective (f a_2))
        (hs :
          PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(Insert.insert a s) : Set α))
            id)
        (ih : #t ∣ #(image₂ f s t)) (h : ∃ (x : α) (_ : x ∈ s), ¬Disjoint (image (f a) t) (image (f x) t)),
        #t ∣ #(image (fun (b : β) ↦ f a b) t ∪ image₂ f s t)
neg₃ :
  ∀ (a : α) (s : Finset α),
    a ∉ s →
      ∀ (hf : ∀ a_2 ∈ Insert.insert a s, Injective (f a_2))
        (hs :
          PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(Insert.insert a s) : Set α))
            id)
        (ih : #t ∣ #(image₂ f s t)) (b : α) (hb : b ∈ s) (h : ¬Disjoint (image (f a) t) (image (f b) t)),
        #t ∣ #(image (fun (b : β) ↦ f a b) t ∪ image₂ f s t)
neg₄ :
  ∀ (a : α) (s : Finset α),
    a ∉ s →
      ∀ (hf : ∀ a_2 ∈ Insert.insert a s, Injective (f a_2))
        (hs :
          PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(Insert.insert a s) : Set α))
            id)
        (ih : #t ∣ #(image₂ f s t)) (b : α) (hb : b ∈ s) (h : ¬Disjoint (image (f a) t) (image (f b) t)),
        image (fun (b : β) ↦ f a b) t ⊆ image₂ f s t
⊢ #t ∣ #(image₂ f s t)

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s _ ih => ?_
  specialize ih (forall_of_forall_insert hf)
    (hs.subset <| Set.image_mono <| coe_subset.2 <| subset_insert _ _)
  rw [image₂_insert_left]
  by_cases h : Disjoint (image (f a) t) (image₂ f s t)
  · rw [card_union_of_disjoint h]
    exact Nat.dvd_add (card_image_of_injective _ <| hf _ <| mem_insert_self _ _).symm.dvd ih
  simp_rw [← biUnion_image_left, disjoint_biUnion_right, not_forall] at h
  obtain ⟨b, hb, h⟩ := h
  rwa [union_eq_right.2]
  exact (hs.eq (Set.mem_image_of_mem _ <| mem_insert_self _ _)
      (Set.mem_image_of_mem _ <| mem_insert_of_mem hb) h).trans_subset
    (image_subset_image₂_right hb)

Premises used: Iff.mpr, Finset.biUnion_image_left, Finset.image₂_insert_left, Insert.insert, Finset.union_eq_right, Finset.disjoint_biUnion_right, Classical.not_forall