awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst : IsEquiv α r
s : Set ι
hs : s.Nonempty
z : α
hz : ∀ (x : ι), x ∈ s → r (f x) z
x : ι
hx : x ∈ s
y : ι
hy : y ∈ s
h : x ≠ y
⊢ (r on f) x y

Tactic:
@IsTrans.trans α r _ (f x) z (f y) (hz _ hx) (symm <| hz _ hy)

Premises used: IsTrans.trans, symm
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst : IsEquiv α r
s : Set ι
hs : s.Nonempty
z : α
hz : ∀ (x : ι), x ∈ s → r (f x) z
x : ι
hx : x ∈ s
y : ι
hy : y ∈ s
h : x ≠ y
⊢ (r on f) x y

Tactic:
exact @IsTrans.trans α r _ (f x) z (f y) (hz _ hx) (symm <| hz _ hy)

Premises used: IsTrans.trans, symm
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
s : Set α
hs : s.Nonempty
f : α → ι
⊢ (s.Pairwise fun (x y : α) ↦ f x = f y) ↔ ∃ (z : ι), ∀ (x : α), x ∈ s → f x = z

Tactic:
hs.pairwise_iff_exists_forall

Premises used: Set.Nonempty.pairwise_iff_exists_forall
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst_1 : IsEquiv ι r
inl : Set.Pairwise ∅ (r on f) ↔ ∃ (z : ι), ∀ (x : α), Membership.mem (γ := Set α) ∅ x → r (f x) z
inr : ∀ (hne : s.Nonempty), s.Pairwise (r on f) ↔ ∃ (z : ι), ∀ (x : α), x ∈ s → r (f x) z
⊢ s.Pairwise (r on f) ↔ ∃ (z : ι), ∀ (x : α), x ∈ s → r (f x) z

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hne)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : Nonempty ι
f : α → ι
r : ι → ι → Prop
inst_1 : IsEquiv ι r
⊢ Set.Pairwise ∅ (r on f) ↔ ∃ (z : ι), ∀ (x : α), Membership.mem (γ := Set α) ∅ x → r (f x) z

Tactic:
simp
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst_1 : IsEquiv ι r
hne : s.Nonempty
⊢ s.Pairwise (r on f) ↔ ∃ (z : ι), ∀ (x : α), x ∈ s → r (f x) z

Tactic:
hne.pairwise_iff_exists_forall

Premises used: Set.Nonempty.pairwise_iff_exists_forall
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst_1 : IsEquiv ι r
hne : s.Nonempty
⊢ s.Pairwise (r on f) ↔ ∃ (z : ι), ∀ (x : α), x ∈ s → r (f x) z

Tactic:
exact hne.pairwise_iff_exists_forall

Premises used: Set.Nonempty.pairwise_iff_exists_forall
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : Nonempty ι
s : Set α
f : α → ι
⊢ (s.Pairwise fun (x y : α) ↦ f x = f y) ↔ ∃ (z : ι), ∀ (x : α), x ∈ s → f x = z

Tactic:
pairwise_iff_exists_forall s f

Premises used: Set.pairwise_iff_exists_forall
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
⊢ (s ∪ t).Pairwise r ↔ s.Pairwise r ∧ t.Pairwise r ∧ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b → r a b ∧ r b a

Tactic:
grind [Set.Pairwise]

Premises used: Set.Pairwise
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
hr : Symmetric r
⊢ (s.Pairwise r ∧ t.Pairwise r ∧ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b → r a b ∧ r b a) ↔
    s.Pairwise r ∧ t.Pairwise r ∧ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b → r a b

Tactic:
simp only [hr.iff, and_self_iff]

