Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
S : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
abv : AbsoluteValue R S
toFun✝¹ : R → S
map_mul'✝¹ : ∀ (x y : R), toFun✝¹ (x * y) = toFun✝¹ x * toFun✝¹ y
nonneg'✝¹ : ∀ (x : R), 0 ≤ { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun x
eq_zero'✝¹ : ∀ (x : R), { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun x = 0 ↔ x = 0
add_le'✝¹ :
  ∀ (x y : R),
    { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun (x + y) ≤
      { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun x + { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun y
toFun✝ : R → S
map_mul'✝ : ∀ (x y : R), toFun✝ (x * y) = toFun✝ x * toFun✝ y
nonneg'✝ : ∀ (x : R), 0 ≤ { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun x
eq_zero'✝ : ∀ (x : R), { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun x = 0 ↔ x = 0
add_le'✝ :
  ∀ (x y : R),
    { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun (x + y) ≤
      { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun x + { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun y
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝¹, map_mul' := map_mul'✝¹, nonneg' := nonneg'✝¹, eq_zero' := eq_zero'✝¹, add_le' := add_le'✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := toFun✝, map_mul' := map_mul'✝, nonneg' := nonneg'✝, eq_zero' := eq_zero'✝, add_le' := add_le'✝ }
⊢ { toFun := toFun✝¹, map_mul' := map_mul'✝¹, nonneg' := nonneg'✝¹, eq_zero' := eq_zero'✝¹, add_le' := add_le'✝¹ } =
    { toFun := toFun✝, map_mul' := map_mul'✝, nonneg' := nonneg'✝, eq_zero' := eq_zero'✝, add_le' := add_le'✝ }

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
S : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
abv : AbsoluteValue R S
toFun✝¹ : R → S
map_mul'✝¹ : ∀ (x y : R), toFun✝¹ (x * y) = toFun✝¹ x * toFun✝¹ y
nonneg'✝¹ : ∀ (x : R), 0 ≤ { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun x
eq_zero'✝¹ : ∀ (x : R), { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun x = 0 ↔ x = 0
add_le'✝¹ :
  ∀ (x y : R),
    { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun (x + y) ≤
      { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun x + { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun y
toFun✝ : R → S
map_mul'✝ : ∀ (x y : R), toFun✝ (x * y) = toFun✝ x * toFun✝ y
nonneg'✝ : ∀ (x : R), 0 ≤ { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun x
eq_zero'✝ : ∀ (x : R), { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun x = 0 ↔ x = 0
add_le'✝ :
  ∀ (x y : R),
    { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun (x + y) ≤
      { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun x + { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun y
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝¹, map_mul' := map_mul'✝¹, nonneg' := nonneg'✝¹, eq_zero' := eq_zero'✝¹, add_le' := add_le'✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := toFun✝, map_mul' := map_mul'✝, nonneg' := nonneg'✝, eq_zero' := eq_zero'✝, add_le' := add_le'✝ }
⊢ { toFun := toFun✝¹, map_mul' := map_mul'✝¹, nonneg' := nonneg'✝¹, eq_zero' := eq_zero'✝¹, add_le' := add_le'✝¹ } =
    { toFun := toFun✝, map_mul' := map_mul'✝, nonneg' := nonneg'✝, eq_zero' := eq_zero'✝, add_le' := add_le'✝ }