awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
⊢ (s ∪ t) \ s = t

Tactic:
h.sup_sdiff_cancel_left

Premises used: Disjoint.sup_sdiff_cancel_left
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
⊢ (s ∪ t) \ t = s

Tactic:
h.sup_sdiff_cancel_right

Premises used: Disjoint.sup_sdiff_cancel_right
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ∪ t \ s = t ∪ s \ t

Tactic:
simp [union_comm]

Premises used: Finset.union_comm
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s \ t ∪ s ∩ t = s

Tactic:
sup_sdiff_inf _ _

Premises used: sup_sdiff_inf
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ (s \ t) \ t = s \ t

Tactic:
_root_.sdiff_idem

Premises used: sdiff_idem
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u

Tactic:
le_iff_subset.symm.trans le_sdiff

Premises used: le_sdiff, Iff.trans, Finset.le_iff_subset, Iff.symm
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s \ t = ∅ ↔ s ⊆ t

Tactic:
sdiff_eq_bot_iff

Premises used: sdiff_eq_bot_iff
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ (s \ t).Nonempty ↔ ¬s ⊆ t

Tactic:
nonempty_iff_ne_empty.trans sdiff_eq_empty_iff_subset.not

Premises used: Iff.not, Finset.nonempty_iff_ne_empty, Finset.sdiff_eq_empty_iff_subset, Iff.trans
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ ∅ \ s = ∅

Tactic:
bot_sdiff

Premises used: bot_sdiff
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
x : α
h : x ∉ t
⊢ insert x s \ t = insert x (s \ t)

Tactic:
grind
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
t s : Finset α
x : α
h : x ∈ t
⊢ insert x s \ t = s \ t

Tactic:
grind
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ insert a (s \ {a}) = s

Tactic:
grind
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
ha : a ∉ s
⊢ insert a s \ s = {a}

Tactic:
grind
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
x : α
⊢ insert x s \ insert x t = s \ insert x t

Tactic:
insert_sdiff_of_mem _ (mem_insert_self _ _)

Premises used: Finset.mem_insert_self, Finset.insert_sdiff_of_mem
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
ha : a ∉ s
h : ∀ (a_1 : α), a_1 ∈ insert a s \ insert b s ↔ Membership.mem (γ := Finset α) {a} a_1
⊢ insert a s \ insert b s = {a}

Tactic:
ext
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
ha : a ∉ s
a_1 : α
⊢ a_1 ∈ insert a s \ insert b s ↔ Membership.mem (γ := Finset α) {a} a_1

Tactic:
aesop
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
ha : a ∉ s
hb : b ∉ s
⊢ cons a s ha \ cons b s hb = {a}

Tactic:
grind
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
x : α
h : x ∉ s
t : Finset α
⊢ s \ insert x t = s \ t

Tactic:
grind
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s \ t ⊆ s

Tactic:
le_iff_subset.mp sdiff_le

Premises used: sdiff_le, Iff.mp, Finset.le_iff_subset
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : t ⊆ s
ht : t.Nonempty
⊢ s \ t ⊂ s

Tactic:
grind
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ t : Finset α
⊢ (s₁ ∪ s₂) \ t = s₁ \ t ∪ s₂ \ t

Tactic:
sup_sdiff

Premises used: sup_sdiff
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t₁ t₂ : Finset α
⊢ s \ (t₁ ∪ t₂) = s \ t₁ ∩ (s \ t₂)

Tactic:
sdiff_sup

Premises used: sdiff_sup
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
c : α
s : Finset α
hS : s.Nontrivial
⊢ (s \ {c}).Nonempty

Tactic:
grind
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
⊢ (s \ t) \ u = s \ t ∩ (s \ u)

Tactic:
_root_.sdiff_sdiff_left'

Premises used: sdiff_sdiff_left'
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
hts : t ⊆ s
hut : u ⊆ t
⊢ s \ t ∪ t \ u = s \ u

Tactic:
sdiff_sup_sdiff_cancel hts hut

Premises used: sdiff_sup_sdiff_cancel
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
h : u ⊆ s
⊢ s \ (t \ u) = s \ t ∪ u

