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 B : Rep.{u_1, u, v} k ↥S
f : A ⟶ B
g₁ : G
a : (↑A : Type u_1)
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))

Tactic:
simp [S.1.smul_def, hom_comm_apply]

Premises used: Submonoid.smul_def, Rep.hom_comm_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 B : Rep.{u_1, u, v} k ↥S
f : A ⟶ B
g₁ g₂ : G
a : (↑A : Type u_1)
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))

Tactic:
simp [indToCoindAux_of_not_rel (h := h)]

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
x : (↑A : Type w)
x_1 : ↥S
x_2 : G
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((A.indToCoindAux g : (a : (↑A : Type w)) → G → (↑A : Type w)) x
        (HMul.hMul (α := G) ((S.subtype : (a : ↥S) → G) x_1 : G) x_2) :
      (↑A : Type w))
    ((((A.ρ : (a : ↥S) → (↑A : Type w) →ₗ[k] (↑A : Type w)) x_1 : (↑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)) x x_2 : (↑A : Type w)) :
      (↑A : Type w))

Tactic:
simp
-- 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
x : ↥S
a :
  ∀ (a : G) (x_1 : (↑A : Type w)) (x_2 : G),
    Eq.{w + 1} (α := (↑A : Type w))
      ((↑((((AlgebraTensorModule.curry
                          (TensorProduct.lift
                              (linearCombination k fun (g : G) ↦
                                LinearMap.codRestrict (coindV S.subtype A.ρ) (A.indToCoindAux g) ⋯) ∘ₗ
                            (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ :
                                (a : ↥S) → (G →₀ k) ⊗[k] (↑A : Type w) →ₗ[k] (G →₀ k) ⊗[k] (↑A : Type w))
                              x) ∘ₗ
                        lsingle a :
                      k →ₗ[k] (↑A : Type w) →ₗ[k] (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))) :
                    (a : k) → (↑A : Type w) →ₗ[k] (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w)))
                  1 :
                (a : (↑A : Type w)) → (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w)))
              x_1) :
          G → (↑A : Type w))
        x_2)
      ((↑((((AlgebraTensorModule.curry
                          (TensorProduct.lift
                            (linearCombination k fun (g : G) ↦
                              LinearMap.codRestrict (coindV S.subtype A.ρ) (A.indToCoindAux g) ⋯)) ∘ₗ
                        lsingle a :
                      k →ₗ[k] (↑A : Type w) →ₗ[k] (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))) :
                    (a : k) → (↑A : Type w) →ₗ[k] (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w)))
                  1 :
                (a : (↑A : Type w)) → (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w)))
              x_1) :
          G → (↑A : Type w))
        x_2)
⊢ Eq (α := (G →₀ k) ⊗[k] (↑A : Type w) →ₗ[k] (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w)))
    (TensorProduct.lift
        (linearCombination k fun (g : G) ↦ LinearMap.codRestrict (coindV S.subtype A.ρ) (A.indToCoindAux g) ⋯) ∘ₗ
      (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ :
          (a : ↥S) → (G →₀ k) ⊗[k] (↑A : Type w) →ₗ[k] (G →₀ k) ⊗[k] (↑A : Type w))
        x)
    (TensorProduct.lift
      (linearCombination k fun (g : G) ↦ LinearMap.codRestrict (coindV S.subtype A.ρ) (A.indToCoindAux g) ⋯))

Tactic:
ext
-- 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
x : ↥S
a : G
x_1 : (↑A : Type w)
x_2 : G
⊢ Eq.{w + 1} (α := (↑A : Type w))
    ((↑((((AlgebraTensorModule.curry
                        (TensorProduct.lift
                            (linearCombination k fun (g : G) ↦
                              LinearMap.codRestrict (coindV S.subtype A.ρ) (A.indToCoindAux g) ⋯) ∘ₗ
                          (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ :
                              (a : ↥S) → (G →₀ k) ⊗[k] (↑A : Type w) →ₗ[k] (G →₀ k) ⊗[k] (↑A : Type w))
                            x) ∘ₗ
                      lsingle a :
                    k →ₗ[k] (↑A : Type w) →ₗ[k] (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))) :
                  (a : k) → (↑A : Type w) →ₗ[k] (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w)))
                1 :
              (a : (↑A : Type w)) → (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w)))
            x_1) :
        G → (↑A : Type w))
      x_2)
    ((↑((((AlgebraTensorModule.curry
                        (TensorProduct.lift
                          (linearCombination k fun (g : G) ↦
                            LinearMap.codRestrict (coindV S.subtype A.ρ) (A.indToCoindAux g) ⋯)) ∘ₗ
                      lsingle a :
                    k →ₗ[k] (↑A : Type w) →ₗ[k] (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))) :
                  (a : k) → (↑A : Type w) →ₗ[k] (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w)))
                1 :
              (a : (↑A : Type w)) → (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w)))
            x_1) :
        G → (↑A : Type w))
      x_2)

