awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)))

Tactic:
simp
-- 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 : ↥(Representation.coindV φ A.ρ)
g : G
h :
  ∀ (a : H),
    Eq (α := (↑A : Type (max u w)))
      (((linearCombination k (↑f : H → (↑A : Type (max u w))) ∘ₗ
              (Representation.ofMulAction k H H : (a : H) → (H →₀ k) →ₗ[k] H →₀ k) ((φ : (a : G) → H) g)) ∘ₗ
            lsingle a :
          (a : k) → (↑A : Type (max u w)))
        1)
      ((((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g ∘ₗ
              linearCombination k (↑f : H → (↑A : Type (max u w)))) ∘ₗ
            lsingle a :
          (a : k) → (↑A : Type (max u w)))
        1)
⊢ Eq (α := (H →₀ k) →ₗ[k] (↑A : Type (max u w)))
    (linearCombination k (↑f : H → (↑A : Type (max u w))) ∘ₗ
      (Representation.ofMulAction k H H : (a : H) → (H →₀ k) →ₗ[k] H →₀ k) ((φ : (a : G) → H) g))
    ((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g ∘ₗ
      linearCombination k (↑f : H → (↑A : Type (max u w))))

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
f : ↥(Representation.coindV φ A.ρ)
g : G
a : H
⊢ Eq (α := (↑A : Type (max u w)))
    (((linearCombination k (↑f : H → (↑A : Type (max u w))) ∘ₗ
            (Representation.ofMulAction k H H : (a : H) → (H →₀ k) →ₗ[k] H →₀ k) ((φ : (a : G) → H) g)) ∘ₗ
          lsingle a :
        (a : k) → (↑A : Type (max u w)))
      1)
    ((((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g ∘ₗ
            linearCombination k (↑f : H → (↑A : Type (max u w)))) ∘ₗ
          lsingle a :
        (a : k) → (↑A : Type (max u w)))
      1)

Tactic:
simp [f.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
x x_1 : ↥(Representation.coindV φ A.ρ)
⊢ ∀ (h : H),
    Eq (α := (↑(of A.ρ) : Type (max u w)))
      ((Representation.IntertwiningMap.toLinearMap
              (Hom.hom
                (ofHom
                  { toLinearMap := linearCombination k (↑(x + x_1) : H → (↑A : Type (max u w))), isIntertwining' := ⋯ :
                    Representation.IntertwiningMap (V := (↑(leftRegular k H) : Type (max u w)))
                      (MonoidHom.comp (ρ (leftRegular k H)) φ) A.ρ })) :
            (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑(of A.ρ) : Type (max u w)))
          (single h 1) :
        (↑(of A.ρ) : Type (max u w)))
      (((Hom.hom
                (HAdd.hAdd (α := res φ (leftRegular k H) ⟶ A)
                  (ofHom
                    { toLinearMap := linearCombination k (↑x : H → (↑A : Type (max u w))), isIntertwining' := ⋯ :
                      Representation.IntertwiningMap (V := (↑(leftRegular k H) : Type (max u w)))
                        (MonoidHom.comp (ρ (leftRegular k H)) φ) A.ρ })
                  (ofHom
                    { toLinearMap := linearCombination k (↑x_1 : H → (↑A : Type (max u w))), isIntertwining' := ⋯ :
                      Representation.IntertwiningMap (V := (↑(leftRegular k H) : Type (max u w)))
                        (MonoidHom.comp (ρ (leftRegular k H)) φ) A.ρ }))).toLinearMap :
            (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑(of A.ρ) : Type (max u w)))
          (single h 1) :
        (↑(of A.ρ) : Type (max u w)))

Tactic:
simp [Rep.add_hom]

Premises used: Rep.add_hom
-- 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 : k
x_1 : ↥(Representation.coindV φ A.ρ)
⊢ ∀ (h : H),
    Eq (α := (↑(of A.ρ) : Type (max u w)))
      ((Representation.IntertwiningMap.toLinearMap
              (Hom.hom
                (ofHom
                  { toLinearMap := linearCombination k (↑(x • x_1) : H → (↑A : Type (max u w))), isIntertwining' := ⋯ :
                    Representation.IntertwiningMap (V := (↑(leftRegular k H) : Type (max u w)))
                      (MonoidHom.comp (ρ (leftRegular k H)) φ) A.ρ })) :
            (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑(of A.ρ) : Type (max u w)))
          (single h 1) :
        (↑(of A.ρ) : Type (max u w)))
      (((Hom.hom
                (HSMul.hSMul (α := k) (β := res φ (leftRegular k H) ⟶ A) ((RingHom.id k : (a : k) → k) x : k)
                  (ofHom
                    { toLinearMap := linearCombination k (↑x_1 : H → (↑A : Type (max u w))), isIntertwining' := ⋯ :
                      Representation.IntertwiningMap (V := (↑(leftRegular k H) : Type (max u w)))
                        (MonoidHom.comp (ρ (leftRegular k H)) φ) A.ρ }))).toLinearMap :
            (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑(of A.ρ) : Type (max u w)))
          (single h 1) :
        (↑(of A.ρ) : Type (max u w)))

Tactic:
simp [smul_hom]

Premises used: Rep.smul_hom
-- 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 : res φ (leftRegular k H) ⟶ A
g : G
h : H
simp :
  Eq (α := (↑A : Type (max u w)))
    ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) 1) :
      (↑A : Type (max u w)))
    ((((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g :
            (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) :
          (a : (↑A : Type (max u w))) → (↑A : Type (max u w)))
        ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single h 1)) :
      (↑A : Type (max u w)))
⊢ Eq (α := (↑A : Type (max u w)))
    ((fun (h : H) ↦
        (((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))))
      (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h))
    ((((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g :
          (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) :
        (a : (↑A : Type (max u w))) → (↑A : Type (max u w)))
      ((fun (h : H) ↦
          (((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))))
        h))

Tactic:
simp only [res_obj_V, res_obj_ρ, Representation.IntertwiningMap.toLinearMap_apply]

Premises used: Representation.IntertwiningMap.toLinearMap_apply, Rep.res_obj_ρ, Rep.res_obj_V
-- 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 : res φ (leftRegular k H) ⟶ A
g : G
h : H
⊢ Eq (α := (↑A : Type (max u w)))
    ((((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g :
            (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) :
          (a : (↑A : Type (max u w))) → (↑A : Type (max u w)))
        ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single h 1)) :
      (↑A : Type (max u w)))
    ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) 1) :
      (↑A : Type (max u w)))

