awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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
h :
  ∀ (g : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))) (a : G),
    Eq.{w + 1} (α := (↑A : Type w))
      ((↑((A.indToCoind ∘ₗ A.coindToInd :
                (a : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))) →
                  (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w)))
              g) :
          G → (↑A : Type w))
        a)
      ((↑((LinearMap.id :
                (a : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))) →
                  (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w)))
              g) :
          G → (↑A : Type w))
        a)
⊢ A.indToCoind ∘ₗ A.coindToInd = LinearMap.id

Tactic:
ext g a
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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
g : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
a : G
h :
  (↑((A.indToCoind : (a : IndV S.subtype A.ρ) → ↥(coindV S.subtype A.ρ))
            ((A.coindToInd : (a : ↥(coindV S.subtype A.ρ)) → IndV S.subtype A.ρ) g)) :
        G → (↑A : Type w))
      a =
    (↑g : G → (↑A : Type w)) a
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((↑((A.indToCoind ∘ₗ A.coindToInd :
              (a : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))) →
                (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w)))
            g) :
        G → (↑A : Type w))
      a)
    ((↑((LinearMap.id :
              (a : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))) →
                (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w)))
            g) :
        G → (↑A : Type w))
      a)

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.id_coe, id_eq]

Premises used: LinearMap.id_coe, LinearMap.coe_comp, Function.comp_apply, id_eq
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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
g : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
a : G
rw :
  (↑((A.indToCoind : (a : IndV S.subtype A.ρ) → ↥(coindV S.subtype A.ρ))
          (∑ g_1 : Quotient (QuotientGroup.rightRel S),
            g_1.liftOn
              (fun (g_2 : G) ↦
                (IndV.mk S.subtype A.ρ g_2 : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑g : G → (↑A : Type w)) g_2))
              ⋯)) :
      G → (↑A : Type w))
    a
| (↑((A.indToCoind : (a : IndV S.subtype A.ρ) → ↥(coindV S.subtype A.ρ))
          ((A.coindToInd : (a : ↥(coindV S.subtype A.ρ)) → IndV S.subtype A.ρ) g)) :
      G → (↑A : Type w))
    a

Tactic:
rw [coindToInd_apply]

Premises used: Rep.coindToInd_apply
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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
g : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
a : G
h :
  (↑((A.indToCoind : (a : IndV S.subtype A.ρ) → ↥(coindV S.subtype A.ρ))
            (∑ g_1 : Quotient (QuotientGroup.rightRel S),
              g_1.liftOn
                (fun (g_2 : G) ↦
                  (IndV.mk S.subtype A.ρ g_2 : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑g : G → (↑A : Type w)) g_2))
                ⋯)) :
        G → (↑A : Type w))
      a =
    (↑g : G → (↑A : Type w)) a
⊢ (↑((A.indToCoind : (a : IndV S.subtype A.ρ) → ↥(coindV S.subtype A.ρ))
            ((A.coindToInd : (a : ↥(coindV S.subtype A.ρ)) → IndV S.subtype A.ρ) g)) :
        G → (↑A : Type w))
      a =
    (↑g : G → (↑A : Type w)) a

Tactic:
conv_lhs => rw [coindToInd_apply]

Premises used: Rep.coindToInd_apply
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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
g : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
a : G
h :
  ∑ c : Quotient (QuotientGroup.rightRel S),
      (↑((A.indToCoind : (a : IndV S.subtype A.ρ) → ↥(coindV S.subtype A.ρ))
              (c.liftOn
                (fun (g_1 : G) ↦
                  (IndV.mk S.subtype A.ρ g_1 : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑g : G → (↑A : Type w)) g_1))
                ⋯)) :
          G → (↑A : Type w))
        a =
    (↑g : G → (↑A : Type w)) a
