awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.NAry
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 γ)
rw₂ rw₃ : (↑t : Set γ) = (↑t : Set γ)
⊢ (↑(image₂ f {a} t) : Set γ) = (↑t : Set γ)

Tactic:
rw [coe_image₂, coe_singleton, Set.image2_left_identity h]

Premises used: Finset.coe_singleton, Set.image2_left_identity, Finset.coe_image₂
-- Module: Mathlib.Data.Finset.NAry
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
rw₂ rw₃ : s = s
⊢ image₂ f s {b} = s

Tactic:
rw [image₂_singleton_right, funext h, image_id']

Premises used: funext, Finset.image_id', Finset.image₂_singleton_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
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:
simp
-- Module: Mathlib.Data.Finset.NAry
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)

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

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert a s _ ih => ?_

Premises used: Insert.insert
-- Module: Mathlib.Data.Finset.NAry
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 s t)

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

Premises used: Iff.mpr, Finset.forall_of_forall_insert, Set.image_mono, Set.PairwiseDisjoint.subset, Finset.subset_insert, Finset.coe_subset
-- Module: Mathlib.Data.Finset.NAry
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.insert a s, Injective (f a_1)
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)
insert : #t ∣ #(image (fun (b : β) ↦ f a b) t ∪ image₂ f s t)
⊢ #t ∣ #(image₂ f (Insert.insert a s) t)

Tactic:
rw [image₂_insert_left]

Premises used: Finset.image₂_insert_left
-- Module: Mathlib.Data.Finset.NAry
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)
neg : ∀ (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)

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

Premises used: Disjoint, Finset.image, Finset.image₂
-- Module: Mathlib.Data.Finset.NAry
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)
pos : #t ∣ #(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]

Premises used: Finset.card_union_of_disjoint
-- Module: Mathlib.Data.Finset.NAry
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 (f a) t) + #(image₂ f s t)

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

Premises used: Finset.mem_insert_self, Eq.dvd, Finset.card_image_of_injective, Nat.dvd_add, Eq.symm
-- Module: Mathlib.Data.Finset.NAry
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 (f a) t) + #(image₂ f s t)

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

Premises used: Finset.mem_insert_self, Eq.dvd, Finset.card_image_of_injective, Nat.dvd_add, Eq.symm
-- Module: Mathlib.Data.Finset.NAry
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)
⊢ ∃ (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

Premises used: Finset.biUnion_image_left, Finset.disjoint_biUnion_right, Classical.not_forall
-- Module: Mathlib.Data.Finset.NAry
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)
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)
⊢ #t ∣ #(image (fun (b : β) ↦ f a b) t ∪ image₂ f s t)

Tactic:
obtain ⟨b, hb, h⟩ := h
-- Module: Mathlib.Data.Finset.NAry
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)
neg : image (fun (b : β) ↦ f a b) t ⊆ image₂ f s t
⊢ #t ∣ #(image (fun (b : β) ↦ f a b) t ∪ image₂ f s t)

Tactic:
rwa [union_eq_right.2]

Premises used: Iff.mpr, Finset.union_eq_right
-- Module: Mathlib.Data.Finset.NAry
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)
⊢ image (fun (b : β) ↦ f a b) t ⊆ image₂ f s t

Tactic:
(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: Finset.mem_insert_self, Set.Mem, setOf, Finset.mem_insert_of_mem, Set.mem_image_of_mem, Finset.image_subset_image₂_right, Set.Pairwise.eq, Eq.trans_subset
-- Module: Mathlib.Data.Finset.NAry
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)
⊢ 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)

Premises used: Finset.mem_insert_self, Finset.mem_insert_of_mem, Set.mem_image_of_mem, Finset.image_subset_image₂_right, Set.Pairwise.eq, Eq.trans_subset
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ b ∈ t, Injective.{u_1 + 1, u_5 + 1} (β := γ) fun (a : α) ↦ f a b
ht : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (b : β) ↦ image (fun (a : α) ↦ f a b) s) '' (↑t : Set β)) id
rw : #s ∣ card.{u_5} (α := γ) (image₂ (fun (b : β) (a : α) ↦ f a b) t s)
⊢ #s ∣ #(image₂ f s t)

Tactic:
rw [← image₂_swap]

Premises used: Finset.image₂_swap
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ b ∈ t, Injective.{u_1 + 1, u_5 + 1} (β := γ) fun (a : α) ↦ f a b
ht : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (b : β) ↦ image (fun (a : α) ↦ f a b) s) '' (↑t : Set β)) id
⊢ #s ∣ card.{u_5} (α := γ) (image₂ (fun (b : β) (a : α) ↦ f a b) t s)

