awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
hi : ∀ (a : ℕ) (ha : a ∈ range k), ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1) ∈ F
i_inj :
  ∀ (a₁ : ℕ) (ha₁ : a₁ ∈ range k) (a₂ : ℕ) (ha₂ : a₂ ∈ range k),
    ((p (↑a₁ : Fin (k + 1))).2, (p (↑a₁.succ : Fin (k + 1))).1) =
        ((p (↑a₂ : Fin (k + 1))).2, (p (↑a₂.succ : Fin (k + 1))).1) →
      a₁ = a₂
i_surj : ∀ b ∈ F, ∃ (a : ℕ) (_ : a ∈ range k), ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1) = b
h₁ :
  ∀ (a : ℕ) (ha : a ∈ range k),
    f (p (↑a : Fin (k + 1))).2 (p (↑a.succ : Fin (k + 1))).1 =
      f ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1).1
        ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1).2
⊢ Eq.{u_2 + 1} (α := β) (∏ i ∈ range k, f (p (↑i : Fin (k + 1))).2 (p (↑i.succ : Fin (k + 1))).1) (∏ z ∈ F, f z.1 z.2)

Tactic:
apply prod_bij (fun (i : ℕ) hi ↦ ((p i).2, (p i.succ).1))

Premises used: Prod.mk, Nat.cast, Prod.fst, Nat.succ, Prod.snd, Finset.prod_bij
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
i : ℕ
h_1 : i ∈ range k
⊢ i ∈ Set.Iio k

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
⊢ ∀ (a : ℕ) (ha : a ∈ range k), ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1) ∈ F

Tactic:
exact fun i _ ↦ F.intervalGapsWithin_mapsTo h a b (x := i) (by grind)

Premises used: Finset.intervalGapsWithin_mapsTo
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
i : ℕ
hi : i ∈ range k
j : ℕ
hj : j ∈ range k
hij :
  ((p (↑i : Fin (k + 1))).2, (p (↑i.succ : Fin (k + 1))).1) = ((p (↑j : Fin (k + 1))).2, (p (↑j.succ : Fin (k + 1))).1)
i_inj :
  ∀ (hi : i < k) (j : ℕ) (hj : j < k)
    (hij :
      ((p (↑i : Fin (k + 1))).2, (p (↑i.succ : Fin (k + 1))).1) =
        ((p (↑j : Fin (k + 1))).2, (p (↑j.succ : Fin (k + 1))).1)),
    i = j
⊢ i = j

Tactic:
rw [mem_range] at hi hj

Premises used: Finset.mem_range
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
i : ℕ
hi : i < k
j : ℕ
hj : j < k
hij :
  ((p (↑i : Fin (k + 1))).2, (p (↑i.succ : Fin (k + 1))).1) = ((p (↑j : Fin (k + 1))).2, (p (↑j.succ : Fin (k + 1))).1)
