awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeSup δ
inst_2 : OrderBot δ
g : γ → δ
simp :
  Eq.{u_7 + 1} (α := δ) (s.sup fun (i : α) ↦ t.sup fun (i' : β) ↦ (g ∘ uncurry f) (i, i'))
    (s.sup fun (x : α) ↦ t.sup fun (x_1 : β) ↦ g (f x x_1))
⊢ (image₂ f s t).sup g = s.sup fun (x : α) ↦ t.sup fun (x_1 : β) ↦ g (f x x_1)

Tactic:
simp only [image₂, sup_image, sup_product_left]

Premises used: Finset.sup_product_left, Finset.sup_image, Finset.image₂
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeSup δ
inst_2 : OrderBot δ
g : γ → δ
⊢ Eq.{u_7 + 1} (α := δ) (s.sup fun (i : α) ↦ t.sup fun (i' : β) ↦ (g ∘ uncurry f) (i, i'))
    (s.sup fun (x : α) ↦ t.sup fun (x_1 : β) ↦ g (f x x_1))

Tactic:
rfl
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeSup δ
inst_2 : OrderBot δ
g : γ → δ
simp :
  Eq.{u_7 + 1} (α := δ) (t.sup fun (i' : β) ↦ s.sup fun (i : α) ↦ (g ∘ uncurry f) (i, i'))
    (t.sup fun (y : β) ↦ s.sup fun (x : α) ↦ g (f x y))
⊢ (image₂ f s t).sup g = t.sup fun (y : β) ↦ s.sup fun (x : α) ↦ g (f x y)

Tactic:
simp only [image₂, sup_image, sup_product_right]

Premises used: Finset.sup_product_right, Finset.sup_image, Finset.image₂
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeSup δ
inst_2 : OrderBot δ
g : γ → δ
⊢ Eq.{u_7 + 1} (α := δ) (t.sup fun (i' : β) ↦ s.sup fun (i : α) ↦ (g ∘ uncurry f) (i, i'))
    (t.sup fun (y : β) ↦ s.sup fun (x : α) ↦ g (f x y))

Tactic:
rfl
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeInf δ
g : γ → δ
a : δ
h : (image₂ f s t).Nonempty
rw : (∀ b ∈ image₂ f s t, a ≤ g b) ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)
rw₁ rw₂ : (∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)) ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)
⊢ a ≤ (image₂ f s t).inf' h g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)

Tactic:
rw [le_inf'_iff, forall_mem_image₂]

Premises used: Finset.le_inf'_iff, Finset.forall_mem_image₂
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeInf δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (image₂ f s t).inf' h g = s.inf' ⋯ fun (x : α) ↦ t.inf' ⋯ fun (x_1 : β) ↦ g (f x x_1)

Tactic:
sup'_image₂_left (δ := δᵒᵈ) g h

Premises used: Finset.sup'_image₂_left, Finset.inf', WithTop.some, WithTop.untop, OrderDual, Finset.inf, WithTop
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeInf δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (image₂ f s t).inf' h g = t.inf' ⋯ fun (y : β) ↦ s.inf' ⋯ fun (x : α) ↦ g (f x y)

Tactic:
sup'_image₂_right (δ := δᵒᵈ) g h

Premises used: Finset.inf', WithTop.some, WithTop.untop, OrderDual, Finset.inf, Finset.sup'_image₂_right, WithTop
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeInf δ
inst_2 : OrderTop δ
g : γ → δ
a : δ
⊢ a ≤ (image₂ f s t).inf g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)

Tactic:
sup_image₂_le (δ := δᵒᵈ)

Premises used: OrderDual, Finset.inf, Finset.sup_image₂_le
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeInf δ
inst_2 : OrderTop δ
g : γ → δ
⊢ (image₂ f s t).inf g = s.inf fun (x : α) ↦ t.inf (g ∘ f x)

Tactic:
sup_image₂_left (δ := δᵒᵈ) ..

Premises used: OrderDual, Finset.inf, Finset.sup_image₂_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeInf δ
inst_2 : OrderTop δ
g : γ → δ
⊢ (image₂ f s t).inf g = t.inf fun (y : β) ↦ s.inf fun (x : α) ↦ g (f x y)

