awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
m : Multiset ι
f : { x : ι // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x : ι // x ∈ m }), f x = g (↑x : ι)
refine_1 :
  ∀ (a : { x : ι // x ∈ m }) (ha : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ a),
    (fun (x : { x : ι // x ∈ m }) (x_1 : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ x) ↦ (↑x : ι)) a ha ∈
      m.toFinset
⊢ Eq.{u_3 + 1} (α := M) (∏ x : { x : ι // x ∈ m }, f x) (∏ x ∈ m.toFinset, g x)
have refine_2 : ∀ (a : ι) (ha : a ∈ m.toFinset),
  Membership.mem (γ := Finset { x : ι // x ∈ m }) univ
    ((fun (x : ι) (hx : x ∈ m.toFinset) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ m) x sorry) a ha)
Tactic: refine prod_bij' (fun x _ ↦ x) (fun x hx ↦ ⟨x, Multiset.mem_toFinset.1 hx⟩) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
m : Multiset ι
f : { x : ι // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x : ι // x ∈ m }), f x = g (↑x : ι)
refine_1 :
  ∀ (a : { x : ι // x ∈ m }) (ha : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ a),
    (fun (x : { x : ι // x ∈ m }) (x_1 : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ x) ↦ (↑x : ι)) a ha ∈
      m.toFinset
refine_2 :
  ∀ (a : ι) (ha : a ∈ m.toFinset),
    Membership.mem (γ := Finset { x : ι // x ∈ m }) univ
      ((fun (x : ι) (hx : x ∈ m.toFinset) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ m) x ⋯) a ha)
⊢ Eq.{u_3 + 1} (α := M) (∏ x : { x : ι // x ∈ m }, f x) (∏ x ∈ m.toFinset, g x)
have refine_3 : ∀ (a : { x : ι // x ∈ m }) (ha : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ a),
  (fun (x : ι) (hx : x ∈ m.toFinset) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ m) x sorry)
      ((fun (x : { x : ι // x ∈ m }) (x_1 : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ x) ↦ (↑x : ι)) a ha)
      sorry =
    a
Tactic: refine prod_bij' (fun x _ ↦ x) (fun x hx ↦ ⟨x, Multiset.mem_toFinset.1 hx⟩) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
m : Multiset ι
f : { x : ι // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x : ι // x ∈ m }), f x = g (↑x : ι)
refine_1 :
  ∀ (a : { x : ι // x ∈ m }) (ha : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ a),
    (fun (x : { x : ι // x ∈ m }) (x_1 : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ x) ↦ (↑x : ι)) a ha ∈
      m.toFinset
refine_2 :
  ∀ (a : ι) (ha : a ∈ m.toFinset),
    Membership.mem (γ := Finset { x : ι // x ∈ m }) univ
      ((fun (x : ι) (hx : x ∈ m.toFinset) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ m) x ⋯) a ha)
refine_3 :
  ∀ (a : { x : ι // x ∈ m }) (ha : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ a),
    (fun (x : ι) (hx : x ∈ m.toFinset) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ m) x ⋯)
        ((fun (x : { x : ι // x ∈ m }) (x_1 : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ x) ↦ (↑x : ι)) a ha)
        ⋯ =
      a
⊢ Eq.{u_3 + 1} (α := M) (∏ x : { x : ι // x ∈ m }, f x) (∏ x ∈ m.toFinset, g x)
have refine_4 : ∀ (a : ι) (ha : a ∈ m.toFinset),
  (fun (x : { x : ι // x ∈ m }) (x_1 : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ x) ↦ (↑x : ι))
      ((fun (x : ι) (hx : x ∈ m.toFinset) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ m) x sorry) a ha) sorry =
    a
Tactic: refine prod_bij' (fun x _ ↦ x) (fun x hx ↦ ⟨x, Multiset.mem_toFinset.1 hx⟩) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
m : Multiset ι
f : { x : ι // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x : ι // x ∈ m }), f x = g (↑x : ι)
refine_1 :
  ∀ (a : { x : ι // x ∈ m }) (ha : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ a),
    (fun (x : { x : ι // x ∈ m }) (x_1 : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ x) ↦ (↑x : ι)) a ha ∈
      m.toFinset
refine_2 :
  ∀ (a : ι) (ha : a ∈ m.toFinset),
    Membership.mem (γ := Finset { x : ι // x ∈ m }) univ
      ((fun (x : ι) (hx : x ∈ m.toFinset) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ m) x ⋯) a ha)
refine_3 :
  ∀ (a : { x : ι // x ∈ m }) (ha : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ a),
    (fun (x : ι) (hx : x ∈ m.toFinset) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ m) x ⋯)
        ((fun (x : { x : ι // x ∈ m }) (x_1 : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ x) ↦ (↑x : ι)) a ha)
        ⋯ =
      a
refine_4 :
  ∀ (a : ι) (ha : a ∈ m.toFinset),
    (fun (x : { x : ι // x ∈ m }) (x_1 : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ x) ↦ (↑x : ι))
        ((fun (x : ι) (hx : x ∈ m.toFinset) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ m) x ⋯) a ha) ⋯ =
      a
⊢ Eq.{u_3 + 1} (α := M) (∏ x : { x : ι // x ∈ m }, f x) (∏ x ∈ m.toFinset, g x)
have refine_5 : ∀ (a : { x : ι // x ∈ m }) (ha : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ a),
  f a =
    g ((fun (x : { x : ι // x ∈ m }) (x_1 : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ x) ↦ (↑x : ι)) a ha)
Tactic: refine prod_bij' (fun x _ ↦ x) (fun x hx ↦ ⟨x, Multiset.mem_toFinset.1 hx⟩) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ Multiset.sum (Multiset.map (fun (x : ℕ) ↦ x % n) (Multiset.map (fun (i : ι) ↦ f i) s.val)) % n =
    (∑ i ∈ s, f i % n) % n
have rw : Multiset.sum (Multiset.map ((fun (x : ℕ) ↦ x % n) ∘ fun (i : ι) ↦ f i) s.val) % n =
  Multiset.sum (Multiset.map (fun (i : ι) ↦ f i % n) s.val) % n
Tactic: rw [Finset.sum, Multiset.map_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ Multiset.prod (Multiset.map (fun (x : ℕ) ↦ x % n) (Multiset.map (fun (i : ι) ↦ f i) s.val)) % n =
    (∏ i ∈ s, f i % n) % n
have rw : Multiset.prod (Multiset.map ((fun (x : ℕ) ↦ x % n) ∘ fun (i : ι) ↦ f i) s.val) % n =
  Multiset.prod (Multiset.map (fun (i : ι) ↦ f i % n) s.val) % n
Tactic: rw [Finset.prod, Multiset.map_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ Multiset.sum (Multiset.map (fun (x : ℤ) ↦ x % n) (Multiset.map (fun (i : ι) ↦ f i) s.val)) % n =
    (∑ i ∈ s, f i % n) % n
have rw : Multiset.sum (Multiset.map ((fun (x : ℤ) ↦ x % n) ∘ fun (i : ι) ↦ f i) s.val) % n =
  Multiset.sum (Multiset.map (fun (i : ι) ↦ f i % n) s.val) % n
Tactic: rw [Finset.sum, Multiset.map_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ Multiset.prod (Multiset.map (fun (x : ℤ) ↦ x % n) (Multiset.map (fun (i : ι) ↦ f i) s.val)) % n =
    (∏ i ∈ s, f i % n) % n
have rw : Multiset.prod (Multiset.map ((fun (x : ℤ) ↦ x % n) ∘ fun (i : ι) ↦ f i) s.val) % n =
  Multiset.prod (Multiset.map (fun (i : ι) ↦ f i % n) s.val) % n
Tactic: rw [Finset.prod, Multiset.map_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
f : ι → M
i : ↥s
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ s.attach.erase i, f (↑j : ι)) (∏ j ∈ s.erase (↑i : ι), f j)
have rw : Eq.{u_3 + 1} (α := M) (∏ x ∈ map (Embedding.subtype fun (x : ι) ↦ x ∈ s) (s.attach.erase i), f x)
  (∏ j ∈ s.erase ((Embedding.subtype fun (x : ι) ↦ x ∈ s : (a : ↥s) → ι) i), f j)
Tactic: rw [← Function.Embedding.coe_subtype, ← prod_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
α : Type u_6
a : Multiset α
l : List (Multiset α)
⊢ Disjoint l.sum a ↔ ∀ b ∈ l, Disjoint b a
have nil : Disjoint (List.sum []) a ↔ ∀ (b : Multiset α), Membership.mem (γ := List (Multiset α)) [] b → Disjoint b a
Tactic: induction l with
  | nil =>
    simp only [zero_disjoint, List.not_mem_nil, IsEmpty.forall_iff, forall_const, List.sum_nil]
  | cons b bs ih =>
    simp [ih]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
α : Type u_6
a : Multiset α
l : List (Multiset α)
nil : Disjoint (List.sum []) a ↔ ∀ (b : Multiset α), Membership.mem (γ := List (Multiset α)) [] b → Disjoint b a
⊢ Disjoint l.sum a ↔ ∀ b ∈ l, Disjoint b a
have cons : ∀ (b : Multiset α) (bs : List (Multiset α)) (ih : Disjoint bs.sum a ↔ ∀ b ∈ bs, Disjoint b a),
  Disjoint (b :: bs).sum a ↔ ∀ b_1 ∈ b :: bs, Disjoint b_1 a
Tactic: induction l with
  | nil =>
    simp only [zero_disjoint, List.not_mem_nil, IsEmpty.forall_iff, forall_const, List.sum_nil]
  | cons b bs ih =>
    simp [ih]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
α : Type u_6
i : Finset ι
f : ι → Multiset α
a : Multiset α
⊢ Disjoint (i.sum f) a ↔ ∀ b ∈ i, Disjoint (f b) a
have h : (∀ b ∈ i, Disjoint (f b) a) ↔ ∀ b ∈ map f i.val, Disjoint b a
Tactic: convert! @disjoint_sum_left _ a (map f i.val)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
ι : Type u_1
α : Type u_6
inst : DecidableEq α
s : Finset ι
a : α
f : ι → Multiset α
⊢ count a (sum (map (fun (x : ι) ↦ f x) s.val)) = sum (map (fun (x : ι) ↦ count a (f x)) s.val)
have rw : Eq (α := ℕ) (sum (map (fun (b : ι) ↦ count a (f b)) s.val)) (sum (map (fun (x : ι) ↦ count a (f x)) s.val))
Tactic: rw [count_sum]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
M : Type u_3
inst : DecidableEq M
inst_1 : CommMonoid M
S : Multiset M
⊢ S.toFinset.prod id ∣ S.prod
have rw : (map id S.toFinset.val).prod ∣ S.prod
Tactic: rw [Finset.prod_eq_multiset_prod]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
M : Type u_3
inst : DecidableEq M
inst_1 : CommMonoid M
S : Multiset M
⊢ (map id S.toFinset.val).prod ∣ S.prod
have refine : map id S.toFinset.val ≤ S
Tactic: refine Multiset.prod_dvd_prod_of_le ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
M : Type u_3
inst : Monoid M
s : List M
⊢ Eq (α := Additive M) ((ofMul : (a : M) → Additive M) s.prod : Additive M)
    (List.sum (List.map (⇑ofMul : (a : M) → Additive M) s) : Additive M)
have simp : s.prod = s.sum
Tactic: simp [ofMul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
M : Type u_3
inst : Monoid M
s : List (Additive M)
⊢ Eq (α := M) ((toMul : (a : Additive M) → M) s.sum : M) (List.prod (List.map (⇑toMul : (a : Additive M) → M) s) : M)
have simp : s.sum = s.prod
Tactic: simp [toMul, ofMul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
M : Type u_3
inst : AddMonoid M
s : List M
⊢ Eq (α := Multiplicative M) ((ofAdd : (a : M) → Multiplicative M) s.sum : Multiplicative M)
    (List.prod (List.map (⇑ofAdd : (a : M) → Multiplicative M) s) : Multiplicative M)
have simp : s.sum = s.prod
Tactic: simp [ofAdd]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
M : Type u_3
inst : AddMonoid M
s : List (Multiplicative M)
⊢ Eq (α := M) ((toAdd : (a : Multiplicative M) → M) s.prod : M)
    (List.sum (List.map (⇑toAdd : (a : Multiplicative M) → M) s) : M)
have simp : s.prod = s.sum
Tactic: simp [toAdd, ofAdd]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset M
⊢ Eq (α := Additive M) ((ofMul : (a : M) → Additive M) s.prod : Additive M)
    (Multiset.sum (Multiset.map (⇑ofMul : (a : M) → Additive M) s) : Additive M)
have simp : s.prod = s.sum
Tactic: simp [ofMul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset (Additive M)
⊢ Eq (α := M) ((toMul : (a : Additive M) → M) s.sum : M)
    (Multiset.prod (Multiset.map (⇑toMul : (a : Additive M) → M) s) : M)
have simp : s.sum = s.prod
Tactic: simp [toMul, ofMul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
M : Type u_3
inst : AddCommMonoid M
s : Multiset M
⊢ Eq (α := Multiplicative M) ((ofAdd : (a : M) → Multiplicative M) s.sum : Multiplicative M)
    (Multiset.prod (Multiset.map (⇑ofAdd : (a : M) → Multiplicative M) s) : Multiplicative M)
have simp : s.sum = s.prod
Tactic: simp [ofAdd]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Defs (goal)
Goal:
M : Type u_3
inst : AddCommMonoid M
s : Multiset (Multiplicative M)
⊢ Eq (α := M) ((toAdd : (a : Multiplicative M) → M) s.prod : M)
    (Multiset.sum (Multiset.map (⇑toAdd : (a : Multiplicative M) → M) s) : M)
have simp : s.prod = s.sum
Tactic: simp [toAdd, ofAdd]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Gaps (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
⊢ Eq.{u_2 + 1} (α := β) (∏ z ∈ F, f z.1 z.2) (∏ i ∈ range k, f (p (↑i : Fin (k + 1))).2 (p (↑i.succ : Fin (k + 1))).1)
have symm : Eq.{u_2 + 1} (α := β) (∏ i ∈ range k, f (p (↑i : Fin (k + 1))).2 (p (↑i.succ : Fin (k + 1))).1) (∏ z ∈ F, f z.1 z.2)
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Gaps (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
⊢ Eq.{u_2 + 1} (α := β) (∏ i ∈ range k, f (p (↑i : Fin (k + 1))).2 (p (↑i.succ : Fin (k + 1))).1) (∏ z ∈ F, f z.1 z.2)
have hi : ∀ (a : ℕ) (ha : a ∈ range k), ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1) ∈ F
Tactic: apply prod_bij (fun (i : ℕ) hi ↦ ((p i).2, (p i.succ).1))
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Gaps (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
hi : ∀ (a : ℕ) (ha : a ∈ range k), ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1) ∈ F
⊢ Eq.{u_2 + 1} (α := β) (∏ i ∈ range k, f (p (↑i : Fin (k + 1))).2 (p (↑i.succ : Fin (k + 1))).1) (∏ z ∈ F, f z.1 z.2)
have i_inj : ∀ (a₁ : ℕ) (ha₁ : a₁ ∈ range k) (a₂ : ℕ) (ha₂ : a₂ ∈ range k),
  ((p (↑a₁ : Fin (k + 1))).2, (p (↑a₁.succ : Fin (k + 1))).1) =
      ((p (↑a₂ : Fin (k + 1))).2, (p (↑a₂.succ : Fin (k + 1))).1) →
    a₁ = a₂
Tactic: apply prod_bij (fun (i : ℕ) hi ↦ ((p i).2, (p i.succ).1))
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Gaps (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
hi : ∀ (a : ℕ) (ha : a ∈ range k), ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1) ∈ F
i_inj :
  ∀ (a₁ : ℕ) (ha₁ : a₁ ∈ range k) (a₂ : ℕ) (ha₂ : a₂ ∈ range k),
    ((p (↑a₁ : Fin (k + 1))).2, (p (↑a₁.succ : Fin (k + 1))).1) =
        ((p (↑a₂ : Fin (k + 1))).2, (p (↑a₂.succ : Fin (k + 1))).1) →
      a₁ = a₂
⊢ Eq.{u_2 + 1} (α := β) (∏ i ∈ range k, f (p (↑i : Fin (k + 1))).2 (p (↑i.succ : Fin (k + 1))).1) (∏ z ∈ F, f z.1 z.2)
have i_surj : ∀ b ∈ F, ∃ (a : ℕ) (_ : a ∈ range k), ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1) = b
Tactic: apply prod_bij (fun (i : ℕ) hi ↦ ((p i).2, (p i.succ).1))
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Gaps (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
hi : ∀ (a : ℕ) (ha : a ∈ range k), ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1) ∈ F
i_inj :
  ∀ (a₁ : ℕ) (ha₁ : a₁ ∈ range k) (a₂ : ℕ) (ha₂ : a₂ ∈ range k),
    ((p (↑a₁ : Fin (k + 1))).2, (p (↑a₁.succ : Fin (k + 1))).1) =
        ((p (↑a₂ : Fin (k + 1))).2, (p (↑a₂.succ : Fin (k + 1))).1) →
      a₁ = a₂
i_surj : ∀ b ∈ F, ∃ (a : ℕ) (_ : a ∈ range k), ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1) = b
⊢ Eq.{u_2 + 1} (α := β) (∏ i ∈ range k, f (p (↑i : Fin (k + 1))).2 (p (↑i.succ : Fin (k + 1))).1) (∏ z ∈ F, f z.1 z.2)
have h₁ : ∀ (a : ℕ) (ha : a ∈ range k),
  f (p (↑a : Fin (k + 1))).2 (p (↑a.succ : Fin (k + 1))).1 =
    f ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1).1
      ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1).2
Tactic: apply prod_bij (fun (i : ℕ) hi ↦ ((p i).2, (p i.succ).1))
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Gaps (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
i : ℕ
hi : i ∈ range k
j : ℕ
hj : j ∈ range k
hij :
  ((p (↑i : Fin (k + 1))).2, (p (↑i.succ : Fin (k + 1))).1) = ((p (↑j : Fin (k + 1))).2, (p (↑j.succ : Fin (k + 1))).1)
⊢ i = j
have i_inj : ∀ (hi : i < k) (j : ℕ) (hj : j < k)
  (hij :
    ((p (↑i : Fin (k + 1))).2, (p (↑i.succ : Fin (k + 1))).1) =
      ((p (↑j : Fin (k + 1))).2, (p (↑j.succ : Fin (k + 1))).1)),
  i = j
Tactic: rw [mem_range] at hi hj
Cleared hypotheses: hi, j, hj, hij
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Gaps (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
i : ℕ
hi : i < k
j : ℕ
hj : j < k
hij :
  ((p (↑i : Fin (k + 1))).2, (p (↑i.succ : Fin (k + 1))).1) = ((p (↑j : Fin (k + 1))).2, (p (↑j.succ : Fin (k + 1))).1)
⊢ i = j
have i_inj : i ∈ Set.Iio k
Tactic: apply F.intervalGapsWithin_injOn h a b
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Gaps (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
i : ℕ
hi : i < k
j : ℕ
hj : j < k
hij :
  ((p (↑i : Fin (k + 1))).2, (p (↑i.succ : Fin (k + 1))).1) = ((p (↑j : Fin (k + 1))).2, (p (↑j.succ : Fin (k + 1))).1)
i_inj : i ∈ Set.Iio k
⊢ i = j
have i_inj₁ : j ∈ Set.Iio k
Tactic: apply F.intervalGapsWithin_injOn h a b
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Gaps (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
z : α × α
hz : z ∈ F
⊢ ∃ (a : ℕ) (_ : a ∈ range k), ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1) = z
have i_surj : ∀ (i : ℕ) (hi₁ : i ∈ Set.Iio k)
  (hi₂ :
    (fun (j : ℕ) ↦
          ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
        i =
      z),
  ∃ (a : ℕ) (_ : a ∈ range k), ((p (↑a : Fin (k + 1))).2, (p (↑a.succ : Fin (k + 1))).1) = z
Tactic: obtain ⟨i, hi₁, hi₂⟩ := F.intervalGapsWithin_surjOn h a b hz
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Gaps (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ HMul.hMul (α := β)
      (∏ i ∈ range (k + 1),
        g (F.intervalGapsWithin h a b (↑i : Fin (k + 1))).2 / g (F.intervalGapsWithin h a b (↑i : Fin (k + 1))).1)
      (∏ z ∈ F, g z.2 / g z.1) =
    g b / g a
have rw : g (F.intervalGapsWithin h a b (↑k : Fin (k + 1))).1 / g (F.intervalGapsWithin h a b (↑0 : Fin (k + 1))).1 *
    (g (F.intervalGapsWithin h a b (↑k : Fin (k + 1))).2 / g (F.intervalGapsWithin h a b (↑k : Fin (k + 1))).1) =
  g b / g a
Tactic: rw [F.prod_eq_prod_range_intervalGapsWithin h (fun x y ↦ g y / g x), mul_comm,
      prod_range_succ, ← mul_assoc,
      ← prod_mul_distrib,
      prod_congr rfl (fun _ _ ↦ div_mul_div_cancel _ _ _),
      prod_range_div (fun i ↦ g (F.intervalGapsWithin h a b i).1)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : CommMonoid β
inst_1 : One α
f : ι → α
g : ι → α → β
s t : Finset ι
h : s ⊆ t
hg : ∀ (a : ι), g a 1 = 1
⊢ Eq.{u_4 + 1} (α := β) (∏ i ∈ t, g i ((↑s : Set ι).mulIndicator f i)) (∏ i ∈ s, g i ((↑s : Set ι).mulIndicator f i))
have rw : Eq.{u_4 + 1} (α := β) (∏ i ∈ t, g i ((↑s : Set ι).mulIndicator f i)) (∏ x ∈ t, g x ((↑s : Set ι).mulIndicator f x))
Tactic: rw [prod_subset h fun i _ hn ↦ by simp [hn, hg]]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : CommMonoid β
inst_1 : One α
f : ι → α
g : ι → α → β
s t : Finset ι
h : s ⊆ t
hg : ∀ (a : ι), g a 1 = 1
⊢ Eq.{u_4 + 1} (α := β) (∏ i ∈ t, g i ((↑s : Set ι).mulIndicator f i)) (∏ i ∈ s, g i (f i))
have _ : Eq.{u_4 + 1} (α := β) (∏ i ∈ t, g i ((↑s : Set ι).mulIndicator f i)) (∏ i ∈ s, g i ((↑s : Set ι).mulIndicator f i))
Tactic: calc
    _ = ∏ i ∈ s, g i (mulIndicator ↑s f i) := by rw [prod_subset h fun i _ hn ↦ by simp [hn, hg]]
    _ = _ := prod_congr rfl fun i hi ↦ congr_arg _ <| mulIndicator_of_mem hi f
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Indicator (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
s : Finset ι
f : ι → κ → β
t : ι → Set κ
g : ι → κ
inst_1 : DecidablePred fun (i : ι) ↦ g i ∈ t i
⊢ Eq.{u_4 + 1} (α := β) (∏ i ∈ s, (t i).mulIndicator (f i) (g i)) (∏ i ∈ s with g i ∈ t i, f i (g i))
have refine_1 : Eq.{u_4 + 1} (α := β) (∏ x ∈ s with g x ∈ t x, (t x).mulIndicator (f x) (g x)) (∏ i ∈ s with g i ∈ t i, f i (g i))
Tactic: refine (prod_filter_mul_prod_filter_not s (fun i ↦ g i ∈ t i) _).symm.trans <|
     Eq.trans (congr_arg₂ (· * ·) ?_ ?_) (mul_one _)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Indicator (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
s : Finset ι
f : ι → κ → β
t : ι → Set κ
g : ι → κ
inst_1 : DecidablePred fun (i : ι) ↦ g i ∈ t i
refine_1 :
  Eq.{u_4 + 1} (α := β) (∏ x ∈ s with g x ∈ t x, (t x).mulIndicator (f x) (g x)) (∏ i ∈ s with g i ∈ t i, f i (g i))
⊢ Eq.{u_4 + 1} (α := β) (∏ i ∈ s, (t i).mulIndicator (f i) (g i)) (∏ i ∈ s with g i ∈ t i, f i (g i))
have refine_2 : Eq.{u_4 + 1} (α := β) (∏ x ∈ s with g x ∉ t x, (t x).mulIndicator (f x) (g x)) 1
Tactic: refine (prod_filter_mul_prod_filter_not s (fun i ↦ g i ∈ t i) _).symm.trans <|
     Eq.trans (congr_arg₂ (· * ·) ?_ ?_) (mul_one _)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Indicator (goal)
Goal:
ι : Type u_1
β : Type u_4
inst : CommMonoid β
inst_1 : DecidableEq ι
s t : Finset ι
f : ι → β
⊢ Eq.{u_4 + 1} (α := β) (∏ i ∈ s, (↑t : Set ι).mulIndicator f i) (∏ i ∈ s ∩ t, f i)
have rw : Eq.{u_4 + 1} (α := β) (∏ i ∈ s with i ∈ (↑t : Set ι), f i) (∏ i ∈ s with i ∈ t, f i)
Tactic: rw [← filter_mem_eq_inter, prod_mulIndicator_eq_prod_filter]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Indicator (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hs : (↑s : Set ι).PairwiseDisjoint t),
    mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑(cons i s hi) : Set ι).PairwiseDisjoint t
⊢ mulIndicator (⋃ i_1 ∈ cons i s hi, t i_1) f = fun (a : κ) ↦ ∏ i ∈ cons i s hi, (t i).mulIndicator f a
have cons : ∀ (j : κ), mulIndicator (⋃ i_1 ∈ cons i s hi, t i_1) f j = ∏ i ∈ cons i s hi, (t i).mulIndicator f j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Indicator (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hs : (↑s : Set ι).PairwiseDisjoint t),
    mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑(cons i s hi) : Set ι).PairwiseDisjoint t
j : κ
⊢ mulIndicator (⋃ i_1 ∈ cons i s hi, t i_1) f j = ∏ i ∈ cons i s hi, (t i).mulIndicator f j
have cons : ∀ (hs : (↑s : Set ι).PairwiseDisjoint t ∧ ∀ j ∈ (↑s : Set ι), Disjoint (t i) (t j)) (j : κ),
  mulIndicator (⋃ i_1 ∈ cons i s hi, t i_1) f j = ∏ i ∈ cons i s hi, (t i).mulIndicator f j
Tactic: rw [coe_cons, Set.pairwiseDisjoint_insert_of_notMem (Finset.mem_coe.not.2 hi)] at hs
Cleared hypotheses: hs, j