awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
inst : DecidableEq (Option α)
inst_1 : DecidableEq α
s t : Finset (Option α)
h :
  ∀ (a : α),
    Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) (s ∪ t) : Finset α) a ↔
      Membership.mem (γ := Finset α)
        ((eraseNone : (a : Finset (Option α)) → Finset α) s ∪ (eraseNone : (a : Finset (Option α)) → Finset α) t :
          Finset α)
        a
⊢ Eq (α := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) (s ∪ t) : Finset α)
    ((eraseNone : (a : Finset (Option α)) → Finset α) s ∪ (eraseNone : (a : Finset (Option α)) → Finset α) t : Finset α)

Tactic:
ext
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
inst : DecidableEq (Option α)
inst_1 : DecidableEq α
s t : Finset (Option α)
a : α
⊢ Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) (s ∪ t) : Finset α) a ↔
    Membership.mem (γ := Finset α)
      ((eraseNone : (a : Finset (Option α)) → Finset α) s ∪ (eraseNone : (a : Finset (Option α)) → Finset α) t :
        Finset α)
      a

Tactic:
simp
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
inst : DecidableEq (Option α)
inst_1 : DecidableEq α
s t : Finset (Option α)
h :
  ∀ (a : α),
    Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) (s ∩ t) : Finset α) a ↔
      Membership.mem (γ := Finset α)
        ((eraseNone : (a : Finset (Option α)) → Finset α) s ∩ (eraseNone : (a : Finset (Option α)) → Finset α) t :
          Finset α)
        a
⊢ Eq (α := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) (s ∩ t) : Finset α)
    ((eraseNone : (a : Finset (Option α)) → Finset α) s ∩ (eraseNone : (a : Finset (Option α)) → Finset α) t : Finset α)

Tactic:
ext
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
inst : DecidableEq (Option α)
inst_1 : DecidableEq α
s t : Finset (Option α)
a : α
⊢ Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) (s ∩ t) : Finset α) a ↔
    Membership.mem (γ := Finset α)
      ((eraseNone : (a : Finset (Option α)) → Finset α) s ∩ (eraseNone : (a : Finset (Option α)) → Finset α) t :
        Finset α)
      a

Tactic:
simp
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
h :
  ∀ (a : α),
    Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) ∅ : Finset α) a ↔
      Membership.mem (γ := Finset α) ∅ a
⊢ Eq.{u_1 + 1} (α := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) ∅ : Finset α) (∅ : Finset α)

Tactic:
ext
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
a : α
⊢ Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) ∅ : Finset α) a ↔
    Membership.mem (γ := Finset α) ∅ a

Tactic:
simp
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
h :
  ∀ (a : α),
    Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) {none} : Finset α) a ↔
      Membership.mem (γ := Finset α) ∅ a
⊢ Eq (α := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) {none} : Finset α) (∅ : Finset α)

Tactic:
ext
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
a : α
⊢ Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) {none} : Finset α) a ↔
    Membership.mem (γ := Finset α) ∅ a

Tactic:
simp
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
inst : DecidableEq (Option α)
s : Finset (Option α)
h :
  Membership.mem (γ := Finset (Option α)) (image some ((eraseNone : (a : Finset (Option α)) → Finset α) s)) none ↔
    none ∈ s.erase none
h₁ :
  ∀ (x : α),
    Membership.mem (γ := Finset (Option α)) (image some ((eraseNone : (a : Finset (Option α)) → Finset α) s)) (some x) ↔
      some x ∈ s.erase none
⊢ image some ((eraseNone : (a : Finset (Option α)) → Finset α) s) = s.erase none

Tactic:
ext (_ | x)
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
inst : DecidableEq (Option α)
s : Finset (Option α)
⊢ Membership.mem (γ := Finset (Option α)) (image some ((eraseNone : (a : Finset (Option α)) → Finset α) s)) none ↔
    none ∈ s.erase none

Tactic:
simp
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
inst : DecidableEq (Option α)
s : Finset (Option α)
x : α
⊢ Membership.mem (γ := Finset (Option α)) (image some ((eraseNone : (a : Finset (Option α)) → Finset α) s)) (some x) ↔
    some x ∈ s.erase none

Tactic:
simp
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
inst : DecidableEq (Option α)
s : Finset (Option α)
rw :
  image (α := α) (⇑Embedding.some : (a : α) → Option α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) =
    s.erase none
