awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
refine_1 :
  ∀ (a : ι) (ha : a ∈ s),
    Membership.mem (γ := Finset ↥s) univ ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha)
refine_2 :
  ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
    (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha ∈ s
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if hi : p i then f i hi else g i hi) (∏ i : ↥s, g (↑i : ι) ⋯)
have refine_3 : ∀ (a : ι) (ha : a ∈ s),
  (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι))
      ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha) sorry =
    a
Tactic: refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
refine_1 :
  ∀ (a : ι) (ha : a ∈ s),
    Membership.mem (γ := Finset ↥s) univ ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha)
refine_2 :
  ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
    (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha ∈ s
refine_3 :
  ∀ (a : ι) (ha : a ∈ s),
    (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι))
        ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha) ⋯ =
      a
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if hi : p i then f i hi else g i hi) (∏ i : ↥s, g (↑i : ι) ⋯)
have refine_4 : ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
  (fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx)
      ((fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha) sorry =
    a
Tactic: refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
refine_1 :
  ∀ (a : ι) (ha : a ∈ s),
    Membership.mem (γ := Finset ↥s) univ ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha)
refine_2 :
  ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
    (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha ∈ s
refine_3 :
  ∀ (a : ι) (ha : a ∈ s),
    (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι))
        ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha) ⋯ =
      a
refine_4 :
  ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
    (fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx)
        ((fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha) ⋯ =
      a
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if hi : p i then f i hi else g i hi) (∏ i : ↥s, g (↑i : ι) ⋯)
have refine_5 : ∀ (a : ι) (ha : a ∈ s),
  (if hi : p a then f a hi else g a hi) =
    g (↑((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha) : ι) sorry
Tactic: refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if hi : p i then f i hi else g i hi) (∏ i : ↥s, f (↑i : ι) ⋯)
have refine_1 : ∀ (a : ι) (ha : a ∈ s),
  Membership.mem (γ := Finset ↥s) univ ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha)
Tactic: refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
refine_1 :
  ∀ (a : ι) (ha : a ∈ s),
    Membership.mem (γ := Finset ↥s) univ ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha)
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if hi : p i then f i hi else g i hi) (∏ i : ↥s, f (↑i : ι) ⋯)
have refine_2 : ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
  (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha ∈ s
Tactic: refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
refine_1 :
  ∀ (a : ι) (ha : a ∈ s),
    Membership.mem (γ := Finset ↥s) univ ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha)
refine_2 :
  ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
    (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha ∈ s
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if hi : p i then f i hi else g i hi) (∏ i : ↥s, f (↑i : ι) ⋯)
have refine_3 : ∀ (a : ι) (ha : a ∈ s),
  (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι))
      ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha) sorry =
    a
Tactic: refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
refine_1 :
  ∀ (a : ι) (ha : a ∈ s),
    Membership.mem (γ := Finset ↥s) univ ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha)
refine_2 :
  ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
    (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha ∈ s
refine_3 :
  ∀ (a : ι) (ha : a ∈ s),
    (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι))
        ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha) ⋯ =
      a
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if hi : p i then f i hi else g i hi) (∏ i : ↥s, f (↑i : ι) ⋯)
have refine_4 : ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
  (fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx)
      ((fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha) sorry =
    a
Tactic: refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
refine_1 :
  ∀ (a : ι) (ha : a ∈ s),
    Membership.mem (γ := Finset ↥s) univ ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha)
refine_2 :
  ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
    (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha ∈ s
refine_3 :
  ∀ (a : ι) (ha : a ∈ s),
    (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι))
        ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha) ⋯ =
      a