⊢ (↑((A.indToCoind : (a : IndV S.subtype A.ρ) → ↥(coindV S.subtype A.ρ))
            (∑ g_1 : Quotient (QuotientGroup.rightRel S),
              g_1.liftOn
                (fun (g_2 : G) ↦
                  (IndV.mk S.subtype A.ρ g_2 : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑g : G → (↑A : Type w)) g_2))
                ⋯)) :
        G → (↑A : Type w))
      a =
    (↑g : G → (↑A : Type w)) a

Tactic:
simp only [map_sum, AddSubmonoidClass.coe_finsetSum, Finset.sum_apply]

Premises used: Finset.sum_apply, AddSubmonoidClass.coe_finsetSum, map_sum
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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
g : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
a : G
h :
  (↑((A.indToCoind : (a : IndV S.subtype A.ρ) → ↥(coindV S.subtype A.ρ))
            (⟦a⟧.liftOn
              (fun (g_1 : G) ↦
                (IndV.mk S.subtype A.ρ g_1 : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑g : G → (↑A : Type w)) g_1))
              ⋯)) :
        G → (↑A : Type w))
      a =
    (↑g : G → (↑A : Type w)) a
h₁ :
  ∀ (b : Quotient (QuotientGroup.rightRel S)),
    Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ b →
      b ≠ ⟦a⟧ →
        Eq.{w + 1} (α := (↑A : Type w))
          ((↑((A.indToCoind : (a : IndV S.subtype A.ρ) → ↥(coindV S.subtype A.ρ))
                  (b.liftOn
                    (fun (g_1 : G) ↦
                      (IndV.mk S.subtype A.ρ g_1 : (a : (↑A : Type w)) → IndV S.subtype A.ρ)
                        ((↑g : G → (↑A : Type w)) g_1))
                    ⋯)) :
              G → (↑A : Type w))
            a)
          0
h₂ :
  ⟦a⟧ ∉ Finset.univ →
    Eq.{w + 1} (α := (↑A : Type w))
      ((↑((A.indToCoind : (a : IndV S.subtype A.ρ) → ↥(coindV S.subtype A.ρ))
              (⟦a⟧.liftOn
                (fun (g_1 : G) ↦
                  (IndV.mk S.subtype A.ρ g_1 : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑g : G → (↑A : Type w)) g_1))
                ⋯)) :
          G → (↑A : Type w))
        a)
      0
⊢ ∑ c : Quotient (QuotientGroup.rightRel S),
      (↑((A.indToCoind : (a : IndV S.subtype A.ρ) → ↥(coindV S.subtype A.ρ))
              (c.liftOn
                (fun (g_1 : G) ↦
                  (IndV.mk S.subtype A.ρ g_1 : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑g : G → (↑A : Type w)) g_1))
                ⋯)) :
          G → (↑A : Type w))
        a =
    (↑g : G → (↑A : Type w)) a

Tactic:
rw [Finset.sum_eq_single ⟦a⟧]

Premises used: Finset.sum_eq_single, Quotient.mk
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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
g : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
a : G
⊢ (↑((A.indToCoind : (a : IndV S.subtype A.ρ) → ↥(coindV S.subtype A.ρ))
            (⟦a⟧.liftOn
              (fun (g_1 : G) ↦
                (IndV.mk S.subtype A.ρ g_1 : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑g : G → (↑A : Type w)) g_1))
              ⋯)) :
        G → (↑A : Type w))
      a =
    (↑g : G → (↑A : Type w)) a

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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
g : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
a : G
b : Quotient (QuotientGroup.rightRel S)
h :
  Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ b →
    b ≠ ⟦a⟧ →
      Eq.{w + 1} (α := (↑A : Type w))
        ((↑((A.indToCoind : (a : IndV S.subtype A.ρ) → ↥(coindV S.subtype A.ρ))
                (b.liftOn
                  (fun (g_1 : G) ↦
                    (IndV.mk S.subtype A.ρ g_1 : (a : (↑A : Type w)) → IndV S.subtype A.ρ)
                      ((↑g : G → (↑A : Type w)) g_1))
                  ⋯)) :
            G → (↑A : Type w))
          a)
        0
