awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ g₂ : G
a : (↑A : Type w)
s : ↥S
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux ((↑s : G) * g₁) : (a : (↑A : Type w)) → G → (↑A : Type w))
        ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
              (a : (↑A : Type w)) → (↑A : Type w))
            a :
          (↑A : Type w))
        g₂ :
      (↑A : Type w))
    ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₂ : (↑A : Type w))
have inl : ∀ (s₁ : ↥S),
  Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux ((↑s : G) * g₁) : (a : (↑A : Type w)) → G → (↑A : Type w))
        ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
              (a : (↑A : Type w)) → (↑A : Type w))
            a :
          (↑A : Type w))
        ((fun (m : ↥S) ↦ m • g₁) s₁) :
      (↑A : Type w))
    ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((fun (m : ↥S) ↦ m • g₁) s₁) : (↑A : Type w))
Tactic: rcases em ((QuotientGroup.rightRel S).r g₂ g₁) with ⟨s₁, rfl⟩ | h
Cleared hypotheses: g₂
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ g₂ : G
a : (↑A : Type w)
s : ↥S
inl :
  ∀ (s₁ : ↥S),
    Eq.{w + 1} (α := (↑A : Type w))
      ((A.indToCoindAux ((↑s : G) * g₁) : (a : (↑A : Type w)) → G → (↑A : Type w))
          ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
                (a : (↑A : Type w)) → (↑A : Type w))
              a :
            (↑A : Type w))
          ((fun (m : ↥S) ↦ m • g₁) s₁) :
        (↑A : Type w))
      ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((fun (m : ↥S) ↦ m • g₁) s₁) : (↑A : Type w))
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux ((↑s : G) * g₁) : (a : (↑A : Type w)) → G → (↑A : Type w))
        ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
              (a : (↑A : Type w)) → (↑A : Type w))
            a :
          (↑A : Type w))
        g₂ :
      (↑A : Type w))
    ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₂ : (↑A : Type w))
have inr : ∀ (h : ¬(QuotientGroup.rightRel S : G → G → Prop) g₂ g₁),
  Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux ((↑s : G) * g₁) : (a : (↑A : Type w)) → G → (↑A : Type w))
        ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
              (a : (↑A : Type w)) → (↑A : Type w))
            a :
          (↑A : Type w))
        g₂ :
      (↑A : Type w))
    ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₂ : (↑A : Type w))
Tactic: rcases em ((QuotientGroup.rightRel S).r g₂ g₁) with ⟨s₁, rfl⟩ | h
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ : G
a : (↑A : Type w)
s s₁ : ↥S
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux ((↑s : G) * g₁) : (a : (↑A : Type w)) → G → (↑A : Type w))
        ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
              (a : (↑A : Type w)) → (↑A : Type w))
            a :
          (↑A : Type w))
        ((fun (m : ↥S) ↦ m • g₁) s₁) :
      (↑A : Type w))
    ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((fun (m : ↥S) ↦ m • g₁) s₁) : (↑A : Type w))
have inl : Eq (α := (↑A : Type w))
  ((if h : (QuotientGroup.rightRel S : G → G → Prop) (s₁ • g₁) ((↑s : G) * g₁) then
          (A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
            (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * ((↑s : G) * g₁)⁻¹) sorry)
        else 0 :
        (a : (↑A : Type w)) → (↑A : Type w))
      ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
            (a : (↑A : Type w)) → (↑A : Type w))
          a :
        (↑A : Type w)) :
    (↑A : Type w))
  ((if h : (QuotientGroup.rightRel S : G → G → Prop) (s₁ • g₁) g₁ then
          (A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
            (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * g₁⁻¹) sorry)
        else 0 :
        (a : (↑A : Type w)) → (↑A : Type w))
      a :
    (↑A : Type w))
Tactic: simp only [indToCoindAux, LinearMap.pi_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ : G
a : (↑A : Type w)
s s₁ : ↥S
⊢ Eq (α := (↑A : Type w))
    ((if h : (QuotientGroup.rightRel S : G → G → Prop) (s₁ • g₁) ((↑s : G) * g₁) then
            (A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * ((↑s : G) * g₁)⁻¹) ⋯)
          else 0 :
          (a : (↑A : Type w)) → (↑A : Type w))
        ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
              (a : (↑A : Type w)) → (↑A : Type w))
            a :
          (↑A : Type w)) :
      (↑A : Type w))
    ((if h : (QuotientGroup.rightRel S : G → G → Prop) (s₁ • g₁) g₁ then
            (A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * g₁⁻¹) ⋯)
          else 0 :
          (a : (↑A : Type w)) → (↑A : Type w))
        a :
      (↑A : Type w))