Tactic:
simpa using (hom_comm_apply f g (.single h 1)).symm

Premises used: Rep.hom_comm_apply, OfNat.ofNat, Eq.symm, Finsupp.single
-- 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 : res φ (leftRegular k H) ⟶ A
g : G
h : H
⊢ Eq (α := (↑A : Type (max u w)))
    ((((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g :
            (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) :
          (a : (↑A : Type (max u w))) → (↑A : Type (max u w)))
        ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single h 1)) :
      (↑A : Type (max u w)))
    ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) 1) :
      (↑A : Type (max u w)))

Tactic:
have := by simpa using (hom_comm_apply f g (.single h 1)).symm
-- 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 : res φ (leftRegular k H) ⟶ A
g : G
h : H
this :
  Eq (α := (↑A : Type (max u w)))
    ((((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g :
            (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) :
          (a : (↑A : Type (max u w))) → (↑A : Type (max u w)))
        ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single h 1)) :
      (↑A : Type (max u w)))
    ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) 1) :
      (↑A : Type (max u w)))
rw rw₁ :
  Eq (α := (↑A : Type (max u w)))
    ((((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g :
            (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) :
          (a : (↑A : Type (max u w))) → (↑A : Type (max u w)))
        ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single h 1)) :
      (↑A : Type (max u w)))
    ((((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g :
            (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) :
          (a : (↑A : Type (max u w))) → (↑A : Type (max u w)))
        ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single h 1)) :
      (↑A : Type (max u w)))