⊢ Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ b →
    b ≠ ⟦a⟧ →
      Eq.{w + 1} (α := (↑A : Type w))
        ((↑((A.indToCoind : (a : IndV S.subtype A.ρ) → ↥(coindV S.subtype A.ρ))
                (b.liftOn
                  (fun (g_1 : G) ↦
                    (IndV.mk S.subtype A.ρ g_1 : (a : (↑A : Type w)) → IndV S.subtype A.ρ)
                      ((↑g : G → (↑A : Type w)) g_1))
                  ⋯)) :
            G → (↑A : Type w))
          a)
        0

Tactic:
_
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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
g : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
a b : G
h : Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ ⟦b⟧
hb : ⟦b⟧ ≠ ⟦a⟧
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((↑((A.indToCoind : (a : IndV S.subtype A.ρ) → ↥(coindV S.subtype A.ρ))
            (⟦b⟧.liftOn
              (fun (g_1 : G) ↦
                (IndV.mk S.subtype A.ρ g_1 : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑g : G → (↑A : Type w)) g_1))
              ⋯)) :
        G → (↑A : Type w))
      a)
    0

Tactic:
simpa using indToCoindAux_of_not_rel b a (g.1 b) (mt Quotient.sound hb.symm)

Premises used: mt, Ne.symm, Quotient.sound, Rep.indToCoindAux_of_not_rel, Subtype.val
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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
g : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
a : G
b : Quotient (QuotientGroup.rightRel S)
h_1 : Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ b
hb : b ≠ ⟦a⟧
h :
  ∀ (b : G),
    Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ ⟦b⟧ →
      ∀ (hb : ⟦b⟧ ≠ ⟦a⟧),
        Eq.{w + 1} (α := (↑A : Type w))
          ((↑((A.indToCoind : (a : IndV S.subtype A.ρ) → ↥(coindV S.subtype A.ρ))
                  (⟦b⟧.liftOn
                    (fun (g_1 : G) ↦
                      (IndV.mk S.subtype A.ρ g_1 : (a : (↑A : Type w)) → IndV S.subtype A.ρ)
                        ((↑g : G → (↑A : Type w)) g_1))
                    ⋯)) :
              G → (↑A : Type w))
            a)
          0
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((↑((A.indToCoind : (a : IndV S.subtype A.ρ) → ↥(coindV S.subtype A.ρ))
            (b.liftOn
              (fun (g_1 : G) ↦
                (IndV.mk S.subtype A.ρ g_1 : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑g : G → (↑A : Type w)) g_1))
              ⋯)) :
        G → (↑A : Type w))
      a)
    0

Tactic:
induction b using Quotient.inductionOn with | h b =>
    simpa using indToCoindAux_of_not_rel b a (g.1 b) (mt Quotient.sound hb.symm)
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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
g : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
a : G
⊢ ⟦a⟧ ∉ Finset.univ →
    Eq.{w + 1} (α := (↑A : Type w))
      ((↑((A.indToCoind : (a : IndV S.subtype A.ρ) → ↥(coindV S.subtype A.ρ))
              (⟦a⟧.liftOn
                (fun (g_1 : G) ↦
                  (IndV.mk S.subtype A.ρ g_1 : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑g : G → (↑A : Type w)) g_1))
                ⋯)) :
          G → (↑A : Type w))
        a)
      0

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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
X Y : Rep.{max u w, u, v} k ↥S
f : X ⟶ Y
simp :
  Eq (α := ind S.subtype X ⟶ coind.{u, v, v, max u w} S.subtype Y)
    (CategoryTheory.Functor.map (indFunctor k S.subtype) f ≫ (indCoindIso.{w, u, v} Y).hom :
      ind S.subtype X ⟶ coind.{u, v, v, max u w} S.subtype Y)
    ((indCoindIso.{w, u, v} X).hom ≫ CategoryTheory.Functor.map (coindFunctor k S.subtype) f :
      ind S.subtype X ⟶ coind.{u, v, v, max u w} S.subtype Y)