i_inj : i ∈ Set.Iio k
i_inj₁ : j ∈ Set.Iio k
i_inj₂ :
  Eq.{u_1 + 1} (α := α × α)
    ((fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
      i)
    ((fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
      j)
⊢ i = j

Tactic:
apply F.intervalGapsWithin_injOn h a b

Premises used: Finset.intervalGapsWithin_injOn
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
i : ℕ
hi : i < k
j : ℕ
hj : j < k
hij :
  ((p (↑i : Fin (k + 1))).2, (p (↑i.succ : Fin (k + 1))).1) = ((p (↑j : Fin (k + 1))).2, (p (↑j.succ : Fin (k + 1))).1)
⊢ i ∈ Set.Iio k

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
i : ℕ
hi : i < k
j : ℕ
hj : j < k
hij :
  ((p (↑i : Fin (k + 1))).2, (p (↑i.succ : Fin (k + 1))).1) = ((p (↑j : Fin (k + 1))).2, (p (↑j.succ : Fin (k + 1))).1)
⊢ j ∈ Set.Iio k

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
i : ℕ
hi : i < k
j : ℕ
hj : j < k
hij :
  ((p (↑i : Fin (k + 1))).2, (p (↑i.succ : Fin (k + 1))).1) = ((p (↑j : Fin (k + 1))).2, (p (↑j.succ : Fin (k + 1))).1)
⊢ Eq.{u_1 + 1} (α := α × α)
    ((fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
      i)
    ((fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
      j)

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
z : α × α
hz : z ∈ F
i_surj :
  ∀ (i : ℕ) (hi₁ : i ∈ Set.Iio k)
    (hi₂ :
      (fun (j : ℕ) ↦
            ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
          i =
        z),
    ∃ (a : ℕ) (_ : a ∈ range k), ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1) = z
⊢ ∃ (a : ℕ) (_ : a ∈ range k), ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1) = z

Tactic:
obtain ⟨i, hi₁, hi₂⟩ := F.intervalGapsWithin_surjOn h a b hz

Premises used: Finset.intervalGapsWithin_surjOn
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
z : α × α
hz : z ∈ F
i : ℕ
hi₁ : i ∈ Set.Iio k
hi₂ :
  (fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
      i =
    z
⊢ i ∈ range k

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
z : α × α
hz : z ∈ F
i : ℕ
hi₁ : i ∈ Set.Iio k
hi₂ :
  (fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
      i =
    z
⊢ ∃ (a : ℕ) (_ : a ∈ range k), ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1) = z

Tactic:
exact ⟨i, by grind, hi₂⟩
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
⊢ ∀ (a : ℕ) (ha : a ∈ range k),
    f (p (↑a : Fin (k + 1))).2 (p (↑a.succ : Fin (k + 1))).1 =
      f ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1).1
        ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1).2

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
rw :
  g (F.intervalGapsWithin h a b (↑k : Fin (k + 1))).1 / g (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).1 *
      (g (F.intervalGapsWithin h a b (↑k : Fin (k + 1))).2 / g (F.intervalGapsWithin h a b (↑k : Fin (k + 1))).1) =
    g b / g a
⊢ HMul.hMul (α := β)
      (∏ i ∈ range (k + 1),
        g (F.intervalGapsWithin h a b (↑i : Fin (k + 1))).2 / g (F.intervalGapsWithin h a b (↑i : Fin (k + 1))).1)
      (∏ z ∈ F, g z.2 / g z.1) =
    g b / g a

Tactic:
rw [F.prod_eq_prod_range_intervalGapsWithin h (fun x y ↦ g y / g x), mul_comm,
      prod_range_succ, ← mul_assoc,
      ← prod_mul_distrib,
      prod_congr rfl (fun _ _ ↦ div_mul_div_cancel _ _ _),
      prod_range_div (fun i ↦ g (F.intervalGapsWithin h a b i).1)]

Premises used: Finset.prod_mul_distrib, Finset.prod_range_div, mul_assoc, Finset.intervalGapsWithin, HDiv.hDiv, Finset.prod_eq_prod_range_intervalGapsWithin, Finset.prod_congr, Nat.cast, Prod.fst, mul_comm, Finset.prod_range_succ, rfl, div_mul_div_cancel
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ g (F.intervalGapsWithin h a b (↑k : Fin (k + 1))).1 / g (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).1 *
      (g (F.intervalGapsWithin h a b (↑k : Fin (k + 1))).2 / g (F.intervalGapsWithin h a b (↑k : Fin (k + 1))).1) =
    g b / g a

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ ∏ i ∈ range (k + 1),
      g (F.intervalGapsWithin h a b (↑i : Fin (k + 1))).2 / g (F.intervalGapsWithin h a b (↑i : Fin (k + 1))).1 =
    g b / g a / ∏ z ∈ F, g z.2 / g z.1

Tactic:
eq_div_iff_mul_eq'.mpr (F.prod_intervalGapsWithin_mul_prod_eq_div h g)

Premises used: Iff.mpr, Finset.prod_intervalGapsWithin_mul_prod_eq_div, eq_div_iff_mul_eq'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : CommMonoid β
inst_1 : One α
f : ι → α
g : ι → α → β
s t : Finset ι
h : s ⊆ t
hg : ∀ (a : ι), g a 1 = 1
i : ι
h_1 : i ∈ t
hn : i ∉ s
⊢ g i ((↑s : Set ι).mulIndicator f i) = 1

Tactic:
simp [hn, hg]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : CommMonoid β
inst_1 : One α
f : ι → α
g : ι → α → β
s t : Finset ι
h : s ⊆ t
hg : ∀ (a : ι), g a 1 = 1
rw rw₁ :
  Eq.{u_4 + 1} (α := β) (∏ i ∈ t, g i ((↑s : Set ι).mulIndicator f i)) (∏ x ∈ t, g x ((↑s : Set ι).mulIndicator f x))
⊢ Eq.{u_4 + 1} (α := β) (∏ i ∈ t, g i ((↑s : Set ι).mulIndicator f i)) (∏ i ∈ s, g i ((↑s : Set ι).mulIndicator f i))

Tactic:
rw [prod_subset h fun i _ hn ↦ by simp [hn, hg]]

Premises used: Finset.prod_subset
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : CommMonoid β
inst_1 : One α
f : ι → α
g : ι → α → β
s t : Finset ι
h : s ⊆ t
hg : ∀ (a : ι), g a 1 = 1
⊢ Eq.{u_4 + 1} (α := β) (∏ i ∈ s, g i ((↑s : Set ι).mulIndicator f i)) (∏ i ∈ s, g i (f i))

Tactic:
prod_congr rfl fun i hi ↦ congr_arg _ <| mulIndicator_of_mem hi f

Premises used: Finset.prod_congr, congr_arg, Set.mulIndicator_of_mem, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : CommMonoid β
inst_1 : One α
f : ι → α
g : ι → α → β
s t : Finset ι
h : s ⊆ t
hg : ∀ (a : ι), g a 1 = 1
_ : Eq.{u_4 + 1} (α := β) (∏ i ∈ t, g i ((↑s : Set ι).mulIndicator f i)) (∏ i ∈ s, g i ((↑s : Set ι).mulIndicator f i))
⊢ Eq.{u_4 + 1} (α := β) (∏ i ∈ t, g i ((↑s : Set ι).mulIndicator f i)) (∏ i ∈ s, g i (f i))

Tactic:
calc
    _ = ∏ i ∈ s, g i (mulIndicator ↑s f i) := by rw [prod_subset h fun i _ hn ↦ by simp [hn, hg]]
    _ = _ := prod_congr rfl fun i hi ↦ congr_arg _ <| mulIndicator_of_mem hi f

Premises used: Finset.prod_congr, congr_arg, Set.mulIndicator_of_mem, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
β : Type u_4
inst : CommMonoid β
f : ι → β
s t : Finset ι
h : s ⊆ t
⊢ Eq.{u_4 + 1} (α := β) (∏ i ∈ t, (↑s : Set ι).mulIndicator f i) (∏ i ∈ s, f i)

Tactic:
prod_mulIndicator_subset_of_eq_one _ (fun _ ↦ id) h fun _ ↦ rfl

Premises used: Set.mulIndicator, Finset.prod_mulIndicator_subset_of_eq_one, id, rfl, ite
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
s : Finset ι
f : ι → κ → β
t : ι → Set κ
g : ι → κ
inst_1 : DecidablePred fun (i : ι) ↦ g i ∈ t i
⊢ Eq.{u_4 + 1} (α := β) (∏ i ∈ s, (t i).mulIndicator (f i) (g i)) (∏ i ∈ s with g i ∈ t i, f i (g i))

Tactic:
(prod_filter_mul_prod_filter_not s (fun i ↦ g i ∈ t i) _).symm.trans <|
     Eq.trans (congr_arg₂ (· * ·) ?_ ?_) (mul_one _)

Premises used: HMul.hMul, Membership.mem, Finset.prod_filter_mul_prod_filter_not, mul_one, Eq.symm, Eq.trans, congr_arg₂
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
s : Finset ι
f : ι → κ → β
t : ι → Set κ
g : ι → κ
inst_1 : DecidablePred fun (i : ι) ↦ g i ∈ t i
refine_1 :
  Eq.{u_4 + 1} (α := β) (∏ x ∈ s with g x ∈ t x, (t x).mulIndicator (f x) (g x)) (∏ i ∈ s with g i ∈ t i, f i (g i))
refine_2 : Eq.{u_4 + 1} (α := β) (∏ x ∈ s with g x ∉ t x, (t x).mulIndicator (f x) (g x)) 1
⊢ Eq.{u_4 + 1} (α := β) (∏ i ∈ s, (t i).mulIndicator (f i) (g i)) (∏ i ∈ s with g i ∈ t i, f i (g i))

Tactic:
refine (prod_filter_mul_prod_filter_not s (fun i ↦ g i ∈ t i) _).symm.trans <|
     Eq.trans (congr_arg₂ (· * ·) ?_ ?_) (mul_one _)

Premises used: HMul.hMul, Membership.mem, Finset.prod_filter_mul_prod_filter_not, mul_one, Eq.symm, Eq.trans, congr_arg₂
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
s : Finset ι
f : ι → κ → β
t : ι → Set κ
g : ι → κ
inst_1 : DecidablePred fun (i : ι) ↦ g i ∈ t i
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s with g x ∈ t x, (t x).mulIndicator (f x) (g x)) (∏ i ∈ s with g i ∈ t i, f i (g i))

Tactic:
prod_congr rfl fun x hx ↦ mulIndicator_of_mem (mem_filter.1 hx).2 _

Premises used: Finset.prod_congr, And.right, Iff.mp, Finset.mem_filter, Set.mulIndicator_of_mem, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
s : Finset ι
f : ι → κ → β
t : ι → Set κ
g : ι → κ
inst_1 : DecidablePred fun (i : ι) ↦ g i ∈ t i
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s with g x ∈ t x, (t x).mulIndicator (f x) (g x)) (∏ i ∈ s with g i ∈ t i, f i (g i))

