awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
j : ℕ
rw :
  Eq (α :=
    Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (j + 1))
      (HomologicalComplex.X (standardComplex k G) j))
    (CategoryStruct.comp (Y := HomologicalComplex.X (standardComplex k G) (j + 1))
      (Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          (j + 1)))
      (HomologicalComplex.d (standardComplex k G) (j + 1) j))
    (d k G j ≫
      Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          j))
rw₁ :
  Eq (α :=
    Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (j + 1))
      (HomologicalComplex.X (standardComplex k G) j))
    (Iso.inv (diagonalSuccIsoFree k G (j + 1)) ≫ HomologicalComplex.d (standardComplex k G) (j + 1) j)
    (d k G j ≫
      Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          j))
⊢ Eq (α :=
    Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (j + 1))
      (HomologicalComplex.X (standardComplex k G) j))
    (CategoryStruct.comp (Y := HomologicalComplex.X (standardComplex k G) (j + 1))
      (Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          (j + 1)))
      (HomologicalComplex.d (standardComplex k G) (j + 1) j))
    (HomologicalComplex.d (barComplex k G) (j + 1) j ≫
      Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          j))
have rw₂ : Eq (α :=
  Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (j + 1))
    (HomologicalComplex.X (standardComplex k G) j))
  (Iso.inv (diagonalSuccIsoFree k G (j + 1)) ≫ HomologicalComplex.d (standardComplex k G) (j + 1) j)
  (d k G j ≫ Iso.inv (diagonalSuccIsoFree k G j))
Tactic: rw [d_def, Iso.symm_hom, Iso.symm_hom, d_comp_diagonalSuccIsoFree_inv_eq]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
j : ℕ
rw :
  Eq (α :=
    Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (j + 1))
      (HomologicalComplex.X (standardComplex k G) j))
    (CategoryStruct.comp (Y := HomologicalComplex.X (standardComplex k G) (j + 1))
      (Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          (j + 1)))
      (HomologicalComplex.d (standardComplex k G) (j + 1) j))
    (d k G j ≫
      Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          j))
rw₁ :
  Eq (α :=
    Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (j + 1))
      (HomologicalComplex.X (standardComplex k G) j))
    (Iso.inv (diagonalSuccIsoFree k G (j + 1)) ≫ HomologicalComplex.d (standardComplex k G) (j + 1) j)
    (d k G j ≫
      Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          j))
rw₂ :
  Eq (α :=
    Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (j + 1))
      (HomologicalComplex.X (standardComplex k G) j))
    (Iso.inv (diagonalSuccIsoFree k G (j + 1)) ≫ HomologicalComplex.d (standardComplex k G) (j + 1) j)
    (d k G j ≫ Iso.inv (diagonalSuccIsoFree k G j))
⊢ Eq (α :=
    Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (j + 1))
      (HomologicalComplex.X (standardComplex k G) j))
    (CategoryStruct.comp (Y := HomologicalComplex.X (standardComplex k G) (j + 1))
      (Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          (j + 1)))
      (HomologicalComplex.d (standardComplex k G) (j + 1) j))
    (HomologicalComplex.d (barComplex k G) (j + 1) j ≫
      Iso.hom
        ((fun (i : ℕ) ↦
            (Iso.symm (diagonalSuccIsoFree k G i) : Iso (C := Rep k G) (free k G (Fin i → G)) (diagonal k G (i + 1))))
          j))
have rw₃ : Eq (α :=
  Quiver.Hom (V := Rep k G) (HomologicalComplex.X (barComplex k G) (j + 1))
    (HomologicalComplex.X (standardComplex k G) j))
  (Iso.inv (diagonalSuccIsoFree k G (j + 1)) ≫ HomologicalComplex.d (standardComplex k G) (j + 1) j)
  (Iso.inv (diagonalSuccIsoFree k G (j + 1)) ≫ HomologicalComplex.d (standardComplex k G) (j + 1) j)
