Theorem: Imo2009P5.pnat_to_nat_prop2 (Compfiles/Imo2009P5.lean)

State before:
P : ℕ+ → ℕ+ → Prop
⊢ (∀ (m n : ℕ+), P m n) ↔ ∀ (m n : ℕ), P m.succPNat n.succPNat
Tactic:
rw [pnat_to_nat_prop]
State after:
P : ℕ+ → ℕ+ → Prop
⊢ (∀ (n : ℕ) (n_1 : ℕ+), P n.succPNat n_1) ↔ ∀ (m n : ℕ), P m.succPNat n.succPNat

State before:
P : ℕ+ → ℕ+ → Prop
⊢ (∀ (n : ℕ) (n_1 : ℕ+), P n.succPNat n_1) ↔ ∀ (m n : ℕ), P m.succPNat n.succPNat
Tactic:
refine forall_congr' (λ m ↦ ?_)
State after:
P : ℕ+ → ℕ+ → Prop
m : ℕ
⊢ (∀ (n : ℕ+), P m.succPNat n) ↔ ∀ (n : ℕ), P m.succPNat n.succPNat

State before:
P : ℕ+ → ℕ+ → Prop
m : ℕ
⊢ (∀ (n : ℕ+), P m.succPNat n) ↔ ∀ (n : ℕ), P m.succPNat n.succPNat
Tactic:
rw [pnat_to_nat_prop]
State after:
no goals