awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
ρ : ContRepresentation R G V
⊢ (↑(refl ρ) : ρ →ⁱL ρ) = ContIntertwiningMap.id

Tactic:
rfl

Premises used: ContinuousLinearMap.id, ContIntertwiningMap.id, rfl
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
ρ : ContRepresentation R G V
⊢ (↑(refl ρ).toContinuousLinearEquiv : V →L[R] V) = ContinuousLinearMap.id R V

Tactic:
rfl

Premises used: ContinuousLinearMap.id, rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
ρ : ContRepresentation R G V
v : V
⊢ (refl ρ : (a : V) → V) v = v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ : ρ.Equiv σ
⊢ Eq (α := (a : V) → W) (⇑(↑φ : ρ →ⁱL σ) : (a : V) → W) (⇑φ : (a : V) → W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ : ρ.Equiv σ
⊢ Eq (α := (a : V) → W) (⇑(↑φ.toContinuousLinearEquiv : V →L[R] W) : (a : V) → W) (⇑φ : (a : V) → W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ : ρ.Equiv σ
⊢ (↑φ.toContinuousLinearEquiv : V ≃ₗ[R] W).invFun = (⇑φ.symm : (a : W) → V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ : ρ.Equiv σ
⊢ (↑φ.toContinuousLinearEquiv : V →L[R] W) = (↑φ : ρ →ⁱL σ).toContinuousLinearMap

Tactic:
rfl

Premises used: rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ : ρ.Equiv σ
v : V
⊢ Eq.{u_4 + 1} (α := W) ((φ.toContinuousLinearEquiv : (a : V) → W) v : W) (((↑φ : ρ →ⁱL σ) : (a : V) → W) v : W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
inst_10 : AddCommGroup U
inst_11 : Module R U
inst_12 : TopologicalSpace U
inst_13 : IsTopologicalAddGroup U
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
τ : ContRepresentation R G U
φ : ρ.Equiv σ
g : G
rw :
  ((↑φ.toContinuousLinearEquiv : V →L[R] W) ∘SL (↑φ.symm : W →L[R] V)).comp (σ₁₂ := RingHom.id R)
      ((σ : (a : G) → W →L[R] W) g) =
    (↑φ.toContinuousLinearEquiv : V →L[R] W).comp (σ₁₂ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g) ∘SL
      (↑φ.symm : W →L[R] V)
⊢ (↑φ.symm : W →L[R] V).comp (σ₁₂ := RingHom.id R) ((σ : (a : G) → W →L[R] W) g) =
    comp (σ₂₃ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g) (↑φ.symm : W →L[R] V)

Tactic:
rw [← cancel_left' (g := φ.toContinuousLinearEquiv.toContinuousLinearMap)
    φ.toContinuousLinearEquiv.injective, ← comp_assoc, ← comp_assoc]

Premises used: ContinuousLinearMap.cancel_left', ContRepresentation.Equiv.toContinuousLinearEquiv, ContinuousLinearEquiv.injective, ContinuousLinearMap.comp_assoc
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
inst_10 : AddCommGroup U
inst_11 : Module R U
inst_12 : TopologicalSpace U
inst_13 : IsTopologicalAddGroup U
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
τ : ContRepresentation R G U
φ : ρ.Equiv σ
g : G
⊢ ((↑φ.toContinuousLinearEquiv : V →L[R] W) ∘SL (↑φ.symm : W →L[R] V)).comp (σ₁₂ := RingHom.id R)
      ((σ : (a : G) → W →L[R] W) g) =
    (↑φ.toContinuousLinearEquiv : V →L[R] W).comp (σ₁₂ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g) ∘SL
      (↑φ.symm : W →L[R] V)

Tactic:
simp [φ.isIntertwining g, comp_assoc]

Premises used: ContRepresentation.Equiv.isIntertwining, ContinuousLinearMap.comp_assoc
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
e : V ≃L[R] W
he :
  ∀ (g : G),
    (↑e : V →L[R] W).comp (σ₁₂ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g) =
      comp (σ₂₃ := RingHom.id R) ((σ : (a : G) → W →L[R] W) g) (↑e : V →L[R] W)
g : G
⊢ (↑e.symm : W →L[R] V).comp (σ₁₂ := RingHom.id R) ((σ : (a : G) → W →L[R] W) g) =
    comp (σ₂₃ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g) (↑e.symm : W →L[R] V)

Tactic:
(mk e he).symm.isIntertwining g

Premises used: ContRepresentation.Equiv.isIntertwining, ContinuousLinearEquiv.symm, ContRepresentation.Equiv.mk, ContRepresentation.Equiv.symm
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
e : V ≃L[R] W
he :
  ∀ (g : G),
    (↑e : V →L[R] W).comp (σ₁₂ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g) =
      comp (σ₂₃ := RingHom.id R) ((σ : (a : G) → W →L[R] W) g) (↑e : V →L[R] W)
⊢ (mk e he).symm = mk e.symm ⋯

Tactic:
rfl

Premises used: ContRepresentation.Equiv.symm, rfl
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ : ρ.Equiv σ
⊢ (↑(↑φ.symm.toContinuousLinearEquiv : W ≃ₗ[R] V) : W →ₗ[R] V) =
    (↑(↑φ.toContinuousLinearEquiv : V ≃ₗ[R] W).symm : W →ₗ[R] V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ : ρ.Equiv σ
⊢ Eq (α := (a : W) → V) (⇑(↑φ.toContinuousLinearEquiv : V ≃ₗ[R] W).symm : (a : W) → V) (⇑φ.symm : (a : W) → V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
inst_10 : AddCommGroup U
inst_11 : Module R U
inst_12 : TopologicalSpace U
inst_13 : IsTopologicalAddGroup U
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
τ : ContRepresentation R G U
φ_1 φ : ρ.Equiv σ
ψ : σ.Equiv τ
g : G
rw :
  ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W)).comp (σ₁₂ := RingHom.id R)
      ((ρ : (a : G) → V →L[R] V) g) =
    comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g)
      ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W))
rw₁ :
  (↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL
      (↑φ.toContinuousLinearEquiv : V →L[R] W).comp (σ₁₂ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g) =
    comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g)
      ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W))
