awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
ι : Sort u_1
f : ι → α
⊢ Function.Bijective (rangeFactorization f) ↔ Function.Injective f

Tactic:
simp [Function.Bijective]

Premises used: Function.Bijective
-- Module: Mathlib.Data.Set.Operations
Goal:
ι : Sort u_2
α : Type u_3
f : ι → α
a b : ι
⊢ rangeFactorization f a = rangeFactorization f b ↔ f a = f b

Tactic:
simp [Set.rangeFactorization]

Premises used: Set.rangeFactorization
-- Module: Mathlib.Data.Set.Operations
Goal:
ι : Sort u_2
α : Type u_3
f : ι → α
a : ι
b : (↑(range f) : Type u_3)
rw : Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f a) ⋯ = b ↔ f a = (↑b : α)
rw₁ :
  Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f a) ⋯ = Subtype.mk (p := fun (a : α) ↦ a ∈ range f) (↑b : α) ⋯ ↔
    f a = (↑(Subtype.mk (p := fun (a : α) ↦ a ∈ range f) (↑b : α) ⋯) : α)
rw₂ rw₃ :
  (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f a) ⋯) : α) =
      (↑(Subtype.mk (p := fun (a : α) ↦ a ∈ range f) (↑b : α) ⋯) : α) ↔
    f a = (↑(Subtype.mk (p := fun (a : α) ↦ a ∈ range f) (↑b : α) ⋯) : α)
⊢ rangeFactorization f a = b ↔ f a = (↑b : α)

Tactic:
rw [Set.rangeFactorization, ← b.coe_eta b.2, Subtype.ext_iff]

Premises used: Subtype.ext_iff, Subtype.coe_eta, Set.rangeFactorization, Subtype.property
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
f : α → β
x : (↑(range f) : Type v)
⊢ f (rangeSplitting f x) = (↑x : β)

Tactic:
x.2.choose_spec

Premises used: Exists.choose_spec, Set.rangeSplitting, Subtype.property
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
f : α → β
h : ∀ (x : (↑(range f) : Type v)), (f ∘ rangeSplitting f) x = (↑x : β)
⊢ f ∘ rangeSplitting f = Subtype.val (p := fun (x : β) ↦ x ∈ range f)

Tactic:
ext
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
f : α → β
x : (↑(range f) : Type v)
h : f (rangeSplitting f x) = (↑x : β)
⊢ (f ∘ rangeSplitting f) x = (↑x : β)

