awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ_1 : Quiver.Hom.{?u.450927, max (?u.450927 + 1) u} (res f A) B
n_1 n : ℕ
X Y : Rep k H
φ : X ⟶ Y
⊢ Eq (α := Functor.obj (functor k H n) X ⟶ Functor.obj (resFunctor f ⋙ functor k G n) Y)
    (CategoryTheory.Functor.map (functor k H n) φ ≫ map f (𝟙 (res f Y)) n)
    (map f (𝟙 (res f X)) n ≫ CategoryTheory.Functor.map (resFunctor f ⋙ functor k G n) φ)
have simp : Eq (α := cocycles X n ⟶ groupCohomology (of (MonoidHom.comp Y.ρ f)) n)
  (HomologicalComplex.cyclesMap
      (cochainsMap (MonoidHom.comp (MonoidHom.id H) f)
        (ofHom
          {
            toLinearMap :=
              (↑(Hom.hom φ) :
                [inst_3 :
                    FunLike (IntertwiningMap (MonoidHom.comp X.ρ (MonoidHom.id H)) Y.ρ) (↑X : Type u) (↑Y : Type u)] →
                  [SemilinearMapClass (IntertwiningMap (MonoidHom.comp X.ρ (MonoidHom.id H)) Y.ρ) (RingHom.id k)
                        (↑X : Type u) (↑Y : Type u)] →
                    (↑X : Type u) →ₗ[k] (↑Y : Type u)),
            isIntertwining' := sorry }))
      n ≫
    HomologicalComplex.homologyπ (inhomogeneousCochains (res f Y)) n)
  (HomologicalComplex.cyclesMap
      (cochainsMap (f.comp (MonoidHom.id G))
        (CategoryStruct.comp (Y := of ((MonoidHom.comp X.ρ f).comp (MonoidHom.id G)))
          (ofHom
            {
              toLinearMap :=
                (↑(IntertwiningMap.id (MonoidHom.comp X.ρ f)) :
                  [inst_3 :
                      FunLike (IntertwiningMap (MonoidHom.comp X.ρ f) (MonoidHom.comp X.ρ f)) (↑X : Type u)
                        (↑X : Type u)] →
                    [SemilinearMapClass (IntertwiningMap (MonoidHom.comp X.ρ f) (MonoidHom.comp X.ρ f)) (RingHom.id k)
                          (↑X : Type u) (↑X : Type u)] →
                      (↑X : Type u) →ₗ[k] (↑X : Type u)),
              isIntertwining' := sorry })
          (ofHom
            {
              toLinearMap :=
                (↑(Hom.hom φ) :
                  [inst_3 : FunLike (X.ρ.IntertwiningMap Y.ρ) (↑X : Type u) (↑Y : Type u)] →
                    [SemilinearMapClass (X.ρ.IntertwiningMap Y.ρ) (RingHom.id k) (↑X : Type u) (↑Y : Type u)] →
                      (↑X : Type u) →ₗ[k] (↑Y : Type u)),
              isIntertwining' := sorry })))
      n ≫
    HomologicalComplex.homologyπ (inhomogeneousCochains (of (MonoidHom.comp Y.ρ f))) n)
Tactic: simp only [functor_obj, Functor.comp_obj, functor_map, Functor.comp_map,
      ← cancel_epi (groupCohomology.π _ n), HomologicalComplex.homologyπ_naturality_assoc,
      HomologicalComplex.homologyπ_naturality, ← HomologicalComplex.cyclesMap_comp_assoc,
      ← cochainsMap_comp, res_obj_ρ, Category.comp_id, Rep.hom_id]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
f : Gal(L/K) → Lˣ
x y : Gal(L/K)
h :
  Eq.{u_2 + 1} (α := L →* L) ((fun (f : Gal(L/K)) ↦ ((↑f : L →* L) : L →* L)) x)
    ((fun (f : Gal(L/K)) ↦ ((↑f : L →* L) : L →* L)) y)
⊢ x = y
have h₁ : ∀ (a : L), Eq (α := L) ((x : (a : L) → L) a : L) ((y : (a : L) → L) a : L)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
f : Gal(L/K) → Lˣ
hf : IsMulCocycle₁ f
⊢ IsMulCoboundary₁ f
have obtain : ∀ (z : L) (hz : aux f z ≠ 0), IsMulCoboundary₁ f
Tactic: obtain ⟨z, hz⟩ : ∃ z, aux f z ≠ 0 :=
    not_forall.1 (fun H => aux_ne_zero f <| funext <| fun x => H x)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
f : Gal(L/K) → Lˣ
hf : IsMulCocycle₁ f
z : L
hz : aux f z ≠ 0
⊢ IsMulCoboundary₁ f
have this : aux f z = ∑ h : Gal(L/K), HMul.hMul (β := L) (↑(f h) : L) ((h : (a : L) → L) z : L)
Tactic: have : aux f z = ∑ h, f h * h z := by simp [aux, Finsupp.linearCombination, Finsupp.sum_fintype]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
f : Gal(L/K) → Lˣ
hf : IsMulCocycle₁ f
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h : Gal(L/K), HMul.hMul (β := L) (↑(f h) : L) ((h : (a : L) → L) z : L)
⊢ IsMulCoboundary₁ f
have h : ∀ (g : Gal(L/K)),
  HDiv.hDiv (β := Lˣ) (HSMul.hSMul (β := Lˣ) g ((Units.mk0 (aux f z) hz)⁻¹ : Lˣ)) ((Units.mk0 (aux f z) hz)⁻¹ : Lˣ) =
    f g
Tactic: use (Units.mk0 (aux f z) hz)⁻¹
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
f : Gal(L/K) → Lˣ
hf : IsMulCocycle₁ f
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h : Gal(L/K), HMul.hMul (β := L) (↑(f h) : L) ((h : (a : L) → L) z : L)
g : Gal(L/K)
⊢ HDiv.hDiv (β := Lˣ) (HSMul.hSMul (β := Lˣ) g ((Units.mk0 (aux f z) hz)⁻¹ : Lˣ)) ((Units.mk0 (aux f z) hz)⁻¹ : Lˣ) =
    f g
have h : ∀ (hf : ∀ (g h : Gal(L/K)), (↑(f (g * h)) : L) = HMul.hMul (α := L) ((g : (a : L) → L) (↑(f h) : L) : L) (↑(f g) : L)),
  ∑ h : Gal(L/K), HMul.hMul (β := L) (↑(f h) : L) ((h : (a : L) → L) z : L) =
    HMul.hMul (α := L)
      ((g : (a : L) → L) (∑ h : Gal(L/K), HMul.hMul (β := L) (↑(f h) : L) ((h : (a : L) → L) z : L)) : L) (↑(f g) : L)
Tactic: simp only [IsMulCocycle₁, AlgEquiv.smul_units_def,
    map_inv, div_inv_eq_mul, inv_mul_eq_iff_eq_mul, Units.ext_iff, this,
    Units.val_mul, Units.coe_map, Units.val_mk0, MonoidHom.coe_coe] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
f : Gal(L/K) → Lˣ
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h : Gal(L/K), HMul.hMul (β := L) (↑(f h) : L) ((h : (a : L) → L) z : L)
g : Gal(L/K)
hf : ∀ (g h : Gal(L/K)), (↑(f (g * h)) : L) = HMul.hMul (α := L) ((g : (a : L) → L) (↑(f h) : L) : L) (↑(f g) : L)
⊢ ∑ h : Gal(L/K), HMul.hMul (β := L) (↑(f h) : L) ((h : (a : L) → L) z : L) =
    HMul.hMul (α := L)
      ((g : (a : L) → L) (∑ h : Gal(L/K), HMul.hMul (β := L) (↑(f h) : L) ((h : (a : L) → L) z : L)) : L) (↑(f g) : L)
have h : Eq.{u_2 + 1} (α := L) (∑ h : Gal(L/K), HMul.hMul (β := L) (↑(f h) : L) ((h : (a : L) → L) z : L))
  (∑ x : Gal(L/K), HMul.hMul (β := L) (↑(f (g * x)) : L) ((g : (a : L) → L) ((x : (a : L) → L) z : L) : L))
Tactic: simp_rw [map_sum, map_mul, Finset.sum_mul, mul_assoc, mul_comm _ (f _ : L), ← mul_assoc, ← hf g]
-- 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
a : (↑(H1 (G := Gal(L/K)) (Rep.ofAlgebraAutOnUnits K L)) : Type)
x : ↥(cocycles₁ (Rep.ofAlgebraAutOnUnits K L))
⊢ Membership.mem (γ := Submodule ℤ (Gal(L/K) → (↑(Rep.ofAlgebraAutOnUnits K L) : Type)))
    (coboundaries₁ (Rep.ofAlgebraAutOnUnits K L)) (⇑x : (a : Gal(L/K)) → (↑(Rep.ofAlgebraAutOnUnits K L) : Type))
have refine : IsMulCoboundary₁ (G := Gal(L/K)) (M := Lˣ) x.1
Tactic: refine (coboundariesOfIsMulCoboundary₁ ?_).2
-- 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
a : (↑(H1 (G := Gal(L/K)) (Rep.ofAlgebraAutOnUnits K L)) : Type)
x : ↥(cocycles₁ (Rep.ofAlgebraAutOnUnits K L))
⊢ IsMulCoboundary₁ (G := Gal(L/K)) (M := Lˣ) x.1
have rcases : ∀ (β : Lˣ) (hβ : ∀ (g : Gal(L/K)), g • β / β = (↑x : Gal(L/K) → (↑(Rep.ofAlgebraAutOnUnits K L) : Type)) g),
  IsMulCoboundary₁ (G := Gal(L/K)) (M := Lˣ) x.1
Tactic: rcases isMulCoboundary₁_of_isMulCocycle₁_of_aut_to_units x.1
      (isMulCocycle₁_of_mem_cocycles₁ _ x.2) with ⟨β, hβ⟩
-- 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
a : (↑(H1 (G := Gal(L/K)) (Rep.ofAlgebraAutOnUnits K L)) : Type)
x : ↥(cocycles₁ (Rep.ofAlgebraAutOnUnits K L))
β : Lˣ
hβ : ∀ (g : Gal(L/K)), g • β / β = (↑x : Gal(L/K) → (↑(Rep.ofAlgebraAutOnUnits K L) : Type)) g
w : Lˣ
⊢ IsMulCoboundary₁ (G := Gal(L/K)) (M := Lˣ) x.1
have h : ∀ (g : Gal(L/K)), g • β / β = x.1 g
Tactic: use β
-- 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 : L
hx : Eq (α := K) ((Algebra.norm K : (a : L) → K) x : K) (1 : K)
H :
  ∀ (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
have hxinv : Eq (α := K) ((Algebra.norm K : (a : L) → K) x⁻¹ : K) (1 : K)
Tactic: have hxinv : Algebra.norm K x⁻¹ = 1 := by simp [Algebra.norm_inv, hx]
-- 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 : L
hx : Eq (α := K) ((Algebra.norm K : (a : L) → K) x : K) (1 : K)
H :
  ∀ (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
hxinv : Eq (α := K) ((Algebra.norm K : (a : L) → K) x⁻¹ : K) (1 : K)
⊢ ∃ (y : Lˣ), HDiv.hDiv (β := L) (↑y : L) ((g : (a : L) → L) (↑y : L) : L) = x
have obtain : ∀ (y : Lˣ) (hy : 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: obtain ⟨y, hy⟩ := H _ hxinv
-- 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 : L
hx : Eq (α := K) ((Algebra.norm K : (a : L) → K) x : K) (1 : K)
H :
  ∀ (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
hxinv : Eq (α := K) ((Algebra.norm K : (a : L) → K) x⁻¹ : K) (1 : K)
y : Lˣ
hy : 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
have h : HDiv.hDiv (β := L) (↑y : L) ((g : (a : L) → L) (↑y : L) : L) = x
Tactic: use y
-- 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 : L
hx : Eq (α := K) ((Algebra.norm K : (a : L) → K) x : K) (1 : K)
H :
  ∀ (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
hxinv : Eq (α := K) ((Algebra.norm K : (a : L) → K) x⁻¹ : K) (1 : K)
y : Lˣ
hy : HDiv.hDiv (α := L) ((g : (a : L) → L) (↑y : L) : L) (↑y : L) = x⁻¹
⊢ HDiv.hDiv (β := L) (↑y : L) ((g : (a : L) → L) (↑y : L) : L) = x
have hy₁ : (g : (a : L) → L) (↑y : L) = x⁻¹ * (↑y : L)
Tactic: rw [IsUnit.div_eq_iff y.isUnit] at hy
Cleared hypotheses: hy
-- 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 : L
hx : Eq (α := K) ((Algebra.norm K : (a : L) → K) x : K) (1 : K)
H :
  ∀ (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
hxinv : Eq (α := K) ((Algebra.norm K : (a : L) → K) x⁻¹ : K) (1 : K)
y : Lˣ
hy : (g : (a : L) → L) (↑y : L) = x⁻¹ * (↑y : L)
⊢ HDiv.hDiv (β := L) (↑y : L) ((g : (a : L) → L) (↑y : L) : L) = x
have h : (↑y : L) / (x⁻¹ * (↑y : L)) = x
Tactic: rw [hy]
-- 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 : L
hx : Eq (α := K) ((Algebra.norm K : (a : L) → K) x : K) (1 : K)
⊢ ∃ (y : Lˣ), HDiv.hDiv (β := L) (↑y : L) ((g : (a : L) → L) (↑y : L) : L) = x
have 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
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
-- 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) ⋯
⊢ ∃ (y : Lˣ), HDiv.hDiv (α := L) ((g : (a : L) → L) (↑y : L) : L) (↑y : L) = x
have 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)
Tactic: have hx' : algebraMap K L (Algebra.norm K (xu : L)) = _ := congrArg (algebraMap K L) hx
-- 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) ((algebraMap K L : (a : K) → L) ((Algebra.norm K : (a : L) → K) (↑xu : L) : K) : L)
    ((algebraMap K L : (a : K) → L) 1 : L)
⊢ ∃ (y : Lˣ), HDiv.hDiv (α := L) ((g : (a : L) → L) (↑y : L) : L) (↑y : L) = x
have 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
Tactic: rw [← norm_ofAlgebraAutOnUnits_eq xu, map_one] at hx'
Cleared hypotheses: hx'
-- 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
⊢ ∃ (y : Lˣ), HDiv.hDiv (α := L) ((g : (a : L) → L) (↑y : L) : L) (↑y : L) = x
have this : 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⟩
-- 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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∃ (y : Lˣ), HDiv.hDiv (α := L) ((g : (a : L) → L) (↑y : L) : L) (↑y : L) = x
have 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))
              sorry) :
          (↑(ofAlgebraAutOnUnits K L) : Type)) :
        (↑(ofAlgebraAutOnUnits K L) : Type))),
  ∃ (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⟩
-- 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 : 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))
⊢ ∃ (y : Lˣ), HDiv.hDiv (α := L) ((g : (a : L) → L) (↑y : L) : L) (↑y : 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) =
  x
Tactic: use toMul <| toAdditive y
-- 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)
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
have rw : Function.Injective (α := A) (β := L)
  (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap A K)) : (a : A) → L)
Tactic: rw [Module.isTorsionFree_iff_algebraMap_injective, IsScalarTower.algebraMap_eq A K L]