rw₂ :
  (↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL
      comp (σ₂₃ := RingHom.id R) ((σ : (a : G) → W →L[R] W) g) (↑φ.toContinuousLinearEquiv : V →L[R] W) =
    comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g)
      ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W))
rw₃ :
  (↑ψ.toContinuousLinearEquiv : W →L[R] U).comp (σ₁₂ := RingHom.id R) ((σ : (a : G) → W →L[R] W) g) ∘SL
      (↑φ.toContinuousLinearEquiv : V →L[R] W) =
    comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g)
      ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W))
rw₄ :
  Eq (α := V →L[R] U)
    (comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g) (↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL
      (↑φ.toContinuousLinearEquiv : V →L[R] W))
    (comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g)
      ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W)))
rw₅ rw₆ :
  Eq (α := V →L[R] U)
    (comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g)
      ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W)))
    (comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g)
      ((↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W)))
⊢ (↑(φ.trans ψ.toContinuousLinearEquiv) : V →L[R] U).comp (σ₁₂ := RingHom.id R) ((ρ : (a : G) → V →L[R] V) g) =
    comp (σ₂₃ := RingHom.id R) ((τ : (a : G) → U →L[R] U) g) (↑(φ.trans ψ.toContinuousLinearEquiv) : V →L[R] U)

Tactic:
rw [← ContinuousLinearEquiv.comp_coe, comp_assoc,
    φ.isIntertwining, ← comp_assoc, ψ.isIntertwining, comp_assoc]

Premises used: ContRepresentation.Equiv.isIntertwining, ContinuousLinearEquiv.comp_coe, ContinuousLinearMap.comp_assoc
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
inst_10 : AddCommGroup U
inst_11 : Module R U
inst_12 : TopologicalSpace U
inst_13 : IsTopologicalAddGroup U
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
τ : ContRepresentation R G U
φ : ρ.Equiv σ
ψ : σ.Equiv τ
⊢ (↑(φ.trans ψ) : ρ →ⁱL τ) = (↑ψ : σ →ⁱL τ).comp (↑φ : ρ →ⁱL σ)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, ContIntertwiningMap.comp, rfl
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
inst_10 : AddCommGroup U
inst_11 : Module R U
inst_12 : TopologicalSpace U
inst_13 : IsTopologicalAddGroup U
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
τ : ContRepresentation R G U
φ : ρ.Equiv σ
ψ : σ.Equiv τ
⊢ (↑(φ.trans ψ).toContinuousLinearEquiv : V →L[R] U) =
    (↑ψ.toContinuousLinearEquiv : W →L[R] U) ∘SL (↑φ.toContinuousLinearEquiv : V →L[R] W)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
