awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g g₁ : G
a : (↑A : Type w)
s : ↥S
inl :
  ∀ (s₁ : ↥S),
    Eq.{w + 1} (α := (↑A : Type w))
      ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((↑s : G) * (fun (m : ↥S) ↦ m • g) s₁) :
        (↑A : Type w))
      ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
            (a : (↑A : Type w)) → (↑A : Type w))
          ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((fun (m : ↥S) ↦ m • g) s₁) :
            (↑A : Type w)) :
        (↑A : Type w))
inr :
  ∀ (h : ¬(QuotientGroup.rightRel S : G → G → Prop) g₁ g),
    Eq.{w + 1} (α := (↑A : Type w))
      ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((↑s : G) * g₁) : (↑A : Type w))
      ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
            (a : (↑A : Type w)) → (↑A : Type w))
          ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₁ : (↑A : Type w)) :
        (↑A : Type w))
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((↑s : G) * g₁) : (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₁ : (↑A : Type w)) :
      (↑A : Type w))

Tactic:
rcases em ((QuotientGroup.rightRel S).r g₁ g) with ⟨s₁, rfl⟩ | h

Premises used: em, rfl, Setoid.r
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g : G
a : (↑A : Type w)
s s₁ : ↥S
inl :
  Eq (α := (↑A : Type w))
    ((if h : (QuotientGroup.rightRel S : G → G → Prop) ((↑s : G) * s₁ • g) g then
            (A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ S) ((↑s : G) * s₁ • g * g⁻¹) ⋯)
          else 0 :
          (a : (↑A : Type w)) → (↑A : Type w))
        a :
      (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        ((if h : (QuotientGroup.rightRel S : G → G → Prop) (s₁ • g) g then
                (A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
                  (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g * g⁻¹) ⋯)
              else 0 :
              (a : (↑A : Type w)) → (↑A : Type w))
            a :
          (↑A : Type w)) :
      (↑A : Type w))
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((↑s : G) * (fun (m : ↥S) ↦ m • g) s₁) :
      (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((fun (m : ↥S) ↦ m • g) s₁) : (↑A : Type w)) :
      (↑A : Type w))

Tactic:
simp only [indToCoindAux, LinearMap.pi_apply]

Premises used: LinearMap.pi_apply, Rep.indToCoindAux
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g : G
a : (↑A : Type w)
s s₁ : ↥S
inl :
  Eq (α := (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ S) ((↑s : G) * s₁ • g * g⁻¹) ⋯) :
            (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        a :
      (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
                  (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g * g⁻¹) ⋯) :
                (↑A : Type w) →ₗ[k] (↑A : Type w)) :
              (a : (↑A : Type w)) → (↑A : Type w))
            a :
          (↑A : Type w)) :
      (↑A : Type w))
⊢ Eq (α := (↑A : Type w))
    ((if h : (QuotientGroup.rightRel S : G → G → Prop) ((↑s : G) * s₁ • g) g then
            (A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ S) ((↑s : G) * s₁ • g * g⁻¹) ⋯)
          else 0 :
          (a : (↑A : Type w)) → (↑A : Type w))
        a :
      (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        ((if h : (QuotientGroup.rightRel S : G → G → Prop) (s₁ • g) g then
                (A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
                  (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g * g⁻¹) ⋯)
              else 0 :
              (a : (↑A : Type w)) → (↑A : Type w))
            a :
          (↑A : Type w)) :
      (↑A : Type w))

Tactic:
rw [dif_pos ⟨s * s₁, mul_assoc ..⟩, dif_pos ⟨s₁, rfl⟩]

Premises used: dif_pos
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g : G
a : (↑A : Type w)
s s₁ : ↥S
⊢ Eq (α := (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ S) ((↑s : G) * s₁ • g * g⁻¹) ⋯) :
            (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        a :
      (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
                  (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g * g⁻¹) ⋯) :
                (↑A : Type w) →ₗ[k] (↑A : Type w)) :
              (a : (↑A : Type w)) → (↑A : Type w))
            a :
          (↑A : Type w)) :
      (↑A : Type w))

Tactic:
simp [S.1.smul_def, mul_assoc, ← S.1.mul_def]