Tactic:
simp
-- 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
inst_3 : S.FiniteIndex
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
g : Quotient (QuotientGroup.rightRel S)
g₁ g₂ : G
h : g₁ ≈ g₂
s : ↥S
hs : (↑s : G) * g₂ = g₁
⊢ (↑f : G → (↑A : Type w)) (HMul.hMul (α := G) ((S.subtype : (a : ↥S) → G) s : G) g₂) =
    (((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))
      ((↑f : G → (↑A : Type w)) g₂)

Tactic:
have := f.2 s g₂
-- 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
inst_3 : S.FiniteIndex
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
g : Quotient (QuotientGroup.rightRel S)
g₁ g₂ : G
h : g₁ ≈ g₂
s : ↥S
hs : (↑s : G) * g₂ = g₁
this :
  (↑f : G → (↑A : Type w)) (HMul.hMul (α := G) ((S.subtype : (a : ↥S) → G) s : G) g₂) =
    (((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))
      ((↑f : G → (↑A : Type w)) g₂)
⊢ HSub.hSub (α := (G →₀ k) ⊗[k] (↑A : Type w)) (β := (G →₀ k) ⊗[k] (↑A : Type w))
      ((((tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ :
                  (a : ↥S) → (G →₀ k) ⊗[k] (↑A : Type w) →ₗ[k] (G →₀ k) ⊗[k] (↑A : Type w))
                s :
              (G →₀ k) ⊗[k] (↑A : Type w) →ₗ[k] (G →₀ k) ⊗[k] (↑A : Type w)) :
            (a : (G →₀ k) ⊗[k] (↑A : Type w)) → (G →₀ k) ⊗[k] (↑A : Type w))
          (single g₂ 1 ⊗ₜ[k] (↑f : G → (↑A : Type w)) g₂) :
        (G →₀ k) ⊗[k] (↑A : Type w))
      (single g₂ 1 ⊗ₜ[k] (↑f : G → (↑A : Type w)) g₂ : (G →₀ k) ⊗[k] (↑A : Type w)) =
    HSub.hSub (α := (G →₀ k) ⊗[k] (↑A : Type w)) (β := (G →₀ k) ⊗[k] (↑A : Type w))
      ((((TensorProduct.mk k (G →₀ k) (↑A : Type w) : (a : G →₀ k) → (↑A : Type w) →ₗ[k] (G →₀ k) ⊗[k] (↑A : Type w))
                (single g₁ 1) :
              (↑A : Type w) →ₗ[k] (G →₀ k) ⊗[k] (↑A : Type w)) :
            (a : (↑A : Type w)) → (G →₀ k) ⊗[k] (↑A : Type w))
          ((↑f : G → (↑A : Type w)) g₁) :
        (G →₀ k) ⊗[k] (↑A : Type w))
      ((((TensorProduct.mk k (G →₀ k) (↑A : Type w) : (a : G →₀ k) → (↑A : Type w) →ₗ[k] (G →₀ k) ⊗[k] (↑A : Type w))
                (single g₂ 1) :
              (↑A : Type w) →ₗ[k] (G →₀ k) ⊗[k] (↑A : Type w)) :
            (a : (↑A : Type w)) → (G →₀ k) ⊗[k] (↑A : Type w))
          ((↑f : G → (↑A : Type w)) g₂) :
        (G →₀ k) ⊗[k] (↑A : Type w))

Tactic:
simp_all
-- 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
inst_3 : S.FiniteIndex
x x_1 : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
z : Quotient (QuotientGroup.rightRel S)
h : Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ z
x_2 : G
⊢ ⟦x_2⟧.liftOn
      (fun (g : G) ↦
        HAdd.hAdd (α := IndV S.subtype A.ρ) (β := IndV S.subtype A.ρ)
          ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ) :
                (a : (G →₀ k) ⊗[k] (↑A : Type w)) → IndV S.subtype A.ρ)
              (single g 1 ⊗ₜ[k] (↑x : G → (↑A : Type w)) g) :
            IndV S.subtype A.ρ)
          ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ) :
                (a : (G →₀ k) ⊗[k] (↑A : Type w)) → IndV S.subtype A.ρ)
              (single g 1 ⊗ₜ[k] (↑x_1 : G → (↑A : Type w)) g) :
            IndV S.subtype A.ρ))
      ⋯ =
    HAdd.hAdd (α := IndV S.subtype A.ρ)
      (⟦x_2⟧.liftOn
        (fun (g : G) ↦
          (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ) :
              (a : (G →₀ k) ⊗[k] (↑A : Type w)) → IndV S.subtype A.ρ)
            (single g 1 ⊗ₜ[k] (↑x : G → (↑A : Type w)) g))
        ⋯)
      (⟦x_2⟧.liftOn
        (fun (g : G) ↦
          (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ) :
              (a : (G →₀ k) ⊗[k] (↑A : Type w)) → IndV S.subtype A.ρ)
            (single g 1 ⊗ₜ[k] (↑x_1 : G → (↑A : Type w)) g))
        ⋯)

