-- Mathlib/RepresentationTheory/GroupCohomology/Hilbert90.lean
theorem isMulOneCoboundary_of_isMulOneCocycle_of_aut_to_units
    (f : (L ≃ₐ[K] L) → Lˣ) (hf : IsMulOneCocycle f) :
    IsMulOneCoboundary f

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : (L ≃ₐ[K] L) → Lˣ
hf : IsMulOneCocycle f
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h : L ≃ₐ[K] L, ↑(f h) * h z
g : L ≃ₐ[K] L
⊢ g • (Units.mk0 (aux f z) hz)⁻¹ / (Units.mk0 (aux f z) hz)⁻¹ = f g

Tactic:
simp only [IsMulOneCocycle, IsMulOneCoboundary, 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 ⊢

Result:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : (L ≃ₐ[K] L) → Lˣ
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h : L ≃ₐ[K] L, ↑(f h) * h z
g : L ≃ₐ[K] L
hf : ∀ (g h : L ≃ₐ[K] L), ↑(f (g * h)) = g ↑(f h) * ↑(f g)
⊢ ∑ h : L ≃ₐ[K] L, ↑(f h) * h z = g (∑ h : L ≃ₐ[K] L, ↑(f h) * h z) * ↑(f g)

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : (L ≃ₐ[K] L) → Lˣ
hf : IsMulOneCocycle f
⊢ IsMulOneCoboundary f

Tactic:
obtain ⟨z, hz⟩ : ∃ z, aux f z ≠ 0 :=
  not_forall.1 (fun H => aux_ne_zero f <| funext <| fun x => H x)

Result:
case intro
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : (L ≃ₐ[K] L) → Lˣ
hf : IsMulOneCocycle f
z : L
hz : aux f z ≠ 0
⊢ IsMulOneCoboundary f

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : (L ≃ₐ[K] L) → Lˣ
hf : IsMulOneCocycle f
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h : L ≃ₐ[K] L, ↑(f h) * h z
⊢ ∀ (g : L ≃ₐ[K] L), g • (Units.mk0 (aux f z) hz)⁻¹ / (Units.mk0 (aux f z) hz)⁻¹ = f g

Tactic:
intro g

Result:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : (L ≃ₐ[K] L) → Lˣ
hf : IsMulOneCocycle f
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h : L ≃ₐ[K] L, ↑(f h) * h z
g : L ≃ₐ[K] L
⊢ g • (Units.mk0 (aux f z) hz)⁻¹ / (Units.mk0 (aux f z) hz)⁻¹ = f g

Proof state:
case intro
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : (L ≃ₐ[K] L) → Lˣ
hf : IsMulOneCocycle f
z : L
hz : aux f z ≠ 0
⊢ IsMulOneCoboundary f

Tactic:
have : aux f z = ∑ h, f h * h z := by simp [aux, Finsupp.linearCombination, Finsupp.sum_fintype]

Result:
case intro
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : (L ≃ₐ[K] L) → Lˣ
hf : IsMulOneCocycle f
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h : L ≃ₐ[K] L, ↑(f h) * h z
⊢ IsMulOneCoboundary f

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : (L ≃ₐ[K] L) → Lˣ
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h : L ≃ₐ[K] L, ↑(f h) * h z
g : L ≃ₐ[K] L
hf : ∀ (g h : L ≃ₐ[K] L), ↑(f (g * h)) = g ↑(f h) * ↑(f g)
⊢ ∑ h : L ≃ₐ[K] L, ↑(f h) * h z = g (∑ h : L ≃ₐ[K] L, ↑(f h) * h z) * ↑(f g)

Tactic:
simp_rw [map_sum, map_mul, Finset.sum_mul, mul_assoc, mul_comm _ (f _ : L), ← mul_assoc, ← hf g]

Result:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : (L ≃ₐ[K] L) → Lˣ
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h : L ≃ₐ[K] L, ↑(f h) * h z
g : L ≃ₐ[K] L
hf : ∀ (g h : L ≃ₐ[K] L), ↑(f (g * h)) = g ↑(f h) * ↑(f g)
⊢ ∑ h : L ≃ₐ[K] L, ↑(f h) * h z = ∑ x : L ≃ₐ[K] L, ↑(f (g * x)) * g (x z)

Proof state:
case intro
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : (L ≃ₐ[K] L) → Lˣ
hf : IsMulOneCocycle f
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h : L ≃ₐ[K] L, ↑(f h) * h z
⊢ IsMulOneCoboundary f

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

Result:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : (L ≃ₐ[K] L) → Lˣ
hf : IsMulOneCocycle f
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h : L ≃ₐ[K] L, ↑(f h) * h z
⊢ ∀ (g : L ≃ₐ[K] L), g • (Units.mk0 (aux f z) hz)⁻¹ / (Units.mk0 (aux f z) hz)⁻¹ = f g

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : (L ≃ₐ[K] L) → Lˣ
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h : L ≃ₐ[K] L, ↑(f h) * h z
g : L ≃ₐ[K] L
hf : ∀ (g h : L ≃ₐ[K] L), ↑(f (g * h)) = g ↑(f h) * ↑(f g)
⊢ ∑ h : L ≃ₐ[K] L, ↑(f h) * h z = ∑ x : L ≃ₐ[K] L, ↑(f (g * x)) * g (x z)

Tactic:
exact eq_comm.1 (Fintype.sum_bijective (fun i => g * i)
  (Group.mulLeft_bijective g) _ _ (fun i => rfl))

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : (L ≃ₐ[K] L) → Lˣ
hf : IsMulOneCocycle f
z : L
hz : aux f z ≠ 0
⊢ aux f z = ∑ h : L ≃ₐ[K] L, ↑(f h) * h z

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

Result:
no goals