Tactic:
sdiff_sdiff_eq_sdiff_sup h

Premises used: sdiff_sdiff_eq_sdiff_sup
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s \ (s \ t) = s ∩ t

Tactic:
sdiff_sdiff_right_self

Premises used: sdiff_sdiff_right_self
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : t ⊆ s
⊢ s \ (s \ t) = t

Tactic:
_root_.sdiff_sdiff_eq_self h

Premises used: sdiff_sdiff_eq_self
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t₁ t₂ : Finset α
⊢ s \ t₁ = s \ t₂ ↔ s ∩ t₁ = s ∩ t₂

Tactic:
sdiff_eq_sdiff_iff_inf_eq_inf

Premises used: sdiff_eq_sdiff_iff_inf_eq_inf
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ∪ t = s \ t ∪ t \ s ∪ s ∩ t

Tactic:
sup_eq_sdiff_sup_sdiff_sup_inf

Premises used: sup_eq_sdiff_sup_sdiff_sup_inf
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s \ t = s ↔ Disjoint s t

Tactic:
sdiff_eq_left

Premises used: sdiff_eq_left
-- Module: Mathlib.Data.Finset.SDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
⊢ s \ t = s

Tactic:
sdiff_eq_self_iff_disjoint.2 h

Premises used: Iff.mpr, Finset.sdiff_eq_self_iff_disjoint
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : Preorder G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
rw : IsPWO.{u_2} (α := P) ((fun (x : G × P) ↦ x.1 • x.2) '' s ×ˢ t)
⊢ (s • t).IsPWO

Tactic:
rw [← @image_smul_prod]

Premises used: Set.image_smul_prod
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : Preorder G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
⊢ IsPWO.{u_2} (α := P) ((fun (x : G × P) ↦ x.1 • x.2) '' s ×ˢ t)

Tactic:
(hs.prod ht).image_of_monotone (monotone_fst.smul monotone_snd)

Premises used: monotone_fst, Set.IsPWO.prod, Set.IsPWO.image_of_monotone, monotone_snd, Monotone.smul
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : Preorder G
inst_1 : Preorder P
inst_2 : SMul G P
inst_3 : IsOrderedSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
⊢ IsPWO.{u_2} (α := P) ((fun (x : G × P) ↦ x.1 • x.2) '' s ×ˢ t)

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

Premises used: monotone_fst, Set.IsPWO.prod, Set.IsPWO.image_of_monotone, monotone_snd, Monotone.smul
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
⊢ (s • t).IsWF

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

Premises used: Set.IsPWO.isWF, Set.IsPWO.smul, Set.IsWF.isPWO
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedSMul G P
s : Set G
t : Set P
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_smul.2 ⟨_, hs.min_mem _, _, ht.min_mem _, rfl⟩)) ?_

Premises used: Iff.mpr, Set.mem_smul, Set.IsWF.min_mem, le_antisymm, And.intro, Exists.intro, Set.IsWF.min_le, rfl
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedSMul G P
s : Set G
t : Set P
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_smul.2 ⟨_, hs.min_mem _, _, ht.min_mem _, rfl⟩)) ?_

Premises used: Iff.mpr, Set.mem_smul, Set.IsWF.min_mem, le_antisymm, And.intro, Exists.intro, Set.IsWF.min_le, rfl
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedSMul G P
s : Set G
t : Set P
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.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
x : G
hx : x ∈ s
y : P
hy : y ∈ t
⊢ hs.min (s := s) hsn • ht.min (s := t) htn ≤ (fun (x1 : G) (x2 : P) ↦ x1 • x2) x y

Tactic:
IsOrderedSMul.smul_le_smul (hs.min_le _ hx) (ht.min_le _ hy)

Premises used: IsOrderedSMul.smul_le_smul, Set.IsWF.min_le
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
x : G
hx : x ∈ s
y : P
hy : y ∈ t
⊢ hs.min (s := s) hsn • ht.min (s := t) htn ≤ (fun (x1 : G) (x2 : P) ↦ x1 • x2) x y

Tactic:
exact IsOrderedSMul.smul_le_smul (hs.min_le _ hx) (ht.min_le _ hy)

