awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval
Goal:
α : Type u_1
inst : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
ih : ∏ m ∈ Icc (-(↑N : ℤ)) (↑N : ℤ), f m = HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1), f (↑m : ℤ)) 2 / f 0
⊢ Disjoint (α := Finset ℤ) (Icc (-(↑N : ℤ)) (↑N : ℤ)) {-HAdd.hAdd (α := ℤ) (↑N : ℤ) 1, HAdd.hAdd (α := ℤ) (↑N : ℤ) 1}

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

Tactic:
lia
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval
Goal:
α : Type u_1
inst : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
zero :
  ∏ m ∈ Icc (-(↑0 : ℤ)) (↑0 : ℤ), f m =
    HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (HAdd.hAdd (α := ℕ) 0 1), f (↑m : ℤ)) 2 / f 0
succ :
  ∀ (N : ℕ)
    (ih : ∏ m ∈ Icc (-(↑N : ℤ)) (↑N : ℤ), f m = HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1), f (↑m : ℤ)) 2 / f 0),
    ∏ m ∈ Icc (-(↑(N + 1) : ℤ)) (↑(N + 1) : ℤ), f m =
      HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1 + 1), f (↑m : ℤ)) 2 / f 0
⊢ ∏ m ∈ Icc (-(↑N : ℤ)) (↑N : ℤ), f m = HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1), f (↑m : ℤ)) 2 / f 0

Tactic:
induction N with
  | zero => simp [sq]
  | succ N ih =>
    rw [Nat.cast_add, Nat.cast_one, Icc_succ_succ, prod_union (by simp), prod_pair (by lia), ih,
      prod_range_succ _ (N + 1), hf, ← pow_two, div_mul_eq_mul_div, ← mul_pow, Nat.cast_succ]

Premises used: Nat.cast_succ, Finset.Icc_succ_succ, pow_two, Finset.prod_pair, Finset.prod_union, div_mul_eq_mul_div, sq, Nat.cast_add, HAdd.hAdd, Finset.prod_range_succ, OfNat.ofNat, mul_pow, Nat.cast_one
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval
Goal:
α : Type u_1
inst : CommMonoid α
f : ℤ → α
l u : ℤ
h : l ≤ u
⊢ ∏ m ∈ Icc l u, f m = (∏ m ∈ Ico l u, f m) * f u

Tactic:
simp [Icc_eq_cons_Ico h, mul_comm]

Premises used: mul_comm, Finset.Icc_eq_cons_Ico
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval
Goal:
R : Type u_1
inst : CommGroup R
f : ℤ → R
N : ℕ
zero :
  ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1), f m =
    f (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * ∏ m ∈ Icc (-(↑0 : ℤ)) (↑0 : ℤ), f m
succ :
  ∀ (n : ℕ),
    ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1), f m =
        f (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * ∏ m ∈ Icc (-(↑n : ℤ)) (↑n : ℤ), f m →
      ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1), f m =
        f (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) *
          ∏ m ∈ Icc (-(↑(n + 1) : ℤ)) (↑(n + 1) : ℤ), f m
⊢ ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑N : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑N : ℤ) 1), f m =
    f (HAdd.hAdd (α := ℤ) (↑N : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑N : ℤ) 1) * ∏ m ∈ Icc (-(↑N : ℤ)) (↑N : ℤ), f m