refine_4 :
  ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
    (fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx)
        ((fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha) ⋯ =
      a
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if hi : p i then f i hi else g i hi) (∏ i : ↥s, f (↑i : ι) ⋯)
have refine_5 : ∀ (a : ι) (ha : a ∈ s),
  (if hi : p a then f a hi else g a hi) =
    f (↑((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha) : ι) sorry
Tactic: refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, ¬p x
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, k (if p x then f x else g x)) (∏ x ∈ s, k (g x))
have simp_rw : Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if p x then k (f x) else k (g x)) (∏ x ∈ s, k (g x))
Tactic: simp_rw [apply_ite k]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, p x
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, k (if p x then f x else g x)) (∏ x ∈ s, k (f x))
have simp_rw : Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if p x then k (f x) else k (g x)) (∏ x ∈ s, k (f x))
Tactic: simp_rw [apply_ite k]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if i ∈ t then f i else 1) (∏ i ∈ s ∩ t, f i)
have rw : Eq.{u_3 + 1} (α := M) (∏ a ∈ s with a ∈ t, f a) (∏ i ∈ s ∩ t, f i)
Tactic: rw [← Finset.prod_filter, Finset.filter_mem_eq_inter]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s t : Finset ι
f : ι → M
rw : Eq.{u_3 + 1} (α := M) (∏ a ∈ s with a ∈ t, f a) (∏ i ∈ s ∩ t, f i)
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if i ∈ t then f i else 1) (∏ i ∈ s ∩ t, f i)
have rw₁ : Eq.{u_3 + 1} (α := M) (∏ a ∈ s ∩ t, f a) (∏ i ∈ s ∩ t, f i)
Tactic: rw [← Finset.prod_filter, Finset.filter_mem_eq_inter]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ↥s → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s.attach, f i)
    (∏ i : ι, if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else 1)
have rw : Eq.{u_3 + 1} (α := M) (∏ i ∈ s.attach, f i)
  (∏ x ∈ attach {x : ι | x ∈ s}, f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑x : ι) sorry))
Tactic: rw [Finset.prod_dite, Finset.univ_eq_attach, Finset.prod_const_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ↥s → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s.attach, f i)
    (∏ x ∈ attach {x : ι | x ∈ s}, f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑x : ι) ⋯))
have h : Eq.{u_1 + 1} (α := ι → Prop) (fun (x : ι) ↦ x ∈ s) fun (x : ι) ↦ Membership.mem (γ := Finset ι) {x : ι | x ∈ s} x
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ↥s → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
h : Eq.{u_1 + 1} (α := ι → Prop) (fun (x : ι) ↦ x ∈ s) fun (x : ι) ↦ Membership.mem (γ := Finset ι) {x : ι | x ∈ s} x
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s.attach, f i)
    (∏ x ∈ attach {x : ι | x ∈ s}, f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑x : ι) ⋯))
have h₁ : s = {x : ι | x ∈ s}
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ↥s → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
h : Eq.{u_1 + 1} (α := ι → Prop) (fun (x : ι) ↦ x ∈ s) fun (x : ι) ↦ Membership.mem (γ := Finset ι) {x : ι | x ∈ s} x
h₁ : s = {x : ι | x ∈ s}
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s.attach, f i)
    (∏ x ∈ attach {x : ι | x ∈ s}, f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑x : ι) ⋯))
have h₂ : HEq (α := ↥s → M) fun (i : ↥s) ↦ f i (β := ↥{x : ι | x ∈ s} → M) fun (x : ↥{x : ι | x ∈ s}) ↦
  f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑x : ι) sorry)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ↥s → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
⊢ s = {x : ι | x ∈ s}
have h : ∀ (a : ι), a ∈ s ↔ Membership.mem (γ := Finset ι) {x : ι | x ∈ s} a
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ↥s → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
⊢ HEq (α := ↥s → M) fun (i : ↥s) ↦ f i (β := ↥{x : ι | x ∈ s} → M) fun (x : ↥{x : ι | x ∈ s}) ↦
    f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑x : ι) ⋯)
