Theorem: SetTheory.ran_rcomp (SetTheory/Relation.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
⊢ ran (rcomp s r) ⊆ ran s
Tactic:
intro t
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z s t : V
⊢ t ∈ ran (rcomp s r) → t ∈ ran s

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z s t : V
⊢ t ∈ ran (rcomp s r) → t ∈ ran s
Tactic:
simp only [mem_ran_iff, mem_rcomp_iff, opair_injective]
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z s t : V
⊢ (∃ z a b c, (z = a ∧ t = c) ∧ opair b c ∈ s ∧ opair a b ∈ r) → ∃ z, opair z t ∈ s

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z s t : V
⊢ (∃ z a b c, (z = a ∧ t = c) ∧ opair b c ∈ s ∧ opair a b ∈ r) → ∃ z, opair z t ∈ s
Tactic:
rintro ⟨z, _, b, _, ⟨rfl, rfl⟩, hc, _⟩
State after:
case intro.intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x y z✝ s t z b : V
hc : opair b t ∈ s
right✝ : opair z b ∈ r
⊢ ∃ z, opair z t ∈ s

State before:
case intro.intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x y z✝ s t z b : V
hc : opair b t ∈ s
right✝ : opair z b ∈ r
⊢ ∃ z, opair z t ∈ s
Tactic:
exact ⟨_, hc⟩
State after:
no goals