awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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ˣ
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)
⊢ 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 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
Tactic: rw [← h, eq_div_iff_mul_eq] 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ˣ
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
⊢ 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 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)
Tactic: rw [← h, eq_div_iff_mul_eq] at hε
Cleared hypotheses: 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ˣ
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
⊢ 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ε₁ : 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ε
Cleared hypotheses: 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ˣ
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 (β := 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ε₁ : 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ε
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ˣ
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
⊢ 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 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)
Tactic: apply IsIntegralClosure.algebraMap_injective B A L
-- 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ˣ
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
⊢ 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)
have 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)
Tactic: rw [map_mul, ← 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ˣ
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
⊢ 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)
have refine_2 : Eq (α := 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)
  (((↑g : L →ₐ[K] L) : (a : L) → L) ((algebraMap B L : (a : B) → L) a : L) : L)
Tactic: congr 1
-- 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ˣ
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) (IsLocalization.mk' L a b) ((g : (a : L) → L) (IsLocalization.mk' L a b) : L)
e : Eq (α := L) ((g : (a : L) → L) (IsLocalization.mk' L a b) : L) (0 : L)
⊢ False
have hε₁ : Eq (α := L) ((algebraMap B L : (a : B) → L) η : L) (0 : L)
Tactic: rw [(map_eq_zero _).mp e, zero_div] at hε
Cleared hypotheses: hε, e
-- 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ˣ
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ε : Eq (α := L) ((algebraMap B L : (a : B) → L) η : L) (0 : L)
e : Eq (α := L) ((g : (a : L) → L) (IsLocalization.mk' L a b) : L) (0 : L)
⊢ False
have refine_2 : ∀ (hη : Eq (α := K) 0 1) (this : Module.IsTorsionFree A L)
  (this : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_2} (R := A) B A⁰) 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_3 : t • IsLocalization.mk' L a b = (algebraMap B L : (a : B) → L) a)
  (hε : Eq (α := L) ((algebraMap B L : (a : B) → L) η : L) (0 : L))
  (e : Eq (α := L) ((g : (a : L) → L) (IsLocalization.mk' L a b) : L) (0 : L)), False
Tactic: rw [hε, Algebra.norm_zero] at hη
Cleared hypotheses: this_1, this_2, η', ε, a, b, h, t, ht, ht', this, hε, e
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i : ℕ
⊢ Exact (ShortComplex.map (X.map (cochainsFunctor k G)) (HomologicalComplex.eval (ModuleCat k) (ComplexShape.up ℕ) i))
have this : (Rep.Hom.hom X.f).range = (Rep.Hom.hom X.g).ker
Tactic: have : LinearMap.range X.f.hom.toLinearMap = LinearMap.ker X.g.hom.toLinearMap :=
        (hX.exact.map (forget₂ (Rep k G) (ModuleCat k))).moduleCat_range_eq_ker
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
y : (↑X.X₂ : Type (max u u_1))
x : G → (↑X.X₁ : Type (max u u_1))
hx :
  Eq (α := G → (↑X.X₂ : Type (max u u_1)))
    ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type (max u u_1))) → (↑X.X₂ : Type (max u u_1))) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u u_1)) →ₗ[k] (↑x2 : Type (max u u_1)))
          (CC := ModuleCat.carrier) (d₀₁.{u, u_1} X.X₂) :
        (a : (↑(ModuleCat.of k (↑X.X₂ : Type (max u u_1))) : Type (max u u_1))) →
          (↑(ModuleCat.of k (G → (↑X.X₂ : Type (max u u_1)))) : Type (max u u_1)))
      y)
⊢ x ∈ cocycles₁ X.X₁
have a : Eq (α := G × G → (↑X.X₂ : Type (max u u_1)))
  ((fun (x : G × G → (↑X.X₁ : Type (max u u_1))) ↦
      ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type (max u u_1))) → (↑X.X₂ : Type (max u u_1))) ∘ x :
        G × G → (↑X.X₂ : Type (max u u_1))))
    ((ModuleCat.Hom.hom (d₁₂ X.X₁) :
        (a : G → (↑X.X₁ : Type (max u u_1))) →
          (↑(ModuleCat.of k (G × G → (↑X.X₁ : Type (max u u_1)))) : Type (max u u_1)))
      x))
  ((fun (x : G × G → (↑X.X₁ : Type (max u u_1))) ↦
      ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type (max u u_1))) → (↑X.X₂ : Type (max u u_1))) ∘ x :
        G × G → (↑X.X₂ : Type (max u u_1))))
    0)