have inl : Eq (α := (↑A : Type w))
  ((((A.ρ : (a : ↥S) → Module.End k (↑A : Type w))
            (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * ((↑s : G) * g₁)⁻¹) sorry * s) :
          Module.End k (↑A : Type w)) :
        (a : (↑A : Type w)) → (↑A : Type w))
      a :
    (↑A : Type w))
  ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * g₁⁻¹) sorry) :
          (↑A : Type w) →ₗ[k] (↑A : Type w)) :
        (a : (↑A : Type w)) → (↑A : Type w))
      a :
    (↑A : Type w))
Tactic: rw [dif_pos ⟨s₁ * s⁻¹, by simp [S.1.smul_def, smul_eq_mul, mul_assoc]⟩, dif_pos ⟨s₁, rfl⟩,
      ← Module.End.mul_apply, ← map_mul]
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ : G
a : (↑A : Type w)
s s₁ : ↥S
⊢ Eq (α := (↑A : Type w))
    ((((A.ρ : (a : ↥S) → Module.End k (↑A : Type w))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * ((↑s : G) * g₁)⁻¹) ⋯ * s) :
            Module.End k (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        a :
      (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * g₁⁻¹) ⋯) :
            (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        a :
      (↑A : Type w))
have inl : Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * ((↑s : G) * g₁)⁻¹) sorry * s =
  Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * g₁⁻¹) sorry
Tactic: congr
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ g₂ : G
a : (↑A : Type w)
s : ↥S
h : ¬(QuotientGroup.rightRel S : G → G → Prop) g₂ g₁
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux ((↑s : G) * g₁) : (a : (↑A : Type w)) → G → (↑A : Type w))
        ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
              (a : (↑A : Type w)) → (↑A : Type w))
            a :
          (↑A : Type w))
        g₂ :
      (↑A : Type w))
    ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₂ : (↑A : Type w))
