awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : L
hx : Eq (α := K) ((Algebra.norm K : (a : L) → K) x : K) (1 : K)
suffices :
  ∀ (x : L),
    Eq (α := K) ((Algebra.norm K : (a : L) → K) x : K) (1 : K) →
      ∃ (y : Lˣ), HDiv.hDiv (α := L) ((g : (a : L) → L) (↑y : L) : L) (↑y : L) = x
⊢ ∃ (y : Lˣ), HDiv.hDiv (β := L) (↑y : L) ((g : (a : L) → L) (↑y : L) : L) = x

Tactic:
suffices H : ∀ x, Algebra.norm K x = 1 → ∃ y : Lˣ, g y / y = x by
    have hxinv : Algebra.norm K x⁻¹ = 1 := by simp [Algebra.norm_inv, hx]
    obtain ⟨y, hy⟩ := H _ hxinv
    use y
    rw [IsUnit.div_eq_iff y.isUnit] at hy
    rw [hy]
    field_simp
-- 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) ⋯
⊢ Eq (α := L) ((algebraMap K L : (a : K) → L) ((Algebra.norm K : (a : L) → K) (↑xu : L) : K) : L)
    ((algebraMap K L : (a : K) → L) 1 : L)

Tactic:
have hx' : algebraMap K L (Algebra.norm K (xu : L)) = _ := congrArg (algebraMap K L) hx
-- 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) ((algebraMap K L : (a : K) → L) ((Algebra.norm K : (a : L) → K) (↑xu : L) : K) : L)
    ((algebraMap K L : (a : K) → L) 1 : L)
⊢ 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

Tactic:
rw [← norm_ofAlgebraAutOnUnits_eq xu, map_one] at hx'

Premises used: groupCohomology.norm_ofAlgebraAutOnUnits_eq, map_one
-- 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
⊢ Odd (α := ℕ) 1

Tactic:
simp
-- 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
⊢ Membership.mem (α := (↑(ofAlgebraAutOnUnits K L) : Type)) (γ := Submodule ℤ (↑(ofAlgebraAutOnUnits K L) : Type))
    (LinearMap.ker (Representation.IntertwiningMap.toLinearMap (Hom.hom (norm (ofAlgebraAutOnUnits K L)))))
    ((AddEquiv.symm toAdditive : (a : Additive Lˣ) → (↑(ofMulDistribMulAction Gal(L/K) Lˣ) : Type))
        ((ofMul : (a : Lˣ) → Additive Lˣ) xu) :
      (↑(ofMulDistribMulAction Gal(L/K) Lˣ) : Type))

Tactic:
simp_all
-- 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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
have := FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff (ofAlgebraAutOnUnits K L) g hg
    1 (by simp) ⟨toAdditive.symm <| ofMul xu, by simp_all⟩
-- 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)
rcases :
  ∀ (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))),
    ∃ (y : Lˣ), HDiv.hDiv (α := L) ((g : (a : L) → L) (↑y : L) : L) (↑y : L) = x
⊢ ∃ (y : Lˣ), HDiv.hDiv (α := L) ((g : (a : L) → L) (↑y : L) : L) (↑y : L) = x

Tactic:
rcases this.1 (Subsingleton.elim (α := groupCohomology.H1 (Rep.ofAlgebraAutOnUnits K L)) _ _)
    with ⟨y, hy⟩

Premises used: Iff.mp, Subsingleton.elim
-- 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))
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) =
    x
⊢ ∃ (y : Lˣ), HDiv.hDiv (α := L) ((g : (a : L) → L) (↑y : L) : L) (↑y : L) = x

Tactic:
use toMul <| toAdditive y

Premises used: Rep.toAdditive, Additive.toMul, DFunLike.coe
-- 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)
A : Type u_1
B : Type u_2
inst_6 : CommRing A
inst_7 : CommRing B
inst_8 : Algebra A B
inst_9 : Algebra A L
inst_10 : Algebra A K
inst_11 : Algebra B L
inst_12 : IsScalarTower A B L
inst_13 : IsScalarTower A K L
inst_14 : IsFractionRing A K
inst_15 : IsDomain A
inst_16 : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (Subgroup.zpowers g) x
η : B
hη : Eq (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) η : L) : K) (1 : K)
rw :
  Function.Injective (α := A) (β := L)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap A K)) : (a : A) → L)
⊢ Module.IsTorsionFree A L

Tactic:
rw [Module.isTorsionFree_iff_algebraMap_injective, IsScalarTower.algebraMap_eq A K L]

