awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
iv : ℕ
ih :
  ∀ {n : Fin iv → ℕ} (k : (i : Fin iv) × Fin (n i)),
    (↑((finSigmaFinEquiv : (a : (i : Fin iv) × Fin (n i)) → Fin (∑ i : Fin iv, n i)) k) : ℕ) =
      ∑ i : Fin (↑k.fst : ℕ), n (Fin.castLE ⋯ i) + (↑(k.snd (β := fun (i : Fin iv) ↦ Fin (n i))) : ℕ)
n : Fin (iv + 1) → ℕ
hi : iv < iv + 1
j : Fin (n ⟨iv, hi⟩)
⊢ (↑(Sum.elim (Fin.castAdd (n (Fin.last iv))) (Fin.natAdd (∑ i : Fin iv, n i.castSucc))
          ((Equiv.sumCongr finSigmaFinEquiv (Equiv.uniqueSigma fun (i : Fin 1) ↦ Fin (n (Fin.natAdd iv i))) :
              (a : (i : Fin iv) × Fin (n (Fin.castAdd 1 i)) ⊕ (i : Fin 1) × Fin (n (Fin.natAdd iv i))) →
                Fin (∑ i : Fin iv, n i.castSucc) ⊕ Fin (n (Fin.last iv)))
            ((Equiv.sumSigmaDistrib fun (a : Fin iv ⊕ Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a)) :
                  (a : (a : Fin iv ⊕ Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a))) →
                    (i : Fin iv) × Fin (n (Fin.castAdd 1 i)) ⊕ (i : Fin 1) × Fin (n (Fin.natAdd iv i)))
                (Sigma.mk (β := fun (a : Fin iv ⊕ Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a)))
                  (Sum.inr 0) j) :
              (i : Fin iv) × Fin (n (Fin.castAdd 1 i)) ⊕ (i : Fin 1) × Fin (n (Fin.natAdd iv i))))) :
      ℕ) =
    ∑ x : Fin iv, n (Fin.castLE ⋯ x) + (↑j : ℕ)

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
m : ℕ
n : Fin m → ℕ
k : (i : Fin m) × Fin (n i)
zero :
  ∀ {n : Fin 0 → ℕ} (k : (i : Fin 0) × Fin (n i)),
    (↑((finSigmaFinEquiv : (a : (i : Fin 0) × Fin (n i)) → Fin (∑ i : Fin 0, n i)) k) : ℕ) =
      ∑ i : Fin (↑k.fst : ℕ), n (Fin.castLE ⋯ i) + (↑(k.snd (β := fun (i : Fin 0) ↦ Fin (n i))) : ℕ)
succ :
  ∀ (m : ℕ)
    (ih :
      ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)),
        (↑((finSigmaFinEquiv : (a : (i : Fin m) × Fin (n i)) → Fin (∑ i : Fin m, n i)) k) : ℕ) =
          ∑ i : Fin (↑k.fst : ℕ), n (Fin.castLE ⋯ i) + (↑(k.snd (β := fun (i : Fin m) ↦ Fin (n i))) : ℕ))
    {n : Fin (m + 1) → ℕ} (k : (i : Fin (m + 1)) × Fin (n i)),
    (↑((finSigmaFinEquiv : (a : (i : Fin (m + 1)) × Fin (n i)) → Fin (∑ i : Fin (m + 1), n i)) k) : ℕ) =
      ∑ i : Fin (↑k.fst : ℕ), n (Fin.castLE ⋯ i) + (↑(k.snd (β := fun (i : Fin (m + 1)) ↦ Fin (n i))) : ℕ)
⊢ (↑((finSigmaFinEquiv : (a : (i : Fin m) × Fin (n i)) → Fin (∑ i : Fin m, n i)) k) : ℕ) =
    ∑ i : Fin (↑k.fst : ℕ), n (Fin.castLE ⋯ i) + (↑(k.snd (β := fun (i : Fin m) ↦ Fin (n i))) : ℕ)

