-- Mathlib/RingTheory/HahnSeries/Addition.lean
@[simp]
lemma addOppositeEquiv_leadingCoeff (x : HahnSeries Γ (Rᵃᵒᵖ)) :
    (addOppositeEquiv x).unop.leadingCoeff = x.leadingCoeff.unop

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
⊢ (AddOpposite.unop (addOppositeEquiv x)).leadingCoeff = AddOpposite.unop x.leadingCoeff

Tactic:
classical
simp only [leadingCoeff, AddOpposite.unop_op, mk_eq_zero, EmbeddingLike.map_eq_zero_iff,
  addOppositeEquiv_support, ne_eq]
simp only [addOppositeEquiv_apply, AddOpposite.unop_op, mk_eq_zero, coeff_zero]
simp_rw [HahnSeries.ext_iff, funext_iff]
simp only [Pi.zero_apply, AddOpposite.unop_eq_zero_iff, coeff_zero]
split <;> rfl

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
⊢ (if h : AddOpposite.unop (addOppositeEquiv x) = 0 then 0
    else (AddOpposite.unop (addOppositeEquiv x)).coeff (⋯.min ⋯)) =
    AddOpposite.unop (if h : x = 0 then 0 else x.coeff (⋯.min ⋯))

Tactic:
simp only [addOppositeEquiv_apply, AddOpposite.unop_op, mk_eq_zero, coeff_zero]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
⊢ (if h : (fun a => AddOpposite.unop (x.coeff a)) = 0 then 0 else AddOpposite.unop (x.coeff (⋯.min ⋯))) =
    AddOpposite.unop (if h : x = 0 then 0 else x.coeff (⋯.min ⋯))

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
⊢ (if h : ∀ (x_1 : Γ), AddOpposite.unop (x.coeff x_1) = 0 x_1 then 0 else AddOpposite.unop (x.coeff (⋯.min ⋯))) =
    AddOpposite.unop (if h : ∀ (x_1 : Γ), x.coeff x_1 = coeff 0 x_1 then 0 else x.coeff (⋯.min ⋯))

Tactic:
simp only [Pi.zero_apply, AddOpposite.unop_eq_zero_iff, coeff_zero]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
⊢ (if h : ∀ (x_1 : Γ), x.coeff x_1 = 0 then 0 else AddOpposite.unop (x.coeff (⋯.min ⋯))) =
    AddOpposite.unop (if h : ∀ (x_1 : Γ), x.coeff x_1 = 0 then 0 else x.coeff (⋯.min ⋯))

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
⊢ (AddOpposite.unop (addOppositeEquiv x)).leadingCoeff = AddOpposite.unop x.leadingCoeff

Tactic:
simp only [leadingCoeff, AddOpposite.unop_op, mk_eq_zero, EmbeddingLike.map_eq_zero_iff,
  addOppositeEquiv_support, ne_eq]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
⊢ (if h : AddOpposite.unop (addOppositeEquiv x) = 0 then 0
    else (AddOpposite.unop (addOppositeEquiv x)).coeff (⋯.min ⋯)) =
    AddOpposite.unop (if h : x = 0 then 0 else x.coeff (⋯.min ⋯))

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
⊢ (if h : ∀ (x_1 : Γ), x.coeff x_1 = 0 then 0 else AddOpposite.unop (x.coeff (⋯.min ⋯))) =
    AddOpposite.unop (if h : ∀ (x_1 : Γ), x.coeff x_1 = 0 then 0 else x.coeff (⋯.min ⋯))

Tactic:
split <;> rfl

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
⊢ (if h : (fun a => AddOpposite.unop (x.coeff a)) = 0 then 0 else AddOpposite.unop (x.coeff (⋯.min ⋯))) =
    AddOpposite.unop (if h : x = 0 then 0 else x.coeff (⋯.min ⋯))

Tactic:
simp_rw [HahnSeries.ext_iff, funext_iff]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
⊢ (if h : ∀ (x_1 : Γ), AddOpposite.unop (x.coeff x_1) = 0 x_1 then 0 else AddOpposite.unop (x.coeff (⋯.min ⋯))) =
    AddOpposite.unop (if h : ∀ (x_1 : Γ), x.coeff x_1 = coeff 0 x_1 then 0 else x.coeff (⋯.min ⋯))