awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → (f : (a : α) → α) a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
x : α
hx : x ∈ l
hx' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a x * f) (permsOfList l)) f
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
hl₁ : Nodup (α := α) ((Equiv.symm g : (a : α) → α) x :: l : List α)
hmeml₁ :
  ∀ {f : Equiv.Perm α},
    f ∈ permsOfList l →
      Eq (α := α) ((f : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α) : α) ((Equiv.symm g : (a : α) → α) x : α)
hf₃ :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap
      (fun (b : α) ↦
        List.map
          (fun (f : Equiv.Perm α) ↦
            HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) b : Equiv.Perm α) f)
          (permsOfList l))
      l)
    f
⊢ Membership.mem (γ := List (Equiv.Perm α))
    (List.map
      (fun (f : Equiv.Perm α) ↦
        HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) x : Equiv.Perm α) f)
      (permsOfList l))
    f

Tactic:
obtain rfl : g.symm x = a := f.injective <| by rw [hmeml hf₁, ← hg.2]; simp

Premises used: Equiv.injective, Equiv.symm, DFunLike.coe, rfl
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → (f : (a : α) → α) a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
x : α
hx : x ∈ l
hx' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a x * f) (permsOfList l)) f
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
hl₁ : Nodup (α := α) ((Equiv.symm g : (a : α) → α) x :: l : List α)
hmeml₁ :
  ∀ {f : Equiv.Perm α},
    f ∈ permsOfList l →
      Eq (α := α) ((f : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α) : α) ((Equiv.symm g : (a : α) → α) x : α)
hf₃ :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap
      (fun (b : α) ↦
        List.map
          (fun (f : Equiv.Perm α) ↦
            HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) b : Equiv.Perm α) f)
          (permsOfList l))
      l)
    f
hx'₁ :
  Membership.mem (γ := List (Equiv.Perm α))
    (List.map
      (fun (f : Equiv.Perm α) ↦
        HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) x : Equiv.Perm α) f)
      (permsOfList l))
    f
⊢ g ∈ permsOfList l ∧ HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) x : Equiv.Perm α) g = f

Tactic:
obtain rfl : g.symm x = a := f.injective <| by rw [hmeml hf₁, ← hg.2]; simp

Premises used: Equiv.injective, Equiv.symm, DFunLike.coe, rfl
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl' : l.Nodup
hln' : (permsOfList l).Nodup
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
x : α
hx : x ∈ l
g : Equiv.Perm α
hl : Nodup (α := α) ((Equiv.symm g : (a : α) → α) x :: l : List α)
hmeml :
  ∀ {f : Equiv.Perm α},
    f ∈ permsOfList l →
      Eq (α := α) ((f : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α) : α) ((Equiv.symm g : (a : α) → α) x : α)
hf₂ :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap
      (fun (b : α) ↦
        List.map
          (fun (f : Equiv.Perm α) ↦
            HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) b : Equiv.Perm α) f)
          (permsOfList l))
      l)
    f
hx' :
  Membership.mem (γ := List (Equiv.Perm α))
    (List.map
      (fun (f : Equiv.Perm α) ↦
        HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) x : Equiv.Perm α) f)
      (permsOfList l))
    f
hg :
  g ∈ permsOfList l ∧ HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) x : Equiv.Perm α) g = f
⊢ x ≠ (Equiv.symm g : (a : α) → α) x

Tactic:
have hxa : x ≠ g.symm x := fun h => (List.nodup_cons.1 hl).1 (h ▸ hx)
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl' : l.Nodup
hln' : (permsOfList l).Nodup
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
x : α
hx : x ∈ l
g : Equiv.Perm α
hl : Nodup (α := α) ((Equiv.symm g : (a : α) → α) x :: l : List α)
hmeml :
  ∀ {f : Equiv.Perm α},
    f ∈ permsOfList l →
      Eq (α := α) ((f : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α) : α) ((Equiv.symm g : (a : α) → α) x : α)
hf₂ :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap
      (fun (b : α) ↦
        List.map
          (fun (f : Equiv.Perm α) ↦
            HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) b : Equiv.Perm α) f)
          (permsOfList l))
      l)
    f