⊢ Eq (α := Functor.obj (indFunctor k S.subtype) X ⟶ Functor.obj (coindFunctor k S.subtype) Y)
    (CategoryTheory.Functor.map (indFunctor k S.subtype) f ≫
      Iso.hom ((fun (A : Rep.{max u w, u, v} k ↥S) ↦ indCoindIso.{w, u, v} A) Y))
    (Iso.hom ((fun (A : Rep.{max u w, u, v} k ↥S) ↦ indCoindIso.{w, u, v} A) X) ≫
      CategoryTheory.Functor.map (coindFunctor k S.subtype) f)

Tactic:
simp only [indFunctor_obj, coindFunctor_obj]

Premises used: Rep.indFunctor_obj, Rep.coindFunctor_obj
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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
X Y : Rep.{max u w, u, v} k ↥S
f : X ⟶ Y
g1 : G
x : (↑X : Type (max u w))
g2 : G
⊢ Eq (α := (↑Y : Type (max u w)))
    ((↑((((AlgebraTensorModule.curry
                        ((IntertwiningMap.toLinearMap (G := G) (ρ := (ind S.subtype X).ρ) (σ :=
                              (coind.{u, v, v, max u w} S.subtype Y).ρ)
                              (Hom.hom
                                (CategoryTheory.Functor.map (indFunctor k S.subtype) f ≫
                                  (indCoindIso.{w, u, v} Y).hom)) :
                            (↑(ind S.subtype X) : Type (max (max u v) w)) →ₗ[k]
                              (↑(coind.{u, v, v, max u w} S.subtype Y) : Type (max (max u v) w))) ∘ₗ
                          (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) X.ρ) :
                            (G →₀ k) ⊗[k] (↑X : Type (max u w)) →ₗ[k]
                              (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) X.ρ).Coinvariants (k :=
                                k) (G := ↥S) (V := (G →₀ k) ⊗[k] (↑X : Type (max u w))))) ∘ₗ
                      lsingle g1 :
                    k →ₗ[k]
                      (↑X : Type (max u w)) →ₗ[k] (↑(coind.{u, v, v, max u w} S.subtype Y) : Type (max (max u v) w))) :
                  (a : k) →
                    (↑X : Type (max u w)) →ₗ[k] (↑(coind.{u, v, v, max u w} S.subtype Y) : Type (max (max u v) w)))
                1 :
              (a : (↑X : Type (max u w))) → (↑(coind.{u, v, v, max u w} S.subtype Y) : Type (max (max u v) w)))
            x) :
        G → (↑Y : Type (max u w)))
      g2)
    ((↑((((AlgebraTensorModule.curry
                        (IntertwiningMap.toLinearMap
                            (Hom.hom
                              ((indCoindIso.{w, u, v} X).hom ≫
                                CategoryTheory.Functor.map (coindFunctor k S.subtype) f)) ∘ₗ
                          Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) X.ρ)) ∘ₗ
                      lsingle g1 :
                    k →ₗ[k]
                      (↑X : Type (max u w)) →ₗ[k] (↑(coind.{u, v, v, max u w} S.subtype Y) : Type (max (max u v) w))) :
                  (a : k) →
                    (↑X : Type (max u w)) →ₗ[k] (↑(coind.{u, v, v, max u w} S.subtype Y) : Type (max (max u v) w)))
                1 :
              (a : (↑X : Type (max u w))) → (↑(coind.{u, v, v, max u w} S.subtype Y) : Type (max (max u v) w)))
            x) :
        G → (↑Y : Type (max u w)))
      g2)