Tactic:
induction N
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval
Goal:
R : Type u_1
inst : CommGroup R
f : ℤ → R
zero :
  ∏ m ∈ Icc (-(↑0 : ℤ)) (↑0 : ℤ) ∪ {-HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1, HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1}, f m =
    f (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * ∏ m ∈ Icc (-(↑0 : ℤ)) (↑0 : ℤ), f m
⊢ ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1), f m =
    f (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * ∏ m ∈ Icc (-(↑0 : ℤ)) (↑0 : ℤ), f m

Tactic:
rw [Icc_succ_succ]

Premises used: Finset.Icc_succ_succ
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval
Goal:
R : Type u_1
inst : CommGroup R
f : ℤ → R
⊢ ∏ m ∈ Icc (-(↑0 : ℤ)) (↑0 : ℤ) ∪ {-HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1, HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1}, f m =
    f (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * ∏ m ∈ Icc (-(↑0 : ℤ)) (↑0 : ℤ), f m

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval
Goal:
R : Type u_1
inst : CommGroup R
f : ℤ → R
n : ℕ
h :
  ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1), f m =
    f (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * ∏ m ∈ Icc (-(↑n : ℤ)) (↑n : ℤ), f m
⊢ Disjoint (α := Finset ℤ) (Icc (-(↑(n + 1) : ℤ)) (↑(n + 1) : ℤ))
    {-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1, HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1}

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval
Goal:
R : Type u_1
inst : CommGroup R
f : ℤ → R
n : ℕ
h :
  ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1), f m =
    f (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * ∏ m ∈ Icc (-(↑n : ℤ)) (↑n : ℤ), f m
succ :
  HMul.hMul (α := R) (∏ x ∈ Icc (-(↑(n + 1) : ℤ)) (↑(n + 1) : ℤ), f x)
      (∏ x ∈ {-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1, HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1}, f x) =
    f (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) *
      ∏ m ∈ Icc (-(↑(n + 1) : ℤ)) (↑(n + 1) : ℤ), f m
⊢ ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1), f m =
    f (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) *
      ∏ m ∈ Icc (-(↑(n + 1) : ℤ)) (↑(n + 1) : ℤ), f m

Tactic:
rw [Icc_succ_succ, prod_union (by simp)]

Premises used: Finset.Icc_succ_succ, Finset.prod_union
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval
Goal:
R : Type u_1
inst : CommGroup R
f : ℤ → R
n : ℕ
h :
  ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1), f m =
    f (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * ∏ m ∈ Icc (-(↑n : ℤ)) (↑n : ℤ), f m
⊢ HMul.hMul (α := R) (∏ x ∈ Icc (-(↑(n + 1) : ℤ)) (↑(n + 1) : ℤ), f x)
      (∏ x ∈ {-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1, HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1}, f x) =
    f (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) *
      ∏ m ∈ Icc (-(↑(n + 1) : ℤ)) (↑(n + 1) : ℤ), f m

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval
Goal:
α : Type u_1
inst : CommGroup α
f : ℤ → α
⊢ ∏ n ∈ Ico (-(↑0 : ℤ)) (↑0 : ℤ), f n / f (n + 1) = f (-(↑0 : ℤ)) / f (↑0 : ℤ)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval
Goal:
α : Type u_1
inst : CommGroup α
f : ℤ → α
b : ℕ
ihb : ∏ n ∈ Ico (-(↑b : ℤ)) (↑b : ℤ), f n / f (n + 1) = f (-(↑b : ℤ)) / f (↑b : ℤ)
succ :
  ∏ x ∈ Ico (-(↑b : ℤ)) (↑b : ℤ) ∪ {-HAdd.hAdd (α := ℤ) (↑b : ℤ) 1, (↑b : ℤ)}, f x / f (x + 1) =
    f (-HAdd.hAdd (α := ℤ) (↑b : ℤ) 1) / f (HAdd.hAdd (α := ℤ) (↑b : ℤ) 1)
⊢ ∏ n ∈ Ico (-(↑(b + 1) : ℤ)) (↑(b + 1) : ℤ), f n / f (n + 1) = f (-(↑(b + 1) : ℤ)) / f (↑(b + 1) : ℤ)

Tactic:
simp only [Nat.cast_add_one, Ico_succ_succ]

Premises used: Finset.Ico_succ_succ, Nat.cast_add_one
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval
Goal:
α : Type u_1
inst : CommGroup α
f : ℤ → α
b : ℕ
ihb : ∏ n ∈ Ico (-(↑b : ℤ)) (↑b : ℤ), f n / f (n + 1) = f (-(↑b : ℤ)) / f (↑b : ℤ)
⊢ Disjoint (α := Finset ℤ) (Ico (-(↑b : ℤ)) (↑b : ℤ)) {-HAdd.hAdd (α := ℤ) (↑b : ℤ) 1, (↑b : ℤ)}

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval
Goal:
α : Type u_1
inst : CommGroup α
f : ℤ → α
b : ℕ
ihb : ∏ n ∈ Ico (-(↑b : ℤ)) (↑b : ℤ), f n / f (n + 1) = f (-(↑b : ℤ)) / f (↑b : ℤ)
⊢ -HAdd.hAdd (α := ℤ) (↑b : ℤ) 1 ∉ {(↑b : ℤ)}

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval
Goal:
α : Type u_1
inst : CommGroup α
f : ℤ → α
b : ℕ
ihb : ∏ n ∈ Ico (-(↑b : ℤ)) (↑b : ℤ), f n / f (n + 1) = f (-(↑b : ℤ)) / f (↑b : ℤ)
succ :
  f (-(↑b : ℤ)) / f (↑b : ℤ) * (f (-HAdd.hAdd (α := ℤ) (↑b : ℤ) 1) / f (-HAdd.hAdd (α := ℤ) (↑b : ℤ) 1 + 1)) *
        f (↑b : ℤ) /
      f (HAdd.hAdd (α := ℤ) (↑b : ℤ) 1) =
    f (-HAdd.hAdd (α := ℤ) (↑b : ℤ) 1) / f (HAdd.hAdd (α := ℤ) (↑b : ℤ) 1)
⊢ ∏ x ∈ Ico (-(↑b : ℤ)) (↑b : ℤ) ∪ {-HAdd.hAdd (α := ℤ) (↑b : ℤ) 1, (↑b : ℤ)}, f x / f (x + 1) =
    f (-HAdd.hAdd (α := ℤ) (↑b : ℤ) 1) / f (HAdd.hAdd (α := ℤ) (↑b : ℤ) 1)

Tactic:
rw [prod_union (by simp), prod_insert (by grind), prod_singleton, ihb, ← mul_assoc, mul_div]

Premises used: mul_div, Finset.prod_insert, Finset.prod_singleton, mul_assoc, Finset.prod_union
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval
Goal:
α : Type u_1
inst : CommGroup α
f : ℤ → α
b : ℕ
ihb : ∏ n ∈ Ico (-(↑b : ℤ)) (↑b : ℤ), f n / f (n + 1) = f (-(↑b : ℤ)) / f (↑b : ℤ)
⊢ f (-(↑b : ℤ)) / f (↑b : ℤ) * (f (-HAdd.hAdd (α := ℤ) (↑b : ℤ) 1) / f (-HAdd.hAdd (α := ℤ) (↑b : ℤ) 1 + 1)) *
        f (↑b : ℤ) /
      f (HAdd.hAdd (α := ℤ) (↑b : ℤ) 1) =
    f (-HAdd.hAdd (α := ℤ) (↑b : ℤ) 1) / f (HAdd.hAdd (α := ℤ) (↑b : ℤ) 1)

Tactic:
simp [mul_comm, mul_div, ← mul_assoc]

Premises used: mul_div, mul_assoc, mul_comm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval
Goal:
b : ℕ
α : Type u_1
inst : CommGroup α
f : ℤ → α
zero : ∏ n ∈ Ico (-(↑0 : ℤ)) (↑0 : ℤ), f n / f (n + 1) = f (-(↑0 : ℤ)) / f (↑0 : ℤ)
succ :
  ∀ (b : ℕ) (ihb : ∏ n ∈ Ico (-(↑b : ℤ)) (↑b : ℤ), f n / f (n + 1) = f (-(↑b : ℤ)) / f (↑b : ℤ)),
    ∏ n ∈ Ico (-(↑(b + 1) : ℤ)) (↑(b + 1) : ℤ), f n / f (n + 1) = f (-(↑(b + 1) : ℤ)) / f (↑(b + 1) : ℤ)
⊢ ∏ n ∈ Ico (-(↑b : ℤ)) (↑b : ℤ), f n / f (n + 1) = f (-(↑b : ℤ)) / f (↑b : ℤ)

Tactic:
induction b with
  | zero => simp
  | succ b ihb =>
    simp only [Nat.cast_add_one, Ico_succ_succ]
    rw [prod_union (by simp), prod_insert (by grind), prod_singleton, ihb, ← mul_assoc, mul_div]
    simp [mul_comm, mul_div, ← mul_assoc]

Premises used: mul_div, Finset.prod_insert, Finset.prod_singleton, mul_assoc, Finset.prod_union, Finset.Ico_succ_succ, mul_comm, Nat.cast_add_one
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : CommMonoid N
f : ι → M →* N
s : Finset ι
⊢ Eq (α := (a : M) → N) (⇑(∏ x ∈ s, f x) : (a : M) → N) (∏ x ∈ s, (⇑(f x) : (a : M) → N))

Tactic:
map_prod (MonoidHom.coeFn M N) _ _

Premises used: MonoidHom.coeFn, map_prod
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : MulOneClass M
inst_1 : CommMonoid N
f : ι → M →* N
s : Finset ι
b : M
⊢ Eq.{u_4 + 1} (α := N) ((∏ x ∈ s, f x : (a : M) → N) b : N) (∏ x ∈ s, (f x : (a : M) → N) b : N)

Tactic:
map_prod (MonoidHom.eval b) _ _

Premises used: map_prod, MonoidHom.eval, DFunLike.coe
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → κ → M
simp : ∀ (x : κ), (∀ (x_1 : ι) (x_2 : x_1 ∈ s), f x_1 x = 1) → Eq.{u_3 + 1} (α := M) (∏ i ∈ s, f i x) 1
⊢ Subset.{u_2} (α := Set κ) (mulSupport.{u_2, u_3} (M := M) fun (x : κ) ↦ ∏ i ∈ s, f i x) (⋃ i ∈ s, mulSupport (f i))

Tactic:
simp only [mulSupport_subset_iff', Set.mem_iUnion, not_exists, notMem_mulSupport]

Premises used: Set.mem_iUnion, Function.mulSupport_subset_iff', not_exists, Function.notMem_mulSupport
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → κ → M
⊢ ∀ (x : κ), (∀ (x_1 : ι) (x_2 : x_1 ∈ s), f x_1 x = 1) → Eq.{u_3 + 1} (α := M) (∏ i ∈ s, f i x) 1

Tactic:
fun x ↦ prod_eq_one

Premises used: Finset.prod_eq_one
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → κ → M
⊢ ∀ (x : κ), (∀ (x_1 : ι) (x_2 : x_1 ∈ s), f x_1 x = 1) → Eq.{u_3 + 1} (α := M) (∏ i ∈ s, f i x) 1

Tactic:
exact fun x ↦ prod_eq_one

Premises used: Finset.prod_eq_one
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
rw : ∃ (r : M), ∏ i ∈ s, f i = HPow.hPow (β := ℕ) r 2
⊢ IsSquare.{u_3} (α := M) (∏ i ∈ s, f i)

Tactic:
rw [isSquare_iff_exists_sq]

Premises used: isSquare_iff_exists_sq
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
h₁ :
  ∏ i ∈ s, f i =
    HPow.hPow (α := M) (β := ℕ) (∏ x : ↥s, ⋯.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2)) 2
⊢ ∃ (r : M), ∏ i ∈ s, f i = HPow.hPow (β := ℕ) r 2

Tactic:
use (∏ (x : s), ((isSquare_iff_exists_sq _).mp (h _ x.2)).choose)

Premises used: Finset.univ, isSquare_iff_exists_sq, Finset.prod, Iff.mp, Exists.choose, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
h₁ :
  Eq.{u_3 + 1} (α := M) (∏ i : ↥s, f (↑i : ι))
    (∏ x : ↥s,
      ⋯.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2) *
        ⋯.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2))