Premises used: mul_assoc, Submonoid.smul_def, Submonoid.mul_def, Subgroup.toSubmonoid
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g g₁ : G
a : (↑A : Type w)
s : ↥S
h : ¬(QuotientGroup.rightRel S : G → G → Prop) g₁ g
inr : ¬(QuotientGroup.rightRel S : G → G → Prop) ((↑s : G) * g₁) g
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((↑s : G) * g₁) : (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₁ : (↑A : Type w)) :
      (↑A : Type w))

Tactic:
rw [indToCoindAux_of_not_rel _ _ _ h, indToCoindAux_of_not_rel, map_zero]

Premises used: map_zero, Rep.indToCoindAux_of_not_rel
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g g₁ : G
a : (↑A : Type w)
s : ↥S
h : ¬(QuotientGroup.rightRel S : G → G → Prop) g₁ g
h_1 : (QuotientGroup.rightRel S : G → G → Prop) ((↑s : G) * g₁) g
s₁ : ↥S
hs₁ : (fun (m : ↥S) ↦ m • g) s₁ = (↑s : G) * g₁
⊢ (fun (m : ↥S) ↦ m • g) (s⁻¹ * s₁) = g₁

Tactic:
simp_all [S.1.smul_def, mul_assoc]

Premises used: mul_assoc, Submonoid.smul_def
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g g₁ : G
a : (↑A : Type w)
s : ↥S
h : ¬(QuotientGroup.rightRel S : G → G → Prop) g₁ g
⊢ ¬(QuotientGroup.rightRel S : G → G → Prop) ((↑s : G) * g₁) g

Tactic:
exact mt (fun ⟨s₁, hs₁⟩ => ⟨s⁻¹ * s₁, by simp_all [S.1.smul_def, mul_assoc]⟩) h

Premises used: mt
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ g₂ : G
a : (↑A : Type w)
s : ↥S
inl :
  ∀ (s₁ : ↥S),
    Eq.{w + 1} (α := (↑A : Type w))
      ((A.indToCoindAux ((↑s : G) * g₁) : (a : (↑A : Type w)) → G → (↑A : Type w))
          ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
                (a : (↑A : Type w)) → (↑A : Type w))
              a :
            (↑A : Type w))
          ((fun (m : ↥S) ↦ m • g₁) s₁) :
        (↑A : Type w))
      ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((fun (m : ↥S) ↦ m • g₁) s₁) : (↑A : Type w))
inr :
  ∀ (h : ¬(QuotientGroup.rightRel S : G → G → Prop) g₂ g₁),
    Eq.{w + 1} (α := (↑A : Type w))
      ((A.indToCoindAux ((↑s : G) * g₁) : (a : (↑A : Type w)) → G → (↑A : Type w))
          ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
                (a : (↑A : Type w)) → (↑A : Type w))
              a :
            (↑A : Type w))
          g₂ :
        (↑A : Type w))
      ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₂ : (↑A : Type w))
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux ((↑s : G) * g₁) : (a : (↑A : Type w)) → G → (↑A : Type w))
        ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
              (a : (↑A : Type w)) → (↑A : Type w))
            a :
          (↑A : Type w))
        g₂ :
      (↑A : Type w))
    ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₂ : (↑A : Type w))

Tactic:
rcases em ((QuotientGroup.rightRel S).r g₂ g₁) with ⟨s₁, rfl⟩ | h

Premises used: em, rfl, Setoid.r
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ : G
a : (↑A : Type w)
s s₁ : ↥S
inl :
  Eq (α := (↑A : Type w))
    ((if h : (QuotientGroup.rightRel S : G → G → Prop) (s₁ • g₁) ((↑s : G) * g₁) then
            (A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * ((↑s : G) * g₁)⁻¹) ⋯)
          else 0 :
          (a : (↑A : Type w)) → (↑A : Type w))
        ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
              (a : (↑A : Type w)) → (↑A : Type w))
            a :
          (↑A : Type w)) :
      (↑A : Type w))
    ((if h : (QuotientGroup.rightRel S : G → G → Prop) (s₁ • g₁) g₁ then
            (A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * g₁⁻¹) ⋯)
          else 0 :
          (a : (↑A : Type w)) → (↑A : Type w))
        a :
      (↑A : Type w))
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux ((↑s : G) * g₁) : (a : (↑A : Type w)) → G → (↑A : Type w))
        ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
              (a : (↑A : Type w)) → (↑A : Type w))
            a :
          (↑A : Type w))
        ((fun (m : ↥S) ↦ m • g₁) s₁) :
      (↑A : Type w))
    ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a ((fun (m : ↥S) ↦ m • g₁) s₁) : (↑A : Type w))

