awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
δ : Type u_7
ε : Type u_9
ε' : Type u_10
inst : DecidableEq ε
inst_1 : DecidableEq ε'
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
⊢ (↑(image₂ f (image₂ g s t) u) : Set ε) = (↑(image₂ f' s (image₂ g' t u)) : Set ε)
have push_cast : image2 f (image2 g (↑s : Set α) (↑t : Set β)) (↑u : Set γ) =
  image2 f' (↑s : Set α) (image2 g' (↑t : Set β) (↑u : Set γ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
δ : Type u_7
δ' : Type u_8
ε : Type u_9
inst : DecidableEq δ'
inst_1 : DecidableEq ε
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
γ : Type u_14
u : Finset γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ (↑(image₂ f s (image₂ g t u)) : Set ε) = (↑(image₂ g' t (image₂ f' s u)) : Set ε)
have push_cast : image2 f (↑s : Set α) (image2 g (↑t : Set β) (↑u : Set γ)) =
  image2 g' (↑t : Set β) (image2 f' (↑s : Set α) (↑u : Set γ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
δ : Type u_7
δ' : Type u_8
ε : Type u_9
inst : DecidableEq δ'
inst_1 : DecidableEq ε
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ (↑(image₂ f (image₂ g s t) u) : Set ε) = (↑(image₂ g' (image₂ f' s u) t) : Set ε)
have push_cast : image2 f (image2 g (↑s : Set α) (↑t : Set β)) (↑u : Set γ) =
  image2 g' (image2 f' (↑s : Set α) (↑u : Set γ)) (↑t : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
inst : DecidableEq ε
inst_1 : DecidableEq ε'
s : Finset α
t : Finset β
γ : Type u_14
δ : Type u_15
u : Finset γ
v : Finset δ
inst_2 : DecidableEq ζ
inst_3 : DecidableEq ζ'
inst_4 : DecidableEq ν
f : ε → ζ → ν
g : α → β → ε
h : γ → δ → ζ
f' : ε' → ζ' → ν
g' : α → γ → ε'
h' : β → δ → ζ'
h_comm : ∀ (a : α) (b : β) (c : γ) (d : δ), f (g a b) (h c d) = f' (g' a c) (h' b d)
⊢ (↑(image₂ f (image₂ g s t) (image₂ h u v)) : Set ν) = (↑(image₂ f' (image₂ g' s u) (image₂ h' t v)) : Set ν)
have push_cast : image2 f (image2 g (↑s : Set α) (↑t : Set β)) (image2 h (↑u : Set γ) (↑v : Set δ)) =
  image2 f' (image2 g' (↑s : Set α) (↑u : Set γ)) (image2 h' (↑t : Set β) (↑v : Set δ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst : DecidableEq α'
inst_1 : DecidableEq β'
inst_2 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_3 : DecidableEq δ
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ (↑(image g (image₂ f s t)) : Set δ) = (↑(image₂ f' (image g₁ s) (image g₂ t)) : Set δ)
have push_cast : g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (g₁ '' (↑s : Set α)) (g₂ '' (↑t : Set β))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq α'
inst_1 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
⊢ (↑(image g (image₂ f s t)) : Set δ) = (↑(image₂ f' (image g' s) t) : Set δ)
have push_cast : g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (g' '' (↑s : Set α)) (↑t : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst : DecidableEq β'
inst_1 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
⊢ (↑(image g (image₂ f s t)) : Set δ) = (↑(image₂ f' s (image g' t)) : Set δ)
have push_cast : g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (↑s : Set α) (g' '' (↑t : Set β))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ' : Type u_6
δ : Type u_7
ε : Type u_9
inst : DecidableEq β'
inst_1 : DecidableEq γ'
inst_2 : DecidableEq ε
s : Finset α
t : Finset β
inst_3 : DecidableEq δ
γ : Type u_14
u : Finset γ
f : α → δ → ε
g : β → γ → δ
f₁ : α → β → β'
f₂ : α → γ → γ'
g' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)
⊢ (↑(image₂ f s (image₂ g t u)) : Set ε) ⊆ (↑(image₂ g' (image₂ f₁ s t) (image₂ f₂ s u)) : Set ε)
have push_cast : image2 f (↑s : Set α) (image2 g (↑t : Set β) (↑u : Set γ)) ⊆
  image2 g' (image2 f₁ (↑s : Set α) (↑t : Set β)) (image2 f₂ (↑s : Set α) (↑u : Set γ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
δ : Type u_7
ε : Type u_9
inst : DecidableEq α'
inst_1 : DecidableEq β'
inst_2 : DecidableEq ε
s : Finset α
t : Finset β
inst_3 : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f₁ : α → γ → α'
f₂ : β → γ → β'
g' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)
⊢ (↑(image₂ f (image₂ g s t) u) : Set ε) ⊆ (↑(image₂ g' (image₂ f₁ s u) (image₂ f₂ t u)) : Set ε)
have push_cast : image2 f (image2 g (↑s : Set α) (↑t : Set β)) (↑u : Set γ) ⊆
  image2 g' (image2 f₁ (↑s : Set α) (↑u : Set γ)) (image2 f₂ (↑t : Set β) (↑u : Set γ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst : DecidableEq α'
inst_1 : DecidableEq β'
inst_2 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_3 : DecidableEq δ
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ image g (image₂ f s t) = image₂ f' (image g₁ t) (image g₂ s)
have rw : image g (image₂ (fun (a : β) (b : α) ↦ f b a) t s) = image₂ f' (image g₁ t) (image g₂ s)
Tactic: rw [image₂_swap f]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst : DecidableEq β'
inst_1 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
⊢ (↑(image g (image₂ f s t)) : Set δ) = (↑(image₂ f' (image g' t) s) : Set δ)
have push_cast : g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (g' '' (↑t : Set β)) (↑s : Set α)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq α'
inst_1 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
⊢ (↑(image g (image₂ f s t)) : Set δ) = (↑(image₂ f' t (image g' s)) : Set δ)
have push_cast : g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (↑t : Set β) (g' '' (↑s : Set α))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
γ : Type u_5
inst : DecidableEq γ
f : α → γ → γ
a : α
h : ∀ (b : γ), f a b = b
t : Finset γ
⊢ (↑(image₂ f {a} t) : Set γ) = (↑t : Set γ)
have rw : image2 f (↑{a} : Set α) (↑t : Set γ) = (↑t : Set γ)
Tactic: rw [coe_image₂, coe_singleton, Set.image2_left_identity h]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
γ : Type u_5
inst : DecidableEq γ
f : α → γ → γ
a : α
h : ∀ (b : γ), f a b = b
t : Finset γ
rw : image2 f (↑{a} : Set α) (↑t : Set γ) = (↑t : Set γ)
⊢ (↑(image₂ f {a} t) : Set γ) = (↑t : Set γ)
have rw₁ : image2 f {a} (↑t : Set γ) = (↑t : Set γ)
Tactic: rw [coe_image₂, coe_singleton, Set.image2_left_identity h]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
γ : Type u_5
inst : DecidableEq γ
f : α → γ → γ
a : α
h : ∀ (b : γ), f a b = b
t : Finset γ
rw : image2 f (↑{a} : Set α) (↑t : Set γ) = (↑t : Set γ)
rw₁ : image2 f {a} (↑t : Set γ) = (↑t : Set γ)
⊢ (↑(image₂ f {a} t) : Set γ) = (↑t : Set γ)
have rw₂ : (↑t : Set γ) = (↑t : Set γ)
Tactic: rw [coe_image₂, coe_singleton, Set.image2_left_identity h]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : γ → β → γ
b : β
h : ∀ (a : γ), f a b = a
s : Finset γ
⊢ image₂ f s {b} = s
have rw : image (fun (a : γ) ↦ f a b) s = s
Tactic: rw [image₂_singleton_right, funext h, image_id']
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : γ → β → γ
b : β
h : ∀ (a : γ), f a b = a
s : Finset γ
rw : image (fun (a : γ) ↦ f a b) s = s
⊢ image₂ f s {b} = s
have rw₁ : image (fun (x : γ) ↦ x) s = s
Tactic: rw [image₂_singleton_right, funext h, image_id']
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : γ → β → γ
b : β
h : ∀ (a : γ), f a b = a
s : Finset γ
rw : image (fun (a : γ) ↦ f a b) s = s
rw₁ : image (fun (x : γ) ↦ x) s = s
⊢ image₂ f s {b} = s
have rw₂ : s = s
Tactic: rw [image₂_singleton_right, funext h, image_id']
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
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
⊢ #t ∣ #(image₂ f s t)
have 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 a s, Injective (f a_2))
      (hs : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(insert a s) : Set α)) id),
      #t ∣ #(image₂ f (insert a s) t)
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert a s _ ih => ?_
Cleared hypotheses: hf, hs
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (hypothesis)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s_1 : Finset α
t : Finset β
a : α
s : Finset α
h : 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_1 ∈ insert a s, Injective (f a_1)
hs : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(insert a s) : Set α)) id
⊢ #t ∣ #(image₂ f (insert a s) t)
have ih₁ : #t ∣ #(image₂ f s t)
Tactic: specialize ih (forall_of_forall_insert hf)
    (hs.subset <| Set.image_mono <| coe_subset.2 <| subset_insert _ _)
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s_1 : Finset α
t : Finset β
a : α
s : Finset α
h : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(insert a s) : Set α)) id
ih : #t ∣ #(image₂ f s t)
⊢ #t ∣ #(image₂ f (insert a s) t)
have insert : #t ∣ #(image (fun (b : β) ↦ f a b) t ∪ image₂ f s t)
Tactic: rw [image₂_insert_left]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s_1 : Finset α
t : Finset β
a : α
s : Finset α
h : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(insert a s) : Set α)) id
ih : #t ∣ #(image₂ f s t)
⊢ #t ∣ #(image (fun (b : β) ↦ f a b) t ∪ image₂ f s t)
have pos : ∀ (h : Disjoint (image (f a) 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)
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s_1 : Finset α
t : Finset β
a : α
s : Finset α
h : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(insert a s) : Set α)) id
ih : #t ∣ #(image₂ f s t)
pos : ∀ (h : Disjoint (image (f a) t) (image₂ f s t)), #t ∣ #(image (fun (b : β) ↦ f a b) t ∪ image₂ f s t)
⊢ #t ∣ #(image (fun (b : β) ↦ f a b) t ∪ image₂ f s t)
have neg : ∀ (h : ¬Disjoint (image (f a) 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)
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s_1 : Finset α
t : Finset β
a : α
s : Finset α
h_1 : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(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)
have pos : #t ∣ #(image (f a) t) + #(image₂ f s t)
Tactic: rw [card_union_of_disjoint h]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (hypothesis)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s_1 : Finset α
t : Finset β
a : α
s : Finset α
h_1 : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(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)
have h₁ : ∃ (x : α) (_ : x ∈ s), ¬Disjoint (image (f a) t) (image (f x) t)
Tactic: simp_rw [← biUnion_image_left, disjoint_biUnion_right, not_forall] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s_1 : Finset α
t : Finset β
a : α
s : Finset α
h_1 : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(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)
have neg : ∀ (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: obtain ⟨b, hb, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s_1 : Finset α
t : Finset β
a : α
s : Finset α
h_1 : a ∉ s
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(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)
have neg : image (fun (b : β) ↦ f a b) t ⊆ image₂ f s t
Tactic: rwa [union_eq_right.2]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
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
⊢ #t ∣ #(image₂ f s t)
have 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)
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)
Cleared hypotheses: hf, hs
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
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)
⊢ #t ∣ #(image₂ f s t)
have 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 a s, Injective (f a_2))
      (hs : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(insert a s) : Set α)) id),
      #t ∣ #(image₂ f (insert a 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)
Cleared hypotheses: hf, hs
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
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)
⊢ #t ∣ #(image₂ f s t)
have 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)
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)
Cleared hypotheses: hf, hs
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
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)
⊢ #t ∣ #(image₂ f s t)
have 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)
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)
Cleared hypotheses: hf, hs