Premises used: Symmetric.iff, and_self_iff
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
a : α
⊢ (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ (b : α), b ∈ s → a ≠ b → r a b ∧ r b a

Tactic:
simp only [insert_eq, pairwise_union, pairwise_singleton, true_and, mem_singleton_iff, forall_eq]

Premises used: Set.insert_eq, forall_eq, Set.pairwise_singleton, Set.pairwise_union, Set.mem_singleton_iff, true_and
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
a : α
ha : ¬a ∈ s
b : α
hb : b ∈ s
⊢ a ≠ b → r a b ∧ r b a ↔ r a b ∧ r b a

Tactic:
simp [(ne_of_mem_of_not_mem hb ha).symm]

Premises used: Ne.symm, ne_of_mem_of_not_mem
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
a : α
hs : s.Pairwise r
h : ∀ (b : α), b ∈ s → a ≠ b → r a b ∧ r b a
⊢ (insert a s).Pairwise r

Tactic:
pairwise_insert.2 ⟨hs, h⟩

Premises used: Iff.mpr, Set.pairwise_insert, And.intro
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
a : α
ha : ¬a ∈ s
hs : s.Pairwise r
h : ∀ (b : α), b ∈ s → r a b ∧ r b a
⊢ (insert a s).Pairwise r

Tactic:
(pairwise_insert_of_notMem ha).2 ⟨hs, h⟩

Premises used: Iff.mpr, Set.pairwise_insert_of_notMem, And.intro
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
a : α
hr : Symmetric r
⊢ (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ (b : α), b ∈ s → a ≠ b → r a b

Tactic:
simp only [pairwise_insert, hr.iff a, and_self_iff]

Premises used: Set.pairwise_insert, Symmetric.iff, and_self_iff
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
a : α
hr : Symmetric r
ha : ¬a ∈ s
⊢ (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ (b : α), b ∈ s → r a b

Tactic:
simp only [pairwise_insert_of_notMem ha, hr.iff a, and_self_iff]

Premises used: Set.pairwise_insert_of_notMem, Symmetric.iff, and_self_iff
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
a : α
hs : s.Pairwise r
hr : Symmetric r
h : ∀ (b : α), b ∈ s → a ≠ b → r a b
⊢ (insert a s).Pairwise r

Tactic:
(pairwise_insert_of_symmetric hr).2 ⟨hs, h⟩

Premises used: Iff.mpr, Set.pairwise_insert_of_symmetric, And.intro
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
r : α → α → Prop
a b : α
⊢ Set.Pairwise {a, b} r ↔ a ≠ b → r a b ∧ r b a

Tactic:
simp [pairwise_insert]

Premises used: Set.pairwise_insert
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
r : α → α → Prop
a b : α
hr : Symmetric r
⊢ Set.Pairwise {a, b} r ↔ a ≠ b → r a b

Tactic:
simp [pairwise_insert_of_symmetric hr]

Premises used: Set.pairwise_insert_of_symmetric
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
r : α → α → Prop
⊢ Set.Pairwise univ r ↔ Pairwise r

Tactic:
simp only [Set.Pairwise, Pairwise, mem_univ, forall_const]

Premises used: Set.Pairwise, Pairwise, Set.mem_univ, forall_const
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
s : Set α
⊢ s.Pairwise ⊥ ↔ s.Subsingleton

Tactic:
⟨fun h _a ha _b hb => h.eq ha hb id, fun h => h.pairwise _⟩

Premises used: id, Bot.bot, Set.Subsingleton.pairwise, Iff.intro, Set.Pairwise.eq
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
f : ι → α
s : Set ι
⊢ InjOn f s ↔ s.Pairwise fun (x1 x2 : ι) ↦ f x1 ≠ f x2

Tactic:
simp only [InjOn, Set.Pairwise, not_imp_not]

Premises used: Set.Pairwise, Set.InjOn, not_imp_not
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
s : Set ι
h : s.Pairwise (r on f)
⊢ (f '' s).Pairwise r

Tactic:
forall_mem_image.2 fun _x hx ↦ forall_mem_image.2 fun _y hy hne ↦ h hx hy <| ne_of_apply_ne _ hne

Premises used: Iff.mpr, Set.Pairwise, ne_of_apply_ne, Set.forall_mem_image
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
s : Set ι
h : InjOn f s
⊢ (f '' s).Pairwise r ↔ s.Pairwise (r on f)

Tactic:
simp +contextual [h.eq_iff, Set.Pairwise]

Premises used: Set.InjOn.eq_iff, Set.Pairwise
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
hr : Pairwise (r on f)
⊢ (range f).Pairwise r

Tactic:
image_univ ▸ (pairwise_univ.mpr hr).image

Premises used: Iff.mpr, Set.image_univ, Set.pairwise_univ, Eq.rec, Set.Pairwise.image
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
⊢ (Pairwise fun (x y : (↑s : Type u_1)) ↦ r (↑x : α) (↑y : α)) ↔ s.Pairwise r

Tactic:
simp only [Pairwise, Set.Pairwise, SetCoe.forall, Ne, Subtype.ext_iff]

Premises used: Ne, Set.Pairwise, Subtype.ext_iff, Pairwise, SetCoe.forall
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
s t : Set ι
f : ι → α
ht : t.PairwiseDisjoint f
h : s ⊆ t
⊢ s.PairwiseDisjoint f

Tactic:
Pairwise.mono h ht

Premises used: Set.PairwiseDisjoint, Set.Pairwise.mono
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
s : Set ι
f g : ι → α
hs : s.PairwiseDisjoint f
h : ∀ ⦃i : ι⦄, i ∈ s → g i ≤ f i
⊢ s.PairwiseDisjoint g

Tactic:
fun _a ha _b hb hab => (hs ha hb hab).mono (h ha) (h hb)

Premises used: Set.PairwiseDisjoint, Set.Pairwise, Disjoint.mono
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
s : Set ι
f g : ι → α
hs : s.PairwiseDisjoint f
h : g ≤ f
⊢ s.PairwiseDisjoint g

Tactic:
hs.mono_on fun i _ => h i

Premises used: Set.PairwiseDisjoint.mono_on
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
f : ι → α
⊢ PairwiseDisjoint ∅ f

Tactic:
pairwise_empty _

Premises used: Set.PairwiseDisjoint, Set.pairwise_empty
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
i : ι
f : ι → α
⊢ PairwiseDisjoint {i} f

Tactic:
pairwise_singleton i _

Premises used: Set.PairwiseDisjoint, Set.pairwise_singleton
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
ι : Type u_4
s : Set ι
x : ι
⊢ x ∈ s → ∀ ⦃y : ι⦄, y ∈ s → x ≠ y → onFun (β := Set ι) Disjoint singleton x y

Tactic:
grind
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
s : Set ι
f : ι → α
i : ι
⊢ (insert i s).PairwiseDisjoint f ↔ s.PairwiseDisjoint f ∧ ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (f i) (f j)

Tactic:
pairwise_insert_of_symmetric <| symmetric_disjoint.comap f

Premises used: Set.PairwiseDisjoint, Symmetric.comap, Set.pairwise_insert_of_symmetric, symmetric_disjoint
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
s : Set ι
f : ι → α
i : ι
hi : ¬i ∈ s
⊢ (insert i s).PairwiseDisjoint f ↔ s.PairwiseDisjoint f ∧ ∀ (j : ι), j ∈ s → Disjoint (f i) (f j)

Tactic:
pairwise_insert_of_symmetric_of_notMem (symmetric_disjoint.comap f) hi

Premises used: Set.PairwiseDisjoint, Symmetric.comap, Set.pairwise_insert_of_symmetric_of_notMem, symmetric_disjoint
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
s : Set ι
f : ι → α
hs : s.PairwiseDisjoint f
i : ι
h : ∀ (j : ι), j ∈ s → i ≠ j → Disjoint (f i) (f j)
⊢ (insert i s).PairwiseDisjoint f

Tactic:
pairwiseDisjoint_insert.2 ⟨hs, h⟩

Premises used: Iff.mpr, And.intro, Set.pairwiseDisjoint_insert
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
s : Set ι
f : ι → α
hs : s.PairwiseDisjoint f
i : ι
hi : ¬i ∈ s
h : ∀ (j : ι), j ∈ s → Disjoint (f i) (f j)
⊢ (insert i s).PairwiseDisjoint f

Tactic:
(pairwiseDisjoint_insert_of_notMem hi).2 ⟨hs, h⟩

Premises used: Iff.mpr, Set.pairwiseDisjoint_insert_of_notMem, And.intro
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
s : Set ι
f : ι → α
hs : s.PairwiseDisjoint f
g : ι → ι
hg : f ∘ g ≤ f
a : ι
ha : a ∈ s
b : ι
hb : b ∈ s
h : g a ≠ g b
⊢ (Disjoint on f) (g a) (g b)

Tactic:
(hs ha hb <| ne_of_apply_ne _ h).mono (hg a) (hg b)

Premises used: ne_of_apply_ne, Disjoint.mono
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
s : Set ι
f : ι → α
hs : s.PairwiseDisjoint f
g : ι → ι
hg : f ∘ g ≤ f
a : ι
ha : a ∈ s
b : ι
hb : b ∈ s
h : g a ≠ g b
⊢ (Disjoint on f) (g a) (g b)

Tactic:
exact (hs ha hb <| ne_of_apply_ne _ h).mono (hg a) (hg b)

Premises used: ne_of_apply_ne, Disjoint.mono
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst : PartialOrder α
inst_1 : OrderBot α
f : ι → α
g : ι' → ι
s : Set ι'
h : InjOn g s
⊢ (g '' s).PairwiseDisjoint f ↔ s.PairwiseDisjoint (f ∘ g)

Tactic:
h.pairwise_image

Premises used: Set.PairwiseDisjoint, Set.InjOn.pairwise_image
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
s : Set ι
f : ι → α
g : (↑s : Type u_4) → ι
hg : ∀ (i : (↑s : Type u_4)), f (g i) ≤ f (↑i : ι)
ht : s.PairwiseDisjoint f
x y : (↑s : Type u_4)
hxy : g x ≠ g y
⊢ (Disjoint on f) (g x) (g y)

Tactic:
((ht x.2 y.2) fun h => hxy <| congr_arg g <| Subtype.ext h).mono (hg x) (hg y)

Premises used: congr_arg, Disjoint.mono, Subtype.property, Subtype.ext
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
s : Set ι
f : ι → α
g : (↑s : Type u_4) → ι
hg : ∀ (i : (↑s : Type u_4)), f (g i) ≤ f (↑i : ι)
ht : s.PairwiseDisjoint f
x y : (↑s : Type u_4)
hxy : g x ≠ g y
⊢ (Disjoint on f) (g x) (g y)

Tactic:
exact ((ht x.2 y.2) fun h => hxy <| congr_arg g <| Subtype.ext h).mono (hg x) (hg y)

Premises used: congr_arg, Disjoint.mono, Subtype.property, Subtype.ext
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
s t : Set ι
f : ι → α
⊢ (s ∪ t).PairwiseDisjoint f ↔
    s.PairwiseDisjoint f ∧ t.PairwiseDisjoint f ∧ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ t → i ≠ j → Disjoint (f i) (f j)

Tactic:
pairwise_union_of_symmetric <| symmetric_disjoint.comap f

Premises used: Set.PairwiseDisjoint, Symmetric.comap, Set.pairwise_union_of_symmetric, symmetric_disjoint
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
s t : Set ι
f : ι → α
hs : s.PairwiseDisjoint f
ht : t.PairwiseDisjoint f
h : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ t → i ≠ j → Disjoint (f i) (f j)
⊢ (s ∪ t).PairwiseDisjoint f

Tactic:
pairwiseDisjoint_union.2 ⟨hs, ht, h⟩

Premises used: Iff.mpr, And.intro, Set.pairwiseDisjoint_union
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
s : Set ι
f : ι → α
hs : s.PairwiseDisjoint f
i j : ι
hi : i ∈ s
hj : j ∈ s
h : ¬Disjoint (f i) (f j)
⊢ i = j

Tactic:
hs.eq hi hj h

Premises used: Set.Pairwise.eq
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
s : Set ι
f : ι → α
h : s.PairwiseDisjoint f
i j : ι
hi : i ∈ s
hj : j ∈ s
rw : ¬Disjoint (f i) (f j) → i = j
⊢ i = j ∨ Disjoint (f i) (f j)

Tactic:
rw [or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
s : Set ι
f : ι → α
h : s.PairwiseDisjoint f
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ¬Disjoint (f i) (f j) → i = j

Tactic:
h.elim hi hj

Premises used: Set.PairwiseDisjoint.elim
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
s : Set ι
f : ι → α
h : s.PairwiseDisjoint f
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ¬Disjoint (f i) (f j) → i = j

Tactic:
exact h.elim hi hj

Premises used: Set.PairwiseDisjoint.elim
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_6
β : Type u_7
f : α → Set β
⊢ (range f).PairwiseDisjoint id ↔ ∀ (x y : α), f x ≠ f y → Disjoint (f x) (f y)

Tactic:
aesop (add simp [PairwiseDisjoint, Set.Pairwise])

Premises used: Set.PairwiseDisjoint, Set.Pairwise
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
f : ι → α
h : Pairwise (Disjoint on f)
s : Set ι
⊢ s.PairwiseDisjoint f

Tactic:
h.set_pairwise s

Premises used: Set.PairwiseDisjoint, Pairwise.set_pairwise
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set ι
f : ι → α
hs : s.PairwiseDisjoint f
i j : ι
hi : i ∈ s
hj : j ∈ s
h : f i ⊓ f j ≠ ⊥
⊢ i = j

Tactic:
(hs.elim hi hj) fun hij => h hij.eq_bot

Premises used: Set.PairwiseDisjoint.elim, Disjoint.eq_bot
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set ι
f : ι → α
hs : s.PairwiseDisjoint f
i j : ι
hi : i ∈ s
hj : j ∈ s
hf : f i ≠ ⊥
hij : f i ≤ f j
⊢ i = j

Tactic:
(hs.elim' hi hj) fun h => hf <| (inf_of_le_left hij).symm.trans h

Premises used: inf_of_le_left, Set.PairwiseDisjoint.elim', Eq.symm, Eq.trans
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
ι : Type u_4
⊢ PairwiseDisjoint (α := Set ι) (range singleton) id

Tactic:
Pairwise.range_pairwise fun _ _ => disjoint_singleton.2

Premises used: Iff.mpr, Pairwise.range_pairwise, Set.PairwiseDisjoint, Set.disjoint_singleton
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
f : ι → α
s : Set α
⊢ PairwiseDisjoint.{u_4, u_1} (α := Set ι) s fun (a : α) ↦ f ⁻¹' {a}

Tactic:
fun _a _ _b _ h => disjoint_iff_inf_le.mpr fun _i ⟨hia, hib⟩ => h <| (Eq.symm hia).trans hib

Premises used: Iff.mpr, Set.PairwiseDisjoint, Membership.mem, Bot.bot, Set.Pairwise, _private.0.Set.pairwiseDisjoint_fiber.match_1, disjoint_iff_inf_le, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
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 <| not_disjoint_iff.2 ⟨a, hai, haj⟩

Premises used: Iff.mpr, Set.not_disjoint_iff, Set.PairwiseDisjoint.elim, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
ι' : Type u_5
s : Set ι
t : Set ι'
f : ι → Set α
g : ι' → Set β
hs : s.PairwiseDisjoint f
ht : t.PairwiseDisjoint g
⊢ (s ×ˢ t).PairwiseDisjoint (α := Set (α × β)) fun (i : ι × ι') ↦ f i.1 ×ˢ g i.2

Tactic:
fun ⟨_, _⟩ ⟨hi, hi'⟩ ⟨_, _⟩ ⟨hj, hj'⟩ hij =>
  disjoint_left.2 fun ⟨_, _⟩ ⟨hai, hbi⟩ ⟨haj, hbj⟩ =>
    hij <| Prod.ext (hs.elim_set hi hj _ hai haj) <| ht.elim_set hi' hj' _ hbi hbj

Premises used: Iff.mpr, False, _private.0.Set.PairwiseDisjoint.prod.match_1, Function.onFun, SProd.sprod, Set.disjoint_left, Set.PairwiseDisjoint, _private.0.Set.PairwiseDisjoint.prod.match_2, Disjoint, Prod.mk, Set.Pairwise, Prod.fst, _private.0.Set.PairwiseDisjoint.prod.match_3, Prod.ext, _private.0.Set.PairwiseDisjoint.prod.match_5, Prod.snd, Set.PairwiseDisjoint.elim_set, _private.0.Set.PairwiseDisjoint.prod.match_4
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
ι : Type u_4
ι' : ι → Type u_6
α : ι → Type u_7
s : (i : ι) → Set (ι' i)
f : (i : ι) → ι' i → Set (α i)
hs : ∀ (i : ι), (s i).PairwiseDisjoint (f i)
⊢ (pi (α := ι') univ s).PairwiseDisjoint (α := Set ((i : ι) → α i)) fun (I : (i : ι) → ι' i) ↦
    pi (α := fun (i : ι) ↦ α i) univ fun (i : ι) ↦ f i (I i)

Tactic:
fun _ hI _ hJ hIJ =>
  disjoint_left.2 fun a haI haJ =>
    hIJ <|
      funext fun i =>
        (hs i).elim_set (hI i trivial) (hJ i trivial) (a i) (haI i trivial) (haJ i trivial)

Premises used: Iff.mpr, trivial, Set.disjoint_left, Set.PairwiseDisjoint, Set.Pairwise, funext, Set.PairwiseDisjoint.elim_set
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
⊢ (PairwiseDisjoint.{u_3, u_1} (α := Set γ) s fun (a : α) ↦ f a '' t) ↔
    InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)

Tactic:
⟨fun hs x hx y hy (h : f _ _ = _) => ?_, fun hs x hx y hy h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
refine_1 :
  ∀ (hs : PairwiseDisjoint.{u_3, u_1} (α := Set γ) s fun (a : α) ↦ f a '' t) (x : α × β) (hx : x ∈ s ×ˢ t) (y : α × β)
    (hy : y ∈ s ×ˢ t) (h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y), x = y
refine_2 :
  ∀ (hs : InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)) (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s) (h : x ≠ y),
    onFun.{u_1 + 1, u_3 + 1, 1} (β := Set γ) Disjoint (fun (a : α) ↦ f a '' t) x y
⊢ (PairwiseDisjoint.{u_3, u_1} (α := Set γ) s fun (a : α) ↦ f a '' t) ↔
    InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)

Tactic:
refine ⟨fun hs x hx y hy (h : f _ _ = _) => ?_, fun hs x hx y hy h => ?_⟩
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : PairwiseDisjoint.{u_3, u_1} (α := Set γ) s fun (a : α) ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
this : x.1 = y.1
rw rw₁ : (fun (p : α × β) ↦ f p.1 p.2) y = f y.1 y.2
⊢ (fun (p : α × β) ↦ f p.1 p.2) y = f x.1 y.2

Tactic:
rw [this]
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : PairwiseDisjoint.{u_3, u_1} (α := Set γ) s fun (a : α) ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
this : x.1 = y.1
⊢ x = y

Tactic:
exact Prod.ext this (hf _ hx.1 <| h.trans <| by rw [this])

Premises used: And.left, Prod.ext, Eq.trans
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : PairwiseDisjoint.{u_3, u_1} (α := Set γ) s fun (a : α) ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
refine_1 : x.1 = y.1
⊢ x = y

Tactic:
suffices x.1 = y.1 by exact Prod.ext this (hf _ hx.1 <| h.trans <| by rw [this])
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : PairwiseDisjoint.{u_3, u_1} (α := Set γ) s fun (a : α) ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
⊢ x.1 = y.1

Tactic:
hs.elim hx.1 hy.1 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.2, ?_⟩)

Premises used: Iff.mpr, Set.not_disjoint_iff, And.right, And.left, Set.mem_image_of_mem, Set.PairwiseDisjoint.elim, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : PairwiseDisjoint.{u_3, u_1} (α := Set γ) s fun (a : α) ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
refine_1 : f x.1 x.2 ∈ f y.1 '' t
⊢ x.1 = y.1

Tactic:
refine hs.elim hx.1 hy.1 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.2, ?_⟩)

Premises used: Iff.mpr, Set.not_disjoint_iff, And.right, And.left, Set.mem_image_of_mem, Set.PairwiseDisjoint.elim, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : PairwiseDisjoint.{u_3, u_1} (α := Set γ) s fun (a : α) ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
refine_1 : (fun (p : α × β) ↦ f p.1 p.2) y ∈ f y.1 '' t
⊢ f x.1 x.2 ∈ f y.1 '' t

Tactic:
rw [h]
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : PairwiseDisjoint.{u_3, u_1} (α := Set γ) s fun (a : α) ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
⊢ (fun (p : α × β) ↦ f p.1 p.2) y ∈ f y.1 '' t

Tactic:
mem_image_of_mem _ hy.2

Premises used: Set.Mem, And.right, Set.mem_image_of_mem
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : PairwiseDisjoint.{u_3, u_1} (α := Set γ) s fun (a : α) ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
⊢ (fun (p : α × β) ↦ f p.1 p.2) y ∈ f y.1 '' t

Tactic:
exact mem_image_of_mem _ hy.2

Premises used: And.right, Set.mem_image_of_mem