awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Preimage
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst : CommMonoid β
f : ι → κ
inst_1 : DecidablePred fun (x : κ) ↦ x ∈ Set.range f
s : Finset κ
hf : Set.InjOn f (f ⁻¹' (↑s : Set κ))
g : κ → β
rw rw₁ : Eq.{u_3 + 1} (α := β) (∏ x ∈ s with x ∈ Set.range f, g x) (∏ x ∈ s with x ∈ Set.range f, g x)
⊢ Eq.{u_3 + 1} (α := β) (∏ x ∈ image f (s.preimage f hf), g x) (∏ x ∈ s with x ∈ Set.range f, g x)

Tactic:
rw [image_preimage]

Premises used: Finset.image_preimage
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Preimage
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst : CommMonoid β
f : ι → κ
inst_1 : DecidablePred fun (x : κ) ↦ x ∈ Set.range f
s : Finset κ
hf : Set.InjOn f (f ⁻¹' (↑s : Set κ))
g : κ → β
x : Eq.{u_3 + 1} (α := β) (∏ x ∈ image f (s.preimage f hf), g x) (∏ x ∈ s with x ∈ Set.range f, g x)
⊢ Eq.{u_3 + 1} (α := β) (∏ x ∈ s.preimage f hf, g (f x)) (∏ x ∈ s with x ∈ Set.range f, g x)

Tactic:
calc
    ∏ x ∈ preimage s f hf, g (f x) = ∏ x ∈ image f (preimage s f hf), g x :=
      Eq.symm <| prod_image <| by simpa [mem_preimage, Set.InjOn] using hf
    _ = ∏ x ∈ s with x ∈ Set.range f, g x := by rw [image_preimage]

Premises used: Finset.preimage, Set.range, Eq.symm, Finset.image, Finset.prod_image
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Preimage
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst : CommMonoid β
f : ι → κ
inst_1 : DecidablePred fun (x : κ) ↦ x ∈ Set.range f
s : Finset κ
hf : Set.InjOn f (f ⁻¹' (↑s : Set κ))
g : κ → β
x : Eq.{u_3 + 1} (α := β) (∏ x ∈ image f (s.preimage f hf), g x) (∏ x ∈ s with x ∈ Set.range f, g x)
⊢ Eq.{u_3 + 1} (α := β) (∏ x ∈ s.preimage f hf, g (f x)) (∏ x ∈ s with x ∈ Set.range f, g x)

Tactic:
classical
  calc
    ∏ x ∈ preimage s f hf, g (f x) = ∏ x ∈ image f (preimage s f hf), g x :=
      Eq.symm <| prod_image <| by simpa [mem_preimage, Set.InjOn] using hf
    _ = ∏ x ∈ s with x ∈ Set.range f, g x := by rw [image_preimage]

Premises used: Finset.preimage, Set.range, Eq.symm, Finset.prod_image
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Preimage
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' (↑s : Set κ))
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
rw : ∀ x ∈ s, g x ≠ 1 → x ∈ Set.range f
⊢ Eq.{u_3 + 1} (α := β) (∏ x ∈ s.preimage f hf, g (f x)) (∏ x ∈ s, g x)

Tactic:
rw [prod_preimage', prod_filter_of_ne]

Premises used: Finset.prod_filter_of_ne, Finset.prod_preimage'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Preimage
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' (↑s : Set κ))
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
⊢ ∀ x ∈ s, g x ≠ 1 → x ∈ Set.range f

Tactic:
fun x hx ↦ Not.imp_symm (hg x hx)

Premises used: Not.imp_symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Preimage
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' (↑s : Set κ))
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
⊢ ∀ x ∈ s, g x ≠ 1 → x ∈ Set.range f

Tactic:
exact fun x hx ↦ Not.imp_symm (hg x hx)

Premises used: Not.imp_symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Preimage
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.InjOn f (f ⁻¹' (↑s : Set κ))
g : κ → β
hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1
classical : Eq.{u_3 + 1} (α := β) (∏ x ∈ s with x ∈ Set.range f, g x) (∏ x ∈ s, g x)
classical₁ : Eq.{u_3 + 1} (α := β) (∏ x ∈ s, g x) (∏ x ∈ s, g x)
classical₂ : ∀ x ∈ s, g x ≠ 1 → x ∈ Set.range f
classical₃ : Eq.{u_3 + 1} (α := β) (∏ x ∈ s, g x) (∏ x ∈ s, g x)
classical₄ classical₅ classical₆ : ∀ x ∈ s, g x ≠ 1 → x ∈ Set.range f
⊢ Eq.{u_3 + 1} (α := β) (∏ x ∈ s.preimage f hf, g (f x)) (∏ x ∈ s, g x)

Tactic:
classical rw [prod_preimage', prod_filter_of_ne]; exact fun x hx ↦ Not.imp_symm (hg x hx)

Premises used: Not.imp_symm, Finset.prod_filter_of_ne, Finset.prod_preimage'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Preimage
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_3
inst : CommMonoid β
f : ι → κ
s : Finset κ
hf : Set.BijOn f (f ⁻¹' (↑s : Set κ)) (↑s : Set κ)
g : κ → β
⊢ Eq.{u_3 + 1} (α := β) (∏ x ∈ s.preimage f ⋯, g (f x)) (∏ x ∈ s, g x)

Tactic:
prod_preimage _ _ hf.injOn g fun _ hs h_f ↦ (h_f <| hf.subset_range hs).elim

Premises used: False.elim, Finset.prod_preimage, Set.BijOn.injOn, Set.BijOn.subset_range
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
inst : CommMonoid β
σ : α → Type u_6
s : Finset α
t : (a : α) → Finset (σ a)
f : Sigma σ → β
simp_rw :
  Eq.{u_4 + 1} (α := β) (∏ x ∈ s.disjiUnion (fun (i : α) ↦ map (Embedding.sigmaMk (β := σ) i) (t i)) ⋯, f x)
    (∏ a ∈ s, ∏ s ∈ t a, f (Sigma.mk (β := σ) a s))
simp_rw₁ :
  Eq.{u_4 + 1} (α := β) (∏ i ∈ s, ∏ x ∈ map (Embedding.sigmaMk (β := σ) i) (t i), f x)
    (∏ a ∈ s, ∏ s ∈ t a, f (Sigma.mk (β := σ) a s))
simp_rw₂ :
  Eq.{u_4 + 1} (α := β) (∏ x ∈ s, ∏ x_1 ∈ t x, f ((Embedding.sigmaMk (β := σ) x : (a : σ x) → (i : α) × σ i) x_1))
    (∏ a ∈ s, ∏ s ∈ t a, f (Sigma.mk (β := σ) a s))
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s.sigma (α := σ) t, f x) (∏ a ∈ s, ∏ s ∈ t a, f (Sigma.mk (β := σ) a s))

Tactic:
simp_rw [← disjiUnion_map_sigma_mk, prod_disjiUnion, prod_map, Function.Embedding.sigmaMk_apply]

Premises used: Function.Embedding.sigmaMk_apply, Finset.prod_disjiUnion, Finset.prod_map, Finset.disjiUnion_map_sigma_mk
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
inst : CommMonoid β
σ : α → Type u_6
s : Finset α
t : (a : α) → Finset (σ a)
f : (a : α) → σ a → β
⊢ Eq.{u_4 + 1} (α := β) (∏ a ∈ s, ∏ s ∈ t a, f a s)
    (∏ x ∈ s.sigma (α := σ) t, f (x.fst (β := fun (i : α) ↦ σ i)) (x.snd (β := fun (i : α) ↦ σ i)))

Tactic:
Eq.symm <| prod_sigma s t fun x => f x.1 x.2

Premises used: Sigma.fst, Finset.prod_sigma, Eq.symm, Sigma.snd
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
⊢ Eq.{u_4 + 1} (α := β) (∏ p ∈ r, f p) (∏ c ∈ s, ∏ a ∈ t c, f (c, a))

Tactic:
Eq.trans ?_ (prod_sigma s t fun p => f (p.1, p.2))

Premises used: Prod.mk, Sigma.fst, Finset.prod_sigma, Sigma.snd, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
refine :
  Eq.{u_4 + 1} (α := β) (∏ p ∈ r, f p)
    (∏ x ∈ s.sigma (α := fun (a : γ) ↦ α) t, f (x.fst (β := fun (a : γ) ↦ α), x.snd (β := fun (a : γ) ↦ α)))
⊢ Eq.{u_4 + 1} (α := β) (∏ p ∈ r, f p) (∏ c ∈ s, ∏ a ∈ t c, f (c, a))

Tactic:
refine Eq.trans ?_ (prod_sigma s t fun p => f (p.1, p.2))

Premises used: Prod.mk, Sigma.fst, Finset.prod_sigma, Sigma.snd, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
hst :
  ∀ (i : γ × α),
    i ∈ r ↔
      Membership.mem (α := (_ : γ) × α) (s.sigma (α := fun (a : γ) ↦ α) t)
        (((Equiv.sigmaEquivProd γ α).symm : (a : γ × α) → (_ : γ) × α) i : (_ : γ) × α)
hfg :
  ∀ i ∈ r,
    f i =
      f
        (Sigma.fst (β := fun (a : γ) ↦ α) (((Equiv.sigmaEquivProd γ α).symm : (a : γ × α) → (_ : γ) × α) i),
          Sigma.snd (β := fun (a : γ) ↦ α) (((Equiv.sigmaEquivProd γ α).symm : (a : γ × α) → (_ : γ) × α) i))
⊢ Eq.{u_4 + 1} (α := β) (∏ p ∈ r, f p)
    (∏ x ∈ s.sigma (α := fun (a : γ) ↦ α) t, f (x.fst (β := fun (a : γ) ↦ α), x.snd (β := fun (a : γ) ↦ α)))

Tactic:
apply prod_equiv (Equiv.sigmaEquivProd _ _).symm

Premises used: Finset.prod_equiv, Equiv.symm, Equiv.sigmaEquivProd
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
⊢ ∀ (i : γ × α),
    i ∈ r ↔
      Membership.mem (α := (_ : γ) × α) (s.sigma (α := fun (a : γ) ↦ α) t)
        (((Equiv.sigmaEquivProd γ α).symm : (a : γ × α) → (_ : γ) × α) i : (_ : γ) × α)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
⊢ ∀ i ∈ r,
    f i =
      f
        (Sigma.fst (β := fun (a : γ) ↦ α) (((Equiv.sigmaEquivProd γ α).symm : (a : γ × α) → (_ : γ) × α) i),
          Sigma.snd (β := fun (a : γ) ↦ α) (((Equiv.sigmaEquivProd γ α).symm : (a : γ × α) → (_ : γ) × α) i))

Tactic:
simp [h]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ → α → β
⊢ Eq.{u_4 + 1} (α := β) (∏ p ∈ r, f p.1 p.2) (∏ c ∈ s, ∏ a ∈ t c, f c a)

Tactic:
prod_finset_product r s t h

Premises used: Finset.prod_finset_product
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
r : Finset (α × γ)
s : Finset γ
t : γ → Finset α
h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
⊢ Eq.{u_4 + 1} (α := β) (∏ p ∈ r, f p) (∏ c ∈ s, ∏ a ∈ t c, f (a, c))

Tactic:
Eq.trans ?_ (prod_sigma s t fun p => f (p.2, p.1))

Premises used: Prod.mk, Sigma.fst, Finset.prod_sigma, Sigma.snd, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
r : Finset (α × γ)
s : Finset γ
t : γ → Finset α
h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
refine :
  Eq.{u_4 + 1} (α := β) (∏ p ∈ r, f p)
    (∏ x ∈ s.sigma (α := fun (a : γ) ↦ α) t, f (x.snd (β := fun (a : γ) ↦ α), x.fst (β := fun (a : γ) ↦ α)))
⊢ Eq.{u_4 + 1} (α := β) (∏ p ∈ r, f p) (∏ c ∈ s, ∏ a ∈ t c, f (a, c))

Tactic:
refine Eq.trans ?_ (prod_sigma s t fun p => f (p.2, p.1))

Premises used: Prod.mk, Sigma.fst, Finset.prod_sigma, Sigma.snd, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
r : Finset (α × γ)
s : Finset γ
t : γ → Finset α
h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
hst :
  ∀ (i : α × γ),
    i ∈ r ↔
      Membership.mem (α := (_ : γ) × α) (s.sigma (α := fun (a : γ) ↦ α) t)
        (((Equiv.prodComm α γ).trans (Equiv.sigmaEquivProd γ α).symm : (a : α × γ) → (_ : γ) × α) i : (_ : γ) × α)
hfg :
  ∀ i ∈ r,
    f i =
      f
        (Sigma.snd (β := fun (a : γ) ↦ α)
            (((Equiv.prodComm α γ).trans (Equiv.sigmaEquivProd γ α).symm : (a : α × γ) → (_ : γ) × α) i),
          Sigma.fst (β := fun (a : γ) ↦ α)
            (((Equiv.prodComm α γ).trans (Equiv.sigmaEquivProd γ α).symm : (a : α × γ) → (_ : γ) × α) i))
⊢ Eq.{u_4 + 1} (α := β) (∏ p ∈ r, f p)
    (∏ x ∈ s.sigma (α := fun (a : γ) ↦ α) t, f (x.snd (β := fun (a : γ) ↦ α), x.fst (β := fun (a : γ) ↦ α)))

Tactic:
apply prod_equiv ((Equiv.prodComm _ _).trans (Equiv.sigmaEquivProd _ _).symm)

Premises used: Equiv.trans, Equiv.prodComm, Finset.prod_equiv, Equiv.symm, Equiv.sigmaEquivProd
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
r : Finset (α × γ)
s : Finset γ
t : γ → Finset α
h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
⊢ ∀ (i : α × γ),
    i ∈ r ↔
      Membership.mem (α := (_ : γ) × α) (s.sigma (α := fun (a : γ) ↦ α) t)
        (((Equiv.prodComm α γ).trans (Equiv.sigmaEquivProd γ α).symm : (a : α × γ) → (_ : γ) × α) i : (_ : γ) × α)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
r : Finset (α × γ)
s : Finset γ
t : γ → Finset α
h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
⊢ ∀ i ∈ r,
    f i =
      f
        (Sigma.snd (β := fun (a : γ) ↦ α)
            (((Equiv.prodComm α γ).trans (Equiv.sigmaEquivProd γ α).symm : (a : α × γ) → (_ : γ) × α) i),
          Sigma.fst (β := fun (a : γ) ↦ α)
            (((Equiv.prodComm α γ).trans (Equiv.sigmaEquivProd γ α).symm : (a : α × γ) → (_ : γ) × α) i))

Tactic:
simp [h]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
r : Finset (α × γ)
s : Finset γ
t : γ → Finset α
h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2
f : α → γ → β
⊢ Eq.{u_4 + 1} (α := β) (∏ p ∈ r, f p.1 p.2) (∏ c ∈ s, ∏ a ∈ t c, f a c)

Tactic:
prod_finset_product_right r s t h

Premises used: Finset.prod_finset_product_right
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
s : Finset γ
t : Finset α
f : γ × α → β
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s ×ˢ t, f x) (∏ x ∈ s, ∏ y ∈ t, f (x, y))

Tactic:
prod_finset_product (s ×ˢ t) s (fun _a => t) fun _p => mem_product

Premises used: Finset.prod_finset_product, SProd.sprod, Finset.mem_product
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
s : Finset γ
t : Finset α
f : γ → α → β
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s ×ˢ t, f x.1 x.2) (∏ x ∈ s, ∏ y ∈ t, f x y)

Tactic:
prod_product ..

Premises used: Finset.prod_product
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
s : Finset γ
t : Finset α
f : γ × α → β
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s ×ˢ t, f x) (∏ y ∈ t, ∏ x ∈ s, f (x, y))

Tactic:
prod_finset_product_right (s ×ˢ t) t (fun _a => s) fun _p => mem_product.trans and_comm

Premises used: SProd.sprod, and_comm, Finset.prod_finset_product_right, Iff.trans, Finset.mem_product
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
s : Finset γ
t : Finset α
f : γ → α → β
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s ×ˢ t, f x.1 x.2) (∏ y ∈ t, ∏ x ∈ s, f x y)

Tactic:
prod_product_right ..

Premises used: Finset.prod_product_right
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
x : γ
y : α
⊢ Membership.mem (γ := Finset (γ × α)) (s.biUnion fun (x : γ) ↦ map (Embedding.sectR x α) (t x)) (x, y) ↔
    (x, y).1 ∈ s ∧ (x, y).2 ∈ t (x, y).1

Tactic:
simp only [mem_biUnion, mem_map, Function.Embedding.sectR_apply, Prod.mk.injEq,
        exists_eq_right, ← and_assoc]

Premises used: Function.Embedding.sectR_apply, exists_eq_right, Prod.mk.injEq, and_assoc, Finset.mem_map, Finset.mem_biUnion
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
⊢ ∀ (z : γ × α),
    Membership.mem (γ := Finset (γ × α)) (s.biUnion fun (x : γ) ↦ map (Embedding.sectR x α) (t x)) z ↔
      z.1 ∈ s ∧ z.2 ∈ t z.1

Tactic:
have : ∀ z : γ × α, (z ∈ s.biUnion fun x => (t x).map <| Function.Embedding.sectR x _) ↔
      z.1 ∈ s ∧ z.2 ∈ t z.1 := by
      rintro ⟨x, y⟩
      simp only [mem_biUnion, mem_map, Function.Embedding.sectR_apply, Prod.mk.injEq,
        exists_eq_right, ← and_assoc]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
this :
  ∀ (z : γ × α),
    Membership.mem (γ := Finset (γ × α)) (s.biUnion fun (x : γ) ↦ map (Embedding.sectR x α) (t x)) z ↔
      z.1 ∈ s ∧ z.2 ∈ t z.1
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s, ∏ y ∈ t x, f x y) (∏ y ∈ t', ∏ x ∈ s' y, f x y)

Tactic:
(prod_finset_product' _ _ _ this).symm.trans
        ((prod_finset_product_right' _ _ _) fun ⟨x, y⟩ => (this _).trans ((h x y).trans and_comm))

Premises used: Finset.map, Membership.mem, Prod.mk, and_comm, Finset.biUnion, Finset.prod_finset_product_right', Prod.fst, And, Iff, _private.0.Finset.prod_comm'.match_4, Iff.trans, Function.Embedding.sectR, Finset.prod_finset_product', Eq.symm, Prod.snd, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
this :
  ∀ (z : γ × α),
    Membership.mem (γ := Finset (γ × α)) (s.biUnion fun (x : γ) ↦ map (Embedding.sectR x α) (t x)) z ↔
      z.1 ∈ s ∧ z.2 ∈ t z.1
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s, ∏ y ∈ t x, f x y) (∏ y ∈ t', ∏ x ∈ s' y, f x y)

Tactic:
exact
      (prod_finset_product' _ _ _ this).symm.trans
        ((prod_finset_product_right' _ _ _) fun ⟨x, y⟩ => (this _).trans ((h x y).trans and_comm))

Premises used: Finset.map, Membership.mem, Prod.mk, and_comm, Finset.biUnion, Finset.prod_finset_product_right', Prod.fst, And, Iff, _private.0.Finset.prod_comm'.match_4, Iff.trans, Function.Embedding.sectR, Finset.prod_finset_product', Eq.symm, Prod.snd, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
have :
  ∀ (z : γ × α),
    Membership.mem (γ := Finset (γ × α)) (s.biUnion fun (x : γ) ↦ map (Embedding.sectR x α) (t x)) z ↔
      z.1 ∈ s ∧ z.2 ∈ t z.1
have₁ :
  ∀
    (this :
      ∀ (z : γ × α),
        Membership.mem (γ := Finset (γ × α)) (s.biUnion fun (x : γ) ↦ map (Embedding.sectR x α) (t x)) z ↔
          z.1 ∈ s ∧ z.2 ∈ t z.1),
    Eq.{u_4 + 1} (α := β) (∏ x ∈ s, ∏ y ∈ t x, f x y) (∏ y ∈ t', ∏ x ∈ s' y, f x y)
have₂ :
  ∀ (z : γ × α),
    Membership.mem (γ := Finset (γ × α)) (s.biUnion fun (x : γ) ↦ map (Embedding.sectR x α) (t x)) z ↔
      z.1 ∈ s ∧ z.2 ∈ t z.1
have₃ have₄ :
  ∀
    (this :
      ∀ (z : γ × α),
        Membership.mem (γ := Finset (γ × α)) (s.biUnion fun (x : γ) ↦ map (Embedding.sectR x α) (t x)) z ↔
          z.1 ∈ s ∧ z.2 ∈ t z.1),
    Eq.{u_4 + 1} (α := β) (∏ x ∈ s, ∏ y ∈ t x, f x y) (∏ y ∈ t', ∏ x ∈ s' y, f x y)
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s, ∏ y ∈ t x, f x y) (∏ y ∈ t', ∏ x ∈ s' y, f x y)

Tactic:
classical
    have : ∀ z : γ × α, (z ∈ s.biUnion fun x => (t x).map <| Function.Embedding.sectR x _) ↔
      z.1 ∈ s ∧ z.2 ∈ t z.1 := by
      rintro ⟨x, y⟩
      simp only [mem_biUnion, mem_map, Function.Embedding.sectR_apply, Prod.mk.injEq,
        exists_eq_right, ← and_assoc]
    exact
      (prod_finset_product' _ _ _ this).symm.trans
        ((prod_finset_product_right' _ _ _) fun ⟨x, y⟩ => (this _).trans ((h x y).trans and_comm))
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
s : Finset γ
t : Finset α
f : γ → α → β
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s, ∏ y ∈ t, f x y) (∏ y ∈ t, ∏ x ∈ s, f x y)

Tactic:
prod_comm' fun _ _ => Iff.rfl

Premises used: Finset.prod_comm', Iff.rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
κ : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst : CommMonoid β
s : Finset γ
t : Finset α
u : Finset κ
f : γ → α → κ → β
simp_rw : Eq.{u_4 + 1} (α := β) (∏ x ∈ s, ∏ y ∈ u, ∏ x_1 ∈ t, f x x_1 y) (∏ z ∈ u, ∏ x ∈ s, ∏ y ∈ t, f x y z)
⊢ Eq.{u_4 + 1} (α := β) (∏ x ∈ s, ∏ y ∈ t, ∏ z ∈ u, f x y z) (∏ z ∈ u, ∏ x ∈ s, ∏ y ∈ t, f x y z)

Tactic:
simp_rw [prod_comm (s := t), prod_comm (s := s)]

Premises used: Finset.prod_comm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Goal:
α : Type u_3
σ : α → Type u_6
s : Finset α
t : (a : α) → Finset (σ a)
⊢ #(s.sigma (α := σ) t) = ∑ a ∈ s, #(t a)

Tactic:
Multiset.card_sigma _ _

Premises used: Multiset.sum, Multiset.foldr, Multiset.sigma, Multiset.join, Finset.card, Multiset.bind, Finset.sum, Multiset.card_sigma
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : Monoid N
R : M → N → Prop
h : R 1 1
hf : (R ⇒ R ⇒ R) (fun (x1 x2 : M) ↦ x1 * x2) fun (x1 x2 : N) ↦ x1 * x2
⊢ (Forall₂ R ⇒ R) prod prod

Tactic:
rel_foldr hf h

Premises used: List.rel_foldr, List.prod
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : Monoid N
l : List M
F : Type u_8
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
hl_1 : l ≠ []
x : M
xs : List M
hl : x :: xs ≠ []
nil :
  ∀ (x : M) (hl : [x] ≠ []),
    Eq.{u_5 + 1} (α := N) (prod (map (⇑f : (a : M) → N) [x]) : N) ((f : (a : M) → N) [x].prod : N)
cons :
  ∀ (head : M) (tail : List M),
    (∀ (x : M) (hl : x :: tail ≠ []),
        Eq.{u_5 + 1} (α := N) (prod (map (⇑f : (a : M) → N) (x :: tail)) : N)
          ((f : (a : M) → N) (x :: tail).prod : N)) →
      ∀ (x : M) (hl : x :: head :: tail ≠ []),
        Eq.{u_5 + 1} (α := N) (prod (map (⇑f : (a : M) → N) (x :: head :: tail)) : N)
          ((f : (a : M) → N) (x :: head :: tail).prod : N)
⊢ Eq.{u_5 + 1} (α := N) (prod (map (⇑f : (a : M) → N) (x :: xs)) : N) ((f : (a : M) → N) (x :: xs).prod : N)

Tactic:
induction xs generalizing x
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : Monoid N
l : List M
F : Type u_8
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
hl_1 : l ≠ []
x : M
hl : [x] ≠ []
⊢ Eq.{u_5 + 1} (α := N) (prod (map (⇑f : (a : M) → N) [x]) : N) ((f : (a : M) → N) [x].prod : N)

Tactic:
simp_all
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : Monoid N
l : List M
F : Type u_8
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
hl_1 : l ≠ []
head : M
tail : List M
tail_ih :
  ∀ (x : M) (hl : x :: tail ≠ []),
    Eq.{u_5 + 1} (α := N) (prod (map (⇑f : (a : M) → N) (x :: tail)) : N) ((f : (a : M) → N) (x :: tail).prod : N)
x : M
hl : x :: head :: tail ≠ []
⊢ Eq.{u_5 + 1} (α := N) (prod (map (⇑f : (a : M) → N) (x :: head :: tail)) : N)
    ((f : (a : M) → N) (x :: head :: tail).prod : N)

Tactic:
simp_all
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : Monoid N
l : List M
F : Type u_8
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
simp :
  Eq.{u_5 + 1} (α := N)
    (foldr (fun (x : M) (y : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) x : N) y) ((f : (a : M) → N) 1) l : N)
    ((f : (a : M) → N) (foldr (fun (x1 x2 : M) ↦ x1 * x2) 1 l) : N)
⊢ Eq.{u_5 + 1} (α := N) (prod (map (⇑f : (a : M) → N) l) : N) ((f : (a : M) → N) l.prod : N)

Tactic:
simp only [prod, foldr_map, ← map_one f]

Premises used: map_one, List.foldr_map, List.prod
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : Monoid N
l : List M
F : Type u_8
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
⊢ Eq.{u_5 + 1} (α := N)
    (foldr (fun (x : M) (y : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) x : N) y) ((f : (a : M) → N) 1) l : N)
    ((f : (a : M) → N) (foldr (fun (x1 x2 : M) ↦ x1 * x2) 1 l) : N)

Tactic:
l.foldr_hom f (fun x y => (map_mul f x y).symm)

Premises used: List.foldr_hom, map_mul, Eq.symm, DFunLike.coe
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : Monoid N
l : List M
F : Type u_8
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
⊢ Eq.{u_5 + 1} (α := N)
    (foldr (fun (x : M) (y : N) ↦ HMul.hMul (α := N) ((f : (a : M) → N) x : N) y) ((f : (a : M) → N) 1) l : N)
    ((f : (a : M) → N) (foldr (fun (x1 x2 : M) ↦ x1 * x2) 1 l) : N)

Tactic:
exact l.foldr_hom f (fun x y => (map_mul f x y).symm)

Premises used: List.foldr_hom, map_mul, Eq.symm, DFunLike.coe