Tactic:
induction m with
  | zero => exact k.fst.elim0
  | succ m ih =>
  rcases k with ⟨⟨iv, hi⟩, j⟩
  rw [finSigmaFinEquiv]
  unfold finSumFinEquiv
  simp only [Equiv.coe_fn_mk, Equiv.sigmaCongrLeft, Equiv.coe_fn_symm_mk, Equiv.trans_def,
    Equiv.trans_apply, finCongr_apply, Fin.val_cast]
  by_cases him : iv < m
  · conv in Sigma.mk _ _ =>
      equals ⟨Sum.inl ⟨iv, him⟩, j⟩ => simp [Fin.addCases, him]
    simpa using ih _
  · replace him := Nat.eq_of_lt_succ_of_not_lt hi him
    subst him
    conv in Sigma.mk _ _ =>
      equals ⟨Sum.inr 0, j⟩ => simp [Fin.addCases, Fin.natAdd]
    simp
    rfl

Premises used: finCongr_apply, Fin.natAdd, Equiv.coe_fn_symm_mk, Equiv.trans_apply, Equiv.sigmaCongrLeft, Equiv.trans_def, finSigmaFinEquiv, finSumFinEquiv, Equiv.coe_fn_mk, Fin.val_cast, Sigma.mk
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
n : Fin 1 → ℕ
ij : (i : Fin 1) × Fin (n i)
rw : Eq (α := ℕ) (∑ i : Fin (↑ij.fst : ℕ), n (Fin.castLE ⋯ i)) 0
⊢ (↑((finSigmaFinEquiv : (a : (i : Fin 1) × Fin (n i)) → Fin (∑ i : Fin 1, n i)) ij) : ℕ) =
    (↑(ij.snd (β := fun (i : Fin 1) ↦ Fin (n i))) : ℕ)

Tactic:
rw [finSigmaFinEquiv_apply, add_eq_right]

Premises used: finSigmaFinEquiv_apply, add_eq_right
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
n : Fin 1 → ℕ
ij : (i : Fin 1) × Fin (n i)
⊢ IsEmpty (Fin (↑(ij.fst (β := fun (i : Fin 1) ↦ Fin (n i))) : ℕ))

Tactic:
simpa using Fin.isEmpty'

Premises used: Fin.isEmpty'
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
n : Fin 1 → ℕ
ij : (i : Fin 1) × Fin (n i)
⊢ Eq (α := ℕ) (∑ i : Fin (↑ij.fst : ℕ), n (Fin.castLE ⋯ i)) 0