Premises used: Module.isTorsionFree_iff_algebraMap_injective, IsScalarTower.algebraMap_eq
-- 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)
A : Type u_1
B : Type u_2
inst_6 : CommRing A
inst_7 : CommRing B
inst_8 : Algebra A B
inst_9 : Algebra A L
inst_10 : Algebra A K
inst_11 : Algebra B L
inst_12 : IsScalarTower A B L
inst_13 : IsScalarTower A K L
inst_14 : IsFractionRing A K
inst_15 : IsDomain A
inst_16 : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (Subgroup.zpowers g) x
η : B
hη : Eq (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) η : L) : K) (1 : K)
⊢ Function.Injective (α := A) (β := L)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap A K)) : (a : A) → L)

Tactic:
(algebraMap K L).injective.comp (IsFractionRing.injective A K)

Premises used: Algebra.algebraMap, IsFractionRing.injective, RingHom.injective, Function.Injective.comp
-- 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)
A : Type u_1
B : Type u_2
inst_6 : CommRing A
inst_7 : CommRing B
inst_8 : Algebra A B
inst_9 : Algebra A L
inst_10 : Algebra A K
inst_11 : Algebra B L
inst_12 : IsScalarTower A B L
inst_13 : IsScalarTower A K L
inst_14 : IsFractionRing A K
inst_15 : IsDomain A
inst_16 : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (Subgroup.zpowers g) x
η : B
hη : Eq (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) η : L) : K) (1 : K)
⊢ Function.Injective (α := A) (β := L)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap A K)) : (a : A) → L)

Tactic:
exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)

Premises used: Algebra.algebraMap, IsFractionRing.injective, RingHom.injective, Function.Injective.comp
-- 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)
A : Type u_1
B : Type u_2
inst_6 : CommRing A
inst_7 : CommRing B
inst_8 : Algebra A B
inst_9 : Algebra A L
inst_10 : Algebra A K
inst_11 : Algebra B L
inst_12 : IsScalarTower A B L
inst_13 : IsScalarTower A K L
inst_14 : IsFractionRing A K
inst_15 : IsDomain A
inst_16 : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (Subgroup.zpowers g) x
η : B
hη : Eq (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) η : L) : K) (1 : K)
⊢ Module.IsTorsionFree A L

Tactic:
have : Module.IsTorsionFree A L := by
    rw [Module.isTorsionFree_iff_algebraMap_injective, IsScalarTower.algebraMap_eq A K L]
    exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)
-- 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)
A : Type u_1
B : Type u_2
inst_6 : CommRing A
inst_7 : CommRing B
inst_8 : Algebra A B
inst_9 : Algebra A L
inst_10 : Algebra A K
inst_11 : Algebra B L
inst_12 : IsScalarTower A B L
inst_13 : IsScalarTower A K L
inst_14 : IsFractionRing A K
inst_15 : IsDomain A
inst_16 : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (Subgroup.zpowers g) x
η : B
hη : Eq (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) η : L) : K) (1 : K)
this : Module.IsTorsionFree A L
⊢ IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L

Tactic:
have : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L :=
    IsIntegralClosure.isLocalization A K L B
-- 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)
A : Type u_1
B : Type u_2
inst_6 : CommRing A
inst_7 : CommRing B
inst_8 : Algebra A B
inst_9 : Algebra A L
inst_10 : Algebra A K
inst_11 : Algebra B L
inst_12 : IsScalarTower A B L
inst_13 : IsScalarTower A K L
inst_14 : IsFractionRing A K
inst_15 : IsDomain A
inst_16 : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (Subgroup.zpowers g) x
η : B
hη : Eq (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) η : L) : K) (1 : K)
this_1 : Module.IsTorsionFree A L
this : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
h : Eq (α := L) ((algebraMap B L : (a : B) → L) η : L) (0 : L)
⊢ False

Tactic:
simp [h] at hη
-- 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)
A : Type u_1
B : Type u_2
inst_6 : CommRing A
inst_7 : CommRing B
inst_8 : Algebra A B
inst_9 : Algebra A L
inst_10 : Algebra A K
inst_11 : Algebra B L
inst_12 : IsScalarTower A B L
inst_13 : IsScalarTower A K L
inst_14 : IsFractionRing A K
inst_15 : IsDomain A
inst_16 : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (Subgroup.zpowers g) x
η : B
hη : Eq (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) η : L) : K) (1 : K)
this_1 : Module.IsTorsionFree A L
this : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L : (a : B) → L) η) ⋯
obtain :
  ∀ (ε : Lˣ) (hε : HDiv.hDiv (β := L) (↑ε : L) ((g : (a : L) → L) (↑ε : L) : L) = (algebraMap B L : (a : B) → L) η),
    ∃ (ε : B),
      ε ≠ 0 ∧
        HMul.hMul (β := B) η
            ((((galRestrict A K L B : (a : Gal(L/K)) → B ≃ₐ[A] B) g : B ≃ₐ[A] B) : (a : B) → B) ε : B) =
          ε
