awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
V : Type u_4
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
inst_4 : Finite G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
refine_1 :
  (Set.range fun (gv : G × V) ↦
      HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2) ⊆
    (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
      Set V)
⊢ Coinvariants.ker ρ =
    (HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range
have refine_2 : (HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range ≤
  Coinvariants.ker ρ
Tactic: refine le_antisymm (Submodule.span_le.2 ?_) ?_
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
V : Type u_4
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
inst_4 : Finite G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
γ : G
α : V
⊢ (fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
      (γ, α) ∈
    (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
      Set V)
have refine_1 : ∀ (i : ℕ),
  (fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
      ((fun (x : ℕ) ↦ g ^ x) i, α) ∈
    (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
      Set V)
Tactic: rcases mem_powers_iff_mem_zpowers.2 (hg γ) with ⟨i, rfl⟩
Cleared hypotheses: γ
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
V : Type u_4
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
inst_4 : Finite G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
α : V
n : ℕ
h :
  (fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
      ((fun (x : ℕ) ↦ g ^ x) n, α) ∈
    (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
      Set V)
⊢ (fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
      ((fun (x : ℕ) ↦ g ^ x) (n + 1), α) ∈
    (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
      Set V)
have h : Eq (α := V)
  ((HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id : (a : V) → V)
      (Fin.partialSum (n := n + 1)
        (fun (j : Fin (n + 1)) ↦ (((ρ : (a : G) → V →ₗ[k] V) (g ^ (↑j : ℕ)) : V →ₗ[k] V) : (a : V) → V) α)
        (Fin.last (n + 1))) :
    V)
  ((fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
      ((fun (x : ℕ) ↦ g ^ x) (n + 1), α) :
    V)
Tactic: use (Fin.partialSum (fun (j : Fin (n + 1)) => ρ (g ^ (j : ℕ)) α) (Fin.last _))
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
V : Type u_4
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
inst_4 : Finite G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
α : V
i : ℕ
⊢ (fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
      ((fun (x : ℕ) ↦ g ^ x) i, α) ∈
    (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
      Set V)
have refine_1 : (fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
    ((fun (x : ℕ) ↦ g ^ x) 0, α) ∈
  (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range : Set V)
Tactic: induction i with | zero => exact ⟨0, by simp⟩ | succ n _ =>
    use (Fin.partialSum (fun (j : Fin (n + 1)) => ρ (g ^ (j : ℕ)) α) (Fin.last _))
    simpa using ρ.apply_sub_id_partialSum_eq _ _ _
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
V : Type u_4
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g : G
inst_4 : Finite G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
α : V
i : ℕ
refine_1 :
  (fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
      ((fun (x : ℕ) ↦ g ^ x) 0, α) ∈
    (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
      Set V)
⊢ (fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
      ((fun (x : ℕ) ↦ g ^ x) i, α) ∈
    (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
      Set V)
have refine_1₁ : ∀ (n : ℕ),
  (fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
        ((fun (x : ℕ) ↦ g ^ x) n, α) ∈
      (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
        Set V) →
    (fun (gv : G × V) ↦ HSub.hSub (α := V) ((((ρ : (a : G) → V →ₗ[k] V) gv.1 : V →ₗ[k] V) : (a : V) → V) gv.2 : V) gv.2)
        ((fun (x : ℕ) ↦ g ^ x) (n + 1), α) ∈
      (↑(HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range :
        Set V)
Tactic: induction i with | zero => exact ⟨0, by simp⟩ | succ n _ =>
    use (Fin.partialSum (fun (j : Fin (n + 1)) => ρ (g ^ (j : ℕ)) α) (Fin.last _))
    simpa using ρ.apply_sub_id_partialSum_eq _ _ _
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
⊢ Eq (α := Submodule k (G →₀ k))
    (Coinvariants.ker (k := k) (G := G) (V := G →₀ k) (leftRegular k G) : Submodule k (G →₀ k))
    (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1) : Submodule k (G →₀ k))
have have : ∀ (this : Fintype G),
  Eq (α := Submodule k (G →₀ k))
    (Coinvariants.ker (k := k) (G := G) (V := G →₀ k) (leftRegular k G) : Submodule k (G →₀ k))
    (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1) : Submodule k (G →₀ k))
Tactic: have := Fintype.ofFinite G
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
this : Fintype G
⊢ Eq (α := Submodule k (G →₀ k))
    (Coinvariants.ker (k := k) (G := G) (V := G →₀ k) (leftRegular k G) : Submodule k (G →₀ k))
    (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1) : Submodule k (G →₀ k))
have refine_1 : (Set.range fun (gv : G × (G →₀ k)) ↦
    HSub.hSub (α := G →₀ k)
      ((((leftRegular k G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) gv.1 : (G →₀ k) →ₗ[k] G →₀ k) : (a : G →₀ k) → G →₀ k)
          gv.2 :
        G →₀ k)
      gv.2) ⊆
  (↑(LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) : Set (G →₀ k))
Tactic: refine le_antisymm (Submodule.span_le.2 ?_) fun x hx => ?_
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
this : Fintype G
refine_1 :
  (Set.range fun (gv : G × (G →₀ k)) ↦
      HSub.hSub (α := G →₀ k)
        ((((leftRegular k G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) gv.1 : (G →₀ k) →ₗ[k] G →₀ k) : (a : G →₀ k) → G →₀ k)
            gv.2 :
          G →₀ k)
        gv.2) ⊆
    (↑(LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) : Set (G →₀ k))
⊢ Eq (α := Submodule k (G →₀ k))
    (Coinvariants.ker (k := k) (G := G) (V := G →₀ k) (leftRegular k G) : Submodule k (G →₀ k))
    (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1) : Submodule k (G →₀ k))
have refine_2 : ∀ (x : G →₀ k)
  (hx : Membership.mem (γ := Submodule k (G →₀ k)) (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) x),
  Membership.mem (γ := Submodule k (G →₀ k))
    (Coinvariants.ker (k := k) (G := G) (V := G →₀ k) (leftRegular k G) : Submodule k (G →₀ k)) x
Tactic: refine le_antisymm (Submodule.span_le.2 ?_) fun x hx => ?_
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
this : Fintype G
x : G →₀ k
hx : Membership.mem (γ := Submodule k (G →₀ k)) (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) x
⊢ x = x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r)
have h : ∀ (g : G),
  Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) g : k)
    ((x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r) : (a : G) → k) g : k)
Tactic: ext g
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
this : Fintype G
x : G →₀ k
hx : Membership.mem (γ := Submodule k (G →₀ k)) (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) x
g : G
⊢ Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) g : k)
    ((x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r) : (a : G) → k) g : k)
have pos : ∀ (hg : g = 1),
  Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) g : k)
    ((x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r) : (a : G) → k) g : k)
