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)
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)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
rw :
  HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) t : L) (IsLocalization.mk' L a b) =
    (algebraMap B L : (a : B) → L) a
rw₁ :
  HMul.hMul (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) t : B) : L)
      (IsLocalization.mk' L a b) =
    (algebraMap B L : (a : B) → L) a
rw₂ :
  HMul.hMul (α := L) ((algebraMap B L : (a : B) → L) (↑b : B) : L) (IsLocalization.mk' L a b) =
    (algebraMap B L : (a : B) → L) a
rw₃ rw₄ : Eq (α := L) ((algebraMap B L : (a : B) → L) a : L) ((algebraMap B L : (a : B) → L) a : L)
⊢ t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a

Tactic:
rw [Algebra.smul_def, IsScalarTower.algebraMap_apply A B L, ht', IsLocalization.mk'_spec']

Premises used: IsLocalization.mk'_spec', Algebra.smul_def, IsScalarTower.algebraMap_apply
-- 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)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
⊢ t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a

Tactic:
have : t • IsLocalization.mk' L a b = algebraMap _ _ a := by
    rw [Algebra.smul_def, IsScalarTower.algebraMap_apply A B L, ht', IsLocalization.mk'_spec']
-- 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_2 : 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)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
this : t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a
⊢ ∃ (ε : 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:
⟨a, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- 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_2 : 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)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
this : t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a
refine_1 : a ≠ 0
refine_2 :
  HMul.hMul (β := B) η ((((galRestrict A K L B : (a : Gal(L/K)) → B ≃ₐ[A] B) g : B ≃ₐ[A] B) : (a : B) → B) a : B) = a
⊢ ∃ (ε : 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:
refine ⟨a, ?_, ?_⟩
-- 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_2 : 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) η
b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
h : IsLocalization.mk' L 0 b = (↑ε : L)
this : t • IsLocalization.mk' L 0 b = (algebraMap B L : (a : B) → L) 0
⊢ Eq (α := L) (0 : L) ((algebraMap B L : (a : B) → L) η : L)

Tactic:
simp only [IsLocalization.mk'_zero, _root_.map_zero, div_zero, ← h] at hε

Premises used: map_zero, IsLocalization.mk'_zero, div_zero
-- 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_2 : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L : (a : B) → L) η) ⋯
ε : Lˣ
b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
h : IsLocalization.mk' L 0 b = (↑ε : L)
this : t • IsLocalization.mk' L 0 b = (algebraMap B L : (a : B) → L) 0
hε : Eq (α := L) (0 : L) ((algebraMap B L : (a : B) → L) η : L)
refine_1 :
  ∀ (hη : Eq (α := K) 0 1) (this : Module.IsTorsionFree A L)
    (this : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L) (ε : Lˣ)
    (b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)) (t : A) (ht : t ∈ (↑(A⁰ : Submonoid A) : Set A))
    (ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)) (h : IsLocalization.mk' L 0 b = (↑ε : L))
    (this : t • IsLocalization.mk' L 0 b = (algebraMap B L : (a : B) → L) 0)
    (hε : Eq (α := L) (0 : L) ((algebraMap B L : (a : B) → L) η : L)), False
⊢ False

Tactic:
rw [← hε, Algebra.norm_zero] at hη

Premises used: Algebra.norm_zero
-- 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η_1 : Eq (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) η : L) : K) (1 : K)
hη : Eq (α := K) 0 1
this_1 : Module.IsTorsionFree A L
this_2 : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L : (a : B) → L) η) ⋯
ε : Lˣ
b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
h : IsLocalization.mk' L 0 b = (↑ε : L)
this : t • IsLocalization.mk' L 0 b = (algebraMap B L : (a : B) → L) 0
hε : Eq (α := L) (0 : L) ((algebraMap B L : (a : B) → L) η : L)
⊢ False

Tactic:
zero_ne_one hη

Premises used: zero_ne_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η_1 : Eq (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) η : L) : K) (1 : K)
hη : Eq (α := K) 0 1
this_1 : Module.IsTorsionFree A L
this_2 : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L : (a : B) → L) η) ⋯
ε : Lˣ
b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
h : IsLocalization.mk' L 0 b = (↑ε : L)
this : t • IsLocalization.mk' L 0 b = (algebraMap B L : (a : B) → L) 0
hε : Eq (α := L) (0 : L) ((algebraMap B L : (a : B) → L) η : L)
⊢ False

Tactic:
exact zero_ne_one hη

Premises used: zero_ne_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_2 : 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)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
this : t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a
⊢ (algebraMap B L : (a : B) → L) η = HDiv.hDiv (β := L) (↑ε : L) ((g : (a : L) → L) (↑ε : L) : L)

