awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst : Group G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
inst_5 : AddCommGroup W
inst_6 : Module k W
inst_7 : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
inst_8 : Fintype G
inst_9 : Invertible (α := k) (↑(Nat.card G) : k)
inst_10 : IsAlgClosed k
inst_11 : ρ.IsIrreducible
inst_12 : σ.IsIrreducible
inl :
  IsEmpty (σ.Equiv ρ) →
    HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, ρ.character g * σ.character g⁻¹) =
      if Nonempty (σ.Equiv ρ) then 1 else 0
⊢ HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, ρ.character g * σ.character g⁻¹) =
    if Nonempty (σ.Equiv ρ) then 1 else 0
have inr : Nonempty (σ.Equiv ρ) →
  HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, ρ.character g * σ.character g⁻¹) =
    if Nonempty (σ.Equiv ρ) then 1 else 0
Tactic: cases isEmpty_or_nonempty (Equiv σ ρ)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst : Group G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
inst_5 : AddCommGroup W
inst_6 : Module k W
inst_7 : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
inst_8 : Fintype G
inst_9 : Invertible (α := k) (↑(Nat.card G) : k)
inst_10 : IsAlgClosed k
inst_11 : ρ.IsIrreducible
inst_12 : σ.IsIrreducible
h : IsEmpty (σ.Equiv ρ)
⊢ HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, ρ.character g * σ.character g⁻¹) =
    if Nonempty (σ.Equiv ρ) then 1 else 0
have inl : Eq.{u_2 + 1} (α := k) (↑(finrank k (σ.IntertwiningMap ρ)) : k) (if Nonempty (σ.Equiv ρ) then 1 else 0)
Tactic: rw [card_inv_mul_sum_char_mul_char_eq_finrank]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst : Group G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
inst_5 : AddCommGroup W
inst_6 : Module k W
inst_7 : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
inst_8 : Fintype G
inst_9 : Invertible (α := k) (↑(Nat.card G) : k)
inst_10 : IsAlgClosed k
inst_11 : ρ.IsIrreducible
inst_12 : σ.IsIrreducible
h : Nonempty (σ.Equiv ρ)
⊢ HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, ρ.character g * σ.character g⁻¹) =
    if Nonempty (σ.Equiv ρ) then 1 else 0
have inr : ∀ (φ : σ.Equiv ρ),
  HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, ρ.character g * σ.character g⁻¹) =
    if Nonempty (σ.Equiv ρ) then 1 else 0
Tactic: obtain φ : σ.Equiv ρ := Classical.choice inferInstance
-- Lean 4 proof step from Mathlib.RepresentationTheory.Character (goal)
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst : Group G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
inst_5 : AddCommGroup W
inst_6 : Module k W
inst_7 : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
inst_8 : Fintype G
inst_9 : Invertible (α := k) (↑(Nat.card G) : k)
inst_10 : IsAlgClosed k
inst_11 : ρ.IsIrreducible
inst_12 : σ.IsIrreducible
h : Nonempty (σ.Equiv ρ)
φ : σ.Equiv ρ
⊢ HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, ρ.character g * σ.character g⁻¹) =
    if Nonempty (σ.Equiv ρ) then 1 else 0