Tactic:
sup_image₂_right (δ := δᵒᵈ) ..

Premises used: OrderDual, Finset.inf, Finset.sup_image₂_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
ι : Type u_14
α : ι → Type u_15
β : ι → Type u_16
γ : ι → Type u_17
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → DecidableEq (γ i)
f : (i : ι) → α i → β i → γ i
s : (i : ι) → Finset (α i)
t : (i : ι) → Finset (β i)
h :
  ∀ (a : (a : ι) → γ a),
    Membership.mem (γ := Finset ((a : ι) → γ a)) (piFinset (δ := γ) fun (i : ι) ↦ image₂ (f i) (s i) (t i)) a ↔
      Membership.mem (γ := Finset ((a : ι) → γ a))
        (image₂ (fun (a : (a : ι) → α a) (b : (a : ι) → β a) (i : ι) ↦ f i (a i) (b i)) (piFinset (δ := α) s)
          (piFinset (δ := β) t))
        a
⊢ Eq (α := Finset ((a : ι) → γ a)) (piFinset (δ := γ) fun (i : ι) ↦ image₂ (f i) (s i) (t i))
    (image₂ (fun (a : (a : ι) → α a) (b : (a : ι) → β a) (i : ι) ↦ f i (a i) (b i)) (piFinset (δ := α) s)
      (piFinset (δ := β) t))

Tactic:
ext
-- Module: Mathlib.Data.Finset.NAry
Goal:
ι : Type u_14
α : ι → Type u_15
β : ι → Type u_16
γ : ι → Type u_17
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → DecidableEq (γ i)
f : (i : ι) → α i → β i → γ i
s : (i : ι) → Finset (α i)
t : (i : ι) → Finset (β i)
a : (a : ι) → γ a
⊢ Membership.mem (γ := Finset ((a : ι) → γ a)) (piFinset (δ := γ) fun (i : ι) ↦ image₂ (f i) (s i) (t i)) a ↔
    Membership.mem (γ := Finset ((a : ι) → γ a))
      (image₂ (fun (a : (a : ι) → α a) (b : (a : ι) → β a) (i : ι) ↦ f i (a i) (b i)) (piFinset (δ := α) s)
        (piFinset (δ := β) t))
      a

Tactic:
simp only [mem_piFinset, mem_image₂, Classical.skolem, forall_and, funext_iff]

Premises used: Classical.skolem, Fintype.mem_piFinset, funext_iff, Finset.mem_image₂, forall_and
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
inst_1 : Fintype (↑s : Type u_1)
inst_2 : Fintype (↑t : Type u_3)
inst_3 : Fintype (↑(image2 f s t) : Type u_5)
⊢ (↑(image2 f s t).toFinset : Set γ) = (↑(image₂ f s.toFinset t.toFinset) : Set γ)

Tactic:
simp
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
hf : (image2 f s t).Finite
⊢ (↑(hf.toFinset (s := image2 f s t)) : Set γ) = (↑(image₂ f (hs.toFinset (s := s)) (ht.toFinset (s := t))) : Set γ)

Tactic:
simp
-- Module: Mathlib.Data.Finset.NatDivisors
Goal:
m n : ℕ
h : ∀ (k : ℕ), k ∈ (m * n).divisors ↔ k ∈ m.divisors * n.divisors
⊢ (m * n).divisors = m.divisors * n.divisors

Tactic:
ext k
-- Module: Mathlib.Data.Finset.NatDivisors
Goal:
m n k : ℕ
h :
  (∃ (x : ℕ) (x_1 : ℕ), (x ∣ m ∧ x_1 ∣ n ∧ x * x_1 = k) ∧ m ≠ 0 ∧ n ≠ 0) ↔
    ∃ (y : ℕ) (x : ℕ), (y ∣ m ∧ m ≠ 0) ∧ (x ∣ n ∧ n ≠ 0) ∧ y * x = k
⊢ k ∈ (m * n).divisors ↔ k ∈ m.divisors * n.divisors

Tactic:
simp_rw [mem_mul, mem_divisors, Nat.dvd_mul, mul_ne_zero_iff, ← exists_and_left,
    ← exists_and_right]

