awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (α := { l : List ι // ∀ (i : ι), i ∈ l })
  (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
        (fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯ :
      (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
        Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
    (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) (Finset.val Finset.univ) ⋯)
l : { l : List ι // ∀ (i : ι), i ∈ l }
⊢ ∀ ⦃a b : (i : ι) → i ∈ (↑l : List ι) → α i⦄,
    a ≈ b →
      HasEquiv.Equiv (α := (i : ι) → α i) ((fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) a)
        ((fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) b)

Tactic:
exact fun _ _ h i ↦ h i _
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (α := { l : List ι // ∀ (i : ι), i ∈ l })
  (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
        (fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯ :
      (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
        Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
    (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) (Finset.val Finset.univ) ⋯)
a : { l : List ι // ∀ (i : ι), i ∈ l }
refine_2 :
  ∀ (b : { l : List ι // ∀ (i : ι), i ∈ l }),
    a ≈ b →
      Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
        ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
            (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
                (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
                (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ q i) :
              Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
          a)
        ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
            (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
                (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
                (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ q i) :
              Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
          b)
⊢ ∀ (b : { l : List ι // ∀ (i : ι), i ∈ l }),
    a ≈ b →
      Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
        ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
            (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
                (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
                (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ q i) :
              Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
          a)
        ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
            (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
                (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
                (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ q i) :
              Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
          b)

Tactic:
_
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (α := { l : List ι // ∀ (i : ι), i ∈ l })
  (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
        (fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯ :
      (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
        Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
    (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) (Finset.val Finset.univ) ⋯)
a b : { l : List ι // ∀ (i : ι), i ∈ l }
refine_2 :
  a ≈ b →
    Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
      ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
          (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
              (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
              (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ q i) :
            Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
        a)
      ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
          (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
              (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
              (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ q i) :
            Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
        b)
⊢ a ≈ b →
    Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
      ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
          (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
              (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
              (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ q i) :
            Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
        a)
      ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
          (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
              (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
              (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ q i) :
            Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
        b)

Tactic:
_
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (α := { l : List ι // ∀ (i : ι), i ∈ l })
  (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
        (fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯ :
      (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
        Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
    (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) (Finset.val Finset.univ) ⋯)
a b : { l : List ι // ∀ (i : ι), i ∈ l }
h : a ≈ b
⊢ Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
            (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
            (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ q i) :
          Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
      a)
    ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
            (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
            (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ q i) :
          Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
      b)

Tactic:
ind_fintype_pi (fun a ↦ ?_) q

Premises used: Quotient.ind_fintype_pi
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (α := { l : List ι // ∀ (i : ι), i ∈ l })
  (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
        (fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯ :
      (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
        Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
    (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) (Finset.val Finset.univ) ⋯)
a b : { l : List ι // ∀ (i : ι), i ∈ l }
h : a ≈ b
refine_2 :
  ∀ (a_1 : (i : ι) → α i),
    Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
      ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
          (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
              (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
              (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ (fun (x : ι) ↦ ⟦a_1 x⟧) i) :
            Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
        a)
      ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
          (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
              (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
              (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ (fun (x : ι) ↦ ⟦a_1 x⟧) i) :
            Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
        b)
⊢ Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
            (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
            (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ q i) :
          Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
      a)
    ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
            (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
            (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ q i) :
          Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
      b)

Tactic:
refine ind_fintype_pi (fun a ↦ ?_) q
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (α := { l : List ι // ∀ (i : ι), i ∈ l })
  (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
        (fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯ :
      (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
        Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
    (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) (Finset.val Finset.univ) ⋯)
a_1 b : { l : List ι // ∀ (i : ι), i ∈ l }
h : a_1 ≈ b
a : (i : ι) → α i
refine_2 refine_2₁ :
  Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑a_1 : List ι) → α i))
      (fun (a : (i : ι) → i ∈ (↑a_1 : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
      (listChoice (α := α) fun (i : ι) (x : i ∈ (↑a_1 : List ι)) ↦ ⟦a i⟧))
    (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑b : List ι) → α i))
      (fun (a : (i : ι) → i ∈ (↑b : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
      (listChoice (α := α) fun (i : ι) (x : i ∈ (↑b : List ι)) ↦ ⟦a i⟧))
refine_2₂ :
  Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑a_1 : List ι) → α i))
      (fun (a : (i : ι) → i ∈ (↑a_1 : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
      ⟦fun (x1 : ι) (x2 : x1 ∈ (↑a_1 : List ι)) ↦ a x1⟧)
    (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑b : List ι) → α i))
      (fun (a : (i : ι) → i ∈ (↑b : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯ ⟦fun (x1 : ι) (x2 : x1 ∈ (↑b : List ι)) ↦ a x1⟧)
⊢ Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
            (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
            (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ (fun (x : ι) ↦ ⟦a x⟧) i) :
          Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
      a_1)
    ((fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        (Quotient.map (sa := piSetoid (α := fun (i : ι) ↦ i ∈ (↑l : List ι) → α i))
            (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
            (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ (fun (x : ι) ↦ ⟦a x⟧) i) :
          Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
      b)

Tactic:
simp_rw [listChoice_mk, Quotient.map_mk]

Premises used: Quotient.map_mk, Quotient.listChoice_mk
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
a : (i : ι) → α i
dsimp :
  Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    (Quotient.liftOn
      ((Equiv.subtypeQuotientEquivQuotientSubtype (fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
            (fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯ :
          (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
            Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
        (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) (Finset.val Finset.univ) ⋯))
      (fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        Quotient.map (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
          (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ ⟦a i⟧))
      ⋯)
    ⟦a⟧
⊢ Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α))) (finChoice (α := α) fun (x : ι) ↦ ⟦a x⟧) ⟦a⟧

Tactic:
dsimp [finChoice]

Premises used: Quotient.finChoice
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
a : (i : ι) → α i
obtain :
  ∀ (l : List ι) (hl : ⟦l⟧ = Finset.val Finset.univ),
    Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
      (Quotient.liftOn
        ((Equiv.subtypeQuotientEquivQuotientSubtype (fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
              (fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯ :
            (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
              Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
          (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) (Finset.val Finset.univ) ⋯))
        (fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
          Quotient.map (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
            (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ ⟦a i⟧))
        ⋯)
      ⟦a⟧
⊢ Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    (Quotient.liftOn
      ((Equiv.subtypeQuotientEquivQuotientSubtype (fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
            (fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯ :
          (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
            Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
        (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) (Finset.val Finset.univ) ⋯))
      (fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        Quotient.map (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
          (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ ⟦a i⟧))
      ⋯)
    ⟦a⟧

Tactic:
obtain ⟨l, hl⟩ := (Finset.univ.val : Multiset ι).exists_rep

Premises used: Finset.univ, Finset.val, Quotient.exists_rep
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
a : (i : ι) → α i
l : List ι
hl : ⟦l⟧ = Finset.val Finset.univ
simp_rw :
  Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    (Quotient.liftOn (s := Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
      (({
            toFun := fun (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) ↦
              Quotient.hrecOn (motive := fun (x : Quotient (List.isSetoid ι)) ↦
                (∀ (i : ι), i ∈ x) →
                  Quotient (α := { l : List ι // ∀ (i : ι), i ∈ l })
                    (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
                (↑a : Quotient (List.isSetoid ι))
                (fun (a : List ι) (h : ∀ (i : ι), i ∈ ⟦a⟧) ↦
                  ⟦Subtype.mk (p := fun (l : List ι) ↦ ∀ (i : ι), i ∈ l) a ⋯⟧)
                ⋯ ⋯,
            invFun :=
              fun
                (a :
                  Quotient (α := { l : List ι // ∀ (i : ι), i ∈ l })
                    (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)) ↦
              a.liftOn
                (fun (a : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
                  Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) ⟦(↑a : List ι)⟧ ⋯)
                ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
            Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
        (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) ⟦l⟧ ⋯))
      (fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        Quotient.map (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
          ⟦fun (x1 : ι) (x2 : x1 ∈ (↑l : List ι)) ↦ a x1⟧)
      ⋯)
    ⟦a⟧
⊢ Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    (Quotient.liftOn
      ((Equiv.subtypeQuotientEquivQuotientSubtype (fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
            (fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯ :
          (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
            Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
        (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) (Finset.val Finset.univ) ⋯))
      (fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        Quotient.map (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
          (listChoice (α := α) fun (i : ι) (x : i ∈ (↑l : List ι)) ↦ ⟦a i⟧))
      ⋯)
    ⟦a⟧

Tactic:
simp_rw [← hl, Equiv.subtypeQuotientEquivQuotientSubtype, listChoice_mk]

Premises used: Equiv.subtypeQuotientEquivQuotientSubtype, Quotient.listChoice_mk
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
a : (i : ι) → α i
l : List ι
hl : ⟦l⟧ = Finset.val Finset.univ
⊢ Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    (Quotient.liftOn (s := Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)
      (({
            toFun := fun (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) ↦
              Quotient.hrecOn (motive := fun (x : Quotient (List.isSetoid ι)) ↦
                (∀ (i : ι), i ∈ x) →
                  Quotient (α := { l : List ι // ∀ (i : ι), i ∈ l })
                    (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
                (↑a : Quotient (List.isSetoid ι))
                (fun (a : List ι) (h : ∀ (i : ι), i ∈ ⟦a⟧) ↦
                  ⟦Subtype.mk (p := fun (l : List ι) ↦ ∀ (i : ι), i ∈ l) a ⋯⟧)
                ⋯ ⋯,
            invFun :=
              fun
                (a :
                  Quotient (α := { l : List ι // ∀ (i : ι), i ∈ l })
                    (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l)) ↦
              a.liftOn
                (fun (a : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
                  Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) ⟦(↑a : List ι)⟧ ⋯)
                ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : { x : Quotient (List.isSetoid ι) // ∀ (i : ι), i ∈ x }) →
            Quotient (Subtype.instSetoid_mathlib fun (l : List ι) ↦ ∀ (i : ι), i ∈ l))
        (Subtype.mk (p := fun (x : Quotient (List.isSetoid ι)) ↦ ∀ (i : ι), i ∈ x) ⟦l⟧ ⋯))
      (fun (l : { l : List ι // ∀ (i : ι), i ∈ l }) ↦
        Quotient.map (fun (a : (i : ι) → i ∈ (↑l : List ι) → α i) (i : ι) ↦ a i ⋯) ⋯
          ⟦fun (x1 : ι) (x2 : x1 ∈ (↑l : List ι)) ↦ a x1⟧)
      ⋯)
    ⟦a⟧

Tactic:
rfl
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
f : (i : ι) → Quotient (S i)
a : (i : ι) → α i
rw : Eq (α := (i : ι) → Quotient (S i)) (eval (α := α) ⟦a⟧) fun (x : ι) ↦ ⟦a x⟧
⊢ Eq (α := (i : ι) → Quotient (S i)) (eval (α := α) (finChoice (α := α) fun (x : ι) ↦ ⟦a x⟧)) fun (x : ι) ↦ ⟦a x⟧

Tactic:
rw [finChoice_eq]

Premises used: Quotient.finChoice_eq
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
f : (i : ι) → Quotient (S i)
a : (i : ι) → α i
⊢ Eq (α := (i : ι) → Quotient (S i)) (eval (α := α) ⟦a⟧) fun (x : ι) ↦ ⟦a x⟧

Tactic:
rfl
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
e : IsEmpty ι
q : (i : ι) → Quotient (S i)
h :
  ∀ (f : ((i : ι) → α i) → β) (h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b),
    finLiftOn (α := α) q f h = f fun (a : ι) ↦ e.elim (p := fun (x : ι) ↦ α x) a
⊢ Eq (α := (f : ((i : ι) → α i) → β) → (h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b) → β)
    (finLiftOn (α := α) q)
    fun (f : ((i : ι) → α i) → β) (x : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b) ↦
    f fun (a : ι) ↦ e.elim (p := fun (x : ι) ↦ α x) a

Tactic:
ext f h
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
e : IsEmpty ι
q : (i : ι) → Quotient (S i)
f : ((i : ι) → α i) → β
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b
h₁ : (finChoice (α := α) q).liftOn f h = f fun (a : ι) ↦ e.elim (p := fun (x : ι) ↦ α x) a
⊢ finLiftOn (α := α) q f h = f fun (a : ι) ↦ e.elim (p := fun (x : ι) ↦ α x) a

Tactic:
dsimp [finLiftOn]

Premises used: Quotient.finLiftOn
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
e : IsEmpty ι
q : (i : ι) → Quotient (S i)
f : ((i : ι) → α i) → β
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b
h₁ :
  ∀ (a : (i : ι) → α i),
    Quotient.liftOn (s := piSetoid (α := α)) ⟦a⟧ f h = f fun (a : ι) ↦ e.elim (p := fun (x : ι) ↦ α x) a
⊢ (finChoice (α := α) q).liftOn f h = f fun (a : ι) ↦ e.elim (p := fun (x : ι) ↦ α x) a

Tactic:
induction finChoice q using Quotient.ind

Premises used: Quotient.finChoice, Quotient.ind
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
e : IsEmpty ι
q : (i : ι) → Quotient (S i)
f : ((i : ι) → α i) → β
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b
a : (i : ι) → α i
⊢ Quotient.liftOn (s := piSetoid (α := α)) ⟦a⟧ f h = f fun (a : ι) ↦ e.elim (p := fun (x : ι) ↦ α x) a

Tactic:
h _ _ e.elim

Premises used: IsEmpty.elim
-- Module: Mathlib.Data.Fintype.Quotient
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid.{u_2} (α i)
β : Sort u_3
e : IsEmpty ι
q : (i : ι) → Quotient (S i)
f : ((i : ι) → α i) → β
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b
a : (i : ι) → α i
⊢ Quotient.liftOn (s := piSetoid (α := α)) ⟦a⟧ f h = f fun (a : ι) ↦ e.elim (p := fun (x : ι) ↦ α x) a

Tactic:
exact h _ _ e.elim

Premises used: IsEmpty.elim