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

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

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

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

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

State before:
σ : Instantiation
σ' : VarName → VarName
a1_left : ↑σ ∘ σ' = id
a1_right : σ' ∘ ↑σ = id
s1 : Function.LeftInverse σ' ↑σ
⊢ Function.Injective ↑σ
Tactic:
exact Function.LeftInverse.injective s1
State after:
no goals