have inr : ¬(QuotientGroup.rightRel S : G → G → Prop) g₂ ((↑s : G) * g₁)
Tactic: rw [indToCoindAux_of_not_rel (h := h), indToCoindAux_of_not_rel]
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ g₂ g₃ : G
a : (↑A : Type w)
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a (g₂ * g₃⁻¹) : (↑A : Type w))
    ((A.indToCoindAux (g₁ * g₃) : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₂ : (↑A : Type w))
have inl : ∀ (s : ↥S) (hs : (fun (m : ↥S) ↦ m • g₁) s = g₂ * g₃⁻¹),
  Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a (g₂ * g₃⁻¹) : (↑A : Type w))
    ((A.indToCoindAux (g₁ * g₃) : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₂ : (↑A : Type w))
Tactic: rcases em ((QuotientGroup.rightRel S).r (g₂ * g₃⁻¹) g₁) with ⟨s, hs⟩ | h
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ g₂ g₃ : G
a : (↑A : Type w)
inl :
  ∀ (s : ↥S) (hs : (fun (m : ↥S) ↦ m • g₁) s = g₂ * g₃⁻¹),
    Eq.{w + 1} (α := (↑A : Type w))
      ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a (g₂ * g₃⁻¹) : (↑A : Type w))
      ((A.indToCoindAux (g₁ * g₃) : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₂ : (↑A : Type w))
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a (g₂ * g₃⁻¹) : (↑A : Type w))
    ((A.indToCoindAux (g₁ * g₃) : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₂ : (↑A : Type w))
have inr : ∀ (h : ¬(QuotientGroup.rightRel S : G → G → Prop) (g₂ * g₃⁻¹) g₁),
  Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a (g₂ * g₃⁻¹) : (↑A : Type w))
    ((A.indToCoindAux (g₁ * g₃) : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₂ : (↑A : Type w))
Tactic: rcases em ((QuotientGroup.rightRel S).r (g₂ * g₃⁻¹) g₁) with ⟨s, hs⟩ | h
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ g₂ g₃ : G
a : (↑A : Type w)
h : ¬(QuotientGroup.rightRel S : G → G → Prop) (g₂ * g₃⁻¹) g₁
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a (g₂ * g₃⁻¹) : (↑A : Type w))
    ((A.indToCoindAux (g₁ * g₃) : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₂ : (↑A : Type w))
have inr : ¬(QuotientGroup.rightRel S : G → G → Prop) g₂ (g₁ * g₃)
Tactic: rw [indToCoindAux_of_not_rel (h := h), indToCoindAux_of_not_rel]
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A B : Rep.{u_1, u, v} k ↥S
f : A ⟶ B
g₁ g₂ : G
a : (↑A : Type u_1)
⊢ Eq.{u_1 + 1} (α := (↑B : Type u_1))
    ((B.indToCoindAux g₁ : (a : (↑B : Type u_1)) → G → (↑B : Type u_1))
        ((Hom.hom f : (a : (↑A : Type u_1)) → (↑B : Type u_1)) a : (↑B : Type u_1)) g₂ :
      (↑B : Type u_1))
    ((Hom.hom f : (a : (↑A : Type u_1)) → (↑B : Type u_1))
        ((A.indToCoindAux g₁ : (a : (↑A : Type u_1)) → G → (↑A : Type u_1)) a g₂ : (↑A : Type u_1)) :
      (↑B : Type u_1))
have inl : ∀ (s : ↥S),
  Eq.{u_1 + 1} (α := (↑B : Type u_1))
    ((B.indToCoindAux g₁ : (a : (↑B : Type u_1)) → G → (↑B : Type u_1))
        ((Hom.hom f : (a : (↑A : Type u_1)) → (↑B : Type u_1)) a : (↑B : Type u_1)) ((fun (m : ↥S) ↦ m • g₁) s) :
      (↑B : Type u_1))
    ((Hom.hom f : (a : (↑A : Type u_1)) → (↑B : Type u_1))
        ((A.indToCoindAux g₁ : (a : (↑A : Type u_1)) → G → (↑A : Type u_1)) a ((fun (m : ↥S) ↦ m • g₁) s) :
          (↑A : Type u_1)) :
      (↑B : Type u_1))
Tactic: rcases em ((QuotientGroup.rightRel S).r g₂ g₁) with ⟨s, rfl⟩ | h
Cleared hypotheses: g₂
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A B : Rep.{u_1, u, v} k ↥S
f : A ⟶ B
g₁ g₂ : G
a : (↑A : Type u_1)
inl :
  ∀ (s : ↥S),
    Eq.{u_1 + 1} (α := (↑B : Type u_1))
      ((B.indToCoindAux g₁ : (a : (↑B : Type u_1)) → G → (↑B : Type u_1))
          ((Hom.hom f : (a : (↑A : Type u_1)) → (↑B : Type u_1)) a : (↑B : Type u_1)) ((fun (m : ↥S) ↦ m • g₁) s) :
        (↑B : Type u_1))
      ((Hom.hom f : (a : (↑A : Type u_1)) → (↑B : Type u_1))
          ((A.indToCoindAux g₁ : (a : (↑A : Type u_1)) → G → (↑A : Type u_1)) a ((fun (m : ↥S) ↦ m • g₁) s) :
            (↑A : Type u_1)) :
        (↑B : Type u_1))
⊢ Eq.{u_1 + 1} (α := (↑B : Type u_1))
    ((B.indToCoindAux g₁ : (a : (↑B : Type u_1)) → G → (↑B : Type u_1))
        ((Hom.hom f : (a : (↑A : Type u_1)) → (↑B : Type u_1)) a : (↑B : Type u_1)) g₂ :
      (↑B : Type u_1))
    ((Hom.hom f : (a : (↑A : Type u_1)) → (↑B : Type u_1))
        ((A.indToCoindAux g₁ : (a : (↑A : Type u_1)) → G → (↑A : Type u_1)) a g₂ : (↑A : Type u_1)) :
      (↑B : Type u_1))
have inr : ∀ (h : ¬(QuotientGroup.rightRel S : G → G → Prop) g₂ g₁),
  Eq.{u_1 + 1} (α := (↑B : Type u_1))
    ((B.indToCoindAux g₁ : (a : (↑B : Type u_1)) → G → (↑B : Type u_1))
        ((Hom.hom f : (a : (↑A : Type u_1)) → (↑B : Type u_1)) a : (↑B : Type u_1)) g₂ :
      (↑B : Type u_1))
    ((Hom.hom f : (a : (↑A : Type u_1)) → (↑B : Type u_1))
        ((A.indToCoindAux g₁ : (a : (↑A : Type u_1)) → G → (↑A : Type u_1)) a g₂ : (↑A : Type u_1)) :
      (↑B : Type u_1))
Tactic: rcases em ((QuotientGroup.rightRel S).r g₂ g₁) with ⟨s, rfl⟩ | h
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
x : ↥S
⊢ Eq (α := (G →₀ k) ⊗[k] (↑A : Type w) →ₗ[k] (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w)))
    (TensorProduct.lift
        (linearCombination k fun (g : G) ↦ LinearMap.codRestrict (coindV S.subtype A.ρ) (A.indToCoindAux g) ⋯) ∘ₗ
      (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ :
          (a : ↥S) → (G →₀ k) ⊗[k] (↑A : Type w) →ₗ[k] (G →₀ k) ⊗[k] (↑A : Type w))
        x)
    (TensorProduct.lift
      (linearCombination k fun (g : G) ↦ LinearMap.codRestrict (coindV S.subtype A.ρ) (A.indToCoindAux g) ⋯))