rw₁ : image some ((eraseNone : (a : Finset (Option α)) → Finset α) s) = s.erase none
rw₂ rw₃ : s.erase none = s.erase none
⊢ map Embedding.some ((eraseNone : (a : Finset (Option α)) → Finset α) s) = s.erase none

Tactic:
rw [map_eq_image, Embedding.some_apply, image_some_eraseNone]

Premises used: Finset.image_some_eraseNone, Finset.map_eq_image, Function.Embedding.some_apply
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
inst : DecidableEq (Option α)
s : Finset (Option α)
h :
  Membership.mem (γ := Finset (Option α))
      ((insertNone : (a : Finset α) → Finset (Option α))
          ((eraseNone : (a : Finset (Option α)) → Finset α) s : Finset α) :
        Finset (Option α))
      none ↔
    none ∈ insert none s
h₁ :
  ∀ (x : α),
    Membership.mem (γ := Finset (Option α))
        ((insertNone : (a : Finset α) → Finset (Option α))
            ((eraseNone : (a : Finset (Option α)) → Finset α) s : Finset α) :
          Finset (Option α))
        (some x) ↔
      some x ∈ insert none s
⊢ (insertNone : (a : Finset α) → Finset (Option α)) ((eraseNone : (a : Finset (Option α)) → Finset α) s : Finset α) =
    insert none s

Tactic:
ext (_ | x)
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
inst : DecidableEq (Option α)
s : Finset (Option α)
⊢ Membership.mem (γ := Finset (Option α))
      ((insertNone : (a : Finset α) → Finset (Option α))
          ((eraseNone : (a : Finset (Option α)) → Finset α) s : Finset α) :
        Finset (Option α))
      none ↔
    none ∈ insert none s

Tactic:
simp
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
inst : DecidableEq (Option α)
s : Finset (Option α)
x : α
⊢ Membership.mem (γ := Finset (Option α))
      ((insertNone : (a : Finset α) → Finset (Option α))
          ((eraseNone : (a : Finset (Option α)) → Finset α) s : Finset α) :
        Finset (Option α))
      (some x) ↔
    some x ∈ insert none s

Tactic:
simp
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset α
h :
  ∀ (a : α),
    Membership.mem (γ := Finset α)
        ((eraseNone : (a : Finset (Option α)) → Finset α)
            ((insertNone : (a : Finset α) → Finset (Option α)) s : Finset (Option α)) :
          Finset α)
        a ↔
      a ∈ s
⊢ (eraseNone : (a : Finset (Option α)) → Finset α)
      ((insertNone : (a : Finset α) → Finset (Option α)) s : Finset (Option α)) =
    s

Tactic:
ext
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset α
a : α
⊢ Membership.mem (γ := Finset α)
      ((eraseNone : (a : Finset (Option α)) → Finset α)
          ((insertNone : (a : Finset α) → Finset (Option α)) s : Finset (Option α)) :
        Finset α)
      a ↔
    a ∈ s

Tactic:
simp
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
inst : DecidableEq (Option α)
s : Finset (Option α)
rw :
  card.{u_1} (α := Option α) (map Embedding.some ((eraseNone : (a : Finset (Option α)) → Finset α) s)) = #(s.erase none)
rw₁ rw₂ : #(s.erase none) = #(s.erase none)
⊢ card.{u_1} (α := α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) = #(s.erase none)

Tactic:
rw [← card_map Function.Embedding.some, map_some_eraseNone]

Premises used: Function.Embedding.some, Finset.card_map, Finset.map_some_eraseNone
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset (Option α)
rw : #(s.erase none) ≤ #s
⊢ card.{u_1} (α := α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) ≤ #s

Tactic:
rw [card_eraseNone_eq_card_erase]

Premises used: Finset.card_eraseNone_eq_card_erase
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset (Option α)
⊢ #(s.erase none) ≤ #s

Tactic:
apply card_erase_le

Premises used: Finset.card_erase_le
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset (Option α)
rw rw₁ rw₂ : #(s.erase none) ≤ #s
⊢ card.{u_1} (α := α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) ≤ #s

Tactic:
classical
  rw [card_eraseNone_eq_card_erase]
  apply card_erase_le

Premises used: Finset.card_erase_le, Finset.card_eraseNone_eq_card_erase
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset (Option α)
h : none ∈ s
rw : #(s.erase none) = #s - 1
rw₁ rw₂ : #s - 1 = #s - 1
⊢ card.{u_1} (α := α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) = #s - 1