Tactic:
card_dvd_card_image₂_right hf ht

Premises used: Finset.card_dvd_card_image₂_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ b ∈ t, Injective.{u_1 + 1, u_5 + 1} (β := γ) fun (a : α) ↦ f a b
ht : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (b : β) ↦ image (fun (a : α) ↦ f a b) s) '' (↑t : Set β)) id
⊢ #s ∣ card.{u_5} (α := γ) (image₂ (fun (b : β) (a : α) ↦ f a b) t s)

Tactic:
exact card_dvd_card_image₂_right hf ht

Premises used: Finset.card_dvd_card_image₂_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
u : Finset γ
s : Set α
t : Set β
hu : (↑u : Set γ) ⊆ image2 f s t
⊢ ∃ (s' : Finset (α × β)), (↑s' : Set (α × β)) ⊆ s ×ˢ t ∧ image (fun (x : α × β) ↦ f x.1 x.2) s' = u

Tactic:
rw [← Set.image_prod, subset_set_image_iff] at hu

Premises used: Set.image_prod, Finset.subset_set_image_iff
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
u : Finset γ
s : Set α
t : Set β
hu : ∃ (s' : Finset (α × β)), (↑s' : Set (α × β)) ⊆ s ×ˢ t ∧ image (fun (x : α × β) ↦ f x.1 x.2) s' = u
rcases :
  ∀ (u : Finset (α × β)) (hu : (↑u : Set (α × β)) ⊆ s ×ˢ t),
    ∃ (s' : Finset α) (t' : Finset β),
      (↑s' : Set α) ⊆ s ∧ (↑t' : Set β) ⊆ t ∧ image (fun (x : α × β) ↦ f x.1 x.2) u ⊆ image₂ f s' t'
⊢ ∃ (s' : Finset α) (t' : Finset β), (↑s' : Set α) ⊆ s ∧ (↑t' : Set β) ⊆ t ∧ u ⊆ image₂ f s' t'

Tactic:
rcases hu with ⟨u, hu, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : (↑u : Set (α × β)) ⊆ s ×ˢ t
h :
  (↑(image Prod.fst u) : Set α) ⊆ s ∧
    (↑(image Prod.snd u) : Set β) ⊆ t ∧
      image (fun (x : α × β) ↦ f x.1 x.2) u ⊆ image₂ f (image Prod.fst u) (image Prod.snd u)
⊢ ∃ (s' : Finset α) (t' : Finset β),
    (↑s' : Set α) ⊆ s ∧ (↑t' : Set β) ⊆ t ∧ image (fun (x : α × β) ↦ f x.1 x.2) u ⊆ image₂ f s' t'

Tactic:
use u.image Prod.fst, u.image Prod.snd

Premises used: Prod.fst, Prod.snd, Finset.image
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : (↑u : Set (α × β)) ⊆ s ×ˢ t
h :
  (↑u : Set (α × β)) ⊆ Prod.fst ⁻¹' s ∧
    (↑u : Set (α × β)) ⊆ Prod.snd ⁻¹' t ∧
      ∀ x ∈ u, Membership.mem (γ := Finset γ) (image₂ (fun (a b : α × β) ↦ f a.1 b.2) u u) (f x.1 x.2)
⊢ (↑(image Prod.fst u) : Set α) ⊆ s ∧
    (↑(image Prod.snd u) : Set β) ⊆ t ∧
      image (fun (x : α × β) ↦ f x.1 x.2) u ⊆ image₂ f (image Prod.fst u) (image Prod.snd u)

Tactic:
simp only [coe_image, Set.image_subset_iff, image₂_image_left, image₂_image_right,
    image_subset_iff]

Premises used: Finset.image₂_image_left, Finset.coe_image, Finset.image_subset_iff, Set.image_subset_iff, Finset.image₂_image_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : (↑u : Set (α × β)) ⊆ s ×ˢ t
⊢ (↑u : Set (α × β)) ⊆ Prod.fst ⁻¹' s ∧
    (↑u : Set (α × β)) ⊆ Prod.snd ⁻¹' t ∧
      ∀ x ∈ u, Membership.mem (γ := Finset γ) (image₂ (fun (a b : α × β) ↦ f a.1 b.2) u u) (f x.1 x.2)

Tactic:
⟨fun _ h ↦ (hu h).1, fun _ h ↦ (hu h).2, fun x hx ↦ mem_image₂_of_mem hx hx⟩