Tactic:
replace hε := hε.symm
-- 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_2 : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L : (a : B) → L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)
h : IsLocalization.mk' L a b = (↑ε : L)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
this : t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a
hε : (algebraMap B L : (a : B) → L) η = HDiv.hDiv (β := L) (↑ε : L) ((g : (a : L) → L) (↑ε : L) : L)
refine_2 :
  ∀
    (hε :
      HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) η : L)
          ((g : (a : L) → L) (IsLocalization.mk' L a b) : L) =
        IsLocalization.mk' L a b),
    HMul.hMul (β := B) η ((((galRestrict A K L B : (a : Gal(L/K)) → B ≃ₐ[A] B) g : B ≃ₐ[A] B) : (a : B) → B) a : B) = a
refine_2₁ :
  ∀
    (hε :
      (algebraMap B L : (a : B) → L) η =
        HDiv.hDiv (β := L) (IsLocalization.mk' L a b) ((g : (a : L) → L) (IsLocalization.mk' L a b) : L)),
    Ne (α := L) ((g : (a : L) → L) (IsLocalization.mk' L a b) : L) (0 : L)
⊢ HMul.hMul (β := B) η ((((galRestrict A K L B : (a : Gal(L/K)) → B ≃ₐ[A] B) g : B ≃ₐ[A] B) : (a : B) → B) a : B) = a

Tactic:
rw [← h, eq_div_iff_mul_eq] at hε

Premises used: eq_div_iff_mul_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_2 : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L : (a : B) → L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)
h : IsLocalization.mk' L a b = (↑ε : L)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
this : t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a
hε :
  HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) η : L)
      ((g : (a : L) → L) (IsLocalization.mk' L a b) : L) =
    IsLocalization.mk' L a b
⊢ Eq (α := L)
    ((fun (x : L) ↦ t • x)
      (HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) η : L)
        ((g : (a : L) → L) (IsLocalization.mk' L a b) : L)))
    ((fun (x : L) ↦ t • x) (IsLocalization.mk' L a b))

Tactic:
replace hε := congr_arg (t • ·) 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_2 : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L : (a : B) → L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)
h : IsLocalization.mk' L a b = (↑ε : L)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
this : t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a
hε :
  t •
      HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) η : L)
        ((g : (a : L) → L) (IsLocalization.mk' L a b) : L) =
    t • IsLocalization.mk' L a b
⊢ HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) η : L)
      (((↑g : L →ₐ[K] L) : (a : L) → L) ((algebraMap B L : (a : B) → L) a : L) : L) =
    (algebraMap B L : (a : B) → L) a

Tactic:
rw [Algebra.smul_def, mul_left_comm, ← Algebra.smul_def t, ← g.toAlgHom_apply,
        ← AlgHom.map_smul_of_tower, this] at hε

Premises used: mul_left_comm, AlgHom.map_smul_of_tower, Algebra.smul_def, AlgEquiv.toAlgHom_apply
-- 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_2 : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L : (a : B) → L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)
h : IsLocalization.mk' L a b = (↑ε : L)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
this : t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a
hε :
  HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) η : L)
      (((↑g : L →ₐ[K] L) : (a : L) → L) ((algebraMap B L : (a : B) → L) a : L) : L) =
    (algebraMap B L : (a : B) → L) a
refine_2 :
  Eq (α := L)
    ((algebraMap B L : (a : B) → L)
        (HMul.hMul (β := B) η
          ((((galRestrict A K L B : (a : Gal(L/K)) → B ≃ₐ[A] B) g : B ≃ₐ[A] B) : (a : B) → B) a : B)) :
      L)
    ((algebraMap B L : (a : B) → L) a : L)
⊢ HMul.hMul (β := B) η ((((galRestrict A K L B : (a : Gal(L/K)) → B ≃ₐ[A] B) g : B ≃ₐ[A] B) : (a : B) → B) a : B) = a

Tactic:
apply IsIntegralClosure.algebraMap_injective B A L

Premises used: IsIntegralClosure.algebraMap_injective
-- 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_2 : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L : (a : B) → L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰)
h : IsLocalization.mk' L a b = (↑ε : L)
t : A
ht : t ∈ (↑(A⁰ : Submonoid A) : Set A)
ht' : (algebraMap A B : (a : A) → B) t = (↑b : B)
this : t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a
hε :
  HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) η : L)
      (((↑g : L →ₐ[K] L) : (a : L) → L) ((algebraMap B L : (a : B) → L) a : L) : L) =
    (algebraMap B L : (a : B) → L) a
refine_2 :
  HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) η : L)
      ((algebraMap B L : (a : B) → L)
          ((((galRestrict A K L B : (a : Gal(L/K)) → B ≃ₐ[A] B) g : B ≃ₐ[A] B) : (a : B) → B) a : B) :
        L) =
    HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) η : L)
      (((↑g : L →ₐ[K] L) : (a : L) → L) ((algebraMap B L : (a : B) → L) a : L) : L)
⊢ Eq (α := L)
    ((algebraMap B L : (a : B) → L)
        (HMul.hMul (β := B) η
          ((((galRestrict A K L B : (a : Gal(L/K)) → B ≃ₐ[A] B) g : B ≃ₐ[A] B) : (a : B) → B) a : B)) :
      L)
    ((algebraMap B L : (a : B) → L) a : L)

Tactic:
rw [map_mul, ← hε]

Premises used: map_mul