Tactic: by_cases hg : g = 1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
this : Fintype G
x : G →₀ k
hx : Membership.mem (γ := Submodule k (G →₀ k)) (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) x
g : G
pos :
  ∀ (hg : g = 1),
    Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) g : k)
      ((x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r) : (a : G) → k) g : k)
⊢ Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) g : k)
    ((x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r) : (a : G) → k) g : k)
have neg : ∀ (hg : ¬g = 1),
  Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) g : k)
    ((x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r) : (a : G) → k) g : k)
Tactic: by_cases hg : g = 1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (hypothesis)
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
this : Fintype G
x : G →₀ k
hx : Membership.mem (γ := Submodule k (G →₀ k)) (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) x
⊢ Membership.mem (γ := Submodule k (G →₀ k))
    (Coinvariants.ker (k := k) (G := G) (V := G →₀ k) (leftRegular k G) : Submodule k (G →₀ k)) x
have this₁ : x = x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r)
Tactic: have : x = x.sum (fun g r => single g r - single 1 r) := by
      ext g
      by_cases hg : g = 1
      · simp_all [linearCombination, sum_apply']
      · simp_all [sum_apply']
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
this_1 : Fintype G
x : G →₀ k
hx : Membership.mem (γ := Submodule k (G →₀ k)) (LinearMap.ker (M₂ := k) (linearCombination k fun (x : G) ↦ 1)) x
this : x = x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r)
⊢ Membership.mem (γ := Submodule k (G →₀ k))
    (Coinvariants.ker (k := k) (G := G) (V := G →₀ k) (leftRegular k G) : Submodule k (G →₀ k)) x
have refine_2 : Membership.mem (γ := Submodule k (G →₀ k))
  (Coinvariants.ker (k := k) (G := G) (V := G →₀ k) (leftRegular k G) : Submodule k (G →₀ k))
  (x.sum fun (g : G) (r : k) ↦ HSub.hSub (α := G →₀ k) (single g r) (single 1 r))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x : (↑(leftRegular k G) : Type u)
hx :
  x ∈
    (Hom.hom
        (HSub.hSub (α := Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G)) (β :=
          Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G))
          (applyAsHom (leftRegular k G) g : Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G))
          (𝟙 (leftRegular k G)))).ker
