awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep.{u_1, u, u} k H
B : Rep.{u_1, u, u} k G
f : G →* H
φ : res f A ⟶ B
x : (↑(ModuleCat.of k ↥(cocycles₂ A)) : Type (max u u_1))
⊢ Eq (α := (a : G × G) → (↑B : Type u_1))
    (⇑((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u u_1)) →ₗ[k] (↑x2 : Type (max u u_1)))
                (CC := ModuleCat.carrier) (mapCocycles₂ f φ) :
              (a : (↑(ModuleCat.of k ↥(cocycles₂ A)) : Type (max u u_1))) →
                (↑(ModuleCat.of k ↥(cocycles₂ B)) : Type (max u u_1)))
            x :
          (↑(ModuleCat.of k ↥(cocycles₂ B)) : Type (max u u_1))) :
      (a : G × G) → (↑B : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u u_1)) →ₗ[k] (↑x2 : Type (max u u_1)))
          (CC := ModuleCat.carrier) (cochainsMap₂ f φ) :
        (a : (↑(ModuleCat.of k (H × H → (↑A : Type u_1))) : Type (max u u_1))) →
          (↑(ModuleCat.of k (G × G → (↑B : Type u_1))) : Type (max u u_1)))
      (⇑x : (a : H × H) → (↑A : Type u_1)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
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
φ : res f A ⟶ B
⊢ cocyclesMap f φ 2 ≫ (isoCocycles₂ B).hom = (isoCocycles₂ A).hom ≫ mapCocycles₂ f φ

Tactic:
simp [← cancel_mono (moduleCatLeftHomologyData (shortComplexH2 B)).i, mapShortComplexH2,
    cochainsMap_f_2_comp_cochainsIso₂ f]

Premises used: groupCohomology.cochainsMap_f_2_comp_cochainsIso₂, groupCohomology.shortComplexH2, CategoryTheory.cancel_mono, groupCohomology.mapShortComplexH2, CategoryTheory.ShortComplex.moduleCatLeftHomologyData, CategoryTheory.ShortComplex.LeftHomologyData.i
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
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
φ : res f A ⟶ B
⊢ H2π A ≫ map f φ 2 = mapCocycles₂ f φ ≫ H2π B

Tactic:
simp [H2π, Iso.inv_comp_eq, ← cocyclesMap_comp_isoCocycles₂_hom_assoc]

Premises used: CategoryTheory.Iso.inv_comp_eq, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_assoc, groupCohomology.H2π
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
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
φ : Quiver.Hom.{?u.445319, max (?u.445319 + 1) u} (res f A) B
n_1 n : ℕ
X Y Z : Rep k G
x : X ⟶ Y
x_1 : Y ⟶ Z
simp :
  Eq (α := groupCohomology X n ⟶ groupCohomology Z n) (map (MonoidHom.id G) (x ≫ x_1) n)
    (HomologicalComplex.homologyMap
      (CategoryStruct.comp (Y := inhomogeneousCochains Y) (cochainsMap (MonoidHom.id G) x)
        (cochainsMap (MonoidHom.id G) x_1))
      n)
⊢ Eq (α := groupCohomology X n ⟶ groupCohomology Z n) (map (MonoidHom.id G) (x ≫ x_1) n)
    (CategoryStruct.comp (Y := groupCohomology Y n) (map (MonoidHom.id G) x n) (map (MonoidHom.id G) x_1 n))

Tactic:
simp only [← HomologicalComplex.homologyMap_comp]

Premises used: HomologicalComplex.homologyMap_comp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
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
φ : Quiver.Hom.{?u.445319, max (?u.445319 + 1) u} (res f A) B
n_1 n : ℕ
X Y Z : Rep k G
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ Eq (α := groupCohomology X n ⟶ groupCohomology Z n) (map (MonoidHom.id G) (x ≫ x_1) n)
    (HomologicalComplex.homologyMap
      (CategoryStruct.comp (Y := inhomogeneousCochains Y) (cochainsMap (MonoidHom.id G) x)
        (cochainsMap (MonoidHom.id G) x_1))
      n)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
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
φ : Quiver.Hom.{?u.448114, max (?u.448114 + 1) u} (res f A) B
n_1 n : ℕ
x x_1 : Rep k G
⊢ Eq (α := Functor.obj (functor k G n) x ⟶ Functor.obj (functor k G n) x_1)
    (CategoryTheory.Functor.map (functor k G n) 0) 0

Tactic:
simp [map]

Premises used: groupCohomology.map
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
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 (α := 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' := ⋯ }))
        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' := ⋯ })
            (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' := ⋯ })))
        n ≫
      HomologicalComplex.homologyπ (inhomogeneousCochains (of (MonoidHom.comp Y.ρ f))) n)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
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)
h₁ : ∀ (a : L), Eq (α := L) ((x : (a : L) → L) a : L) ((y : (a : L) → L) a : L)
⊢ x = y

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
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)
a : L
⊢ Eq (α := L) ((x : (a : L) → L) a : L) ((y : (a : L) → L) a : L)

Tactic:
DFunLike.ext_iff.1 h _

Premises used: DFunLike.ext_iff, Iff.mp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
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)
a : L
⊢ Eq (α := L) ((x : (a : L) → L) a : L) ((y : (a : L) → L) a : L)

Tactic:
exact DFunLike.ext_iff.1 h _

Premises used: DFunLike.ext_iff, Iff.mp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
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), aux f z ≠ 0

Tactic:
not_forall.1 (fun H => aux_ne_zero f <| funext <| fun x => H x)

Premises used: groupCohomology.Hilbert90.aux_ne_zero, funext, Iff.mp, Classical.not_forall
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
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
obtain : ∀ (z : L) (hz : aux f z ≠ 0), IsMulCoboundary₁ f
⊢ 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)

