Theorem: Smt.Reconstruct.Arith.castSndEQ (Smt/Reconstruct/Arith/MulPosNeg/Lemmas.lean)

State before:
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
⊢ p ∧ a = b → p ∧ zToR a = zToR b
Tactic:
rintro ⟨h₁, h₂⟩
State after:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
h₁ : p
h₂ : a = b
⊢ p ∧ zToR a = zToR b

State before:
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
h₁ : p
h₂ : a = b
⊢ p ∧ zToR a = zToR b
Tactic:
exact ⟨h₁, by rw [h₂]⟩
State after:
no goals

State before:
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
h₁ : p
h₂ : a = b
⊢ zToR a = zToR b
Tactic:
rw [h₂]
State after:
no goals