-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 (hypothesis)
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))
⊢ HDiv.hDiv (α := L) (β := L)
      ((g : (a : L) → L)
          (↑((toMul : (a : Additive Lˣ) → Lˣ)
                ((toAdditive : (a : (↑(ofMulDistribMulAction Gal(L/K) Lˣ) : Type)) → Additive Lˣ) y)) :
            L) :
        L)
      ((↑((toMul : (a : Additive Lˣ) → Lˣ)
              ((toAdditive : (a : (↑(ofMulDistribMulAction Gal(L/K) Lˣ) : Type)) → Additive Lˣ) y)) :
          L) :
        L) =
    x
have this₁ : 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))
                sorry) :
            (↑(ofAlgebraAutOnUnits K L) : Type)))) :
    L)
Tactic: have := Units.ext_iff.1 congr(toMul <| toAdditive $hy)