awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G_1 : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G_1
inst_2 : Monoid H
φ : G_1 →* H
A : Rep k G_1
G : Type v'
inst_3 : Group G
S : Subgroup G
X Y : Rep.{u_1, u, v'} k ↥S
f : X ⟶ Y
inst_4 : Epi f
y : (↑(Functor.obj (coindFunctor k S.subtype) Y) : Type (max u_1 v'))
this : Setoid G := QuotientGroup.rightRel S
s : (b : (↑Y : Type u_1)) → (↑X : Type u_1)
hs : ∀ (b : (↑Y : Type u_1)), (Hom.hom f : (a : (↑X : Type u_1)) → (↑Y : Type u_1)) (s b) = b
choose! :
  ∀ (i : (b : Quotient this) → G) (hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b),
    ∃ (a : (↑(Functor.obj (coindFunctor k S.subtype) X) : Type (max u_1 v'))),
      (Hom.hom (CategoryTheory.Functor.map (coindFunctor k S.subtype) f) :
            (a : (↑((coindFunctor k S.subtype).obj X) : Type (max u_1 v'))) →
              (↑((coindFunctor k S.subtype).obj Y) : Type (max u_1 v')))
          a =
        y
⊢ ∃ (a : (↑(Functor.obj (coindFunctor k S.subtype) X) : Type (max u_1 v'))),
    (Hom.hom (CategoryTheory.Functor.map (coindFunctor k S.subtype) f) :
          (a : (↑((coindFunctor k S.subtype).obj X) : Type (max u_1 v'))) →
            (↑((coindFunctor k S.subtype).obj Y) : Type (max u_1 v')))
        a =
      y

Tactic:
choose! i hi using Quotient.mk'_surjective (α := G)

Premises used: Quotient.mk'_surjective
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G_1 : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G_1
inst_2 : Monoid H
φ : G_1 →* H
A : Rep k G_1
G : Type v'
inst_3 : Group G
S : Subgroup G
X Y : Rep.{u_1, u, v'} k ↥S
f : X ⟶ Y
inst_4 : Epi f
y : (↑(Functor.obj (coindFunctor k S.subtype) Y) : Type (max u_1 v'))
this : Setoid G := QuotientGroup.rightRel S
s_1 : (b : (↑Y : Type u_1)) → (↑X : Type u_1)
hs : ∀ (b : (↑Y : Type u_1)), (Hom.hom f : (a : (↑X : Type u_1)) → (↑Y : Type u_1)) (s_1 b) = b
i : (b : Quotient this) → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : (g : G) → ↥S := fun (g : G) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g * (i (Quotient.mk' g))⁻¹) ⋯
s : ↥S
g : G
⊢ g * ((↑s : G) * g)⁻¹ ∈ S

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G_1 : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G_1
inst_2 : Monoid H
φ : G_1 →* H
A : Rep k G_1
G : Type v'
inst_3 : Group G
S : Subgroup G
X Y : Rep.{u_1, u, v'} k ↥S
f : X ⟶ Y
inst_4 : Epi f
y : (↑(Functor.obj (coindFunctor k S.subtype) Y) : Type (max u_1 v'))
this : Setoid G := QuotientGroup.rightRel S
s : (b : (↑Y : Type u_1)) → (↑X : Type u_1)
hs : ∀ (b : (↑Y : Type u_1)), (Hom.hom f : (a : (↑X : Type u_1)) → (↑Y : Type u_1)) (s b) = b
i : (b : Quotient this) → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : (g : G) → ↥S := fun (g : G) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g * (i (Quotient.mk' g))⁻¹) ⋯
⊢ ∀ (s : ↥S) (g : G), Eq (α := Quotient this) (Quotient.mk' ((↑s : G) * g)) (Quotient.mk' g)

Tactic:
have hmk (s : S) (g : G) : Quotient.mk' (s.1 * g) = Quotient.mk' g :=
      Quotient.eq'.2 (QuotientGroup.rightRel_apply.2 (by simp))
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G_1 : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G_1
inst_2 : Monoid H
φ : G_1 →* H
A : Rep k G_1
G : Type v'
inst_3 : Group G
S : Subgroup G
X Y : Rep.{u_1, u, v'} k ↥S
f : X ⟶ Y
inst_4 : Epi f
y : (↑(Functor.obj (coindFunctor k S.subtype) Y) : Type (max u_1 v'))
this : Setoid G := QuotientGroup.rightRel S
s_1 : (b : (↑Y : Type u_1)) → (↑X : Type u_1)
hs : ∀ (b : (↑Y : Type u_1)), (Hom.hom f : (a : (↑X : Type u_1)) → (↑Y : Type u_1)) (s_1 b) = b
i : (b : Quotient this) → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : (g : G) → ↥S := fun (g : G) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g * (i (Quotient.mk' g))⁻¹) ⋯
hmk : ∀ (s : ↥S) (g : G), Eq (α := Quotient this) (Quotient.mk' ((↑s : G) * g)) (Quotient.mk' g)
s : ↥S
g : G
a : (↑(γ ((↑s : G) * g)) : G) = (↑(s * γ g) : G)
⊢ γ ((↑s : G) * g) = s * γ g

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G_1 : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G_1
inst_2 : Monoid H
φ : G_1 →* H
A : Rep k G_1
G : Type v'
inst_3 : Group G
S : Subgroup G
X Y : Rep.{u_1, u, v'} k ↥S
f : X ⟶ Y
inst_4 : Epi f
y : (↑(Functor.obj (coindFunctor k S.subtype) Y) : Type (max u_1 v'))
this : Setoid G := QuotientGroup.rightRel S
s_1 : (b : (↑Y : Type u_1)) → (↑X : Type u_1)
hs : ∀ (b : (↑Y : Type u_1)), (Hom.hom f : (a : (↑X : Type u_1)) → (↑Y : Type u_1)) (s_1 b) = b
i : (b : Quotient this) → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : (g : G) → ↥S := fun (g : G) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g * (i (Quotient.mk' g))⁻¹) ⋯
hmk : ∀ (s : ↥S) (g : G), Eq (α := Quotient this) (Quotient.mk' ((↑s : G) * g)) (Quotient.mk' g)
s : ↥S
g : G
⊢ (↑(γ ((↑s : G) * g)) : G) = (↑(s * γ g) : G)

Tactic:
simp [mul_assoc, γ, hmk]

Premises used: mul_assoc
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G_1 : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G_1
inst_2 : Monoid H
φ : G_1 →* H
A : Rep k G_1
G : Type v'
inst_3 : Group G
S : Subgroup G
X Y : Rep.{u_1, u, v'} k ↥S
f : X ⟶ Y
inst_4 : Epi f
y : (↑(Functor.obj (coindFunctor k S.subtype) Y) : Type (max u_1 v'))
this : Setoid G := QuotientGroup.rightRel S
s : (b : (↑Y : Type u_1)) → (↑X : Type u_1)
hs : ∀ (b : (↑Y : Type u_1)), (Hom.hom f : (a : (↑X : Type u_1)) → (↑Y : Type u_1)) (s b) = b
i : (b : Quotient this) → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : (g : G) → ↥S := fun (g : G) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g * (i (Quotient.mk' g))⁻¹) ⋯
hmk : ∀ (s : ↥S) (g : G), Eq (α := Quotient this) (Quotient.mk' ((↑s : G) * g)) (Quotient.mk' g)
⊢ ∀ (s : ↥S) (g : G), γ ((↑s : G) * g) = s * γ g

Tactic:
have hγ (s : S) (g : G) : γ (s.1 * g) = s * γ g := by ext; simp [mul_assoc, γ, hmk]
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G_1 : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G_1
inst_2 : Monoid H
φ : G_1 →* H
A : Rep k G_1
G : Type v'
inst_3 : Group G
S : Subgroup G
X Y : Rep.{u_1, u, v'} k ↥S
f : X ⟶ Y
inst_4 : Epi f
y : (↑(Functor.obj (coindFunctor k S.subtype) Y) : Type (max u_1 v'))
this : Setoid G := QuotientGroup.rightRel S
s : (b : (↑Y : Type u_1)) → (↑X : Type u_1)
hs : ∀ (b : (↑Y : Type u_1)), (Hom.hom f : (a : (↑X : Type u_1)) → (↑Y : Type u_1)) (s b) = b
i : (b : Quotient this) → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : (g : G) → ↥S := fun (g : G) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g * (i (Quotient.mk' g))⁻¹) ⋯
hmk : ∀ (s : ↥S) (g : G), Eq (α := Quotient this) (Quotient.mk' ((↑s : G) * g)) (Quotient.mk' g)
hγ : ∀ (s : ↥S) (g : G), γ ((↑s : G) * g) = s * γ g
x : (g : G) → (↑X : Type u_1) :=
  fun (g : G) ↦
    (((X.ρ : (a : ↥S) → (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) (γ g) : (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) :
        (a : (↑X : Type u_1)) → (↑X : Type u_1))
      (s ((↑y : G → (↑Y : Type u_1)) (i (Quotient.mk' g))))
⊢ ∃ (a : (↑(Functor.obj (coindFunctor k S.subtype) X) : Type (max u_1 v'))),
    (Hom.hom (CategoryTheory.Functor.map (coindFunctor k S.subtype) f) :
          (a : (↑((coindFunctor k S.subtype).obj X) : Type (max u_1 v'))) →
            (↑((coindFunctor k S.subtype).obj Y) : Type (max u_1 v')))
        a =
      y

Tactic:
⟨⟨x, fun _ _ => ?_⟩, Subtype.ext <| funext fun g => ?_⟩

Premises used: Subtype.mk, funext, Exists.intro, Subtype.ext
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G_1 : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G_1
inst_2 : Monoid H
φ : G_1 →* H
A : Rep k G_1
G : Type v'
inst_3 : Group G
S : Subgroup G
X Y : Rep.{u_1, u, v'} k ↥S
f : X ⟶ Y
inst_4 : Epi f
y : (↑(Functor.obj (coindFunctor k S.subtype) Y) : Type (max u_1 v'))
this : Setoid G := QuotientGroup.rightRel S
s : (b : (↑Y : Type u_1)) → (↑X : Type u_1)
hs : ∀ (b : (↑Y : Type u_1)), (Hom.hom f : (a : (↑X : Type u_1)) → (↑Y : Type u_1)) (s b) = b
i : (b : Quotient this) → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : (g : G) → ↥S := fun (g : G) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g * (i (Quotient.mk' g))⁻¹) ⋯
hmk : ∀ (s : ↥S) (g : G), Eq (α := Quotient this) (Quotient.mk' ((↑s : G) * g)) (Quotient.mk' g)
hγ : ∀ (s : ↥S) (g : G), γ ((↑s : G) * g) = s * γ g
x : (g : G) → (↑X : Type u_1) :=
  fun (g : G) ↦
    (((X.ρ : (a : ↥S) → (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) (γ g) : (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) :
        (a : (↑X : Type u_1)) → (↑X : Type u_1))
      (s ((↑y : G → (↑Y : Type u_1)) (i (Quotient.mk' g))))
refine_1 :
  ∀ (x_1 : ↥S) (x_2 : G),
    x (HMul.hMul (α := G) ((S.subtype : (a : ↥S) → G) x_1 : G) x_2) =
      (((X.ρ : (a : ↥S) → (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) x_1 : (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) :
          (a : (↑X : Type u_1)) → (↑X : Type u_1))
        (x x_2)
refine_2 :
  ∀ (g : G),
    (↑((Hom.hom (CategoryTheory.Functor.map (coindFunctor k S.subtype) f) :
                (a : (↑((coindFunctor k S.subtype).obj X) : Type (max u_1 v'))) →
                  (↑((coindFunctor k S.subtype).obj Y) : Type (max u_1 v')))
              (Subtype.mk (p := fun (x : G → (↑X : Type u_1)) ↦ x ∈ Representation.coindV S.subtype X.ρ) x ⋯)) :
          G → (↑Y : Type u_1))
        g =
      (↑y : G → (↑Y : Type u_1)) g
⊢ ∃ (a : (↑(Functor.obj (coindFunctor k S.subtype) X) : Type (max u_1 v'))),
    (Hom.hom (CategoryTheory.Functor.map (coindFunctor k S.subtype) f) :
          (a : (↑((coindFunctor k S.subtype).obj X) : Type (max u_1 v'))) →
            (↑((coindFunctor k S.subtype).obj Y) : Type (max u_1 v')))
        a =
      y

Tactic:
refine ⟨⟨x, fun _ _ => ?_⟩, Subtype.ext <| funext fun g => ?_⟩
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G_1 : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G_1
inst_2 : Monoid H
φ : G_1 →* H
A : Rep k G_1
G : Type v'
inst_3 : Group G
S : Subgroup G
X Y : Rep.{u_1, u, v'} k ↥S
f : X ⟶ Y
inst_4 : Epi f
y : (↑(Functor.obj (coindFunctor k S.subtype) Y) : Type (max u_1 v'))
this : Setoid G := QuotientGroup.rightRel S
s : (b : (↑Y : Type u_1)) → (↑X : Type u_1)
hs : ∀ (b : (↑Y : Type u_1)), (Hom.hom f : (a : (↑X : Type u_1)) → (↑Y : Type u_1)) (s b) = b
i : (b : Quotient this) → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : (g : G) → ↥S := fun (g : G) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g * (i (Quotient.mk' g))⁻¹) ⋯
hmk : ∀ (s : ↥S) (g : G), Eq (α := Quotient this) (Quotient.mk' ((↑s : G) * g)) (Quotient.mk' g)
hγ : ∀ (s : ↥S) (g : G), γ ((↑s : G) * g) = s * γ g
x : (g : G) → (↑X : Type u_1) :=
  fun (g : G) ↦
    (((X.ρ : (a : ↥S) → (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) (γ g) : (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) :
        (a : (↑X : Type u_1)) → (↑X : Type u_1))
      (s ((↑y : G → (↑Y : Type u_1)) (i (Quotient.mk' g))))
x_1 : ↥S
x_2 : G
⊢ x (HMul.hMul (α := G) ((S.subtype : (a : ↥S) → G) x_1 : G) x_2) =
    (((X.ρ : (a : ↥S) → (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) x_1 : (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) :
        (a : (↑X : Type u_1)) → (↑X : Type u_1))
      (x x_2)

Tactic:
simp [x, ← Module.End.mul_apply, ← map_mul, hmk, hγ]

Premises used: map_mul, Module.End.mul_apply
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G_1 : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G_1
inst_2 : Monoid H
φ : G_1 →* H
A : Rep k G_1
G : Type v'
inst_3 : Group G
S : Subgroup G
X Y : Rep.{u_1, u, v'} k ↥S
f : X ⟶ Y
inst_4 : Epi f
y : (↑(Functor.obj (coindFunctor k S.subtype) Y) : Type (max u_1 v'))
this : Setoid G := QuotientGroup.rightRel S
s : (b : (↑Y : Type u_1)) → (↑X : Type u_1)
hs : ∀ (b : (↑Y : Type u_1)), (Hom.hom f : (a : (↑X : Type u_1)) → (↑Y : Type u_1)) (s b) = b
i : (b : Quotient this) → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : (g : G) → ↥S := fun (g : G) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g * (i (Quotient.mk' g))⁻¹) ⋯
hmk : ∀ (s : ↥S) (g : G), Eq (α := Quotient this) (Quotient.mk' ((↑s : G) * g)) (Quotient.mk' g)
hγ : ∀ (s : ↥S) (g : G), γ ((↑s : G) * g) = s * γ g
x : (g : G) → (↑X : Type u_1) :=
  fun (g : G) ↦
    (((X.ρ : (a : ↥S) → (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) (γ g) : (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) :
        (a : (↑X : Type u_1)) → (↑X : Type u_1))
      (s ((↑y : G → (↑Y : Type u_1)) (i (Quotient.mk' g))))
g : G
refine_2 :
  (((Y.ρ : (a : ↥S) → (↑Y : Type u_1) →ₗ[k] (↑Y : Type u_1)) (γ g) : (↑Y : Type u_1) →ₗ[k] (↑Y : Type u_1)) :
        (a : (↑Y : Type u_1)) → (↑Y : Type u_1))
      ((Hom.hom f : (a : (↑X : Type u_1)) → (↑Y : Type u_1)) (s ((↑y : G → (↑Y : Type u_1)) (i (Quotient.mk' g)))) :
        (↑Y : Type u_1)) =
    (↑y : G → (↑Y : Type u_1)) g
⊢ (↑((Hom.hom (CategoryTheory.Functor.map (coindFunctor k S.subtype) f) :
              (a : (↑((coindFunctor k S.subtype).obj X) : Type (max u_1 v'))) →
                (↑((coindFunctor k S.subtype).obj Y) : Type (max u_1 v')))
            (Subtype.mk (p := fun (x : G → (↑X : Type u_1)) ↦ x ∈ Representation.coindV S.subtype X.ρ) x ⋯)) :
        G → (↑Y : Type u_1))
      g =
    (↑y : G → (↑Y : Type u_1)) g

Tactic:
simp only [coindFunctor_obj, coindFunctor_map, hom_ofHom,
        Representation.coindMap_coe_apply_apply, hom_comm_apply, x]

Premises used: Rep.coindFunctor_map, Rep.hom_ofHom, Representation.coindMap_coe_apply_apply, Rep.hom_comm_apply, Rep.coindFunctor_obj
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G_1 : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G_1
inst_2 : Monoid H
φ : G_1 →* H
A : Rep k G_1
G : Type v'
inst_3 : Group G
S : Subgroup G
X Y : Rep.{u_1, u, v'} k ↥S
f : X ⟶ Y
inst_4 : Epi f
y : (↑(Functor.obj (coindFunctor k S.subtype) Y) : Type (max u_1 v'))
this : Setoid G := QuotientGroup.rightRel S
s : (b : (↑Y : Type u_1)) → (↑X : Type u_1)
hs : ∀ (b : (↑Y : Type u_1)), (Hom.hom f : (a : (↑X : Type u_1)) → (↑Y : Type u_1)) (s b) = b
i : (b : Quotient this) → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : (g : G) → ↥S := fun (g : G) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g * (i (Quotient.mk' g))⁻¹) ⋯
hmk : ∀ (s : ↥S) (g : G), Eq (α := Quotient this) (Quotient.mk' ((↑s : G) * g)) (Quotient.mk' g)
hγ : ∀ (s : ↥S) (g : G), γ ((↑s : G) * g) = s * γ g
x : (g : G) → (↑X : Type u_1) :=
  fun (g : G) ↦
    (((X.ρ : (a : ↥S) → (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) (γ g) : (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) :
        (a : (↑X : Type u_1)) → (↑X : Type u_1))
      (s ((↑y : G → (↑Y : Type u_1)) (i (Quotient.mk' g))))
g : G
⊢ (((Y.ρ : (a : ↥S) → (↑Y : Type u_1) →ₗ[k] (↑Y : Type u_1)) (γ g) : (↑Y : Type u_1) →ₗ[k] (↑Y : Type u_1)) :
        (a : (↑Y : Type u_1)) → (↑Y : Type u_1))
      ((Hom.hom f : (a : (↑X : Type u_1)) → (↑Y : Type u_1)) (s ((↑y : G → (↑Y : Type u_1)) (i (Quotient.mk' g)))) :
        (↑Y : Type u_1)) =
    (↑y : G → (↑Y : Type u_1)) g

Tactic:
simp_all [← y.2 (γ g), γ]

Premises used: Subtype.property
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Rep k G
h :
  ∀ (x : res φ (leftRegular k H) ⟶ A) (a : H),
    Eq (α := (↑A : Type (max u w)))
      (((Representation.IntertwiningMap.toLinearMap
                (Hom.hom
                  (({
                        toFun := fun (f : res φ (leftRegular k H) ⟶ A) ↦
                          CategoryTheory.Functor.map (resFunctor φ)
                              (((↑(LinearEquiv.symm (leftRegularHomEquiv (leftRegular k H))) :
                                    (↑(leftRegular k H) : Type (max u w)) →ₗ[k] leftRegular k H ⟶ leftRegular k H) :
                                  (a : (↑(leftRegular k H) : Type (max u w))) → leftRegular k H ⟶ leftRegular k H)
                                (single 1 1)) ≫
                            f,
                        map_add' := ⋯, map_smul' := ⋯ :
                        (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ A } :
                      (a : res φ (leftRegular k H) ⟶ A) → res φ (leftRegular k H) ⟶ A)
                    x)) :
              (↑(res φ (leftRegular k H)) : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) ∘ₗ
            lsingle a :
          (a : k) → (↑A : Type (max u w)))
        1)
      (((Representation.IntertwiningMap.toLinearMap
                (Hom.hom ((1 : (a : res φ (leftRegular k H) ⟶ A) → res φ (leftRegular k H) ⟶ A) x)) :
              (↑(res φ (leftRegular k H)) : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) ∘ₗ
            lsingle a :
          (a : k) → (↑A : Type (max u w)))
        1)
⊢ Eq (α := (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ A)
    {
      toFun := fun (f : res φ (leftRegular k H) ⟶ A) ↦
        CategoryTheory.Functor.map (resFunctor φ)
            (((↑(LinearEquiv.symm (leftRegularHomEquiv (leftRegular k H))) :
                  (↑(leftRegular k H) : Type (max u w)) →ₗ[k] leftRegular k H ⟶ leftRegular k H) :
                (a : (↑(leftRegular k H) : Type (max u w))) → leftRegular k H ⟶ leftRegular k H)
              (single 1 1)) ≫
          f,
      map_add' := ⋯, map_smul' := ⋯ }
    1

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Rep k G
x : res φ (leftRegular k H) ⟶ A
a : H
⊢ Eq (α := (↑A : Type (max u w)))
    (((Representation.IntertwiningMap.toLinearMap
              (Hom.hom
                (({
                      toFun := fun (f : res φ (leftRegular k H) ⟶ A) ↦
                        CategoryTheory.Functor.map (resFunctor φ)
                            (((↑(LinearEquiv.symm (leftRegularHomEquiv (leftRegular k H))) :
                                  (↑(leftRegular k H) : Type (max u w)) →ₗ[k] leftRegular k H ⟶ leftRegular k H) :
                                (a : (↑(leftRegular k H) : Type (max u w))) → leftRegular k H ⟶ leftRegular k H)
                              (single 1 1)) ≫
                          f,
                      map_add' := ⋯, map_smul' := ⋯ :
                      (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ A } :
                    (a : res φ (leftRegular k H) ⟶ A) → res φ (leftRegular k H) ⟶ A)
                  x)) :
            (↑(res φ (leftRegular k H)) : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) ∘ₗ
          lsingle a :
        (a : k) → (↑A : Type (max u w)))
      1)
    (((Representation.IntertwiningMap.toLinearMap
              (Hom.hom ((1 : (a : res φ (leftRegular k H) ⟶ A) → res φ (leftRegular k H) ⟶ A) x)) :
            (↑(res φ (leftRegular k H)) : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) ∘ₗ
          lsingle a :
        (a : k) → (↑A : Type (max u w)))
      1)

Tactic:
simp [homEquiv]

Premises used: Rep.homEquiv
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Rep k G
f g : (↑(coind' φ A) : Type (max u w))
hfg :
  ∀ (h : H),
    Eq (α := (↑A : Type (max u w)))
      (((Hom.hom f).toLinearMap : (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑A : Type (max u w)))
          (single h 1) :
        (↑A : Type (max u w)))
      (((Hom.hom g).toLinearMap : (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑A : Type (max u w)))
          (single h 1) :
        (↑A : Type (max u w)))
h : (Hom.hom f).toLinearMap = (Hom.hom g).toLinearMap
⊢ Hom.hom f = Hom.hom g

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Rep k G
f g : (↑(coind' φ A) : Type (max u w))
hfg :
  ∀ (h : H),
    Eq (α := (↑A : Type (max u w)))
      (((Hom.hom f).toLinearMap : (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑A : Type (max u w)))
          (single h 1) :
        (↑A : Type (max u w)))
      (((Hom.hom g).toLinearMap : (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑A : Type (max u w)))
          (single h 1) :
        (↑A : Type (max u w)))
h :
  ∀ (h : H),
    Eq (α := (↑A : Type (max u w))) (((Hom.hom f).toLinearMap ∘ₗ lsingle h : (a : k) → (↑A : Type (max u w))) 1)
      (((Hom.hom g).toLinearMap ∘ₗ lsingle h : (a : k) → (↑A : Type (max u w))) 1)
⊢ (Hom.hom f).toLinearMap = (Hom.hom g).toLinearMap

Tactic:
ext h
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Rep k G
f g : (↑(coind' φ A) : Type (max u w))
hfg :
  ∀ (h : H),
    Eq (α := (↑A : Type (max u w)))
      (((Hom.hom f).toLinearMap : (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑A : Type (max u w)))
          (single h 1) :
        (↑A : Type (max u w)))
      (((Hom.hom g).toLinearMap : (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑A : Type (max u w)))
          (single h 1) :
        (↑A : Type (max u w)))
h : H
⊢ Eq (α := (↑A : Type (max u w))) (((Hom.hom f).toLinearMap ∘ₗ lsingle h : (a : k) → (↑A : Type (max u w))) 1)
    (((Hom.hom g).toLinearMap ∘ₗ lsingle h : (a : k) → (↑A : Type (max u w))) 1)

Tactic:
simpa using hfg h
-- Module: Mathlib.RepresentationTheory.Coinduced
Goal:
k : Type u
G : Type v
H : Type w
inst : CommRing k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A_1 : Rep k G
A B : Rep k G
f : A ⟶ B
h : H
h₁ :
  ∀ (x : res φ (leftRegular k H) ⟶ A) (h_1 : H),
    Eq (α := (↑B : Type (max u w)))
      ((Representation.IntertwiningMap.toLinearMap
              (Hom.hom
                (((Linear.rightComp k (res φ (leftRegular k H)) f ∘ₗ
                        (Representation.coind' φ A :
                            (a : H) → (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ A)
                          h :
                      (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ B) :
                    (a : res φ (leftRegular k H) ⟶ A) → res φ (leftRegular k H) ⟶ B)
                  x)) :
            (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑B : Type (max u w)))
          (single h_1 1) :
        (↑B : Type (max u w)))
      ((Representation.IntertwiningMap.toLinearMap
              (Hom.hom
                ((((Representation.coind' φ B :
                            (a : H) → (res φ (leftRegular k H) ⟶ B) →ₗ[k] res φ (leftRegular k H) ⟶ B)
                          h ∘ₗ
                        Linear.rightComp k (res φ (leftRegular k H)) f :
                      (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ B) :
                    (a : res φ (leftRegular k H) ⟶ A) → res φ (leftRegular k H) ⟶ B)
                  x)) :
            (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑B : Type (max u w)))
          (single h_1 1) :
        (↑B : Type (max u w)))
⊢ Eq (α := (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ B)
    (Linear.rightComp k (res φ (leftRegular k H)) f ∘ₗ
        (Representation.coind' φ A : (a : H) → (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ A) h :
      (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ B)
    ((Representation.coind' φ B : (a : H) → (res φ (leftRegular k H) ⟶ B) →ₗ[k] res φ (leftRegular k H) ⟶ B) h ∘ₗ
        Linear.rightComp k (res φ (leftRegular k H)) f :
      (res φ (leftRegular k H) ⟶ A) →ₗ[k] res φ (leftRegular k H) ⟶ B)

Tactic:
ext