Tactic:
apply @Finset.sum_of_isEmpty _ _ _ _ (by simpa using Fin.isEmpty')

Premises used: Finset.sum_of_isEmpty
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
⊢ (take 0 (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < 0, f j

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
pos : ∀ (h : i < n), (take (i + 1) (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i + 1, f j
neg : ∀ (h : ¬i < n), (take (i + 1) (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i + 1, f j
⊢ (take (i + 1) (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i + 1, f j

Tactic:
by_cases h : i < n
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h rwa rwa₁ rwa₂ rwa₃ : i < n
⊢ i < (ofFn f).length

Tactic:
rwa [length_ofFn]

Premises used: List.length_ofFn
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : i < n
⊢ i < (ofFn f).length

Tactic:
have : i < length (ofFn f) := by rwa [length_ofFn]
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : i < n
this : i < (ofFn f).length
pos :
  (take i (ofFn f)).prod * getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) (ofFn f) i this =
    ∏ j : Fin n with (↑j : ℕ) < i + 1, f j
⊢ (take (i + 1) (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i + 1, f j

Tactic:
rw [prod_take_succ _ _ this]

Premises used: List.prod_take_succ
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : i < n
this : i < (ofFn f).length
⊢ Eq (α := Finset (Fin n)) {j : Fin n | (↑j : ℕ) < i + 1} (insert (⟨i, h⟩ : Fin n) {j : Fin n | (↑j : ℕ) < i})

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : i < n
this : i < (ofFn f).length
⊢ Eq (α := Finset (Fin n)) {j : Fin n | (↑j : ℕ) < i + 1} (insert (⟨i, h⟩ : Fin n) {j : Fin n | (↑j : ℕ) < i})

Tactic:
have A : ({j | j.val < i + 1} : Finset (Fin n)) =
          insert ⟨i, h⟩ ({j | Fin.val j < i} : Finset (Fin n)) := by grind
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : i < n
this : i < (ofFn f).length
A : Eq (α := Finset (Fin n)) {j : Fin n | (↑j : ℕ) < i + 1} (insert (⟨i, h⟩ : Fin n) {j : Fin n | (↑j : ℕ) < i})
⊢ (take i (ofFn f)).prod * getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) (ofFn f) i this =
    ∏ j : Fin n with (↑j : ℕ) < i + 1, f j

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : ¬i < n
⊢ ¬i < (ofFn f).length

Tactic:
rw [← length_ofFn (f := f)] at h

Premises used: List.length_ofFn
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : ¬i < (ofFn f).length
⊢ (ofFn f).length ≤ i

Tactic:
have : length (ofFn f) ≤ i := not_lt.mp h
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : ¬i < (ofFn f).length
this : (ofFn f).length ≤ i
rw : ofFn f = take i.succ (ofFn f)
rw₁ rw₂ : ofFn f = ofFn f
⊢ take i (ofFn f) = take i.succ (ofFn f)

Tactic:
rw [take_of_length_le this, take_of_length_le (le_trans this (Nat.le_succ _))]

Premises used: List.take_of_length_le, Nat.le_succ, le_trans
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : ¬i < n
⊢ take i (ofFn f) = take i.succ (ofFn f)

Tactic:
have A : (ofFn f).take i = (ofFn f).take i.succ := by
        rw [← length_ofFn (f := f)] at h
        have : length (ofFn f) ≤ i := not_lt.mp h
        rw [take_of_length_le this, take_of_length_le (le_trans this (Nat.le_succ _))]
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : ¬i < n
A : take i (ofFn f) = take i.succ (ofFn f)
j : Fin n
⊢ (↑j : ℕ) < i

Tactic:
have : (j : ℕ) < i := lt_of_lt_of_le j.2 (not_lt.mp h)
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : ¬i < n
A : take i (ofFn f) = take i.succ (ofFn f)
j : Fin n
this : (↑j : ℕ) < i
⊢ ((↑j : ℕ) < i.succ) = ((↑j : ℕ) < i)

Tactic:
simp [this, lt_trans this (Nat.lt_succ_self _)]

Premises used: lt_trans, Nat.lt_succ_self
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : ¬i < n
A : take i (ofFn f) = take i.succ (ofFn f)
⊢ ∀ (j : Fin n), ((↑j : ℕ) < i.succ) = ((↑j : ℕ) < i)

Tactic:
have B : ∀ j : Fin n, ((j : ℕ) < i.succ) = ((j : ℕ) < i) := by
        intro j
        have : (j : ℕ) < i := lt_of_lt_of_le j.2 (not_lt.mp h)
        simp [this, lt_trans this (Nat.lt_succ_self _)]
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : ¬i < n
A : take i (ofFn f) = take i.succ (ofFn f)
B : ∀ (j : Fin n), ((↑j : ℕ) < i.succ) = ((↑j : ℕ) < i)
⊢ (take (i + 1) (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i + 1, f j

Tactic:
simp [← A, B, IH]
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
zero : (take 0 (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < 0, f j
succ :
  ∀ (i : ℕ) (IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j),
    (take (i + 1) (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i + 1, f j
⊢ (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j

Tactic:
induction i with
  | zero =>
    simp
  | succ i IH =>
    by_cases h : i < n
    · have : i < length (ofFn f) := by rwa [length_ofFn]
      rw [prod_take_succ _ _ this]
      have A : ({j | j.val < i + 1} : Finset (Fin n)) =
          insert ⟨i, h⟩ ({j | Fin.val j < i} : Finset (Fin n)) := by grind
      grind
    · have A : (ofFn f).take i = (ofFn f).take i.succ := by
        rw [← length_ofFn (f := f)] at h
        have : length (ofFn f) ≤ i := not_lt.mp h
        rw [take_of_length_le this, take_of_length_le (le_trans this (Nat.le_succ _))]
      have B : ∀ j : Fin n, ((j : ℕ) < i.succ) = ((j : ℕ) < i) := by
        intro j
        have : (j : ℕ) < i := lt_of_lt_of_le j.2 (not_lt.mp h)
        simp [this, lt_trans this (Nat.lt_succ_self _)]
      simp [← A, B, IH]
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
⊢ (ofFn f).prod = ∏ i : Fin n, f i

Tactic:
Fin.prod_ofFn f

Premises used: Fin.prod_ofFn
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
G : Type u_3
inst : DivisionCommMonoid G
rw :
  ∀ (x : Fin (length.{u_3} (α := G) [])),
    Membership.mem (γ := Finset (Fin (length.{u_3} (α := G) []))) univ x →
      getElem (valid := fun (xs : List G) (i : Fin (length.{u_3} (α := G) [])) ↦ (↑i : ℕ) < xs.length) [] x ⋯ ^
          HPow.hPow (α := ℤ) (-1) (↑x : ℕ) =
        1
⊢ Eq.{u_3 + 1} (α := G) (alternatingProd [])
    (∏ i : Fin [].length,
      getElem (valid := fun (xs : List G) (i : Fin (length.{u_3} (α := G) [])) ↦ (↑i : ℕ) < xs.length) [] i ⋯ ^
        HPow.hPow (α := ℤ) (-1) (↑i : ℕ))

Tactic:
rw [alternatingProd, Finset.prod_eq_one]

Premises used: Finset.prod_eq_one, List.alternatingProd
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
G : Type u_3
inst : DivisionCommMonoid G
g : G
change :
  g =
    ∏ i : Fin 1,
      getElem (valid := fun (xs : List G) (i : Fin 1) ↦ (↑i : ℕ) < xs.length) [g] i ⋯ ^ HPow.hPow (α := ℤ) (-1) (↑i : ℕ)
⊢ [g].alternatingProd =
    ∏ i : Fin [g].length,
      getElem (valid := fun (xs : List G) (i : Fin [g].length) ↦ (↑i : ℕ) < xs.length) [g] i ⋯ ^
        HPow.hPow (α := ℤ) (-1) (↑i : ℕ)

Tactic:
change g = ∏ i : Fin 1, [g][i] ^ (-1 : ℤ) ^ (i : ℕ)

Premises used: OfNat.ofNat, Fin, Neg.neg
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
G : Type u_3
inst : DivisionCommMonoid G
g : G
rw :
  g =
    getElem (valid := fun (xs : List G) (i : Fin 1) ↦ (↑i : ℕ) < xs.length) [g] 0 ⋯ ^ HPow.hPow (α := ℤ) (-1) (↑0 : ℕ) *
      ∏ i : Fin 0,
        getElem (valid := fun (xs : List G) (i : Fin 1) ↦ (↑i : ℕ) < xs.length) [g] i.succ ⋯ ^
          HPow.hPow (α := ℤ) (-1) (↑i.succ : ℕ)
⊢ g =
    ∏ i : Fin 1,
      getElem (valid := fun (xs : List G) (i : Fin 1) ↦ (↑i : ℕ) < xs.length) [g] i ⋯ ^ HPow.hPow (α := ℤ) (-1) (↑i : ℕ)

Tactic:
rw [Fin.prod_univ_succ]

Premises used: Fin.prod_univ_succ
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
G : Type u_3
inst : DivisionCommMonoid G
g : G
⊢ g =
    getElem (valid := fun (xs : List G) (i : Fin 1) ↦ (↑i : ℕ) < xs.length) [g] 0 ⋯ ^ HPow.hPow (α := ℤ) (-1) (↑0 : ℕ) *
      ∏ i : Fin 0,
        getElem (valid := fun (xs : List G) (i : Fin 1) ↦ (↑i : ℕ) < xs.length) [g] i.succ ⋯ ^
          HPow.hPow (α := ℤ) (-1) (↑i.succ : ℕ)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
G : Type u_3
inst : DivisionCommMonoid G
g h : G
L : List G
rw :
  g *
      (h⁻¹ *
        ∏ i : Fin L.length,
          getElem (valid := fun (xs : List G) (i : Fin L.length) ↦ (↑i : ℕ) < xs.length) L i ⋯ ^
            HPow.hPow (α := ℤ) (-1) (↑i : ℕ)) =
    getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) 0 ⋯ ^
        HPow.hPow (α := ℤ) (-1) (↑0 : ℕ) *
      (getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) (Fin.succ 0)
            ⋯ ^
          HPow.hPow (α := ℤ) (-1) (↑(Fin.succ 0) : ℕ) *
        ∏ i : Fin L.length,
          getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) i.succ.succ
              ⋯ ^
            HPow.hPow (α := ℤ) (-1) (↑i.succ.succ : ℕ))
⊢ g * h⁻¹ *
      ∏ i : Fin L.length,
        getElem (valid := fun (xs : List G) (i : Fin L.length) ↦ (↑i : ℕ) < xs.length) L i ⋯ ^
          HPow.hPow (α := ℤ) (-1) (↑i : ℕ) =
    ∏ i : Fin (L.length + 2),
      getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) i ⋯ ^
        HPow.hPow (α := ℤ) (-1) (↑i : ℕ)

Tactic:
rw [Fin.prod_univ_succ, Fin.prod_univ_succ, mul_assoc]

Premises used: mul_assoc, Fin.prod_univ_succ
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
G : Type u_3
inst : DivisionCommMonoid G
g h : G
L : List G
⊢ g *
      (h⁻¹ *
        ∏ i : Fin L.length,
          getElem (valid := fun (xs : List G) (i : Fin L.length) ↦ (↑i : ℕ) < xs.length) L i ⋯ ^
            HPow.hPow (α := ℤ) (-1) (↑i : ℕ)) =
    getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) 0 ⋯ ^
        HPow.hPow (α := ℤ) (-1) (↑0 : ℕ) *
      (getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) (Fin.succ 0)
            ⋯ ^
          HPow.hPow (α := ℤ) (-1) (↑(Fin.succ 0) : ℕ) *
        ∏ i : Fin L.length,
          getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) i.succ.succ
              ⋯ ^
            HPow.hPow (α := ℤ) (-1) (↑i.succ.succ : ℕ))

Tactic:
simp [pow_add]

Premises used: pow_add
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
G : Type u_3
inst : DivisionCommMonoid G
g h : G
L : List G
rw :
  g * h⁻¹ *
      ∏ i : Fin L.length,
        getElem (valid := fun (xs : List G) (i : Fin L.length) ↦ (↑i : ℕ) < xs.length) L i ⋯ ^
          HPow.hPow (α := ℤ) (-1) (↑i : ℕ) =
    getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) 0 ⋯ ^
        HPow.hPow (α := ℤ) (-1) (↑0 : ℕ) *
      ∏ i : Fin (L.length + 1),
        getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) i.succ ⋯ ^
          HPow.hPow (α := ℤ) (-1) (↑i.succ : ℕ)
rw₁ :
  g * h⁻¹ *
      ∏ i : Fin L.length,
        getElem (valid := fun (xs : List G) (i : Fin L.length) ↦ (↑i : ℕ) < xs.length) L i ⋯ ^
          HPow.hPow (α := ℤ) (-1) (↑i : ℕ) =
    getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) 0 ⋯ ^
        HPow.hPow (α := ℤ) (-1) (↑0 : ℕ) *
      (getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) (Fin.succ 0)
            ⋯ ^
          HPow.hPow (α := ℤ) (-1) (↑(Fin.succ 0) : ℕ) *
        ∏ i : Fin L.length,
          getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) i.succ.succ
              ⋯ ^
            HPow.hPow (α := ℤ) (-1) (↑i.succ.succ : ℕ))
rw₂ rw₃ rw₄ :
  g *
      (h⁻¹ *
        ∏ i : Fin L.length,
          getElem (valid := fun (xs : List G) (i : Fin L.length) ↦ (↑i : ℕ) < xs.length) L i ⋯ ^
            HPow.hPow (α := ℤ) (-1) (↑i : ℕ)) =
    getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) 0 ⋯ ^
        HPow.hPow (α := ℤ) (-1) (↑0 : ℕ) *
      (getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) (Fin.succ 0)
            ⋯ ^
          HPow.hPow (α := ℤ) (-1) (↑(Fin.succ 0) : ℕ) *
        ∏ i : Fin L.length,
          getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) i.succ.succ
              ⋯ ^
            HPow.hPow (α := ℤ) (-1) (↑i.succ.succ : ℕ))
⊢ g * h⁻¹ *
      ∏ i : Fin L.length,
        getElem (valid := fun (xs : List G) (i : Fin L.length) ↦ (↑i : ℕ) < xs.length) L i ⋯ ^
          HPow.hPow (α := ℤ) (-1) (↑i : ℕ) =
    ∏ i : Fin (L.length + 2),
      getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) i ⋯ ^
        HPow.hPow (α := ℤ) (-1) (↑i : ℕ)