Tactic:
rw [card_eraseNone_eq_card_erase, card_erase_of_mem h]

Premises used: Finset.card_erase_of_mem, Finset.card_eraseNone_eq_card_erase
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset (Option α)
h : none ∈ s
classical : #(s.erase none) = #s - 1
classical₁ classical₂ : #s - 1 = #s - 1
⊢ card.{u_1} (α := α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) = #s - 1

Tactic:
classical rw [card_eraseNone_eq_card_erase, card_erase_of_mem h]

Premises used: Finset.card_eraseNone_eq_card_erase
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset (Option α)
h : none ∉ s
rw : #(s.erase none) = #s
rw₁ rw₂ : #s = #s
⊢ card.{u_1} (α := α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) = #s

Tactic:
rw [card_eraseNone_eq_card_erase, erase_eq_of_notMem h]

Premises used: Finset.erase_eq_of_notMem, Finset.card_eraseNone_eq_card_erase
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset (Option α)
h : none ∉ s
classical : #(s.erase none) = #s
classical₁ classical₂ : #s = #s
⊢ card.{u_1} (α := α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) = #s

Tactic:
classical rw [card_eraseNone_eq_card_erase, erase_eq_of_notMem h]

Premises used: Finset.card_eraseNone_eq_card_erase
-- Module: Mathlib.Data.Finset.Order
Goal:
α : Type u
r : α → α → Prop
inst : IsTrans α r
ι : Type u_1
hι : Nonempty ι
f : ι → α
D : Directed r f
s : Finset ι
z x : ι
⊢ Membership.mem (γ := Multiset ι) 0 x → r (f x) (f z)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Order
Goal:
α : Type u
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsDirectedOrder α
s : Finset α
⊢ ∃ (M : α), ∀ i ∈ s, i ≤ M

Tactic:
directed_id.finset_le _

Premises used: Directed.finset_le, directed_id
-- Module: Mathlib.Data.Finset.PImage
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
x : α
⊢ x ∈ o.toFinset ↔ x ∈ o

Tactic:
simp [toFinset]

Premises used: Part.toFinset
-- Module: Mathlib.Data.Finset.PImage
Goal:
α : Type u_1
inst : Decidable (Dom.{u_1} (α := α) none)
⊢ Eq.{u_1 + 1} (α := Finset α) (toFinset none) ∅

Tactic:
simp [toFinset]

Premises used: Part.toFinset
-- Module: Mathlib.Data.Finset.PImage
Goal:
α : Type u_1
a : α
inst : Decidable (some a).Dom
⊢ (some a).toFinset = {a}

Tactic:
simp [toFinset]

Premises used: Part.toFinset
-- Module: Mathlib.Data.Finset.PImage
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
⊢ (↑o.toFinset : Set α) = {x : α | x ∈ o}

Tactic:
Set.ext fun _ => mem_toFinset

Premises used: Set.ext, Part.mem_toFinset
-- Module: Mathlib.Data.Finset.PImage
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α →. β
inst_1 : (x : α) → Decidable (f x).Dom
s : Finset α
b : β
⊢ b ∈ pimage f s ↔ ∃ a ∈ s, b ∈ f a

Tactic:
simp [pimage]

Premises used: Finset.pimage
-- Module: Mathlib.Data.Finset.PImage
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α →. β
inst_1 : (x : α) → Decidable (f x).Dom
s : Finset α
⊢ (↑(pimage f s) : Set β) = f.image (↑s : Set α)

Tactic:
Set.ext fun _ => mem_pimage

Premises used: Set.ext, Finset.mem_pimage
-- Module: Mathlib.Data.Finset.PImage
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
f : α → β
inst_1 : (x : α) → Decidable (Part.some (f x)).Dom
h : ∀ (a : β), Membership.mem (γ := Finset β) (pimage (fun (x : α) ↦ Part.some (f x)) s) a ↔ a ∈ image f s
⊢ pimage (fun (x : α) ↦ Part.some (f x)) s = image f s

