awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
ι : Type u_6
s : Finset ι
f : ι → ρ.IntertwiningMap σ
empty :
  Eq (α := V →ₗ[A] W) (toLinearMap.{u_1, u_2, u_3, u_4} (G := G) (ρ := ρ) (σ := σ) (∑ i ∈ ∅, f i))
    (∑ i ∈ ∅, (f i).toLinearMap)
insert :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (ih :
      Eq (α := V →ₗ[A] W) (toLinearMap.{u_1, u_2, u_3, u_4} (G := G) (ρ := ρ) (σ := σ) (∑ i ∈ s, f i))
        (∑ i ∈ s, (f i).toLinearMap)),
    Eq (α := V →ₗ[A] W) (toLinearMap.{u_1, u_2, u_3, u_4} (G := G) (ρ := ρ) (σ := σ) (∑ i ∈ Insert.insert i s, f i))
      (∑ i ∈ Insert.insert i s, (f i).toLinearMap)
⊢ Eq (α := V →ₗ[A] W) (toLinearMap.{u_1, u_2, u_3, u_4} (G := G) (ρ := ρ) (σ := σ) (∑ i ∈ s, f i))
    (∑ i ∈ s, (f i).toLinearMap)

Tactic:
classical induction s using Finset.induction with
  | empty => simp
  | insert i s hi ih => simp [Finset.sum_insert hi, ih]

Premises used: Insert.insert
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
ι : Type u_6
s : Finset ι
f : ι → ρ.IntertwiningMap σ
v : V
⊢ Eq.{u_4 + 1} (α := W) ((∑ i ∈ s, f i : (a : V) → W) v : W) (∑ i ∈ s, (f i : (a : V) → W) v : W)

Tactic:
simp [← toLinearMap_apply _ _ (∑ _ ∈ s, _), toLinearMap_sum, LinearMap.sum_apply]

Premises used: Representation.IntertwiningMap.toLinearMap_sum, Representation.IntertwiningMap.toLinearMap_apply, LinearMap.sum_apply, Finset.sum
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V_1 : Type u_3
W_1 : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V_1
inst_3 : AddCommMonoid W_1
inst_4 : AddCommMonoid U
inst_5 : Module A V_1
inst_6 : Module A W_1
inst_7 : Module A U
ρ_1 : Representation A G V_1
σ_1 : Representation A G W_1
τ_1 : Representation A G U
f_1 : V_1 →ₗ[A] W_1
V : Type u_6
W : Type u_7
P : Type u_8
inst_8 : AddCommMonoid V
inst_9 : AddCommGroup W
inst_10 : AddCommGroup P
inst_11 : Module A V
inst_12 : Module A W
inst_13 : Module A P
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G P
f_2 : V →ₗ[A] W
f : ρ.IntertwiningMap σ
⊢ ∀ (g : G), (-f.toLinearMap) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ (-f.toLinearMap)

Tactic:
simp [LinearMap.neg_comp, f.2]

Premises used: Representation.IntertwiningMap.isIntertwining', LinearMap.neg_comp
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
inst : Semiring A
inst_1 : Monoid G
V : Type u_6
W : Type u_7
inst_2 : AddCommMonoid V
inst_3 : AddCommGroup W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
f : ρ.IntertwiningMap σ
⊢ Eq (α := (a : V) → W) (⇑(-f) : (a : V) → W) (-(⇑f : (a : V) → W))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V_1 : Type u_3
W_1 : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V_1
inst_3 : AddCommMonoid W_1
inst_4 : AddCommMonoid U
inst_5 : Module A V_1
inst_6 : Module A W_1
inst_7 : Module A U
ρ_1 : Representation A G V_1
σ_1 : Representation A G W_1
τ_1 : Representation A G U
f_1 : V_1 →ₗ[A] W_1
V : Type u_6
W : Type u_7
P : Type u_8
inst_8 : AddCommMonoid V
inst_9 : AddCommGroup W
inst_10 : AddCommGroup P
inst_11 : Module A V
inst_12 : Module A W
inst_13 : Module A P
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G P
f_2 : V →ₗ[A] W
f g : ρ.IntertwiningMap σ
⊢ ∀ (g_1 : G),
    (f.toLinearMap - g.toLinearMap) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g_1 =
      (σ : (a : G) → W →ₗ[A] W) g_1 ∘ₗ (f.toLinearMap - g.toLinearMap)

Tactic:
simp [LinearMap.sub_comp, LinearMap.comp_sub, f.2, g.2]

