awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Pairwise
Goal:
α : Type u_5
ι : Type u_6
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : DecidableEq ι
l : List ι
f : ι → α
hn : l.Nodup
⊢ (↑l.toFinset : Set ι).PairwiseDisjoint f ↔ Pairwise (_root_.Disjoint on f) l

Tactic:
pairwise_iff_coe_toFinset_pairwise hn (symmetric_disjoint.comap f)

Premises used: Set.PairwiseDisjoint, Symmetric.comap, List.pairwise_iff_coe_toFinset_pairwise, symmetric_disjoint
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
s : Finset α
t : (a : α) → Finset (β a)
⊢ (s.pi (β := β) t).val = s.val.pi (β := β) fun (a : α) ↦ (t a).val

Tactic:
rfl

Premises used: Multiset.recOn, Multiset.rec, Multiset.pi, rfl
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
s : Finset α
t : (a : α) → Finset (β a)
f : (a : α) → a ∈ s → β a
⊢ f ∈ s.pi (β := β) t ↔ ∀ (a : α) (h : a ∈ s), f a h ∈ t a

Tactic:
Multiset.mem_pi _ _ _

Premises used: Multiset.mem_pi, Set.Mem, setOf, Multiset.recOn, Multiset.Mem, Multiset.rec, Multiset.pi
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
δ : α → Sort v
inst : DecidableEq α
s : Finset α
a : α
b : δ a
f : (a : α) → a ∈ s → δ a
h : a ∈ insert a s
⊢ cons (δ := δ) s a b f a h = b

Tactic:
Multiset.Pi.cons_same _

Premises used: Finset.Pi.cons, Multiset.Pi.cons_same
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
δ : α → Sort v
inst : DecidableEq α
s : Finset α
a a' : α
b : δ a
f : (a : α) → a ∈ s → δ a
h : a' ∈ insert a s
ha : a ≠ a'
⊢ cons (δ := δ) s a b f a' h = f a' ⋯

Tactic:
Multiset.Pi.cons_ne _ (Ne.symm ha)