have h : ↥s = ↥{x : ι | x ∈ s}
Tactic: apply Function.hfunext
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ↥s → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
h : ↥s = ↥{x : ι | x ∈ s}
⊢ HEq (α := ↥s → M) fun (i : ↥s) ↦ f i (β := ↥{x : ι | x ∈ s} → M) fun (x : ↥{x : ι | x ∈ s}) ↦
    f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑x : ι) ⋯)
have h₁ : ∀ (a : ↥s) (a' : ↥{x : ι | x ∈ s}), a ≍ a' → f a ≍ f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑a' : ι) sorry)
Tactic: apply Function.hfunext
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = if a ∈ s then b a ⋯ else 1
have pos : ∀ (h : a ∈ s), (∏ x ∈ s, if h : a = x then b x h else 1) = b a sorry
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
pos : ∀ (h : a ∈ s), (∏ x ∈ s, if h : a = x then b x h else 1) = b a ⋯
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = if a ∈ s then b a ⋯ else 1
have neg : ∀ (h : a ∉ s), Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if h : a = x then b x h else 1) 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = b a ⋯
have pos : ∀ b_1 ∈ s, b_1 ≠ a → Eq.{u_3 + 1} (α := M) (if h : a = b_1 then b b_1 h else 1) 1
Tactic: rw [Finset.prod_eq_single a, dif_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
pos : ∀ b_1 ∈ s, b_1 ≠ a → Eq.{u_3 + 1} (α := M) (if h : a = b_1 then b b_1 h else 1) 1
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = b a ⋯
have pos₁ : a ∉ s → Eq.{u_3 + 1} (α := M) (if h : a = a then b a h else 1) 1
Tactic: rw [Finset.prod_eq_single a, dif_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h_1 : a ∈ s
b_1 : ι
h_2 : b_1 ∈ s
h : b_1 ≠ a
⊢ Eq.{u_3 + 1} (α := M) (if h : a = b_1 then b b_1 h else 1) 1
have pos : ¬a = b_1
Tactic: rw [dif_neg]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∉ s
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if h : a = x then b x h else 1) 1
have neg : ∀ x ∈ s, Eq.{u_3 + 1} (α := M) (if h : a = x then b x h else 1) 1
Tactic: rw [Finset.prod_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
⊢ (∏ x ∈ s, if h : x = a then b x h else 1) = if a ∈ s then b a ⋯ else 1
have pos : ∀ (h : a ∈ s), (∏ x ∈ s, if h : x = a then b x h else 1) = b a sorry
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
pos : ∀ (h : a ∈ s), (∏ x ∈ s, if h : x = a then b x h else 1) = b a ⋯
⊢ (∏ x ∈ s, if h : x = a then b x h else 1) = if a ∈ s then b a ⋯ else 1
have neg : ∀ (h : a ∉ s), Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if h : x = a then b x h else 1) 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
⊢ (∏ x ∈ s, if h : x = a then b x h else 1) = b a ⋯
have pos : ∀ b_1 ∈ s, b_1 ≠ a → Eq.{u_3 + 1} (α := M) (if h : b_1 = a then b b_1 h else 1) 1
Tactic: rw [Finset.prod_eq_single a, dif_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
pos : ∀ b_1 ∈ s, b_1 ≠ a → Eq.{u_3 + 1} (α := M) (if h : b_1 = a then b b_1 h else 1) 1
⊢ (∏ x ∈ s, if h : x = a then b x h else 1) = b a ⋯
have pos₁ : a ∉ s → Eq.{u_3 + 1} (α := M) (if h : a = a then b a h else 1) 1
Tactic: rw [Finset.prod_eq_single a, dif_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h_1 : a ∈ s
b_1 : ι
h_2 : b_1 ∈ s
h : b_1 ≠ a
⊢ Eq.{u_3 + 1} (α := M) (if h : b_1 = a then b b_1 h else 1) 1
have pos : ¬b_1 = a
Tactic: rw [dif_neg]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∉ s
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if h : x = a then b x h else 1) 1
have neg : ∀ x ∈ s, Eq.{u_3 + 1} (α := M) (if h : x = a then b x h else 1) 1
Tactic: rw [Finset.prod_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s t : Finset ι
f g : ι → M
⊢ ∏ x ∈ s, t.piecewise (π := fun (i : ι) ↦ M) f g x = HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, g x)
have simp : (∏ x ∈ s, if x ∈ t then f x else g x) = HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, g x)
Tactic: simp only [piecewise]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s t : Finset ι
f g : ι → M
⊢ (∏ x ∈ s, if x ∈ t then f x else g x) = HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, g x)
have rw : HMul.hMul (α := M) (∏ x ∈ s with x ∈ t, f x) (∏ x ∈ s with x ∉ t, g x) =
  HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, g x)
