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
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))
b : G
hx : ∀ (x : G), ¬(↑f : G → (↑A : Type w)) x = 0 → x ∈ MulAction.orbit (↥S) g
h : Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ ⟦b⟧
hb : ¬(QuotientGroup.rightRel S : G → G → Prop) b g
⊢ (↑f : G → (↑A : Type w)) b = 0
have contrapose! : ∀ (hx : (↑f : G → (↑A : Type w)) b ≠ 0), ∃ (x : G), (↑f : G → (↑A : Type w)) x ≠ 0 ∧ x ∉ MulAction.orbit (↥S) g
Tactic: contrapose! hx
Cleared hypotheses: hx
-- 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))
b : G
h : Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ ⟦b⟧
hb : ¬(QuotientGroup.rightRel S : G → G → Prop) b g
hx : (↑f : G → (↑A : Type w)) b ≠ 0
w : G
left : (↑f : G → (↑A : Type w)) b ≠ 0
⊢ ∃ (x : G), (↑f : G → (↑A : Type w)) x ≠ 0 ∧ x ∉ MulAction.orbit (↥S) g
have right : b ∉ MulAction.orbit (↥S) g
Tactic: use b, hx, 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⟧
⊢ ⟦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
have this : (↑f : G → (↑A : Type w)) b = 0
Tactic: have : f.1 b = 0 := by
      simp_all only [Function.support_subset_iff, ne_eq, Quotient.eq]
      contrapose! hx
      use b, hx, hb
-- 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
b : Quotient (QuotientGroup.rightRel S)
h : Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ b
hb : 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
have h₀ : ∀ (b : G),
  Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ ⟦b⟧ →
    ∀ (hb : ⟦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: induction b using Quotient.inductionOn with | h b =>
    have : f.1 b = 0 := by
      simp_all only [Function.support_subset_iff, ne_eq, Quotient.eq]
      contrapose! hx
      use b, hx, hb
    simp_all
Cleared hypotheses: b, h, hb
-- 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
inst_3 : S.FiniteIndex
⊢ A.indToCoind ∘ₗ A.coindToInd = LinearMap.id
have 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)
Tactic: ext g a
-- 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
inst_3 : S.FiniteIndex
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)
have 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
Tactic: simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.id_coe, id_eq]
-- 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
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.coindToInd : (a : ↥(coindV S.subtype A.ρ)) → IndV S.subtype A.ρ) g)) :
      G → (↑A : Type w))
    a
have 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))
            sorry)) :
    G → (↑A : Type w))
  a
Tactic: rw [coindToInd_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
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.coindToInd : (a : ↥(coindV S.subtype A.ρ)) → IndV S.subtype A.ρ) g)) :
        G → (↑A : Type w))
      a =
    (↑g : G → (↑A : Type w)) a
have 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))
              sorry)) :
      G → (↑A : Type w))
    a =
  (↑g : G → (↑A : Type w)) a
Tactic: conv_lhs => rw [coindToInd_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
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.ρ))
            (∑ 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
have 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))
              sorry)) :
        G → (↑A : Type w))
      a =
  (↑g : G → (↑A : Type w)) a
Tactic: simp only [map_sum, AddSubmonoidClass.coe_finsetSum, Finset.sum_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
inst_3 : S.FiniteIndex
g : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
a : G
⊢ ∑ 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
have 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))
            sorry)) :
      G → (↑A : Type w))
    a =
  (↑g : G → (↑A : Type w)) a
Tactic: rw [Finset.sum_eq_single ⟦a⟧]
-- 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
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
⊢ ∑ 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
have 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))
                  sorry)) :
            G → (↑A : Type w))
          a)
        0
Tactic: rw [Finset.sum_eq_single ⟦a⟧]
-- 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
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
⊢ ∑ 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
have 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))
              sorry)) :
        G → (↑A : Type w))
      a)
    0
Tactic: rw [Finset.sum_eq_single ⟦a⟧]
-- 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
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
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
have 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))
                  sorry)) :
            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)
Cleared hypotheses: b, h, hb
-- 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
inst_3 : S.FiniteIndex
X Y : Rep.{max u w, u, v} k ↥S
f : X ⟶ 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)
have 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)
Tactic: simp only [indFunctor_obj, coindFunctor_obj]
-- 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)
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 (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)
have 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)
Tactic: rw [resIndAdjunction, Adjunction.homEquiv_ofNatIsoRight_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)
inst_3 : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
⊢ 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
have 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)))
Tactic: ext
-- 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)
inst_3 : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
B : Rep.{max (max u v) w, u, v} k G
f : A ⟶ res S.subtype B
⊢ Eq (α := Functor.obj (coindFunctor k S.subtype) A ⟶ B)
    (((Adjunction.homEquiv (coindResAdjunction k S) A B).symm :
          (a : A ⟶ (resFunctor S.subtype).obj B) → (coindFunctor k S.subtype).obj A ⟶ B)
        f :
      Functor.obj (coindFunctor k S.subtype) A ⟶ B)
    (A.indCoindIso.inv ≫
        ((indResHomEquiv.{w, u, v, v} S.subtype A B).symm : (a : A ⟶ res S.subtype B) → ind S.subtype A ⟶ B) f :
      coind.{u, v, v, max u w u v} S.subtype A ⟶ B)