Premises used: Ne.symm, Finset.Pi.cons, Multiset.Pi.cons_ne
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
δ : α → Sort v
inst : DecidableEq α
a : α
b : δ a
s : Finset α
hs : a ∉ s
e₁ e₂ : (a : α) → a ∈ s → δ a
eq : Eq (α := (a' : α) → (h : a' ∈ insert a s) → δ a') (cons (δ := δ) s a b e₁) (cons (δ := δ) s a b e₂)
e : α
h : e ∈ a ::ₘ s.val
⊢ e ∈ insert a s

Tactic:
simpa only [Multiset.mem_cons, mem_insert] using h

Premises used: Finset.mem_insert, Multiset.mem_cons
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
δ : α → Sort v
inst : DecidableEq α
a : α
b : δ a
s : Finset α
hs : a ∉ s
e₁ e₂ : (a : α) → a ∈ s → δ a
eq : Eq (α := (a' : α) → (h : a' ∈ insert a s) → δ a') (cons (δ := δ) s a b e₁) (cons (δ := δ) s a b e₂)
e : α
h : e ∈ a ::ₘ s.val
rw rw₁ : cons (δ := δ) s a b e₂ e ⋯ = cons (δ := δ) s a b e₂ e ⋯
⊢ cons (δ := δ) s a b e₁ e ⋯ = cons (δ := δ) s a b e₂ e ⋯

Tactic:
rw [eq]
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
t : (a : α) → Finset (β a)
⊢ Eq (α := Finset ((a : α) → Membership.mem (γ := Finset α) ∅ a → β a)) (pi (β := β) ∅ t) {Pi.empty β}

Tactic:
rfl

Premises used: Set.Mem, setOf, Multiset.zero, Multiset.recOn, Multiset.Mem, Multiset.ofList, Multiset.rec, Finset.pi, Multiset.pi, Finset.Pi.empty, rfl
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
β : α → Type u
s : Finset α
t : (a : α) → Finset (β a)
inst : DecidableEq α
⊢ (s.pi (β := β) t).Nonempty ↔ ∀ a ∈ s, (t a).Nonempty

Tactic:
simp [Finset.Nonempty, Classical.skolem]

Premises used: Classical.skolem, Finset.Nonempty
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
β : α → Type u
s : Finset α
t : (a : α) → Finset (β a)
inst : DecidableEq α
contrapose! : (s.pi (β := β) t).Nonempty ↔ ∀ (a : α) (_ : a ∈ s), (t a).Nonempty
⊢ s.pi (β := β) t = ∅ ↔ ∃ a ∈ s, t a = ∅

Tactic:
contrapose!
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
β : α → Type u
s : Finset α
t : (a : α) → Finset (β a)
inst : DecidableEq α
⊢ (s.pi (β := β) t).Nonempty ↔ ∀ (a : α) (_ : a ∈ s), (t a).Nonempty

Tactic:
pi_nonempty

Premises used: Finset.pi_nonempty
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
β : α → Type u
s : Finset α
t : (a : α) → Finset (β a)
inst : DecidableEq α
⊢ (s.pi (β := β) t).Nonempty ↔ ∀ (a : α) (_ : a ∈ s), (t a).Nonempty

Tactic:
exact pi_nonempty

Premises used: Finset.pi_nonempty
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
a₁ :
  ((insert a s).pi (β := β) t).val =
    val ((t a).biUnion fun (b : β a) ↦ image (Pi.cons (δ := β) s a b) (s.pi (β := β) t))
⊢ (insert a s).pi (β := β) t = (t a).biUnion fun (b : β a) ↦ image (Pi.cons (δ := β) s a b) (s.pi (β := β) t)

Tactic:
apply eq_of_veq

Premises used: Finset.eq_of_veq
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
a₁ :
  ((insert a s).pi (β := β) t).val.dedup =
    val ((t a).biUnion fun (b : β a) ↦ image (Pi.cons (δ := β) s a b) (s.pi (β := β) t))
⊢ ((insert a s).pi (β := β) t).val =
    val ((t a).biUnion fun (b : β a) ↦ image (Pi.cons (δ := β) s a b) (s.pi (β := β) t))

Tactic:
rw [← (pi (insert a s) t).2.dedup]

Premises used: Insert.insert, Finset.nodup, Finset.pi, Multiset.Nodup.dedup
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((insert a s).pi (β := β) t).val.dedup =
    val ((t a).biUnion fun (b : β a) ↦ image (Pi.cons (δ := β) s a b) (s.pi (β := β) t))

Tactic:
(fun s' (h : s' = a ::ₘ s.1) =>
        (?_ :
          dedup (Multiset.pi s' fun a => (t a).1) =
            dedup
              ((t a).1.bind fun b =>
                dedup <|
                  (Multiset.pi s.1 fun a : α => (t a).val).map fun f a' h' =>
                    Multiset.Pi.cons s.1 a b f a' (h ▸ h'))))
      _ (insert_val_of_notMem ha)

Premises used: Set.Mem, Finset.insert_val_of_notMem, Multiset.dedup, setOf, Multiset.recOn, Multiset.Mem, Finset.Pi.cons, Multiset.rec, Multiset.pi, Multiset.ndinsert
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
a₁ :
  ∀ (s' : Multiset α) (h : s' = a ::ₘ s.val),
    Eq (α := Multiset ((a : α) → a ∈ s' → β a)) (dedup (s'.pi (β := β) fun (a : α) ↦ (t a).val))
      (dedup
        ((t a).val.bind fun (b : β a) ↦
          dedup
            (Multiset.map
              (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ s') ↦ Multiset.Pi.cons (δ := β) s.val a b f a' ⋯)
              (s.val.pi (β := β) fun (a : α) ↦ (t a).val))))
⊢ ((insert a s).pi (β := β) t).val.dedup =
    val ((t a).biUnion fun (b : β a) ↦ image (Pi.cons (δ := β) s a b) (s.pi (β := β) t))

Tactic:
refine
    (fun s' (h : s' = a ::ₘ s.1) =>
        (?_ :
          dedup (Multiset.pi s' fun a => (t a).1) =
            dedup
              ((t a).1.bind fun b =>
                dedup <|
                  (Multiset.pi s.1 fun a : α => (t a).val).map fun f a' h' =>
                    Multiset.Pi.cons s.1 a b f a' (h ▸ h'))))
      _ (insert_val_of_notMem ha)

Premises used: Finset.insert_val_of_notMem
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
s' : Multiset α
h : s' = a ::ₘ s.val
a₁ :
  Eq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ s.val → β a_1)) (dedup ((a ::ₘ s.val).pi (β := β) fun (a : α) ↦ (t a).val))
    (dedup
      ((t a).val.bind fun (b : β a) ↦
        dedup
          (Multiset.map
            (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ a ::ₘ s.val) ↦
              Multiset.Pi.cons (δ := β) s.val a b f a' ⋯)
            (s.val.pi (β := β) fun (a : α) ↦ (t a).val))))