Premises used: IsOrderedSMul.smul_le_smul, Set.IsWF.min_le
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : SMul G P
s : Set G
t : Set P
a : P
h : (s.smulAntidiagonal t a).Finite
x : G × P
simp : x ∈ s.smulAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a
⊢ x ∈ SMulAntidiagonal (s := s) (t := t) a h ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a

Tactic:
simp only [SMulAntidiagonal, Set.Finite.mem_toFinset]

Premises used: Set.Finite.mem_toFinset, Finset.SMulAntidiagonal
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : SMul G P
s : Set G
t : Set P
a : P
h : (s.smulAntidiagonal t a).Finite
x : G × P
⊢ x ∈ s.smulAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a

Tactic:
Set.mem_sep_iff

Premises used: Set.Mem, setOf, Set.mem_sep_iff, Set.smulAntidiagonal
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : SMul G P
s : Set G
t : Set P
a : P
h : (s.smulAntidiagonal t a).Finite
x : G × P
⊢ x ∈ s.smulAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a

Tactic:
exact Set.mem_sep_iff

Premises used: Set.mem_sep_iff
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : SMul G P
s u : Set G
t : Set P
a : P
h : u ⊆ s
hst : (s.smulAntidiagonal t a).Finite
hut : (u.smulAntidiagonal t a).Finite
⊢ SMulAntidiagonal (s := u) (t := t) a hut ⊆ SMulAntidiagonal (s := s) (t := t) a hst

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

Premises used: Set.smulAntidiagonal_mono_left, Set.Mem, setOf, Set.Finite.toFinset_mono
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : SMul G P
s : Set G
t v : Set P
a : P
hst : (s.smulAntidiagonal t a).Finite
hsv : (s.smulAntidiagonal v a).Finite
h : v ⊆ t
⊢ SMulAntidiagonal (s := s) (t := v) a hsv ⊆ SMulAntidiagonal (s := s) (t := t) a hst

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

Premises used: Set.smulAntidiagonal_mono_right, Set.Mem, setOf, Set.Finite.toFinset_mono
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : SMul G P
s : Set G
t : Set P
hst : ∀ (a : P), (s.smulAntidiagonal t a).Finite
⊢ {a : P | (SMulAntidiagonal (s := s) (t := t) a ⋯).Nonempty} ⊆ s • t

Tactic:
grind [mem_smul, mem_smulAntidiagonal]

Premises used: Set.mem_smul, Finset.mem_smulAntidiagonal
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : SMul G P
inst_1 : PartialOrder G
inst_2 : PartialOrder P
inst_3 : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
⊢ IsPWO.{u_2} (α := P) {a : P | (SMulAntidiagonal (s := s) (t := t) a ⋯).Nonempty}

Tactic:
(hs.smul ht).mono
    (support_smulAntidiagonal_subset_smul (fun a ↦ (Set.SMulAntidiagonal.finite_of_isPWO hs ht a)))

Premises used: Finset.support_smulAntidiagonal_subset_smul, Set.SMulAntidiagonal.finite_of_isPWO, Set.IsPWO.smul, Set.IsPWO.mono
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
h :
  ∀ (a : G) (b : P),
    (a, b) ∈ SMulAntidiagonal (s := s) (t := t) (hs.min (s := s) hns • ht.min (s := t) hnt) ⋯ ↔
      Membership.mem (γ := Finset (G × P)) {(hs.min (s := s) hns, ht.min (s := t) hnt)} (a, b)
⊢ SMulAntidiagonal (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.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
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) ∈ SMulAntidiagonal (s := s) (t := t) (hs.min (s := s) hns • ht.min (s := t) hnt) ⋯ ↔
    Membership.mem (γ := Finset (G × P)) {(hs.min (s := s) hns, ht.min (s := t) hnt)} (a, b)

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

Premises used: Finset.mem_singleton, Prod.ext_iff, Finset.mem_smulAntidiagonal
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
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.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
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 =>
        (SMul.smul_lt_smul_of_lt_of_le hlt <| ht.min_le hnt hat).ne' hst

