awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Character
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
ρ : Representation k G V
σ : Representation k G W
φ : ρ.Equiv σ
g : G
⊢ ρ.character g = σ.character g

Tactic:
simp [character, ← φ.conj_apply_self]

Premises used: Representation.character, Representation.Equiv.conj_apply_self
-- Module: Mathlib.RepresentationTheory.Character
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
inst : Group G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
g h : G
rw : ρ.character (h⁻¹ * (h * g)) = ρ.character g
rw₁ rw₂ : ρ.character g = ρ.character g
⊢ ρ.character (h * g * h⁻¹) = ρ.character g

Tactic:
rw [char_mul_comm, inv_mul_cancel_left]

Premises used: inv_mul_cancel_left, Representation.char_mul_comm
-- Module: Mathlib.RepresentationTheory.Character
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
inst : Group G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
ρ : Representation k G V
g : G
⊢ ρ.dual.character (V := Dual k V) g = ρ.character g⁻¹

Tactic:
trace_transpose' (ρ g⁻¹)

Premises used: Representation.character, LinearMap.trace_transpose', Inv.inv, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Character
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
inst : Group G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
ρ : Representation k G V
inst_5 : Fintype G
inst_6 rw : Invertible (α := k) (↑(Nat.card G) : k)
⊢ Invertible (α := k) (↑(Fintype.card G) : k)

Tactic:
rw [Fintype.card_eq_nat_card]

Premises used: Fintype.card_eq_nat_card
-- Module: Mathlib.RepresentationTheory.Character
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
inst : Group G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
ρ : Representation k G V
inst_5 : Fintype G
inst_6 : Invertible (α := k) (↑(Nat.card G) : k)
⊢ Invertible (α := k) (↑(Nat.card G) : k)

Tactic:
assumption
-- Module: Mathlib.RepresentationTheory.Character
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
inst : Group G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
ρ : Representation k G V
inst_5 : Fintype G
inst_6 : Invertible (α := k) (↑(Nat.card G) : k)
have :
  ∀ (this : Invertible (α := k) (↑(Fintype.card G) : k)),
    HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, ρ.character g) = (↑(finrank.{u_2, u_3} k ↥ρ.invariants) : k)
⊢ HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, ρ.character g) = (↑(finrank.{u_2, u_3} k ↥ρ.invariants) : k)

Tactic:
have : Invertible (Fintype.card G : k) := by rw [Fintype.card_eq_nat_card]; assumption
-- Module: Mathlib.RepresentationTheory.Character
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
inst : Group G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
ρ : Representation k G V
inst_5 : Fintype G
inst_6 : Invertible (α := k) (↑(Nat.card G) : k)
this : Invertible (α := k) (↑(Fintype.card G) : k)
rw : HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, ρ.character g) = (trace k V : (a : V →ₗ[k] V) → k) ρ.averageMap
⊢ HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, ρ.character g) = (↑(finrank.{u_2, u_3} k ↥ρ.invariants) : k)

Tactic:
rw [← (isProj_averageMap ρ).trace]

Premises used: Representation.isProj_averageMap, LinearMap.IsProj.trace
-- Module: Mathlib.RepresentationTheory.Character
Goal:
G : Type u_1
k : Type u_2
V : Type u_3
inst : Group G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
ρ : Representation k G V
inst_5 : Fintype G
inst_6 : Invertible (α := k) (↑(Nat.card G) : k)
this : Invertible (α := k) (↑(Fintype.card G) : k)
⊢ HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, ρ.character g) = (trace k V : (a : V →ₗ[k] V) → k) ρ.averageMap

Tactic:
simp [character, GroupAlgebra.average, _root_.map_sum]

Premises used: GroupAlgebra.average, Representation.character, map_sum
-- Module: Mathlib.RepresentationTheory.Character
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)
simp_rw :
  HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ x : G, ρ.character x⁻¹ * σ.character x) =
    (↑(finrank k (ρ.IntertwiningMap σ)) : k)
simp_rw₁ :
  HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ x : G, (ρ.linHom σ).character x) =
    (↑(finrank k (ρ.IntertwiningMap σ)) : k)
simp_rw₂ : Eq.{u_2 + 1} (α := k) (↑(finrank k ↥(ρ.linHom σ).invariants) : k) (↑(finrank k (ρ.IntertwiningMap σ)) : k)
⊢ HMul.hMul (α := k) (↑(Nat.card G) : k)⁻¹ (∑ g : G, σ.character g * ρ.character g⁻¹) =
    (↑(finrank k (ρ.IntertwiningMap σ)) : k)

Tactic:
simp_rw [mul_comm, ← char_linHom, card_inv_mul_sum_char_eq_finrank,
    (invariantsEquivIntertwiningMap ρ σ).finrank_eq]