Tactic:
simp [indToCoind, indMap, indToCoindAux_comm]

Premises used: Rep.indToCoind, Rep.indToCoindAux_comm, Rep.indMap
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : S.FiniteIndex
⊢ Functor.IsRightAdjoint (C := Rep.{max w u v, u, v} k G) (indFunctor k S.subtype)

Tactic:
open scoped Classical in (resIndAdjunction k S).isRightAdjoint

Premises used: Rep.resIndAdjunction, CategoryTheory.Adjunction.isRightAdjoint
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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)
inst_3 : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
⊢ NatTrans.app (Adjunction.counit (resIndAdjunction.{w, u, v} k S)) A =
    CategoryTheory.Functor.map (resFunctor S.subtype) A.indCoindIso.hom ≫
      NatTrans.app (Adjunction.counit (resCoindAdjunction k S.subtype)) A

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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)
inst_3 : S.FiniteIndex
B : Rep.{max w u v, u, v} k G
⊢ NatTrans.app (Adjunction.unit (resIndAdjunction.{w, u, v} k S)) B =
    NatTrans.app (Adjunction.unit (resCoindAdjunction k S.subtype)) B ≫ (res S.subtype B).indCoindIso.inv

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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)
inst_3 : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
B : Rep.{max w u v, u, v} k G
f : res S.subtype B ⟶ A
rw :
  Eq (α := B ⟶ Functor.obj (indFunctor k S.subtype) A)
    ((Adjunction.homEquiv (resCoindAdjunction k S.subtype) B A :
            (a : (resFunctor S.subtype).obj B ⟶ A) → B ⟶ (coindFunctor k S.subtype).obj A)
          f ≫
        NatTrans.app (Iso.hom (Iso.symm (indCoindNatIso k S))) A :
      B ⟶ Functor.obj (indFunctor k S.subtype) A)
    ((resCoindHomEquiv.{max w u v, u, v, v} S.subtype B A :
            (a : res S.subtype B ⟶ A) → B ⟶ coind.{u, v, v, max (max w u v) v} S.subtype A)
          f ≫
        A.indCoindIso.inv :
      B ⟶ ind S.subtype A)
⊢ Eq (α := B ⟶ Functor.obj (indFunctor k S.subtype) A)
    ((Adjunction.homEquiv (resIndAdjunction.{w, u, v} k S) B A :
          (a : (resFunctor S.subtype).obj B ⟶ A) → B ⟶ (indFunctor k S.subtype).obj A)
        f :
      B ⟶ Functor.obj (indFunctor k S.subtype) A)
    ((resCoindHomEquiv.{max w u v, u, v, v} S.subtype B A :
            (a : res S.subtype B ⟶ A) → B ⟶ coind.{u, v, v, max (max w u v) v} S.subtype A)
          f ≫
        A.indCoindIso.inv :
      B ⟶ ind S.subtype A)

Tactic:
rw [resIndAdjunction, Adjunction.homEquiv_ofNatIsoRight_apply]

Premises used: CategoryTheory.Adjunction.homEquiv_ofNatIsoRight_apply, Rep.resIndAdjunction
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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)
inst_3 : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
B : Rep.{max w u v, u, v} k G
f : res S.subtype B ⟶ A
⊢ Eq (α := B ⟶ Functor.obj (indFunctor k S.subtype) A)
    ((Adjunction.homEquiv (resCoindAdjunction k S.subtype) B A :
            (a : (resFunctor S.subtype).obj B ⟶ A) → B ⟶ (coindFunctor k S.subtype).obj A)
          f ≫
        NatTrans.app (Iso.hom (Iso.symm (indCoindNatIso k S))) A :
      B ⟶ Functor.obj (indFunctor k S.subtype) A)
    ((resCoindHomEquiv.{max w u v, u, v, v} S.subtype B A :
            (a : res S.subtype B ⟶ A) → B ⟶ coind.{u, v, v, max (max w u v) v} S.subtype A)
          f ≫
        A.indCoindIso.inv :
      B ⟶ ind S.subtype A)