have simp : Eq (α := Functor.obj (coindFunctor k S.subtype) A ⟶ B)
  (NatTrans.app (Iso.inv (indCoindNatIso k S)) A ≫
    ((Adjunction.homEquiv
            (Adjunction.mkOfHomEquiv
              {
                homEquiv := fun (A : Rep.{max w u v, u, v} k ↥S) (B : Rep.{max w u v, u, v} k G) ↦
                  (indResHomEquiv S.subtype A B).toEquiv,
                homEquiv_naturality_left_symm := sorry, homEquiv_naturality_right := sorry :
                Adjunction.CoreHomEquiv (C := Rep.{max w u v, u, v} k ↥S) (indFunctor k S.subtype)
                  (resFunctor S.subtype) })
            A B).symm :
        (a : A ⟶ of (MonoidHom.comp B.ρ S.subtype)) → (indFunctor k S.subtype).obj A ⟶ B)
      f)
  (A.indCoindIso.inv ≫
    ((indResHomEquiv.{w, u, v, v} S.subtype A B).symm : (a : A ⟶ res S.subtype B) → ind S.subtype A ⟶ B) f)
Tactic: simp only [coindResAdjunction, indResAdjunction,
    Adjunction.homEquiv_ofNatIsoLeft_symm_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)
inst_3 : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
B : Rep.{max (max u v) w, u, v} k G
f : A ⟶ res S.subtype B
⊢ Eq (α := Functor.obj (coindFunctor k S.subtype) A ⟶ B)
    (NatTrans.app (Iso.inv (indCoindNatIso k S)) A ≫
      ((Adjunction.homEquiv
              (Adjunction.mkOfHomEquiv
                {
                  homEquiv := fun (A : Rep.{max w u v, u, v} k ↥S) (B : Rep.{max w u v, u, v} k G) ↦
                    (indResHomEquiv S.subtype A B).toEquiv,
                  homEquiv_naturality_left_symm := ⋯, homEquiv_naturality_right := ⋯ :
                  Adjunction.CoreHomEquiv (C := Rep.{max w u v, u, v} k ↥S) (indFunctor k S.subtype)
                    (resFunctor S.subtype) })
              A B).symm :
          (a : A ⟶ of (MonoidHom.comp B.ρ S.subtype)) → (indFunctor k S.subtype).obj A ⟶ B)
        f)
    (A.indCoindIso.inv ≫
      ((indResHomEquiv.{w, u, v, v} S.subtype A B).symm : (a : A ⟶ res S.subtype B) → ind S.subtype A ⟶ B) f)
have simp : Eq (α := ind S.subtype A ⟶ B)
  (((indResHomEquiv S.subtype A B).toEquiv.symm : (a : A ⟶ of (MonoidHom.comp B.ρ S.subtype)) → ind S.subtype A ⟶ B) f :
    ind S.subtype A ⟶ B)
  (ofHom
      {
        toLinearMap :=
          Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ)
            (TensorProduct.lift
              ((Finsupp.lift ((↑A : Type (max (max u v) w)) →ₗ[k] (↑B : Type (max (max u v) w))) k G :
                  (a : G → (↑A : Type (max (max u v) w)) →ₗ[k] (↑B : Type (max (max u v) w))) →
                    (G →₀ k) →ₗ[k] (↑A : Type (max (max u v) w)) →ₗ[k] (↑B : Type (max (max u v) w)))
                fun (h : G) ↦
                (B.ρ : (a : G) → (↑B : Type (max (max u v) w)) →ₗ[k] (↑B : Type (max (max u v) w))) h⁻¹ ∘ₗ
                  (Hom.hom f).toLinearMap))
            sorry,
        isIntertwining' := sorry } :
    of (Representation.ind S.subtype A.ρ) ⟶ of B.ρ)
Tactic: simp
-- 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
⊢ Coinvariants.ker ρ =
    (HSub.hSub (α := V →ₗ[k] V) (β := V →ₗ[k] V) ((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) LinearMap.id).range
have 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)
Tactic: refine le_antisymm (Submodule.span_le.2 ?_) ?_