Theorem: SetTheory.Function.ext (SetTheory/Function.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
⊢ f = g
Tactic:
suffices f.graph = g.graph from by
  cases f
  cases this
  rfl
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
⊢ f.graph = g.graph

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
⊢ f.graph = g.graph
Tactic:
ext x
State after:
case h
V : Type u_1
inst✝ : Zermelo V
r x✝ y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x : V
⊢ x ∈ f.graph ↔ x ∈ g.graph

State before:
case h
V : Type u_1
inst✝ : Zermelo V
r x✝ y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x : V
⊢ x ∈ f.graph ↔ x ∈ g.graph
Tactic:
constructor
State after:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x✝ y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x : V
⊢ x ∈ f.graph → x ∈ g.graph

case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x✝ y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x : V
⊢ x ∈ g.graph → x ∈ f.graph

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
this : f.graph = g.graph
⊢ f = g
Tactic:
cases f
State after:
case mk
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
g : a ⟶ b
graph✝ : V
isFunction✝ : IsFunction graph✝
dom_eq✝ : dom graph✝ = a
ran_subset✝ : ran graph✝ ⊆ b
h :
  ∀ (x : V),
    x ∈ a →
      apply { graph := graph✝, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ }.graph x =
        apply g.graph x
this : { graph := graph✝, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ }.graph = g.graph
⊢ { graph := graph✝, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ } = g

State before:
case mk
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
g : a ⟶ b
graph✝ : V
isFunction✝ : IsFunction graph✝
dom_eq✝ : dom graph✝ = a
ran_subset✝ : ran graph✝ ⊆ b
h :
  ∀ (x : V),
    x ∈ a →
      apply { graph := graph✝, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ }.graph x =
        apply g.graph x
this : { graph := graph✝, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ }.graph = g.graph
⊢ { graph := graph✝, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ } = g
Tactic:
cases this
State after:
case mk.refl
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
g : a ⟶ b
isFunction✝ : IsFunction g.1
dom_eq✝ : dom g.1 = a
ran_subset✝ : ran g.1 ⊆ b
h :
  ∀ (x : V),
    x ∈ a →
      apply { graph := g.1, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ }.graph x =
        apply g.graph x
⊢ { graph := g.1, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ } = g

State before:
case mk.refl
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
g : a ⟶ b
isFunction✝ : IsFunction g.1
dom_eq✝ : dom g.1 = a
ran_subset✝ : ran g.1 ⊆ b
h :
  ∀ (x : V),
    x ∈ a →
      apply { graph := g.1, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ }.graph x =
        apply g.graph x
⊢ { graph := g.1, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ } = g
Tactic:
rfl
State after:
no goals

State before:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x✝ y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x : V
⊢ x ∈ f.graph → x ∈ g.graph
Tactic:
intro hx
State after:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x✝ y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x : V
hx : x ∈ f.graph
⊢ x ∈ g.graph

State before:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x✝ y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x : V
hx : x ∈ f.graph
⊢ x ∈ g.graph
Tactic:
obtain ⟨x, y, rfl⟩ := f.isFunction.1 x hx
State after:
case h.mp.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : opair x y ∈ f.graph
⊢ opair x y ∈ g.graph

State before:
case h.mp.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : opair x y ∈ f.graph
⊢ opair x y ∈ g.graph
Tactic:
have : x ∈ a := by
  refine mem_of_mem_dom f ?_
  rw [mem_dom_iff]
  exact ⟨y, hx⟩
State after:
case h.mp.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : opair x y ∈ f.graph
this : x ∈ a
⊢ opair x y ∈ g.graph

State before:
case h.mp.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : opair x y ∈ f.graph
this : x ∈ a
⊢ opair x y ∈ g.graph
Tactic:
rw [opair_mem_graph_iff _ this] at hx ⊢
State after:
case h.mp.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : y = apply f.graph x
this : x ∈ a
⊢ y = apply g.graph x

State before:
case h.mp.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : y = apply f.graph x
this : x ∈ a
⊢ y = apply g.graph x
Tactic:
rw [hx]
State after:
case h.mp.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : y = apply f.graph x
this : x ∈ a
⊢ apply f.graph x = apply g.graph x

State before:
case h.mp.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : y = apply f.graph x
this : x ∈ a
⊢ apply f.graph x = apply g.graph x
Tactic:
exact h _ this
State after:
no goals

State before:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : opair x y ∈ f.graph
⊢ x ∈ a
Tactic:
refine mem_of_mem_dom f ?_
State after:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : opair x y ∈ f.graph
⊢ x ∈ dom f.graph

State before:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : opair x y ∈ f.graph
⊢ x ∈ dom f.graph
Tactic:
rw [mem_dom_iff]
State after:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : opair x y ∈ f.graph
⊢ ∃ z, opair x z ∈ f.graph

State before:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : opair x y ∈ f.graph
⊢ ∃ z, opair x z ∈ f.graph
Tactic:
exact ⟨y, hx⟩
State after:
no goals

State before:
case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x✝ y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x : V
⊢ x ∈ g.graph → x ∈ f.graph
Tactic:
intro hx
State after:
case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x✝ y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x : V
hx : x ∈ g.graph
⊢ x ∈ f.graph

State before:
case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x✝ y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x : V
hx : x ∈ g.graph
⊢ x ∈ f.graph
Tactic:
obtain ⟨x, y, rfl⟩ := g.isFunction.1 x hx
State after:
case h.mpr.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : opair x y ∈ g.graph
⊢ opair x y ∈ f.graph

State before:
case h.mpr.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : opair x y ∈ g.graph
⊢ opair x y ∈ f.graph
Tactic:
have : x ∈ a := by
  refine mem_of_mem_dom g ?_
  rw [mem_dom_iff]
  exact ⟨y, hx⟩
State after:
case h.mpr.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : opair x y ∈ g.graph
this : x ∈ a
⊢ opair x y ∈ f.graph

State before:
case h.mpr.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : opair x y ∈ g.graph
this : x ∈ a
⊢ opair x y ∈ f.graph
Tactic:
rw [opair_mem_graph_iff _ this] at hx ⊢
State after:
case h.mpr.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : y = apply g.graph x
this : x ∈ a
⊢ y = apply f.graph x

State before:
case h.mpr.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : y = apply g.graph x
this : x ∈ a
⊢ y = apply f.graph x
Tactic:
rw [hx]
State after:
case h.mpr.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : y = apply g.graph x
this : x ∈ a
⊢ apply g.graph x = apply f.graph x

State before:
case h.mpr.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : y = apply g.graph x
this : x ∈ a
⊢ apply g.graph x = apply f.graph x
Tactic:
exact (h _ this).symm
State after:
no goals

State before:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : opair x y ∈ g.graph
⊢ x ∈ a
Tactic:
refine mem_of_mem_dom g ?_
State after:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : opair x y ∈ g.graph
⊢ x ∈ dom g.graph

State before:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : opair x y ∈ g.graph
⊢ x ∈ dom g.graph
Tactic:
rw [mem_dom_iff]
State after:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : opair x y ∈ g.graph
⊢ ∃ z, opair x z ∈ g.graph

State before:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
x y : V
hx : opair x y ∈ g.graph
⊢ ∃ z, opair x z ∈ g.graph
Tactic:
exact ⟨y, hx⟩
State after:
no goals