⊢ Eq (α := (↑A : Type (max u w)))
    ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) 1) :
      (↑A : Type (max u w)))
    ((((A.ρ : (a : G) → (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) g :
            (↑A : Type (max u w)) →ₗ[k] (↑A : Type (max u w))) :
          (a : (↑A : Type (max u w))) → (↑A : Type (max u w)))
        ((Hom.hom f : (a : H →₀ k) → (↑A : Type (max u w))) (single h 1)) :
      (↑A : Type (max u w)))

Tactic:
rw [← this]
-- 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 : ↥(Representation.coindV φ A.ρ)
⊢ (fun (f : res φ (leftRegular k H) ⟶ A) ↦
        (Subtype.mk (p := fun (x : H → (↑A : Type (max u w))) ↦ x ∈ Representation.coindV φ A.ρ)
            (fun (h : H) ↦
              ((Hom.hom f).toLinearMap : (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑A : Type (max u w)))
                (single h 1))
            ⋯ :
          ↥(Representation.coindV φ A.ρ)))
      ((fun (f : ↥(Representation.coindV φ A.ρ)) ↦
          (ofHom { toLinearMap := linearCombination k (↑f : H → (↑A : Type (max u w))), isIntertwining' := ⋯ } :
            of (X := (↑(leftRegular k H) : Type (max u w))) (MonoidHom.comp (ρ (leftRegular k H)) φ) ⟶ of A.ρ))
        x) =
    x

Tactic:
simp
-- 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
x_1 : H
⊢ Eq (α := (↑(of A.ρ) : Type (max u w)))
    ((Representation.IntertwiningMap.toLinearMap
            (Hom.hom
              ((fun (f : ↥(Representation.coindV φ A.ρ)) ↦
                  (ofHom
                      { toLinearMap := linearCombination k (↑f : H → (↑A : Type (max u w))), isIntertwining' := ⋯ :
                        Representation.IntertwiningMap (V := (↑(leftRegular k H) : Type (max u w)))
                          (MonoidHom.comp (ρ (leftRegular k H)) φ) A.ρ } :
                    of (X := (↑(leftRegular k H) : Type (max u w))) (MonoidHom.comp (ρ (leftRegular k H)) φ) ⟶ of A.ρ))
                ((fun (f : res φ (leftRegular k H) ⟶ A) ↦
                    (Subtype.mk (p := fun (x : H → (↑A : Type (max u w))) ↦ x ∈ Representation.coindV φ A.ρ)
                        (fun (h : H) ↦
                          ((Hom.hom f).toLinearMap :
                              (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑A : Type (max u w)))
                            (single h 1))
                        ⋯ :
                      ↥(Representation.coindV φ A.ρ)))
                  x))) :
          (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑(of A.ρ) : Type (max u w)))
        (single x_1 1) :
      (↑(of A.ρ) : Type (max u w)))
    (((Hom.hom x).toLinearMap : (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑(of A.ρ) : Type (max u w)))
        (single x_1 1) :
      (↑(of A.ρ) : Type (max u w)))

Tactic:
simp
-- 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 Y : Rep k G
x : X ⟶ Y
hf :
  ∀ (x_1 : (↑(Functor.obj (coindFunctor k φ) X) : Type (max u w))),
    Eq (α := (↑(Functor.obj (coindFunctor' k φ) Y) : Type (max u w)))
      (((Hom.hom (CategoryTheory.Functor.map (coindFunctor k φ) x ≫ (coindIso φ Y).hom)).toLinearMap :
            (a : (↑((coindFunctor k φ).obj X) : Type (max u w))) → (↑((coindFunctor' k φ).obj Y) : Type (max u w)))
          x_1 :
        (↑(Functor.obj (coindFunctor' k φ) Y) : Type (max u w)))
      ((Representation.IntertwiningMap.toLinearMap
              (Hom.hom ((coindIso φ X).hom ≫ CategoryTheory.Functor.map (coindFunctor' k φ) x)) :
            (a : (↑((coindFunctor k φ).obj X) : Type (max u w))) → (↑((coindFunctor' k φ).obj Y) : Type (max u w)))
          x_1 :
        (↑(Functor.obj (coindFunctor' k φ) Y) : Type (max u w)))
⊢ CategoryTheory.Functor.map (coindFunctor k φ) x ≫ (coindIso φ Y).hom =
    (coindIso φ X).hom ≫ CategoryTheory.Functor.map (coindFunctor' k φ) x

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 Y : Rep k G
x : X ⟶ Y
x_1 : (↑(Functor.obj (coindFunctor k φ) X) : Type (max u w))
x_2 : H
⊢ Eq (α := (↑Y : Type (max u w)))
    ((Representation.IntertwiningMap.toLinearMap
            (Hom.hom
              (((Hom.hom (CategoryTheory.Functor.map (coindFunctor k φ) x ≫ (coindIso φ Y).hom)).toLinearMap :
                  (a : (↑((coindFunctor k φ).obj X) : Type (max u w))) →
                    (↑((coindFunctor' k φ).obj Y) : Type (max u w)))
                x_1)) :
          (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑Y : Type (max u w)))
        (single x_2 1) :
      (↑Y : Type (max u w)))
    ((Representation.IntertwiningMap.toLinearMap
            (Hom.hom
              ((Representation.IntertwiningMap.toLinearMap
                    (Hom.hom ((coindIso φ X).hom ≫ CategoryTheory.Functor.map (coindFunctor' k φ) x)) :
                  (a : (↑((coindFunctor k φ).obj X) : Type (max u w))) →
                    (↑((coindFunctor' k φ).obj Y) : Type (max u w)))
                x_1)) :
          (a : (↑(res φ (leftRegular k H)) : Type (max u w))) → (↑Y : Type (max u w)))
        (single x_2 1) :
      (↑Y : Type (max u w)))

Tactic:
simp [coindIso, coindMap']

Premises used: Rep.coindIso, Rep.coindMap'
-- 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 Y : Rep k G
x : X ⟶ Y
x_1 : (↑(Functor.obj (coindFunctor k φ) X) : Type (max u w))
⊢ Eq (α := (↑(Functor.obj (coindFunctor' k φ) Y) : Type (max u w)))
    (((Hom.hom (CategoryTheory.Functor.map (coindFunctor k φ) x ≫ (coindIso φ Y).hom)).toLinearMap :
          (a : (↑((coindFunctor k φ).obj X) : Type (max u w))) → (↑((coindFunctor' k φ).obj Y) : Type (max u w)))
        x_1 :
      (↑(Functor.obj (coindFunctor' k φ) Y) : Type (max u w)))
    ((Representation.IntertwiningMap.toLinearMap
            (Hom.hom ((coindIso φ X).hom ≫ CategoryTheory.Functor.map (coindFunctor' k φ) x)) :
          (a : (↑((coindFunctor k φ).obj X) : Type (max u w))) → (↑((coindFunctor' k φ).obj Y) : Type (max u w)))
        x_1 :
      (↑(Functor.obj (coindFunctor' k φ) Y) : Type (max u w)))

Tactic:
exact coind'_ext _ fun _ ↦ by simp [coindIso, coindMap']

Premises used: Rep.coind'_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_1 : Rep k G
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
x : (↑B : Type (max w u_1))
x_1 : G
x_2 : H
⊢ Eq (α := (↑A : Type (max u_1 w)))
    ((LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
            (Hom.hom f).toLinearMap ∘ₗ (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h :
          (a : (↑B : Type (max w u_1))) → (i : H) → (↑A : Type (max w u_1)))
        x (HMul.hMul (α := H) ((φ : (a : G) → H) x_1 : H) x_2) :
      (↑A : Type (max w u_1)))
    ((((A.ρ : (a : G) → (↑A : Type (max u_1 w)) →ₗ[k] (↑A : Type (max u_1 w))) x_1 :
            (↑A : Type (max u_1 w)) →ₗ[k] (↑A : Type (max u_1 w))) :
          (a : (↑A : Type (max u_1 w))) → (↑A : Type (max u_1 w)))
        ((LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
              (Hom.hom f).toLinearMap ∘ₗ (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h :
            (a : (↑B : Type (max w u_1))) → (i : H) → (↑A : Type (max w u_1)))
          x x_2) :
      (↑A : Type (max u_1 w)))

Tactic:
simpa using hom_comm_apply f _ _

Premises used: Rep.hom_comm_apply
-- 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
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
g : H
dsimp :
  Eq (α := (↑B : Type (max w u_1)) →ₗ[k] ↥(Representation.coindV φ A.ρ))
    (LinearMap.codRestrict (Representation.coindV φ A.ρ)
        (LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
          (Hom.hom f).toLinearMap ∘ₗ (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h)
        ⋯ ∘ₗ
      (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) g)
    (LinearMap.restrict (LinearMap.funLeft k (↑A : Type (max u_1 w)) fun (x : H) ↦ x * g) ⋯ ∘ₗ
      LinearMap.codRestrict (Representation.coindV φ A.ρ)
        (LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
          (Hom.hom f).toLinearMap ∘ₗ (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h)
        ⋯)
⊢ Eq (α := (↑B : Type (max w u_1)) →ₗ[k] ↥(Representation.coindV φ A.ρ))
    (LinearMap.codRestrict (Representation.coindV φ A.ρ)
        (LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
          (Hom.hom f).toLinearMap ∘ₗ (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h)
        ⋯ ∘ₗ
      (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) g)
    ((Representation.coind φ A.ρ : (a : H) → ↥(Representation.coindV φ A.ρ) →ₗ[k] ↥(Representation.coindV φ A.ρ)) g ∘ₗ
      LinearMap.codRestrict (Representation.coindV φ A.ρ)
        (LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
          (Hom.hom f).toLinearMap ∘ₗ (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h)
        ⋯)

Tactic:
dsimp
-- 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
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
g : H
h :
  ∀ (x : (↑B : Type (max w u_1))) (x_1 : H),
    Eq (α := (↑A : Type (max u_1 w)))
      ((↑((LinearMap.codRestrict (Representation.coindV φ A.ρ)
                    (LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
                      (Hom.hom f).toLinearMap ∘ₗ
                        (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h)
                    ⋯ ∘ₗ
                  (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) g :
                (a : (↑B : Type (max w u_1))) → ↥(Representation.coindV φ A.ρ))
              x) :
          H → (↑A : Type (max u_1 w)))
        x_1)
      ((↑((LinearMap.restrict (LinearMap.funLeft k (↑A : Type (max u_1 w)) fun (x : H) ↦ x * g) ⋯ ∘ₗ
                  LinearMap.codRestrict (Representation.coindV φ A.ρ)
                    (LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
                      (Hom.hom f).toLinearMap ∘ₗ
                        (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h)
                    ⋯ :
                (a : (↑B : Type (max w u_1))) → ↥(Representation.coindV φ A.ρ))
              x) :
          H → (↑A : Type (max u_1 w)))
        x_1)
⊢ Eq (α := (↑B : Type (max w u_1)) →ₗ[k] ↥(Representation.coindV φ A.ρ))
    (LinearMap.codRestrict (Representation.coindV φ A.ρ)
        (LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
          (Hom.hom f).toLinearMap ∘ₗ (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h)
        ⋯ ∘ₗ
      (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) g)
    (LinearMap.restrict (LinearMap.funLeft k (↑A : Type (max u_1 w)) fun (x : H) ↦ x * g) ⋯ ∘ₗ
      LinearMap.codRestrict (Representation.coindV φ A.ρ)
        (LinearMap.pi (φ := fun (h : H) ↦ (↑A : Type (max w u_1))) fun (h : H) ↦
          (Hom.hom f).toLinearMap ∘ₗ (B.ρ : (a : H) → (↑B : Type (max w u_1)) →ₗ[k] (↑B : Type (max w u_1))) h)
        ⋯)

Tactic:
ext