hx' :
  Membership.mem (γ := List (Equiv.Perm α))
    (List.map
      (fun (f : Equiv.Perm α) ↦
        HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) x : Equiv.Perm α) f)
      (permsOfList l))
    f
hg :
  g ∈ permsOfList l ∧ HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) x : Equiv.Perm α) g = f
hxa : x ≠ (Equiv.symm g : (a : α) → α) x
⊢ Ne (α := α) ((g : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α) : α) ((Equiv.symm g : (a : α) → α) x : α)

Tactic:
simpa using hxa
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl' : l.Nodup
hln' : (permsOfList l).Nodup
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
x : α
hx : x ∈ l
g : Equiv.Perm α
hl : Nodup (α := α) ((Equiv.symm g : (a : α) → α) x :: l : List α)
hmeml :
  ∀ {f : Equiv.Perm α},
    f ∈ permsOfList l →
      Eq (α := α) ((f : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α) : α) ((Equiv.symm g : (a : α) → α) x : α)
hf₂ :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap
      (fun (b : α) ↦
        List.map
          (fun (f : Equiv.Perm α) ↦
            HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) b : Equiv.Perm α) f)
          (permsOfList l))
      l)
    f
hx' :
  Membership.mem (γ := List (Equiv.Perm α))
    (List.map
      (fun (f : Equiv.Perm α) ↦
        HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) x : Equiv.Perm α) f)
      (permsOfList l))
    f
hg :
  g ∈ permsOfList l ∧ HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) x : Equiv.Perm α) g = f
hxa : x ≠ (Equiv.symm g : (a : α) → α) x
⊢ False

Tactic:
exact (List.nodup_cons.1 hl).1 <| mem_of_mem_permsOfList hg.1 (by simpa using hxa)

Premises used: List.nodup_cons, And.left, Iff.mp, mem_of_mem_permsOfList
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
s : Finset α
a b : List α
hab : a ≈ b
ha : Multiset.Nodup ⟦a⟧
hb : Multiset.Nodup ⟦b⟧
h : ha ≍ hb
⊢ ∀ (a_1 : Equiv.Perm α),
    a_1 ∈ { val := (↑(permsOfList a) : Multiset (Equiv.Perm α)), nodup := ⋯ : Finset (Equiv.Perm α) } ↔
      a_1 ∈ { val := (↑(permsOfList b) : Multiset (Equiv.Perm α)), nodup := ⋯ : Finset (Equiv.Perm α) }

Tactic:
simp [mem_permsOfList_iff, hab.mem_iff]

Premises used: mem_permsOfList_iff, List.Perm.mem_iff
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
val : Multiset α
l : List α
hs : Multiset.Nodup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)
f : Equiv.Perm α
⊢ f ∈ permsOfFinset { val := Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l, nodup := hs : Finset α } ↔
    ∀ {x : α},
      (f : (a : α) → α) x ≠ x →
        x ∈ { val := Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l, nodup := hs : Finset α }

Tactic:
mem_permsOfList_iff

Premises used: Set.Mem, setOf, Multiset.Mem, mem_permsOfList_iff
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
val : Multiset α
l : List α
hs : Multiset.Nodup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)
f : Equiv.Perm α
⊢ f ∈ permsOfFinset { val := Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l, nodup := hs : Finset α } ↔
    ∀ {x : α},
      (f : (a : α) → α) x ≠ x →
        x ∈ { val := Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l, nodup := hs : Finset α }

Tactic:
exact mem_permsOfList_iff