Premises used: LE.le.eq_of_not_lt, LT.lt.ne', SMul.smul_lt_smul_of_lt_of_le, Set.IsWF.min_le, rfl
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
b : P
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, IsCancelSMul.left_cancel _ _ _ hst⟩

Premises used: IsCancelSMul.left_cancel, And.intro, rfl
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
b : P
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, IsCancelSMul.left_cancel _ _ _ hst⟩
-- Module: Mathlib.Data.Finset.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
s : Set G
t : Set P
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.SMulAntidiagonal
Goal:
G : Type u_1
P : Type u_2
inst : LinearOrder G
inst_1 : LinearOrder P
inst_2 : SMul G P
inst_3 : IsOrderedCancelSMul G P
s : Set G
t : Set P
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.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
a : (i : ι) × α i
⊢ a ∈ s.sigma (α := α) t ↔
    a.fst (β := fun (i : ι) ↦ α i) ∈ s ∧
      Membership.mem (γ := Finset (α (a.fst (β := fun (i : ι) ↦ α i)))) (t (a.fst (β := fun (i : ι) ↦ α i)))
        (a.snd (β := fun (i : ι) ↦ α i))

Tactic:
Multiset.mem_sigma

Premises used: Multiset.sum, Multiset.foldr, Multiset.mem_sigma, Multiset.sigma, Set.Mem, setOf, Multiset.Mem, Multiset.join, Multiset.bind
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ (↑(s.sigma (α := α) t) : Set ((i : ι) × α i)) = (↑s : Set ι).sigma (α := α) fun (i : ι) ↦ (↑(t i) : Set (α i))

Tactic:
Set.ext fun _ => mem_sigma