Premises used: Representation.card_inv_mul_sum_char_eq_finrank, LinearEquiv.finrank_eq, mul_comm, Representation.invariantsEquivIntertwiningMap, Representation.char_linHom
-- Module: Mathlib.RepresentationTheory.Character
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
inr :
  Nonempty (σ.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

Tactic:
cases isEmpty_or_nonempty (Equiv σ ρ)

Premises used: isEmpty_or_nonempty, Representation.Equiv
-- Module: Mathlib.RepresentationTheory.Character
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 ρ)
inl : Eq.{u_2 + 1} (α := k) (↑(finrank k (σ.IntertwiningMap ρ)) : k) (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

Tactic:
rw [card_inv_mul_sum_char_mul_char_eq_finrank]

Premises used: Representation.card_inv_mul_sum_char_mul_char_eq_finrank
-- Module: Mathlib.RepresentationTheory.Character
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 ρ)
⊢ Eq.{u_2 + 1} (α := k) (↑(finrank k (σ.IntertwiningMap ρ)) : k) (if Nonempty (σ.Equiv ρ) then 1 else 0)

Tactic:
simpa [finrank_eq_zero_of_subsingleton]

Premises used: Module.finrank_eq_zero_of_subsingleton
-- Module: Mathlib.RepresentationTheory.Character
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 ρ)
inr :
  ∀ (φ : σ.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

Tactic:
obtain φ : σ.Equiv ρ := Classical.choice inferInstance

Premises used: Classical.choice, inferInstance, Representation.Equiv
-- Module: Mathlib.RepresentationTheory.Character
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 ρ
inr : Eq.{u_2 + 1} (α := k) (↑(finrank.{u_2, u_3} k (ρ.IntertwiningMap ρ)) : k) (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

Tactic:
rw [char_iso φ, card_inv_mul_sum_char_mul_char_eq_finrank]

Premises used: Representation.char_iso, Representation.card_inv_mul_sum_char_mul_char_eq_finrank
-- Module: Mathlib.RepresentationTheory.Character
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 ρ
⊢ Eq.{u_2 + 1} (α := k) (↑(finrank.{u_2, u_3} k (ρ.IntertwiningMap ρ)) : k) (if Nonempty (σ.Equiv ρ) then 1 else 0)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Coinduced
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
a b : H → A
h :
  Membership.mem (γ := Set (H → A))
    {f : H → A |
      ∀ (g : G) (h : H),
        f (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) =
          (((σ : (a : G) → A →ₗ[k] A) g : A →ₗ[k] A) : (a : A) → A) (f h)}
    a
h_1 :
  Membership.mem (γ := Set (H → A))
    {f : H → A |
      ∀ (g : G) (h : H),
        f (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) =
          (((σ : (a : G) → A →ₗ[k] A) g : A →ₗ[k] A) : (a : A) → A) (f h)}
    b
x : G
x_1 : H
⊢ (a + b) (HMul.hMul (α := H) ((φ : (a : G) → H) x : H) x_1) =
    (((σ : (a : G) → A →ₗ[k] A) x : A →ₗ[k] A) : (a : A) → A) ((a + b) x_1)

Tactic:
simp_all
-- Module: Mathlib.RepresentationTheory.Coinduced
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
⊢ Membership.mem (γ := Set (H → A))
    {f : H → A |
      ∀ (g : G) (h : H),
        f (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) =
          (((σ : (a : G) → A →ₗ[k] A) g : A →ₗ[k] A) : (a : A) → A) (f h)}
    0

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Coinduced
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 : k
x_1 : H → A
h :
  Membership.mem (γ := Set (H → A))
    {f : H → A |
      ∀ (g : G) (h : H),
        f (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) =
          (((σ : (a : G) → A →ₗ[k] A) g : A →ₗ[k] A) : (a : A) → A) (f h)}
    x_1
⊢ Membership.mem (γ := Set (H → A))
    {f : H → A |
      ∀ (g : G) (h : H),
        f (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) =
          (((σ : (a : G) → A →ₗ[k] A) g : A →ₗ[k] A) : (a : A) → A) (f h)}
    (x • x_1)

Tactic:
simp_all
-- Module: Mathlib.RepresentationTheory.Coinduced
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
inst_3 : AddCommMonoid A
inst_4 : Module k A
σ : Representation k G A
f : H → A
⊢ f ∈ coindV φ σ ↔
    ∀ (g : G) (h : H),
      f (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) =
        (((σ : (a : G) → A →ₗ[k] A) g : A →ₗ[k] A) : (a : A) → A) (f h)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RepresentationTheory.Coinduced
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
h : H
x : H → B
hx : x ∈ coindV φ ρ
g : G
h₁ : H
⊢ Eq.{u_5 + 1} (α := B)
    ((LinearMap.funLeft k B fun (x : H) ↦ x * h : (a : H → B) → H → B) x
        (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h₁) :
      B)
    ((((ρ : (a : G) → B →ₗ[k] B) g : B →ₗ[k] B) : (a : B) → B)
        ((LinearMap.funLeft k B fun (x : H) ↦ x * h : (a : H → B) → H → B) x h₁ : B) :
      B)

Tactic:
simpa [mul_assoc] using hx g (h₁ * h)

Premises used: HMul.hMul, mul_assoc
-- Module: Mathlib.RepresentationTheory.Coinduced
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
h :
  ∀ (x : ↥(coindV φ ρ)) (x_1 : H),
    Eq.{u_5 + 1} (α := B)
      ((↑((LinearMap.restrict (LinearMap.funLeft k B fun (x : H) ↦ x * 1) ⋯ : (a : ↥(coindV φ ρ)) → ↥(coindV φ ρ)) x) :
          H → B)
        x_1)
      ((↑((1 : (a : ↥(coindV φ ρ)) → ↥(coindV φ ρ)) x) : H → B) x_1)
⊢ Eq (α := ↥(coindV φ ρ) →ₗ[k] ↥(coindV φ ρ)) (LinearMap.restrict (LinearMap.funLeft k B fun (x : H) ↦ x * 1) ⋯) 1

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Coinduced
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 : ↥(coindV φ ρ)
x_1 : H
⊢ Eq.{u_5 + 1} (α := B)
    ((↑((LinearMap.restrict (LinearMap.funLeft k B fun (x : H) ↦ x * 1) ⋯ : (a : ↥(coindV φ ρ)) → ↥(coindV φ ρ)) x) :
        H → B)
      x_1)
    ((↑((1 : (a : ↥(coindV φ ρ)) → ↥(coindV φ ρ)) x) : H → B) x_1)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Coinduced
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
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)) ⋯ :
                (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) ⋯)
                  (LinearMap.restrict (LinearMap.funLeft k B fun (x : H) ↦ x * x_1) ⋯) :
                (a : ↥(coindV φ ρ)) → ↥(coindV φ ρ))
              x_2) :
          H → B)
        x_3)
