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

State before:
U V : Type
R : Rel U V
u : U
v : V
⊢ invRel (remove_one R u v) = remove_one (invRel R) v u
Tactic:
apply relext
State after:
case h
U V : Type
R : Rel U V
u : U
v : V
⊢ ∀ (u_1 : V) (v_1 : U), invRel (remove_one R u v) u_1 v_1 ↔ remove_one (invRel R) v u u_1 v_1

State before:
case h
U V : Type
R : Rel U V
u : U
v : V
⊢ ∀ (u_1 : V) (v_1 : U), invRel (remove_one R u v) u_1 v_1 ↔ remove_one (invRel R) v u u_1 v_1
Tactic:
fix y : V
State after:
case h
U V : Type
R : Rel U V
u : U
v y : V
⊢ ∀ (v_1 : U), invRel (remove_one R u v) y v_1 ↔ remove_one (invRel R) v u y v_1

State before:
case h
U V : Type
R : Rel U V
u : U
v y : V
⊢ ∀ (v_1 : U), invRel (remove_one R u v) y v_1 ↔ remove_one (invRel R) v u y v_1
Tactic:
fix x : U
State after:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
⊢ invRel (remove_one R u v) y x ↔ remove_one (invRel R) v u y x

State before:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
⊢ invRel (remove_one R u v) y x ↔ remove_one (invRel R) v u y x
Tactic:
rewrite [invRel_def, remove_one_def, remove_one_def]
State after:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
⊢ x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y) ↔ y ≠ v ∧ x ≠ u ∧ (invRel R y x ∨ invRel R y u ∧ invRel R v x)

State before:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
⊢ x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y) ↔ y ≠ v ∧ x ≠ u ∧ (invRel R y x ∨ invRel R y u ∧ invRel R v x)
Tactic:
rewrite [invRel_def, invRel_def, invRel_def]
State after:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
⊢ x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y) ↔ y ≠ v ∧ x ≠ u ∧ (R x y ∨ R u y ∧ R x v)

State before:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
⊢ x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y) ↔ y ≠ v ∧ x ≠ u ∧ (R x y ∨ R u y ∧ R x v)
Tactic:
rewrite [←and_assoc, ←and_assoc]
State after:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
⊢ (x ≠ u ∧ y ≠ v) ∧ (R x y ∨ R x v ∧ R u y) ↔ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v)

State before:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
⊢ (x ≠ u ∧ y ≠ v) ∧ (R x y ∨ R x v ∧ R u y) ↔ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v)
Tactic:
have h1 : x ≠ u ∧ y ≠ v ↔ y ≠ v ∧ x ≠ u := and_comm
State after:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
h1 : x ≠ u ∧ y ≠ v ↔ y ≠ v ∧ x ≠ u
⊢ (x ≠ u ∧ y ≠ v) ∧ (R x y ∨ R x v ∧ R u y) ↔ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v)

State before:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
h1 : x ≠ u ∧ y ≠ v ↔ y ≠ v ∧ x ≠ u
⊢ (x ≠ u ∧ y ≠ v) ∧ (R x y ∨ R x v ∧ R u y) ↔ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v)
Tactic:
have h2 : R x v ∧ R u y ↔ R u y ∧ R x v := and_comm
State after:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
h1 : x ≠ u ∧ y ≠ v ↔ y ≠ v ∧ x ≠ u
h2 : R x v ∧ R u y ↔ R u y ∧ R x v
⊢ (x ≠ u ∧ y ≠ v) ∧ (R x y ∨ R x v ∧ R u y) ↔ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v)

State before:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
h1 : x ≠ u ∧ y ≠ v ↔ y ≠ v ∧ x ≠ u
h2 : R x v ∧ R u y ↔ R u y ∧ R x v
⊢ (x ≠ u ∧ y ≠ v) ∧ (R x y ∨ R x v ∧ R u y) ↔ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v)
Tactic:
rewrite [h1, h2]
State after:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
h1 : x ≠ u ∧ y ≠ v ↔ y ≠ v ∧ x ≠ u
h2 : R x v ∧ R u y ↔ R u y ∧ R x v
⊢ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v) ↔ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v)

State before:
case h
U V : Type
R : Rel U V
u : U
v y : V
x : U
h1 : x ≠ u ∧ y ≠ v ↔ y ≠ v ∧ x ≠ u
h2 : R x v ∧ R u y ↔ R u y ∧ R x v
⊢ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v) ↔ (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v)
Tactic:
rfl
State after:
no goals