have a : ∀ (a : G) (x_1 : (↑A : Type w)) (x_2 : G),
  Eq.{w + 1} (α := (↑A : Type w))
    ((↑((((AlgebraTensorModule.curry
                        (TensorProduct.lift
                            (linearCombination k fun (g : G) ↦
                              LinearMap.codRestrict (coindV S.subtype A.ρ) (A.indToCoindAux g) sorry) ∘ₗ
                          (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ :
                              (a : ↥S) → (G →₀ k) ⊗[k] (↑A : Type w) →ₗ[k] (G →₀ k) ⊗[k] (↑A : Type w))
                            x) ∘ₗ
                      lsingle a :
                    k →ₗ[k] (↑A : Type w) →ₗ[k] (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))) :
                  (a : k) → (↑A : Type w) →ₗ[k] (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w)))
                1 :
              (a : (↑A : Type w)) → (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w)))
            x_1) :
        G → (↑A : Type w))
      x_2)
    ((↑((((AlgebraTensorModule.curry
                        (TensorProduct.lift
                          (linearCombination k fun (g : G) ↦
                            LinearMap.codRestrict (coindV S.subtype A.ρ) (A.indToCoindAux g) sorry)) ∘ₗ
                      lsingle a :
                    k →ₗ[k] (↑A : Type w) →ₗ[k] (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))) :
                  (a : k) → (↑A : Type w) →ₗ[k] (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w)))
                1 :
              (a : (↑A : Type w)) → (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w)))
            x_1) :
        G → (↑A : Type w))
      x_2)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (hypothesis)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
inst_3 : S.FiniteIndex
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
g : Quotient (QuotientGroup.rightRel S)
g₁ g₂ : G
h : g₁ ≈ g₂
s : ↥S
hs : (↑s : G) * g₂ = g₁
⊢ HSub.hSub (α := (G →₀ k) ⊗[k] (↑A : Type w)) (β := (G →₀ k) ⊗[k] (↑A : Type w))
      ((((tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ :
                  (a : ↥S) → (G →₀ k) ⊗[k] (↑A : Type w) →ₗ[k] (G →₀ k) ⊗[k] (↑A : Type w))
                s :
              (G →₀ k) ⊗[k] (↑A : Type w) →ₗ[k] (G →₀ k) ⊗[k] (↑A : Type w)) :
            (a : (G →₀ k) ⊗[k] (↑A : Type w)) → (G →₀ k) ⊗[k] (↑A : Type w))
          (single g₂ 1 ⊗ₜ[k] (↑f : G → (↑A : Type w)) g₂) :
        (G →₀ k) ⊗[k] (↑A : Type w))
      (single g₂ 1 ⊗ₜ[k] (↑f : G → (↑A : Type w)) g₂ : (G →₀ k) ⊗[k] (↑A : Type w)) =
    HSub.hSub (α := (G →₀ k) ⊗[k] (↑A : Type w)) (β := (G →₀ k) ⊗[k] (↑A : Type w))
      ((((TensorProduct.mk k (G →₀ k) (↑A : Type w) : (a : G →₀ k) → (↑A : Type w) →ₗ[k] (G →₀ k) ⊗[k] (↑A : Type w))
                (single g₁ 1) :
              (↑A : Type w) →ₗ[k] (G →₀ k) ⊗[k] (↑A : Type w)) :
            (a : (↑A : Type w)) → (G →₀ k) ⊗[k] (↑A : Type w))
          ((↑f : G → (↑A : Type w)) g₁) :
        (G →₀ k) ⊗[k] (↑A : Type w))
      ((((TensorProduct.mk k (G →₀ k) (↑A : Type w) : (a : G →₀ k) → (↑A : Type w) →ₗ[k] (G →₀ k) ⊗[k] (↑A : Type w))
                (single g₂ 1) :
              (↑A : Type w) →ₗ[k] (G →₀ k) ⊗[k] (↑A : Type w)) :
            (a : (↑A : Type w)) → (G →₀ k) ⊗[k] (↑A : Type w))
          ((↑f : G → (↑A : Type w)) g₂) :
        (G →₀ k) ⊗[k] (↑A : Type w))
