awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : (s.mulAntidiagonal t a).Infinite
⊢ (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)

Tactic:
have h1 : (mulAntidiagonal s t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o (· ≤ ·)) :=
    fun f ↦ hs fun n ↦ ⟨_, (mem_mulAntidiagonal.1 (f n).2).1⟩
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : (s.mulAntidiagonal t a).Infinite
h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
⊢ (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)

Tactic:
have h2 : (mulAntidiagonal s t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o (· ≤ ·)) :=
    fun f ↦ ht fun n ↦ ⟨_, (mem_mulAntidiagonal.1 (f n).2).2.1⟩
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : (s.mulAntidiagonal t a).Infinite
h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
h2 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
obtain :
  ∀ (g : ℕ ↪o ℕ)
    (hg :
      ∀ (m n : ℕ),
        m ≤ n →
          Order.Preimage (α := α × α) Prod.fst (fun (x1 x2 : α) ↦ x1 ≤ x2)
            (↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_2 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
                  ((g : (a : ℕ) → ℕ) m : ℕ)) :
              α × α)
            (↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_2 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
                  ((g : (a : ℕ) → ℕ) n : ℕ)) :
              α × α)),
    False
⊢ False

Tactic:
obtain ⟨g, hg⟩ :=
    h1.exists_monotone_subseq fun n ↦ (h.natEmbedding _ n).2

Premises used: Set.mulAntidiagonal, Set.PartiallyWellOrderedOn.exists_monotone_subseq, Set.Infinite.natEmbedding, DFunLike.coe, Subtype.property
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : (s.mulAntidiagonal t a).Infinite
h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
h2 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      Order.Preimage (α := α × α) Prod.fst (fun (x1 x2 : α) ↦ x1 ≤ x2)
        (↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_2 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
              ((g : (a : ℕ) → ℕ) m : ℕ)) :
          α × α)
        (↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_2 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
              ((g : (a : ℕ) → ℕ) n : ℕ)) :
          α × α)
obtain :
  ∀ (m n : ℕ) (mn : m < n)
    (h2' :
      Subrel (Prod.snd ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x : α × α) ↦ x ∈ s.mulAntidiagonal t a)
        ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
          ((g : (a : ℕ) → ℕ) m : ℕ))
        ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
          ((g : (a : ℕ) → ℕ) n : ℕ))),
    False
⊢ False

Tactic:
obtain ⟨m, n, mn, h2'⟩ := h2 fun n ↦ h.natEmbedding _ _

Premises used: Set.mulAntidiagonal, Set.Infinite.natEmbedding, DFunLike.coe
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : (s.mulAntidiagonal t a).Infinite
h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
h2 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      Order.Preimage (α := α × α) Prod.fst (fun (x1 x2 : α) ↦ x1 ≤ x2)
        (↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_2 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
              ((g : (a : ℕ) → ℕ) m : ℕ)) :
          α × α)
        (↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_2 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
              ((g : (a : ℕ) → ℕ) n : ℕ)) :
          α × α)
m n : ℕ
mn : m < n
h2' :
  Subrel (Prod.snd ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x : α × α) ↦ x ∈ s.mulAntidiagonal t a)
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
      ((g : (a : ℕ) → ℕ) m : ℕ))
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
      ((g : (a : ℕ) → ℕ) n : ℕ))
⊢ False

Tactic:
mn.ne (g.injective <| (h.natEmbedding _).injective ?_)

Premises used: RelEmbedding.injective, Set.Infinite.natEmbedding, Function.Embedding.injective, LT.lt.ne
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : (s.mulAntidiagonal t a).Infinite
h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
h2 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      Order.Preimage (α := α × α) Prod.fst (fun (x1 x2 : α) ↦ x1 ≤ x2)
        (↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_2 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
              ((g : (a : ℕ) → ℕ) m : ℕ)) :
          α × α)
        (↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_2 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
              ((g : (a : ℕ) → ℕ) n : ℕ)) :
          α × α)
m n : ℕ
mn : m < n
h2' :
  Subrel (Prod.snd ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x : α × α) ↦ x ∈ s.mulAntidiagonal t a)
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
      ((g : (a : ℕ) → ℕ) m : ℕ))
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
      ((g : (a : ℕ) → ℕ) n : ℕ))
