awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (hypothesis)
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)
⊢ (take (i + 1) (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i + 1, f j
have B : ∀ (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 _)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
⊢ (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
have zero : (take 0 (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < 0, 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]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
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
⊢ (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
have 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
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]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : DivisionCommMonoid G
⊢ 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 : ℕ))
have 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 sorry ^
        HPow.hPow (α := ℤ) (-1) (↑x : ℕ) =
      1
Tactic: rw [alternatingProd, Finset.prod_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : DivisionCommMonoid G
g : G
⊢ [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 : ℕ)
have change : g =
  ∏ i : Fin 1,
    getElem (valid := fun (xs : List G) (i : Fin 1) ↦ (↑i : ℕ) < xs.length) [g] i sorry ^ HPow.hPow (α := ℤ) (-1) (↑i : ℕ)
Tactic: change g = ∏ i : Fin 1, [g][i] ^ (-1 : ℤ) ^ (i : ℕ)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : DivisionCommMonoid G
g : G
⊢ g =
    ∏ i : Fin 1,
      getElem (valid := fun (xs : List G) (i : Fin 1) ↦ (↑i : ℕ) < xs.length) [g] i ⋯ ^ HPow.hPow (α := ℤ) (-1) (↑i : ℕ)
have rw : g =
  getElem (valid := fun (xs : List G) (i : Fin 1) ↦ (↑i : ℕ) < xs.length) [g] 0 sorry ^ HPow.hPow (α := ℤ) (-1) (↑0 : ℕ) *
    ∏ i : Fin 0,
      getElem (valid := fun (xs : List G) (i : Fin 1) ↦ (↑i : ℕ) < xs.length) [g] i.succ sorry ^
        HPow.hPow (α := ℤ) (-1) (↑i.succ : ℕ)
Tactic: rw [Fin.prod_univ_succ]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
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 : ℕ) =
    ∏ 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 : ℕ)
have rw : g *
    (h⁻¹ *
      ∏ i : Fin L.length,
        getElem (valid := fun (xs : List G) (i : Fin L.length) ↦ (↑i : ℕ) < xs.length) L i sorry ^
          HPow.hPow (α := ℤ) (-1) (↑i : ℕ)) =
  getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) 0 sorry ^
      HPow.hPow (α := ℤ) (-1) (↑0 : ℕ) *
    (getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) (Fin.succ 0) sorry ^
        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
            sorry ^
          HPow.hPow (α := ℤ) (-1) (↑i.succ.succ : ℕ))
Tactic: rw [Fin.prod_univ_succ, Fin.prod_univ_succ, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
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 : ℕ) =
    ∏ 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 : ℕ)
have rw : g * h⁻¹ *
    ∏ i : Fin L.length,
      getElem (valid := fun (xs : List G) (i : Fin L.length) ↦ (↑i : ℕ) < xs.length) L i sorry ^
        HPow.hPow (α := ℤ) (-1) (↑i : ℕ) =
  getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) 0 sorry ^
      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 sorry ^
        HPow.hPow (α := ℤ) (-1) (↑i.succ : ℕ)
Tactic: { rw [Fin.prod_univ_succ, Fin.prod_univ_succ, mul_assoc]
          simp [pow_add]}
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
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 : ℕ)
⊢ 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 : ℕ)
have rw₁ : g * h⁻¹ *
    ∏ i : Fin L.length,
      getElem (valid := fun (xs : List G) (i : Fin L.length) ↦ (↑i : ℕ) < xs.length) L i sorry ^
        HPow.hPow (α := ℤ) (-1) (↑i : ℕ) =
  getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) 0 sorry ^
      HPow.hPow (α := ℤ) (-1) (↑0 : ℕ) *
    (getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) (Fin.succ 0) sorry ^
        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
            sorry ^
          HPow.hPow (α := ℤ) (-1) (↑i.succ.succ : ℕ))
Tactic: { rw [Fin.prod_univ_succ, Fin.prod_univ_succ, mul_assoc]
          simp [pow_add]}
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
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 : ℕ))
⊢ 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 : ℕ)
have rw₂ : g *
    (h⁻¹ *
      ∏ i : Fin L.length,
        getElem (valid := fun (xs : List G) (i : Fin L.length) ↦ (↑i : ℕ) < xs.length) L i sorry ^
          HPow.hPow (α := ℤ) (-1) (↑i : ℕ)) =
  getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) 0 sorry ^
      HPow.hPow (α := ℤ) (-1) (↑0 : ℕ) *
    (getElem (valid := fun (xs : List G) (i : Fin (L.length + 2)) ↦ (↑i : ℕ) < xs.length) (g :: h :: L) (Fin.succ 0) sorry ^
        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
            sorry ^
          HPow.hPow (α := ℤ) (-1) (↑i.succ.succ : ℕ))