have this : (↑f : G → (↑A : Type w)) (HMul.hMul (α := G) ((S.subtype : (a : ↥S) → G) s : G) g₂) =
  (((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
      (a : (↑A : Type w)) → (↑A : Type w))
    ((↑f : G → (↑A : Type w)) g₂)
Tactic: have := f.2 s g₂
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst_2 : S.FiniteIndex
g : G
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
hx : Function.support (↑f : G → (↑A : Type w)) ⊆ MulAction.orbit (↥S) g
⊢ Eq (α := (↑(ind S.subtype A) : Type (max (max u v) w)))
    ((A.coindToInd :
          (a : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))) → (↑(ind S.subtype A) : Type (max (max u v) w)))
        f :
      (↑(ind S.subtype A) : Type (max (max u v) w)))
    ((IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g) :
      IndV S.subtype A.ρ)
have rw : ⟦g⟧.liftOn
    (fun (g : G) ↦ (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g))
    sorry =
  (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g)
Tactic: rw [coindToInd_apply, Finset.sum_eq_single ⟦g⟧]
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst_2 : S.FiniteIndex
g : G
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
hx : Function.support (↑f : G → (↑A : Type w)) ⊆ MulAction.orbit (↥S) g
rw :
  ⟦g⟧.liftOn
      (fun (g : G) ↦ (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g))
      ⋯ =
    (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g)
⊢ Eq (α := (↑(ind S.subtype A) : Type (max (max u v) w)))
    ((A.coindToInd :
          (a : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))) → (↑(ind S.subtype A) : Type (max (max u v) w)))
        f :
      (↑(ind S.subtype A) : Type (max (max u v) w)))
    ((IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g) :
      IndV S.subtype A.ρ)
have h₀ : ∀ (b : Quotient (QuotientGroup.rightRel S)),
  Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ b →
    b ≠ ⟦g⟧ →
      b.liftOn
          (fun (g : G) ↦
            (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g))
          sorry =
        0
Tactic: rw [coindToInd_apply, Finset.sum_eq_single ⟦g⟧]
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst_2 : S.FiniteIndex
g : G
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
hx : Function.support (↑f : G → (↑A : Type w)) ⊆ MulAction.orbit (↥S) g
rw :
  ⟦g⟧.liftOn
      (fun (g : G) ↦ (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g))
      ⋯ =
    (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g)
h₀ :
  ∀ (b : Quotient (QuotientGroup.rightRel S)),
    Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ b →
      b ≠ ⟦g⟧ →
        b.liftOn
            (fun (g : G) ↦
              (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g))
            ⋯ =
          0
⊢ Eq (α := (↑(ind S.subtype A) : Type (max (max u v) w)))
    ((A.coindToInd :
          (a : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))) → (↑(ind S.subtype A) : Type (max (max u v) w)))
        f :
      (↑(ind S.subtype A) : Type (max (max u v) w)))
    ((IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g) :
      IndV S.subtype A.ρ)
have h₁ : ⟦g⟧ ∉ Finset.univ →
  ⟦g⟧.liftOn
      (fun (g : G) ↦ (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g))
      sorry =
    0
Tactic: rw [coindToInd_apply, Finset.sum_eq_single ⟦g⟧]
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (hypothesis)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst_2 : S.FiniteIndex
g : G
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
hx : Function.support (↑f : G → (↑A : Type w)) ⊆ MulAction.orbit (↥S) g
b : G
h : Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ ⟦b⟧
hb : ⟦b⟧ ≠ ⟦g⟧
⊢ (↑f : G → (↑A : Type w)) b = 0
have hx₁ : ∀ (x : G), ¬(↑f : G → (↑A : Type w)) x = 0 → x ∈ MulAction.orbit (↥S) g
Tactic: simp_all only [Function.support_subset_iff, ne_eq, Quotient.eq]
Cleared hypotheses: hx, h, hb
-- Lean 4 proof step from Mathlib.RepresentationTheory.FiniteIndex (hypothesis)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst_2 : S.FiniteIndex
g : G
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
hx : Function.support (↑f : G → (↑A : Type w)) ⊆ MulAction.orbit (↥S) g
b : G
h : Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ ⟦b⟧
hb : ⟦b⟧ ≠ ⟦g⟧
hx₁ : ∀ (x : G), ¬(↑f : G → (↑A : Type w)) x = 0 → x ∈ MulAction.orbit (↥S) g
a : Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ ⟦b⟧
⊢ (↑f : G → (↑A : Type w)) b = 0
have hb₁ : ¬(QuotientGroup.rightRel S : G → G → Prop) b g
Tactic: simp_all only [Function.support_subset_iff, ne_eq, Quotient.eq]
Cleared hypotheses: hx, h, hb