Tactic:
exact prod_congr rfl fun x hx ↦ mulIndicator_of_mem (mem_filter.1 hx).2 _

Premises used: Finset.prod_congr, And.right, Iff.mp, Finset.mem_filter, Set.mulIndicator_of_mem, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
s : Finset ι
f : ι → κ → β
t : ι → Set κ
g : ι → κ
inst_1 : DecidablePred fun (i : ι) ↦ g i ∈ t i
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s with g x ∉ t x, (t x).mulIndicator (f x) (g x)) 1

Tactic:
prod_eq_one fun x hx ↦ mulIndicator_of_notMem (mem_filter.1 hx).2 _

Premises used: Finset.prod_eq_one, Set.mulIndicator_of_notMem, And.right, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
s : Finset ι
f : ι → κ → β
t : ι → Set κ
g : ι → κ
inst_1 : DecidablePred fun (i : ι) ↦ g i ∈ t i
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s with g x ∉ t x, (t x).mulIndicator (f x) (g x)) 1

Tactic:
exact prod_eq_one fun x hx ↦ mulIndicator_of_notMem (mem_filter.1 hx).2 _

Premises used: Finset.prod_eq_one, Set.mulIndicator_of_notMem, And.right, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
β : Type u_4
inst : CommMonoid β
inst_1 : DecidableEq ι
s t : Finset ι
f : ι → β
rw : Eq.{u_4 + 1} (α := β) (∏ i ∈ s with i ∈ (↑t : Set ι), f i) (∏ i ∈ s with i ∈ t, f i)
⊢ Eq.{u_4 + 1} (α := β) (∏ i ∈ s, (↑t : Set ι).mulIndicator f i) (∏ i ∈ s ∩ t, f i)