Tactic:
{ rw [Fin.prod_univ_succ, Fin.prod_univ_succ, mul_assoc]
          simp [pow_add]}

Premises used: mul_assoc, pow_add, Fin.prod_univ_succ
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
hf : HasFiniteMulSupport (f ∘ PLift.down)
s : Finset (PLift α)
hs : Finite.toFinset (s := mulSupport (f ∘ PLift.down)) hf ⊆ s
rw :
  Eq.{u_2 + 1} (α := M)
    (∏ i ∈ Finite.toFinset (s := mulSupport.{u_4, u_2} (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)) hf, f i.down)
    (∏ i ∈ s, f i.down)
⊢ Eq.{u_2 + 1} (α := M) (∏ᶠ (i : α), f i) (∏ i ∈ s, f i.down)

Tactic:
rw [finprod, dif_pos hf]

Premises used: dif_pos, finprod
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
hf : HasFiniteMulSupport (f ∘ PLift.down)
s : Finset (PLift α)
hs : Finite.toFinset (s := mulSupport (f ∘ PLift.down)) hf ⊆ s
⊢ Eq.{u_2 + 1} (α := M)
    (∏ i ∈ Finite.toFinset (s := mulSupport.{u_4, u_2} (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)) hf, f i.down)
    (∏ i ∈ s, f i.down)