Tactic: rw [d_def, Iso.symm_hom, Iso.symm_hom, d_comp_diagonalSuccIsoFree_inv_eq]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Induced (goal)
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst_3 : AddCommGroup A
inst_4 : Module k A
ρ : Representation k G A
inst_5 : AddCommGroup B
inst_6 : Module k B
τ : Representation k G B
h : H
x : G
⊢ Eq (α := TensorProduct k (H →₀ k) A →ₗ[k] TensorProduct k (H →₀ k) A)
    (LinearMap.rTensor A (lmapDomain k k fun (x : H) ↦ x * h⁻¹) ∘ₗ
      (tprod (MonoidHom.comp (leftRegular k H) φ) ρ :
          (a : G) → TensorProduct k (H →₀ k) A →ₗ[k] TensorProduct k (H →₀ k) A)
        x)
    ((tprod (MonoidHom.comp (leftRegular k H) φ) ρ :
          (a : G) → TensorProduct k (H →₀ k) A →ₗ[k] TensorProduct k (H →₀ k) A)
        x ∘ₗ
      LinearMap.rTensor A (lmapDomain k k fun (x : H) ↦ x * h⁻¹))
have a : ∀ (a : H) (x_1 : A),
  Eq (α := TensorProduct k (H →₀ k) A)
    ((((TensorProduct.AlgebraTensorModule.curry
                    (LinearMap.rTensor A (lmapDomain k k fun (x : H) ↦ x * h⁻¹) ∘ₗ
                      (tprod (MonoidHom.comp (leftRegular k H) φ) ρ :
                          (a : G) → TensorProduct k (H →₀ k) A →ₗ[k] TensorProduct k (H →₀ k) A)
                        x) ∘ₗ
                  lsingle a :
                k →ₗ[k] A →ₗ[k] TensorProduct k (H →₀ k) A) :
              (a : k) → A →ₗ[k] TensorProduct k (H →₀ k) A)
            1 :
          (a : A) → TensorProduct k (H →₀ k) A)
        x_1 :
      TensorProduct k (H →₀ k) A)
    ((((TensorProduct.AlgebraTensorModule.curry
                    ((tprod (MonoidHom.comp (leftRegular k H) φ) ρ :
                          (a : G) → TensorProduct k (H →₀ k) A →ₗ[k] TensorProduct k (H →₀ k) A)
                        x ∘ₗ
                      LinearMap.rTensor A (lmapDomain k k fun (x : H) ↦ x * h⁻¹)) ∘ₗ
                  lsingle a :
                k →ₗ[k] A →ₗ[k] TensorProduct k (H →₀ k) A) :
              (a : k) → A →ₗ[k] TensorProduct k (H →₀ k) A)
            1 :
          (a : A) → TensorProduct k (H →₀ k) A)
        x_1 :
      TensorProduct k (H →₀ k) A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Induced (goal)
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst_3 : AddCommGroup A
inst_4 : Module k A
ρ : Representation k G A
inst_5 : AddCommGroup B
inst_6 : Module k B
τ : Representation k G B
⊢ Eq (α := IndV φ ρ →ₗ[k] IndV φ ρ)
    (Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
      { toLinearMap := LinearMap.rTensor A (lmapDomain k k fun (x : H) ↦ x * 1⁻¹), isIntertwining' := ⋯ })
    1
have H₁ : ∀ (a : H) (x : A),
  Eq (α :=
    (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants (k := k) (G := G) (V := TensorProduct k (H →₀ k) A))
    ((((TensorProduct.AlgebraTensorModule.curry
                    (Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                        (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                        { toLinearMap := LinearMap.rTensor A (lmapDomain k k fun (x : H) ↦ x * 1⁻¹),
                          isIntertwining' := sorry } ∘ₗ
                      Coinvariants.mk (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)) ∘ₗ
                  lsingle a :
                k →ₗ[k]
                  A →ₗ[k]
                    (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants (k := k) (G := G) (V :=
                      TensorProduct k (H →₀ k) A)) :
              (a : k) → A →ₗ[k] (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants)
            1 :
          (a : A) → (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants)
        x :
      (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants (k := k) (G := G) (V := TensorProduct k (H →₀ k) A))
    ((((TensorProduct.AlgebraTensorModule.curry (1 ∘ₗ Coinvariants.mk (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)) ∘ₗ
                  lsingle a :
                k →ₗ[k]
                  A →ₗ[k]
                    (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants (k := k) (G := G) (V :=
                      TensorProduct k (H →₀ k) A)) :
              (a : k) → A →ₗ[k] (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants)
            1 :
          (a : A) → (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants)
        x :
      (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).Coinvariants (k := k) (G := G) (V := TensorProduct k (H →₀ k) A))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Induced (goal)
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst_3 : AddCommGroup A
inst_4 : Module k A
ρ : Representation k G A
inst_5 : AddCommGroup B
inst_6 : Module k B
τ : Representation k G B
x x_1 : H
⊢ Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
      { toLinearMap := LinearMap.rTensor A (lmapDomain k k fun (x_2 : H) ↦ x_2 * (x * x_1)⁻¹), isIntertwining' := ⋯ } =
    HMul.hMul (α := IndV φ ρ →ₗ[k] IndV φ ρ)
      (Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
        { toLinearMap := LinearMap.rTensor A (lmapDomain k k fun (x_2 : H) ↦ x_2 * x⁻¹), isIntertwining' := ⋯ :
          (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).IntertwiningMap
            (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) })
      (Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
        { toLinearMap := LinearMap.rTensor A (lmapDomain k k fun (x : H) ↦ x * x_1⁻¹), isIntertwining' := ⋯ :
          (tprod (MonoidHom.comp (leftRegular k H) φ) ρ).IntertwiningMap
            (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) })
have H₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Induced (goal)
Goal:
k : Type u
G : Type v
H : Type v'
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A_1 : Rep.{w, u, v} k G
A B : Rep.{u_1, u, v} k G
f : A ⟶ B
g : H
⊢ Eq (α := Representation.IndV φ A.ρ →ₗ[k] Representation.IndV φ B.ρ)
    (Representation.Coinvariants.map (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
        (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) B.ρ)
        { toLinearMap := LinearMap.lTensor (H →₀ k) (Hom.hom f).toLinearMap, isIntertwining' := ⋯ } ∘ₗ
      (Representation.ind φ A.ρ : (a : H) → Representation.IndV φ A.ρ →ₗ[k] Representation.IndV φ A.ρ) g)
    ((Representation.ind φ B.ρ : (a : H) → Representation.IndV φ B.ρ →ₗ[k] Representation.IndV φ B.ρ) g ∘ₗ
      Representation.Coinvariants.map (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
        (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) B.ρ)
        { toLinearMap := LinearMap.lTensor (H →₀ k) (Hom.hom f).toLinearMap, isIntertwining' := ⋯ })
have H₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Induced (goal)
Goal:
k : Type u
G : Type v
H : Type v'
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A x : Rep.{w, u, v} k G
⊢ indMap φ (𝟙 x) = 𝟙 (ind φ x)
have hf : ∀ (a : H) (x_1 : (↑x : Type w)),
  Eq (α := (↑(ind φ x) : Type (max (max u v') w)))
    ((((TensorProduct.AlgebraTensorModule.curry
                    ((Hom.hom (indMap φ (𝟙 x))).toLinearMap ∘ₗ
                      Representation.Coinvariants.mk
                        (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) x.ρ)) ∘ₗ
                  lsingle a :
                k →ₗ[k] (↑x : Type w) →ₗ[k] (↑(ind φ x) : Type (max (max u v') w))) :
              (a : k) → (↑x : Type w) →ₗ[k] (↑(ind φ x) : Type (max (max u v') w)))
            1 :
          (a : (↑x : Type w)) → (↑(ind φ x) : Type (max (max u v') w)))
        x_1 :
      (↑(ind φ x) : Type (max (max u v') w)))
    ((((TensorProduct.AlgebraTensorModule.curry
                    ((Hom.hom (𝟙 (ind φ x))).toLinearMap ∘ₗ
                      Representation.Coinvariants.mk
                        (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) x.ρ)) ∘ₗ
                  lsingle a :
                k →ₗ[k] (↑x : Type w) →ₗ[k] (↑(ind φ x) : Type (max (max u v') w))) :
              (a : k) → (↑x : Type w) →ₗ[k] (↑(ind φ x) : Type (max (max u v') w)))
            1 :
          (a : (↑x : Type w)) → (↑(ind φ x) : Type (max (max u v') w)))
        x_1 :
      (↑(ind φ x) : Type (max (max u v') w)))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Induced (goal)
Goal:
k : Type u
G : Type v
H : Type v'
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A X Y Z : Rep.{w, u, v} k G
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ indMap φ (x ≫ x_1) = indMap φ x ≫ indMap φ x_1
have hf : ∀ (a : H) (x_2 : (↑X : Type w)),
  Eq (α := (↑(ind φ Z) : Type (max (max u v') w)))
    ((((TensorProduct.AlgebraTensorModule.curry
                    ((Hom.hom (indMap φ (x ≫ x_1))).toLinearMap ∘ₗ
                      Representation.Coinvariants.mk
                        (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) X.ρ)) ∘ₗ
                  lsingle a :
                k →ₗ[k] (↑X : Type w) →ₗ[k] (↑(ind φ Z) : Type (max (max u v') w))) :
              (a : k) → (↑X : Type w) →ₗ[k] (↑(ind φ Z) : Type (max (max u v') w)))
            1 :
          (a : (↑X : Type w)) → (↑(ind φ Z) : Type (max (max u v') w)))
        x_2 :
      (↑(ind φ Z) : Type (max (max u v') w)))
    ((((TensorProduct.AlgebraTensorModule.curry
                    ((Hom.hom (indMap φ x ≫ indMap φ x_1)).toLinearMap ∘ₗ
                      Representation.Coinvariants.mk
                        (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) X.ρ)) ∘ₗ
                  lsingle a :
                k →ₗ[k] (↑X : Type w) →ₗ[k] (↑(ind φ Z) : Type (max (max u v') w))) :
              (a : k) → (↑X : Type w) →ₗ[k] (↑(ind φ Z) : Type (max (max u v') w)))
            1 :
          (a : (↑X : Type w)) → (↑(ind φ Z) : Type (max (max u v') w)))
        x_2 :
      (↑(ind φ Z) : Type (max (max u v') w)))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Induced (goal)
Goal:
k : Type u
G : Type v
H : Type v'
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A_1 : Rep.{w, u, v} k G
B_1 : Rep k H
A : Rep k G
B : Rep k H
f : ind φ A ⟶ B
g : G
⊢ ((Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
      (A.ρ : (a : G) → (↑A : Type (max (max u v') w)) →ₗ[k] (↑A : Type (max (max u v') w))) g =
    (MonoidHom.comp B.ρ φ : (a : G) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) g ∘ₗ
      (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1
have h : ∀ (x : (↑A : Type (max (max u v') w))),
  Eq (α := (↑B : Type (max (max u v') w)))
    ((((Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
            (A.ρ : (a : G) → (↑A : Type (max (max u v') w)) →ₗ[k] (↑A : Type (max (max u v') w))) g :
          (a : (↑A : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
        x :
      (↑B : Type (max (max u v') w)))
    (((MonoidHom.comp B.ρ φ : (a : G) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) g ∘ₗ
            (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1 :
          (a : (↑A : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
        x :
      (↑B : Type (max (max u v') w)))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Induced (hypothesis)
Goal:
k : Type u
G : Type v
H : Type v'
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A_1 : Rep.{w, u, v} k G
B_1 : Rep k H
A : Rep k G
B : Rep k H
f : ind φ A ⟶ B
g : G
x : (↑A : Type (max (max u v') w))
⊢ Eq (α := (↑B : Type (max (max u v') w)))
    ((((Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
            (A.ρ : (a : G) → (↑A : Type (max (max u v') w)) →ₗ[k] (↑A : Type (max (max u v') w))) g :
          (a : (↑A : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
        x :
      (↑B : Type (max (max u v') w)))
    (((MonoidHom.comp B.ρ φ : (a : G) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) g ∘ₗ
            (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1 :
          (a : (↑A : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
        x :
      (↑B : Type (max (max u v') w)))
have this : Eq (α := (↑B : Type (max (max u v') w)))
  ((((B.ρ : (a : H) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) ((φ : (a : G) → H) g) :
          (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) :
        (a : (↑B : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
      ((Hom.hom f : (a : (↑(ind φ A) : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
        ((IndV.mk φ A.ρ 1 : (a : (↑A : Type (max (max u v') w))) → IndV φ A.ρ) x)) :
    (↑B : Type (max (max u v') w)))
  ((Hom.hom f : (a : (↑(ind φ A) : Type (max (max u v') w))) → (↑B : Type (max (max u v') w)))
      (((((ind φ A).ρ : (a : H) → (↑(ind φ A) : Type (max (max u v') w)) →ₗ[k] (↑(ind φ A) : Type (max (max u v') w)))
              ((φ : (a : G) → H) g) :
            (↑(ind φ A) : Type (max (max u v') w)) →ₗ[k] (↑(ind φ A) : Type (max (max u v') w))) :
          (a : (↑(ind φ A) : Type (max (max u v') w))) → (↑(ind φ A) : Type (max (max u v') w)))
        ((IndV.mk φ A.ρ 1 : (a : (↑A : Type (max (max u v') w))) → IndV φ A.ρ) x)) :
    (↑B : Type (max (max u v') w)))
Tactic: have := (hom_comm_apply f (φ g) (IndV.mk φ A.ρ 1 x)).symm
-- Lean 4 proof step from Mathlib.RepresentationTheory.Induced (goal)
Goal:
k : Type u
G : Type v
H : Type v'
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
φ : G →* H
A_1 : Rep.{w, u, v} k G
B_1 : Rep k H
A : Rep k G
B : Rep k H
f : A ⟶ res φ B
g : G
⊢ Eq (α := TensorProduct k (H →₀ k) (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
    (TensorProduct.lift
        ((lift ((↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) k H :
            (a : H → (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) →
              (H →₀ k) →ₗ[k] (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
          fun (h : H) ↦
          (B.ρ : (a : H) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) h⁻¹ ∘ₗ
            (Hom.hom f).toLinearMap) ∘ₗ
      (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ :
          (a : G) →
            TensorProduct k (H →₀ k) (↑A : Type (max (max u v') w)) →ₗ[k]
              TensorProduct k (H →₀ k) (↑A : Type (max (max u v') w)))
        g)
    (TensorProduct.lift
      ((lift ((↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) k H :
          (a : H → (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) →
            (H →₀ k) →ₗ[k] (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
        fun (h : H) ↦
        (B.ρ : (a : H) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) h⁻¹ ∘ₗ
          (Hom.hom f).toLinearMap))
have simp : Eq (α := TensorProduct k (H →₀ k) (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
  (TensorProduct.lift
    (LinearMap.compl₂ (R₂ := k) (N := (↑A : Type (max (max u v') w))) (σ₂₃ := RingHom.id k) (σ₄₂ := RingHom.id k)
      (((lift ((↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) k H :
            (a : H → (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) →
              (H →₀ k) →ₗ[k] (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
          fun (h : H) ↦
          (B.ρ : (a : H) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) h⁻¹ ∘ₗ
            (Hom.hom f).toLinearMap) ∘ₗ
        (Representation.leftRegular k H : (a : H) → (H →₀ k) →ₗ[k] H →₀ k) ((φ : (a : G) → H) g))
      ((A.ρ : (a : G) → (↑A : Type (max (max u v') w)) →ₗ[k] (↑A : Type (max (max u v') w))) g)))
  (TensorProduct.lift
    ((lift ((↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) k H :
        (a : H → (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) →
          (H →₀ k) →ₗ[k] (↑A : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w)))
      fun (h : H) ↦
      (B.ρ : (a : H) → (↑B : Type (max (max u v') w)) →ₗ[k] (↑B : Type (max (max u v') w))) h⁻¹ ∘ₗ
        (Hom.hom f).toLinearMap))
Tactic: simp only [res_obj_ρ, tprod_apply, MonoidHom.coe_comp, Function.comp_apply,
        TensorProduct.lift_comp_map]