⊢ ∃ (ε : B),
    ε ≠ 0 ∧
      HMul.hMul (β := B) η ((((galRestrict A K L B : (a : Gal(L/K)) → B ≃ₐ[A] B) g : B ≃ₐ[A] B) : (a : B) → B) ε : B) =
        ε

Tactic:
obtain ⟨ε, hε⟩ := exists_div_of_norm_eq_one hg hη

Premises used: groupCohomology.exists_div_of_norm_eq_one
-- 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)
A : Type u_1
B : Type u_2
inst_6 : CommRing A
inst_7 : CommRing B
inst_8 : Algebra A B
inst_9 : Algebra A L
inst_10 : Algebra A K
inst_11 : Algebra B L
inst_12 : IsScalarTower A B L
inst_13 : IsScalarTower A K L
inst_14 : IsFractionRing A K
inst_15 : IsDomain A
inst_16 : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (Subgroup.zpowers g) x
η : B
hη : Eq (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) η : L) : K) (1 : K)
this_1 : Module.IsTorsionFree A L
this : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L : (a : B) → L) η) ⋯
ε : Lˣ
hε : HDiv.hDiv (β := L) (↑ε : L) ((g : (a : L) → L) (↑ε : L) : L) = (algebraMap B L : (a : B) → L) η
obtain :
  ∀ (a : B) (b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)) (h : IsLocalization.mk' L a b = (↑ε : L)),
    ∃ (ε : B),
      ε ≠ 0 ∧
        HMul.hMul (β := B) η
            ((((galRestrict A K L B : (a : Gal(L/K)) → B ≃ₐ[A] B) g : B ≃ₐ[A] B) : (a : B) → B) ε : B) =
          ε
⊢ ∃ (ε : B),
    ε ≠ 0 ∧
      HMul.hMul (β := B) η ((((galRestrict A K L B : (a : Gal(L/K)) → B ≃ₐ[A] B) g : B ≃ₐ[A] B) : (a : B) → B) ε : B) =
        ε

Tactic:
obtain ⟨a, b, h⟩ := IsLocalization.exists_mk'_eq (Algebra.algebraMapSubmonoid B A⁰) ε.1

Premises used: Units.val, nonZeroDivisors, Algebra.algebraMapSubmonoid, IsLocalization.exists_mk'_eq
-- 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)
A : Type u_1
B : Type u_2
inst_6 : CommRing A
inst_7 : CommRing B
inst_8 : Algebra A B
inst_9 : Algebra A L
inst_10 : Algebra A K
inst_11 : Algebra B L
inst_12 : IsScalarTower A B L
inst_13 : IsScalarTower A K L
inst_14 : IsFractionRing A K
inst_15 : IsDomain A
inst_16 : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (Subgroup.zpowers g) x
η : B
hη : Eq (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) η : L) : K) (1 : K)
this_1 : Module.IsTorsionFree A L
this : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L : (a : B) → L) η) ⋯
ε : Lˣ
hε : HDiv.hDiv (β := L) (↑ε : L) ((g : (a : L) → L) (↑ε : L) : L) = (algebraMap B L : (a : B) → L) η
a : B
b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)
h : IsLocalization.mk' L a b = (↑ε : L)
obtain :
  ∀ (t : A) (ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)) (ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)),
    ∃ (ε : B),
      ε ≠ 0 ∧
        HMul.hMul (β := B) η
            ((((galRestrict A K L B : (a : Gal(L/K)) → B ≃ₐ[A] B) g : B ≃ₐ[A] B) : (a : B) → B) ε : B) =
          ε
⊢ ∃ (ε : B),
    ε ≠ 0 ∧
      HMul.hMul (β := B) η ((((galRestrict A K L B : (a : Gal(L/K)) → B ≃ₐ[A] B) g : B ≃ₐ[A] B) : (a : B) → B) ε : B) =
        ε

Tactic:
obtain ⟨t, ht, ht'⟩ := b.prop

Premises used: Subtype.prop