Theorem: HTPI.right_inv_onto_below (HTPILib/Chap7.lean)

State before:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : maps_below n g'
⊢ onto_below n g
Tactic:
define at h2
State after:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
⊢ onto_below n g

State before:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
⊢ onto_below n g
Tactic:
define
State after:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
⊢ ∀ k < n, ∃ i < n, g i = k

State before:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
⊢ ∀ k < n, ∃ i < n, g i = k
Tactic:
fix k : Nat
State after:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
k : ℕ
⊢ k < n → ∃ i < n, g i = k

State before:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
k : ℕ
⊢ k < n → ∃ i < n, g i = k
Tactic:
assume h3 : k < n
State after:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
k : ℕ
h3 : k < n
⊢ ∃ i < n, g i = k

State before:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
k : ℕ
h3 : k < n
⊢ ∃ i < n, g i = k
Tactic:
apply Exists.intro (g' k)
State after:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
k : ℕ
h3 : k < n
⊢ g' k < n ∧ g (g' k) = k

State before:
n : ℕ
g g' : ℕ → ℕ
h1 : ∀ i < n, g (g' i) = i
h2 : ∀ i < n, g' i < n
k : ℕ
h3 : k < n
⊢ g' k < n ∧ g (g' k) = k
Tactic:
show g' k < n ∧ g (g' k) = k from And.intro (h2 k h3) (h1 k h3)
State after:
no goals