⊢ ∏ i ∈ s, f i =
    HPow.hPow (α := M) (β := ℕ) (∏ x : ↥s, ⋯.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2)) 2

Tactic:
rw [@sq, ← Finset.prod_mul_distrib, ← Finset.prod_coe_sort]

Premises used: Finset.prod_mul_distrib, Finset.prod_coe_sort, sq
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
h₁ :
  Eq (α := ↥s → M) (fun (i : ↥s) ↦ f (↑i : ι)) fun (x : ↥s) ↦
    ⋯.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2) *
      ⋯.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2)
⊢ Eq.{u_3 + 1} (α := M) (∏ i : ↥s, f (↑i : ι))
    (∏ x : ↥s,
      ⋯.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2) *
        ⋯.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2))

Tactic:
congr
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
h₁ :
  ∀ (i : ↥s),
    f (↑i : ι) =
      ⋯.choose (p := fun (r : M) ↦ f (↑i : ι) = HPow.hPow (β := ℕ) r 2) *
        ⋯.choose (p := fun (r : M) ↦ f (↑i : ι) = HPow.hPow (β := ℕ) r 2)
⊢ Eq (α := ↥s → M) (fun (i : ↥s) ↦ f (↑i : ι)) fun (x : ↥s) ↦
    ⋯.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2) *
      ⋯.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2)