Tactic:
ext
-- Module: Mathlib.Data.Finset.PImage
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
f : α → β
inst_1 : (x : α) → Decidable (Part.some (f x)).Dom
a : β
⊢ Membership.mem (γ := Finset β) (pimage (fun (x : α) ↦ Part.some (f x)) s) a ↔ a ∈ image f s

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.Finset.PImage
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f g : α →. β
inst_1 : (x : α) → Decidable (f x).Dom
inst_2 : (x : α) → Decidable (g x).Dom
s t : Finset α
h₁ : s = t
h₂ : ∀ x ∈ t, f x = g x
⊢ pimage f s = pimage g t

Tactic:
aesop
-- Module: Mathlib.Data.Finset.PImage
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α →. β
inst_1 : (x : α) → Decidable (f x).Dom
s : Finset α
⊢ pimage f s = image (fun (x : ↥({x ∈ s | (f x).Dom})) ↦ (f (↑x : α)).get ⋯) {x ∈ s | (f x).Dom}.attach

Tactic:
aesop (add simp Part.mem_eq)

Premises used: Part.mem_eq
-- Module: Mathlib.Data.Finset.PImage
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α →. β
inst_1 : (x : α) → Decidable (f x).Dom
s t : Finset α
inst_2 : DecidableEq α
⊢ (↑(pimage f (s ∪ t)) : Set β) = (↑(pimage f s ∪ pimage f t) : Set β)

Tactic:
simp only [coe_pimage, coe_union, ← PFun.image_union]

Premises used: PFun.image_union, Finset.coe_pimage, Finset.coe_union
-- Module: Mathlib.Data.Finset.PImage
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α →. β
inst_1 : (x : α) → Decidable (f x).Dom
h : ∀ (a : β), a ∈ pimage f ∅ ↔ Membership.mem (γ := Finset β) ∅ a
⊢ pimage f ∅ = ∅

Tactic:
ext
-- Module: Mathlib.Data.Finset.PImage
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α →. β
inst_1 : (x : α) → Decidable (f x).Dom
a : β
⊢ a ∈ pimage f ∅ ↔ Membership.mem (γ := Finset β) ∅ a

Tactic:
simp
-- Module: Mathlib.Data.Finset.PImage
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α →. β
inst_1 : (x : α) → Decidable (f x).Dom
s : Finset α
t : Finset β
⊢ pimage f s ⊆ t ↔ ∀ x ∈ s, ∀ y ∈ f x, y ∈ t

Tactic:
simp [subset_iff, @forall_comm _ β]

Premises used: forall_comm, Finset.subset_iff
-- Module: Mathlib.Data.Finset.PImage
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α →. β
inst_1 : (x : α) → Decidable (f x).Dom
s t : Finset α
h : s ⊆ t
⊢ pimage f s ⊆ pimage f t

Tactic:
pimage_subset.2 fun x hx _ hy => mem_pimage.2 ⟨x, h hx, hy⟩

Premises used: Iff.mpr, Finset.mem_pimage, Finset.pimage_subset, And.intro, Exists.intro
-- Module: Mathlib.Data.Finset.PImage
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α →. β
inst_1 : (x : α) → Decidable (f x).Dom
s t : Finset α
inst_2 : DecidableEq α
⊢ pimage f (s ∩ t) ⊆ pimage f s ∩ pimage f t

Tactic:
simp only [← coe_subset, coe_pimage, coe_inter, PFun.image_inter]

Premises used: PFun.image_inter, Finset.coe_pimage, Finset.coe_inter, Finset.coe_subset
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
a b : α
h : Ne (α := Finset α) {a} {b}
⊢ Function.onFun (α := Finset α) Disjoint id {a} {b}

Tactic:
disjoint_singleton.2 (ne_of_apply_ne _ h)

Premises used: Iff.mpr, ne_of_apply_ne, Finset.disjoint_singleton
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
a b : α
h : Ne (α := Finset α) {a} {b}
⊢ Function.onFun (α := Finset α) Disjoint id {a} {b}

Tactic:
exact disjoint_singleton.2 (ne_of_apply_ne _ h)

Premises used: Iff.mpr, ne_of_apply_ne, Finset.disjoint_singleton
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
ι : Type u_2
s : Set ι
f : ι → Finset α
hs : s.PairwiseDisjoint f
i j : ι
hi : i ∈ s
hj : j ∈ s
a : α
hai : a ∈ f i
haj : a ∈ f j
⊢ i = j

Tactic:
hs.elim hi hj (Finset.not_disjoint_iff.2 ⟨a, hai, haj⟩)

