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

State before:
σ : Instantiation
⊢ Function.Surjective ↑σ
Tactic:
obtain ⟨σ', a1⟩ := σ.2
State after:
case intro
σ : Instantiation
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ Function.Surjective ↑σ

State before:
case intro
σ : Instantiation
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ Function.Surjective ↑σ
Tactic:
cases a1
State after:
case intro.intro
σ : Instantiation
σ' : VarName → VarName
left✝ : ↑σ ∘ σ' = id
right✝ : σ' ∘ ↑σ = id
⊢ Function.Surjective ↑σ

State before:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ Function.Surjective ↑σ
Tactic:
case intro a1_left a1_right =>
  have s1 : Function.RightInverse σ' σ.1 := congr_fun a1_left
  exact Function.RightInverse.surjective s1
State after:
no goals

State before:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
⊢ Function.Surjective ↑σ
Tactic:
have s1 : Function.RightInverse σ' σ.1 := congr_fun a1_left
State after:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
s1 : Function.RightInverse σ' ↑σ
⊢ Function.Surjective ↑σ

State before:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
s1 : Function.RightInverse σ' ↑σ
⊢ Function.Surjective ↑σ
Tactic:
exact Function.RightInverse.surjective s1
State after:
no goals