Tactic:
simp only [indToCoindAux, LinearMap.pi_apply]

Premises used: LinearMap.pi_apply, Rep.indToCoindAux
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ : G
a : (↑A : Type w)
s s₁ : ↥S
⊢ (fun (m : ↥S) ↦ m • ((↑s : G) * g₁)) (s₁ * s⁻¹) = s₁ • g₁

Tactic:
simp [S.1.smul_def, smul_eq_mul, mul_assoc]

Premises used: mul_assoc, Submonoid.smul_def, smul_eq_mul
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ : G
a : (↑A : Type w)
s s₁ : ↥S
inl :
  Eq (α := (↑A : Type w))
    ((((A.ρ : (a : ↥S) → Module.End k (↑A : Type w))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * ((↑s : G) * g₁)⁻¹) ⋯ * s) :
            Module.End k (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        a :
      (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * g₁⁻¹) ⋯) :
            (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        a :
      (↑A : Type w))
⊢ Eq (α := (↑A : Type w))
    ((if h : (QuotientGroup.rightRel S : G → G → Prop) (s₁ • g₁) ((↑s : G) * g₁) then
            (A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * ((↑s : G) * g₁)⁻¹) ⋯)
          else 0 :
          (a : (↑A : Type w)) → (↑A : Type w))
        ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
              (a : (↑A : Type w)) → (↑A : Type w))
            a :
          (↑A : Type w)) :
      (↑A : Type w))
    ((if h : (QuotientGroup.rightRel S : G → G → Prop) (s₁ • g₁) g₁ then
            (A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * g₁⁻¹) ⋯)
          else 0 :
          (a : (↑A : Type w)) → (↑A : Type w))
        a :
      (↑A : Type w))

Tactic:
rw [dif_pos ⟨s₁ * s⁻¹, by simp [S.1.smul_def, smul_eq_mul, mul_assoc]⟩, dif_pos ⟨s₁, rfl⟩,
      ← Module.End.mul_apply, ← map_mul]

Premises used: dif_pos, map_mul, Module.End.mul_apply
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ : G
a : (↑A : Type w)
s s₁ : ↥S
inl :
  Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * ((↑s : G) * g₁)⁻¹) ⋯ * s =
    Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * g₁⁻¹) ⋯
⊢ Eq (α := (↑A : Type w))
    ((((A.ρ : (a : ↥S) → Module.End k (↑A : Type w))
              (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * ((↑s : G) * g₁)⁻¹) ⋯ * s) :
            Module.End k (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        a :
      (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) (Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * g₁⁻¹) ⋯) :
            (↑A : Type w) →ₗ[k] (↑A : Type w)) :
          (a : (↑A : Type w)) → (↑A : Type w))
        a :
      (↑A : Type w))

Tactic:
congr
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ : G
a : (↑A : Type w)
s s₁ : ↥S
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * ((↑s : G) * g₁)⁻¹) ⋯ * s =
    Subtype.mk (p := fun (x : G) ↦ x ∈ S) (s₁ • g₁ * g₁⁻¹) ⋯

Tactic:
simp [Subtype.ext_iff, S.1.smul_def, mul_assoc]

Premises used: mul_assoc, Submonoid.smul_def, Subtype.ext_iff
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ g₂ : G
a : (↑A : Type w)
s : ↥S
h : ¬(QuotientGroup.rightRel S : G → G → Prop) g₂ g₁
inr : ¬(QuotientGroup.rightRel S : G → G → Prop) g₂ ((↑s : G) * g₁)
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux ((↑s : G) * g₁) : (a : (↑A : Type w)) → G → (↑A : Type w))
        ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) s : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
              (a : (↑A : Type w)) → (↑A : Type w))
            a :
          (↑A : Type w))
        g₂ :
      (↑A : Type w))
    ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₂ : (↑A : Type w))