Premises used: Iff.mpr, Set.PairwiseDisjoint.elim, And.intro, Exists.intro, Finset.not_disjoint_iff
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
ι : Type u_2
inst : SemilatticeInf α
inst_1 : OrderBot α
inst_2 : DecidableEq ι
s : Finset ι
f : ι → α
hs : (↑s : Set ι).PairwiseDisjoint f
g : ι → ι
hf : ∀ (a : ι), f (g a) ≤ f a
rw : (g '' (↑s : Set ι)).PairwiseDisjoint f
⊢ (↑(Finset.image g s) : Set ι).PairwiseDisjoint f

Tactic:
rw [coe_image]

Premises used: Finset.coe_image
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
ι : Type u_2
inst : SemilatticeInf α
inst_1 : OrderBot α
inst_2 : DecidableEq ι
s : Finset ι
f : ι → α
hs : (↑s : Set ι).PairwiseDisjoint f
g : ι → ι
hf : ∀ (a : ι), f (g a) ≤ f a
⊢ (g '' (↑s : Set ι)).PairwiseDisjoint f

Tactic:
hs.image_of_le hf

Premises used: Set.PairwiseDisjoint.image_of_le
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
ι : Type u_2
inst : SemilatticeInf α
inst_1 : OrderBot α
inst_2 : DecidableEq ι
s : Finset ι
f : ι → α
hs : (↑s : Set ι).PairwiseDisjoint f
g : ι → ι
hf : ∀ (a : ι), f (g a) ≤ f a
⊢ (g '' (↑s : Set ι)).PairwiseDisjoint f

Tactic:
exact hs.image_of_le hf

Premises used: Set.PairwiseDisjoint.image_of_le
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
ι : Type u_2
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
hs : (↑s : Set ι).PairwiseDisjoint f
⊢ (↑s.attach : Set ↥s).PairwiseDisjoint (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))

Tactic:
fun i _ j _ hij =>
  hs i.2 j.2 <| mt Subtype.ext hij

Premises used: Set.PairwiseDisjoint, mt, Set.Pairwise, Subtype.property, Subtype.ext
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i) : Set ι).PairwiseDisjoint f
a : ι
ha : Membership.mem (γ := Set ι) (⋃ i ∈ s, (↑(g i) : Set ι)) a
b : ι
hb : Membership.mem (γ := Set ι) (⋃ i ∈ s, (↑(g i) : Set ι)) b
hab : a ≠ b
⊢ ∃ (i : ι') (_ : i ∈ s), a ∈ (↑(g i) : Set ι)

Tactic:
simp_rw [Set.mem_iUnion] at ha hb

Premises used: Set.mem_iUnion
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i) : Set ι).PairwiseDisjoint f
a : ι
ha : Membership.mem (γ := Set ι) (⋃ i ∈ s, (↑(g i) : Set ι)) a
b : ι
hb : Membership.mem (γ := Set ι) (⋃ i ∈ s, (↑(g i) : Set ι)) b
hab : a ≠ b
ha₁ : ∃ (i : ι') (_ : i ∈ s), a ∈ (↑(g i) : Set ι)
⊢ ∃ (i : ι') (_ : i ∈ s), b ∈ (↑(g i) : Set ι)

Tactic:
simp_rw [Set.mem_iUnion] at ha hb

Premises used: Set.mem_iUnion
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i) : Set ι).PairwiseDisjoint f
a b : ι
hab : a ≠ b
ha : ∃ (i : ι') (_ : i ∈ s), a ∈ (↑(g i) : Set ι)
hb : ∃ (i : ι') (_ : i ∈ s), b ∈ (↑(g i) : Set ι)
obtain : ∀ (c : ι') (hc : c ∈ s) (ha : a ∈ (↑(g c) : Set ι)), Function.onFun Disjoint f a b
⊢ Function.onFun Disjoint f a b

Tactic:
obtain ⟨c, hc, ha⟩ := ha
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i) : Set ι).PairwiseDisjoint f
a b : ι
hab : a ≠ b
hb : ∃ (i : ι') (_ : i ∈ s), b ∈ (↑(g i) : Set ι)
c : ι'
hc : c ∈ s
ha : a ∈ (↑(g c) : Set ι)
obtain : ∀ (d : ι') (hd : d ∈ s) (hb : b ∈ (↑(g d) : Set ι)), Function.onFun Disjoint f a b
⊢ Function.onFun Disjoint f a b

Tactic:
obtain ⟨d, hd, hb⟩ := hb
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i) : Set ι).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ (↑(g c) : Set ι)
d : ι'
hd : d ∈ s
hb : b ∈ (↑(g d) : Set ι)
inl : ∀ (hcd : g c = g d), Function.onFun Disjoint f a b
inr : ∀ (hcd : g c ≠ g d), Function.onFun Disjoint f a b
⊢ Function.onFun Disjoint f a b

Tactic:
obtain hcd | hcd := eq_or_ne (g c) (g d)

Premises used: eq_or_ne
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i) : Set ι).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ (↑(g c) : Set ι)
d : ι'
hd : d ∈ s
hb : b ∈ (↑(g d) : Set ι)
hcd : g c = g d
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (ha : a ∈ (↑(g d) : Set ι)) (hd : d ∈ s) (hb : b ∈ (↑(g d) : Set ι)) (hcd : g c = g d), a ∈ (↑(g d) : Set ι)
⊢ a ∈ (↑(g d) : Set ι)