Tactic:
rw [← filter_mem_eq_inter, prod_mulIndicator_eq_prod_filter]

Premises used: Finset.prod_mulIndicator_eq_prod_filter, Finset.filter_mem_eq_inter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
β : Type u_4
inst : CommMonoid β
inst_1 : DecidableEq ι
s t : Finset ι
f : ι → β
⊢ Eq.{u_4 + 1} (α := β) (∏ i ∈ s with i ∈ (↑t : Set ι), f i) (∏ i ∈ s with i ∈ t, f i)

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
s : Finset ι
t : Set κ
f : ι → κ → β
⊢ Eq (α := (x : κ) → β) (t.mulIndicator (∏ i ∈ s, f i)) (∏ i ∈ s, t.mulIndicator (f i))

Tactic:
map_prod (mulIndicatorHom _ _) _ _

Premises used: Set.mulIndicatorHom, Set.mulIndicator, map_prod, ite
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
t : ι → Set κ
f : κ → β
hs : (↑∅ : Set ι).PairwiseDisjoint t
⊢ mulIndicator (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), t i) f = fun (a : κ) ↦
    ∏ i ∈ ∅, (t i).mulIndicator f a

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hs : (↑s : Set ι).PairwiseDisjoint t),
    mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑(Finset.cons i s hi) : Set ι).PairwiseDisjoint t