Premises used: Nat.mem_divisors, exists_and_left, exists_and_right, Nat.dvd_mul, mul_ne_zero_iff, Finset.mem_mul
-- Module: Mathlib.Data.Finset.NatDivisors
Goal:
m n k : ℕ
⊢ (∃ (x : ℕ) (x_1 : ℕ), (x ∣ m ∧ x_1 ∣ n ∧ x * x_1 = k) ∧ m ≠ 0 ∧ n ≠ 0) ↔
    ∃ (y : ℕ) (x : ℕ), (y ∣ m ∧ m ≠ 0) ∧ (x ∣ n ∧ n ≠ 0) ∧ y * x = k

Tactic:
simp only [and_assoc, and_comm, and_left_comm]

Premises used: and_left_comm, and_comm, and_assoc
-- Module: Mathlib.Data.Finset.NatDivisors
Goal:
p : ℕ
hp : Prime p
⊢ (HPow.hPow (β := ℕ) p 2).divisors = {HPow.hPow (β := ℕ) p 2, p, 1}

Tactic:
simp [divisors_prime_pow hp, range_add_one]

Premises used: Nat.divisors_prime_pow, Finset.range_add_one
-- Module: Mathlib.Data.Finset.NatDivisors
Goal:
l : List ℕ
⊢ l.prod.divisors = (map divisors l).prod

Tactic:
map_list_prod Nat.divisorsHom l

Premises used: Nat.divisorsHom, map_list_prod, Nat.divisors, Finset.filter
-- Module: Mathlib.Data.Finset.NatDivisors
Goal:
s : Multiset ℕ
⊢ s.prod.divisors = (map divisors s).prod

Tactic:
map_multiset_prod Nat.divisorsHom s

Premises used: Nat.divisorsHom, map_multiset_prod, Nat.divisors, Finset.filter
-- Module: Mathlib.Data.Finset.NatDivisors
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ divisors (∏ i ∈ s, f i) = ∏ i ∈ s, (f i).divisors

Tactic:
map_prod Nat.divisorsHom f s