Tactic: rw [prod_ite, filter_mem_eq_inter, ← sdiff_eq_filter]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s t : Finset ι
f g : ι → M
rw :
  HMul.hMul (α := M) (∏ x ∈ s with x ∈ t, f x) (∏ x ∈ s with x ∉ t, g x) =
    HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, g x)
⊢ (∏ x ∈ s, if x ∈ t then f x else g x) = HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, g x)
have rw₁ : HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s with x ∉ t, g x) =
  HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, g x)
Tactic: rw [prod_ite, filter_mem_eq_inter, ← sdiff_eq_filter]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s t : Finset ι
f g : ι → M
rw :
  HMul.hMul (α := M) (∏ x ∈ s with x ∈ t, f x) (∏ x ∈ s with x ∉ t, g x) =
    HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, g x)
rw₁ :
  HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s with x ∉ t, g x) =
    HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, g x)
⊢ (∏ x ∈ s, if x ∈ t then f x else g x) = HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, g x)
have rw₂ : HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, g x) = HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, g x)
Tactic: rw [prod_ite, filter_mem_eq_inter, ← sdiff_eq_filter]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, f x) = ∏ x ∈ s, f x
have h : ∀ x ∈ s, f = t.piecewise (π := fun (i : ι) ↦ M) f f
Tactic: convert! (s.prod_piecewise t f f).symm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x
have pos : ∀ (hs : i ∈ s), ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x
Tactic: by_cases hs : i ∈ s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
pos : ∀ (hs : i ∈ s), ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x
have neg : ∀ (hs : i ∉ s), ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x
Tactic: by_cases hs : i ∈ s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∈ s
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x
have h₁ : f i = ∏ x ∈ s ∩ {i}, f x
Tactic: convert! (s.prod_inter_mul_prod_diff { i } f).symm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∉ s
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x
have neg : ∀ (h : f i = 1) (hs : i ∉ s), Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s \ {i}, f x)
Tactic: simp_all only [not_false_eq_true, forall_const, one_mul]
Cleared hypotheses: h, hs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : f i = 1
hs : i ∉ s
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s \ {i}, f x)
have neg : s = s \ {i}
Tactic: apply Finset.prod_congr
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : f i = 1
hs : i ∉ s
neg : s = s \ {i}
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s \ {i}, f x)
have neg₁ : ∀ x ∈ s \ {i}, f x = f x
Tactic: apply Finset.prod_congr
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
h : i ∈ s
f : ι → M
⊢ ∏ x ∈ s, f x = (∏ x ∈ s \ {i}, f x) * f i
have rw : f i * ∏ x ∈ s \ {i}, f x = (∏ x ∈ s \ {i}, f x) * f i
Tactic: rw [prod_eq_mul_prod_diff_singleton_of_mem h, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
i : ι
h : i ∈ s
f : ι → M
rw : f i * ∏ x ∈ s \ {i}, f x = (∏ x ∈ s \ {i}, f x) * f i
⊢ ∏ x ∈ s, f x = (∏ x ∈ s \ {i}, f x) * f i
have rw₁ : (∏ x ∈ s \ {i}, f x) * f i = (∏ x ∈ s \ {i}, f x) * f i
Tactic: rw [prod_eq_mul_prod_diff_singleton_of_mem h, mul_comm]