Tactic:
ext i
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
i : ↥s
h₁ : f (↑i : ι) = HPow.hPow (β := ℕ) (⋯.choose (p := fun (r : M) ↦ f (↑i : ι) = HPow.hPow (β := ℕ) r 2)) 2
⊢ f (↑i : ι) =
    ⋯.choose (p := fun (r : M) ↦ f (↑i : ι) = HPow.hPow (β := ℕ) r 2) *
      ⋯.choose (p := fun (r : M) ↦ f (↑i : ι) = HPow.hPow (β := ℕ) r 2)

Tactic:
rw [← @sq]

Premises used: sq
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
i : ↥s
⊢ f (↑i : ι) = HPow.hPow (β := ℕ) (⋯.choose (p := fun (r : M) ↦ f (↑i : ι) = HPow.hPow (β := ℕ) r 2)) 2

Tactic:
((isSquare_iff_exists_sq _).mp (h _ i.2)).choose_spec

Premises used: Exists.choose_spec, isSquare_iff_exists_sq, Iff.mp, Subtype.property
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
i : ↥s
⊢ f (↑i : ι) = HPow.hPow (β := ℕ) (⋯.choose (p := fun (r : M) ↦ f (↑i : ι) = HPow.hPow (β := ℕ) r 2)) 2

