```
(def-theorem inverse-composes-to-id
"forall(f:[ind_1,ind_2], inverse{f} oo f =id{ran{inverse{f}}})"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-inference
extensionality
direct-inference
(case-split ("#(f(x_0))"))
(block
(script-comment "node added by `case-split' at (1)")
simplify
direct-and-antecedent-inference-strategy
(block
(script-comment "node added by `direct-and-antecedent-inference-strategy' at (0 0)")
(backchain "with(i,x_0:ind_1,x_0=i);")
(eliminate-defined-iota-expression 1 u)
simplify)
(block
(script-comment "node added by `direct-and-antecedent-inference-strategy' at (1)")
(contrapose "with(p:prop,not(p));")
(instantiate-existential ("f(x_0)"))
(eliminate-defined-iota-expression 0 u)
simplify))
(block
(script-comment "node added by `case-split' at (2)")
simplify
direct-inference
(contrapose "with(p:prop,p);")
(backchain "with(p:prop,p);")
(eliminate-defined-iota-expression 0 u))
)))
```

```
(def-theorem inverse-is-injective
"forall(f:[ind_1,ind_2], injective_q{inverse{f}})"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-inference
insistent-direct-inference
simplify
direct-inference
(cut-with-single-formula "#(iota(y:ind_1,f(y)=x_\$0))")
(cut-with-single-formula "#(iota(y:ind_1,f(y)=x_\$1))")
(incorporate-antecedent "with(x,y:ind_1, x=y)")
(eliminate-defined-iota-expression 0 u)
(eliminate-defined-iota-expression 0 v)
direct-inference
(force-substitution "x_\$0" "f(u)" (0))
simplify
)))
```

```
(def-theorem inverse-defined-within-range
"forall(f:[ind_1,ind_2],
injective_q(f) implies ran(f) subseteq dom{inverse{f}})"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
insistent-direct-inference
simplify-insistently
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises eliminate-iota-macete)
(instantiate-existential ("x"))
(instantiate-universal-antecedent
"with(f:[ind_1,ind_2],injective_q{f});"
("x" "j"))
)))
```

```
(def-theorem inverse-defined-only-in-range
"forall(f:[ind_1,ind_2], dom{inverse{f}} subseteq ran(f))"
lemma
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
insistent-direct-inference
simplify-insistently
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises eliminate-forsome-macete)
(force-substitution "x_\$0=f(i)" "f(i)=x_\$0" (0))
direct-and-antecedent-inference-strategy
)))
```

```
(def-theorem dom-of-inverse
"forall(f:[ind_1,ind_2],
injective_q(f) implies dom{inverse{f}} = ran(f))"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
(apply-macete-with-minor-premises inverse-defined-only-in-range)
(apply-macete-with-minor-premises inverse-defined-within-range)
)))
```

```
(def-theorem inverse-range-within-domain
"forall(f:[ind_1,ind_2],
injective_q(f) implies dom(f) subseteq ran{inverse{f}})"
lemma
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
insistent-direct-inference
simplify-insistently
direct-inference
(instantiate-existential ("f(x_\$0)"))
(apply-macete-with-minor-premises eliminate-iota-macete)
simplify
)))
```

```
(def-theorem inverse-range-only-in-domain
"forall(f:[ind_1,ind_2], ran{inverse{f}} subseteq dom(f))"
lemma
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-inference
insistent-direct-inference
simplify-insistently
direct-and-antecedent-inference-strategy
(force-substitution "x_\$0" "iota(y:ind_1,f(y)=x_\$1)" (0))
(eliminate-defined-iota-expression 0 u)
)))
```

```
(def-theorem ran-of-inverse
"forall(f:[ind_1,ind_2],
injective_q(f) implies ran{inverse{f}} = dom(f))"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
(apply-macete-with-minor-premises inverse-range-within-domain)
(apply-macete-with-minor-premises inverse-range-only-in-domain)
)))
```

```
(def-theorem inverse-is-a-left-inverse
"forall(f:[ind_1,ind_2],
injective_q(f) implies inverse{f} oo f = id{dom{f}})"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
extensionality
direct-inference
simplify
(case-split-on-conditionals (0))
(apply-macete-with-minor-premises eliminate-iota-macete)
simplify
)))
```

```
(def-theorem inverse-is-a-left-inverse-applied
"forall(f:[ind_1,ind_2], x:ind_1,
injective_q(f) and #(f(x)) implies inverse{f}(f(x)) = x)"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
simplify-insistently
direct-and-antecedent-inference-strategy
(eliminate-iota 0)
(instantiate-existential ("x"))
(backchain "with(f:[ind_1,ind_2],injective_q{f});"))))
```

```
(def-theorem inverse-is-a-right-inverse
"forall(f:[ind_1,ind_2],
injective_q(f) implies f oo inverse{f} = id{ran{f}})"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof; 46 nodes
(
direct-and-antecedent-inference-strategy
extensionality
direct-inference
simplify
direct-and-antecedent-inference-strategy
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy' at (0 0)")
(eliminate-iota 0)
(instantiate-existential ("x"))
simplify)
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy' at (1)")
(contrapose "with(p:prop,not(p));")
(instantiate-existential ("iota(y:ind_1,f(y)=x_0)"))
(eliminate-defined-iota-expression 0 u))
)))
```

```
(def-theorem inverse-is-a-right-inverse-applied
"forall(f:[ind_1,ind_2], x:ind_2,
injective_q(f) and x in ran{f} implies f(inverse{f}(x)) = x)"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-theorem inverse-is-a-right-inverse ("f"))
(contrapose "with(f:[ind_2,ind_2],f=f);")
extensionality
(apply-macete-with-minor-premises tr%restricted-to-range-composition-lemma)
beta-reduce-insistently
(instantiate-existential ("x_\$1"))
(contrapose "with(p:prop,not(p));")
(case-split ("forsome(x:ind_1,x_\$1=f(x))"))
simplify
(contrapose "with(x_\$1:ind_2,f:sets[ind_2],x_\$1 in f);")
(apply-macete-with-minor-premises indicator-facts-macete)
simplify)))
```

```
(def-theorem image-under-inverse-of-injective-mapping
"forall(f:[ind_1,ind_2],a:sets[ind_1],b:sets[ind_2],
injective_q{f} and image{f,a}=b and a subseteq dom{f}
implies
image{inverse{f},b}=a)"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-inference
(block
(script-comment "node added by `direct-inference' at (0)")
insistent-direct-inference
simplify
direct-and-antecedent-inference-strategy
(backchain "with(i,x_\$2:ind_1,x_\$2=i);")
(eliminate-defined-iota-expression 0 u)
(contrapose "with(b,f:sets[ind_2],f=b);")
extensionality
(instantiate-existential ("x_\$1"))
simplify
direct-and-antecedent-inference-strategy
(contrapose
"with(u:ind_1,x_\$1,i:ind_2, forall(u_1:ind_1,i=x_\$1 implies u=u_1));")
(instantiate-existential ("x"))
(contrapose "with(p:prop,not(p));")
simplify)
(block
(script-comment "node added by `direct-inference' at (1)")
insistent-direct-inference
simplify
direct-and-antecedent-inference-strategy
(instantiate-existential ("f(x_\$0)"))
(block
(script-comment "node added by `instantiate-existential' at (0 0)")
(contrapose "with(b,f:sets[ind_2],f=b);")
extensionality
(instantiate-existential ("x_\$0"))
(instantiate-existential ("f(x_\$0)"))
simplify
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-with-minor-premises
(instantiate-existential ("x_\$0"))
simplify
(instantiate-universal-antecedent
"with(f:[ind_1,ind_2],a:sets[ind_1],a subseteq dom{f});"
("x_\$0"))
(incorporate-antecedent
"with(x_\$0:ind_1,f:[ind_1,ind_2],x_\$0 in dom{f});")
(apply-macete-with-minor-premises domain-membership-iff-defined))
(block
(script-comment "node added by `instantiate-existential' at (0 1)")
(eliminate-iota 0)
(instantiate-existential ("x_\$0"))
(backchain "with(f:[ind_1,ind_2],injective_q{f});"))
(instantiate-universal-antecedent
"with(f:[ind_1,ind_2],a:sets[ind_1],a subseteq dom{f});"
("x_\$0")))
)))
```

```
(def-theorem inverse-inverse-is-restriction
"forall(f:[ind_1,ind_2],
injective_q{f} implies inverse{inverse{f}}=restrict{f,dom{f}})"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
extensionality
direct-inference
simplify
(case-split-on-conditionals (0))
(apply-macete-with-minor-premises eliminate-iota-macete)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises eliminate-iota-macete)
direct-and-antecedent-inference-strategy
simplify
(force-substitution "x_0" "iota(y:ind_1,f(y)=b)" (0))
(eliminate-defined-iota-expression 0 u)
(apply-macete-with-minor-premises eliminate-iota-macete)
simplify
direct-and-antecedent-inference-strategy
(contrapose "with(p:prop, not(p))")
(force-substitution "x_0" "iota(y:ind_1,f(y)=i)" (0))
(eliminate-defined-iota-expression 0 u)
)))
```

```
(def-theorem surjective-inverse
"forall(a:sets[ind_1],f:[ind_1,ind_2],
injective_on_q(f,a) and dom(f)=a
implies
surjective_on_q{inverse{f},ran{f},a})"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
insistent-direct-inference-strategy
(apply-macete-with-minor-premises dom-of-inverse)
insistent-direct-inference-strategy
(backchain "with(f:[ind_1,ind_2],a:sets[ind_1],injective_on_q{f,a});")
direct-inference
(apply-macete-with-minor-premises tr%membership-in-a-domain)
auto-instantiate-existential
(apply-macete-with-minor-premises tr%membership-in-a-domain)
auto-instantiate-existential
(apply-macete-with-minor-premises ran-of-inverse)
)))
```

```
(def-theorem inverse-composition-image-lemma
"forall(phi:[ind_1,ind_3],psi:[ind_2,ind_3],
injective_q{psi} and ran{psi}=ran{phi}
implies
image{(inverse{psi}) oo phi,dom{phi}}=dom{psi})"
(theory pure-generic-theory-3)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-and-antecedent-inference-strategy
insistent-direct-inference
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
(apply-macete-with-minor-premises eliminate-iota-macete)
direct-and-antecedent-inference-strategy
insistent-direct-inference
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
(apply-macete-with-minor-premises eliminate-iota-macete)
direct-and-antecedent-inference-strategy
(cut-with-single-formula "psi(x_\$3) in ran{psi}")
(incorporate-antecedent
"with(x_\$3:ind_2,psi:[ind_2,ind_3],psi(x_\$3) in ran{psi});")
(backchain
"with(phi:[ind_1,ind_3],psi:[ind_2,ind_3],ran{psi}=ran{phi});")
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(instantiate-existential ("x"))
(cut-with-single-formula "psi(b)=psi(x_\$3)")
(backchain "with(psi:[ind_2,ind_3],injective_q{psi});")
(apply-macete-with-minor-premises tr%range-domain-membership)
(apply-macete-with-minor-premises tr%domain-membership-iff-defined)
)))
```

```
(def-theorem inverse-defined-only-in-range-existential
"forall(f:[ind_1,ind_2],y:ind_2,
#(inverse{f}(y)) implies forsome(x:ind_1,y=f(x)))"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-existential ("(inverse{f}(y_\$0))"))
simplify-insistently
(eliminate-defined-iota-expression 0 z))))
```