Tactic:
Finset.prod_subset hs fun x _ hxf => ?_

Premises used: Finset.prod_subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
hf : HasFiniteMulSupport (f ∘ PLift.down)
s : Finset (PLift α)
hs : Finite.toFinset (s := mulSupport (f ∘ PLift.down)) hf ⊆ s
refine :
  ∀ x ∈ s,
    ∀ (hxf : x ∉ Finite.toFinset (s := mulSupport.{u_4, u_2} (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)) hf),
      f x.down = 1
⊢ Eq.{u_2 + 1} (α := M)
    (∏ i ∈ Finite.toFinset (s := mulSupport.{u_4, u_2} (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)) hf, f i.down)
    (∏ i ∈ s, f i.down)

Tactic:
refine Finset.prod_subset hs fun x _ hxf => ?_

Premises used: Finset.prod_subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
hf : HasFiniteMulSupport (f ∘ PLift.down)
s : Finset (PLift α)
hs : Finite.toFinset (s := mulSupport (f ∘ PLift.down)) hf ⊆ s
x : PLift α
h : x ∈ s
hxf : x ∉ Finite.toFinset (s := mulSupport.{u_4, u_2} (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)) hf
rwa : ∀ (hxf : x ∉ mulSupport (f ∘ PLift.down)), f x.down = 1
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hxf : (f ∘ PLift.down) x = 1), f x.down = 1
⊢ f x.down = 1