have inr : Eq.{u_2 + 1} (α := k) (↑(finrank.{u_2, u_3} k (ρ.IntertwiningMap ρ)) : k) (if Nonempty (σ.Equiv ρ) then 1 else 0)
Tactic: rw [char_iso φ, card_inv_mul_sum_char_mul_char_eq_finrank]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst_3 : AddCommMonoid A
inst_4 : Module k A
inst_5 : AddCommMonoid B
inst_6 : Module k B
σ : Representation k G A
ρ : Representation k G B
⊢ Eq (α := ↥(coindV φ ρ) →ₗ[k] ↥(coindV φ ρ)) (LinearMap.restrict (LinearMap.funLeft k B fun (x : H) ↦ x * 1) ⋯) 1
have h : ∀ (x : ↥(coindV φ ρ)) (x_1 : H),
  Eq.{u_5 + 1} (α := B)
    ((↑((LinearMap.restrict (LinearMap.funLeft k B fun (x : H) ↦ x * 1) sorry : (a : ↥(coindV φ ρ)) → ↥(coindV φ ρ)) x) :
        H → B)
      x_1)
    ((↑((1 : (a : ↥(coindV φ ρ)) → ↥(coindV φ ρ)) x) : H → B) x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst_3 : AddCommMonoid A
inst_4 : Module k A
inst_5 : AddCommMonoid B
inst_6 : Module k B
σ : Representation k G A
ρ : Representation k G B
x x_1 : H
⊢ LinearMap.restrict (LinearMap.funLeft k B fun (x_2 : H) ↦ x_2 * (x * x_1)) ⋯ =
    HMul.hMul (α := ↥(coindV φ ρ) →ₗ[k] ↥(coindV φ ρ))
      (LinearMap.restrict (LinearMap.funLeft k B fun (x_2 : H) ↦ x_2 * x) ⋯)
      (LinearMap.restrict (LinearMap.funLeft k B fun (x : H) ↦ x * x_1) ⋯)
have h : ∀ (x_2 : ↥(coindV φ ρ)) (x_3 : H),
  Eq.{u_5 + 1} (α := B)
    ((↑((LinearMap.restrict (LinearMap.funLeft k B fun (x_4 : H) ↦ x_4 * (x * x_1)) sorry :
              (a : ↥(coindV φ ρ)) → ↥(coindV φ ρ))
            x_2) :
        H → B)
      x_3)
    ((↑((HMul.hMul (α := ↥(coindV φ ρ) →ₗ[k] ↥(coindV φ ρ))
                (LinearMap.restrict (LinearMap.funLeft k B fun (x_4 : H) ↦ x_4 * x) sorry)
                (LinearMap.restrict (LinearMap.funLeft k B fun (x : H) ↦ x * x_1) sorry) :
              (a : ↥(coindV φ ρ)) → ↥(coindV φ ρ))
            x_2) :
        H → B)
      x_3)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst_3 : AddCommMonoid A
inst_4 : Module k A
inst_5 : AddCommMonoid B
inst_6 : Module k B
σ : Representation k G A
ρ : Representation k G B
f : σ.IntertwiningMap ρ
x : H → A
h : x ∈ coindV φ σ
⊢ Membership.mem (α := H → B) (coindV φ ρ) ((f.compLeft H : (a : H → A) → H → B) x : H → B)
have simp : ∀
  (h :
    ∀ (g : G) (h : H),
      x (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) =
        (((σ : (a : G) → A →ₗ[k] A) g : A →ₗ[k] A) : (a : A) → A) (x h))
  (g : G) (h : H),
  Eq.{u_5 + 1} (α := B) ((f : (a : A) → B) (x (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h)) : B)
    ((((ρ : (a : G) → B →ₗ[k] B) g : B →ₗ[k] B) : (a : B) → B) ((f : (a : A) → B) (x h) : B) : B)
Tactic: simp only [mem_coindV, LinearMap.compLeft_apply, Function.comp_apply,
      IntertwiningMap.toLinearMap_apply] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst_3 : AddCommMonoid A
inst_4 : Module k A
inst_5 : AddCommMonoid B
inst_6 : Module k B
σ : Representation k G A
ρ : Representation k G B
f : σ.IntertwiningMap ρ
h : H
⊢ Eq (α := ↥(coindV φ σ) →ₗ[k] ↥(coindV φ ρ))
    ((f.compLeft H).restrict ⋯ ∘ₗ (coind φ σ : (a : H) → ↥(coindV φ σ) →ₗ[k] ↥(coindV φ σ)) h)
    ((coind φ ρ : (a : H) → ↥(coindV φ ρ) →ₗ[k] ↥(coindV φ ρ)) h ∘ₗ (f.compLeft H).restrict ⋯)
have h₁ : ∀ (x : ↥(coindV φ σ)) (x_1 : H),
  Eq.{u_5 + 1} (α := B)
    ((↑(((f.compLeft H).restrict sorry ∘ₗ (coind φ σ : (a : H) → ↥(coindV φ σ) →ₗ[k] ↥(coindV φ σ)) h :
              (a : ↥(coindV φ σ)) → ↥(coindV φ ρ))
            x) :
        H → B)
      x_1)
    ((↑(((coind φ ρ : (a : H) → ↥(coindV φ ρ) →ₗ[k] ↥(coindV φ ρ)) h ∘ₗ (f.compLeft H).restrict sorry :
              (a : ↥(coindV φ σ)) → ↥(coindV φ ρ))
            x) :
        H → B)
      x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
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
⊢ ∃ (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
have choose! : ∀ (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),
  ∃ (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! s hs using (Rep.epi_iff_surjective f).1 ‹_›
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
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
⊢ ∃ (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
have 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
Tactic: choose! i hi using Quotient.mk'_surjective (α := G)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (hypothesis)
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))⁻¹) ⋯
⊢ ∃ (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
have hmk : ∀ (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))
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
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) = s * γ g
have a : (↑(γ ((↑s : G) * g)) : G) = (↑(s * γ g) : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (hypothesis)
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)
⊢ ∃ (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
have hγ : ∀ (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]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
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
have 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)
Tactic: refine ⟨⟨x, fun _ _ => ?_⟩, Subtype.ext <| funext fun g => ?_⟩
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
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)
⊢ ∃ (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
have 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 sorry)) :
        G → (↑Y : Type u_1))
      g =
    (↑y : G → (↑Y : Type u_1)) g
Tactic: refine ⟨⟨x, fun _ _ => ?_⟩, Subtype.ext <| funext fun g => ?_⟩
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
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
⊢ (↑((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
have 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
Tactic: simp only [coindFunctor_obj, coindFunctor_map, hom_ofHom,
        Representation.coindMap_coe_apply_apply, hom_comm_apply, x]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
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
⊢ 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
have 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' := sorry, map_smul' := sorry :
                      (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: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
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)))
⊢ Hom.hom f = Hom.hom g
have h : (Hom.hom f).toLinearMap = (Hom.hom g).toLinearMap
Tactic: ext1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Coinduced (goal)
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)))
⊢ (Hom.hom f).toLinearMap = (Hom.hom g).toLinearMap
have 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)
Tactic: ext h