Premises used: Nat.divisorsHom, map_prod, Nat.divisors, Finset.filter
-- Module: Mathlib.Data.Finset.NatDivisors
Goal:
m n : ℕ
hmn : m.Coprime n
dm₁ dn₁ : ℕ
h₁ : (dm₁, dn₁) ∈ (↑(m.divisors ×ˢ n.divisors) : Set (ℕ × ℕ))
dm₂ dn₂ : ℕ
h₂ : (dm₂, dn₂) ∈ (↑(m.divisors ×ˢ n.divisors) : Set (ℕ × ℕ))
hd : Eq (α := ℕ) ((fun (p : ℕ × ℕ) ↦ p.1 * p.2) (dm₁, dn₁)) ((fun (p : ℕ × ℕ) ↦ p.1 * p.2) (dm₂, dn₂))
⊢ (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0

Tactic:
simp only [Finset.mem_coe, Finset.mem_product, mem_divisors] at *

Premises used: Nat.mem_divisors, Finset.mem_product, Finset.mem_coe
-- Module: Mathlib.Data.Finset.NatDivisors
Goal:
m n : ℕ
hmn : m.Coprime n
dm₁ dn₁ : ℕ
h₁ : (dm₁, dn₁) ∈ (↑(m.divisors ×ˢ n.divisors) : Set (ℕ × ℕ))
dm₂ dn₂ : ℕ
h₂ : (dm₂, dn₂) ∈ (↑(m.divisors ×ˢ n.divisors) : Set (ℕ × ℕ))
hd : Eq (α := ℕ) ((fun (p : ℕ × ℕ) ↦ p.1 * p.2) (dm₁, dn₁)) ((fun (p : ℕ × ℕ) ↦ p.1 * p.2) (dm₂, dn₂))
h₃ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0
⊢ (dm₂ ∣ m ∧ m ≠ 0) ∧ dn₂ ∣ n ∧ n ≠ 0

Tactic:
simp only [Finset.mem_coe, Finset.mem_product, mem_divisors] at *

Premises used: Nat.mem_divisors, Finset.mem_product, Finset.mem_coe
-- Module: Mathlib.Data.Finset.NatDivisors
Goal:
m n : ℕ
hmn : m.Coprime n
dm₁ dn₁ dm₂ dn₂ : ℕ
hd : dm₁ * dn₁ = dm₂ * dn₂
h₁ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0
h₂ : (dm₂ ∣ m ∧ m ≠ 0) ∧ dn₂ ∣ n ∧ n ≠ 0
this : dm₁ = dm₂
rwa :
  ∀ (hd : dm₂ * dn₁ = dm₂ * dn₂) (h₁ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0) (h₂ : (dm₂ ∣ m ∧ m ≠ 0) ∧ dn₂ ∣ n ∧ n ≠ 0)
    (this : dm₁ = dm₂), (dm₁, dn₁).2 = (dm₂, dn₂).2
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (hd : dn₁ = dn₂) (h₁ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0) (h₂ : (dm₂ ∣ m ∧ m ≠ 0) ∧ dn₂ ∣ n ∧ n ≠ 0)
    (this : dm₁ = dm₂), (dm₁, dn₁).2 = (dm₂, dn₂).2
⊢ (dm₁, dn₁).2 = (dm₂, dn₂).2

Tactic:
rwa [this, Nat.mul_right_inj (by simp [·] at h₂)] at hd

Premises used: Nat.mul_right_inj
-- Module: Mathlib.Data.Finset.NatDivisors
Goal:
m n : ℕ
hmn : m.Coprime n
dm₁ dn₁ dm₂ dn₂ : ℕ
hd : dm₁ * dn₁ = dm₂ * dn₂
h₁ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0
h₂ : (dm₂ ∣ m ∧ m ≠ 0) ∧ dn₂ ∣ n ∧ n ≠ 0
suffices : dm₁ = dm₂
⊢ (dm₁, dn₁) = (dm₂, dn₂)

Tactic:
suffices dm₁ = dm₂ from Prod.ext this <| by
    rwa [this, Nat.mul_right_inj (by simp [·] at h₂)] at hd
-- Module: Mathlib.Data.Finset.NatDivisors
Goal:
m n : ℕ
hmn : m.Coprime n
dm₁ dn₁ dm₂ dn₂ : ℕ
hd : dm₁ * dn₁ = dm₂ * dn₂
h₁ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0
h₂ : (dm₂ ∣ m ∧ m ≠ 0) ∧ dn₂ ∣ n ∧ n ≠ 0
⊢ dm₁ = dm₂

Tactic:
dvd_antisymm
    (hmn.coprime_dvd_left h₁.1.1 |>.coprime_dvd_right h₂.2.1
      |>.dvd_of_dvd_mul_right (hd ▸ dm₁.dvd_mul_right dn₁))
    (hmn.coprime_dvd_left h₂.1.1 |>.coprime_dvd_right h₁.2.1
      |>.dvd_of_dvd_mul_right (hd ▸ dm₂.dvd_mul_right dn₂))

Premises used: Nat.Coprime.coprime_dvd_left, dvd_antisymm, Eq.rec, And.right, And.left, Nat.dvd_mul_right, Eq.symm, Nat.Coprime.dvd_of_dvd_mul_right, Nat.Coprime.coprime_dvd_right
-- Module: Mathlib.Data.Finset.NatDivisors
Goal:
m n : ℕ
hmn : m.Coprime n
dm₁ dn₁ dm₂ dn₂ : ℕ
hd : dm₁ * dn₁ = dm₂ * dn₂
h₁ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0
h₂ : (dm₂ ∣ m ∧ m ≠ 0) ∧ dn₂ ∣ n ∧ n ≠ 0
⊢ dm₁ = dm₂

Tactic:
exact dvd_antisymm
    (hmn.coprime_dvd_left h₁.1.1 |>.coprime_dvd_right h₂.2.1
      |>.dvd_of_dvd_mul_right (hd ▸ dm₁.dvd_mul_right dn₁))
    (hmn.coprime_dvd_left h₂.1.1 |>.coprime_dvd_right h₁.2.1
      |>.dvd_of_dvd_mul_right (hd ▸ dm₂.dvd_mul_right dn₂))

Premises used: Nat.Coprime.coprime_dvd_left, dvd_antisymm, Eq.rec, And.right, And.left, Nat.dvd_mul_right, Eq.symm, Nat.Coprime.dvd_of_dvd_mul_right, Nat.Coprime.coprime_dvd_right
-- Module: Mathlib.Data.Finset.NatDivisors
Goal:
m n : ℕ
hmn : m.Coprime n
rw : (m * n).divisors = image (fun (p : ℕ × ℕ) ↦ p.1 * p.2) (m.divisors ×ˢ n.divisors)
rw₁ : (m * n).divisors = m.divisors * n.divisors
rw₂ rw₃ : m.divisors * n.divisors = m.divisors * n.divisors
⊢ (m * n).divisors =
    image (fun (p : ℕ × ℕ) ↦ p.1 * p.2)
      (image (Subtype.val (p := fun (x : ℕ × ℕ) ↦ x ∈ m.divisors ×ˢ n.divisors)) (m.divisors ×ˢ n.divisors).attach)

Tactic:
rw [Finset.attach_image_val, ← Finset.mul_def, Nat.divisors_mul]

Premises used: Nat.divisors_mul, Finset.mul_def, Finset.attach_image_val
-- Module: Mathlib.Data.Finset.NatDivisors
Goal:
m n : ℕ
hmn : m.Coprime n
rw :
  Eq (α := Finset ℕ)
    (image ((fun (p : ℕ × ℕ) ↦ p.1 * p.2) ∘ Subtype.val (p := fun (x : ℕ × ℕ) ↦ x ∈ m.divisors ×ˢ n.divisors))
      (m.divisors ×ˢ n.divisors).attach)
    (image
      (⇑{
            toFun := fun (p : { x : ℕ × ℕ // x ∈ (↑(m.divisors ×ˢ n.divisors) : Set (ℕ × ℕ)) }) ↦
              (↑p : ℕ × ℕ).1 * (↑p : ℕ × ℕ).2,
            inj' := ⋯ } :
        (a : { x : ℕ × ℕ // x ∈ (↑(m.divisors ×ˢ n.divisors) : Set (ℕ × ℕ)) }) → ℕ)
      (m.divisors ×ˢ n.divisors).attach)
⊢ Eq (α := Finset ℕ)
    (image (fun (p : ℕ × ℕ) ↦ p.1 * p.2)
      (image (Subtype.val (p := fun (x : ℕ × ℕ) ↦ x ∈ m.divisors ×ˢ n.divisors)) (m.divisors ×ˢ n.divisors).attach))
    (map
      {
        toFun := fun (p : { x : ℕ × ℕ // x ∈ (↑(m.divisors ×ˢ n.divisors) : Set (ℕ × ℕ)) }) ↦
          (↑p : ℕ × ℕ).1 * (↑p : ℕ × ℕ).2,
        inj' := ⋯ }
      (m.divisors ×ˢ n.divisors).attach)

Tactic:
rw [Finset.map_eq_image, Finset.image_image]

Premises used: Finset.map_eq_image, Finset.image_image
-- Module: Mathlib.Data.Finset.NatDivisors
Goal:
m n : ℕ
hmn : m.Coprime n
⊢ Eq (α := Finset ℕ)
    (image ((fun (p : ℕ × ℕ) ↦ p.1 * p.2) ∘ Subtype.val (p := fun (x : ℕ × ℕ) ↦ x ∈ m.divisors ×ˢ n.divisors))
      (m.divisors ×ˢ n.divisors).attach)
    (image
      (⇑{
            toFun := fun (p : { x : ℕ × ℕ // x ∈ (↑(m.divisors ×ˢ n.divisors) : Set (ℕ × ℕ)) }) ↦
              (↑p : ℕ × ℕ).1 * (↑p : ℕ × ℕ).2,
            inj' := ⋯ } :
        (a : { x : ℕ × ℕ // x ∈ (↑(m.divisors ×ˢ n.divisors) : Set (ℕ × ℕ)) }) → ℕ)
      (m.divisors ×ˢ n.divisors).attach)

Tactic:
rfl
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
f : α → β → β
l : List α
comm : Set.Pairwise {x : α | x ∈ (↑l : Multiset α)} fun (x y : α) ↦ ∀ (b : β), f x (f y b) = f y (f x b)
b : β
simp :
  List.foldr (fun (x : { x : α // x ∈ (↑l : Multiset α) }) ↦ f (↑x : α)) b
      (List.pmap (P := fun (x : α) ↦ x ∈ l) (Subtype.mk (p := fun (x : α) ↦ x ∈ l)) l ⋯) =
    List.foldr f b l
⊢ noncommFoldr f (↑l : Multiset α) comm b = List.foldr f b l

Tactic:
simp only [noncommFoldr, coe_foldr, coe_attach, List.attach, List.attachWith, Function.comp_def]

Premises used: List.attachWith, Multiset.coe_foldr, Multiset.noncommFoldr, Function.comp_def, List.attach, Multiset.coe_attach
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
f : α → β → β
l : List α
comm : Set.Pairwise {x : α | x ∈ (↑l : Multiset α)} fun (x y : α) ↦ ∀ (b : β), f x (f y b) = f y (f x b)
b : β
rw :
  List.foldr f b
      (List.map (Subtype.val (p := fun (x : α) ↦ x ∈ (↑l : Multiset α)))
        (List.pmap (P := fun (x : α) ↦ x ∈ l) (Subtype.mk (p := fun (x : α) ↦ x ∈ l)) l ⋯)) =
    List.foldr f b l
⊢ List.foldr (fun (x : { x : α // x ∈ (↑l : Multiset α) }) ↦ f (↑x : α)) b
      (List.pmap (P := fun (x : α) ↦ x ∈ l) (Subtype.mk (p := fun (x : α) ↦ x ∈ l)) l ⋯) =
    List.foldr f b l

Tactic:
rw [← List.foldr_map]

Premises used: List.foldr_map
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
f : α → β → β
l : List α
comm : Set.Pairwise {x : α | x ∈ (↑l : Multiset α)} fun (x y : α) ↦ ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ List.foldr f b
      (List.map (Subtype.val (p := fun (x : α) ↦ x ∈ (↑l : Multiset α)))
        (List.pmap (P := fun (x : α) ↦ x ∈ l) (Subtype.mk (p := fun (x : α) ↦ x ∈ l)) l ⋯)) =
    List.foldr f b l

Tactic:
simp [List.map_pmap]

Premises used: List.map_pmap
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
f : α → β → β
h : Set.Pairwise {x : α | Membership.mem (γ := Multiset α) 0 x} fun (x y : α) ↦ ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ noncommFoldr f 0 h b = b

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.noncommFoldr, Multiset.zero, Multiset.ofList, List.foldr, rfl
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
f : α → β → β
s : Multiset α
a : α
h : Set.Pairwise {x : α | x ∈ a ::ₘ s} fun (x y : α) ↦ ∀ (b : β), f x (f y b) = f y (f x b)
h' : Set.Pairwise {x : α | x ∈ s} fun (x y : α) ↦ ∀ (b : β), f x (f y b) = f y (f x b)
b : β
h₁ :
  ∀ (a_1 : List α) (h : Set.Pairwise {x : α | x ∈ a ::ₘ ⟦a_1⟧} fun (x y : α) ↦ ∀ (b : β), f x (f y b) = f y (f x b))
    (h' : Set.Pairwise {x : α | x ∈ ⟦a_1⟧} fun (x y : α) ↦ ∀ (b : β), f x (f y b) = f y (f x b)),
    noncommFoldr f (a ::ₘ ⟦a_1⟧) h b = f a (noncommFoldr f ⟦a_1⟧ h' b)
⊢ noncommFoldr f (a ::ₘ s) h b = f a (noncommFoldr f s h' b)

Tactic:
induction s using Quotient.inductionOn
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
f : α → β → β
a : α
b : β
a_1 : List α
h : Set.Pairwise {x : α | x ∈ a ::ₘ ⟦a_1⟧} fun (x y : α) ↦ ∀ (b : β), f x (f y b) = f y (f x b)
h' : Set.Pairwise {x : α | x ∈ ⟦a_1⟧} fun (x y : α) ↦ ∀ (b : β), f x (f y b) = f y (f x b)
⊢ noncommFoldr f (a ::ₘ ⟦a_1⟧) h b = f a (noncommFoldr f ⟦a_1⟧ h' b)

Tactic:
simp
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
f : α → β → β
s : Multiset α
h : LeftCommutative f
b : β
h₁ : ∀ (a : List α), noncommFoldr f ⟦a⟧ ⋯ b = foldr f b ⟦a⟧
⊢ noncommFoldr f s ⋯ b = foldr f b s

Tactic:
induction s using Quotient.inductionOn
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
f : α → β → β
h : LeftCommutative f
b : β
a : List α
⊢ noncommFoldr f ⟦a⟧ ⋯ b = foldr f b ⟦a⟧

Tactic:
simp
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
assoc : Std.Associative op
s : Multiset α
comm : Set.Pairwise {x : α | x ∈ s} fun (x y : α) ↦ op x y = op y x
x : α
hx : Membership.mem (γ := Set α) {x : α | x ∈ s} x
y : α
hy : Membership.mem (γ := Set α) {x : α | x ∈ s} y
h : x ≠ y
b : α
rw : op (op x y) b = op y (op x b)
rw₁ : op (op y x) b = op y (op x b)
rw₂ rw₃ : op y (op x b) = op y (op x b)
⊢ op x (op y b) = op y (op x b)

Tactic:
rw [← assoc.assoc, comm hx hy h, assoc.assoc]

Premises used: Std.Associative.assoc
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
op : α → α → α
assoc : Std.Associative op
l : List α
comm : Set.Pairwise {x : α | x ∈ (↑l : Multiset α)} fun (x y : α) ↦ op x y = op y x
a : α
⊢ noncommFold op (↑l : Multiset α) comm a = List.foldr op a l

Tactic:
simp [noncommFold]

Premises used: Multiset.noncommFold
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
op : α → α → α
assoc : Std.Associative op
h : Set.Pairwise {x : α | Membership.mem (γ := Multiset α) 0 x} fun (x y : α) ↦ op x y = op y x
a : α
⊢ noncommFold op 0 h a = a

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.noncommFoldr, Multiset.zero, Multiset.noncommFold, Multiset.ofList, List.foldr, rfl
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
op : α → α → α
assoc : Std.Associative op
s : Multiset α
a : α
h : Set.Pairwise {x : α | x ∈ a ::ₘ s} fun (x y : α) ↦ op x y = op y x
h' : Set.Pairwise {x : α | x ∈ s} fun (x y : α) ↦ op x y = op y x
x : α
h₁ :
  ∀ (a_1 : List α) (h : Set.Pairwise {x : α | x ∈ a ::ₘ ⟦a_1⟧} fun (x y : α) ↦ op x y = op y x)
    (h' : Set.Pairwise {x : α | x ∈ ⟦a_1⟧} fun (x y : α) ↦ op x y = op y x),
    noncommFold op (a ::ₘ ⟦a_1⟧) h x = op a (noncommFold op ⟦a_1⟧ h' x)
⊢ noncommFold op (a ::ₘ s) h x = op a (noncommFold op s h' x)

Tactic:
induction s using Quotient.inductionOn
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
op : α → α → α
assoc : Std.Associative op
a x : α
a_1 : List α
h : Set.Pairwise {x : α | x ∈ a ::ₘ ⟦a_1⟧} fun (x y : α) ↦ op x y = op y x
h' : Set.Pairwise {x : α | x ∈ ⟦a_1⟧} fun (x y : α) ↦ op x y = op y x
⊢ noncommFold op (a ::ₘ ⟦a_1⟧) h x = op a (noncommFold op ⟦a_1⟧ h' x)

Tactic:
simp
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
op : α → α → α
assoc : Std.Associative op
s : Multiset α
inst : Std.Commutative op
a : α
h : ∀ (a_1 : List α), noncommFold op ⟦a_1⟧ ⋯ a = fold op a ⟦a_1⟧
⊢ noncommFold op s ⋯ a = fold op a s

Tactic:
induction s using Quotient.inductionOn
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
op : α → α → α
assoc : Std.Associative op
inst : Std.Commutative op
a : α
a_1 : List α
⊢ noncommFold op ⟦a_1⟧ ⋯ a = fold op a ⟦a_1⟧

Tactic:
simp
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
l : List α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ (↑l : Multiset α)} Commute
simp : List.foldr (fun (x1 x2 : α) ↦ x1 * x2) 1 l = l.prod
⊢ noncommFold (fun (x1 x2 : α) ↦ x1 * x2) (↑l : Multiset α) comm 1 = l.prod

Tactic:
simp only [noncommFold_coe]

Premises used: Multiset.noncommFold_coe
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
comm : Set.Pairwise.{u_3} (α := α) {x : α | Membership.mem (γ := Multiset α) (↑[] : Multiset α) x} Commute
⊢ Eq.{u_3 + 1} (α := α) (List.foldr (fun (x1 x2 : α) ↦ x1 * x2) 1 []) (List.prod [])

Tactic:
simp
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
hd : α
tl : List α
hl :
  ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ (↑tl : Multiset α)} Commute),
    List.foldr (fun (x1 x2 : α) ↦ x1 * x2) 1 tl = tl.prod
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ (↑(hd :: tl) : Multiset α)} Commute
cons : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ (↑tl : Multiset α)} Commute
⊢ List.foldr (fun (x1 x2 : α) ↦ x1 * x2) 1 (hd :: tl) = (hd :: tl).prod

Tactic:
rw [List.prod_cons, List.foldr, hl]

Premises used: List.prod_cons, List.foldr
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
hd : α
tl : List α
hl :
  ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ (↑tl : Multiset α)} Commute),
    List.foldr (fun (x1 x2 : α) ↦ x1 * x2) 1 tl = tl.prod
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ (↑(hd :: tl) : Multiset α)} Commute
x : α
hx : Membership.mem (γ := Set α) {x : α | x ∈ (↑tl : Multiset α)} x
y : α
hy : Membership.mem (γ := Set α) {x : α | x ∈ (↑tl : Multiset α)} y
⊢ x ≠ y → Commute x y

Tactic:
comm (List.mem_cons_of_mem _ hx) (List.mem_cons_of_mem _ hy)

Premises used: List.mem_cons_of_mem
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
hd : α
tl : List α
hl :
  ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ (↑tl : Multiset α)} Commute),
    List.foldr (fun (x1 x2 : α) ↦ x1 * x2) 1 tl = tl.prod
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ (↑(hd :: tl) : Multiset α)} Commute
x : α
hx : Membership.mem (γ := Set α) {x : α | x ∈ (↑tl : Multiset α)} x
y : α
hy : Membership.mem (γ := Set α) {x : α | x ∈ (↑tl : Multiset α)} y
⊢ x ≠ y → Commute x y

Tactic:
exact comm (List.mem_cons_of_mem _ hx) (List.mem_cons_of_mem _ hy)

Premises used: List.mem_cons_of_mem
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
l : List α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ (↑l : Multiset α)} Commute
nil :
  ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | Membership.mem (γ := Multiset α) (↑[] : Multiset α) x} Commute),
    Eq.{u_3 + 1} (α := α) (List.foldr (fun (x1 x2 : α) ↦ x1 * x2) 1 []) (List.prod [])
cons :
  ∀ (hd : α) (tl : List α)
    (hl :
      ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ (↑tl : Multiset α)} Commute),
        List.foldr (fun (x1 x2 : α) ↦ x1 * x2) 1 tl = tl.prod)
    (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ (↑(hd :: tl) : Multiset α)} Commute),
    List.foldr (fun (x1 x2 : α) ↦ x1 * x2) 1 (hd :: tl) = (hd :: tl).prod
⊢ List.foldr (fun (x1 x2 : α) ↦ x1 * x2) 1 l = l.prod

Tactic:
induction l with
  | nil => simp
  | cons hd tl hl =>
    rw [List.prod_cons, List.foldr, hl]
    intro x hx y hy
    exact comm (List.mem_cons_of_mem _ hx) (List.mem_cons_of_mem _ hy)

Premises used: Multiset.cons, List.prod_cons, List.foldr