Tactic:
rwa [hf.mem_toFinset, notMem_mulSupport] at hxf

Premises used: Set.Finite.mem_toFinset, Function.notMem_mulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
s : Finset (PLift α)
hs : mulSupport (f ∘ PLift.down) ⊆ (↑s : Set (PLift α))
x : PLift α
hx : x ∈ ⋯.toFinset (s := mulSupport (f ∘ PLift.down))
⊢ x ∈ mulSupport (f ∘ PLift.down)

Tactic:
rw [Finite.mem_toFinset] at hx

Premises used: Set.Finite.mem_toFinset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
s : Finset (PLift α)
hs : mulSupport (f ∘ PLift.down) ⊆ (↑s : Set (PLift α))
x : PLift α
hx : x ∈ mulSupport (f ∘ PLift.down)
⊢ x ∈ s

Tactic:
hs hx
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
s : Finset (PLift α)
hs : mulSupport (f ∘ PLift.down) ⊆ (↑s : Set (PLift α))
x : PLift α
hx : x ∈ mulSupport (f ∘ PLift.down)
⊢ x ∈ s

Tactic:
exact hs hx
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
x : PLift α
h :
  Membership.mem (γ := Set (PLift α))
    (mulSupport.{u_4, u_2} (M := M) fun (x : PLift α) ↦ (fun (x : α) ↦ (1 : M)) x.down) x
