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

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

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

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

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