Tactic:
simp [resCoindHomEquiv]

Premises used: Rep.resCoindHomEquiv
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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)
inst_3 : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
B : Rep.{max w u v, u, v} k G
f : B ⟶ Functor.obj (indFunctor k S.subtype) A
⊢ Eq (α := Functor.obj (resFunctor S.subtype) B ⟶ A)
    (((Adjunction.homEquiv (resIndAdjunction.{w, u, v} k S) B A).symm :
          (a : B ⟶ (indFunctor k S.subtype).obj A) → (resFunctor S.subtype).obj B ⟶ A)
        f :
      Functor.obj (resFunctor S.subtype) B ⟶ A)
    (((resCoindHomEquiv.{max w u v, u, v, v} S.subtype B A).symm :
          (a : B ⟶ coind.{u, v, v, max (max w u v) v} S.subtype A) → res S.subtype B ⟶ A)
        (f ≫ A.indCoindIso.hom) :
      res S.subtype B ⟶ A)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : S.FiniteIndex
⊢ Functor.IsLeftAdjoint (C := Rep.{max w u v, u, v} k ↥S) (coindFunctor k S.subtype)

Tactic:
open scoped Classical in (coindResAdjunction k S).isLeftAdjoint

Premises used: Rep.coindResAdjunction, CategoryTheory.Adjunction.isLeftAdjoint
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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)
inst_3 : S.FiniteIndex
B : Rep.{max w u v, u, v} k G
⊢ NatTrans.app (Adjunction.counit (coindResAdjunction.{w, u, v} k S)) B =
    (res S.subtype B).indCoindIso.inv ≫ NatTrans.app (Adjunction.counit (indResAdjunction.{w, u, v, v} k S.subtype)) B

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.FiniteIndex
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)
inst_3 : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
hf :
  ∀ (x : (↑(Functor.obj (𝟭 (Rep.{max (max u v) w, u, v} k ↥S)) A) : Type (max (max u v) w))),
    Eq (α := (↑(Functor.obj (coindFunctor k S.subtype ⋙ resFunctor S.subtype) A) : Type (max (max u v) w)))
      (((Hom.hom (NatTrans.app (Adjunction.unit (coindResAdjunction.{w, u, v} k S)) A)).toLinearMap :
            (a : (↑((𝟭 (Rep.{max (max u v) w, u, v} k ↥S)).obj A) : Type (max (max u v) w))) →
              (↑((coindFunctor k S.subtype ⋙ resFunctor S.subtype).obj A) : Type (max (max u v) w)))
          x :
        (↑(Functor.obj (coindFunctor k S.subtype ⋙ resFunctor S.subtype) A) : Type (max (max u v) w)))
      ((IntertwiningMap.toLinearMap
              (Hom.hom
                (NatTrans.app (Adjunction.unit (indResAdjunction.{w, u, v, v} k S.subtype)) A ≫
                  CategoryTheory.Functor.map (resFunctor S.subtype) A.indCoindIso.hom)) :
            (a : (↑((𝟭 (Rep.{max (max u v) w, u, v} k ↥S)).obj A) : Type (max (max u v) w))) →
              (↑((coindFunctor k S.subtype ⋙ resFunctor S.subtype).obj A) : Type (max (max u v) w)))
          x :
        (↑(Functor.obj (coindFunctor k S.subtype ⋙ resFunctor S.subtype) A) : Type (max (max u v) w)))
⊢ NatTrans.app (Adjunction.unit (coindResAdjunction.{w, u, v} k S)) A =
    NatTrans.app (Adjunction.unit (indResAdjunction.{w, u, v, v} k S.subtype)) A ≫
      CategoryTheory.Functor.map (resFunctor S.subtype) A.indCoindIso.hom

Tactic:
ext