awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ ∃ (ε : 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) =
        ε
have this : 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)
-- 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)
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
⊢ ∃ (ε : 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) =
        ε
have this₁ : 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
-- 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)
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) η) ⋯
⊢ ∃ (ε : 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) =
        ε
have 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) =
        ε
Tactic: obtain ⟨ε, hε⟩ := exists_div_of_norm_eq_one hg 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
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) η
⊢ ∃ (ε : 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) =
        ε
have 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) =
        ε
Tactic: obtain ⟨a, b, h⟩ := IsLocalization.exists_mk'_eq (Algebra.algebraMapSubmonoid B A⁰) ε.1
-- 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)
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)
⊢ ∃ (ε : 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) =
        ε
have 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) =
        ε
Tactic: obtain ⟨t, ht, ht'⟩ := b.prop
-- 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)
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
have rw : HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) t : L) (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']
-- 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)
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
⊢ t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a
have 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
Tactic: rw [Algebra.smul_def, IsScalarTower.algebraMap_apply A B L, ht', IsLocalization.mk'_spec']
-- 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)
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
⊢ t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a
have 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
Tactic: rw [Algebra.smul_def, IsScalarTower.algebraMap_apply A B L, ht', IsLocalization.mk'_spec']
-- 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)
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
⊢ t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a
have rw₃ : Eq (α := L) ((algebraMap B L : (a : B) → L) a : L) ((algebraMap B L : (a : B) → L) a : L)
Tactic: rw [Algebra.smul_def, IsScalarTower.algebraMap_apply A B L, ht', IsLocalization.mk'_spec']
-- 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)
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)
⊢ ∃ (ε : 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) =
        ε
have this₁ : 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']
-- 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)
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) =
        ε
have refine_1 : a ≠ 0
Tactic: refine ⟨a, ?_, ?_⟩
-- 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)
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
⊢ ∃ (ε : 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) =
        ε
have 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
Tactic: refine ⟨a, ?_, ?_⟩
-- 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)
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
⊢ False
have hε₁ : 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ε
Cleared hypotheses: 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
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)
⊢ False
have 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
Tactic: rw [← hε, Algebra.norm_zero] at hη
Cleared hypotheses: this_1, this_2, η', ε, b, t, ht, ht', h, this, hε
-- 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)
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
⊢ 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
have hε₁ : (algebraMap B L : (a : B) → L) η = HDiv.hDiv (β := L) (↑ε : L) ((g : (a : L) → L) (↑ε : L) : L)
Tactic: replace hε := hε.symm
Cleared hypotheses: hε