Theorem: eq_I_Nat (ECTate/Algebra/EllipticCurve/KodairaTypes.lean)

State before:
m n : Nat
⊢ m = n ↔ I m = I n
Tactic:
apply Iff.intro
State after:
case mp
m n : Nat
⊢ m = n → I m = I n

case mpr
m n : Nat
⊢ I m = I n → m = n

State before:
case mp
m n : Nat
⊢ m = n → I m = I n

case mpr
m n : Nat
⊢ I m = I n → m = n
Tactic:
intro h
State after:
case mp
m n : Nat
h : m = n
⊢ I m = I n

case mpr
m n : Nat
⊢ I m = I n → m = n

State before:
case mp
m n : Nat
h : m = n
⊢ I m = I n

case mpr
m n : Nat
⊢ I m = I n → m = n
Tactic:
exact congrArg I h
State after:
case mpr
m n : Nat
⊢ I m = I n → m = n

State before:
case mpr
m n : Nat
⊢ I m = I n → m = n
Tactic:
intro h
State after:
case mpr
m n : Nat
h : I m = I n
⊢ m = n

State before:
case mpr
m n : Nat
h : I m = I n
⊢ m = n
Tactic:
cases h
State after:
case mpr.refl
m : Nat
⊢ m = m

State before:
case mpr.refl
m : Nat
⊢ m = m
Tactic:
rfl
State after:
no goals