Tactic:
simp
-- 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
inst_3 : S.FiniteIndex
x x_1 : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
⊢ ∑ g : Quotient (QuotientGroup.rightRel S),
      g.liftOn
        (fun (g : G) ↦
          (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑(x + x_1) : G → (↑A : Type w)) g))
        ⋯ =
    HAdd.hAdd (α := (↑(ind S.subtype A) : Type (max (max u v) w)))
      (∑ g : Quotient (QuotientGroup.rightRel S),
        g.liftOn
          (fun (g : G) ↦
            (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑x : G → (↑A : Type w)) g))
          ⋯)
      (∑ g : Quotient (QuotientGroup.rightRel S),
        g.liftOn
          (fun (g : G) ↦
            (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑x_1 : G → (↑A : Type w)) g))
          ⋯)

Tactic:
simpa [← Finset.sum_add_distrib, TensorProduct.tmul_add] using
      Finset.sum_congr rfl fun z _ => Quotient.inductionOn z fun _ => by simp

Premises used: Finset.sum_add_distrib, Quotient.inductionOn, TensorProduct.tmul_add, Finset.sum_congr, rfl
-- 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
inst_3 : S.FiniteIndex
x : k
x_1 : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
z : Quotient (QuotientGroup.rightRel S)
h : Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ z
x_2 : G
⊢ ⟦x_2⟧.liftOn
      (fun (g : G) ↦
        HSMul.hSMul (β := IndV S.subtype A.ρ) x
          ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ) :
                (a : (G →₀ k) ⊗[k] (↑A : Type w)) → IndV S.subtype A.ρ)
              (single g 1 ⊗ₜ[k] (↑x_1 : G → (↑A : Type w)) g) :
            IndV S.subtype A.ρ))
      ⋯ =
    HSMul.hSMul (β := IndV S.subtype A.ρ) x
      (⟦x_2⟧.liftOn
        (fun (g : G) ↦
          (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ) :
              (a : (G →₀ k) ⊗[k] (↑A : Type w)) → IndV S.subtype A.ρ)
            (single g 1 ⊗ₜ[k] (↑x_1 : G → (↑A : Type w)) g))
        ⋯)

Tactic:
simp
-- 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
inst_3 : S.FiniteIndex
x : k
x_1 : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
⊢ ∑ g : Quotient (QuotientGroup.rightRel S),
      g.liftOn
        (fun (g : G) ↦
          (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑(x • x_1) : G → (↑A : Type w)) g))
        ⋯ =
    HSMul.hSMul (α := k) (β := (↑(ind S.subtype A) : Type (max (max u v) w))) ((RingHom.id k : (a : k) → k) x : k)
      (∑ g : Quotient (QuotientGroup.rightRel S),
        g.liftOn
          (fun (g : G) ↦
            (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑x_1 : G → (↑A : Type w)) g))
          ⋯)