Tactic:
rw [indToCoindAux_of_not_rel (h := h), indToCoindAux_of_not_rel]

Premises used: Rep.indToCoindAux_of_not_rel
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ g₂ : G
a : (↑A : Type w)
s : ↥S
h : ¬(QuotientGroup.rightRel S : G → G → Prop) g₂ g₁
h_1 : (QuotientGroup.rightRel S : G → G → Prop) g₂ ((↑s : G) * g₁)
s₁ : ↥S
hs₁ : (fun (m : ↥S) ↦ m • ((↑s : G) * g₁)) s₁ = g₂
⊢ (fun (m : ↥S) ↦ m • g₁) (s₁ * s) = g₂

Tactic:
simp_all [S.1.smul_def, mul_assoc]

Premises used: mul_assoc, Submonoid.smul_def
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ g₂ : G
a : (↑A : Type w)
s : ↥S
h : ¬(QuotientGroup.rightRel S : G → G → Prop) g₂ g₁
⊢ ¬(QuotientGroup.rightRel S : G → G → Prop) g₂ ((↑s : G) * g₁)

Tactic:
exact mt (fun ⟨s₁, hs₁⟩ => ⟨s₁ * s, by simp_all [S.1.smul_def, mul_assoc]⟩) h

Premises used: mt
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ g₂ g₃ : G
a : (↑A : Type w)
inl :
  ∀ (s : ↥S) (hs : (fun (m : ↥S) ↦ m • g₁) s = g₂ * g₃⁻¹),
    Eq.{w + 1} (α := (↑A : Type w))
      ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a (g₂ * g₃⁻¹) : (↑A : Type w))
      ((A.indToCoindAux (g₁ * g₃) : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₂ : (↑A : Type w))
inr :
  ∀ (h : ¬(QuotientGroup.rightRel S : G → G → Prop) (g₂ * g₃⁻¹) g₁),
    Eq.{w + 1} (α := (↑A : Type w))
      ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a (g₂ * g₃⁻¹) : (↑A : Type w))
      ((A.indToCoindAux (g₁ * g₃) : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₂ : (↑A : Type w))
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a (g₂ * g₃⁻¹) : (↑A : Type w))
    ((A.indToCoindAux (g₁ * g₃) : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₂ : (↑A : Type w))

Tactic:
rcases em ((QuotientGroup.rightRel S).r (g₂ * g₃⁻¹) g₁) with ⟨s, hs⟩ | h

Premises used: HMul.hMul, em, Inv.inv, Setoid.r
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ g₂ g₃ : G
a : (↑A : Type w)
s : ↥S
hs : (fun (m : ↥S) ↦ m • g₁) s = g₂ * g₃⁻¹
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a (g₂ * g₃⁻¹) : (↑A : Type w))
    ((A.indToCoindAux (g₁ * g₃) : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₂ : (↑A : Type w))

Tactic:
simp [S.1.smul_def, mul_assoc, ← eq_mul_inv_iff_mul_eq.1 hs]

Premises used: mul_assoc, eq_mul_inv_iff_mul_eq, Submonoid.smul_def, Iff.mp
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ g₂ g₃ : G
a : (↑A : Type w)
h : ¬(QuotientGroup.rightRel S : G → G → Prop) (g₂ * g₃⁻¹) g₁
inr : ¬(QuotientGroup.rightRel S : G → G → Prop) g₂ (g₁ * g₃)
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a (g₂ * g₃⁻¹) : (↑A : Type w))
    ((A.indToCoindAux (g₁ * g₃) : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₂ : (↑A : Type w))

Tactic:
rw [indToCoindAux_of_not_rel (h := h), indToCoindAux_of_not_rel]

Premises used: HMul.hMul, Inv.inv, Rep.indToCoindAux_of_not_rel
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ g₂ g₃ : G
a : (↑A : Type w)
h : ¬(QuotientGroup.rightRel S : G → G → Prop) (g₂ * g₃⁻¹) g₁
h_1 : (QuotientGroup.rightRel S : G → G → Prop) g₂ (g₁ * g₃)
s : ↥S
hs : (fun (m : ↥S) ↦ m • (g₁ * g₃)) s = g₂
⊢ (fun (m : ↥S) ↦ m • g₁) s = g₂ * g₃⁻¹

Tactic:
simpa [S.1.smul_def, eq_mul_inv_iff_mul_eq, mul_assoc]

Premises used: mul_assoc, eq_mul_inv_iff_mul_eq, Submonoid.smul_def
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ g₂ g₃ : G
a : (↑A : Type w)
h : ¬(QuotientGroup.rightRel S : G → G → Prop) (g₂ * g₃⁻¹) g₁
⊢ ¬(QuotientGroup.rightRel S : G → G → Prop) g₂ (g₁ * g₃)

Tactic:
exact mt (fun ⟨s, hs⟩ => ⟨s, by simpa [S.1.smul_def, eq_mul_inv_iff_mul_eq, mul_assoc]⟩) h

Premises used: mt
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A : Rep.{w, u, v} k ↥S
g₁ g₂ g₃ : G
a : (↑A : Type w)
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux (g₁ * g₂⁻¹) : (a : (↑A : Type w)) → G → (↑A : Type w)) a g₃ : (↑A : Type w))
    ((A.indToCoindAux g₁ : (a : (↑A : Type w)) → G → (↑A : Type w)) a (g₃ * g₂) : (↑A : Type w))

