-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
rw :
  Eq (α := FiniteResidueField K)
    ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K)
        (if h : LE.le (α := ArchimedeanClass K) 0 (mk x) then
          (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
            (FiniteElement.mk x h)
        else 0) :
      FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
rw₁ :
  Eq (α := FiniteResidueField K)
    ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K)
        ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
            (FiniteElement.mk x hx) :
          ℝ) :
      FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
rw₂ :
  Eq (α := FiniteResidueField K)
    ((OrderRingHom.comp (FiniteResidueField.ofArchimedean f)
            (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk) :
          (a : FiniteElement K) → FiniteResidueField K)
        (FiniteElement.mk x hx) :
      FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
rw₃ :
  Eq (α := FiniteResidueField K)
    ((OrderRingHom.comp (OrderRingHom.comp (FiniteResidueField.ofArchimedean f) Classical.ofNonempty)
            FiniteResidueField.mk :
          (a : FiniteElement K) → FiniteResidueField K)
        (FiniteElement.mk x hx) :
      FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
rw₄ :
  Eq (α := FiniteResidueField K)
    ((OrderRingHom.comp (FiniteResidueField.ofArchimedean f) Classical.ofNonempty :
          (a : FiniteResidueField K) → FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx)) :
      FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
rw₅ rw₆ :
  Eq (α := FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
⊢ Eq (α := FiniteResidueField K)
    ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K) (stdPart x) : FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)

Tactic:
rw [stdPart, dif_pos hx, ← OrderRingHom.comp_apply, ← OrderRingHom.comp_assoc,
    OrderRingHom.comp_apply, OrderRingHom.apply_eq_self]

Premises used: OrderRingHom.apply_eq_self, dif_pos, ArchimedeanClass.stdPart, OrderRingHom.comp_assoc, OrderRingHom.comp_apply