awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
b : β
⊢ b ∈ R.cod ↔ ∃ (a : α), (a, b) ∈ R

Tactic:
.rfl

Premises used: SetRel.cod, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R₁ R₂ : SetRel α β
h : R₁ ≤ R₂
⊢ R₁.dom ⊆ R₂.dom

Tactic:
fun _a ⟨b, hab⟩ ↦ ⟨b, h hab⟩

Premises used: _private.0.SetRel.dom_mono.match_1, Membership.mem, SetRel.dom, Set.Subset, Exists.intro
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R₁ R₂ : SetRel α β
h : R₁ ≤ R₂
⊢ R₁.cod ⊆ R₂.cod

Tactic:
fun _b ⟨a, hab⟩ ↦ ⟨a, h hab⟩

Premises used: SetRel.cod, Membership.mem, Set.Subset, _private.0.SetRel.cod_mono.match_1, Exists.intro
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
⊢ Eq.{u_1 + 1} (α := Set α) (dom.{u_1, u_2} (β := β) ∅) ∅

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
⊢ Eq.{u_2 + 1} (α := Set β) (cod.{u_1, u_2} (α := α) ∅) ∅

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
h : R.dom = ∅
⊢ ∀ (x : α × β), ¬x ∈ R

Tactic:
simp_all [Set.eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
h : R.cod = ∅
⊢ ∀ (x : α × β), ¬x ∈ R

Tactic:
simp_all [Set.eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
⊢ Eq.{u_1 + 1} (α := Set α) (dom.{u_1, u_2} (β := β) Set.univ) Set.univ

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
⊢ Eq.{u_2 + 1} (α := Set β) (cod.{u_1, u_2} (α := α) Set.univ) Set.univ

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.inv.cod = R.dom

Tactic:
rfl

Premises used: Set.Mem, SetRel.inv, setOf, SetRel.dom, Set.preimage, Prod.swap, rfl
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.inv.dom = R.cod

Tactic:
rfl

Premises used: SetRel.cod, Set.Mem, SetRel.inv, setOf, Set.preimage, Prod.swap, rfl
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
a₁ a₂ : α
⊢ Membership.mem (γ := SetRel α α) SetRel.id (a₁, a₂) ↔ a₁ = a₂

Tactic:
.rfl

Premises used: SetRel.id, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := SetRel α α) (inv SetRel.id) SetRel.id

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
S : SetRel β γ
a : α
c : γ
⊢ (a, c) ∈ R ○ S ↔ ∃ (b : β), (a, b) ∈ R ∧ (b, c) ∈ S

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SetRel.comp
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
S : SetRel β γ
a : α
b : β
c : γ
hab : (a, b) ∈ R
hbc : (b, c) ∈ S
⊢ (a, c) ∈ R ○ S

Tactic:
⟨b, hab, hbc⟩

Premises used: Set.Mem, setOf, SetRel.comp, And.intro, Exists.intro
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : SetRel α β
S : SetRel β γ
t : SetRel γ δ
⊢ R ○ S ○ t = R ○ (S ○ t)

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R ○ SetRel.id = R

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
⊢ SetRel.id ○ R = R

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
S : SetRel β γ
⊢ (R ○ S).inv = S.inv ○ R.inv

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
⊢ Eq (α := SetRel α γ) (R ○ ∅) ∅

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
S : SetRel β γ
⊢ Eq (α := SetRel α γ) (∅ ○ S) ∅

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
⊢ Eq (α := SetRel α γ) (R ○ Set.univ)
    {x : α × γ |
      match (motive := α × γ → Prop) x with
      | (a, _c) => a ∈ R.dom}

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
S : SetRel β γ
⊢ Eq (α := SetRel α γ) (Set.univ ○ S)
    {x : α × γ |
      match (motive := α × γ → Prop) x with
      | (_b, c) => c ∈ S.cod}

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
R : SetRel α β
S : ι → SetRel β γ
⊢ Eq (α := SetRel α γ) (R ○ ⋃ (i : ι), S i) (⋃ (i : ι), R ○ S i)

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
R : ι → SetRel α β
S : SetRel β γ
⊢ Eq (α := SetRel α γ) ((⋃ (i : ι), R i) ○ S) (⋃ (i : ι), R i ○ S)

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
𝒮 : Set (SetRel β γ)
⊢ R ○ ⋃₀ 𝒮 = ⋃ S ∈ 𝒮, R ○ S

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ℛ : Set (SetRel α β)
S : SetRel β γ
⊢ ⋃₀ ℛ ○ S = ⋃ R ∈ ℛ, R ○ S

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R₁ R₂ : SetRel α β
S₁ S₂ : SetRel β γ
hR : R₁ ⊆ R₂
hS : S₁ ⊆ S₂
⊢ R₁ ○ S₁ ⊆ R₂ ○ S₂

Tactic:
fun _ ↦ .imp fun _ ↦ .imp (@hR _) (@hS _)

Premises used: And.imp, Set.Mem, setOf, Exists.imp, Set.Subset, SetRel.comp
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R₁ R₂ : SetRel α β
S : SetRel β γ
hR : R₁ ⊆ R₂
⊢ R₁ ○ S ⊆ R₂ ○ S

Tactic:
comp_subset_comp hR .rfl

Premises used: SetRel.comp_subset_comp, Set.Subset.rfl
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
S₁ S₂ : SetRel β γ
hS : S₁ ⊆ S₂
⊢ R ○ S₁ ⊆ R ○ S₂

Tactic:
comp_subset_comp .rfl hS

Premises used: SetRel.comp_subset_comp, Set.Subset.rfl
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_6
inst : Preorder ι
f : ι → SetRel α β
g : ι → SetRel β γ
hf : Monotone f
hg : Monotone g
⊢ Monotone (β := SetRel α γ) fun (x : ι) ↦ f x ○ g x

Tactic:
fun _i _j hij ⟨_a, _c⟩ ⟨b, hab, hbc⟩ ↦ ⟨b, hf hij hab, hg hij hbc⟩

Premises used: Monotone, Membership.mem, Prod.mk, Set.Subset, _private.0.Monotone.relComp.match_2, SetRel.comp, _private.0.Monotone.relComp.match_1, And.intro, Exists.intro
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t₁ t₂ : Set β
ht : (t₁ ∩ t₂).Nonempty
s : Set α
u : Set γ
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = s ×ˢ u

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t₁ t₂ : Set β
ht : Disjoint t₁ t₂
s : Set α
u : Set γ
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = ∅

Tactic:
Set.eq_empty_of_forall_notMem fun _ ⟨_z, ⟨_, hzs⟩, hzu, _⟩ ↦ Set.disjoint_left.1 ht hzs hzu

Premises used: _private.0.SetRel.prod_comp_prod_of_disjoint.match_1, False, Set.disjoint_left, Set.eq_empty_of_forall_notMem, Iff.mp
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t₁ t₂ : Set β
u : Set γ
inst : Decidable (Disjoint t₁ t₂)
pos : ∀ (hst : Disjoint t₁ t₂), s ×ˢ t₁ ○ t₂ ×ˢ u = ∅
neg : ∀ (hst : ¬Disjoint t₁ t₂), s ×ˢ t₁ ○ t₂ ×ˢ u = s ×ˢ u
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = if Disjoint t₁ t₂ then ∅ else s ×ˢ u

Tactic:
split_ifs with hst
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t₁ t₂ : Set β
u : Set γ
inst : Decidable (Disjoint t₁ t₂)
hst : Disjoint t₁ t₂
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = ∅

Tactic:
prod_comp_prod_of_disjoint hst ..

Premises used: SetRel.prod_comp_prod_of_disjoint
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t₁ t₂ : Set β
u : Set γ
inst : Decidable (Disjoint t₁ t₂)
hst : Disjoint t₁ t₂
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = ∅

Tactic:
exact prod_comp_prod_of_disjoint hst ..

Premises used: SetRel.prod_comp_prod_of_disjoint
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t₁ t₂ : Set β
u : Set γ
inst : Decidable (Disjoint t₁ t₂)
hst : ¬Disjoint t₁ t₂
neg neg₁ : s ×ˢ u = s ×ˢ u
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = s ×ˢ u

Tactic:
rw [prod_comp_prod_of_inter_nonempty <| Set.not_disjoint_iff_nonempty_inter.1 hst]

Premises used: SetRel.prod_comp_prod_of_inter_nonempty, Set.not_disjoint_iff_nonempty_inter, Iff.mp
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
b : β
⊢ b ∈ R.image s ↔ ∃ (a : α), a ∈ s ∧ (a, b) ∈ R

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SetRel.image
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
t : Set β
a : α
⊢ a ∈ R.preimage t ↔ ∃ (b : β), b ∈ t ∧ (a, b) ∈ R

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SetRel.preimage
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
s₁ s₂ : Set α
hs : s₁ ⊆ s₂
⊢ R.image s₁ ⊆ R.image s₂

Tactic:
fun _ ⟨a, ha, hab⟩ ↦ ⟨a, hs ha, hab⟩

Premises used: Membership.mem, Set.Subset, _private.0.SetRel.image_subset_image.match_1, And.intro, Exists.intro, SetRel.image
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R₁ R₂ : SetRel α β
s : Set α
hR : R₁ ⊆ R₂
⊢ R₁.image s ⊆ R₂.image s

Tactic:
fun _ ⟨a, ha, hab⟩ ↦ ⟨a, ha, hR hab⟩

Premises used: Membership.mem, Set.Subset, _private.0.SetRel.image_subset_image.match_1, And.intro, Exists.intro, SetRel.image
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
t₁ t₂ : Set β
ht : t₁ ⊆ t₂
⊢ R.preimage t₁ ⊆ R.preimage t₂

Tactic:
fun _ ⟨a, ha, hab⟩ ↦ ⟨a, ht ha, hab⟩

Premises used: Membership.mem, Set.Subset, And.intro, Exists.intro, SetRel.preimage, _private.0.SetRel.preimage_subset_preimage.match_1
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R₁ R₂ : SetRel α β
t : Set β
hR : R₁ ⊆ R₂
⊢ R₁.preimage t ⊆ R₂.preimage t

Tactic:
fun _ ⟨a, ha, hab⟩ ↦ ⟨a, ha, hR hab⟩

Premises used: Membership.mem, Set.Subset, And.intro, Exists.intro, SetRel.preimage, _private.0.SetRel.preimage_subset_preimage.match_1
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
t : Set β
⊢ R.inv.image t = R.preimage t

Tactic:
rfl

Premises used: Set.Mem, SetRel.inv, setOf, Set.preimage, SetRel.preimage, Prod.swap, rfl
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
⊢ R.inv.preimage s = R.image s

Tactic:
rfl

Premises used: Set.Mem, SetRel.inv, setOf, Set.preimage, SetRel.image, Prod.swap, rfl
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
⊢ Monotone R.image

Tactic:
fun _ _ ↦ image_subset_image

Premises used: Monotone, SetRel.image_subset_image
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
⊢ Monotone R.preimage

Tactic:
fun _ _ ↦ preimage_subset_preimage

Premises used: Monotone, SetRel.preimage_subset_preimage
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.image ∅ = ∅

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.preimage ∅ = ∅

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.image Set.univ = R.cod

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.preimage Set.univ = R.dom

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
s₁ s₂ : Set α
⊢ R.image (s₁ ∩ s₂) ⊆ R.image s₁ ∩ R.image s₂

Tactic:
image_mono.map_inf_le ..

Premises used: SetRel.image_mono, Monotone.map_inf_le
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
t₁ t₂ : Set β
⊢ R.preimage (t₁ ∩ t₂) ⊆ R.preimage t₁ ∩ R.preimage t₂

Tactic:
preimage_mono.map_inf_le ..

Premises used: SetRel.preimage_mono, Monotone.map_inf_le
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
s₁ s₂ : Set α
⊢ R.image (s₁ ∪ s₂) = R.image s₁ ∪ R.image s₂

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
R : SetRel α β
s : ι → Set α
⊢ R.image (⋃ (i : ι), s i) = ⋃ (i : ι), R.image (s i)

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
S : Set (Set α)
⊢ R.image (⋃₀ S) = ⋃ s ∈ S, R.image s

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
t₁ t₂ : Set β
⊢ R.preimage (t₁ ∪ t₂) = R.preimage t₁ ∪ R.preimage t₂

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
R : SetRel α β
t : ι → Set β
⊢ R.preimage (⋃ (i : ι), t i) = ⋃ (i : ι), R.preimage (t i)

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
T : Set (Set β)
⊢ R.preimage (⋃₀ T) = ⋃ t ∈ T, R.preimage t

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
s : Set α
⊢ image SetRel.id s = s

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
s : Set α
⊢ preimage SetRel.id s = s

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
S : SetRel β γ
s : Set α
⊢ (R ○ S).image s = S.image (R.image s)

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
S : SetRel β γ
u : Set γ
⊢ (R ○ S).preimage u = R.preimage (S.preimage u)

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
s : Set α
⊢ Eq.{u_2 + 1} (α := Set β) (image ∅ s) ∅

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
t : Set β
⊢ Eq.{u_1 + 1} (α := Set α) (preimage ∅ t) ∅

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
s : Set α
hs : s.Nonempty
⊢ Eq.{u_2 + 1} (α := Set β) (image Set.univ s) Set.univ

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
t : Set β
ht : t.Nonempty
⊢ Eq.{u_1 + 1} (α := Set α) (preimage Set.univ t) Set.univ

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
h : R.dom ⊆ s
⊢ R.image s = R.cod

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
t : Set β
h : R.cod ⊆ t
⊢ R.preimage t = R.dom

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
⊢ R.image (s ∩ R.dom) = R.image s

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
t : Set β
⊢ R.preimage (t ∩ R.cod) = R.preimage t

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
⊢ s ∩ R.dom ⊆ R.preimage (R.image s)

Tactic:
aesop (add simp [Set.subset_def])

Premises used: Set.subset_def
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
t : Set β
⊢ t ∩ R.cod ⊆ R.image (R.preimage t)

Tactic:
aesop (add simp [Set.subset_def])

Premises used: Set.subset_def
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
⊢ R.image s = ⋃ x ∈ s, {y : β | (x, y) ∈ R}

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
t : Set β
⊢ R.preimage t = ⋃ y ∈ t, {x : α | (x, y) ∈ R}

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
t : Set β
a : α
⊢ a ∈ R.core t ↔ ∀ ⦃b : β⦄, (a, b) ∈ R → b ∈ t

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SetRel.core
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
t₁ t₂ : Set β
ht : t₁ ⊆ t₂
⊢ R.core t₁ ⊆ R.core t₂

Tactic:
fun _a ha _b hab ↦ ht <| ha hab

Premises used: Set.Mem, setOf, Set.Subset, SetRel.core
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
⊢ Monotone R.core

Tactic:
fun _ _ ↦ core_subset_core

Premises used: Monotone, SetRel.core_subset_core
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
t₁ t₂ : Set β
⊢ R.core (t₁ ∩ t₂) = R.core t₁ ∩ R.core t₂

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
t₁ t₂ : Set β
⊢ R.core t₁ ∪ R.core t₂ ⊆ R.core (t₁ ∪ t₂)

Tactic:
core_mono.le_map_sup ..

Premises used: SetRel.core_mono, Monotone.le_map_sup
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
⊢ R.core Set.univ = Set.univ

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
β : Type u_2
t : Set β
⊢ core SetRel.id t = t

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : SetRel α β
S : SetRel β γ
u : Set γ
⊢ (R ○ S).core u = R.core (S.core u)

Tactic:
aesop
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
t : Set β
⊢ R.image s ⊆ t ↔ s ⊆ R.core t

Tactic:
aesop (add simp [Set.subset_def])

Premises used: Set.subset_def
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α β
⊢ GaloisConnection R.image R.core

Tactic:
fun _ _ ↦ image_subset_iff

Premises used: SetRel.image_subset_iff, GaloisConnection
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R : SetRel α α
inst : R.IsRefl
a : α
⊢ (a, a) ∈ R

Tactic:
refl_of (· ~[R] ·) a

Premises used: refl_of, Membership.mem, Prod.mk
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R : SetRel α α
a : α
inst : R.IsRefl
⊢ (a, a) ∈ R

Tactic:
R.refl a

Premises used: SetRel.refl
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R : SetRel α α
inst : R.IsRefl
fst : α
⊢ (fst, fst) ∈ R

Tactic:
R.rfl

Premises used: SetRel.rfl
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R : SetRel α α
inst : R.IsRefl
fst : α
⊢ (fst, fst) ∈ R

Tactic:
exact R.rfl

Premises used: SetRel.rfl
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R_1 R₁_1 R₂_1 : SetRel α β
S_1 : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a_1 a₁ a₂ : α
b_1 : β
c_1 : γ
R_2 R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
R : ι → SetRel α α
inst : ∀ (i : ι), (R i).IsRefl
⊢ ∀ (R_3 : SetRel α α), Membership.mem (γ := Set (SetRel α α)) (Set.range fun (i : ι) ↦ R i) R_3 → R_3.IsRefl

Tactic:
simpa
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
S : SetRel β β
R : SetRel α β
inst : S.IsRefl
⊢ R ⊆ R ○ S

Tactic:
simpa using comp_subset_comp_right id_subset

Premises used: SetRel.comp_subset_comp_right, SetRel.id_subset
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
R : SetRel α α
inst : R.IsRefl
S : SetRel α β
⊢ S ⊆ R ○ S

Tactic:
simpa using comp_subset_comp_left id_subset

Premises used: SetRel.comp_subset_comp_left, SetRel.id_subset
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R : SetRel α α
inst : R.IsRefl
s : Set α
⊢ s ⊆ R.image s

Tactic:
fun x hx => ⟨x, hx, R.rfl⟩

Premises used: Set.Mem, setOf, Set.Subset, SetRel.rfl, And.intro, Exists.intro, SetRel.image
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R : SetRel α α
inst : R.IsRefl
s : Set α
⊢ s ⊆ R.preimage s

Tactic:
fun x hx => ⟨x, hx, R.rfl⟩

Premises used: Set.Mem, setOf, Set.Subset, SetRel.rfl, And.intro, Exists.intro, SetRel.preimage
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
hst : s ×ˢ t ⊆ SetRel.id
obtain : ∀ (a : α) (ha : a ∈ s), ∃ (x : α), s = {x} ∧ t = {x}
⊢ ∃ (x : α), s = {x} ∧ t = {x}

Tactic:
obtain ⟨a, ha⟩ := hs
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
s t : Set α
ht : t.Nonempty
hst : s ×ˢ t ⊆ SetRel.id
a : α
ha : a ∈ s
obtain : ∀ (b : α) (hb : b ∈ t), ∃ (x : α), s = {x} ∧ t = {x}
⊢ ∃ (x : α), s = {x} ∧ t = {x}

Tactic:
obtain ⟨b, hb⟩ := ht
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
s t : Set α
hst : s ×ˢ t ⊆ SetRel.id
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x = y

Tactic:
simp only [Set.prod_subset_iff, mem_id] at hst

Premises used: Set.prod_subset_iff, SetRel.mem_id
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
s t : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hst : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x = y
⊢ a ∈ t

Tactic:
obtain rfl := hst _ ha _ hb

Premises used: rfl
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
s t : Set α
a : α
ha : a ∈ s
hst : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x = y
hb : a ∈ t
simp : ∃ (x : α), x ∈ s ∧ (∀ (x_1 : α), x_1 ∈ s → x_1 = x) ∧ x ∈ t ∧ ∀ (x_1 : α), x_1 ∈ t → x_1 = x
⊢ ∃ (x : α), s = {x} ∧ t = {x}

Tactic:
simp only [Set.eq_singleton_iff_unique_mem, and_assoc]

Premises used: and_assoc, Set.eq_singleton_iff_unique_mem
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
s t : Set α
a : α
ha : a ∈ s
hst : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x = y
hb : a ∈ t
⊢ ∃ (x : α), x ∈ s ∧ (∀ (x_1 : α), x_1 ∈ s → x_1 = x) ∧ x ∈ t ∧ ∀ (x_1 : α), x_1 ∈ t → x_1 = x

Tactic:
⟨a, ha, (hst · · _ hb), hb, (hst _ ha · · |>.symm)⟩

Premises used: And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
s t : Set α
a : α
ha : a ∈ s
hst : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x = y
hb : a ∈ t
⊢ ∃ (x : α), x ∈ s ∧ (∀ (x_1 : α), x_1 ∈ s → x_1 = x) ∧ x ∈ t ∧ ∀ (x_1 : α), x_1 ∈ t → x_1 = x

Tactic:
exact ⟨a, ha, (hst · · _ hb), hb, (hst _ ha · · |>.symm)⟩
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R : SetRel α α
a b : α
inst : R.IsSymm
hab : (a, b) ∈ R
⊢ (b, a) ∈ R

Tactic:
symm_of (· ~[R] ·) hab

Premises used: Membership.mem, Prod.mk, symm_of
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R : SetRel α α
a b : α
inst : R.IsSymm
⊢ (a, b) ∈ R ↔ (b, a) ∈ R

Tactic:
comm_of (· ~[R] ·)

Premises used: Membership.mem, Prod.mk, comm_of
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R : SetRel α α
inst : R.IsSymm
h : ∀ (x : α × α), x ∈ R.inv ↔ x ∈ R
⊢ R.inv = R

Tactic:
ext
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R : SetRel α α
inst : R.IsSymm
x : α × α
⊢ x ∈ R.inv ↔ x ∈ R

Tactic:
R.comm

Premises used: Set.Mem, SetRel.inv, setOf, Set.preimage, SetRel.comm, Prod.swap
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R : SetRel α α
inst : R.IsSymm
x : α × α
⊢ x ∈ R.inv ↔ x ∈ R

Tactic:
exact R.comm

Premises used: SetRel.comm
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
R : SetRel α α
hR : R.inv = R
a b : α
hab : (a, b) ∈ R
rwa rwa₁ rwa₂ rwa₃ : (b, a) ∈ R.inv
⊢ (b, a) ∈ R

Tactic:
rwa [← hR]
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R_1 R₁_1 R₂_1 : SetRel α β
S_1 : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a_1 a₁ a₂ : α
b_1 : β
c_1 : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
inst : R.IsSymm
⊢ R.inv.IsSymm

Tactic:
simpa
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R_1 R₁_1 R₂_1 : SetRel α β
S_1 : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a_1 a₁ a₂ : α
b_1 : β
c_1 : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c x x_1 : α
⊢ Membership.mem (γ := SetRel α α) ∅ (x, x_1) → Membership.mem (γ := SetRel α α) ∅ (x_1, x)

Tactic:
simp
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R_1 R₁_1 R₂_1 : SetRel α β
S_1 : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a_1 a₁ a₂ : α
b_1 : β
c_1 : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c x x_1 : α
⊢ Membership.mem (γ := SetRel α α) Set.univ (x, x_1) → Membership.mem (γ := SetRel α α) Set.univ (x_1, x)

Tactic:
simp
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R_1 R₁_1 R₂_1 : SetRel α β
S_1 : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a_1 a₁ a₂ : α
b_1 : β
c_1 : γ
R_2 R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
R : ι → SetRel α α
inst : ∀ (i : ι), (R i).IsSymm
⊢ ∀ (R_3 : SetRel α α), Membership.mem (γ := Set (SetRel α α)) (Set.range fun (i : ι) ↦ R i) R_3 → R_3.IsSymm

Tactic:
simpa
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R_1 R₁_1 R₂_1 : SetRel α β
S_1 : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a_1 a₁ a₂ : α
b_1 : β
c_1 : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
f : α → β
inst : R.IsSymm
simp :
  ∀ (a b : β) (x x_1 : α),
    (x, x_1) ∈ R → f x = a → f x_1 = b → ∃ (a_5 : α), ∃ (b_2 : α), (a_5, b_2) ∈ R ∧ f a_5 = b ∧ f b_2 = a
⊢ ∀ (a b : β), (a, b) ∈ Prod.map f f '' R → (b, a) ∈ Prod.map f f '' R

Tactic:
simp only [Set.mem_image, Prod.exists, Prod.map_apply, Prod.mk.injEq, forall_exists_index,
      and_imp]

Premises used: and_imp, Set.mem_image, forall_exists_index, Prod.mk.injEq, Prod.map_apply, Prod.exists
-- Module: Mathlib.Data.Rel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R_1 R₁_1 R₂_1 : SetRel α β
S_1 : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a_1 a₁_1 a₂_1 : α
b_1 : β
c_1 : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
f : α → β
inst : R.IsSymm
a₁ a₂ : α
ha : (a₁, a₂) ∈ R
⊢ ∃ (a : α), ∃ (b : α), (a, b) ∈ R ∧ f a = f a₂ ∧ f b = f a₁

Tactic:
⟨_, _, R.symm ha, rfl, rfl⟩

Premises used: SetRel.symm, And.intro, Exists.intro, rfl