Premises used: Set.ext, Finset.mem_sigma
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ (s.sigma (α := α) t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty

Tactic:
simp [Finset.Nonempty]

Premises used: Finset.Nonempty
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
contrapose! : (s.sigma (α := α) t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty
⊢ s.sigma (α := α) t = ∅ ↔ ∀ i ∈ s, t i = ∅

Tactic:
contrapose!
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ (s.sigma (α := α) t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty

Tactic:
sigma_nonempty

Premises used: Finset.sigma_nonempty
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ (s.sigma (α := α) t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty

Tactic:
exact sigma_nonempty

Premises used: Finset.sigma_nonempty
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Finset ι
t₁ t₂ : (i : ι) → Finset (α i)
hs : s₁ ⊆ s₂
ht : ∀ (i : ι), t₁ i ⊆ t₂ i
⊢ s₁.sigma (α := α) t₁ ⊆ s₂.sigma (α := α) t₂

Tactic:
fun ⟨i, _⟩ h =>
  let ⟨hi, ha⟩ := mem_sigma.1 h
  mem_sigma.2 ⟨hs hi, ht i ha⟩

Premises used: Iff.mpr, _private.0.Finset.sigma_mono.match_1, _private.0.Finset.sigma_mono.match_2, Membership.mem, Finset.sigma, Finset.mem_sigma, And.intro, Iff.mp, Sigma.mk
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
_ :
  i ∈ (↑s : Set ι) →
    ∀ ⦃y : ι⦄,
      y ∈ (↑s : Set ι) →
        i ≠ y →
          onFun (β := Finset ((x : ι) × α x)) Disjoint (fun (i : ι) ↦ map (Embedding.sigmaMk (β := α) i) (t i)) i y
⊢ i ∈ (↑s : Set ι) →
    ∀ ⦃y : ι⦄,
      y ∈ (↑s : Set ι) →
        i ≠ y →
          onFun (β := Finset ((x : ι) × α x)) Disjoint (fun (i : ι) ↦ map (Embedding.sigmaMk (β := α) i) (t i)) i y

Tactic:
_
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
h : i ∈ (↑s : Set ι)
j : ι
_ :
  j ∈ (↑s : Set ι) →
    i ≠ j → onFun (β := Finset ((x : ι) × α x)) Disjoint (fun (i : ι) ↦ map (Embedding.sigmaMk (β := α) i) (t i)) i j
⊢ j ∈ (↑s : Set ι) →
    i ≠ j → onFun (β := Finset ((x : ι) × α x)) Disjoint (fun (i : ι) ↦ map (Embedding.sigmaMk (β := α) i) (t i)) i j

Tactic:
_
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
h : i ∈ (↑s : Set ι)
j : ι
h_1 : j ∈ (↑s : Set ι)
hij : i ≠ j
rw : ∀ ⦃a : (x : ι) × α x⦄, a ∈ map (Embedding.sigmaMk (β := α) i) (t i) → a ∉ map (Embedding.sigmaMk (β := α) j) (t j)
⊢ onFun (β := Finset ((x : ι) × α x)) Disjoint (fun (i : ι) ↦ map (Embedding.sigmaMk (β := α) i) (t i)) i j

Tactic:
rw [Function.onFun, disjoint_left]

Premises used: Function.onFun, Finset.disjoint_left
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
h : i ∈ (↑s : Set ι)
j : ι
h_1 : j ∈ (↑s : Set ι)
hij : i ≠ j
simp_rw : ∀ ⦃a : (x : ι) × α x⦄, (∃ a_1 ∈ t i, Sigma.mk (β := α) i a_1 = a) → ¬∃ a_2 ∈ t j, Sigma.mk (β := α) j a_2 = a
⊢ ∀ ⦃a : (x : ι) × α x⦄, a ∈ map (Embedding.sigmaMk (β := α) i) (t i) → a ∉ map (Embedding.sigmaMk (β := α) j) (t j)

Tactic:
simp_rw [mem_map, Function.Embedding.sigmaMk_apply]

Premises used: Function.Embedding.sigmaMk_apply, Finset.mem_map
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
h : i ∈ (↑s : Set ι)
j : ι
h_1 : j ∈ (↑s : Set ι)
hij : i ≠ j
y : α i
left : y ∈ t i
z : α j
left_1 : z ∈ t j
hz' : Sigma.mk (β := α) j z = Sigma.mk (β := α) i y
⊢ False

Tactic:
hij (congr_arg Sigma.fst hz'.symm)

Premises used: Sigma.fst, congr_arg, Eq.symm
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
h : i ∈ (↑s : Set ι)
j : ι
h_1 : j ∈ (↑s : Set ι)
hij : i ≠ j
y : α i
left : y ∈ t i
z : α j
left_1 : z ∈ t j
hz' : Sigma.mk (β := α) j z = Sigma.mk (β := α) i y
⊢ False

Tactic:
exact hij (congr_arg Sigma.fst hz'.symm)

Premises used: Sigma.fst, congr_arg, Eq.symm
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ s.disjiUnion (fun (i : ι) ↦ map (Embedding.sigmaMk (β := α) i) (t i)) ⋯ = s.sigma (α := α) t

Tactic:
rfl

Premises used: Multiset.map, Multiset.sigma, Finset.sigma, Finset.disjiUnion, rfl
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ((i : ι) × α i)
s : Finset ι
t : (i : ι) → Finset (α i)
h :
  ∀ (x : ι) (y : α x),
    Sigma.mk (β := fun (i : ι) ↦ α i) x y ∈ s.sigma (α := α) t ↔
      Membership.mem (γ := Finset ((i : ι) × α i)) (s.biUnion fun (i : ι) ↦ map (Embedding.sigmaMk (β := α) i) (t i))
        (Sigma.mk (β := fun (i : ι) ↦ α i) x y)
⊢ s.sigma (α := α) t = s.biUnion fun (i : ι) ↦ map (Embedding.sigmaMk (β := α) i) (t i)

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ((i : ι) × α i)
s : Finset ι
t : (i : ι) → Finset (α i)
x : ι
y : α x
⊢ Sigma.mk (β := fun (i : ι) ↦ α i) x y ∈ s.sigma (α := α) t ↔
    Membership.mem (γ := Finset ((i : ι) × α i)) (s.biUnion fun (i : ι) ↦ map (Embedding.sigmaMk (β := α) i) (t i))
      (Sigma.mk (β := fun (i : ι) ↦ α i) x y)

Tactic:
simp [and_left_comm]

Premises used: and_left_comm