Premises used: LinearMap.sub_comp, Representation.IntertwiningMap.isIntertwining', LinearMap.comp_sub
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
inst : Semiring A
inst_1 : Monoid G
V : Type u_6
W : Type u_7
inst_2 : AddCommMonoid V
inst_3 : AddCommGroup W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
f g : ρ.IntertwiningMap σ
⊢ (⇑(f - g) : (a : V) → W) = HSub.hSub (α := (a : V) → W) (⇑f : (a : V) → W) (⇑g : (a : V) → W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
inst : Semiring A
inst_1 : Monoid G
V : Type u_6
W : Type u_7
inst_2 : AddCommMonoid V
inst_3 : AddCommGroup W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
f g : ρ.IntertwiningMap σ
⊢ (f - g).toLinearMap = f.toLinearMap - g.toLinearMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V_1 : Type u_3
W_1 : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V_1
inst_3 : AddCommMonoid W_1
inst_4 : AddCommMonoid U
inst_5 : Module A V_1
inst_6 : Module A W_1
inst_7 : Module A U
ρ_1 : Representation A G V_1
σ_1 : Representation A G W_1
τ_1 : Representation A G U
f_1 : V_1 →ₗ[A] W_1
V : Type u_6
W : Type u_7
P : Type u_8
inst_8 : AddCommMonoid V
inst_9 : AddCommGroup W
inst_10 : AddCommGroup P
inst_11 : Module A V
inst_12 : Module A W
inst_13 : Module A P
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G P
f_2 : V →ₗ[A] W
z : ℤ
f : ρ.IntertwiningMap σ
⊢ ∀ (g : G), (z • f.toLinearMap) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ (z • f.toLinearMap)

Tactic:
simp [LinearMap.smul_comp, LinearMap.comp_smul, f.2]

Premises used: LinearMap.smul_comp, Representation.IntertwiningMap.isIntertwining', LinearMap.comp_smul
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
inst : Semiring A
inst_1 : Monoid G
V : Type u_6
W : Type u_7
inst_2 : AddCommMonoid V
inst_3 : AddCommGroup W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
f : ρ.IntertwiningMap σ
z : ℤ
⊢ (⇑(z • f) : (a : V) → W) = HSMul.hSMul (β := (a : V) → W) z (⇑f : (a : V) → W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
⊢ ∀ (g : G),
    Eq.{u_3 + 1} (α := V →ₗ[A] V) (LinearMap.id ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g)
      ((ρ : (a : G) → V →ₗ[A] V) g ∘ₗ LinearMap.id)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module A V
ρ : Representation A G V
⊢ (id ρ).toLinearMap = LinearMap.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module A V
ρ : Representation A G V
v : V
⊢ (id ρ : (a : V) → V) v = v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f_1 : V →ₗ[A] W
f : σ.IntertwiningMap τ
g : ρ.IntertwiningMap σ
⊢ ∀ (g_1 : G),
    (f.toLinearMap ∘ₗ g.toLinearMap) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g_1 =
      (τ : (a : G) → U →ₗ[A] U) g_1 ∘ₗ f.toLinearMap ∘ₗ g.toLinearMap

Tactic:
simp [LinearMap.comp_assoc, g.2, f.isIntertwining_assoc]

Premises used: LinearMap.comp_assoc, Representation.IntertwiningMap.isIntertwining', Representation.IntertwiningMap.isIntertwining_assoc
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : σ.IntertwiningMap τ
g : ρ.IntertwiningMap σ
⊢ (f.comp g).toLinearMap = f.toLinearMap ∘ₗ g.toLinearMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : σ.IntertwiningMap τ
g : ρ.IntertwiningMap σ
v : V
⊢ Eq.{u_5 + 1} (α := U) ((f.comp g : (a : V) → U) v : U) ((f : (a : W) → U) ((g : (a : V) → W) v : W) : U)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f₁ f₂ : σ.IntertwiningMap τ
g : ρ.IntertwiningMap σ
h : ((f₁ + f₂).comp g).toLinearMap = (f₁.comp g + f₂.comp g).toLinearMap
⊢ (f₁ + f₂).comp g = f₁.comp g + f₂.comp g

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f₁ f₂ : σ.IntertwiningMap τ
g : ρ.IntertwiningMap σ
⊢ ((f₁ + f₂).comp g).toLinearMap = (f₁.comp g + f₂.comp g).toLinearMap

Tactic:
simp [LinearMap.add_comp]

Premises used: LinearMap.add_comp
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : σ.IntertwiningMap τ
g₁ g₂ : ρ.IntertwiningMap σ
h : (f.comp (g₁ + g₂)).toLinearMap = (f.comp g₁ + f.comp g₂).toLinearMap
⊢ f.comp (g₁ + g₂) = f.comp g₁ + f.comp g₂

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : σ.IntertwiningMap τ
g₁ g₂ : ρ.IntertwiningMap σ
⊢ (f.comp (g₁ + g₂)).toLinearMap = (f.comp g₁ + f.comp g₂).toLinearMap

Tactic:
simp [LinearMap.comp_add]

Premises used: LinearMap.comp_add
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
e : V ≃ₗ[A] W
he : ∀ (g : G), (↑e : V →ₗ[A] W) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑e : V →ₗ[A] W)
⊢ (mk e he).toLinearEquiv = e

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
e : V ≃ₗ[A] W
he : ∀ (g : G), (↑e : V →ₗ[A] W) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑e : V →ₗ[A] W)
⊢ (↑(mk e he) : ρ.IntertwiningMap σ) = { toLinearMap := (↑e : V →ₗ[A] W), isIntertwining' := he }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
e : V ≃ₗ[A] W
he : ∀ (g : G), (↑e : V →ₗ[A] W) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑e : V →ₗ[A] W)
⊢ (↑(mk e he) : ρ.IntertwiningMap σ).toLinearMap = (↑e : V →ₗ[A] W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
φ ψ : σ.Equiv ρ
h : φ.toLinearEquiv = ψ.toLinearEquiv
mk' :
  ∀ (toIntertwiningMap : σ.IntertwiningMap ρ) (invFun : V → W)
    (left_inv : Function.LeftInverse invFun toIntertwiningMap.toFun)
    (right_inv : Function.RightInverse invFun toIntertwiningMap.toFun)
    (h :
      { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
            σ.Equiv ρ }.toLinearEquiv =
        ψ.toLinearEquiv),
    { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
        σ.Equiv ρ } =
      ψ
⊢ φ = ψ

Tactic:
cases φ
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
ψ : σ.Equiv ρ
toIntertwiningMap : σ.IntertwiningMap ρ
invFun : V → W
left_inv : Function.LeftInverse invFun toIntertwiningMap.toFun
right_inv : Function.RightInverse invFun toIntertwiningMap.toFun
h :
  { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
        σ.Equiv ρ }.toLinearEquiv =
    ψ.toLinearEquiv
mk' :
  ∀ (toIntertwiningMap_1 : σ.IntertwiningMap ρ) (invFun_1 : V → W)
    (left_inv_1 : Function.LeftInverse invFun_1 toIntertwiningMap_1.toFun)
    (right_inv_1 : Function.RightInverse invFun_1 toIntertwiningMap_1.toFun)
    (h :
      { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
            σ.Equiv ρ }.toLinearEquiv =
        { toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := left_inv_1,
            right_inv := right_inv_1 : σ.Equiv ρ }.toLinearEquiv),
    { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
        σ.Equiv ρ } =
      { toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }
⊢ { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
      σ.Equiv ρ } =
    ψ

Tactic:
cases ψ
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
toIntertwiningMap : σ.IntertwiningMap ρ
invFun : V → W
left_inv : Function.LeftInverse invFun toIntertwiningMap.toFun
right_inv : Function.RightInverse invFun toIntertwiningMap.toFun
toIntertwiningMap_1 : σ.IntertwiningMap ρ
invFun_1 : V → W
left_inv_1 : Function.LeftInverse invFun_1 toIntertwiningMap_1.toFun
right_inv_1 : Function.RightInverse invFun_1 toIntertwiningMap_1.toFun
h :
  { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
        σ.Equiv ρ }.toLinearEquiv =
    { toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 :
        σ.Equiv ρ }.toLinearEquiv
⊢ { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
      σ.Equiv ρ } =
    { toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }

Tactic:
simpa [IntertwiningMap.ext_iff] using h

Premises used: Representation.IntertwiningMap.ext_iff
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
φ ψ : σ.Equiv ρ
⊢ φ.toLinearEquiv = ψ.toLinearEquiv ↔ φ = ψ

Tactic:
toLinearEquiv_injective.eq_iff

Premises used: Function.Injective.eq_iff, Representation.Equiv.toLinearEquiv_injective
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
φ_1 φ ψ : ρ.Equiv σ
h1 : Eq (α := V → W) (⇑φ.toLinearEquiv : (a : V) → W) (⇑ψ.toLinearEquiv : (a : V) → W)
h2 : φ.invFun = ψ.invFun
mk' :
  ∀ (toIntertwiningMap : ρ.IntertwiningMap σ) (invFun : W → V)
    (left_inv : Function.LeftInverse invFun toIntertwiningMap.toFun)
    (right_inv : Function.RightInverse invFun toIntertwiningMap.toFun)
    (h1 :
      Eq (α := V → W)
        (⇑{ toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
                ρ.Equiv σ }.toLinearEquiv :
          (a : V) → W)
        (⇑ψ.toLinearEquiv : (a : V) → W))
    (h2 :
      { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
            ρ.Equiv σ }.invFun =
        ψ.invFun),
    { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
        ρ.Equiv σ } =
      ψ
⊢ φ = ψ

Tactic:
cases φ
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
φ ψ : ρ.Equiv σ
toIntertwiningMap : ρ.IntertwiningMap σ
invFun : W → V
left_inv : Function.LeftInverse invFun toIntertwiningMap.toFun
right_inv : Function.RightInverse invFun toIntertwiningMap.toFun
h1 :
  Eq (α := V → W)
    (⇑{ toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
            ρ.Equiv σ }.toLinearEquiv :
      (a : V) → W)
    (⇑ψ.toLinearEquiv : (a : V) → W)
h2 :
  { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
        ρ.Equiv σ }.invFun =
    ψ.invFun
mk' :
  ∀ (toIntertwiningMap_1 : ρ.IntertwiningMap σ) (invFun_1 : W → V)
    (left_inv_1 : Function.LeftInverse invFun_1 toIntertwiningMap_1.toFun)
    (right_inv_1 : Function.RightInverse invFun_1 toIntertwiningMap_1.toFun)
    (h1 :
      Eq (α := V → W)
        (⇑{ toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
                ρ.Equiv σ }.toLinearEquiv :
          (a : V) → W)
        (⇑{ toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := left_inv_1,
                right_inv := right_inv_1 : ρ.Equiv σ }.toLinearEquiv :
          (a : V) → W))
    (h2 :
      { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
            ρ.Equiv σ }.invFun =
        { toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := left_inv_1,
            right_inv := right_inv_1 : ρ.Equiv σ }.invFun),
    { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
        ρ.Equiv σ } =
      { toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }
⊢ { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
      ρ.Equiv σ } =
    ψ

Tactic:
cases ψ
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
φ : ρ.Equiv σ
toIntertwiningMap : ρ.IntertwiningMap σ
invFun : W → V
left_inv : Function.LeftInverse invFun toIntertwiningMap.toFun
right_inv : Function.RightInverse invFun toIntertwiningMap.toFun
toIntertwiningMap_1 : ρ.IntertwiningMap σ
invFun_1 : W → V
left_inv_1 : Function.LeftInverse invFun_1 toIntertwiningMap_1.toFun
right_inv_1 : Function.RightInverse invFun_1 toIntertwiningMap_1.toFun
h1 :
  Eq (α := V → W)
    (⇑{ toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
            ρ.Equiv σ }.toLinearEquiv :
      (a : V) → W)
    (⇑{ toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 :
            ρ.Equiv σ }.toLinearEquiv :
      (a : V) → W)
h2 :
  { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
        ρ.Equiv σ }.invFun =
    { toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 :
        ρ.Equiv σ }.invFun
⊢ { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
      ρ.Equiv σ } =
    { toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }

Tactic:
simp_all [IntertwiningMap.ext_iff]

Premises used: Representation.IntertwiningMap.ext_iff
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
e : V ≃ₗ[A] W
he : ∀ (g : G), (↑e : V →ₗ[A] W) ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g = (σ : (a : G) → W →ₗ[A] W) g ∘ₗ (↑e : V →ₗ[A] W)
v : V
⊢ Eq.{u_4 + 1} (α := W) ((mk e he : (a : V) → W) v : W) ((e : (a : V) → W) v : W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
φ ψ : ρ.Equiv σ
h : Eq (α := (a : V) → W) (⇑φ : (a : V) → W) (⇑ψ : (a : V) → W)
mk' :
  ∀ (toIntertwiningMap : ρ.IntertwiningMap σ) (invFun : W → V)
    (left_inv : Function.LeftInverse invFun toIntertwiningMap.toFun)
    (right_inv : Function.RightInverse invFun toIntertwiningMap.toFun)
    (h :
      Eq (α := (a : V) → W)
        (⇑{ toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
              ρ.Equiv σ } :
          (a : V) → W)
        (⇑ψ : (a : V) → W)),
    { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
        ρ.Equiv σ } =
      ψ
⊢ φ = ψ

Tactic:
cases φ