⊢ x ∈ (↑∅ : Set (PLift α))

Tactic:
simp at h
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
⊢ (mulSupport.{u_4, u_2} (M := M) fun (x : PLift α) ↦ (fun (x : α) ↦ (1 : M)) x.down) ⊆ (↑∅ : Set (PLift α))

Tactic:
have : (mulSupport fun x : PLift α => (fun _ => 1 : α → M) x.down) ⊆ (∅ : Finset (PLift α)) :=
    fun x h => by simp at h
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
this : (mulSupport.{u_4, u_2} (M := M) fun (x : PLift α) ↦ (fun (x : α) ↦ (1 : M)) x.down) ⊆ (↑∅ : Set (PLift α))
rw : Eq.{u_2 + 1} (α := M) (∏ i ∈ ∅, 1) 1
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) 1 1
⊢ Eq.{u_2 + 1} (α := M) (∏ᶠ (x : α), 1) 1

Tactic:
rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_empty]

Premises used: Finset.prod_empty, finprod_eq_prod_plift_of_mulSupport_subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
inst_1 : IsEmpty α
f : α → M
rw : Eq.{u_2 + 1} (α := M) (∏ᶠ (i : α), f i) (∏ᶠ (x : α), 1)
rw₁ : Sort u_4
⊢ Eq.{u_2 + 1} (α := M) (∏ᶠ (i : α), f i) 1

Tactic:
rw [← finprod_one]

Premises used: finprod_one
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
inst_1 : IsEmpty α
f : α → M
⊢ Eq (α := α → M) (fun (i : α) ↦ f i) fun (x : α) ↦ 1

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
inst : CommMonoid M
f : False → M
⊢ Eq.{u_2 + 1} (α := M) (∏ᶠ (i : False), f i) 1

Tactic:
finprod_of_isEmpty _

Premises used: finprod_of_isEmpty
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
x : PLift α
contrapose : x ∉ (↑{{ down := a : PLift α }} : Set (PLift α)) → x ∉ mulSupport (f ∘ PLift.down)
⊢ x ∈ mulSupport (f ∘ PLift.down) → x ∈ (↑{{ down := a : PLift α }} : Set (PLift α))

Tactic:
contrapose