Theorem: exercise3_2 (LeanCourse/Assignments/Solutions/Solutions3.lean)

State before:
⊢ (ℤ × ℕ → ℤ × ℤ) ≃ (ℕ → ℕ)
Tactic:
have h1 : ℤ × ℕ ≃ ℕ := by exact Denumerable.eqv (ℤ × ℕ)
State after:
h1 : ℤ × ℕ ≃ ℕ
⊢ (ℤ × ℕ → ℤ × ℤ) ≃ (ℕ → ℕ)

State before:
h1 : ℤ × ℕ ≃ ℕ
⊢ (ℤ × ℕ → ℤ × ℤ) ≃ (ℕ → ℕ)
Tactic:
have h2 : ℤ × ℤ ≃ ℕ := by exact Denumerable.eqv (ℤ × ℤ)
State after:
h1 : ℤ × ℕ ≃ ℕ
h2 : ℤ × ℤ ≃ ℕ
⊢ (ℤ × ℕ → ℤ × ℤ) ≃ (ℕ → ℕ)

State before:
h1 : ℤ × ℕ ≃ ℕ
h2 : ℤ × ℤ ≃ ℕ
⊢ (ℤ × ℕ → ℤ × ℤ) ≃ (ℕ → ℕ)
Tactic:
exact Equiv.arrowCongr h1 h2
State after:
no goals

State before:
⊢ ℤ × ℕ ≃ ℕ
Tactic:
exact Denumerable.eqv (ℤ × ℕ)
State after:
no goals

State before:
h1 : ℤ × ℕ ≃ ℕ
⊢ ℤ × ℤ ≃ ℕ
Tactic:
exact Denumerable.eqv (ℤ × ℤ)
State after:
no goals