-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 (goal)
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_1 : 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))
this :
  (↑((toMul : (a : Additive Lˣ) → Lˣ)
          (Mathlib.Tactic.TermCongr.cHole
            (HSub.hSub (α := (↑(ofMulDistribMulAction Gal(L/K) Lˣ) : Type))
              ((ofMul : (a : Lˣ) → Additive Lˣ)
                  ((Units.map (↑g : L →* L) : (a : Lˣ) → Lˣ) ((toMul : (a : Additive Lˣ) → Lˣ) y)) :
                Additive Lˣ)
              y)
            (p :=
            HSub.hSub (α := (↑(ofMulDistribMulAction Gal(L/K) Lˣ) : Type))
                ((ofMul : (a : Lˣ) → Additive Lˣ)
                    ((Units.map (↑g : L →* L) : (a : Lˣ) → Lˣ) ((toMul : (a : Additive Lˣ) → Lˣ) y)) :
                  Additive Lˣ)
                y =
              (ofMul : (a : Lˣ) → Additive Lˣ) (IsUnit.unit (a := x) ⋯))
            ⋯)) :
      L) =
    x
⊢ 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 h : 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) =
  (↑(HDiv.hDiv (α := Lˣ) (β := Lˣ)
        ((toMul : (a : Additive Lˣ) → Lˣ)
            ((ofMul : (a : Lˣ) → Additive Lˣ)
              ((Units.map (↑g : L →* L) : (a : Lˣ) → Lˣ) ((toMul : (a : Additive Lˣ) → Lˣ) y))) :
          Lˣ)
        ((toMul : (a : Additive Lˣ) → Lˣ) y : Lˣ)) :
    L)
Tactic: rw [← this, toMul_sub]