refine :
  Eq (α := (↑(s.mulAntidiagonal t a) : Type u_1))
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
        ((g : (a : ℕ) → ℕ) m : ℕ) :
      (↑(s.mulAntidiagonal t a) : Type u_1))
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
        ((g : (a : ℕ) → ℕ) n : ℕ) :
      (↑(s.mulAntidiagonal t a) : Type u_1))
⊢ False

Tactic:
refine mn.ne (g.injective <| (h.natEmbedding _).injective ?_)

Premises used: RelEmbedding.injective, Set.Infinite.natEmbedding, Function.Embedding.injective, LT.lt.ne
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : (s.mulAntidiagonal t a).Infinite
h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
h2 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      Order.Preimage (α := α × α) Prod.fst (fun (x1 x2 : α) ↦ x1 ≤ x2)
        (↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_2 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
              ((g : (a : ℕ) → ℕ) m : ℕ)) :
          α × α)
        (↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_2 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
              ((g : (a : ℕ) → ℕ) n : ℕ)) :
          α × α)
m n : ℕ
mn : m < n
h2' :
  Subrel (Prod.snd ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x : α × α) ↦ x ∈ s.mulAntidiagonal t a)
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
      ((g : (a : ℕ) → ℕ) m : ℕ))
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
      ((g : (a : ℕ) → ℕ) n : ℕ))
⊢ Eq (α := (↑(s.mulAntidiagonal t a) : Type u_1))
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
        ((g : (a : ℕ) → ℕ) m : ℕ) :
      (↑(s.mulAntidiagonal t a) : Type u_1))
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
        ((g : (a : ℕ) → ℕ) n : ℕ) :
      (↑(s.mulAntidiagonal t a) : Type u_1))

Tactic:
eq_of_fst_le_fst_of_snd_le_snd _ _ _ (hg _ _ mn.le) h2'

Premises used: LT.lt.le, Set.MulAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : (s.mulAntidiagonal t a).Infinite
h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
h2 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      Order.Preimage (α := α × α) Prod.fst (fun (x1 x2 : α) ↦ x1 ≤ x2)
        (↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_2 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
              ((g : (a : ℕ) → ℕ) m : ℕ)) :
          α × α)
        (↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_2 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
              ((g : (a : ℕ) → ℕ) n : ℕ)) :
          α × α)
m n : ℕ
mn : m < n
h2' :
  Subrel (Prod.snd ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x : α × α) ↦ x ∈ s.mulAntidiagonal t a)
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
      ((g : (a : ℕ) → ℕ) m : ℕ))
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
      ((g : (a : ℕ) → ℕ) n : ℕ))
⊢ Eq (α := (↑(s.mulAntidiagonal t a) : Type u_1))
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
        ((g : (a : ℕ) → ℕ) m : ℕ) :
      (↑(s.mulAntidiagonal t a) : Type u_1))
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
        ((g : (a : ℕ) → ℕ) n : ℕ) :
      (↑(s.mulAntidiagonal t a) : Type u_1))

Tactic:
exact eq_of_fst_le_fst_of_snd_le_snd _ _ _ (hg _ _ mn.le) h2'

Premises used: LT.lt.le, Set.MulAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd
-- Module: Mathlib.Data.Set.MulAntidiagonal
Goal:
α : Type u_1
inst : CancelCommMonoid α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : MulRightStrictMono α
s t : Set α
hs : s.IsWF
ht : t.IsWF
a : α
⊢ (s.mulAntidiagonal t a).Finite

Tactic:
finite_of_isPWO hs.isPWO ht.isPWO a

Premises used: Set.MulAntidiagonal.finite_of_isPWO, Set.IsWF.isPWO
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
hf : Injective2 f
a' : α
ha' : a' ∈ s
b' : β
hb' : b' ∈ t
h : f a' b' = f a b
rcases : ∀ (h : f a' b' = f a' b'), a' ∈ s ∧ b' ∈ t
⊢ a ∈ s ∧ b ∈ t

Tactic:
rcases hf h with ⟨rfl, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
hf : Injective2 f
a' : α
ha' : a' ∈ s
b' : β
hb' : b' ∈ t
h : f a' b' = f a' b'
⊢ a' ∈ s ∧ b' ∈ t

Tactic:
⟨ha', hb'⟩

Premises used: And.intro
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
hf : Injective2 f
a' : α
ha' : a' ∈ s
b' : β
hb' : b' ∈ t
h : f a' b' = f a' b'
⊢ a' ∈ s ∧ b' ∈ t