Premises used: groupCohomology.Hilbert90.aux_ne_zero, funext, Iff.mp, Classical.not_forall
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
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
⊢ aux f z = ∑ h : Gal(L/K), HMul.hMul (β := L) (↑(f h) : L) ((h : (a : L) → L) z : L)

Tactic:
simp [aux, Finsupp.linearCombination, Finsupp.sum_fintype]

Premises used: Finsupp.sum_fintype, Finsupp.linearCombination, groupCohomology.Hilbert90.aux
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
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
⊢ 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]
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
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)
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
⊢ IsMulCoboundary₁ f

Tactic:
use (Units.mk0 (aux f z) hz)⁻¹

Premises used: Units.mk0, groupCohomology.Hilbert90.aux
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
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)
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)
⊢ HDiv.hDiv (β := Lˣ) (HSMul.hSMul (β := Lˣ) g ((Units.mk0 (aux f z) hz)⁻¹ : Lˣ)) ((Units.mk0 (aux f z) hz)⁻¹ : Lˣ) =
    f g

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 ⊢

Premises used: Units.ext_iff, map_inv, Units.coe_map, MonoidHom.coe_coe, groupCohomology.IsMulCocycle₁, AlgEquiv.smul_units_def, div_inv_eq_mul, Units.val_mk0, Units.val_mul, inv_mul_eq_iff_eq_mul
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
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 :
  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))
⊢ ∑ 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_rw [map_sum, map_mul, Finset.sum_mul, mul_assoc, mul_comm _ (f _ : L), ← mul_assoc, ← hf g]

Premises used: Units.val, mul_assoc, map_sum, map_mul, mul_comm, Finset.sum_mul
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
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)
⊢ 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:
eq_comm.1 (Fintype.sum_bijective (fun i => g * i)
    (Group.mulLeft_bijective g) _ _ (fun i => rfl))

Premises used: HMul.hMul, eq_comm, Group.mulLeft_bijective, Fintype.sum_bijective, Iff.mp, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
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)
⊢ 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:
exact eq_comm.1 (Fintype.sum_bijective (fun i => g * i)
    (Group.mulLeft_bijective g) _ _ (fun i => rfl))

Premises used: HMul.hMul, eq_comm, Group.mulLeft_bijective, Fintype.sum_bijective, Iff.mp, rfl
-- 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
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))

Tactic:
(coboundariesOfIsMulCoboundary₁ ?_).2

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, Set.range, groupCohomology.coboundariesOfIsMulCoboundary₁, Subtype.property
-- 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
a : (↑(H1 (G := Gal(L/K)) (Rep.ofAlgebraAutOnUnits K L)) : Type)
x : ↥(cocycles₁ (Rep.ofAlgebraAutOnUnits K L))
refine : IsMulCoboundary₁ (G := Gal(L/K)) (M := Lˣ) x.1
⊢ 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))

Tactic:
refine (coboundariesOfIsMulCoboundary₁ ?_).2

Premises used: groupCohomology.coboundariesOfIsMulCoboundary₁, Subtype.property
-- 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
a : (↑(H1 (G := Gal(L/K)) (Rep.ofAlgebraAutOnUnits K L)) : Type)
x : ↥(cocycles₁ (Rep.ofAlgebraAutOnUnits K L))
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
⊢ 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β⟩

Premises used: groupCohomology.isMulCocycle₁_of_mem_cocycles₁, groupCohomology.isMulCoboundary₁_of_isMulCocycle₁_of_aut_to_units, Subtype.val, Subtype.property
-- 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
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ˣ
h : ∀ (g : Gal(L/K)), g • β / β = x.1 g
⊢ IsMulCoboundary₁ (G := Gal(L/K)) (M := Lˣ) x.1

Tactic:
use β
-- 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
x : 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ˣ) x))))) :
        L) :
      L)
    ((algebraMap K L : (a : K) → L) ((Algebra.norm K : (a : L) → K) (↑x : L) : K) : L)

Tactic:
simp [Algebra.norm_eq_prod_automorphisms, Representation.norm]

Premises used: Algebra.norm_eq_prod_automorphisms, Representation.norm
-- 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)
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
⊢ Eq (α := K) ((Algebra.norm K : (a : L) → K) x⁻¹ : K) (1 : K)

Tactic:
simp [Algebra.norm_inv, hx]

Premises used: Algebra.norm_inv
-- 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)
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
⊢ 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]
-- 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)
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)
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
⊢ ∃ (y : Lˣ), HDiv.hDiv (β := L) (↑y : L) ((g : (a : L) → L) (↑y : L) : L) = x

Tactic:
obtain ⟨y, hy⟩ := H _ hxinv
-- 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)
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⁻¹
h : HDiv.hDiv (β := L) (↑y : L) ((g : (a : L) → L) (↑y : L) : L) = x
⊢ ∃ (y : Lˣ), HDiv.hDiv (β := L) (↑y : L) ((g : (a : L) → L) (↑y : L) : L) = x

Tactic:
use y
-- 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)
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⁻¹
⊢ (g : (a : L) → L) (↑y : L) = x⁻¹ * (↑y : L)

Tactic:
rw [IsUnit.div_eq_iff y.isUnit] at hy

Premises used: IsUnit.div_eq_iff, Units.isUnit
-- 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)
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)
h : (↑y : L) / (x⁻¹ * (↑y : L)) = x
⊢ HDiv.hDiv (β := L) (↑y : L) ((g : (a : L) → L) (↑y : L) : L) = x

Tactic:
rw [hy]
-- 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)
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)
⊢ (↑y : L) / (x⁻¹ * (↑y : L)) = x

Tactic:
field_simp