Premises used: Finset.mem_image₂_of_mem, And.right, And.left, And.intro
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : (↑u : Set (α × β)) ⊆ s ×ˢ t
⊢ (↑u : Set (α × β)) ⊆ Prod.fst ⁻¹' s ∧
    (↑u : Set (α × β)) ⊆ Prod.snd ⁻¹' t ∧
      ∀ x ∈ u, Membership.mem (γ := Finset γ) (image₂ (fun (a b : α × β) ↦ f a.1 b.2) u u) (f x.1 x.2)

Tactic:
exact ⟨fun _ h ↦ (hu h).1, fun _ h ↦ (hu h).2, fun x hx ↦ mem_image₂_of_mem hx hx⟩
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : (↑u : Set (α × β)) ⊆ s ×ˢ t
w : Finset α
w₁ : Finset β
h h₁ :
  (↑(image Prod.fst u) : Set α) ⊆ s ∧
    (↑(image Prod.snd u) : Set β) ⊆ t ∧
      image (fun (x : α × β) ↦ f x.1 x.2) u ⊆ image₂ f (image Prod.fst u) (image Prod.snd u)
h₂ :
  (↑u : Set (α × β)) ⊆ Prod.fst ⁻¹' s ∧
    (↑u : Set (α × β)) ⊆ Prod.snd ⁻¹' t ∧
      ∀ x ∈ u, Membership.mem (γ := Finset γ) (image₂ (fun (a b : α × β) ↦ f a.1 b.2) u u) (f x.1 x.2)
⊢ ∃ (s' : Finset α) (t' : Finset β),
    (↑s' : Set α) ⊆ s ∧ (↑t' : Set β) ⊆ t ∧ image (fun (x : α × β) ↦ f x.1 x.2) u ⊆ image₂ f s' t'

Tactic:
classical
  use u.image Prod.fst, u.image Prod.snd
  simp only [coe_image, Set.image_subset_iff, image₂_image_left, image₂_image_right,
    image_subset_iff]
  exact ⟨fun _ h ↦ (hu h).1, fun _ h ↦ (hu h).2, fun x hx ↦ mem_image₂_of_mem hx hx⟩

Premises used: Finset.image₂_image_left, Finset.coe_image, Finset.image_subset_iff, Set.image_subset_iff, Finset.image₂_image_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
inst_1 : DecidableEq α
inst_2 : DecidableEq β
push_cast :
  image2 f ((↑s : Set α) ∩ (↑s' : Set α)) ((↑t : Set β) ∪ (↑t' : Set β)) ⊆
    image2 f (↑s : Set α) (↑t : Set β) ∪ image2 f (↑s' : Set α) (↑t' : Set β)