Tactic:
exact ⟨ha', hb'⟩
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
hs : s ⊆ s'
ht : t ⊆ t'
a : α
ha : a ∈ s
b : β
hb : b ∈ t
⊢ f a b ∈ image2 f s' t'

Tactic:
mem_image2_of_mem (hs ha) (ht hb)

Premises used: Set.mem_image2_of_mem
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
hs : s ⊆ s'
ht : t ⊆ t'
a : α
ha : a ∈ s
b : β
hb : b ∈ t
⊢ f a b ∈ image2 f s' t'

Tactic:
exact mem_image2_of_mem (hs ha) (ht hb)

Premises used: Set.mem_image2_of_mem
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
ht : t ⊆ t'
⊢ image2 f s t ⊆ image2 f s t'

Tactic:
image2_subset Subset.rfl ht

Premises used: Set.image2_subset, Set.Subset.rfl
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
hs : s ⊆ s'
⊢ image2 f s t ⊆ image2 f s' t

Tactic:
image2_subset hs Subset.rfl

Premises used: Set.image2_subset, Set.Subset.rfl
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
b : β
hb : b ∈ t
⊢ (fun (a : α) ↦ f a b) '' s ⊆ image2 f s t

Tactic:
forall_mem_image.2 fun _ ha => mem_image2_of_mem ha hb

Premises used: Iff.mpr, Set.Subset, Set.mem_image2_of_mem, Set.forall_mem_image
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
a : α
ha : a ∈ s
⊢ f a '' t ⊆ image2 f s t

Tactic:
forall_mem_image.2 fun _ => mem_image2_of_mem ha

Premises used: Iff.mpr, Set.Subset, Set.mem_image2_of_mem, Set.forall_mem_image
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
p : γ → Prop
⊢ (∀ (z : γ), z ∈ image2 f s t → p z) ↔ ∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → p (f x y)

Tactic:
grind
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
p : γ → Prop
⊢ (∃ (z : γ), z ∈ image2 f s t ∧ p z) ↔ ∃ (x : α), x ∈ s ∧ ∃ (y : β), y ∈ t ∧ p (f x y)

Tactic:
grind
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ image2 f s t ⊆ u ↔ ∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u

Tactic:
forall_mem_image2