cons :
  ∀ (j : κ), mulIndicator (⋃ i_1 ∈ Finset.cons i s hi, t i_1) f j = ∏ i ∈ Finset.cons i s hi, (t i).mulIndicator f j
⊢ mulIndicator (⋃ i_1 ∈ Finset.cons i s hi, t i_1) f = fun (a : κ) ↦ ∏ i ∈ Finset.cons i s hi, (t i).mulIndicator f a

Tactic:
ext j
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hs : (↑s : Set ι).PairwiseDisjoint t),
    mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑(Finset.cons i s hi) : Set ι).PairwiseDisjoint t
j : κ
cons :
  ∀ (hs : (↑s : Set ι).PairwiseDisjoint t ∧ ∀ j ∈ (↑s : Set ι), Disjoint (t i) (t j)) (j : κ),
    mulIndicator (⋃ i_1 ∈ Finset.cons i s hi, t i_1) f j = ∏ i ∈ Finset.cons i s hi, (t i).mulIndicator f j
⊢ mulIndicator (⋃ i_1 ∈ Finset.cons i s hi, t i_1) f j = ∏ i ∈ Finset.cons i s hi, (t i).mulIndicator f j

Tactic:
rw [coe_cons, Set.pairwiseDisjoint_insert_of_notMem (Finset.mem_coe.not.2 hi)] at hs

Premises used: Iff.mpr, Finset.coe_cons, Set.pairwiseDisjoint_insert_of_notMem, Iff.not, Finset.mem_coe
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hs : (↑s : Set ι).PairwiseDisjoint t),
    mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s : Set ι).PairwiseDisjoint t ∧ ∀ j ∈ (↑s : Set ι), Disjoint (t i) (t j)
j : κ
cons : j ∉ t i ∩ ⋃ x ∈ s, t x
⊢ mulIndicator (⋃ i_1 ∈ Finset.cons i s hi, t i_1) f j = ∏ i ∈ Finset.cons i s hi, (t i).mulIndicator f j

Tactic:
rw [prod_cons, cons_eq_insert, set_biUnion_insert, mulIndicator_union_of_notMem_inter, ih hs.1]

Premises used: Set.mulIndicator_union_of_notMem_inter, And.left, Finset.cons_eq_insert, Finset.prod_cons, Finset.set_biUnion_insert
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hs : (↑s : Set ι).PairwiseDisjoint t),
    mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s : Set ι).PairwiseDisjoint t ∧ ∀ j ∈ (↑s : Set ι), Disjoint (t i) (t j)
j : κ
⊢ j ∉ t i ∩ ⋃ x ∈ s, t x

Tactic:
(Set.disjoint_iff.mp (Set.disjoint_iUnion₂_right.mpr hs.2) ·)

Premises used: Iff.mpr, Set.Mem, Set.disjoint_iUnion₂_right, And.right, Iff.mp, Not, Set.disjoint_iff
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hs : (↑s : Set ι).PairwiseDisjoint t),
    mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s : Set ι).PairwiseDisjoint t ∧ ∀ j ∈ (↑s : Set ι), Disjoint (t i) (t j)
j : κ
⊢ j ∉ t i ∩ ⋃ x ∈ s, t x

Tactic:
exact (Set.disjoint_iff.mp (Set.disjoint_iUnion₂_right.mpr hs.2) ·)

Premises used: Iff.mpr, Set.disjoint_iUnion₂_right, And.right, Iff.mp, Set.disjoint_iff
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hs : (↑s : Set ι).PairwiseDisjoint t),
    mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s : Set ι).PairwiseDisjoint t ∧ ∀ j ∈ (↑s : Set ι), Disjoint (t i) (t j)