Tactic:
exact ((isSquare_iff_exists_sq _).mp (h _ i.2)).choose_spec

Premises used: Exists.choose_spec, isSquare_iff_exists_sq, Iff.mp, Subtype.property
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Pi
Goal:
ι : Type u_1
β : Type u_2
inst : CommMonoid β
inst_1 : DecidableEq ι
inst_2 : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → Membership.mem (γ := Finset ι) univ i → κ i) → β
hi :
  ∀ (a : (a : ι) → Membership.mem (γ := Finset ι) univ a → κ a),
    Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t) a →
      (fun (i : ι) ↦ a i ⋯) ∈ Fintype.piFinset (δ := κ) t
hj :
  ∀ a ∈ Fintype.piFinset (δ := κ) t,
    Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t)
      fun (i : ι) (x : Membership.mem (γ := Finset ι) univ i) ↦ a i
left_inv :
  ∀ (a : (a : ι) → Membership.mem (γ := Finset ι) univ a → κ a),
    Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t) a →
      (fun (i : ι) (x : Membership.mem (γ := Finset ι) univ i) ↦ (fun (i : ι) ↦ a i ⋯) i) = a
right_inv :
  ∀ a ∈ Fintype.piFinset (δ := κ) t,
    (fun (i : ι) ↦ (fun (i : ι) (x : Membership.mem (γ := Finset ι) univ i) ↦ a i) i ⋯) = a