⊢ Eq (α := Multiset ((a : α) → a ∈ s' → β a)) (dedup (s'.pi (β := β) fun (a : α) ↦ (t a).val))
    (dedup
      ((t a).val.bind fun (b : β a) ↦
        dedup
          (Multiset.map
            (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ s') ↦ Multiset.Pi.cons (δ := β) s.val a b f a' ⋯)
            (s.val.pi (β := β) fun (a : α) ↦ (t a).val))))

Tactic:
subst s'
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
a₁ :
  Eq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ s.val → β a_1))
    (dedup
      ((t a).val.bind fun (b : β a) ↦
        Multiset.map (Multiset.Pi.cons (δ := β) s.val a b) (s.val.pi (β := β) fun (a : α) ↦ (t a).val)))
    (dedup
      ((t a).val.bind fun (b : β a) ↦
        dedup
          (Multiset.map
            (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ a ::ₘ s.val) ↦
              Multiset.Pi.cons (δ := β) s.val a b f a' ⋯)
            (s.val.pi (β := β) fun (a : α) ↦ (t a).val))))
⊢ Eq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ s.val → β a_1)) (dedup ((a ::ₘ s.val).pi (β := β) fun (a : α) ↦ (t a).val))
    (dedup
      ((t a).val.bind fun (b : β a) ↦
        dedup
          (Multiset.map
            (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ a ::ₘ s.val) ↦
              Multiset.Pi.cons (δ := β) s.val a b f a' ⋯)
            (s.val.pi (β := β) fun (a : α) ↦ (t a).val))))

Tactic:
rw [pi_cons]

