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

State before:
σ : Instantiation
⊢ ∃ σ_inv, ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id
Tactic:
apply Exists.elim σ.2
State after:
σ : Instantiation
⊢ ∀ (a : VarName → VarName), ↑σ ∘ a = id ∧ a ∘ ↑σ = id → ∃ σ_inv, ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id

State before:
σ : Instantiation
⊢ ∀ (a : VarName → VarName), ↑σ ∘ a = id ∧ a ∘ ↑σ = id → ∃ σ_inv, ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id
Tactic:
intro σ' a1
State after:
σ : Instantiation
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ ∃ σ_inv, ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id

State before:
σ : Instantiation
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ ∃ σ_inv, ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id
Tactic:
cases a1
State after:
case intro
σ : Instantiation
σ' : VarName → VarName
left✝ : ↑σ ∘ σ' = id
right✝ : σ' ∘ ↑σ = id
⊢ ∃ σ_inv, ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id

State before:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
σ_inv : Instantiation := ⟨σ', ⋯⟩
⊢ ∃ σ_inv, ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id
Tactic:
apply Exists.intro σ_inv
State after:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
σ_inv : Instantiation := ⟨σ', ⋯⟩
⊢ ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id

State before:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
σ_inv : Instantiation := ⟨σ', ⋯⟩
⊢ ↑σ ∘ ↑σ_inv = id ∧ ↑σ_inv ∘ ↑σ = id
Tactic:
constructor
State after:
case left
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
σ_inv : Instantiation := ⟨σ', ⋯⟩
⊢ ↑σ ∘ ↑σ_inv = id

case right
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
σ_inv : Instantiation := ⟨σ', ⋯⟩
⊢ ↑σ_inv ∘ ↑σ = id

State before:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ ∃ σ'_1, σ' ∘ σ'_1 = id ∧ σ'_1 ∘ σ' = id
Tactic:
apply Exists.intro σ.1
State after:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ σ' ∘ ↑σ = id ∧ ↑σ ∘ σ' = id

State before:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ σ' ∘ ↑σ = id ∧ ↑σ ∘ σ' = id
Tactic:
constructor
State after:
case left
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ σ' ∘ ↑σ = id

case right
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ ↑σ ∘ σ' = id

State before:
case left
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ σ' ∘ ↑σ = id
Tactic:
exact a1_right
State after:
no goals

State before:
case right
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ ↑σ ∘ σ' = id
Tactic:
exact a1_left
State after:
no goals

State before:
case left
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
σ_inv : Instantiation := ⟨σ', ⋯⟩
⊢ ↑σ ∘ ↑σ_inv = id
Tactic:
exact a1_left
State after:
no goals

State before:
case right
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
σ_inv : Instantiation := ⟨σ', ⋯⟩
⊢ ↑σ_inv ∘ ↑σ = id
Tactic:
exact a1_right
State after:
no goals