Theorem: MM0.Instantiation.is_bijective (FOL/MM0/MM0.lean)

State before:
σ : Instantiation
⊢ Function.Bijective ↑σ
Tactic:
unfold Function.Bijective
State after:
σ : Instantiation
⊢ Function.Injective ↑σ ∧ Function.Surjective ↑σ

State before:
σ : Instantiation
⊢ Function.Injective ↑σ ∧ Function.Surjective ↑σ
Tactic:
constructor
State after:
case left
σ : Instantiation
⊢ Function.Injective ↑σ

case right
σ : Instantiation
⊢ Function.Surjective ↑σ

State before:
case left
σ : Instantiation
⊢ Function.Injective ↑σ
Tactic:
exact Instantiation.is_injective σ
State after:
no goals

State before:
case right
σ : Instantiation
⊢ Function.Surjective ↑σ
Tactic:
exact Instantiation.is_surjective σ
State after:
no goals