Tactic: { rw [Fin.prod_univ_succ, Fin.prod_univ_succ, mul_assoc]
          simp [pow_add]}
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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 : α), f i) (∏ i ∈ s, f i.down)
have 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)
Tactic: rw [finprod, dif_pos hf]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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)
have 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
Tactic: refine Finset.prod_subset hs fun x _ hxf => ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ f x.down = 1
have rwa : ∀ (hxf : x ∉ mulSupport (f ∘ PLift.down)), f x.down = 1
Tactic: rwa [hf.mem_toFinset, notMem_mulSupport] at hxf
Cleared hypotheses: hxf
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ f x.down = 1
have rwa₁ : ∀ (hxf : (f ∘ PLift.down) x = 1), f x.down = 1
Tactic: rwa [hf.mem_toFinset, notMem_mulSupport] at hxf
Cleared hypotheses: hxf
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
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 ∈ s
have hx₁ : x ∈ mulSupport (f ∘ PLift.down)
Tactic: rw [Finite.mem_toFinset] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
⊢ Eq.{u_2 + 1} (α := M) (∏ᶠ (x : α), 1) 1
have this : (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
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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 α))
⊢ Eq.{u_2 + 1} (α := M) (∏ᶠ (x : α), 1) 1
have rw : Eq.{u_2 + 1} (α := M) (∏ i ∈ ∅, 1) 1
Tactic: rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_empty]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ Eq.{u_2 + 1} (α := M) (∏ᶠ (x : α), 1) 1
have rw₁ : Eq.{u_2 + 1} (α := M) 1 1
Tactic: rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_empty]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
inst_1 : IsEmpty α
f : α → M
⊢ Eq.{u_2 + 1} (α := M) (∏ᶠ (i : α), f i) 1
have rw : Eq.{u_2 + 1} (α := M) (∏ᶠ (i : α), f i) (∏ᶠ (x : α), 1)
Tactic: rw [← finprod_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
x : PLift α
⊢ x ∈ mulSupport (f ∘ PLift.down) → x ∈ (↑{{ down := a : PLift α }} : Set (PLift α))
have contrapose : x ∉ (↑{{ down := a : PLift α }} : Set (PLift α)) → x ∉ mulSupport (f ∘ PLift.down)
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
⊢ ∏ᶠ (x : α), f x = f a
have this : mulSupport (f ∘ PLift.down) ⊆ (↑{{ down := a : PLift α }} : Set (PLift α))
Tactic: have : mulSupport (f ∘ PLift.down) ⊆ ({PLift.up a} : Finset (PLift α)) := by
    intro x
    contrapose
    simpa [PLift.eq_up_iff_down_eq] using ha x.down
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
this : mulSupport (f ∘ PLift.down) ⊆ (↑{{ down := a : PLift α }} : Set (PLift α))
⊢ ∏ᶠ (x : α), f x = f a
have rw : ∏ i ∈ {{ down := a : PLift α }}, f i.down = f a
Tactic: rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
this : mulSupport (f ∘ PLift.down) ⊆ (↑{{ down := a : PLift α }} : Set (PLift α))
rw : ∏ i ∈ {{ down := a : PLift α }}, f i.down = f a
⊢ ∏ᶠ (x : α), f x = f a
have rw₁ : f { down := a : PLift α }.down = f a
Tactic: rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_2
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
f : p → M
⊢ Eq.{u_2 + 1} (α := M) (∏ᶠ (i : p), f i) (if h : p then f h else 1)
have pos : ∀ (h : p), ∏ᶠ (i : p), f i = f h
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_2
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
f : p → M
pos : ∀ (h : p), ∏ᶠ (i : p), f i = f h
⊢ Eq.{u_2 + 1} (α := M) (∏ᶠ (i : p), f i) (if h : p then f h else 1)
have neg : ∀ (h : ¬p), Eq.{u_2 + 1} (α := M) (∏ᶠ (i : p), f i) 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_2
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
f : p → M
h : p
⊢ ∏ᶠ (i : p), f i = f h
have pos : ∀ (this : Unique p), ∏ᶠ (i : p), f i = f h
Tactic: haveI : Unique p := ⟨⟨h⟩, fun _ => rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
Goal:
M : Type u_2
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
f : p → M
h : ¬p
⊢ Eq.{u_2 + 1} (α := M) (∏ᶠ (i : p), f i) 1
have this : IsEmpty p
Tactic: haveI : IsEmpty p := ⟨h⟩
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_2
inst : CommMonoid M
p q : Prop
f : p → M
g : q → M
hpq : p = q
hfg : ∀ (h : q), f ⋯ = g h
⊢ finprod f = finprod g
have subst : ∀ {g : p → M} (hfg : ∀ (h : p), f sorry = g h), finprod f = finprod g
Tactic: subst q
Cleared hypotheses: q, g, hpq, hfg
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
⊢ p (∏ᶠ (i : α), f i)
have rw : p
  (if h : HasFiniteMulSupport.{u_4, u_2} (α := PLift α) (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down) then
    ∏ i ∈ Finite.toFinset (s := mulSupport.{u_4, u_2} (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)) h, f i.down
  else 1)
Tactic: rw [finprod]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
⊢ p
    (if h : HasFiniteMulSupport.{u_4, u_2} (α := PLift α) (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down) then
      ∏ i ∈ Finite.toFinset (s := mulSupport.{u_4, u_2} (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)) h, f i.down
    else 1)
have pos : ∀ (h : HasFiniteMulSupport.{u_4, u_2} (α := PLift α) (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)),
  p (∏ i ∈ Finite.toFinset (s := mulSupport.{u_4, u_2} (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)) h, f i.down)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_2
α : Sort u_4
inst : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
pos :
  ∀ (h : HasFiniteMulSupport.{u_4, u_2} (α := PLift α) (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)),
    p (∏ i ∈ Finite.toFinset (s := mulSupport.{u_4, u_2} (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)) h, f i.down)
⊢ p
    (if h : HasFiniteMulSupport.{u_4, u_2} (α := PLift α) (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down) then
      ∏ i ∈ Finite.toFinset (s := mulSupport.{u_4, u_2} (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down)) h, f i.down
    else 1)
have neg : ¬HasFiniteMulSupport.{u_4, u_2} (α := PLift α) (M := M) ((fun (i : α) ↦ f i) ∘ PLift.down) → p 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_2
N : Type u_3
α : Sort u_4
inst : CommMonoid M
inst_1 : CommMonoid N
f : M →* N
g : α → M
h : HasFiniteMulSupport (g ∘ PLift.down)
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (∏ᶠ (x : α), g x) : N) (∏ᶠ (x : α), (f : (a : M) → N) (g x) : N)
have rw : mulSupport.{u_4, u_3} (M := N) ((fun (x : α) ↦ (f : (a : M) → N) (g x)) ∘ PLift.down) ⊆
  (↑(Finite.toFinset (s := mulSupport (g ∘ PLift.down)) h) : Set (PLift α))