Tactic:
rwa [hcd] at ha
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i) : Set ι).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ (↑(g c) : Set ι)
d : ι'
hd : d ∈ s
hb : b ∈ (↑(g d) : Set ι)
hcd : g c = g d
⊢ Function.onFun Disjoint f a b

Tactic:
exact hg d hd (by rwa [hcd] at ha) hb hab
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i) : Set ι).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ (↑(g c) : Set ι)
d : ι'
hd : d ∈ s
hb : b ∈ (↑(g d) : Set ι)
hcd : g c ≠ g d
⊢ Function.onFun Disjoint f a b

Tactic:
(hs hc hd (ne_of_apply_ne _ hcd)).mono (Finset.le_sup ha) (Finset.le_sup hb)

Premises used: ne_of_apply_ne, Disjoint.mono, Finset.le_sup
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i) : Set ι).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ (↑(g c) : Set ι)
d : ι'
hd : d ∈ s
hb : b ∈ (↑(g d) : Set ι)
hcd : g c ≠ g d
⊢ Function.onFun Disjoint f a b

Tactic:
exact (hs hc hd (ne_of_apply_ne _ hcd)).mono (Finset.le_sup ha) (Finset.le_sup hb)

Premises used: ne_of_apply_ne, Disjoint.mono, Finset.le_sup
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
l : List α
hl : (↑l.toFinset : Set α).Pairwise r
hn : l.Nodup
⊢ Set.Pairwise {a : α | a ∈ l} r

Tactic:
rw [coe_toFinset] at hl

Premises used: List.coe_toFinset
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
l : List α
hl : (↑l.toFinset : Set α).Pairwise r
hn : l.Nodup
hl₁ : Set.Pairwise {a : α | a ∈ l} r
⊢ l.Nodup

Tactic:
rw [coe_toFinset] at hl

Premises used: List.coe_toFinset
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
l : List α
hl : Set.Pairwise {a : α | a ∈ l} r
hn : l.Nodup
⊢ Pairwise r l

Tactic:
hn.pairwise_of_set_pairwise hl

Premises used: List.Nodup.pairwise_of_set_pairwise
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
l : List α
hl : Set.Pairwise {a : α | a ∈ l} r
hn : l.Nodup
⊢ Pairwise r l

Tactic:
exact hn.pairwise_of_set_pairwise hl

Premises used: List.Nodup.pairwise_of_set_pairwise
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
l : List α
hn : l.Nodup
hs : Symmetric r
this : Std.Symm r := ⋯
rw : Set.Pairwise {a : α | a ∈ l} r ↔ Pairwise r l
rw₁ rw₂ : Pairwise r l ↔ Pairwise r l
⊢ (↑l.toFinset : Set α).Pairwise r ↔ Pairwise r l

Tactic:
rw [coe_toFinset, hn.pairwise_coe]

Premises used: List.coe_toFinset, List.Nodup.pairwise_coe
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_5
ι : Type u_6
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : DecidableEq ι
l : List ι
f : ι → α
hl : (↑l.toFinset : Set ι).PairwiseDisjoint f
hn : l.Nodup
⊢ Pairwise (_root_.Disjoint on f) l

Tactic:
pairwise_of_coe_toFinset_pairwise hl hn

Premises used: List.pairwise_of_coe_toFinset_pairwise