j : κ
cons : mulIndicator (⋃ i_1 ∈ Finset.cons i s hi, t i_1) f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
cons₁ : mulIndicator (⋃ i_1 ∈ insert i s, t i_1) f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
cons₂ : (t i ∪ ⋃ x ∈ s, t x).mulIndicator f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
cons₃ :
  (t i).mulIndicator f j * mulIndicator (⋃ x ∈ s, t x) f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
cons₄ : j ∉ t i ∩ ⋃ x ∈ s, t x
cons₅ :
  (t i).mulIndicator f j * (fun (a : κ) ↦ (∏ i ∈ s, (t i).mulIndicator f a : β)) j =
    (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
cons₆ : j ∉ t i ∩ ⋃ x ∈ s, t x
cons₇ :
  (t i).mulIndicator f j * (fun (a : κ) ↦ (∏ i ∈ s, (t i).mulIndicator f a : β)) j =
    (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
cons₈ cons₉ : j ∉ t i ∩ ⋃ x ∈ s, t x
⊢ mulIndicator (⋃ i_1 ∈ Finset.cons i s hi, t i_1) f j = ∏ i ∈ Finset.cons i s hi, (t i).mulIndicator f j

Tactic:
classical
    rw [prod_cons, cons_eq_insert, set_biUnion_insert, mulIndicator_union_of_notMem_inter, ih hs.1]
    exact (Set.disjoint_iff.mp (Set.disjoint_iUnion₂_right.mpr hs.2) ·)

Premises used: Iff.mpr, Set.disjoint_iUnion₂_right, Set.mulIndicator_union_of_notMem_inter, And.right, And.left, Finset.cons_eq_insert, Iff.mp, Finset.prod_cons, Finset.set_biUnion_insert, Set.disjoint_iff
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
s : Finset ι
t : ι → Set κ
f : κ → β
hs : (↑s : Set ι).PairwiseDisjoint t
empty :
  ∀ (hs : (↑∅ : Set ι).PairwiseDisjoint t),
    mulIndicator (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), t i) f = fun (a : κ) ↦
      ∏ i ∈ ∅, (t i).mulIndicator f a
cons :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (ih :
      ∀ (hs : (↑s : Set ι).PairwiseDisjoint t),
        mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a)
    (hs : (↑(Finset.cons i s hi) : Set ι).PairwiseDisjoint t),
    mulIndicator (⋃ i_1 ∈ Finset.cons i s hi, t i_1) f = fun (a : κ) ↦ ∏ i ∈ Finset.cons i s hi, (t i).mulIndicator f a
⊢ mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons i s hi ih =>
    ext j
    rw [coe_cons, Set.pairwiseDisjoint_insert_of_notMem (Finset.mem_coe.not.2 hi)] at hs
    classical
    rw [prod_cons, cons_eq_insert, set_biUnion_insert, mulIndicator_union_of_notMem_inter, ih hs.1]
    exact (Set.disjoint_iff.mp (Set.disjoint_iUnion₂_right.mpr hs.2) ·)

Premises used: Finset.cons, Finset.coe_cons, Set.mulIndicator_union_of_notMem_inter, Finset.cons_eq_insert, Finset.prod_cons, Finset.set_biUnion_insert
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
s : Finset ι
t : ι → Set κ
f : κ → β
h : (↑s : Set ι).PairwiseDisjoint t
x : κ
rw rw₁ :
  Eq.{u_4 + 1} (α := β) ((fun (a : κ) ↦ (∏ i ∈ s, (t i).mulIndicator f a : β)) x) (∏ i ∈ s, (t i).mulIndicator f x)
⊢ mulIndicator (⋃ i ∈ s, t i) f x = ∏ i ∈ s, (t i).mulIndicator f x

Tactic:
rw [mulIndicator_biUnion s t h]

Premises used: Finset.mulIndicator_biUnion
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval
Goal:
α : Type u_1
inst : CommGroup α
f : ℤ → α
hf : Function.Even f
⊢ ∏ m ∈ Icc (-(↑0 : ℤ)) (↑0 : ℤ), f m =
    HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (HAdd.hAdd (α := ℕ) 0 1), f (↑m : ℤ)) 2 / f 0

Tactic:
simp [sq]

Premises used: sq