inst_10 : AddCommGroup U
inst_11 : Module R U
inst_12 : TopologicalSpace U
inst_13 : IsTopologicalAddGroup U
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
τ : ContRepresentation R G U
φ : ρ.Equiv σ
ψ : σ.Equiv τ
v : V
⊢ Eq.{u_5 + 1} (α := U) ((φ.trans ψ : (a : V) → U) v : U) ((ψ : (a : W) → U) ((φ : (a : V) → W) v : W) : U)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ : ρ.Equiv σ
v : W
⊢ (φ : (a : V) → W) ((φ.symm : (a : W) → V) v : V) = v

Tactic:
φ.right_inv v

Premises used: LinearEquiv.right_inv, ContinuousLinearEquiv.toLinearEquiv, ContRepresentation.Equiv.toContinuousLinearEquiv
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ : ρ.Equiv σ
v : V
⊢ (φ.symm : (a : W) → V) ((φ : (a : V) → W) v : W) = v

Tactic:
φ.left_inv v

Premises used: ContinuousLinearEquiv.toLinearEquiv, LinearEquiv.left_inv, ContRepresentation.Equiv.toContinuousLinearEquiv
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ : ρ.Equiv σ
h : ∀ (x : V), Eq (α := V) ((φ.trans φ.symm : (a : V) → V) x : V) ((refl ρ : (a : V) → V) x : V)
⊢ φ.trans φ.symm = refl ρ

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ : ρ.Equiv σ
x : V
⊢ Eq (α := V) ((φ.trans φ.symm : (a : V) → V) x : V) ((refl ρ : (a : V) → V) x : V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ : ρ.Equiv σ
h : ∀ (x : W), Eq (α := W) ((φ.symm.trans φ : (a : W) → W) x : W) ((refl σ : (a : W) → W) x : W)
⊢ φ.symm.trans φ = refl σ

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ : ρ.Equiv σ
x : W
⊢ Eq (α := W) ((φ.symm.trans φ : (a : W) → W) x : W) ((refl σ : (a : W) → W) x : W)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G : Type u_2
V : Type u_3
inst : Monoid G
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
g : G
v : V
⊢ ((((trivial R G V : ContRepresentation R G V) : (a : G) → V →L[R] V) g : V →L[R] V) : (a : V) → V) v = v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G_1 : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Monoid G_1
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
inst_10 : AddCommGroup U
inst_11 : Module R U
inst_12 : TopologicalSpace U
inst_13 : IsTopologicalAddGroup U
G : Type u_6
H : Type u_7
inst_14 : Group G
inst_15 : TopologicalSpace G
inst_16 : TopologicalSpace R
inst_17 : ContinuousSMul R V
inst_18 : ContinuousSMul R W
inst_19 : Group H
inst_20 : TopologicalSpace H
φ : G →ₜ* H
π : ContRepresentation R G V
⊢ ∀ {a b : C(H, V)},
    Membership.mem (γ := Set C(H, V))
        {f : C(H, V) |
          ∀ (g : G) (h : H),
            Eq.{u_3 + 1} (α := V) ((f : (a : H) → V) (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) : V)
              ((((π : (a : G) → V →L[R] V) g : V →L[R] V) : (a : V) → V) ((f : (a : H) → V) h : V) : V)}
        a →
      Membership.mem (γ := Set C(H, V))
          {f : C(H, V) |
            ∀ (g : G) (h : H),
              Eq.{u_3 + 1} (α := V) ((f : (a : H) → V) (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) : V)
                ((((π : (a : G) → V →L[R] V) g : V →L[R] V) : (a : V) → V) ((f : (a : H) → V) h : V) : V)}
          b →
        Membership.mem (γ := Set C(H, V))
          {f : C(H, V) |
            ∀ (g : G) (h : H),
              Eq.{u_3 + 1} (α := V) ((f : (a : H) → V) (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) : V)
                ((((π : (a : G) → V →L[R] V) g : V →L[R] V) : (a : V) → V) ((f : (a : H) → V) h : V) : V)}
          (a + b)

Tactic:
simp +contextual
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G_1 : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Monoid G_1
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
inst_10 : AddCommGroup U
inst_11 : Module R U
inst_12 : TopologicalSpace U
inst_13 : IsTopologicalAddGroup U
G : Type u_6
H : Type u_7
inst_14 : Group G
inst_15 : TopologicalSpace G
inst_16 : TopologicalSpace R
inst_17 : ContinuousSMul R V
inst_18 : ContinuousSMul R W
inst_19 : Group H
inst_20 : TopologicalSpace H
φ : G →ₜ* H
π : ContRepresentation R G V
⊢ Membership.mem (γ := Set C(H, V))
    {f : C(H, V) |
      ∀ (g : G) (h : H),
        Eq.{u_3 + 1} (α := V) ((f : (a : H) → V) (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) : V)
          ((((π : (a : G) → V →L[R] V) g : V →L[R] V) : (a : V) → V) ((f : (a : H) → V) h : V) : V)}
    0

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G_1 : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Monoid G_1
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
inst_10 : AddCommGroup U
inst_11 : Module R U
inst_12 : TopologicalSpace U
inst_13 : IsTopologicalAddGroup U
G : Type u_6
H : Type u_7
inst_14 : Group G
inst_15 : TopologicalSpace G
inst_16 : TopologicalSpace R
inst_17 : ContinuousSMul R V
inst_18 : ContinuousSMul R W
inst_19 : Group H
inst_20 : TopologicalSpace H
φ : G →ₜ* H
π : ContRepresentation R G V
⊢ ∀ (c : R) {x : C(H, V)},
    Membership.mem (γ := Set C(H, V))
        {f : C(H, V) |
          ∀ (g : G) (h : H),
            Eq.{u_3 + 1} (α := V) ((f : (a : H) → V) (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) : V)
              ((((π : (a : G) → V →L[R] V) g : V →L[R] V) : (a : V) → V) ((f : (a : H) → V) h : V) : V)}
        x →
      Membership.mem (γ := Set C(H, V))
        {f : C(H, V) |
          ∀ (g : G) (h : H),
            Eq.{u_3 + 1} (α := V) ((f : (a : H) → V) (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) : V)
              ((((π : (a : G) → V →L[R] V) g : V →L[R] V) : (a : V) → V) ((f : (a : H) → V) h : V) : V)}
        (c • x)

Tactic:
simp +contextual
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
V : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : Module R V
G : Type u_6
H : Type u_7
inst_5 : Group G
inst_6 : TopologicalSpace G
inst_7 : TopologicalSpace R
inst_8 : ContinuousSMul R V
inst_9 : Group H
inst_10 : TopologicalSpace H
φ : G →ₜ* H
π : ContRepresentation R G V
f : C(H, V)
⊢ Membership.mem (γ := Submodule R C(H, V)) (coindV φ π : Submodule R C(H, V)) f ↔
    ∀ (g : G) (h : H),
      Eq.{u_3 + 1} (α := V) ((f : (a : H) → V) (HMul.hMul (α := H) ((φ : (a : G) → H) g : H) h) : V)
        ((((π : (a : G) → V →L[R] V) g : V →L[R] V) : (a : V) → V) ((f : (a : H) → V) h : V) : V)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RepresentationTheory.Continuous.Basic
Goal:
R : Type u_1
G_1 : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : Monoid G_1
inst_1 : Ring R
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : Module R V
inst_6 : AddCommGroup W
inst_7 : TopologicalSpace W
inst_8 : IsTopologicalAddGroup W
inst_9 : Module R W
inst_10 : AddCommGroup U
inst_11 : Module R U
inst_12 : TopologicalSpace U
inst_13 : IsTopologicalAddGroup U
G : Type u_6
H : Type u_7
inst_14 : Group G
inst_15 : TopologicalSpace G
inst_16 : TopologicalSpace R
inst_17 : ContinuousSMul R V
inst_18 : ContinuousSMul R W
inst_19 : Group H
inst_20 : TopologicalSpace H
φ : G →ₜ* H
π : ContRepresentation R G V
⊢ Continuous (Y := ↥(coindV φ π : Submodule R C(H, V))) fun (p : R × ↥(coindV φ π : Submodule R C(H, V))) ↦ p.1 • p.2

Tactic:
continuity