-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem prod_dvd_prod_of_subset_of_dvd [AddCommMonoid M] [CommMonoid N] {f1 f2 : α →₀ M}
    {g1 g2 : α → M → N} (h1 : f1.support ⊆ f2.support)
    (h2 : ∀ a : α, a ∈ f1.support → g1 a (f1 a) ∣ g2 a (f2 a)) : f1.prod g1 ∣ f2.prod g2

Proof state:
case h
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)
⊢ ∏ a ∈ f1.support, g1 a (f1 a) ∣ ∏ x ∈ f1.support, g2 x (f2 x)

Tactic:
apply prod_dvd_prod_of_dvd

Result:
case h.h
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)
⊢ ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)
⊢ f1.prod g1 ∣ f2.prod g2

Tactic:
classical
  simp only [Finsupp.prod, Finsupp.prod_mul]
  rw [← sdiff_union_of_subset h1, prod_union sdiff_disjoint]
  apply dvd_mul_of_dvd_right
  apply prod_dvd_prod_of_dvd
  exact h2

Result:
no goals

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)
⊢ ∏ a ∈ f1.support, g1 a (f1 a) ∣ ∏ a ∈ f2.support, g2 a (f2 a)

Tactic:
rw [← sdiff_union_of_subset h1, prod_union sdiff_disjoint]

Result:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)
⊢ ∏ a ∈ f1.support, g1 a (f1 a) ∣ (∏ x ∈ f2.support \ f1.support, g2 x (f2 x)) * ∏ x ∈ f1.support, g2 x (f2 x)

Proof state:
case h.h
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)
⊢ ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)

Tactic:
exact h2

Result:
no goals

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)
⊢ f1.prod g1 ∣ f2.prod g2

Tactic:
simp only [Finsupp.prod, Finsupp.prod_mul]

Result:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)
⊢ ∏ a ∈ f1.support, g1 a (f1 a) ∣ ∏ a ∈ f2.support, g2 a (f2 a)

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)
⊢ ∏ a ∈ f1.support, g1 a (f1 a) ∣ (∏ x ∈ f2.support \ f1.support, g2 x (f2 x)) * ∏ x ∈ f1.support, g2 x (f2 x)

Tactic:
apply dvd_mul_of_dvd_right

Result:
case h
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)
⊢ ∏ a ∈ f1.support, g1 a (f1 a) ∣ ∏ x ∈ f1.support, g2 x (f2 x)