Tactic:
simpa using (indToCoindAux_snd_mul_inv g₁ g₃ g₂⁻¹ a).symm

Premises used: Inv.inv, Rep.indToCoindAux_snd_mul_inv, Eq.symm
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
inst_2 : DecidableRel (α := G) (⇑(QuotientGroup.rightRel S) : G → G → Prop)
A B : Rep.{u_1, u, v} k ↥S
f : A ⟶ B
g₁ g₂ : G
a : (↑A : Type u_1)
inl :
  ∀ (s : ↥S),
    Eq.{u_1 + 1} (α := (↑B : Type u_1))
      ((B.indToCoindAux g₁ : (a : (↑B : Type u_1)) → G → (↑B : Type u_1))
          ((Hom.hom f : (a : (↑A : Type u_1)) → (↑B : Type u_1)) a : (↑B : Type u_1)) ((fun (m : ↥S) ↦ m • g₁) s) :
        (↑B : Type u_1))
      ((Hom.hom f : (a : (↑A : Type u_1)) → (↑B : Type u_1))
          ((A.indToCoindAux g₁ : (a : (↑A : Type u_1)) → G → (↑A : Type u_1)) a ((fun (m : ↥S) ↦ m • g₁) s) :
            (↑A : Type u_1)) :
        (↑B : Type u_1))
inr :
  ∀ (h : ¬(QuotientGroup.rightRel S : G → G → Prop) g₂ g₁),
    Eq.{u_1 + 1} (α := (↑B : Type u_1))
      ((B.indToCoindAux g₁ : (a : (↑B : Type u_1)) → G → (↑B : Type u_1))
          ((Hom.hom f : (a : (↑A : Type u_1)) → (↑B : Type u_1)) a : (↑B : Type u_1)) g₂ :
        (↑B : Type u_1))
      ((Hom.hom f : (a : (↑A : Type u_1)) → (↑B : Type u_1))
          ((A.indToCoindAux g₁ : (a : (↑A : Type u_1)) → G → (↑A : Type u_1)) a g₂ : (↑A : Type u_1)) :
        (↑B : Type u_1))
⊢ Eq.{u_1 + 1} (α := (↑B : Type u_1))
    ((B.indToCoindAux g₁ : (a : (↑B : Type u_1)) → G → (↑B : Type u_1))
        ((Hom.hom f : (a : (↑A : Type u_1)) → (↑B : Type u_1)) a : (↑B : Type u_1)) g₂ :
      (↑B : Type u_1))
    ((Hom.hom f : (a : (↑A : Type u_1)) → (↑B : Type u_1))
        ((A.indToCoindAux g₁ : (a : (↑A : Type u_1)) → G → (↑A : Type u_1)) a g₂ : (↑A : Type u_1)) :
      (↑B : Type u_1))

Tactic:
rcases em ((QuotientGroup.rightRel S).r g₂ g₁) with ⟨s, rfl⟩ | h

Premises used: em, rfl, Setoid.r