h :
  ∀ (a : (a : ι) → Membership.mem (γ := Finset ι) univ a → κ a),
    Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t) a →
      f a = f fun (a_2 : ι) (x : Membership.mem (γ := Finset ι) univ a_2) ↦ (fun (i : ι) ↦ a i ⋯) a_2
⊢ Eq.{u_2 + 1} (α := β) (∏ x ∈ pi (β := κ) univ t, f x)
    (∏ x ∈ Fintype.piFinset (δ := κ) t, f fun (a : ι) (x_1 : Membership.mem (γ := Finset ι) univ a) ↦ x a)

Tactic:
apply prod_nbij' (fun x i ↦ x i <| mem_univ _) (fun x i _ ↦ x i)

Premises used: Finset.prod_nbij'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Pi
Goal:
ι : Type u_1
β : Type u_2
inst : CommMonoid β
inst_1 : DecidableEq ι
inst_2 : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → Membership.mem (γ := Finset ι) univ i → κ i) → β
⊢ ∀ (a : (a : ι) → Membership.mem (γ := Finset ι) univ a → κ a),
    Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t) a →
      (fun (i : ι) ↦ a i ⋯) ∈ Fintype.piFinset (δ := κ) t

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Pi
Goal:
ι : Type u_1
β : Type u_2
inst : CommMonoid β
inst_1 : DecidableEq ι
inst_2 : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → Membership.mem (γ := Finset ι) univ i → κ i) → β
⊢ ∀ a ∈ Fintype.piFinset (δ := κ) t,
    Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t)
      fun (i : ι) (x : Membership.mem (γ := Finset ι) univ i) ↦ a i

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Pi
Goal:
ι : Type u_1
β : Type u_2
inst : CommMonoid β
inst_1 : DecidableEq ι
inst_2 : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → Membership.mem (γ := Finset ι) univ i → κ i) → β
⊢ ∀ (a : (a : ι) → Membership.mem (γ := Finset ι) univ a → κ a),
    Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t) a →
      (fun (i : ι) (x : Membership.mem (γ := Finset ι) univ i) ↦ (fun (i : ι) ↦ a i ⋯) i) = a

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Pi
Goal:
ι : Type u_1
β : Type u_2
inst : CommMonoid β
inst_1 : DecidableEq ι
inst_2 : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → Membership.mem (γ := Finset ι) univ i → κ i) → β
⊢ ∀ a ∈ Fintype.piFinset (δ := κ) t,
    (fun (i : ι) ↦ (fun (i : ι) (x : Membership.mem (γ := Finset ι) univ i) ↦ a i) i ⋯) = a

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Pi
Goal:
ι : Type u_1
β : Type u_2
inst : CommMonoid β
inst_1 : DecidableEq ι
inst_2 : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → Membership.mem (γ := Finset ι) univ i → κ i) → β
⊢ ∀ (a : (a : ι) → Membership.mem (γ := Finset ι) univ a → κ a),
    Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t) a →
      f a = f fun (a_2 : ι) (x : Membership.mem (γ := Finset ι) univ a_2) ↦ (fun (i : ι) ↦ a i ⋯) a_2

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
β : Type u_4
γ : Type u_5
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : DecidablePred fun (x : ι) ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | p x})
⊢ p (↑x : ι)