Tactic: rw [finprod_eq_prod_plift_of_mulSupport_subset h.coe_toFinset.ge,
    finprod_eq_prod_plift_of_mulSupport_subset, _root_.map_prod]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_2
N : Type u_3
α : Sort u_4
inst : CommMonoid M
inst_1 : CommMonoid N
f : M →* N
g : α → M
h : HasFiniteMulSupport (g ∘ PLift.down)
⊢ mulSupport.{u_4, u_3} (M := N) ((fun (x : α) ↦ (f : (a : M) → N) (g x)) ∘ PLift.down) ⊆
    (↑(Finite.toFinset (s := mulSupport (g ∘ PLift.down)) h) : Set (PLift α))
have rw : mulSupport.{u_4, u_3} (M := N) ((fun (x : α) ↦ (f : (a : M) → N) (g x)) ∘ PLift.down) ⊆ mulSupport (g ∘ PLift.down)
Tactic: rw [h.coe_toFinset]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_2
N : Type u_3
α : Sort u_4
inst : CommMonoid M
inst_1 : CommMonoid N
f : M →* N
hf : ∀ (x : M), Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (1 : N) → x = 1
g : α → M
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (∏ᶠ (i : α), g i) : N) (∏ᶠ (i : α), (f : (a : M) → N) (g i) : N)
have pos : ∀ (hg : HasFiniteMulSupport (g ∘ PLift.down)),
  Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (∏ᶠ (i : α), g i) : N) (∏ᶠ (i : α), (f : (a : M) → N) (g i) : N)
Tactic: by_cases hg : HasFiniteMulSupport <| g ∘ PLift.down
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_2
N : Type u_3
α : Sort u_4
inst : CommMonoid M
inst_1 : CommMonoid N
f : M →* N
hf : ∀ (x : M), Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (1 : N) → x = 1
g : α → M
pos :
  ∀ (hg : HasFiniteMulSupport (g ∘ PLift.down)),
    Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (∏ᶠ (i : α), g i) : N) (∏ᶠ (i : α), (f : (a : M) → N) (g i) : N)
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (∏ᶠ (i : α), g i) : N) (∏ᶠ (i : α), (f : (a : M) → N) (g i) : N)
have neg : ∀ (hg : ¬HasFiniteMulSupport (g ∘ PLift.down)),
  Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (∏ᶠ (i : α), g i) : N) (∏ᶠ (i : α), (f : (a : M) → N) (g i) : N)
Tactic: by_cases hg : HasFiniteMulSupport <| g ∘ PLift.down
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
M : Type u_2
N : Type u_3
α : Sort u_4
inst : CommMonoid M
inst_1 : CommMonoid N
f : M →* N
hf : ∀ (x : M), Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (1 : N) → x = 1
g : α → M
hg : ¬HasFiniteMulSupport (g ∘ PLift.down)
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (∏ᶠ (i : α), g i) : N) (∏ᶠ (i : α), (f : (a : M) → N) (g i) : N)
have neg : ¬HasFiniteMulSupport.{u_4, u_3} (α := PLift α) (M := N) ((fun (i : α) ↦ (f : (a : M) → N) (g i)) ∘ PLift.down)
Tactic: rw [finprod, dif_neg, f.map_one, finprod, dif_neg]