⊢ (IntertwiningMap.toLinearMap (Hom.hom (norm (leftRegular k G))) :
        (a : (↑(leftRegular k G) : Type u)) → (↑(leftRegular k G) : Type u))
      (single 1 ((x : (a : G) → k) g)) =
    x
have h : ∀ (a : G),
  Eq (α := k)
    ((((IntertwiningMap.toLinearMap (Hom.hom (norm (leftRegular k G))) :
                (a : (↑(leftRegular k G) : Type u)) → (↑(leftRegular k G) : Type u))
              (single 1 ((x : (a : G) → k) g)) :
            (↑(leftRegular k G) : Type u)) :
          (a : G) → k)
        a :
      k)
    ((x : (a : G) → k) a : k)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x : (↑(leftRegular k G) : Type u)
hx :
  x ∈
    (Hom.hom
        (HSub.hSub (α := Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G)) (β :=
          Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G))
          (applyAsHom (leftRegular k G) g : Quiver.Hom (V := Rep k G) (leftRegular k G) (leftRegular k G))
          (𝟙 (leftRegular k G)))).ker
a : G
⊢ Eq (α := k)
    ((((IntertwiningMap.toLinearMap (Hom.hom (norm (leftRegular k G))) :
                (a : (↑(leftRegular k G) : Type u)) → (↑(leftRegular k G) : Type u))
              (single 1 ((x : (a : G) → k) g)) :
            (↑(leftRegular k G) : Type u)) :
          (a : G) → k)
        a :
      k)
    ((x : (a : G) → k) a : k)
have this : ∀ (γ : G), Eq (α := k) ((x : (a : G) → k) γ : k) ((x : (a : G) → k) g : k)
Tactic: have := apply_eq_of_leftRegular_eq_of_generator (k := k) g hg x
      (by simpa [sub_hom, sub_eq_zero] using hx)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A_1 : Rep k G
g : G
A : Rep.{u_1, u, u} k G
⊢ A.norm ≫ HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A) (𝟙 A) = 0
have hf : ∀ (x : (↑A : Type u_1)),
  Eq (α := (↑A : Type u_1))
    (((Hom.hom
              (A.norm ≫
                HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A) (𝟙 A))).toLinearMap :
          (a : (↑A : Type u_1)) → (↑A : Type u_1))
        x :
      (↑A : Type u_1))
    ((Representation.IntertwiningMap.toLinearMap (Hom.hom 0) : (a : (↑A : Type u_1)) → (↑A : Type u_1)) x :
      (↑A : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A_1 : Rep k G
g : G
A : Rep.{u_1, u, u} k G
⊢ HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A) (𝟙 A) ≫ A.norm = 0
have hf : ∀ (x : (↑A : Type u_1)),
  Eq (α := (↑A : Type u_1))
    (((Hom.hom
              (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A) (𝟙 A) ≫
                A.norm)).toLinearMap :
          (a : (↑A : Type u_1)) → (↑A : Type u_1))
        x :
      (↑A : Type u_1))
    ((Representation.IntertwiningMap.toLinearMap (Hom.hom 0) : (a : (↑A : Type u_1)) → (↑A : Type u_1)) x :
      (↑A : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
X Y : Rep.{u_1, u, u} k G
f : X ⟶ Y
j : ℕ
⊢ Eq (α :=
    HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X (φ := X.norm) ⋯ ⋯ ⋯)
        (j + 1) ⟶
      HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y (φ := Y.norm) ⋯ ⋯ ⋯) j)
    (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y (φ := Y.norm) ⋯ ⋯ ⋯) (j + 1) j)
    (HomologicalComplex.d (HomologicalComplex.alternatingConst X (φ := X.norm) ⋯ ⋯ ⋯) (j + 1) j ≫ f)
