[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
⊢ inv (inv r) = r
[PROOFSTEP]
ext x y
[GOAL]
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x : α
y : β
⊢ inv (inv r) x y ↔ r x y
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
⊢ codom (inv r) = dom r
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x : α
⊢ x ∈ codom (inv r) ↔ x ∈ dom r
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
⊢ dom (inv r) = codom r
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x : β
⊢ x ∈ dom (inv r) ↔ x ∈ codom r
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Rel α β
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
⊢ (r • s) • t = r • s • t
[PROOFSTEP]
unfold comp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Rel α β
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
⊢ (fun x z => ∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y z) = fun x z => ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 z
[PROOFSTEP]
ext (x w)
[GOAL]
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Rel α β
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
⊢ (∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w) ↔ ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w
[PROOFSTEP]
constructor
[GOAL]
case a.h.a.mp
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Rel α β
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
⊢ (∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w) → ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w
[PROOFSTEP]
rintro ⟨z, ⟨y, rxy, syz⟩, tzw⟩
[GOAL]
case a.h.a.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Rel α β
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
z : γ
tzw : t z w
y : β
rxy : r x y
syz : s y z
⊢ ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w
[PROOFSTEP]
exact ⟨y, rxy, z, syz, tzw⟩
[GOAL]
case a.h.a.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Rel α β
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
⊢ (∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w) → ∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w
[PROOFSTEP]
rintro ⟨y, rxy, z, syz, tzw⟩
[GOAL]
case a.h.a.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Rel α β
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
y : β
rxy : r x y
z : γ
syz : s y z
tzw : t z w
⊢ ∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w
[PROOFSTEP]
exact ⟨z, ⟨y, rxy, syz⟩, tzw⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r : Rel α β
⊢ r • Eq = r
[PROOFSTEP]
unfold comp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r : Rel α β
⊢ (fun x z => ∃ y, r x y ∧ y = z) = r
[PROOFSTEP]
ext y
[GOAL]
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r : Rel α β
y : α
x✝ : β
⊢ (∃ y_1, r y y_1 ∧ y_1 = x✝) ↔ r y x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r : Rel α β
⊢ Eq • r = r
[PROOFSTEP]
unfold comp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r : Rel α β
⊢ (fun x z => ∃ y, x = y ∧ r y z) = r
[PROOFSTEP]
ext x
[GOAL]
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r : Rel α β
x : α
x✝ : β
⊢ (∃ y, x = y ∧ r y x✝) ↔ r x x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
⊢ inv Eq = Eq
[PROOFSTEP]
ext x y
[GOAL]
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x y : α
⊢ inv Eq x y ↔ x = y
[PROOFSTEP]
constructor
[GOAL]
case a.h.a.mp
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x y : α
⊢ inv Eq x y → x = y
[PROOFSTEP]
apply Eq.symm
[GOAL]
case a.h.a.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x y : α
⊢ x = y → inv Eq x y
[PROOFSTEP]
apply Eq.symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r : Rel α β
s : Rel β γ
⊢ inv (r • s) = inv s • inv r
[PROOFSTEP]
ext x z
[GOAL]
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ r : Rel α β
s : Rel β γ
x : γ
z : α
⊢ inv (r • s) x z ↔ (inv s • inv r) x z
[PROOFSTEP]
simp [comp, inv, flip, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Set α
⊢ image Eq s = s
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Set α
x : α
⊢ x ∈ image Eq s ↔ x ∈ s
[PROOFSTEP]
simp [mem_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
⊢ image (r • s) t = image s (image r t)
[PROOFSTEP]
ext z
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ z ∈ image (r • s) t ↔ z ∈ image s (image r t)
[PROOFSTEP]
simp only [mem_image]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ (∃ x, x ∈ t ∧ (r • s) x z) ↔ ∃ x, (∃ x_1, x_1 ∈ t ∧ r x_1 x) ∧ s x z
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ (∃ x, x ∈ t ∧ (r • s) x z) → ∃ x, (∃ x_1, x_1 ∈ t ∧ r x_1 x) ∧ s x z
[PROOFSTEP]
rintro ⟨x, xt, y, rxy, syz⟩
[GOAL]
case h.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
x : α
xt : x ∈ t
y : β
rxy : r x y
syz : s y z
⊢ ∃ x, (∃ x_1, x_1 ∈ t ∧ r x_1 x) ∧ s x z
[PROOFSTEP]
exact ⟨y, ⟨x, xt, rxy⟩, syz⟩
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
⊢ (∃ x, (∃ x_1, x_1 ∈ t ∧ r x_1 x) ∧ s x z) → ∃ x, x ∈ t ∧ (r • s) x z
[PROOFSTEP]
rintro ⟨y, ⟨x, xt, rxy⟩, syz⟩
[GOAL]
case h.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set α
z : γ
y : β
syz : s y z
x : α
xt : x ∈ t
rxy : r x y
⊢ ∃ x, x ∈ t ∧ (r • s) x z
[PROOFSTEP]
exact ⟨x, xt, y, rxy, syz⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
⊢ image r Set.univ = codom r
[PROOFSTEP]
ext y
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
y : β
⊢ y ∈ image r Set.univ ↔ y ∈ codom r
[PROOFSTEP]
simp [mem_image, codom]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Set α
⊢ preimage Eq s = s
[PROOFSTEP]
simp only [preimage, inv_id, image_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
⊢ preimage (r • s) t = preimage r (preimage s t)
[PROOFSTEP]
simp only [preimage, inv_comp, image_comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
⊢ preimage r Set.univ = dom r
[PROOFSTEP]
rw [preimage, image_univ, codom_inv]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s t : Set β
⊢ ∀ (x : α), x ∈ core r (s ∩ t) ↔ x ∈ core r s ∩ core r t
[PROOFSTEP]
simp [mem_core, imp_and, forall_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
⊢ ∀ (x : α), x ∈ core r Set.univ ↔ x ∈ Set.univ
[PROOFSTEP]
simp [mem_core]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Set α
⊢ core Eq s = s
[PROOFSTEP]
simp [core]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
⊢ core (r • s) t = core r (core s t)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
x : α
⊢ x ∈ core (r • s) t ↔ x ∈ core r (core s t)
[PROOFSTEP]
simp [core, comp]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
x : α
⊢ (∀ (y : γ) (x_1 : β), r x x_1 → s x_1 y → y ∈ t) ↔ ∀ (y : β), r x y → ∀ (y_1 : γ), s y y_1 → y_1 ∈ t
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
x : α
⊢ (∀ (y : γ) (x_1 : β), r x x_1 → s x_1 y → y ∈ t) → ∀ (y : β), r x y → ∀ (y_1 : γ), s y y_1 → y_1 ∈ t
[PROOFSTEP]
exact fun h y rxy z => h z y rxy
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
x : α
⊢ (∀ (y : β), r x y → ∀ (y_1 : γ), s y y_1 → y_1 ∈ t) → ∀ (y : γ) (x_1 : β), r x x_1 → s x_1 y → y ∈ t
[PROOFSTEP]
exact fun h z y rzy => h y rzy z
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s : Set α
⊢ f '' s = Rel.image (Function.graph f) s
[PROOFSTEP]
simp [Set.image, Function.graph, Rel.image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s : Set β
⊢ f ⁻¹' s = Rel.preimage (Function.graph f) s
[PROOFSTEP]
simp [Set.preimage, Function.graph, Rel.preimage, Rel.inv, flip, Rel.image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s : Set β
⊢ f ⁻¹' s = Rel.core (Function.graph f) s
[PROOFSTEP]
simp [Set.preimage, Function.graph, Rel.core]
