-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
Goal:
K L : Type
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
inst_5 : IsCyclic Gal(L/K)
g : Gal(L/K)
hg : ∀ (x : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (Subgroup.zpowers g) x
x_1 : L
hx_1 : Eq (α := K) ((Algebra.norm K : (a : L) → K) x_1 : K) (1 : K)
x : L
hx : Eq (α := K) ((Algebra.norm K : (a : L) → K) x : K) (1 : K)
xu : Lˣ := IsUnit.unit (a := x) ⋯
hx' :
  Eq (α := L)
    (↑((toMul : (a : Additive Lˣ) → Lˣ)
          ((toAdditive : (a : (↑(ofMulDistribMulAction Gal(L/K) Lˣ) : Type)) → Additive Lˣ)
            ((Hom.hom (norm (ofAlgebraAutOnUnits K L)) :
                (a : (↑(ofAlgebraAutOnUnits K L) : Type)) → (↑(ofAlgebraAutOnUnits K L) : Type))
              ((AddEquiv.symm toAdditive : (a : Additive Lˣ) → (↑(ofMulDistribMulAction Gal(L/K) Lˣ) : Type))
                ((ofMul : (a : Lˣ) → Additive Lˣ) xu))))) :
      L)
    1
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : (↑(ofAlgebraAutOnUnits K L) : Type)
hy :
  Eq (α := (↑(ofAlgebraAutOnUnits K L) : Type))
    (((Hom.hom
              (HSub.hSub (α := Quiver.Hom (V := Rep ℤ Gal(L/K)) (ofAlgebraAutOnUnits K L) (ofAlgebraAutOnUnits K L))
                (β := Quiver.Hom (V := Rep ℤ Gal(L/K)) (ofAlgebraAutOnUnits K L) (ofAlgebraAutOnUnits K L))
                (applyAsHom (k := ℤ) (ofAlgebraAutOnUnits K L) g :
                  Quiver.Hom (V := Rep ℤ Gal(L/K)) (ofAlgebraAutOnUnits K L) (ofAlgebraAutOnUnits K L))
                (CategoryTheory.CategoryStruct.id (ofAlgebraAutOnUnits K L)))).toLinearMap :
          (a : (↑(ofAlgebraAutOnUnits K L) : Type)) → (↑(ofAlgebraAutOnUnits K L) : Type))
        y :
      (↑(ofAlgebraAutOnUnits K L) : Type))
    ((↑(Subtype.mk (p := fun (x : (↑(ofAlgebraAutOnUnits K L) : Type)) ↦
            Membership.mem (γ := Submodule ℤ (↑(ofAlgebraAutOnUnits K L) : Type))
              (LinearMap.ker (Representation.IntertwiningMap.toLinearMap (Hom.hom (norm (ofAlgebraAutOnUnits K L))))) x)
            ((AddEquiv.symm toAdditive : (a : Additive Lˣ) → (↑(ofMulDistribMulAction Gal(L/K) Lˣ) : Type))
              ((ofMul : (a : Lˣ) → Additive Lˣ) xu))
            ⋯) :
        (↑(ofAlgebraAutOnUnits K L) : Type)) :
      (↑(ofAlgebraAutOnUnits K L) : Type))
⊢ Eq (α := L)
    (↑((toMul : (a : Additive Lˣ) → Lˣ)
          ((toAdditive : (a : (↑(ofMulDistribMulAction Gal(L/K) Lˣ) : Type)) → Additive Lˣ)
            (((Hom.hom
                    (HSub.hSub (α :=
                      Quiver.Hom (V := Rep ℤ Gal(L/K)) (ofAlgebraAutOnUnits K L) (ofAlgebraAutOnUnits K L)) (β :=
                      Quiver.Hom (V := Rep ℤ Gal(L/K)) (ofAlgebraAutOnUnits K L) (ofAlgebraAutOnUnits K L))
                      (applyAsHom (k := ℤ) (ofAlgebraAutOnUnits K L) g :
                        Quiver.Hom (V := Rep ℤ Gal(L/K)) (ofAlgebraAutOnUnits K L) (ofAlgebraAutOnUnits K L))
                      (CategoryTheory.CategoryStruct.id (ofAlgebraAutOnUnits K L)))).toLinearMap :
                (a : (↑(ofAlgebraAutOnUnits K L) : Type)) → (↑(ofAlgebraAutOnUnits K L) : Type))
              y))) :
      L)
    (↑((toMul : (a : Additive Lˣ) → Lˣ)
          ((toAdditive : (a : (↑(ofMulDistribMulAction Gal(L/K) Lˣ) : Type)) → Additive Lˣ)
            (↑(Subtype.mk (p := fun (x : (↑(ofAlgebraAutOnUnits K L) : Type)) ↦
                  Membership.mem (γ := Submodule ℤ (↑(ofAlgebraAutOnUnits K L) : Type))
                    (LinearMap.ker
                      (Representation.IntertwiningMap.toLinearMap (Hom.hom (norm (ofAlgebraAutOnUnits K L)))))
                    x)
                  ((AddEquiv.symm toAdditive : (a : Additive Lˣ) → (↑(ofMulDistribMulAction Gal(L/K) Lˣ) : Type))
                    ((ofMul : (a : Lˣ) → Additive Lˣ) xu))
                  ⋯) :
              (↑(ofAlgebraAutOnUnits K L) : Type)))) :
      L)

Tactic:
have := Units.ext_iff.1 congr(toMul <| toAdditive $hy)