have pos : ∀ (hj : Even (j + 1)),
  Eq (α :=
    HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X (φ := X.norm) sorry sorry sorry)
        (j + 1) ⟶
      HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y (φ := Y.norm) sorry sorry sorry) j)
    (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y (φ := Y.norm) sorry sorry sorry) (j + 1) j)
    (HomologicalComplex.d (HomologicalComplex.alternatingConst X (φ := X.norm) sorry sorry sorry) (j + 1) j ≫ f)
Tactic: by_cases hj : Even (j + 1)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
X Y : Rep.{u_1, u, u} k G
f : X ⟶ Y
j : ℕ
pos :
  ∀ (hj : Even (j + 1)),
    Eq (α :=
      HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X (φ := X.norm) ⋯ ⋯ ⋯)
          (j + 1) ⟶
        HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y (φ := Y.norm) ⋯ ⋯ ⋯) j)
      (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y (φ := Y.norm) ⋯ ⋯ ⋯) (j + 1) j)
      (HomologicalComplex.d (HomologicalComplex.alternatingConst X (φ := X.norm) ⋯ ⋯ ⋯) (j + 1) j ≫ f)
⊢ Eq (α :=
    HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X (φ := X.norm) ⋯ ⋯ ⋯)
        (j + 1) ⟶
      HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y (φ := Y.norm) ⋯ ⋯ ⋯) j)
    (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y (φ := Y.norm) ⋯ ⋯ ⋯) (j + 1) j)
    (HomologicalComplex.d (HomologicalComplex.alternatingConst X (φ := X.norm) ⋯ ⋯ ⋯) (j + 1) j ≫ f)
have neg : ∀ (hj : ¬Even (j + 1)),
  Eq (α :=
    HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X (φ := X.norm) sorry sorry sorry)
        (j + 1) ⟶
      HomologicalComplex.X (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y (φ := Y.norm) sorry sorry sorry) j)
    (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y (φ := Y.norm) sorry sorry sorry) (j + 1) j)
    (HomologicalComplex.d (HomologicalComplex.alternatingConst X (φ := X.norm) sorry sorry sorry) (j + 1) j ≫ f)
Tactic: by_cases hj : Even (j + 1)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep.{u_1, u, u} k G
g : G
⊢ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫
      ModuleCat.ofHom
        (Hom.hom
            (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A) (𝟙 A))).toLinearMap =
    0
have hf : ∀ (x : (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1)),
  Eq (α := (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫
              ModuleCat.ofHom
                (Hom.hom
                    (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A)
                      (𝟙 A))).toLinearMap) :
          (a : (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1)) → (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
        x :
      (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1)) → (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
        x :
      (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep.{u_1, u, u} k G
g : G
⊢ ModuleCat.ofHom
        (Hom.hom
            (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A) (𝟙 A))).toLinearMap ≫
      ModuleCat.ofHom (Hom.hom A.norm).toLinearMap =
    0
have hf : ∀ (x : (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1)),
  Eq (α := (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom
                (Hom.hom
                    (HSub.hSub (α := A ⟶ A) (β := A ⟶ A) (applyAsHom.{u, u, u_1} (k := k) A g : A ⟶ A)
                      (𝟙 A))).toLinearMap ≫
              ModuleCat.ofHom (Hom.hom A.norm).toLinearMap) :
          (a : (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1)) → (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
        x :
      (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1)) → (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
        x :
      (↑(ModuleCat.of k (↑A : Type u_1)) : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
m : ℕ
h : QuasiIsoAt (C := Rep k G) (K := Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (resolution.π k g) m
⊢ QuasiIsoAt (C := Rep k G) (K := Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (resolution.π k g) (m + 1)
have succ : ShortComplex.Exact (C := Rep k G)
  (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
Tactic: rw [quasiIsoAt_iff_exactAt' (hL := ChainComplex.exactAt_succ_single_obj ..),
          HomologicalComplex.exactAt_iff' _ (m + 2) (m + 1) m (by simp) (by simp)]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
m : ℕ
h : QuasiIsoAt (C := Rep k G) (K := Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (resolution.π k g) m
⊢ ShortComplex.Exact (C := Rep k G)
    (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
have succ : ShortComplex.Exact
  (ShortComplex.map (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
    (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
      fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier)))
Tactic: apply (forget₂ _ (ModuleCat k)).reflects_exact_of_faithful