Tactic:
simp only [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
f : α → β
x : (↑(range f) : Type v)
⊢ f (rangeSplitting f x) = (↑x : β)

Tactic:
apply apply_rangeSplitting

Premises used: Set.apply_rangeSplitting
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
f : α → β
p : β → Prop
h : ∀ (a : α), p (f a)
⊢ range (Subtype.coind f (p := p) h) = Subtype.val (p := p) ⁻¹' range f

Tactic:
simp [Set.ext_iff, Subtype.ext_iff]

Premises used: Subtype.ext_iff, Set.ext_iff
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
s : Set α
t : Set β
⊢ s ×ˢ t = Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, Set.preimage, rfl
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
s : Set α
t : Set β
p : α × β
⊢ (p ∈ s ×ˢ t) = (p.fst ∈ s ∧ p.snd ∈ t)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, rfl
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
s : Set α
t : Set β
p : α × β
⊢ p ∈ s ×ˢ t ↔ p.fst ∈ s ∧ p.snd ∈ t

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.prod
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
a : α
b : β
s : Set α
t : Set β
⊢ ((a, b) ∈ s ×ˢ t) = (a ∈ s ∧ b ∈ t)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, rfl
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
a : α
b : β
s : Set α
t : Set β
ha : a ∈ s
hb : b ∈ t
⊢ (a, b) ∈ s ×ˢ t

Tactic:
⟨ha, hb⟩

Premises used: Set.Mem, setOf, Set.prod, And.intro
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
γ : Type w
f : α → γ
s : Set α
t : Set β
⊢ (f '' s) ×ˢ t = (fun (x : α × β) ↦ (f x.fst, x.snd)) '' s ×ˢ t

Tactic:
aesop
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
γ : Type w
f : α → γ
s : Set α
t : Set β
⊢ t ×ˢ (f '' s) = (fun (x : β × α) ↦ (x.fst, f x.snd)) '' t ×ˢ s

Tactic:
aesop
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
x : α
⊢ (x, x) ∈ diagonal α

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.diagonal, rfl
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
x : α × α
⊢ x ∈ diagonal α ↔ x.fst = x.snd

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.diagonal
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
x : α × α
s : Set α
⊢ x ∈ s.offDiag ↔ x.fst ∈ s ∧ x.snd ∈ s ∧ x.fst ≠ x.snd

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.offDiag
-- Module: Mathlib.Data.Set.Operations
Goal:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ s.pi (α := α) t ↔ ∀ (i : ι), i ∈ s → f i ∈ t i

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.pi
-- Module: Mathlib.Data.Set.Operations
Goal:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ pi (α := α) univ t ↔ ∀ (i : ι), f i ∈ t i

Tactic:
simp
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
⊢ MapsTo f s (f '' s)

Tactic:
fun _ ↦ mem_image_of_mem f

Premises used: Set.MapsTo, Set.mem_image_of_mem
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
f : α → β
t : Set β
⊢ MapsTo f (f ⁻¹' t) t

Tactic:
fun _ ↦ id

Premises used: Set.Mem, setOf, id, Set.preimage, Set.MapsTo
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
s : Set α
t : Set β
c : γ
⊢ c ∈ image2 f s t ↔ ∃ (a : α), a ∈ s ∧ ∃ (b : β), b ∈ t ∧ f a b = c

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image2
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
ha : a ∈ s
hb : b ∈ t
⊢ f a b ∈ image2 f s t

Tactic:
⟨a, ha, b, hb, rfl⟩

Premises used: Set.Mem, setOf, Set.image2, And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
s : Set (α → β)
t : Set α
b : β
⊢ b ∈ s.seq t ↔ ∃ (f : α → β), f ∈ s ∧ ∃ (a : α), a ∈ t ∧ f a = b

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image2, Set.seq
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
s : Set (α → β)
t : Set α
⊢ s.seq t = image2 (fun (f : α → β) (a : α) ↦ f a) s t

Tactic:
rfl

Premises used: rfl, Set.seq
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
s : Set α
a : αᵒᵖ
⊢ a ∈ s.op ↔ unop a ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.op
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
s : Set α
a : α
⊢ op a ∈ s.op ↔ a ∈ s

Tactic:
rfl
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
s : Set αᵒᵖ
a : α
⊢ a ∈ s.unop ↔ op a ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Set.unop, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
s : Set αᵒᵖ
a : αᵒᵖ
⊢ unop a ∈ s.unop ↔ a ∈ s

Tactic:
rfl
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
s : Set α
⊢ s.op.unop = s

Tactic:
rfl

Premises used: Set.Mem, Set.unop, setOf, Set.preimage, Set.op, rfl
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
s : Set αᵒᵖ
⊢ s.unop.op = s

Tactic:
rfl

Premises used: Set.Mem, Set.unop, setOf, Set.preimage, Set.op, rfl
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
x : α
h : ∀ (x_1 : αᵒᵖ), Membership.mem (γ := Set αᵒᵖ) (Set.op {x}) x_1 ↔ Membership.mem (γ := Set αᵒᵖ) {op x} x_1
⊢ Eq (α := Set αᵒᵖ) (Set.op {x}) {op x}

Tactic:
ext
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
x : α
x_1 : αᵒᵖ
h : Membership.mem (γ := Set αᵒᵖ) (Set.op {x}) x_1 → Membership.mem (γ := Set αᵒᵖ) {op x} x_1
h₁ : Membership.mem (γ := Set αᵒᵖ) {op x} x_1 → Membership.mem (γ := Set αᵒᵖ) (Set.op {x}) x_1
⊢ Membership.mem (γ := Set αᵒᵖ) (Set.op {x}) x_1 ↔ Membership.mem (γ := Set αᵒᵖ) {op x} x_1

Tactic:
constructor
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
x : α
x_1 : αᵒᵖ
⊢ Membership.mem (γ := Set αᵒᵖ) (Set.op {x}) x_1 → Membership.mem (γ := Set αᵒᵖ) {op x} x_1

Tactic:
apply unop_injective

Premises used: Opposite.unop_injective
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
x : α
x_1 : αᵒᵖ
⊢ Membership.mem (γ := Set αᵒᵖ) {op x} x_1 → Membership.mem (γ := Set αᵒᵖ) (Set.op {x}) x_1

Tactic:
apply op_injective

Premises used: Opposite.op_injective
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
x : αᵒᵖ
h : ∀ (x_1 : α), Membership.mem (γ := Set α) (Set.unop {x}) x_1 ↔ Membership.mem (γ := Set α) {unop x} x_1
⊢ Eq (α := Set α) (Set.unop {x}) {unop x}

Tactic:
ext
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
x : αᵒᵖ
x_1 : α
h : Membership.mem (γ := Set α) (Set.unop {x}) x_1 → Membership.mem (γ := Set α) {unop x} x_1
h₁ : Membership.mem (γ := Set α) {unop x} x_1 → Membership.mem (γ := Set α) (Set.unop {x}) x_1
⊢ Membership.mem (γ := Set α) (Set.unop {x}) x_1 ↔ Membership.mem (γ := Set α) {unop x} x_1

Tactic:
constructor
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
x : αᵒᵖ
x_1 : α
⊢ Membership.mem (γ := Set α) (Set.unop {x}) x_1 → Membership.mem (γ := Set α) {unop x} x_1

Tactic:
apply op_injective

Premises used: Opposite.op_injective
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
x : αᵒᵖ
x_1 : α
⊢ Membership.mem (γ := Set α) {unop x} x_1 → Membership.mem (γ := Set α) (Set.unop {x}) x_1

Tactic:
apply unop_injective

Premises used: Opposite.unop_injective
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
x : α
h : ∀ (x_1 : α), Membership.mem (γ := Set α) (Set.unop {op x}) x_1 ↔ Membership.mem (γ := Set α) {x} x_1
⊢ Eq (α := Set α) (Set.unop {op x}) {x}

Tactic:
ext
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
x x_1 : α
h : Membership.mem (γ := Set α) (Set.unop {op x}) x_1 → Membership.mem (γ := Set α) {x} x_1
h₁ : Membership.mem (γ := Set α) {x} x_1 → Membership.mem (γ := Set α) (Set.unop {op x}) x_1
⊢ Membership.mem (γ := Set α) (Set.unop {op x}) x_1 ↔ Membership.mem (γ := Set α) {x} x_1

Tactic:
constructor
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
x x_1 : α
⊢ Membership.mem (γ := Set α) (Set.unop {op x}) x_1 → Membership.mem (γ := Set α) {x} x_1

Tactic:
apply op_injective

Premises used: Opposite.op_injective
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
x x_1 : α
⊢ Membership.mem (γ := Set α) {x} x_1 → Membership.mem (γ := Set α) (Set.unop {op x}) x_1

Tactic:
apply unop_injective

Premises used: Opposite.unop_injective
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
x : αᵒᵖ
h : ∀ (x_1 : αᵒᵖ), Membership.mem (γ := Set αᵒᵖ) (Set.op {unop x}) x_1 ↔ Membership.mem (γ := Set αᵒᵖ) {x} x_1
⊢ Eq (α := Set αᵒᵖ) (Set.op {unop x}) {x}

Tactic:
ext
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
x x_1 : αᵒᵖ
h : Membership.mem (γ := Set αᵒᵖ) (Set.op {unop x}) x_1 → Membership.mem (γ := Set αᵒᵖ) {x} x_1
h₁ : Membership.mem (γ := Set αᵒᵖ) {x} x_1 → Membership.mem (γ := Set αᵒᵖ) (Set.op {unop x}) x_1
⊢ Membership.mem (γ := Set αᵒᵖ) (Set.op {unop x}) x_1 ↔ Membership.mem (γ := Set αᵒᵖ) {x} x_1

Tactic:
constructor
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
x x_1 : αᵒᵖ
⊢ Membership.mem (γ := Set αᵒᵖ) (Set.op {unop x}) x_1 → Membership.mem (γ := Set αᵒᵖ) {x} x_1

Tactic:
apply unop_injective

Premises used: Opposite.unop_injective
-- Module: Mathlib.Data.Set.Opposite
Goal:
α : Type u_1
x x_1 : αᵒᵖ
⊢ Membership.mem (γ := Set αᵒᵖ) {x} x_1 → Membership.mem (γ := Set αᵒᵖ) (Set.op {unop x}) x_1

Tactic:
apply op_injective

Premises used: Opposite.op_injective
-- Module: Mathlib.Data.Set.Order
Goal:
α : Type u
β : Type v
s : Set α
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ MonotoneOn f s ↔ Monotone.{u, v} (β := β) fun (a : (↑s : Type u)) ↦ f (↑a : α)

Tactic:
simp [Monotone, MonotoneOn]

Premises used: Monotone, MonotoneOn
-- Module: Mathlib.Data.Set.Order
Goal:
α : Type u
β : Type v
s : Set α
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ AntitoneOn f s ↔ Antitone.{u, v} (β := β) fun (a : (↑s : Type u)) ↦ f (↑a : α)

Tactic:
simp [Antitone, AntitoneOn]

Premises used: Antitone, AntitoneOn
-- Module: Mathlib.Data.Set.Order
Goal:
α : Type u
β : Type v
s : Set α
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ StrictMonoOn f s ↔ StrictMono.{u, v} (β := β) fun (a : (↑s : Type u)) ↦ f (↑a : α)

Tactic:
simp [StrictMono, StrictMonoOn]

Premises used: StrictMono, StrictMonoOn
-- Module: Mathlib.Data.Set.Order
Goal:
α : Type u
β : Type v
s : Set α
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ StrictAntiOn f s ↔ StrictAnti.{u, v} (β := β) fun (a : (↑s : Type u)) ↦ f (↑a : α)

Tactic:
simp [StrictAnti, StrictAntiOn]

Premises used: StrictAntiOn, StrictAnti
-- Module: Mathlib.Data.Set.Order
Goal:
α : Type u
β : Type v
s : Set α
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
⊢ ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔
    ∃ (a : α),
      a ∈ s ∧ ∃ (b : α), b ∈ s ∧ ∃ (c : α), c ∈ s ∧ a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
simp [monotoneOn_iff_monotone, antitoneOn_iff_antitone, and_assoc, exists_and_left,
    not_monotone_not_antitone_iff_exists_le_le, @and_left_comm (_ ∈ s)]

Premises used: not_monotone_not_antitone_iff_exists_le_le, Set.antitoneOn_iff_antitone, Set.monotoneOn_iff_monotone, exists_and_left, and_left_comm, and_assoc
-- Module: Mathlib.Data.Set.Order
Goal:
α : Type u
β : Type v
s : Set α
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
⊢ ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔
    ∃ (a : α),
      a ∈ s ∧ ∃ (b : α), b ∈ s ∧ ∃ (c : α), c ∈ s ∧ a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
simp [monotoneOn_iff_monotone, antitoneOn_iff_antitone, and_assoc, exists_and_left,
    not_monotone_not_antitone_iff_exists_lt_lt, @and_left_comm (_ ∈ s)]

Premises used: Set.antitoneOn_iff_antitone, Set.monotoneOn_iff_monotone, exists_and_left, and_left_comm, and_assoc, not_monotone_not_antitone_iff_exists_lt_lt
-- Module: Mathlib.Data.Set.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f g : β → Set α
hf : Monotone f
hg : Monotone g
⊢ Monotone.{u_2, u_1} (β := Set α) fun (x : β) ↦ f x ∩ g x

Tactic:
hf.inf hg

Premises used: Monotone.inf
-- Module: Mathlib.Data.Set.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f g : β → Set α
s : Set β
hf : MonotoneOn f s
hg : MonotoneOn g s
⊢ MonotoneOn.{u_2, u_1} (β := Set α) (fun (x : β) ↦ f x ∩ g x) s

Tactic:
hf.inf hg

Premises used: MonotoneOn.inf
-- Module: Mathlib.Data.Set.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f g : β → Set α
hf : Antitone f
hg : Antitone g
⊢ Antitone.{u_2, u_1} (β := Set α) fun (x : β) ↦ f x ∩ g x

Tactic:
hf.inf hg

Premises used: Antitone.inf
-- Module: Mathlib.Data.Set.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f g : β → Set α
s : Set β
hf : AntitoneOn f s
hg : AntitoneOn g s
⊢ AntitoneOn.{u_2, u_1} (β := Set α) (fun (x : β) ↦ f x ∩ g x) s

Tactic:
hf.inf hg

Premises used: AntitoneOn.inf
-- Module: Mathlib.Data.Set.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f g : β → Set α
hf : Monotone f
hg : Monotone g
⊢ Monotone.{u_2, u_1} (β := Set α) fun (x : β) ↦ f x ∪ g x

Tactic:
hf.sup hg

Premises used: Monotone.sup
-- Module: Mathlib.Data.Set.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f g : β → Set α
s : Set β
hf : MonotoneOn f s
hg : MonotoneOn g s
⊢ MonotoneOn.{u_2, u_1} (β := Set α) (fun (x : β) ↦ f x ∪ g x) s

Tactic:
hf.sup hg

Premises used: MonotoneOn.sup
-- Module: Mathlib.Data.Set.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f g : β → Set α
hf : Antitone f
hg : Antitone g
⊢ Antitone.{u_2, u_1} (β := Set α) fun (x : β) ↦ f x ∪ g x

Tactic:
hf.sup hg

Premises used: Antitone.sup
-- Module: Mathlib.Data.Set.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f g : β → Set α
s : Set β
hf : AntitoneOn f s
hg : AntitoneOn g s
⊢ AntitoneOn.{u_2, u_1} (β := Set α) (fun (x : β) ↦ f x ∪ g x) s

Tactic:
hf.sup hg

Premises used: AntitoneOn.sup
-- Module: Mathlib.Data.Set.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → β → Prop
hp : ∀ (b : β), Monotone (β := Prop) fun (a : α) ↦ p a b
⊢ Monotone.{u_1, u_2} (β := Set β) fun (a : α) ↦ {b : β | p a b}

Tactic:
fun _ _ h b => hp b h

Premises used: Set.Mem, Monotone, setOf, Set.Subset
-- Module: Mathlib.Data.Set.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
p : α → β → Prop
hp : ∀ (b : β), Antitone (β := Prop) fun (a : α) ↦ p a b
⊢ Antitone.{u_1, u_2} (β := Set β) fun (a : α) ↦ {b : β | p a b}

Tactic:
fun _ _ h b => hp b h

Premises used: Set.Mem, setOf, Set.Subset, Antitone
-- Module: Mathlib.Data.Set.Order
Goal:
α : Type u_1
P : α → Prop
⊢ Antitone (β := Prop) fun (s : Set α) ↦ ∀ (x : α), x ∈ s → P x

Tactic:
fun _ _ hst h x hx => h x <| hst hx

Premises used: Antitone
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
r : α → α → Prop
hr : Symmetric r
a b : α
⊢ Pairwise (α := Bool) (r on fun (c : Bool) ↦ bif c then a else b) ↔ r a b

Tactic:
simpa [Pairwise, Function.onFun] using @hr a b

Premises used: Function.onFun, Pairwise
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a b : α
⊢ Pairwise (α := Bool) (onFun.{1, u_1 + 1, 1} (β := α) Disjoint fun (c : Bool) ↦ bif c then a else b) ↔ Disjoint a b

Tactic:
pairwise_on_bool Disjoint.symm

Premises used: pairwise_on_bool, Disjoint.symm
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
inst : LinearOrder ι
hr : Symmetric r
f : ι → α
⊢ Pairwise (r on f) ↔ ∀ ⦃m n : ι⦄, m < n → r (f m) (f n)

Tactic:
⟨fun h _m _n hmn => h hmn.ne, fun h _m _n hmn => hmn.lt_or_gt.elim (@h _ _) fun h' => hr (h h')⟩

Premises used: Iff.intro, Or.elim, Ne.lt_or_gt, LT.lt.ne
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : LinearOrder ι
f : ι → α
⊢ Pairwise (Disjoint on f) ↔ ∀ ⦃m n : ι⦄, m < n → Disjoint (f m) (f n)

Tactic:
Symmetric.pairwise_on Disjoint.symm f

Premises used: Disjoint.symm, Symmetric.pairwise_on
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
f g : ι → α
inst : PartialOrder α
inst_1 : OrderBot α
hs : Pairwise (Disjoint on f)
h : g ≤ f
⊢ Pairwise (Disjoint on g)

Tactic:
hs.mono fun i j hij => Disjoint.mono (h i) (h j) hij

Premises used: Disjoint.mono, Pairwise.mono
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder γ
inst_1 : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₁ b₂ : β
hne : b₁ ≠ b₂
inl : ∀ (a₁ : α) (hne : e a₁ ≠ b₂), (Disjoint on extend e f ⊥) (e a₁) b₂
inr : ∀ (hb₁ : ¬∃ (a₁ : α), e a₁ = b₁), (Disjoint on extend e f ⊥) b₁ b₂
⊢ (Disjoint on extend e f ⊥) b₁ b₂

Tactic:
rcases em (∃ a₁, e a₁ = b₁) with ⟨a₁, rfl⟩ | hb₁

Premises used: Exists, em, Eq, rfl
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder γ
inst_1 : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₂ : β
a₁ : α
hne : e a₁ ≠ b₂
inl : ∀ (a₂ : α) (hne : e a₁ ≠ e a₂), (Disjoint on extend e f ⊥) (e a₁) (e a₂)
inl₁ : ∀ (hb₂ : ¬∃ (a₂ : α), e a₂ = b₂), (Disjoint on extend e f ⊥) (e a₁) b₂
⊢ (Disjoint on extend e f ⊥) (e a₁) b₂

Tactic:
rcases em (∃ a₂, e a₂ = b₂) with ⟨a₂, rfl⟩ | hb₂

Premises used: Exists, em, Eq, rfl
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder γ
inst_1 : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
a₁ a₂ : α
hne : e a₁ ≠ e a₂
⊢ (Disjoint on extend e f ⊥) (e a₁) (e a₂)

Tactic:
simpa only [onFun, he.extend_apply] using hf (ne_of_apply_ne e hne)

Premises used: Function.onFun, Function.FactorsThrough.extend_apply, ne_of_apply_ne
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder γ
inst_1 : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₂ : β
a₁ : α
hne : e a₁ ≠ b₂
hb₂ : ¬∃ (a₂ : α), e a₂ = b₂
⊢ (Disjoint on extend e f ⊥) (e a₁) b₂

Tactic:
simpa only [onFun, extend_apply' _ _ _ hb₂] using disjoint_bot_right

Premises used: Function.onFun, disjoint_bot_right, Function.extend_apply'
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder γ
inst_1 : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₁ b₂ : β
hne : b₁ ≠ b₂
hb₁ : ¬∃ (a₁ : α), e a₁ = b₁
⊢ (Disjoint on extend e f ⊥) b₁ b₂

Tactic:
simpa only [onFun, extend_apply' _ _ _ hb₁] using disjoint_bot_left

Premises used: Function.onFun, disjoint_bot_left, Function.extend_apply'
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
h : t ⊆ s
hs : s.Pairwise r
⊢ t.Pairwise r

Tactic:
fun _x xt _y yt => hs (h xt) (h yt)

Premises used: Set.Pairwise
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
r p : α → α → Prop
s : Set α
H : r ≤ p
hr : s.Pairwise r
⊢ s.Pairwise p

Tactic:
hr.imp H

Premises used: Set.Pairwise.imp
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
s : Set α
⊢ s.Pairwise ⊤

Tactic:
pairwise_of_forall s _ fun _ _ => trivial

Premises used: trivial, Set.pairwise_of_forall
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
s : Set α
h : s.Subsingleton
r : α → α → Prop
⊢ s.Pairwise r

Tactic:
fun _x hx _y hy hne => (hne (h hx hy)).elim

Premises used: False.elim, Set.Pairwise
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
r : α → α → Prop
⊢ Set.Pairwise ∅ r

Tactic:
subsingleton_empty.pairwise r

Premises used: Set.Subsingleton.pairwise, Set.subsingleton_empty
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
a : α
r : α → α → Prop
⊢ Set.Pairwise {a} r

Tactic:
subsingleton_singleton.pairwise r

Premises used: Set.subsingleton_singleton, Set.Subsingleton.pairwise
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Refl r
⊢ s.Pairwise r ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b

Tactic:
forall₄_congr fun _ _ _ _ => or_iff_not_imp_left.symm.trans <| or_iff_right_of_imp of_eq

Premises used: Set.Pairwise, of_eq, Classical.or_iff_not_imp_left, Iff.trans, or_iff_right_of_imp, Iff.symm, forall₄_congr
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst : IsEquiv α r
s : Set ι
hs : s.Nonempty
mp : s.Pairwise (r on f) → ∃ (z : α), ∀ (x : ι), x ∈ s → r (f x) z
mpr : (∃ (z : α), ∀ (x : ι), x ∈ s → r (f x) z) → s.Pairwise (r on f)
⊢ s.Pairwise (r on f) ↔ ∃ (z : α), ∀ (x : ι), x ∈ s → r (f x) z

Tactic:
constructor
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst : IsEquiv α r
s : Set ι
hs : s.Nonempty
mp : ∀ (y : ι) (hy : y ∈ s), 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 hs with ⟨y, hy⟩
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
⊢ s.Pairwise (r on f) → ∃ (z : α), ∀ (x : ι), x ∈ s → r (f x) z

Tactic:
fun H => ⟨f y, fun x hx => ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
mp : ∀ (H : s.Pairwise (r on f)) (x : ι) (hx : x ∈ s), r (f x) (f y)
⊢ s.Pairwise (r on f) → ∃ (z : α), ∀ (x : ι), x ∈ s → r (f x) z

Tactic:
refine fun H => ⟨f y, fun x hx => ?_⟩
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : s.Pairwise (r on f)
x : ι
hx : x ∈ s
mp : ∀ (hy : x ∈ s), r (f x) (f x)
mp₁ : ∀ (hne : x ≠ y), r (f x) (f y)
⊢ r (f x) (f y)

Tactic:
rcases eq_or_ne x y with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst : IsEquiv α r
s : Set ι
H : s.Pairwise (r on f)
x : ι
hx hy : x ∈ s
⊢ r (f x) (f x)

Tactic:
apply Std.Refl.refl

Premises used: Std.Refl.refl
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : s.Pairwise (r on f)
x : ι
hx : x ∈ s
hne : x ≠ y
⊢ r (f x) (f y)

Tactic:
H hx hy hne
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : s.Pairwise (r on f)
x : ι
hx : x ∈ s
hne : x ≠ y
⊢ r (f x) (f y)

Tactic:
exact H hx hy hne