⊢ 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) ⋯)

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Coinduced
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
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)) ⋯ :
              (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) ⋯)
                (LinearMap.restrict (LinearMap.funLeft k B fun (x : H) ↦ x * x_1) ⋯) :
              (a : ↥(coindV φ ρ)) → ↥(coindV φ ρ))
            x_2) :
        H → B)
      x_3)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RepresentationTheory.Coinduced
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 φ σ
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)
⊢ Membership.mem (α := H → B) (coindV φ ρ) ((f.compLeft H : (a : H → A) → H → B) x : H → B)

Tactic:
simp only [mem_coindV, LinearMap.compLeft_apply, Function.comp_apply,
      IntertwiningMap.toLinearMap_apply] at h ⊢

Premises used: LinearMap.compLeft_apply, Representation.IntertwiningMap.toLinearMap_apply, Representation.mem_coindV, Function.comp_apply
-- Module: Mathlib.RepresentationTheory.Coinduced
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 :
  ∀ (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
h0 : H
⊢ Eq.{u_5 + 1} (α := B) ((f : (a : A) → B) (x (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h0)) : B)
    ((((ρ : (a : G) → B →ₗ[k] B) g : B →ₗ[k] B) : (a : B) → B) ((f : (a : A) → B) (x h0) : B) : B)

Tactic:
simpa [h] using LinearMap.ext_iff.1 (f.2 g) (x h0)

Premises used: LinearMap.ext_iff, Representation.IntertwiningMap.isIntertwining', Iff.mp
-- Module: Mathlib.RepresentationTheory.Coinduced
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
h₁ :
  ∀ (x : ↥(coindV φ σ)) (x_1 : H),
    Eq.{u_5 + 1} (α := B)
      ((↑(((f.compLeft H).restrict ⋯ ∘ₗ (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 ⋯ :
                (a : ↥(coindV φ σ)) → ↥(coindV φ ρ))
              x) :
          H → B)
        x_1)
⊢ 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 ⋯)

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Coinduced
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
x : ↥(coindV φ σ)
x_1 : H
⊢ Eq.{u_5 + 1} (α := B)
    ((↑(((f.compLeft H).restrict ⋯ ∘ₗ (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 ⋯ :
              (a : ↥(coindV φ σ)) → ↥(coindV φ ρ))
            x) :
        H → B)
      x_1)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Coinduced
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 : ↥(coindV φ σ)
⊢ Eq (α := H → B) ((↑((coindMap φ f : (a : ↥(coindV φ σ)) → ↥(coindV φ ρ)) x) : H → B) : H → B)
    ((f.compLeft H : (a : H → A) → H → B) (↑x : H → A) : H → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Coinduced
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 : ↥(coindV φ σ)
h : H
⊢ Eq.{u_5 + 1} (α := B) ((↑((coindMap φ f : (a : ↥(coindV φ σ)) → ↥(coindV φ ρ)) x) : H → B) h : B)
    ((f : (a : A) → B) ((↑x : H → A) h) : B)

Tactic:
rfl

Premises used: rfl
-- 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
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
⊢ ∃ (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 ‹_›

Premises used: Iff.mp, Rep.epi_iff_surjective