Tactic:
simpa using (mem_filter.mp x.2).2

Premises used: And.right, Iff.mp, Finset.mem_filter, Subtype.property
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
β : Type u_4
γ : Type u_5
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : DecidablePred fun (x : ι) ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | ¬p x})
⊢ ¬p (↑x : ι)

Tactic:
simpa using (mem_filter.mp x.2).2

Premises used: And.right, Iff.mp, Finset.mem_filter, Subtype.property
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : DecidablePred fun (x : ι) ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | p x})
⊢ p (↑x : ι)

Tactic:
simpa using (mem_filter.mp x.2).2

Premises used: And.right, Iff.mp, Finset.mem_filter, Subtype.property
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : DecidablePred fun (x : ι) ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | ¬p x})
⊢ ¬p (↑x : ι)

Tactic:
simpa using (mem_filter.mp x.2).2

Premises used: And.right, Iff.mp, Finset.mem_filter, Subtype.property
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : DecidablePred fun (x : ι) ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | p x})
_hx : Membership.mem (γ := Finset ↥({x ∈ s | p x})) univ x
⊢ p (↑x : ι)

Tactic:
simpa using (mem_filter.mp x.2).2

Premises used: And.right, Iff.mp, Finset.mem_filter, Subtype.property
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : DecidablePred fun (x : ι) ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | ¬p x})
_hx : Membership.mem (γ := Finset ↥({x ∈ s | ¬p x})) univ x
⊢ ¬p (↑x : ι)

Tactic:
simpa using (mem_filter.mp x.2).2

Premises used: And.right, Iff.mp, Finset.mem_filter, Subtype.property
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
γ : Type u_5
inst : CommMonoid M
s : Finset ι
p : ι → Prop
inst_1 : DecidablePred p
f g : ι → γ
h : γ → M
⊢ ∏ x ∈ s, h (if p x then f x else g x) = HMul.hMul (α := M) (∏ x ∈ s with p x, h (f x)) (∏ x ∈ s with ¬p x, h (g x))

Tactic:
(prod_apply_dite _ _ _).trans <| congr_arg₂ _ (prod_attach _ (h ∘ f)) (prod_attach _ (h ∘ g))

Premises used: Function.comp, Finset.prod_apply_dite, Finset.prod_attach, Eq.trans, congr_arg₂, ite
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
β : Type u_4
γ : Type u_5
s_1 : Finset ι
inst : CommMonoid M
s : Finset ι
p : ι → Prop
inst_1 : DecidablePred p
f : (x : ι) → p x → M
g : (x : ι) → ¬p x → M
x : ↥({x ∈ s | p x})
⊢ p (↑x : ι)

Tactic:
simpa using (mem_filter.mp x.2).2

Premises used: And.right, Iff.mp, Finset.mem_filter, Subtype.property
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
β : Type u_4
γ : Type u_5
s_1 : Finset ι
inst : CommMonoid M
s : Finset ι
p : ι → Prop
inst_1 : DecidablePred p
f : (x : ι) → p x → M
g : (x : ι) → ¬p x → M
x : ↥({x ∈ s | ¬p x})
⊢ ¬p (↑x : ι)

Tactic:
simpa using (mem_filter.mp x.2).2

Premises used: And.right, Iff.mp, Finset.mem_filter, Subtype.property
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
p : ι → Prop
inst_1 : DecidablePred p
f : (x : ι) → p x → M
g : (x : ι) → ¬p x → M
⊢ (∏ x ∈ s, if hx : p x then f x hx else g x hx) =
    HMul.hMul (α := M) (∏ x : ↥({x ∈ s | p x}), f (↑x : ι) ⋯) (∏ x : ↥({x ∈ s | ¬p x}), g (↑x : ι) ⋯)

Tactic:
simp [prod_apply_dite _ _ fun x => x]

Premises used: Finset.prod_apply_dite