awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
⊢ (Finset.image₂ f s t).Nonempty

Tactic:
image₂_nonempty_iff.2 ⟨hs, ht⟩

Premises used: Iff.mpr, And.intro, Finset.image₂_nonempty_iff
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
h : (Finset.image₂ f s t).Nonempty
⊢ s.Nonempty

Tactic:
(image₂_nonempty_iff.1 h).1

Premises used: And.left, Iff.mp, Finset.image₂_nonempty_iff
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
h : (Finset.image₂ f s t).Nonempty
⊢ t.Nonempty

Tactic:
(image₂_nonempty_iff.1 h).2

Premises used: And.right, Iff.mp, Finset.image₂_nonempty_iff
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
t : Finset β
⊢ (↑(image₂ f ∅ t) : Set γ) = (↑∅ : Set γ)

Tactic:
simp
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
⊢ (↑(image₂ f s ∅) : Set γ) = (↑∅ : Set γ)

Tactic:
simp
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
contrapose! : (image₂ f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
⊢ image₂ f s t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
contrapose!
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ (image₂ f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
image₂_nonempty_iff

Premises used: Finset.image₂_nonempty_iff
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ (image₂ f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
exact image₂_nonempty_iff

Premises used: Finset.image₂_nonempty_iff
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
t : Finset β
a : α
x : γ
⊢ x ∈ image₂ f {a} t ↔ Membership.mem (γ := Finset γ) (image (fun (b : β) ↦ f a b) t) x

Tactic:
simp
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
b : β
x : γ
⊢ x ∈ image₂ f s {b} ↔ Membership.mem (γ := Finset γ) (image (fun (a : α) ↦ f a b) s) x

Tactic:
simp
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
t : Finset β
a : α
⊢ image₂ f {a} t = image (f a) t

Tactic:
image₂_singleton_left

Premises used: Finset.image₂_singleton_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
a : α
b : β
⊢ image₂ f {a} {b} = {f a b}

Tactic:
simp
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst_1 : DecidableEq α
push_cast :
  image2 f ((↑s : Set α) ∪ (↑s' : Set α)) (↑t : Set β) =
    image2 f (↑s : Set α) (↑t : Set β) ∪ image2 f (↑s' : Set α) (↑t : Set β)
⊢ (↑(image₂ f (s ∪ s') t) : Set γ) = (↑(image₂ f s t ∪ image₂ f s' t) : Set γ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst_1 : DecidableEq α
⊢ image2 f ((↑s : Set α) ∪ (↑s' : Set α)) (↑t : Set β) =
    image2 f (↑s : Set α) (↑t : Set β) ∪ image2 f (↑s' : Set α) (↑t : Set β)

Tactic:
image2_union_left

Premises used: Set.image2_union_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst_1 : DecidableEq α
⊢ image2 f ((↑s : Set α) ∪ (↑s' : Set α)) (↑t : Set β) =
    image2 f (↑s : Set α) (↑t : Set β) ∪ image2 f (↑s' : Set α) (↑t : Set β)

Tactic:
exact image2_union_left

Premises used: Set.image2_union_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst_1 : DecidableEq β
push_cast :
  image2 f (↑s : Set α) ((↑t : Set β) ∪ (↑t' : Set β)) =
    image2 f (↑s : Set α) (↑t : Set β) ∪ image2 f (↑s : Set α) (↑t' : Set β)
⊢ (↑(image₂ f s (t ∪ t')) : Set γ) = (↑(image₂ f s t ∪ image₂ f s t') : Set γ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst_1 : DecidableEq β
⊢ image2 f (↑s : Set α) ((↑t : Set β) ∪ (↑t' : Set β)) =
    image2 f (↑s : Set α) (↑t : Set β) ∪ image2 f (↑s : Set α) (↑t' : Set β)

Tactic:
image2_union_right

Premises used: Set.image2_union_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst_1 : DecidableEq β
⊢ image2 f (↑s : Set α) ((↑t : Set β) ∪ (↑t' : Set β)) =
    image2 f (↑s : Set α) (↑t : Set β) ∪ image2 f (↑s : Set α) (↑t' : Set β)

Tactic:
exact image2_union_right

Premises used: Set.image2_union_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
inst_1 : DecidableEq α
push_cast :
  image2 f (insert a (↑s : Set α)) (↑t : Set β) =
    (fun (b : β) ↦ f a b) '' (↑t : Set β) ∪ image2 f (↑s : Set α) (↑t : Set β)
⊢ (↑(image₂ f (insert a s) t) : Set γ) = (↑(image (fun (b : β) ↦ f a b) t ∪ image₂ f s t) : Set γ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
inst_1 : DecidableEq α
⊢ image2 f (insert a (↑s : Set α)) (↑t : Set β) =
    (fun (b : β) ↦ f a b) '' (↑t : Set β) ∪ image2 f (↑s : Set α) (↑t : Set β)

Tactic:
image2_insert_left

Premises used: Set.image2_insert_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
inst_1 : DecidableEq α
⊢ image2 f (insert a (↑s : Set α)) (↑t : Set β) =
    (fun (b : β) ↦ f a b) '' (↑t : Set β) ∪ image2 f (↑s : Set α) (↑t : Set β)

Tactic:
exact image2_insert_left

Premises used: Set.image2_insert_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
b : β
inst_1 : DecidableEq β
push_cast :
  image2 f (↑s : Set α) (insert b (↑t : Set β)) =
    (fun (a : α) ↦ f a b) '' (↑s : Set α) ∪ image2 f (↑s : Set α) (↑t : Set β)
⊢ (↑(image₂ f s (insert b t)) : Set γ) = (↑(image (fun (a : α) ↦ f a b) s ∪ image₂ f s t) : Set γ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
b : β
inst_1 : DecidableEq β
⊢ image2 f (↑s : Set α) (insert b (↑t : Set β)) =
    (fun (a : α) ↦ f a b) '' (↑s : Set α) ∪ image2 f (↑s : Set α) (↑t : Set β)

Tactic:
image2_insert_right

Premises used: Set.image2_insert_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
b : β
inst_1 : DecidableEq β
⊢ image2 f (↑s : Set α) (insert b (↑t : Set β)) =
    (fun (a : α) ↦ f a b) '' (↑s : Set α) ∪ image2 f (↑s : Set α) (↑t : Set β)

Tactic:
exact image2_insert_right

Premises used: Set.image2_insert_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst_1 : DecidableEq α
hf : Injective2 f
push_cast :
  image2 f ((↑s : Set α) ∩ (↑s' : Set α)) (↑t : Set β) =
    image2 f (↑s : Set α) (↑t : Set β) ∩ image2 f (↑s' : Set α) (↑t : Set β)
⊢ (↑(image₂ f (s ∩ s') t) : Set γ) = (↑(image₂ f s t ∩ image₂ f s' t) : Set γ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst_1 : DecidableEq α
hf : Injective2 f
⊢ image2 f ((↑s : Set α) ∩ (↑s' : Set α)) (↑t : Set β) =
    image2 f (↑s : Set α) (↑t : Set β) ∩ image2 f (↑s' : Set α) (↑t : Set β)

Tactic:
image2_inter_left hf

Premises used: Set.image2_inter_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst_1 : DecidableEq α
hf : Injective2 f
⊢ image2 f ((↑s : Set α) ∩ (↑s' : Set α)) (↑t : Set β) =
    image2 f (↑s : Set α) (↑t : Set β) ∩ image2 f (↑s' : Set α) (↑t : Set β)

Tactic:
exact image2_inter_left hf

Premises used: Set.image2_inter_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst_1 : DecidableEq β
hf : Injective2 f
push_cast :
  image2 f (↑s : Set α) ((↑t : Set β) ∩ (↑t' : Set β)) =
    image2 f (↑s : Set α) (↑t : Set β) ∩ image2 f (↑s : Set α) (↑t' : Set β)
⊢ (↑(image₂ f s (t ∩ t')) : Set γ) = (↑(image₂ f s t ∩ image₂ f s t') : Set γ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst_1 : DecidableEq β
hf : Injective2 f
⊢ image2 f (↑s : Set α) ((↑t : Set β) ∩ (↑t' : Set β)) =
    image2 f (↑s : Set α) (↑t : Set β) ∩ image2 f (↑s : Set α) (↑t' : Set β)

Tactic:
image2_inter_right hf

Premises used: Set.image2_inter_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst_1 : DecidableEq β
hf : Injective2 f
⊢ image2 f (↑s : Set α) ((↑t : Set β) ∩ (↑t' : Set β)) =
    image2 f (↑s : Set α) (↑t : Set β) ∩ image2 f (↑s : Set α) (↑t' : Set β)

Tactic:
exact image2_inter_right hf

Premises used: Set.image2_inter_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst_1 : DecidableEq α
push_cast :
  image2 f ((↑s : Set α) ∩ (↑s' : Set α)) (↑t : Set β) ⊆
    image2 f (↑s : Set α) (↑t : Set β) ∩ image2 f (↑s' : Set α) (↑t : Set β)
⊢ (↑(image₂ f (s ∩ s') t) : Set γ) ⊆ (↑(image₂ f s t ∩ image₂ f s' t) : Set γ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst_1 : DecidableEq α
⊢ image2 f ((↑s : Set α) ∩ (↑s' : Set α)) (↑t : Set β) ⊆
    image2 f (↑s : Set α) (↑t : Set β) ∩ image2 f (↑s' : Set α) (↑t : Set β)

Tactic:
image2_inter_subset_left

Premises used: Set.image2_inter_subset_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst_1 : DecidableEq α
⊢ image2 f ((↑s : Set α) ∩ (↑s' : Set α)) (↑t : Set β) ⊆
    image2 f (↑s : Set α) (↑t : Set β) ∩ image2 f (↑s' : Set α) (↑t : Set β)

Tactic:
exact image2_inter_subset_left

Premises used: Set.image2_inter_subset_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst_1 : DecidableEq β
push_cast :
  image2 f (↑s : Set α) ((↑t : Set β) ∩ (↑t' : Set β)) ⊆
    image2 f (↑s : Set α) (↑t : Set β) ∩ image2 f (↑s : Set α) (↑t' : Set β)
⊢ (↑(image₂ f s (t ∩ t')) : Set γ) ⊆ (↑(image₂ f s t ∩ image₂ f s t') : Set γ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst_1 : DecidableEq β
⊢ image2 f (↑s : Set α) ((↑t : Set β) ∩ (↑t' : Set β)) ⊆
    image2 f (↑s : Set α) (↑t : Set β) ∩ image2 f (↑s : Set α) (↑t' : Set β)

Tactic:
image2_inter_subset_right

Premises used: Set.image2_inter_subset_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst_1 : DecidableEq β
⊢ image2 f (↑s : Set α) ((↑t : Set β) ∩ (↑t' : Set β)) ⊆
    image2 f (↑s : Set α) (↑t : Set β) ∩ image2 f (↑s : Set α) (↑t' : Set β)

Tactic:
exact image2_inter_subset_right

Premises used: Set.image2_inter_subset_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f f' : α → β → γ
s : Finset α
t : Finset β
h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b
push_cast : image2 f (↑s : Set α) (↑t : Set β) = image2 f' (↑s : Set α) (↑t : Set β)
⊢ (↑(image₂ f s t) : Set γ) = (↑(image₂ f' s t) : Set γ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f f' : α → β → γ
s : Finset α
t : Finset β
h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b
⊢ image2 f (↑s : Set α) (↑t : Set β) = image2 f' (↑s : Set α) (↑t : Set β)

Tactic:
image2_congr h

Premises used: Set.image2_congr
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f f' : α → β → γ
s : Finset α
t : Finset β
h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b
⊢ image2 f (↑s : Set α) (↑t : Set β) = image2 f' (↑s : Set α) (↑t : Set β)

Tactic:
exact image2_congr h

Premises used: Set.image2_congr
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f f' : α → β → γ
s : Finset α
t : Finset β
h : ∀ (a : α) (b : β), f a b = f' a b
⊢ image₂ f s t = image₂ f' s t

Tactic:
image₂_congr fun a _ b _ => h a b

Premises used: Finset.image₂_congr
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
t : Finset β
a : α
hf : Injective (f a)
rw : card.{u_5} (α := γ) (image (fun (b : β) ↦ f a b) t) = #t
rw₁ rw₂ : #t = #t
⊢ #(image₂ f {a} t) = #t

Tactic:
rw [image₂_singleton_left, card_image_of_injective _ hf]

Premises used: Finset.card_image_of_injective, Finset.image₂_singleton_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
b : β
hf : Injective.{u_1 + 1, u_5 + 1} (β := γ) fun (a : α) ↦ f a b
rw : card.{u_5} (α := γ) (image (fun (a : α) ↦ f a b) s) = #s
rw₁ rw₂ : #s = #s
⊢ #(image₂ f s {b}) = #s

Tactic:
rw [image₂_singleton_right, card_image_of_injective _ hf]

Premises used: Finset.card_image_of_injective, Finset.image₂_singleton_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
a : α
inst_1 : DecidableEq β
t₁ t₂ : Finset β
hf : Injective (f a)
simp_rw :
  Eq.{u_5 + 1} (α := Finset γ) (image (fun (b : β) ↦ f a b) (t₁ ∩ t₂))
    (image (fun (b : β) ↦ f a b) t₁ ∩ image (fun (b : β) ↦ f a b) t₂)
⊢ image₂ f {a} (t₁ ∩ t₂) = image₂ f {a} t₁ ∩ image₂ f {a} t₂

Tactic:
simp_rw [image₂_singleton_left, image_inter _ _ hf]

Premises used: Finset.image_inter, Finset.image₂_singleton_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
b : β
inst_1 : DecidableEq α
s₁ s₂ : Finset α
hf : Injective.{u_1 + 1, u_5 + 1} (β := γ) fun (a : α) ↦ f a b
simp_rw :
  Eq.{u_5 + 1} (α := Finset γ) (image (fun (a : α) ↦ f a b) (s₁ ∩ s₂))
    (image (fun (a : α) ↦ f a b) s₁ ∩ image (fun (a : α) ↦ f a b) s₂)
⊢ image₂ f (s₁ ∩ s₂) {b} = image₂ f s₁ {b} ∩ image₂ f s₂ {b}

Tactic:
simp_rw [image₂_singleton_right, image_inter _ _ hf]

Premises used: Finset.image_inter, Finset.image₂_singleton_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
t : Finset β
a : α
s : Finset α
ha : a ∈ s
hf : Injective (f a)
⊢ #t ≤ #(image₂ f s t)

Tactic:
card_le_card_of_injOn (f a) (fun _ hb ↦ mem_image₂_of_mem ha hb) hf.injOn

Premises used: Function.Injective.injOn, Finset.card_le_card_of_injOn, Finset.mem_image₂_of_mem
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
b : β
t : Finset β
hb : b ∈ t
hf : Injective.{u_1 + 1, u_5 + 1} (β := γ) fun (x : α) ↦ f x b
⊢ #s ≤ #(image₂ f s t)

Tactic:
card_le_card_of_injOn (f · b) (fun _ ha ↦ mem_image₂_of_mem ha hb) hf.injOn

Premises used: Function.Injective.injOn, Finset.card_le_card_of_injOn, Finset.mem_image₂_of_mem
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
push_cast : ⋃ x ∈ (↑s : Set α), f x '' (↑t : Set β) = image2 f (↑s : Set α) (↑t : Set β)
⊢ (↑(s.biUnion fun (a : α) ↦ image (f a) t) : Set γ) = (↑(image₂ f s t) : Set γ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ ⋃ x ∈ (↑s : Set α), f x '' (↑t : Set β) = image2 f (↑s : Set α) (↑t : Set β)

Tactic:
Set.iUnion_image_left _

Premises used: Set.iUnion_image_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ ⋃ x ∈ (↑s : Set α), f x '' (↑t : Set β) = image2 f (↑s : Set α) (↑t : Set β)

Tactic:
exact Set.iUnion_image_left _

Premises used: Set.iUnion_image_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
push_cast : ⋃ x ∈ (↑t : Set β), (fun (a : α) ↦ f a x) '' (↑s : Set α) = image2 f (↑s : Set α) (↑t : Set β)
⊢ (↑(t.biUnion fun (b : β) ↦ image (fun (a : α) ↦ f a b) s) : Set γ) = (↑(image₂ f s t) : Set γ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ ⋃ x ∈ (↑t : Set β), (fun (a : α) ↦ f a x) '' (↑s : Set α) = image2 f (↑s : Set α) (↑t : Set β)

Tactic:
Set.iUnion_image_right _

Premises used: Set.iUnion_image_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ ⋃ x ∈ (↑t : Set β), (fun (a : α) ↦ f a x) '' (↑s : Set α) = image2 f (↑s : Set α) (↑t : Set β)

Tactic:
exact Set.iUnion_image_right _

Premises used: Set.iUnion_image_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
s : Finset α
t : Finset β
inst_1 : DecidableEq δ
f : α → β → γ
g : γ → δ
push_cast : g '' image2 f (↑s : Set α) (↑t : Set β) = image2 (fun (a : α) (b : β) ↦ g (f a b)) (↑s : Set α) (↑t : Set β)
⊢ (↑(image g (image₂ f s t)) : Set δ) = (↑(image₂ (fun (a : α) (b : β) ↦ g (f a b)) s t) : Set δ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
s : Finset α
t : Finset β
inst_1 : DecidableEq δ
f : α → β → γ
g : γ → δ
⊢ g '' image2 f (↑s : Set α) (↑t : Set β) = image2 (fun (a : α) (b : β) ↦ g (f a b)) (↑s : Set α) (↑t : Set β)

Tactic:
image_image2 _ _

Premises used: Set.image_image2
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
s : Finset α
t : Finset β
inst_1 : DecidableEq δ
f : α → β → γ
g : γ → δ
⊢ g '' image2 f (↑s : Set α) (↑t : Set β) = image2 (fun (a : α) (b : β) ↦ g (f a b)) (↑s : Set α) (↑t : Set β)

Tactic:
exact image_image2 _ _

Premises used: Set.image_image2
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
s : Finset α
t : Finset β
inst_1 : DecidableEq δ
f : γ → β → δ
g : α → γ
push_cast :
  image2 f (g '' (↑s : Set α)) (↑t : Set β) = image2 (fun (a : α) (b : β) ↦ f (g a) b) (↑s : Set α) (↑t : Set β)
⊢ (↑(image₂ f (image g s) t) : Set δ) = (↑(image₂ (fun (a : α) (b : β) ↦ f (g a) b) s t) : Set δ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
s : Finset α
t : Finset β
inst_1 : DecidableEq δ
f : γ → β → δ
g : α → γ
⊢ image2 f (g '' (↑s : Set α)) (↑t : Set β) = image2 (fun (a : α) (b : β) ↦ f (g a) b) (↑s : Set α) (↑t : Set β)

Tactic:
image2_image_left _ _

Premises used: Set.image2_image_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
s : Finset α
t : Finset β
inst_1 : DecidableEq δ
f : γ → β → δ
g : α → γ
⊢ image2 f (g '' (↑s : Set α)) (↑t : Set β) = image2 (fun (a : α) (b : β) ↦ f (g a) b) (↑s : Set α) (↑t : Set β)

Tactic:
exact image2_image_left _ _

Premises used: Set.image2_image_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
s : Finset α
t : Finset β
inst_1 : DecidableEq δ
f : α → γ → δ
g : β → γ
push_cast :
  image2 f (↑s : Set α) (g '' (↑t : Set β)) = image2 (fun (a : α) (b : β) ↦ f a (g b)) (↑s : Set α) (↑t : Set β)
⊢ (↑(image₂ f s (image g t)) : Set δ) = (↑(image₂ (fun (a : α) (b : β) ↦ f a (g b)) s t) : Set δ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
s : Finset α
t : Finset β
inst_1 : DecidableEq δ
f : α → γ → δ
g : β → γ
⊢ image2 f (↑s : Set α) (g '' (↑t : Set β)) = image2 (fun (a : α) (b : β) ↦ f a (g b)) (↑s : Set α) (↑t : Set β)

Tactic:
image2_image_right _ _

Premises used: Set.image2_image_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
s : Finset α
t : Finset β
inst_1 : DecidableEq δ
f : α → γ → δ
g : β → γ
⊢ image2 f (↑s : Set α) (g '' (↑t : Set β)) = image2 (fun (a : α) (b : β) ↦ f a (g b)) (↑s : Set α) (↑t : Set β)

Tactic:
exact image2_image_right _ _

Premises used: Set.image2_image_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
s : Finset α
t : Finset β
h : ∀ (a : α × β), a ∈ image₂ Prod.mk s t ↔ a ∈ s ×ˢ t
⊢ image₂ Prod.mk s t = s ×ˢ t

Tactic:
ext
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
s : Finset α
t : Finset β
a : α × β
⊢ a ∈ image₂ Prod.mk s t ↔ a ∈ s ×ˢ t

Tactic:
simp [Prod.ext_iff]

Premises used: Prod.ext_iff
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α × β → γ
s : Finset α
t : Finset β
⊢ image₂ (curry f) s t = image f (s ×ˢ t)

Tactic:
rfl

Premises used: rfl, Finset.image₂
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ image (uncurry f) (s ×ˢ t) = image₂ f s t

Tactic:
rfl

Premises used: rfl, Finset.image₂
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
push_cast : image2 f (↑s : Set α) (↑t : Set β) = image2 (fun (a : β) (b : α) ↦ f b a) (↑t : Set β) (↑s : Set α)
⊢ (↑(image₂ f s t) : Set γ) = (↑(image₂ (fun (a : β) (b : α) ↦ f b a) t s) : Set γ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ image2 f (↑s : Set α) (↑t : Set β) = image2 (fun (a : β) (b : α) ↦ f b a) (↑t : Set β) (↑s : Set α)

Tactic:
image2_swap _ _ _

Premises used: Set.image2_swap
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ image2 f (↑s : Set α) (↑t : Set β) = image2 (fun (a : β) (b : α) ↦ f b a) (↑t : Set β) (↑s : Set α)

Tactic:
exact image2_swap _ _ _

Premises used: Set.image2_swap
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
s : Finset α
t : Finset β
inst : DecidableEq α
h : t.Nonempty
push_cast : image2 (fun (x : α) (x_1 : β) ↦ x) (↑s : Set α) (↑t : Set β) = (↑s : Set α)
⊢ (↑(image₂ (fun (x : α) (x_1 : β) ↦ x) s t) : Set α) = (↑s : Set α)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
s : Finset α
t : Finset β
inst : DecidableEq α
h : t.Nonempty
⊢ image2 (fun (x : α) (x_1 : β) ↦ x) (↑s : Set α) (↑t : Set β) = (↑s : Set α)

Tactic:
image2_left h

Premises used: Set.image2_left