Premises used: mem_permsOfList_iff
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
val : Multiset α
l : List α
hs : Multiset.Nodup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)
⊢ #(permsOfFinset { val := Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l, nodup := hs : Finset α }) =
    (#{ val := Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l, nodup := hs : Finset α })!

Tactic:
length_permsOfList l

Premises used: length_permsOfList, Finset.card, Multiset.card
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
val : Multiset α
l : List α
hs : Multiset.Nodup (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)
⊢ #(permsOfFinset { val := Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l, nodup := hs : Finset α }) =
    (#{ val := Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l, nodup := hs : Finset α })!

Tactic:
exact length_permsOfList l

Premises used: length_permsOfList
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
⊢ ∀ (x : Equiv.Perm α), Membership.mem (γ := Finset (Equiv.Perm α)) (permsOfFinset univ) x

Tactic:
simp [mem_perms_of_finset_iff]

Premises used: mem_perms_of_finset_iff
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : DecidableEq α_1
inst_1 : DecidableEq β_1
α : Type u_4
β : Type u_5
inst_2 : Mul α
inst_3 : Mul β
inst_4 : DecidableEq α
inst_5 : DecidableEq β
inst_6 : Fintype α
inst_7 : Fintype β
⊢ ∀ (a a' : α ≃ β) (b : α ≃* β),
    Membership.mem (γ := Option (α ≃* β))
        ((fun (e : α ≃ β) ↦
            (if h :
                  ∀ (a b : α),
                    (e : (a : α) → β) (a * b) =
                      HMul.hMul (α := β) (β := β) ((e : (a : α) → β) a : β) ((e : (a : α) → β) b : β) then
                some { toEquiv := e, map_mul' := h }
              else none :
              Option (α ≃* β)))
          a)
        b →
      Membership.mem (γ := Option (α ≃* β))
          ((fun (e : α ≃ β) ↦
              (if h :
                    ∀ (a b : α),
                      (e : (a : α) → β) (a * b) =
                        HMul.hMul (α := β) (β := β) ((e : (a : α) → β) a : β) ((e : (a : α) → β) b : β) then
                  some { toEquiv := e, map_mul' := h }
                else none :
                Option (α ≃* β)))
            a')
          b →
        a = a'

Tactic:
aesop
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : DecidableEq α_1
inst_1 : DecidableEq β_1
α : Type u_4
β : Type u_5
inst_2 : Mul α
inst_3 : Mul β
inst_4 : DecidableEq α
inst_5 : DecidableEq β
inst_6 : Fintype α
inst_7 : Fintype β
me : α ≃* β
simp : { toEquiv := (↑me : α ≃ β), map_mul' := ⋯ } = me
⊢ (if h :
        ∀ (a b : α),
          (me.toEquiv : (a : α) → β) (a * b) =
            HMul.hMul (α := β) (β := β) ((me.toEquiv : (a : α) → β) a : β) ((me.toEquiv : (a : α) → β) b : β) then
      some { toEquiv := me.toEquiv, map_mul' := h }
    else none) =
    some me

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : DecidableEq α_1
inst_1 : DecidableEq β_1
α : Type u_4
β : Type u_5
inst_2 : Mul α
inst_3 : Mul β
inst_4 : DecidableEq α
inst_5 : DecidableEq β
inst_6 : Fintype α
inst_7 : Fintype β
me : α ≃* β
⊢ { toEquiv := (↑me : α ≃ β), map_mul' := ⋯ } = me

Tactic:
rfl
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : DecidableEq α_1
inst_1 : DecidableEq β_1
α : Type u_4
β : Type u_5
inst_2 : Mul α
inst_3 : Mul β
inst_4 : DecidableEq α
inst_5 : DecidableEq β
inst_6 : Fintype α
inst_7 : Fintype β
me : α ≃* β
this this₁ : { toEquiv := (↑me : α ≃ β), map_mul' := ⋯ } = me
⊢ (if h :
        ∀ (a b : α),
          (me.toEquiv : (a : α) → β) (a * b) =
            HMul.hMul (α := β) (β := β) ((me.toEquiv : (a : α) → β) a : β) ((me.toEquiv : (a : α) → β) b : β) then
      some { toEquiv := me.toEquiv, map_mul' := h }
    else none) =
    some me

Tactic:
{simp; rfl}
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ card.{u_1} (Equiv.Perm α) = (card α)!

Tactic:
Subsingleton.elim (@fintypePerm α _ _) (@Equiv.instFintype α α _ _ _ _) ▸ card_perms_of_finset _

Premises used: fintypePerm, Eq.rec, card_perms_of_finset, Equiv.instFintype, Subsingleton.elim
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
e : α ≃ β
⊢ card (α ≃ β) = (card α)!

Tactic:
Fintype.card_congr (equivCongr (Equiv.refl α) e) ▸ Fintype.card_perm

Premises used: Fintype.card_congr, Fintype.card_perm, Equiv.equivCongr, Eq.rec, Equiv.refl
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
γ : α → Type u_3
δ : α → Type u_4
s : (a : α) → Finset (γ a)
t : (a : α) → Finset (δ a)
x x_1 : (a : α) → Membership.mem (γ := Finset α) univ a → δ a
⊢ Eq (α := (a : α) → δ a) ((fun (f : (a : α) → Membership.mem (γ := Finset α) univ a → δ a) (a : α) ↦ f a ⋯) x)
      ((fun (f : (a : α) → Membership.mem (γ := Finset α) univ a → δ a) (a : α) ↦ f a ⋯) x_1) →
    x = x_1

Tactic:
simp +contextual [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
mp : f ∈ piFinset (δ := δ) t → ∀ (a : α), f a ∈ t a
mpr : (∀ (a : α), f a ∈ t a) → f ∈ piFinset (δ := δ) t
⊢ f ∈ piFinset (δ := δ) t ↔ ∀ (a : α), f a ∈ t a

Tactic:
constructor
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
mp :
  ∀ (x : (a : α) → Membership.mem (γ := Finset α) univ a → δ a),
    (∀ (a : α), x a ⋯ ∈ t a) →
      ({ toFun := fun (f : (a : α) → Membership.mem (γ := Finset α) univ a → δ a) (a : α) ↦ f a ⋯, inj' := ⋯ } :
              (a : (a : α) → a ∈ univ → δ a) → (a : α) → δ a)
            x =
          f →
        ∀ (a : α), f a ∈ t a
⊢ f ∈ piFinset (δ := δ) t → ∀ (a : α), f a ∈ t a

Tactic:
simp only [piFinset, mem_map, and_imp, forall_prop_of_true, mem_univ, exists_imp,
      mem_pi]

Premises used: Finset.mem_univ, and_imp, Fintype.piFinset, forall_prop_of_true, Finset.mem_pi, Finset.mem_map, exists_imp
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → Membership.mem (γ := Finset α) univ a → δ a
hg : ∀ (a : α), g a ⋯ ∈ t a
hgf :
  ({ toFun := fun (f : (a : α) → Membership.mem (γ := Finset α) univ a → δ a) (a : α) ↦ f a ⋯, inj' := ⋯ } :
        (a : (a : α) → a ∈ univ → δ a) → (a : α) → δ a)
      g =
    f
a : α
mp :
  Membership.mem (α := δ a) (t a)
    (({ toFun := fun (f : (a : α) → Membership.mem (γ := Finset α) univ a → δ a) (a : α) ↦ f a ⋯, inj' := ⋯ } :
          (a : (a : α) → a ∈ univ → δ a) → (a : α) → δ a)
        g a :
      δ a)
⊢ f a ∈ t a

Tactic:
rw [← hgf]
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → Membership.mem (γ := Finset α) univ a → δ a
hg : ∀ (a : α), g a ⋯ ∈ t a
hgf :
  ({ toFun := fun (f : (a : α) → Membership.mem (γ := Finset α) univ a → δ a) (a : α) ↦ f a ⋯, inj' := ⋯ } :
        (a : (a : α) → a ∈ univ → δ a) → (a : α) → δ a)
      g =
    f
a : α
⊢ Membership.mem (α := δ a) (t a)
    (({ toFun := fun (f : (a : α) → Membership.mem (γ := Finset α) univ a → δ a) (a : α) ↦ f a ⋯, inj' := ⋯ } :
          (a : (a : α) → a ∈ univ → δ a) → (a : α) → δ a)
        g a :
      δ a)

Tactic:
hg a

Premises used: Set.Mem, setOf
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → Membership.mem (γ := Finset α) univ a → δ a
hg : ∀ (a : α), g a ⋯ ∈ t a
hgf :
  ({ toFun := fun (f : (a : α) → Membership.mem (γ := Finset α) univ a → δ a) (a : α) ↦ f a ⋯, inj' := ⋯ } :
        (a : (a : α) → a ∈ univ → δ a) → (a : α) → δ a)
      g =
    f
a : α
⊢ Membership.mem (α := δ a) (t a)
    (({ toFun := fun (f : (a : α) → Membership.mem (γ := Finset α) univ a → δ a) (a : α) ↦ f a ⋯, inj' := ⋯ } :
          (a : (a : α) → a ∈ univ → δ a) → (a : α) → δ a)
        g a :
      δ a)

Tactic:
exact hg a
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
mpr :
  (∀ (a : α), f a ∈ t a) →
    ∃ (a : (a : α) → Membership.mem (γ := Finset α) univ a → δ a),
      (∀ (a_1 : α), a a_1 ⋯ ∈ t a_1) ∧
        ({ toFun := fun (f : (a : α) → Membership.mem (γ := Finset α) univ a → δ a) (a : α) ↦ f a ⋯, inj' := ⋯ } :
              (a : (a : α) → a ∈ univ → δ a) → (a : α) → δ a)
            a =
          f
⊢ (∀ (a : α), f a ∈ t a) → f ∈ piFinset (δ := δ) t

Tactic:
simp only [piFinset, mem_map, forall_prop_of_true, mem_univ, mem_pi]

Premises used: Finset.mem_univ, Fintype.piFinset, forall_prop_of_true, Finset.mem_pi, Finset.mem_map
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) →
    ∃ (a : (a : α) → Membership.mem (γ := Finset α) univ a → δ a),
      (∀ (a_1 : α), a a_1 ⋯ ∈ t a_1) ∧
        ({ toFun := fun (f : (a : α) → Membership.mem (γ := Finset α) univ a → δ a) (a : α) ↦ f a ⋯, inj' := ⋯ } :
              (a : (a : α) → a ∈ univ → δ a) → (a : α) → δ a)
            a =
          f

Tactic:
fun hf => ⟨fun a _ => f a, hf, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) →
    ∃ (a : (a : α) → Membership.mem (γ := Finset α) univ a → δ a),
      (∀ (a_1 : α), a a_1 ⋯ ∈ t a_1) ∧
        ({ toFun := fun (f : (a : α) → Membership.mem (γ := Finset α) univ a → δ a) (a : α) ↦ f a ⋯, inj' := ⋯ } :
              (a : (a : α) → a ∈ univ → δ a) → (a : α) → δ a)
            a =
          f

Tactic:
exact fun hf => ⟨fun a _ => f a, hf, rfl⟩
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
rw : x ∈ (↑(piFinset (δ := δ) t) : Set ((a : α) → δ a)) ↔ ∀ (i : α), x i ∈ (↑(t i) : Set (δ i))
⊢ x ∈ (↑(piFinset (δ := δ) t) : Set ((a : α) → δ a)) ↔
    Membership.mem (γ := Set ((a : α) → δ a)) (Set.pi (α := δ) Set.univ fun (a : α) ↦ (↑(t a) : Set (δ a))) x

Tactic:
rw [Set.mem_univ_pi]

Premises used: Set.mem_univ_pi
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ (↑(piFinset (δ := δ) t) : Set ((a : α) → δ a)) ↔ ∀ (i : α), x i ∈ (↑(t i) : Set (δ i))

Tactic:
Fintype.mem_piFinset

Premises used: Fintype.mem_piFinset
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ (↑(piFinset (δ := δ) t) : Set ((a : α) → δ a)) ↔ ∀ (i : α), x i ∈ (↑(t i) : Set (δ i))

Tactic:
exact Fintype.mem_piFinset

Premises used: Fintype.mem_piFinset
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t₁ t₂ : (a : α) → Finset (δ a)
h : ∀ (a : α), t₁ a ⊆ t₂ a
⊢ piFinset (δ := δ) t₁ ⊆ piFinset (δ := δ) t₂

Tactic:
fun _ hg => mem_piFinset.2 fun a => h a <| mem_piFinset.1 hg a

Premises used: Iff.mpr, Fintype.mem_piFinset, Iff.mp
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
γ : α → Type u_3
s : (a : α) → Finset (γ a)
⊢ piFinset (δ := γ) s = ∅ ↔ ∃ (i : α), s i = ∅

Tactic:
simp [piFinset]

Premises used: Fintype.piFinset
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
inst_2 : Nonempty α
⊢ Eq (α := Finset ((a : α) → δ a)) (piFinset (δ := δ) fun (x : α) ↦ ∅) ∅

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
γ : α → Type u_3
s : (a : α) → Finset (γ a)
⊢ (piFinset (δ := γ) s).Nonempty ↔ ∀ (a : α), (s a).Nonempty

Tactic:
simp [piFinset]

Premises used: Fintype.piFinset
-- Module: Mathlib.Data.Fintype.Pi
Goal:
β : Type u_2
ι : Type u_5
inst : Fintype ι
inst_1 : DecidableEq ι
s : Finset β
hs : s.Nonempty
⊢ Finset.Nonempty (α := (a : ι) → β) (piFinset (δ := fun (x : ι) ↦ β) fun (x : ι) ↦ s)

Tactic:
piFinset_nonempty.2 fun _ ↦ hs

Premises used: Iff.mpr, Fintype.piFinset_nonempty
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
γ : α → Type u_3
inst_2 : IsEmpty α
s : (a : α) → Finset (γ a)
x : (a : α) → γ a
⊢ x ∈ piFinset (δ := γ) s

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
f x : (a : α) → δ a
⊢ Membership.mem (γ := Finset ((a : α) → δ a)) (piFinset (δ := δ) fun (i : α) ↦ {f i}) x ↔
    Membership.mem (γ := Finset ((a : α) → δ a)) {f} x

Tactic:
grind
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
f : (i : α) → Finset (δ i)
hf : ∀ (i : α), (↑(f i) : Set (δ i)).Subsingleton
⊢ (↑(piFinset (δ := δ) f) : Set ((i : α) → δ i)).Subsingleton

Tactic:
fun _ ha _ hb =>
  funext fun _ => hf _ (mem_piFinset.1 ha _) (mem_piFinset.1 hb _)

Premises used: Fintype.mem_piFinset, funext, Set.Subsingleton, Iff.mp
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t₁ t₂ : (a : α) → Finset (δ a)
a : α
h : Disjoint (t₁ a) (t₂ a)
⊢ Disjoint (piFinset (δ := δ) t₁) (piFinset (δ := δ) t₂)

Tactic:
disjoint_iff_ne.2 fun f₁ hf₁ f₂ hf₂ eq₁₂ =>
    disjoint_iff_ne.1 h (f₁ a) (mem_piFinset.1 hf₁ a) (f₂ a) (mem_piFinset.1 hf₂ a)
      (congr_fun eq₁₂ a)

Premises used: Iff.mpr, Fintype.mem_piFinset, Finset.disjoint_iff_ne, Iff.mp, congr_fun
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
γ : α → Type u_3
δ : α → Type u_4
inst_2 : (a : α) → DecidableEq (δ a)
f : (a : α) → γ a → δ a
s : (a : α) → Finset (γ a)
h :
  ∀ (a : (a : α) → δ a),
    Membership.mem (γ := Finset ((a : α) → δ a)) (piFinset (δ := δ) fun (a : α) ↦ image (f a) (s a)) a ↔
      Membership.mem (γ := Finset ((a : α) → δ a))
        (image (fun (b : (a : α) → γ a) (a : α) ↦ f a (b a)) (piFinset (δ := γ) s)) a
⊢ Eq (α := Finset ((a : α) → δ a)) (piFinset (δ := δ) fun (a : α) ↦ image (f a) (s a))
    (image (fun (b : (a : α) → γ a) (a : α) ↦ f a (b a)) (piFinset (δ := γ) s))

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Pi
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
γ : α → Type u_3
δ : α → Type u_4
inst_2 : (a : α) → DecidableEq (δ a)
f : (a : α) → γ a → δ a
s : (a : α) → Finset (γ a)
a : (a : α) → δ a
⊢ Membership.mem (γ := Finset ((a : α) → δ a)) (piFinset (δ := δ) fun (a : α) ↦ image (f a) (s a)) a ↔
    Membership.mem (γ := Finset ((a : α) → δ a))
      (image (fun (b : (a : α) → γ a) (a : α) ↦ f a (b a)) (piFinset (δ := γ) s)) a

Tactic:
simp only [mem_piFinset, mem_image, Classical.skolem, forall_and, funext_iff]

Premises used: Classical.skolem, Fintype.mem_piFinset, Finset.mem_image, funext_iff, forall_and