Premises used: Set.forall_mem_image2, Set.Subset
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
simp_rw : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (a : α), a ∈ s → (fun (b : β) ↦ f a b) '' t ⊆ u
simp_rw₁ : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (a : α), a ∈ s → t ⊆ (fun (b : β) ↦ f a b) ⁻¹' u
simp_rw₂ :
  (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔
    ∀ (a : α), a ∈ s → ∀ (x : β), x ∈ t → Membership.mem (γ := Set β) ((fun (b : β) ↦ f a b) ⁻¹' u) x
⊢ image2 f s t ⊆ u ↔ ∀ (a : α), a ∈ s → (fun (b : β) ↦ f a b) '' t ⊆ u

Tactic:
simp_rw [image2_subset_iff, image_subset_iff, subset_def, mem_preimage]

Premises used: Set.subset_def, Set.image2_subset_iff, Set.image_subset_iff, Set.mem_preimage
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
simp_rw : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (b : β), b ∈ t → (fun (a : α) ↦ f a b) '' s ⊆ u
simp_rw₁ : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (b : β), b ∈ t → s ⊆ (fun (a : α) ↦ f a b) ⁻¹' u
simp_rw₂ :
  (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔
    ∀ (b : β), b ∈ t → ∀ (x : α), x ∈ s → Membership.mem (γ := Set α) ((fun (a : α) ↦ f a b) ⁻¹' u) x
simp_rw₃ : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (b : β), b ∈ t → ∀ (x : α), x ∈ s → f x b ∈ u
⊢ image2 f s t ⊆ u ↔ ∀ (b : β), b ∈ t → (fun (a : α) ↦ f a b) '' s ⊆ u

Tactic:
simp_rw [image2_subset_iff, image_subset_iff, subset_def, mem_preimage, @forall₂_comm α]

Premises used: Set.subset_def, Set.image2_subset_iff, Set.image_subset_iff, forall₂_comm, Set.mem_preimage
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
x : γ
⊢ Membership.mem (γ := Set γ) ((fun (x : α × β) ↦ f x.1 x.2) '' s ×ˢ t) x ↔ x ∈ image2 f s t

Tactic:
simp [and_assoc]

Premises used: and_assoc
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ uncurry f '' s ×ˢ t = image2 f s t

Tactic:
image_prod _

Premises used: Set.image_prod
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
s : Set α
t : Set β
⊢ ∀ (x : α × β), x ∈ image2 Prod.mk s t ↔ x ∈ s ×ˢ t

Tactic:
simp
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α × β → γ
s : Set α
t : Set β
⊢ image2 (fun (a : α) (b : β) ↦ f (a, b)) s t = f '' s ×ˢ t

Tactic:
simp [← image_uncurry_prod, uncurry]

Premises used: Set.image_uncurry_prod, Function.uncurry
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = image2 (fun (a : β) (b : α) ↦ f b a) t s

Tactic:
grind
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
simp_rw :
  Eq.{u_5 + 1} (α := Set γ) ((fun (x : α × β) ↦ f x.1 x.2) '' (s ∪ s') ×ˢ t)
    ((fun (x : α × β) ↦ f x.1 x.2) '' s ×ˢ t ∪ (fun (x : α × β) ↦ f x.1 x.2) '' s' ×ˢ t)
simp_rw₁ :
  Eq.{u_5 + 1} (α := Set γ) ((fun (x : α × β) ↦ f x.1 x.2) '' (s ×ˢ t ∪ s' ×ˢ t))
    ((fun (x : α × β) ↦ f x.1 x.2) '' s ×ˢ t ∪ (fun (x : α × β) ↦ f x.1 x.2) '' s' ×ˢ t)
⊢ image2 f (s ∪ s') t = image2 f s t ∪ image2 f s' t

Tactic:
simp_rw [← image_prod, union_prod, image_union]

Premises used: Set.image_prod, Set.union_prod, Set.image_union
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
rw : image2 (fun (b : β) (a : α) ↦ f a b) (t ∪ t') s = image2 f s t ∪ image2 f s t'
rw₁ :
  image2 (fun (b : β) (a : α) ↦ f a b) t s ∪ image2 (fun (b : β) (a : α) ↦ f a b) t' s = image2 f s t ∪ image2 f s t'
rw₂ :
  image2 (fun (b : β) (a : α) ↦ f a b) t s ∪ image2 (fun (b : β) (a : α) ↦ f a b) t' s =
    image2 (fun (a : β) (b : α) ↦ f b a) t s ∪ image2 f s t'
rw₃ rw₄ :
  Eq.{u_5 + 1} (α := Set γ) (image2 (fun (b : β) (a : α) ↦ f a b) t s ∪ image2 (fun (b : β) (a : α) ↦ f a b) t' s)
    (image2 (fun (a : β) (b : α) ↦ f b a) t s ∪ image2 (fun (a : β) (b : α) ↦ f b a) t' s)
⊢ image2 f s (t ∪ t') = image2 f s t ∪ image2 f s t'

Tactic:
rw [← image2_swap, image2_union_left, image2_swap f, image2_swap f]

Premises used: Set.image2_swap, Set.image2_union_left
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
hf : Injective2 f
simp_rw : uncurry f '' (s ∩ s') ×ˢ t = uncurry f '' s ×ˢ t ∩ uncurry f '' s' ×ˢ t
simp_rw₁ : uncurry f '' (s ×ˢ t ∩ s' ×ˢ t) = uncurry f '' s ×ˢ t ∩ uncurry f '' s' ×ˢ t
⊢ image2 f (s ∩ s') t = image2 f s t ∩ image2 f s' t

Tactic:
simp_rw [← image_uncurry_prod, inter_prod, image_inter hf.uncurry]

Premises used: Set.image_inter, Function.Injective2.uncurry, Set.image_uncurry_prod, Set.inter_prod
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
hf : Injective2 f
simp_rw : uncurry f '' s ×ˢ (t ∩ t') = uncurry f '' s ×ˢ t ∩ uncurry f '' s ×ˢ t'
simp_rw₁ : uncurry f '' (s ×ˢ t ∩ s ×ˢ t') = uncurry f '' s ×ˢ t ∩ uncurry f '' s ×ˢ t'
⊢ image2 f s (t ∩ t') = image2 f s t ∩ image2 f s t'

Tactic:
simp_rw [← image_uncurry_prod, prod_inter, image_inter hf.uncurry]

Premises used: Set.image_inter, Set.prod_inter, Function.Injective2.uncurry, Set.image_uncurry_prod
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
t : Set β
⊢ ∀ (x : γ), x ∈ image2 f ∅ t ↔ Membership.mem (γ := Set γ) ∅ x

Tactic:
simp
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
⊢ ∀ (x : γ), x ∈ image2 f s ∅ ↔ Membership.mem (γ := Set γ) ∅ x

Tactic:
simp
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ s.Nonempty → t.Nonempty → (Set.image2 f s t).Nonempty

Tactic:
fun ⟨_, ha⟩ ⟨_, hb⟩ => ⟨_, mem_image2_of_mem ha hb⟩

Premises used: Set.Nonempty, Set.image2, Exists.intro, Set.mem_image2_of_mem, _private.0.Set.Nonempty.image2.match_1
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ (image2 f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
⟨fun ⟨_, a, ha, b, hb, _⟩ => ⟨⟨a, ha⟩, b, hb⟩, fun h => h.1.image2 h.2⟩

Premises used: Set.Nonempty.image2, And, Set.Nonempty, And.right, And.left, And.intro, Iff.intro, Exists.intro, _private.0.Set.image2_nonempty_iff.match_1
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
h : (Set.image2 f s t).Nonempty
⊢ s.Nonempty

Tactic:
(image2_nonempty_iff.1 h).1

Premises used: And.left, Iff.mp, Set.image2_nonempty_iff
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
h : (Set.image2 f s t).Nonempty
⊢ t.Nonempty

Tactic:
(image2_nonempty_iff.1 h).2

Premises used: And.right, Iff.mp, Set.image2_nonempty_iff
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
rw : ¬s.Nonempty ∨ ¬t.Nonempty ↔ s = ∅ ∨ t = ∅
⊢ image2 f s t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
rw [← not_nonempty_iff_eq_empty, image2_nonempty_iff, not_and_or]

Premises used: Set.not_nonempty_iff_eq_empty, not_and_or, Set.image2_nonempty_iff
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ ¬s.Nonempty ∨ ¬t.Nonempty ↔ s = ∅ ∨ t = ∅

Tactic:
simp [not_nonempty_iff_eq_empty]

Premises used: Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
s : Set α
t : Set β
hs : s.Subsingleton
ht : t.Subsingleton
f : α → β → γ
rw : Set.Subsingleton.{u_5} (α := γ) ((fun (x : α × β) ↦ f x.1 x.2) '' s ×ˢ t)
⊢ (Set.image2 f s t).Subsingleton

Tactic:
rw [← image_prod]

Premises used: Set.image_prod
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
s : Set α
t : Set β
hs : s.Subsingleton
ht : t.Subsingleton
f : α → β → γ
⊢ Set.Subsingleton.{u_5} (α := γ) ((fun (x : α × β) ↦ f x.1 x.2) '' s ×ˢ t)

Tactic:
apply (hs.prod ht).image

Premises used: Set.Subsingleton.image, Set.Subsingleton.prod
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
⊢ image2 f (s ∩ s') t ⊆ image2 f s t ∩ image2 f s' t

Tactic:
Monotone.map_inf_le (fun _ _ ↦ image2_subset_right) s s'

Premises used: Set.image2_subset_right, Monotone.map_inf_le
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
⊢ image2 f s (t ∩ t') ⊆ image2 f s t ∩ image2 f s t'

Tactic:
Monotone.map_inf_le (fun _ _ ↦ image2_subset_left) t t'

Premises used: Set.image2_subset_left, Monotone.map_inf_le
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
a : α
ha : a ∈ s
b : β
hb : b ∈ t
h : ¬f a b ∈ image2 f s' t
⊢ f a b ∈ image2 f (s \ s') t

Tactic:
⟨_, ⟨ha, fun ha' ↦ h ⟨_, ha', _, hb, rfl⟩⟩, _, hb, rfl⟩

Premises used: Set.Mem, setOf, Set.image2, And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
a : α
ha : a ∈ s
b : β
hb : b ∈ t
h : ¬f a b ∈ image2 f s' t
⊢ f a b ∈ image2 f (s \ s') t

Tactic:
exact ⟨_, ⟨ha, fun ha' ↦ h ⟨_, ha', _, hb, rfl⟩⟩, _, hb, rfl⟩
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
a : α
ha : a ∈ s
b : β
hb : b ∈ t
h : ¬f a b ∈ image2 f s t'
⊢ f a b ∈ image2 f s (t \ t')

Tactic:
⟨_, ha, _, ⟨hb, fun hb' ↦ h ⟨_, ha, _, hb', rfl⟩⟩, rfl⟩

Premises used: Set.Mem, setOf, Set.image2, And.intro, Exists.intro, rfl