Theorem: HTPI.relext (HTPILib/Chap8Part1.lean)

State before:
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
⊢ R = S
Tactic:
have h2 : extension R = extension S := by
  apply Set.ext
  fix (u, v) : U × V rewrite [ext_def, ext_def]  show R u v ↔ S u v from h u v
  done
State after:
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
h2 : extension R = extension S
⊢ R = S

State before:
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
h2 : extension R = extension S
⊢ R = S
Tactic:
show R = S from
  calc R
    _ = RelFromExt (extension R) := by rfl
    _ = RelFromExt (extension S) := by rw [h2]
    _ = S := by rfl
State after:
no goals

State before:
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
⊢ extension R = extension S
Tactic:
apply Set.ext
State after:
case h
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
⊢ ∀ (x : U × V), x ∈ extension R ↔ x ∈ extension S

State before:
case h
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
⊢ ∀ (x : U × V), x ∈ extension R ↔ x ∈ extension S
Tactic:
fix (u, v) : U × V
State after:
case h
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
u : U
v : V
⊢ (u, v) ∈ extension R ↔ (u, v) ∈ extension S

State before:
case h
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
u : U
v : V
⊢ (u, v) ∈ extension R ↔ (u, v) ∈ extension S
Tactic:
rewrite [ext_def, ext_def]
State after:
case h
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
u : U
v : V
⊢ R u v ↔ S u v

State before:
case h
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
u : U
v : V
⊢ R u v ↔ S u v
Tactic:
show R u v ↔ S u v from h u v
State after:
no goals

State before:
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
h2 : extension R = extension S
⊢ R = RelFromExt (extension R)
Tactic:
rfl
State after:
no goals

State before:
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
h2 : extension R = extension S
⊢ RelFromExt (extension R) = RelFromExt (extension S)
Tactic:
rw [h2]
State after:
no goals

State before:
U V : Type
R S : Rel U V
h : ∀ (u : U) (v : V), R u v ↔ S u v
h2 : extension R = extension S
⊢ RelFromExt (extension S) = S
Tactic:
rfl
State after:
no goals