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

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

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

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

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

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

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

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

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

State before:
case mpr
m n : Nat
h : Is m = Is 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