⊢ (↑(image₂ f (s ∩ 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 s' : Finset α
t t' : Finset β
inst_1 : DecidableEq α
inst_2 : DecidableEq β
⊢ image2 f ((↑s : Set α) ∩ (↑s' : Set α)) ((↑t : Set β) ∪ (↑t' : Set β)) ⊆
    image2 f (↑s : Set α) (↑t : Set β) ∪ image2 f (↑s' : Set α) (↑t' : Set β)

Tactic:
Set.image2_inter_union_subset_union

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

Tactic:
exact Set.image2_inter_union_subset_union

Premises used: Set.image2_inter_union_subset_union
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
inst_1 : DecidableEq α
inst_2 : DecidableEq β
push_cast :
  image2 f ((↑s : Set α) ∪ (↑s' : Set α)) ((↑t : Set β) ∩ (↑t' : Set β)) ⊆
    image2 f (↑s : Set α) (↑t : Set β) ∪ image2 f (↑s' : Set α) (↑t' : Set β)
⊢ (↑(image₂ f (s ∪ 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 s' : Finset α
t t' : Finset β
inst_1 : DecidableEq α
inst_2 : DecidableEq β
⊢ image2 f ((↑s : Set α) ∪ (↑s' : Set α)) ((↑t : Set β) ∩ (↑t' : Set β)) ⊆
    image2 f (↑s : Set α) (↑t : Set β) ∪ image2 f (↑s' : Set α) (↑t' : Set β)

Tactic:
Set.image2_union_inter_subset_union

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

Tactic:
exact Set.image2_union_inter_subset_union

Premises used: Set.image2_union_inter_subset_union
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
push_cast : image2 f ((↑s : Set α) ∩ (↑t : Set α)) ((↑s : Set α) ∪ (↑t : Set α)) ⊆ image2 f (↑s : Set α) (↑t : Set α)
⊢ (↑(image₂ f (s ∩ t) (s ∪ t)) : Set β) ⊆ (↑(image₂ f s t) : Set β)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f ((↑s : Set α) ∩ (↑t : Set α)) ((↑s : Set α) ∪ (↑t : Set α)) ⊆ image2 f (↑s : Set α) (↑t : Set α)

Tactic:
image2_inter_union_subset hf

Premises used: Set.image2_inter_union_subset
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f ((↑s : Set α) ∩ (↑t : Set α)) ((↑s : Set α) ∪ (↑t : Set α)) ⊆ image2 f (↑s : Set α) (↑t : Set α)

Tactic:
exact image2_inter_union_subset hf

Premises used: Set.image2_inter_union_subset
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
push_cast : image2 f ((↑s : Set α) ∪ (↑t : Set α)) ((↑s : Set α) ∩ (↑t : Set α)) ⊆ image2 f (↑s : Set α) (↑t : Set α)
⊢ (↑(image₂ f (s ∪ t) (s ∩ t)) : Set β) ⊆ (↑(image₂ f s t) : Set β)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f ((↑s : Set α) ∪ (↑t : Set α)) ((↑s : Set α) ∩ (↑t : Set α)) ⊆ image2 f (↑s : Set α) (↑t : Set α)

Tactic:
image2_union_inter_subset hf

Premises used: Set.image2_union_inter_subset
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f ((↑s : Set α) ∪ (↑t : Set α)) ((↑s : Set α) ∩ (↑t : Set α)) ⊆ image2 f (↑s : Set α) (↑t : Set α)

Tactic:
exact image2_union_inter_subset hf

Premises used: Set.image2_union_inter_subset
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeSup δ
g : γ → δ
a : δ
h : (image₂ f s t).Nonempty
rw : (∀ b ∈ image₂ f s t, g b ≤ a) ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
rw₁ rw₂ : (∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a) ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
⊢ (image₂ f s t).sup' h g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a

Tactic:
rw [sup'_le_iff, forall_mem_image₂]

Premises used: Finset.forall_mem_image₂, Finset.sup'_le_iff
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
simp :
  Eq.{u_7 + 1} (α := δ) (s.sup' ⋯ fun (i : α) ↦ t.sup' ⋯ fun (i' : β) ↦ (g ∘ uncurry f) (i, i'))
    (s.sup' ⋯ fun (x : α) ↦ t.sup' ⋯ fun (x_1 : β) ↦ g (f x x_1))
⊢ (image₂ f s t).sup' h g = s.sup' ⋯ fun (x : α) ↦ t.sup' ⋯ fun (x_1 : β) ↦ g (f x x_1)

Tactic:
simp only [image₂, sup'_image, sup'_product_left]

Premises used: Finset.sup'_product_left, Finset.sup'_image, Finset.image₂
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ Eq.{u_7 + 1} (α := δ) (s.sup' ⋯ fun (i : α) ↦ t.sup' ⋯ fun (i' : β) ↦ (g ∘ uncurry f) (i, i'))
    (s.sup' ⋯ fun (x : α) ↦ t.sup' ⋯ fun (x_1 : β) ↦ g (f x x_1))

Tactic:
rfl
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
simp :
  Eq.{u_7 + 1} (α := δ) (t.sup' ⋯ fun (i' : β) ↦ s.sup' ⋯ fun (i : α) ↦ (g ∘ uncurry f) (i, i'))
    (t.sup' ⋯ fun (y : β) ↦ s.sup' ⋯ fun (x : α) ↦ g (f x y))
⊢ (image₂ f s t).sup' h g = t.sup' ⋯ fun (y : β) ↦ s.sup' ⋯ fun (x : α) ↦ g (f x y)

Tactic:
simp only [image₂, sup'_image, sup'_product_right]

Premises used: Finset.sup'_image, Finset.sup'_product_right, Finset.image₂
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ Eq.{u_7 + 1} (α := δ) (t.sup' ⋯ fun (i' : β) ↦ s.sup' ⋯ fun (i : α) ↦ (g ∘ uncurry f) (i, i'))
    (t.sup' ⋯ fun (y : β) ↦ s.sup' ⋯ fun (x : α) ↦ g (f x y))

Tactic:
rfl
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeSup δ
inst_2 : OrderBot δ
g : γ → δ
a : δ
rw : (∀ b ∈ image₂ f s t, g b ≤ a) ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
rw₁ rw₂ : (∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a) ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
⊢ (image₂ f s t).sup g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a

Tactic:
rw [Finset.sup_le_iff, forall_mem_image₂]

Premises used: Finset.forall_mem_image₂, Finset.sup_le_iff