Premises used: Multiset.pi_cons
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
a₁ :
  Eq (α := β a → Multiset ((a' : α) → a' ∈ a ::ₘ s.val → β a'))
    (fun (b : β a) ↦ Multiset.map (Multiset.Pi.cons (δ := β) s.val a b) (s.val.pi (β := β) fun (a : α) ↦ (t a).val))
    fun (b : β a) ↦
    dedup
      (Multiset.map
        (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ a ::ₘ s.val) ↦
          Multiset.Pi.cons (δ := β) s.val a b f a' ⋯)
        (s.val.pi (β := β) fun (a : α) ↦ (t a).val))
⊢ Eq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ s.val → β a_1))
    (dedup
      ((t a).val.bind fun (b : β a) ↦
        Multiset.map (Multiset.Pi.cons (δ := β) s.val a b) (s.val.pi (β := β) fun (a : α) ↦ (t a).val)))
    (dedup
      ((t a).val.bind fun (b : β a) ↦
        dedup
          (Multiset.map
            (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ a ::ₘ s.val) ↦
              Multiset.Pi.cons (δ := β) s.val a b f a' ⋯)
            (s.val.pi (β := β) fun (a : α) ↦ (t a).val))))

Tactic:
congr
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
a₁ :
  ∀ (b : β a),
    Multiset.map (Multiset.Pi.cons (δ := β) s.val a b) (s.val.pi (β := β) fun (a : α) ↦ (t a).val) =
      dedup
        (Multiset.map
          (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ a ::ₘ s.val) ↦
            Multiset.Pi.cons (δ := β) s.val a b f a' ⋯)
          (s.val.pi (β := β) fun (a : α) ↦ (t a).val))
⊢ Eq (α := β a → Multiset ((a' : α) → a' ∈ a ::ₘ s.val → β a'))
    (fun (b : β a) ↦ Multiset.map (Multiset.Pi.cons (δ := β) s.val a b) (s.val.pi (β := β) fun (a : α) ↦ (t a).val))
    fun (b : β a) ↦
    dedup
      (Multiset.map
        (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ a ::ₘ s.val) ↦
          Multiset.Pi.cons (δ := β) s.val a b f a' ⋯)
        (s.val.pi (β := β) fun (a : α) ↦ (t a).val))

Tactic:
funext b
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
b : β a
⊢ Multiset.map (Multiset.Pi.cons (δ := β) s.val a b) (s.val.pi (β := β) fun (a : α) ↦ (t a).val) =
    dedup
      (Multiset.map
        (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ a ::ₘ s.val) ↦
          Multiset.Pi.cons (δ := β) s.val a b f a' ⋯)
        (s.val.pi (β := β) fun (a : α) ↦ (t a).val))

Tactic:
((pi s t).nodup.map <| Multiset.Pi.cons_injective ha).dedup.symm

Premises used: Multiset.Nodup.map, Finset.nodup, Multiset.recOn, Multiset.rec, Finset.pi, Multiset.pi, Multiset.Nodup.dedup, Eq.symm, Multiset.Pi.cons_injective
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
b : β a
⊢ Multiset.map (Multiset.Pi.cons (δ := β) s.val a b) (s.val.pi (β := β) fun (a : α) ↦ (t a).val) =
    dedup
      (Multiset.map
        (fun (f : (a : α) → a ∈ s.val → β a) (a' : α) (h' : a' ∈ a ::ₘ s.val) ↦
          Multiset.Pi.cons (δ := β) s.val a b f a' ⋯)
        (s.val.pi (β := β) fun (a : α) ↦ (t a).val))

Tactic:
exact ((pi s t).nodup.map <| Multiset.Pi.cons_injective ha).dedup.symm

Premises used: Multiset.Nodup.map, Finset.nodup, Finset.pi, Multiset.Nodup.dedup, Eq.symm, Multiset.Pi.cons_injective
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : Type u_2
s : Finset α
f : α → β
⊢ Eq (α := Finset ((a : α) → a ∈ s → β)) (s.pi (β := fun (a : α) ↦ β) fun (a : α) ↦ {f a})
    {fun (a : α) (x : a ∈ s) ↦ f a}

Tactic:
grind
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : Type u_2
s : Finset α
i : β
⊢ Eq (α := Finset ((a : α) → a ∈ s → β)) (s.pi (β := fun (x : α) ↦ β) fun (x : α) ↦ {i}) {fun (x : α) (x_1 : x ∈ s) ↦ i}

Tactic:
pi_singletons s fun _ => i

Premises used: Finset.pi_singletons
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
β : α → Type u
inst : DecidableEq α
s : Finset α
t₁ t₂ : (a : α) → Finset (β a)
h : ∀ a ∈ s, t₁ a ⊆ t₂ a
⊢ s.pi (β := β) t₁ ⊆ s.pi (β := β) t₂

Tactic:
fun _ hg => mem_pi.2 fun a ha => h a ha (mem_pi.mp hg a ha)

Premises used: Iff.mpr, Finset.mem_pi, Iff.mp
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Type u_2
s : Finset α
t₁ t₂ : (a : α) → Finset (δ a)
a : α
ha : a ∈ s
h : Disjoint (t₁ a) (t₂ a)
⊢ Disjoint (s.pi (β := δ) t₁) (s.pi (β := δ) t₂)

Tactic:
disjoint_iff_ne.2 fun f₁ hf₁ f₂ hf₂ eq₁₂ =>
    disjoint_iff_ne.1 h (f₁ a ha) (mem_pi.mp hf₁ a ha) (f₂ a ha) (mem_pi.mp hf₂ a ha) <|
      congr_fun (congr_fun eq₁₂ a) ha

Premises used: Iff.mpr, Finset.disjoint_iff_ne, Finset.mem_pi, Iff.mp, congr_fun
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : DecidableEq (ι → α)
s : Finset α
f : ι → α
⊢ f ∈ s.piDiag ι ↔ ∃ a ∈ s, const ι a = f

Tactic:
mem_image

Premises used: Finset.mem_image, Set.Mem, setOf
-- Module: Mathlib.Data.Finset.Pi
Goal:
α : Type u_1
s : Finset α
ι : Type u_3
inst : DecidableEq (ι → α)
inst_1 : Nonempty ι
rw : #(image (const ι) s) = #s
rw₁ rw₂ : #s = #s
⊢ #(s.piDiag ι) = #s

Tactic:
rw [piDiag, card_image_of_injective _ const_injective]

Premises used: Finset.piDiag, Finset.card_image_of_injective, Function.const_injective
-- Module: Mathlib.Data.Finset.Pi
Goal:
ι : Type u_2
π : ι → Type u_3
s : Finset ι
⊢ Eq (α := (f : (i : ι) → π i) → (i : ↥s) → π (↑i : ι)) (s.restrict (π := π)) fun (f : (i : ι) → π i) (x : ↥s) ↦
    f (↑x : ι)

Tactic:
rfl

Premises used: Finset.restrict, rfl
-- Module: Mathlib.Data.Finset.Pi
Goal:
ι : Type u_2
π : ι → Type u_3
s : Finset ι
⊢ Eq (α := ((a : ι) → π a) → (b : ↥s) → π (↑b : ι))
    ((⇑(Equiv.piCongrLeft.{u_3 + 1, u_2 + 1, u_2 + 1} (fun (i : ↥s) ↦ π (↑i : ι)) s.equivToSet.symm :
            ((a : (↑(↑s : Set ι) : Type u_2)) →
                π (↑((s.equivToSet.symm : (a : (↑(↑s : Set ι) : Type u_2)) → ↥s) a) : ι)) ≃
              ((b : ↥s) → π (↑b : ι))) :
        (a :
            (a : (↑(↑s : Set ι) : Type u_2)) →
              π (↑((s.equivToSet.symm : (a : (↑(↑s : Set ι) : Type u_2)) → ↥s) a) : ι)) →
          (b : ↥s) → π (↑b : ι)) ∘
      (↑s : Set ι).restrict (π := π))
    (s.restrict (π := π))

Tactic:
rfl

Premises used: Finset.restrict, Set.restrict, rfl
-- Module: Mathlib.Data.Finset.Pi
Goal:
ι : Type u_2
π : ι → Type u_3
s : Finset ι
⊢ Eq (α := ((i : ι) → π i) → (b : ↥s) → π (↑b : ι))
    ((⇑(Equiv.piCongrLeft.{u_3 + 1, u_2 + 1, u_2 + 1} (fun (i : ↥s) ↦ π (↑i : ι)) s.equivToSet :
            ((a : ↥s) → π (↑((s.equivToSet : (a : ↥s) → ↥s) a) : ι)) ≃ ((b : ↥s) → π (↑b : ι))) :
        (a : (a : ↥s) → π (↑((s.equivToSet : (a : ↥s) → ↥s) a) : ι)) → (b : ↥s) → π (↑b : ι)) ∘
      s.restrict (π := π))
    ((↑s : Set ι).restrict (π := π))

Tactic:
rfl

Premises used: Finset.restrict, Set.restrict, rfl
-- Module: Mathlib.Data.Finset.Pi
Goal:
ι : Type u_2
π : ι → Type u_3
s t : Finset ι
hst : s ⊆ t
⊢ Eq (α := (f : (i : ↥t) → π (↑i : ι)) → (i : ↥s) → π (↑i : ι)) (restrict₂ (π := π) hst)
    fun (f : (i : ↥t) → π (↑i : ι)) (x : ↥s) ↦ f (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) (↑x : ι) ⋯)

Tactic:
rfl

Premises used: Finset.restrict₂, rfl
-- Module: Mathlib.Data.Finset.Pi
Goal:
ι : Type u_2
π : ι → Type u_3
s t : Finset ι
hst : s ⊆ t
⊢ Eq (α := ((i : ι) → π i) → (i : ↥s) → π (↑i : ι)) (restrict₂ (π := π) hst ∘ t.restrict (π := π)) (s.restrict (π := π))

Tactic:
rfl

Premises used: Finset.restrict, Finset.restrict₂, rfl
-- Module: Mathlib.Data.Finset.Pi
Goal:
ι : Type u_2
π : ι → Type u_3
s t u : Finset ι
hst : s ⊆ t
htu : t ⊆ u
⊢ Eq (α := ((i : ↥u) → π (↑i : ι)) → (i : ↥s) → π (↑i : ι)) (restrict₂ (π := π) hst ∘ restrict₂ (π := π) htu)
    (restrict₂ (π := π) ⋯)

Tactic:
rfl

Premises used: Finset.restrict₂, rfl
-- Module: Mathlib.Data.Finset.Pi
Goal:
ι : Type u_2
π : ι → Type u_3
s : Finset ι
⊢ DependsOn (α := π) (s.restrict (π := π)) (↑s : Set ι)

Tactic:
(s : Set ι).dependsOn_restrict

Premises used: Finset.restrict, Set.dependsOn_restrict, SetLike.coe, Set.restrict
-- Module: Mathlib.Data.Finset.Pi
Goal:
ι : Type u_2
π : ι → Type u_3
s : Finset ι
inst : DecidablePred fun (x : ι) ↦ x ∈ s
t : (i : ↥s) → Set (π (↑i : ι))
h :
  ∀ (x : (i : ι) → π i),
    x ∈ s.restrict (π := π) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ π (↑i : ι)) Set.univ t ↔
      Membership.mem (γ := Set ((i : ι) → π i))
        ((↑s : Set ι).pi (α := π) fun (i : ι) ↦
          if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ)
        x
⊢ s.restrict (π := π) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ π (↑i : ι)) Set.univ t =
    (↑s : Set ι).pi (α := π) fun (i : ι) ↦ if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ

Tactic:
ext
-- Module: Mathlib.Data.Finset.Pi
Goal:
ι : Type u_2
π : ι → Type u_3
s : Finset ι
inst : DecidablePred fun (x : ι) ↦ x ∈ s
t : (i : ↥s) → Set (π (↑i : ι))
x : (i : ι) → π i
⊢ x ∈ s.restrict (π := π) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ π (↑i : ι)) Set.univ t ↔
    Membership.mem (γ := Set ((i : ι) → π i))
      ((↑s : Set ι).pi (α := π) fun (i : ι) ↦
        if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ)
      x

Tactic:
simp_all
-- Module: Mathlib.Data.Finset.Pi
Goal:
ι : Type u_2
π : ι → Type u_3
inst : DecidableEq ι
I : Set ι
inst_1 : DecidablePred fun (x : ι) ↦ x ∈ I
s : Finset (↑I : Type u_2)
u : (i : (↑I : Type u_2)) → Set (π (↑i : ι))
⊢ I.restrict (π := π) ⁻¹' (↑s : Set (↑I : Type u_2)).pi (α := fun (a : (↑I : Type u_2)) ↦ π (↑a : ι)) u =
    (↑(image (Subtype.val (p := fun (x : ι) ↦ x ∈ I)) s) : Set ι).pi (α := π) fun (i : ι) ↦
      if h : i ∈ I then u (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h) else Set.univ

Tactic:
grind
-- Module: Mathlib.Data.Finset.Pi
Goal:
ι : Type u_2
π : ι → Type u_3
s t : Finset ι
inst : DecidablePred fun (x : ι) ↦ x ∈ s
hst : s ⊆ t
u : (i : ↥s) → Set (π (↑i : ι))
⊢ restrict₂ (π := π) hst ⁻¹' Set.pi (α := fun (i : ↥s) ↦ π (↑i : ι)) Set.univ u =
    Set.pi (α := fun (i : ↥t) ↦ π (↑i : ι)) Set.univ fun (j : ↥t) ↦
      if h : (↑j : ι) ∈ s then u (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑j : ι) h) else Set.univ

Tactic:
grind [restrict₂]

Premises used: Finset.restrict₂
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
f : (i : ι) → Finset (α i)
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
intro : ∀ (val : Fintype ι), p f
⊢ p f

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
f : (i : ι) → Finset (α i)
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
intro :
  ∀ (s : Finset ((i : ι) × α i))
    (ihs : ∀ t ⊂ s, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f)
    (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = s), p f
⊢ p f

Tactic:
induction hs : univ.sigma f using Finset.strongInductionOn generalizing f with | _ s ihs

Premises used: Finset.univ, Finset.sigma
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
s : Finset ((i : ι) × α i)
ihs : ∀ t ⊂ s, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
f : (i : ι) → Finset (α i)
hs : Finset.sigma (α := α) univ f = s
⊢ ∀ t ⊂ Finset.sigma (α := α) univ f, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f

Tactic:
subst s
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ Finset.sigma (α := α) univ f, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
intro : ∀ (he : Finset.sigma (α := α) univ f = ∅), p f
intro₁ : ∀ (hne : (Finset.sigma (α := α) univ f).Nonempty), p f
⊢ p f

Tactic:
rcases eq_empty_or_nonempty (univ.sigma f) with he | hne

Premises used: Finset.univ, Finset.sigma, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ Finset.sigma (α := α) univ f, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
he : Finset.sigma (α := α) univ f = ∅
⊢ p fun (x : ι) ↦ ∅

Tactic:
h0
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    r i x (g i) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
val : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ Finset.sigma (α := α) univ f, ∀ (f : (i : ι) → Finset (α i)) (hs : Finset.sigma (α := α) univ f = t), p f
he : Finset.sigma (α := α) univ f = ∅
h : f = fun (x : ι) ↦ ∅
⊢ p f

Tactic:
convert! h0 using 1