Tactic:
simpa [Finset.smul_sum] using Finset.sum_congr rfl fun z _ =>
    Quotient.inductionOn z fun _ => by simp

Premises used: Quotient.inductionOn, Finset.smul_sum, Finset.sum_congr, rfl
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst_2 : S.FiniteIndex
g : G
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
hx : Function.support (↑f : G → (↑A : Type w)) ⊆ MulAction.orbit (↥S) g
rw :
  ⟦g⟧.liftOn
      (fun (g : G) ↦ (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g))
      ⋯ =
    (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g)
h₀ :
  ∀ (b : Quotient (QuotientGroup.rightRel S)),
    Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ b →
      b ≠ ⟦g⟧ →
        b.liftOn
            (fun (g : G) ↦
              (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g))
            ⋯ =
          0
h₁ :
  ⟦g⟧ ∉ Finset.univ →
    ⟦g⟧.liftOn
        (fun (g : G) ↦
          (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g))
        ⋯ =
      0
⊢ Eq (α := (↑(ind S.subtype A) : Type (max (max u v) w)))
    ((A.coindToInd :
          (a : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))) → (↑(ind S.subtype A) : Type (max (max u v) w)))
        f :
      (↑(ind S.subtype A) : Type (max (max u v) w)))
    ((IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g) :
      IndV S.subtype A.ρ)

Tactic:
rw [coindToInd_apply, Finset.sum_eq_single ⟦g⟧]