Tactic: apply Function.Injective.comp_left ((Rep.mono_iff_injective X.f).1 hX.2)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
y : (↑X.X₂ : Type (max u u_1))
x : G → (↑X.X₁ : Type (max u u_1))
hx :
  Eq (α := G → (↑X.X₂ : Type (max u u_1)))
    ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type (max u u_1))) → (↑X.X₂ : Type (max u u_1))) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u u_1)) →ₗ[k] (↑x2 : Type (max u u_1)))
          (CC := ModuleCat.carrier) (d₀₁.{u, u_1} X.X₂) :
        (a : (↑(ModuleCat.of k (↑X.X₂ : Type (max u u_1))) : Type (max u u_1))) →
          (↑(ModuleCat.of k (G → (↑X.X₂ : Type (max u u_1)))) : Type (max u u_1)))
      y)
⊢ Eq (α := G × G → (↑X.X₂ : Type (max u u_1)))
    ((fun (x : G × G → (↑X.X₁ : Type (max u u_1))) ↦
        ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type (max u u_1))) → (↑X.X₂ : Type (max u u_1))) ∘ x :
          G × G → (↑X.X₂ : Type (max u u_1))))
      ((ModuleCat.Hom.hom (d₁₂ X.X₁) :
          (a : G → (↑X.X₁ : Type (max u u_1))) →
            (↑(ModuleCat.of k (G × G → (↑X.X₁ : Type (max u u_1)))) : Type (max u u_1)))
        x))
    ((fun (x : G × G → (↑X.X₁ : Type (max u u_1))) ↦
        ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type (max u u_1))) → (↑X.X₂ : Type (max u u_1))) ∘ x :
          G × G → (↑X.X₂ : Type (max u u_1))))
      0)
have this : Eq (α := (↑(shortComplexH1.{u, u_1} X.X₂).X₃ : Type (max u 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) (X := X₂ (shortComplexH1.{u, u_1} (G := G) X.1)) (Y :=
          (shortComplexH1.{u, u_1} X.X₂).X₃)
          (g (shortComplexH1.{u, u_1} (G := G) X.1) ≫ Hom.τ₃ (mapShortComplexH1 (MonoidHom.id G) X.f)) :
        (a : (↑(shortComplexH1 X.1).X₂ : Type (max u u_1))) → (↑(shortComplexH1 X.X₂).X₃ : Type (max u u_1)))
      x :
    (↑(shortComplexH1.{u, u_1} X.X₂).X₃ : Type (max u 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) (X := X₂ (shortComplexH1.{u, u_1} (G := G) X.1))
          (Hom.τ₂ (mapShortComplexH1 (MonoidHom.id G) X.f) ≫ (shortComplexH1.{u, u_1} X.X₂).g) :
        (a : (↑(shortComplexH1 X.1).X₂ : Type (max u u_1))) → (↑(shortComplexH1 X.X₂).X₃ : Type (max u u_1)))
      x :
    (↑(shortComplexH1.{u, u_1} X.X₂).X₃ : Type (max u u_1)))
Tactic: have := congr($((mapShortComplexH1 (MonoidHom.id G) X.f).comm₂₃.symm) x)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥X.X₃.ρ.invariants
y : (↑X.X₂ : Type u)
hy : (Rep.Hom.hom X.g : (a : (↑X.X₂ : Type u)) → (↑X.X₃ : Type u)) y = (↑z : (↑X.X₃ : Type u))
x : G → (↑X.X₁ : Type u)
hx :
  Eq (α := G → (↑X.X₂ : Type u)) ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₀₁ X.X₂) :
        (a : (↑(ModuleCat.of k (↑X.X₂ : Type u)) : Type u)) → (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u))
      y)
⊢ Eq (α := (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 0 1)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := (inhomogeneousCochains X.X₃).X 0) (Y :=
            (inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 0 1))
            ((inhomogeneousCochains X.X₃).d 0 (HAdd.hAdd (α := ℕ) 0 1)) :
          (a : (↑((inhomogeneousCochains X.X₃).X 0) : Type u)) → (↑((inhomogeneousCochains X.X₃).X (0 + 1)) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₀ X.X₃).inv :
              (a : (↑(ModuleCat.of k (↑X.X₃ : Type u)) : Type u)) → (↑((inhomogeneousCochains X.X₃).X 0) : Type u))
            (↑z : (↑X.X₃ : Type u)) :
          (↑((inhomogeneousCochains X.X₃).X 0) : Type u)) :
      (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 0 1)) : Type u))
    (0 : (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 0 1)) : Type u))
have rw : Eq (α := (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 0 1)) : Type u))
  ((ModuleCat.Hom.hom (d₀₁ X.X₃ ≫ (cochainsIso₁ X.X₃).inv) :
        (a : (↑(ModuleCat.of k (↑X.X₃ : Type u)) : Type u)) → (↑((inhomogeneousCochains X.X₃).X (0 + 1)) : Type u))
      (↑z : (↑X.X₃ : Type u)) :
    (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 0 1)) : Type u))
  (0 : (↑((inhomogeneousCochains X.X₃).X (HAdd.hAdd (α := ℕ) 0 1)) : Type u))
Tactic: rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₀₁_comp_inv]