awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : (∀ x ∈ (↑s : Set α), i ≤ x) ∧ ∀ x ∈ lowerBounds (↑s : Set α), x ≤ i
⊢ i = s.min' hs

Tactic:
le_antisymm (his.1 (Finset.min' s hs) (Finset.min'_mem s hs)) (his.2 _ (Finset.min'_le s))

Premises used: Finset.min', Finset.min'_le, Finset.min'_mem, le_antisymm, And.right, And.left
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : (∀ x ∈ (↑s : Set α), i ≤ x) ∧ ∀ x ∈ lowerBounds (↑s : Set α), x ≤ i
⊢ i = s.min' hs

Tactic:
exact le_antisymm (his.1 (Finset.min' s hs) (Finset.min'_mem s hs)) (his.2 _ (Finset.min'_le s))

Premises used: Finset.min', Finset.min'_le, Finset.min'_mem, le_antisymm, And.right, And.left
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
⊢ IsLUB (↑s : Set α) i ↔ IsGreatest (↑s : Set α) i

Tactic:
@isGLB_iff_isLeast αᵒᵈ _ i s hs

Premises used: lowerBounds, Set.Mem, setOf, upperBounds, IsLeast, IsGreatest, IsLUB, Finset.isGLB_iff_isLeast, OrderDual
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
i : α
s : Finset α
his : IsGLB (↑s : Set α) i
hs : s.Nonempty
⊢ i ∈ (↑s : Set α)

Tactic:
((isGLB_iff_isLeast i s hs).mp his).1

Premises used: And.left, Finset.isGLB_iff_isLeast, Iff.mp
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
i : α
s : Finset α
his : IsGLB (↑s : Set α) i
hs : s.Nonempty
⊢ i ∈ (↑s : Set α)

Tactic:
exact ((isGLB_iff_isLeast i s hs).mp his).1

Premises used: And.left, Finset.isGLB_iff_isLeast, Iff.mp
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
i : α
s : Finset α
his : IsLUB (↑s : Set α) i
hs : s.Nonempty
⊢ i ∈ s

Tactic:
@isGLB_mem αᵒᵈ _ i s his hs

Premises used: Set.Mem, setOf, Finset.isGLB_mem, OrderDual
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_7
R : Type u_8
inst : LinearOrder R
f : α → R
s : Multiset α
hs : s ≠ 0
obtain : ∀ (y : α) (hys : y ∈ s.toFinset) (hy : ∀ x' ∈ s.toFinset, f x' ≤ f y), ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y
⊢ ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y

Tactic:
obtain ⟨y, hys, hy⟩ := Finset.exists_max_image s.toFinset f (toFinset_nonempty.mpr hs)

Premises used: Multiset.toFinset, Iff.mpr, Finset.exists_max_image, Multiset.toFinset_nonempty
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_7
R : Type u_8
inst : LinearOrder R
f : α → R
s : Multiset α
hs : s ≠ 0
y : α
hys : y ∈ s.toFinset
hy : ∀ x' ∈ s.toFinset, f x' ≤ f y
⊢ ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y

Tactic:
⟨y, mem_toFinset.mp hys, fun _ hz ↦ hy _ (mem_toFinset.mpr hz)⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Iff.mp, Multiset.mem_toFinset
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_7
R : Type u_8
inst : LinearOrder R
f : α → R
s : Multiset α
hs : s ≠ 0
y : α
hys : y ∈ s.toFinset
hy : ∀ x' ∈ s.toFinset, f x' ≤ f y
⊢ ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y

Tactic:
exact ⟨y, mem_toFinset.mp hys, fun _ hz ↦ hy _ (mem_toFinset.mpr hz)⟩
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_7
R : Type u_8
inst : LinearOrder R
f : α → R
s : Multiset α
hs : s ≠ 0
obtain : ∀ (y : α) (hys : y ∈ s.toFinset) (hy : ∀ x' ∈ s.toFinset, f x' ≤ f y), ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y
⊢ ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y

Tactic:
classical
  obtain ⟨y, hys, hy⟩ := Finset.exists_max_image s.toFinset f (toFinset_nonempty.mpr hs)
  exact ⟨y, mem_toFinset.mp hys, fun _ hz ↦ hy _ (mem_toFinset.mpr hz)⟩
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_7
R : Type u_8
inst : LinearOrder R
f : α → R
s : Multiset α
hs : s ≠ 0
⊢ ∃ y ∈ s, ∀ z ∈ s, f y ≤ f z

Tactic:
@exists_max_image α Rᵒᵈ _ f s hs

Premises used: Multiset.exists_max_image
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_1
s t : Set α
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
hs : s.IsPWO
ht : t.IsPWO
rw : IsPWO (α := α) ((fun (x : α × α) ↦ x.1 * x.2) '' s ×ˢ t)
⊢ (s * t).IsPWO

Tactic:
rw [← image_mul_prod]

Premises used: Set.image_mul_prod
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_1
s t : Set α
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
hs : s.IsPWO
ht : t.IsPWO
⊢ IsPWO (α := α) ((fun (x : α × α) ↦ x.1 * x.2) '' s ×ˢ t)

Tactic:
(hs.prod ht).image_of_monotone (monotone_fst.mul' monotone_snd)

Premises used: monotone_fst, Set.IsPWO.prod, Set.IsPWO.image_of_monotone, Monotone.mul', monotone_snd
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_1
s t : Set α
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
hs : s.IsPWO
ht : t.IsPWO
⊢ IsPWO (α := α) ((fun (x : α × α) ↦ x.1 * x.2) '' s ×ˢ t)

Tactic:
exact (hs.prod ht).image_of_monotone (monotone_fst.mul' monotone_snd)

Premises used: monotone_fst, Set.IsPWO.prod, Set.IsPWO.image_of_monotone, Monotone.mul', monotone_snd
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_1
s t : Set α
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
hs : s.IsWF
ht : t.IsWF
⊢ (s * t).IsWF

Tactic:
(hs.isPWO.mul ht.isPWO).isWF

Premises used: Set.IsPWO.isWF, Set.IsWF.isPWO, Set.IsPWO.mul
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_1
s t : Set α
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ min (s := s * t) ⋯ ⋯ = hs.min (s := s) hsn * ht.min (s := t) htn

Tactic:
le_antisymm (IsWF.min_le _ _ (mem_mul.2 ⟨_, hs.min_mem _, _, ht.min_mem _, rfl⟩)) ?_

Premises used: Iff.mpr, Set.IsWF.min_mem, le_antisymm, And.intro, Exists.intro, Set.IsWF.min_le, rfl, Set.mem_mul
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_1
s t : Set α
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
refine : hs.min (s := s) hsn * ht.min (s := t) htn ≤ min (s := s * t) ⋯ ⋯
⊢ min (s := s * t) ⋯ ⋯ = hs.min (s := s) hsn * ht.min (s := t) htn

Tactic:
refine le_antisymm (IsWF.min_le _ _ (mem_mul.2 ⟨_, hs.min_mem _, _, ht.min_mem _, rfl⟩)) ?_

Premises used: Iff.mpr, Set.IsWF.min_mem, le_antisymm, And.intro, Exists.intro, Set.IsWF.min_le, rfl, Set.mem_mul
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_1
s t : Set α
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
rw : ∀ b ∈ s * t, hs.min (s := s) hsn * ht.min (s := t) htn ≤ b
⊢ hs.min (s := s) hsn * ht.min (s := t) htn ≤ min (s := s * t) ⋯ ⋯

Tactic:
rw [IsWF.le_min_iff]

Premises used: Set.IsWF.le_min_iff
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_1
s t : Set α
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ t
⊢ hs.min (s := s) hsn * ht.min (s := t) htn ≤ (fun (x1 x2 : α) ↦ x1 * x2) x y

Tactic:
mul_le_mul' (hs.min_le _ hx) (ht.min_le _ hy)

Premises used: Set.IsWF.min_le, mul_le_mul'
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_1
s t : Set α
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ t
⊢ hs.min (s := s) hsn * ht.min (s := t) htn ≤ (fun (x1 x2 : α) ↦ x1 * x2) x y

Tactic:
exact mul_le_mul' (hs.min_le _ hx) (ht.min_le _ hy)

Premises used: Set.IsWF.min_le, mul_le_mul'
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
x : α × α
⊢ x ∈ mulAntidiagonal (s := s) (t := t) hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 * x.2 = a

Tactic:
simp only [mulAntidiagonal, Set.Finite.mem_toFinset, Set.mem_mulAntidiagonal]

Premises used: Set.Finite.mem_toFinset, Finset.mulAntidiagonal, Set.mem_mulAntidiagonal
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
u : Set α
hu : u.IsPWO
h : u ⊆ s
⊢ mulAntidiagonal (s := u) (t := t) hu ht a ⊆ mulAntidiagonal (s := s) (t := t) hs ht a

Tactic:
Set.Finite.toFinset_mono <| Set.mulAntidiagonal_mono_left h

Premises used: Set.mulAntidiagonal_mono_left, Set.Mem, setOf, Set.Finite.toFinset_mono
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
u : Set α
hu : u.IsPWO
h : u ⊆ t
⊢ mulAntidiagonal (s := s) (t := u) hs hu a ⊆ mulAntidiagonal (s := s) (t := t) hs ht a

Tactic:
Set.Finite.toFinset_mono <| Set.mulAntidiagonal_mono_right h

Premises used: Set.Mem, setOf, Set.Finite.toFinset_mono, Set.mulAntidiagonal_mono_right
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
x : α × α
⊢ x.swap ∈ mulAntidiagonal (s := s) (t := t) hs ht a ↔ x ∈ mulAntidiagonal (s := t) (t := s) ht hs a

Tactic:
simp
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : Membership.mem (γ := Set α) {a : α | (mulAntidiagonal (s := s) (t := t) hs ht a).Nonempty} a
b : α × α
hb : b ∈ mulAntidiagonal (s := s) (t := t) hs ht a
⊢ b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 * b.2 = a

Tactic:
rw [mem_mulAntidiagonal] at hb

Premises used: Finset.mem_mulAntidiagonal
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : Membership.mem (γ := Set α) {a : α | (mulAntidiagonal (s := s) (t := t) hs ht a).Nonempty} a
b : α × α
hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 * b.2 = a
⊢ a ∈ s * t

Tactic:
⟨b.1, hb.1, b.2, hb.2⟩

Premises used: Set.Mem, setOf, Prod.fst, And.right, And.left, Set.image2, And.intro, Exists.intro, Prod.snd
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : Membership.mem (γ := Set α) {a : α | (mulAntidiagonal (s := s) (t := t) hs ht a).Nonempty} a
b : α × α
hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 * b.2 = a
⊢ a ∈ s * t

Tactic:
exact ⟨b.1, hb.1, b.2, hb.2⟩
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
⊢ Set.IsPWO.{u_1} (α := α) {a : α | (mulAntidiagonal (s := s) (t := t) hs ht a).Nonempty}

Tactic:
(hs.mul ht).mono support_mulAntidiagonal_subset_mul

Premises used: Set.IsPWO.mul, Set.IsPWO.mono, Finset.support_mulAntidiagonal_subset_mul
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
h :
  ∀ (a b : α),
    (a, b) ∈ mulAntidiagonal (s := s) (t := t) ⋯ ⋯ (hs.min (s := s) hns * ht.min (s := t) hnt) ↔
      Membership.mem (γ := Finset (α × α)) {(hs.min (s := s) hns, ht.min (s := t) hnt)} (a, b)
⊢ mulAntidiagonal (s := s) (t := t) ⋯ ⋯ (hs.min (s := s) hns * ht.min (s := t) hnt) =
    {(hs.min (s := s) hns, ht.min (s := t) hnt)}

Tactic:
ext ⟨a, b⟩
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
h :
  a ∈ s ∧ b ∈ t ∧ a * b = hs.min (s := s) hns * ht.min (s := t) hnt ↔ a = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt
⊢ (a, b) ∈ mulAntidiagonal (s := s) (t := t) ⋯ ⋯ (hs.min (s := s) hns * ht.min (s := t) hnt) ↔
    Membership.mem (γ := Finset (α × α)) {(hs.min (s := s) hns, ht.min (s := t) hnt)} (a, b)

Tactic:
simp only [mem_mulAntidiagonal, mem_singleton, Prod.ext_iff]

Premises used: Finset.mem_singleton, Finset.mem_mulAntidiagonal, Prod.ext_iff
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
h :
  a ∈ s ∧ b ∈ t ∧ a * b = hs.min (s := s) hns * ht.min (s := t) hnt → a = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt
h₁ :
  a = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt → a ∈ s ∧ b ∈ t ∧ a * b = hs.min (s := s) hns * ht.min (s := t) hnt
⊢ a ∈ s ∧ b ∈ t ∧ a * b = hs.min (s := s) hns * ht.min (s := t) hnt ↔ a = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt

Tactic:
constructor
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
has : a ∈ s
hat : b ∈ t
hst : a * b = hs.min (s := s) hns * ht.min (s := t) hnt
h :
  ∀ (has : hs.min (s := s) hns ∈ s) (hst : hs.min (s := s) hns * b = hs.min (s := s) hns * ht.min (s := t) hnt),
    hs.min (s := s) hns = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt
⊢ a = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt

Tactic:
obtain rfl :=
      (hs.min_le hns has).eq_of_not_lt fun hlt =>
        (mul_lt_mul_of_lt_of_le hlt <| ht.min_le hnt hat).ne' hst

Premises used: LE.le.eq_of_not_lt, LT.lt.ne', Set.IsWF.min_le, mul_lt_mul_of_lt_of_le, rfl
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
b : α
hat : b ∈ t
has : hs.min (s := s) hns ∈ s
hst : hs.min (s := s) hns * b = hs.min (s := s) hns * ht.min (s := t) hnt
⊢ hs.min (s := s) hns = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt

Tactic:
⟨rfl, mul_left_cancel hst⟩

Premises used: mul_left_cancel, And.intro, rfl
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
b : α
hat : b ∈ t
has : hs.min (s := s) hns ∈ s
hst : hs.min (s := s) hns * b = hs.min (s := s) hns * ht.min (s := t) hnt
⊢ hs.min (s := s) hns = hs.min (s := s) hns ∧ b = ht.min (s := t) hnt

Tactic:
exact ⟨rfl, mul_left_cancel hst⟩
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
⊢ hs.min (s := s) hns ∈ s ∧
    ht.min (s := t) hnt ∈ t ∧ hs.min (s := s) hns * ht.min (s := t) hnt = hs.min (s := s) hns * ht.min (s := t) hnt

Tactic:
⟨hs.min_mem _, ht.min_mem _, rfl⟩

Premises used: Set.IsWF.min_mem, And.intro, rfl
-- Module: Mathlib.Data.Finset.MulAntidiagonal
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
⊢ hs.min (s := s) hns ∈ s ∧
    ht.min (s := t) hnt ∈ t ∧ hs.min (s := s) hns * ht.min (s := t) hnt = hs.min (s := s) hns * ht.min (s := t) hnt

Tactic:
exact ⟨hs.min_mem _, ht.min_mem _, rfl⟩
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
c : γ
⊢ c ∈ image₂ f s t ↔ ∃ a ∈ s, ∃ b ∈ t, f a b = c

Tactic:
simp [image₂, and_assoc]

Premises used: and_assoc, 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₂ f s t) : Set γ) = image2 f (↑s : Set α) (↑t : Set β)

Tactic:
Set.ext fun _ => mem_image₂

Premises used: Set.ext, Finset.mem_image₂
-- 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) ≤ #s * #t

Tactic:
card_image_le.trans_eq <| card_product _ _

Premises used: LE.le.trans_eq, Finset.card_product, Finset.card_image_le, Finset.image₂
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
rw : #(image₂ f s t) = #(s ×ˢ t) ↔ InjOn (β := γ) (fun (x : α × β) ↦ f x.1 x.2) (↑(s ×ˢ t) : Set (α × β))
⊢ #(image₂ f s t) = #s * #t ↔ InjOn (β := γ) (fun (x : α × β) ↦ f x.1 x.2) ((↑s : Set α) ×ˢ (↑t : Set β))

Tactic:
rw [← card_product, ← coe_product]

Premises used: Finset.card_product, Finset.coe_product
-- 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) = #(s ×ˢ t) ↔ InjOn (β := γ) (fun (x : α × β) ↦ f x.1 x.2) (↑(s ×ˢ t) : Set (α × β))

Tactic:
card_image_iff

Premises used: Finset.card_image_iff, 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₂ f s t) = #(s ×ˢ t) ↔ InjOn (β := γ) (fun (x : α × β) ↦ f x.1 x.2) (↑(s ×ˢ t) : Set (α × β))

Tactic:
exact card_image_iff

Premises used: Finset.card_image_iff
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
hf : Injective2 f
s : Finset α
t : Finset β
⊢ #(image₂ f s t) = #s * #t

Tactic:
(card_image_of_injective _ hf.uncurry).trans <| card_product _ _

Premises used: Finset.card_product, Finset.card_image_of_injective, Function.Injective2.uncurry, Eq.trans, Finset.image₂
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
b : β
ha : a ∈ s
hb : b ∈ t
⊢ f a b ∈ image₂ f s t

Tactic:
mem_image₂.2 ⟨a, ha, b, hb, rfl⟩

Premises used: Iff.mpr, Finset.mem_image₂, And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
b : β
hf : Injective2 f
rw : f a b ∈ (↑(image₂ f s t) : Set γ) ↔ a ∈ s ∧ b ∈ t
rw₁ : f a b ∈ image2 f (↑s : Set α) (↑t : Set β) ↔ a ∈ s ∧ b ∈ t
rw₂ : a ∈ (↑s : Set α) ∧ b ∈ (↑t : Set β) ↔ a ∈ s ∧ b ∈ t
rw₃ : a ∈ s ∧ b ∈ (↑t : Set β) ↔ a ∈ s ∧ b ∈ t
rw₄ rw₅ : a ∈ s ∧ b ∈ t ↔ a ∈ s ∧ b ∈ t
⊢ f a b ∈ image₂ f s t ↔ a ∈ s ∧ b ∈ t

Tactic:
rw [← mem_coe, coe_image₂, mem_image2_iff hf, mem_coe, mem_coe]

Premises used: Finset.mem_coe, Finset.coe_image₂, Set.mem_image2_iff
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
hs : s ⊆ s'
ht : t ⊆ t'
rw : image2 f (↑s : Set α) (↑t : Set β) ⊆ image2 f (↑s' : Set α) (↑t' : Set β)
⊢ image₂ f s t ⊆ image₂ f s' t'

Tactic:
rw [← coe_subset, coe_image₂, coe_image₂]

Premises used: Finset.coe_image₂, Finset.coe_subset
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
hs : s ⊆ s'
ht : t ⊆ t'
⊢ image2 f (↑s : Set α) (↑t : Set β) ⊆ image2 f (↑s' : Set α) (↑t' : Set β)

Tactic:
image2_subset hs ht

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

Tactic:
exact image2_subset hs ht

Premises used: Set.image2_subset
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
ht : t ⊆ t'
⊢ image₂ f s t ⊆ image₂ f s t'

Tactic:
image₂_subset Subset.rfl ht

Premises used: Finset.Subset.rfl, Finset.image₂_subset
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
hs : s ⊆ s'
⊢ image₂ f s t ⊆ image₂ f s' t

Tactic:
image₂_subset hs Subset.rfl

Premises used: Finset.Subset.rfl, Finset.image₂_subset
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
b : β
hb : b ∈ t
⊢ image (fun (a : α) ↦ f a b) s ⊆ image₂ f s t

Tactic:
image_subset_iff.2 fun _ ha => mem_image₂_of_mem ha hb

Premises used: Iff.mpr, Finset.mem_image₂_of_mem, Finset.image_subset_iff
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
ha : a ∈ s
⊢ image (fun (b : β) ↦ f a b) t ⊆ image₂ f s t

Tactic:
image_subset_iff.2 fun _ => mem_image₂_of_mem ha

Premises used: Iff.mpr, Finset.mem_image₂_of_mem, Finset.image_subset_iff
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
p : γ → Prop
simp_rw : (∀ z ∈ (↑(image₂ f s t) : Set γ), p z) ↔ ∀ x ∈ (↑s : Set α), ∀ y ∈ (↑t : Set β), p (f x y)
simp_rw₁ : (∀ z ∈ image2 f (↑s : Set α) (↑t : Set β), p z) ↔ ∀ x ∈ (↑s : Set α), ∀ y ∈ (↑t : Set β), p (f x y)
⊢ (∀ z ∈ image₂ f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)

Tactic:
simp_rw [← mem_coe, coe_image₂, forall_mem_image2]

Premises used: Set.forall_mem_image2, Finset.mem_coe, Finset.coe_image₂
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
p : γ → Prop
simp_rw : (∃ z ∈ (↑(image₂ f s t) : Set γ), p z) ↔ ∃ x ∈ (↑s : Set α), ∃ y ∈ (↑t : Set β), p (f x y)
simp_rw₁ : (∃ z ∈ image2 f (↑s : Set α) (↑t : Set β), p z) ↔ ∃ x ∈ (↑s : Set α), ∃ y ∈ (↑t : Set β), p (f x y)
⊢ (∃ z ∈ image₂ f s t, p z) ↔ ∃ x ∈ s, ∃ y ∈ t, p (f x y)

Tactic:
simp_rw [← mem_coe, coe_image₂, exists_mem_image2]

Premises used: Set.exists_mem_image2, Finset.mem_coe, Finset.coe_image₂
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
u : Finset γ
⊢ image₂ f s t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, f x y ∈ u

Tactic:
forall_mem_image₂

Premises used: Finset.forall_mem_image₂
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
u : Finset γ
simp_rw : (∀ x ∈ s, ∀ y ∈ t, f x y ∈ u) ↔ ∀ a ∈ s, image (fun (b : β) ↦ f a b) t ⊆ u
⊢ image₂ f s t ⊆ u ↔ ∀ a ∈ s, image (fun (b : β) ↦ f a b) t ⊆ u

Tactic:
simp_rw [image₂_subset_iff, image_subset_iff]

Premises used: Finset.image₂_subset_iff, Finset.image_subset_iff
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
u : Finset γ
simp_rw : (∀ x ∈ s, ∀ y ∈ t, f x y ∈ u) ↔ ∀ b ∈ t, image (fun (a : α) ↦ f a b) s ⊆ u
simp_rw₁ : (∀ x ∈ s, ∀ y ∈ t, f x y ∈ u) ↔ ∀ b ∈ t, ∀ x ∈ s, f x b ∈ u
⊢ image₂ f s t ⊆ u ↔ ∀ b ∈ t, image (fun (a : α) ↦ f a b) s ⊆ u

Tactic:
simp_rw [image₂_subset_iff, image_subset_iff, @forall₂_comm α]

Premises used: Finset.image₂_subset_iff, Finset.image_subset_iff, forall₂_comm
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
rw : (image2 f (↑s : Set α) (↑t : Set β)).Nonempty ↔ s.Nonempty ∧ t.Nonempty
⊢ (image₂ f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
rw [← coe_nonempty, coe_image₂]

Premises used: Finset.coe_nonempty, Finset.coe_image₂
-- 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 β)).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
image2_nonempty_iff

Premises used: Set.Nonempty, Finset.Nonempty, Set.image2_nonempty_iff
-- 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 β)).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
exact image2_nonempty_iff

Premises used: Set.image2_nonempty_iff