-- Mathlib/Data/Finset/NAry.lean
theorem card_dvd_card_image₂_right (hf : ∀ a ∈ s, Injective (f a))
    (hs : ((fun a => t.image <| f a) '' s).PairwiseDisjoint id) : #t ∣ #(image₂ f s t)

Proof state:
case neg.intro.intro
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a => image (f a) t) '' ↑(insert a s)).PairwiseDisjoint 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

Tactic:
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)

Result:
no goals

Proof state:
case insert
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : (∀ a ∈ s, Injective (f a)) → ((fun a => image (f a) t) '' ↑s).PairwiseDisjoint id → #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a => image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
⊢ #t ∣ #(image₂ f (insert a s) t)

Tactic:
specialize ih (forall_of_forall_insert hf)
  (hs.subset <| Set.image_subset _ <| coe_subset.2 <| subset_insert _ _)

Result:
case insert
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a => image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
ih : #t ∣ #(image₂ f s t)
⊢ #t ∣ #(image₂ f (insert a s) t)

Proof state:
case empty
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ a ∈ ∅, Injective (f a)
hs : ((fun a => image (f a) t) '' ↑∅).PairwiseDisjoint id
⊢ #t ∣ #(image₂ f ∅ t)

Tactic:
simp

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a => image (f a) t) '' ↑(insert a s)).PairwiseDisjoint 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)

Tactic:
simp_rw [← biUnion_image_left, disjoint_biUnion_right, not_forall] at h

Result:
case neg
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a => image (f a) t) '' ↑(insert a s)).PairwiseDisjoint 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)

Proof state:
case neg.intro.intro
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a => image (f a) t) '' ↑(insert a s)).PairwiseDisjoint 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)

Tactic:
rwa [union_eq_right.2]

Result:
case neg.intro.intro
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a => image (f a) t) '' ↑(insert a s)).PairwiseDisjoint 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

Proof state:
case pos
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a => image (f a) t) '' ↑(insert a s)).PairwiseDisjoint 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)

Tactic:
rw [card_union_of_disjoint h]

Result:
case pos
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a => image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
ih : #t ∣ #(image₂ f s t)
h : Disjoint (image (f a) t) (image₂ f s t)
⊢ #t ∣ #(image (f a) t) + #(image₂ f s t)

Proof state:
case pos
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a => image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
ih : #t ∣ #(image₂ f s t)
h : Disjoint (image (f a) t) (image₂ f s t)
⊢ #t ∣ #(image (f a) t) + #(image₂ f s t)

Tactic:
exact Nat.dvd_add (card_image_of_injective _ <| hf _ <| mem_insert_self _ _).symm.dvd ih

Result:
no goals

Proof state:
case insert
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a => image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
ih : #t ∣ #(image₂ f s t)
⊢ #t ∣ #(image (fun b => f a b) t ∪ image₂ f s t)

Tactic:
by_cases h : Disjoint (image (f a) t) (image₂ f s t)

Result:
case pos
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a => image (f a) t) '' ↑(insert a s)).PairwiseDisjoint 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)

case neg
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a => image (f a) t) '' ↑(insert a s)).PairwiseDisjoint 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)

Proof state:
case insert
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a => image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
ih : #t ∣ #(image₂ f s t)
⊢ #t ∣ #(image₂ f (insert a s) t)

Tactic:
rw [image₂_insert_left]

Result:
case insert
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a => image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
ih : #t ∣ #(image₂ f s t)
⊢ #t ∣ #(image (fun b => f a b) t ∪ image₂ f s t)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ a ∈ s, Injective (f a)
hs : ((fun a => image (f a) t) '' ↑s).PairwiseDisjoint id
⊢ #t ∣ #(image₂ f s t)

Tactic:
induction' s using Finset.induction with a s _ ih

Result:
case empty
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ a ∈ ∅, Injective (f a)
hs : ((fun a => image (f a) t) '' ↑∅).PairwiseDisjoint id
⊢ #t ∣ #(image₂ f ∅ t)

case insert
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : (∀ a ∈ s, Injective (f a)) → ((fun a => image (f a) t) '' ↑s).PairwiseDisjoint id → #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a => image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
⊢ #t ∣ #(image₂ f (insert a s) t)