Premises used: Rep.coindToInd_apply, Finset.sum_eq_single, Quotient.mk
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst_2 : S.FiniteIndex
g : G
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
hx : Function.support (↑f : G → (↑A : Type w)) ⊆ MulAction.orbit (↥S) g
⊢ ⟦g⟧.liftOn
      (fun (g : G) ↦ (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g))
      ⋯ =
    (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst_2 : S.FiniteIndex
g : G
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
hx : Function.support (↑f : G → (↑A : Type w)) ⊆ MulAction.orbit (↥S) g
b : Quotient (QuotientGroup.rightRel S)
h₀ :
  Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ b →
    b ≠ ⟦g⟧ →
      b.liftOn
          (fun (g : G) ↦
            (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g))
          ⋯ =
        0
⊢ Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ b →
    b ≠ ⟦g⟧ →
      b.liftOn
          (fun (g : G) ↦
            (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g))
          ⋯ =
        0

Tactic:
_
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst_2 : S.FiniteIndex
g : G
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
hx : Function.support (↑f : G → (↑A : Type w)) ⊆ MulAction.orbit (↥S) g
b : G
h : Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ ⟦b⟧
hb : ⟦b⟧ ≠ ⟦g⟧
⊢ ∀ (x : G), ¬(↑f : G → (↑A : Type w)) x = 0 → x ∈ MulAction.orbit (↥S) g

Tactic:
simp_all only [Function.support_subset_iff, ne_eq, Quotient.eq]

Premises used: ne_eq, Function.support_subset_iff, Quotient.eq
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst_2 : S.FiniteIndex
g : G
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
hx : Function.support (↑f : G → (↑A : Type w)) ⊆ MulAction.orbit (↥S) g
b : G
h : Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ ⟦b⟧
hb : ⟦b⟧ ≠ ⟦g⟧
hx₁ : ∀ (x : G), ¬(↑f : G → (↑A : Type w)) x = 0 → x ∈ MulAction.orbit (↥S) g
⊢ Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ ⟦b⟧

Tactic:
simp_all only [Function.support_subset_iff, ne_eq, Quotient.eq]

Premises used: ne_eq, Function.support_subset_iff, Quotient.eq
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst_2 : S.FiniteIndex
g : G
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
hx : Function.support (↑f : G → (↑A : Type w)) ⊆ MulAction.orbit (↥S) g
b : G
h : Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ ⟦b⟧
hb : ⟦b⟧ ≠ ⟦g⟧
hx₁ : ∀ (x : G), ¬(↑f : G → (↑A : Type w)) x = 0 → x ∈ MulAction.orbit (↥S) g
a : Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ ⟦b⟧
⊢ ¬(QuotientGroup.rightRel S : G → G → Prop) b g

Tactic:
simp_all only [Function.support_subset_iff, ne_eq, Quotient.eq]

Premises used: ne_eq, Function.support_subset_iff, Quotient.eq
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst_2 : S.FiniteIndex
g : G
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
b : G
hx : ∀ (x : G), ¬(↑f : G → (↑A : Type w)) x = 0 → x ∈ MulAction.orbit (↥S) g
h : Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ ⟦b⟧
hb : ¬(QuotientGroup.rightRel S : G → G → Prop) b g
contrapose! :
  ∀ (hx : (↑f : G → (↑A : Type w)) b ≠ 0), ∃ (x : G), (↑f : G → (↑A : Type w)) x ≠ 0 ∧ x ∉ MulAction.orbit (↥S) g
⊢ (↑f : G → (↑A : Type w)) b = 0

Tactic:
contrapose! hx
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst_2 : S.FiniteIndex
g : G
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
b : G
h : Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ ⟦b⟧
hb : ¬(QuotientGroup.rightRel S : G → G → Prop) b g
hx : (↑f : G → (↑A : Type w)) b ≠ 0
w : G
left : (↑f : G → (↑A : Type w)) b ≠ 0
right : b ∉ MulAction.orbit (↥S) g
⊢ ∃ (x : G), (↑f : G → (↑A : Type w)) x ≠ 0 ∧ x ∉ MulAction.orbit (↥S) g

Tactic:
use b, hx, hb
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst_2 : S.FiniteIndex
g : G
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
hx : Function.support (↑f : G → (↑A : Type w)) ⊆ MulAction.orbit (↥S) g
b : G
h : Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ ⟦b⟧
hb : ⟦b⟧ ≠ ⟦g⟧
⊢ (↑f : G → (↑A : Type w)) b = 0

Tactic:
have : f.1 b = 0 := by
      simp_all only [Function.support_subset_iff, ne_eq, Quotient.eq]
      contrapose! hx
      use b, hx, hb
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst_2 : S.FiniteIndex
g : G
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
hx : Function.support (↑f : G → (↑A : Type w)) ⊆ MulAction.orbit (↥S) g
b : G
h : Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ ⟦b⟧
hb : ⟦b⟧ ≠ ⟦g⟧
this : (↑f : G → (↑A : Type w)) b = 0
⊢ ⟦b⟧.liftOn
      (fun (g : G) ↦ (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g))
      ⋯ =
    0

Tactic:
simp_all
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst_2 : S.FiniteIndex
g : G
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
hx : Function.support (↑f : G → (↑A : Type w)) ⊆ MulAction.orbit (↥S) g
b : Quotient (QuotientGroup.rightRel S)
h : Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ b
hb : b ≠ ⟦g⟧
h₀ :
  ∀ (b : G),
    Membership.mem (γ := Finset (Quotient (QuotientGroup.rightRel S))) Finset.univ ⟦b⟧ →
      ∀ (hb : ⟦b⟧ ≠ ⟦g⟧),
        ⟦b⟧.liftOn
            (fun (g : G) ↦
              (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g))
            ⋯ =
          0
⊢ b.liftOn
      (fun (g : G) ↦ (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g))
      ⋯ =
    0

Tactic:
induction b using Quotient.inductionOn with | h b =>
    have : f.1 b = 0 := by
      simp_all only [Function.support_subset_iff, ne_eq, Quotient.eq]
      contrapose! hx
      use b, hx, hb
    simp_all
-- Module: Mathlib.RepresentationTheory.FiniteIndex
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst_2 : S.FiniteIndex
g : G
f : (↑(coind.{u, v, v, w} S.subtype A) : Type (max v w))
hx : Function.support (↑f : G → (↑A : Type w)) ⊆ MulAction.orbit (↥S) g
⊢ ⟦g⟧ ∉ Finset.univ →
    ⟦g⟧.liftOn
        (fun (g : G) ↦
          (IndV.mk S.subtype A.ρ g : (a : (↑A : Type w)) → IndV S.subtype A.ρ) ((↑f : G → (↑A : Type w)) g))
        ⋯ =
      0

Tactic:
simp